Email Gateway (Aug 18 2022 at 12:17): Email Gateway (Aug 18 2022 at 12:17):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 18 2022 at 12:21):From: Lionel Elie Mamane <lionel@mamane.lu>
Hi,
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.)
Thanks for the information,
Last updated: Nov 21 2024 at 12:39 UTC