Reasoning States

Reasoning states are snapshots of the proof planning process. They contain the current proof plan, the continuation technique that will be applied next, and contextual information. The proof plan holds the proof so far, the continuation is a reason techniques, and the contextual information is table which holds extra non-logical information such as a cache of the proved lemmas, rippling annotations, and information about goals for which there is a known counter-example.

Functions and Tools on Reasoning States

These are defined in two files:

• src/base/rstate.ML -- this has the basic get/set functions for reasoning states

• rtechn/basic/rst_pp.ML -- this has many derived tools for reasoning states (and proof plans), such as checking if all goals are proved.

Example of how to get an Isabelle theorem from a reasoning state which contains a proof:

(* Load up the natural number theory *)
use_thy "examples/N"; val thry = theory "N";

(* create initial reasoning state *)
val result_name = "a";
val rst0 = PPInterface.init_rst thry (result_name, "a + b = b + (a::N)")
            |> RState.set_rtechn (SOME (RippleLemCalc.induct_ripple_lemcalc result_name));

(* find the proof *)
val my_thm = 
  case Seq.pull (PPInterface.depth_fs rst0)
   of NONE => raise ERROR "no proof found!"
    | SOME (rst, moreproofs) => RstPP.result_thm rst result_name;