Reasoning Techniques
Reasoning Techniques are IsaPlanner's equivalent to Isabelle's tactics, in other words functions that make a step in the proof. A reasoning technique is a function from one of IsaPlanner's reasoning states to a sequence (lazy list) of new reasoning states. Generic code for reasoning techinques is in src/base/rtechn.ML.
Making a Reasoning Technique
A basic reasoning techniques can be made from an Isabelle tactic. The tactic must first be lifted up to a declarative tactic (see src/rtechn/basic/dtac.ML). See src/rtechn/basic/isa_dtacs.ML for examples of tactics lifted to declarative tactics.
Once we have a declarative tactic we can create a reasoning technique with (see src/rtechn/basic/rtechn_env.ML):
If you would like to make a basic reasoning technique from a function on a reasoning state called f, then you want something like: (RTechnEnv.dummy_str is defined in src/rtechn/basic/rtechn_comb.ML) This will do the work of setting the continuation of none after the technique is applied and setting the description and trace information using the string description of the technique.
There are a range of combinators for reasoning techniques, allowing us to plug them together in different ways. The more basic ones are located in src/base/rtechn.ML and src/rtechn/rtechn_comb.ML. There are also some functions for combining reasoning techinques in src/rtechn/basic/rtechn_env.ML, these are mostly for managing application of different reasoning techniques to different goals etc. For example, to perform one technique r2 after another one r1 you would write: Making a Reasoning Technique from dtacs
(* apply dtac to a specific goal *)
val apply_dtac_to_g : DTac.T -> PPlan.gname -> RTechn.T
(* applies dtac to all current goals *)
val apply_dtac : DTac.T -> RTechn.T
(* apply, as or-choice, the dtacs to every goal *)
val apply_or_dtacs : DTac.T list -> RTechn.T
(* applies or-choice of dtacs to a goal (gives back applied dtac and rst *)
val apply_or_dtacs_to_g :
DTac.T list -> PPlan.gname -> RState.T -> (DTac.T * RState.T) Seq.seqMaking a Reasoning Technique functions on Reasoning States
RTechnEnv.dummy_str "name of my reasoning technique" o f
Combining Reasoning Techniques
r1 = ...
r2 = ...
local
open RTechnEnv;
in
val compound_r1_then_r2 = r1 thenr r2
end;