Re: [isabelle] See the proof of a theorem



On Thu, 7 Aug 2008, Lionel Elie Mamane wrote:

> Is there any command to see / dump / pretty-print a (partial) proof in
> Isabelle? What I mean is:
> 
>  - Before one has done "qed", while one is proving a theorem, there is
>    (I presume) a partial proof somewhere in the internals of the
>    system; maybe in the shape of a \lambda-term with (typed) holes /
>    placeholders, or in the shape of a tree of what rule / tactic
>    brought what proof state to what proof state, or both.
> 
>    Can I see that partial proof? (People that know Coq will recognise
>    the "Show Proof." and "Show Tree." commands of Coq.)
> 
> 
>  - After one has done the "qed", the same data as before, except that
>    there will be proof will be complete.
> 
>    (Something like "Print theorem_name." in Coq.)

Isabelle is not as constructivistic as Coq, especially the Isar layer is 
very platonistic, with many non-logical ideas being expressed as abstract 
datatypes instead of lambda terms.  This means there is not a single 
concrete "term" structure that holds all the information.  It depends on 
your application which kind of proof information you want to retrieve from 
the system.

For example, consider the following Isar proof:

lemma "A & B --> B & A"
proof
  assume "A & B"
  then obtain B and A ..
  then show "B & A" ..
qed

The "real" Isar proof is just the source as shown here -- Isabelle does 
not store it in that form, you need to refer to the UI / editor to get 
hold of it.

The internal Isar representation of a partially proof text can be 
retrieved at any point like this:

  ML_val {* Toplevel.proof_of (Isar.state ()) *}

but this gives the the abstract datatype only (with operations provided in 
src/Pure/Isar/proof.ML).

Alternatively you may look at the primitive derivation objects behind 
parts of Isar proofs.  E.g. like this:


ML "proofs := 2"

lemma a: "A & B --> B & A"
proof
  assume "A & B"
  prf this
  then obtain B and A ..
  prf this
  then show "B & A" ..
  prf this
qed

prf a


You may also want to look at the goal states (there can be many of them at 
each level of the structure).  Cf. ML {* Isar.goal () *}


	Makarius






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.