*To*: Lionel Elie Mamane <lionel at mamane.lu>*Subject*: Re: [isabelle] See the proof of a theorem*From*: Makarius <makarius at sketis.net>*Date*: Fri, 8 Aug 2008 12:31:52 +0200 (CEST)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <20080807140120.GA29170@capsaicin.mamane.lu>*References*: <20080807140120.GA29170@capsaicin.mamane.lu>

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

**References**:**[isabelle] See the proof of a theorem***From:*Lionel Elie Mamane

- Previous by Date: Re: [isabelle] A question on isabelle/HOL
- Next by Date: [isabelle] Sledgehammer and HOL-Complex
- Previous by Thread: [isabelle] See the proof of a theorem
- Next by Thread: [isabelle] A question on isabelle/HOL
- Cl-isabelle-users August 2008 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list