# 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.