Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] See the proof of a theorem

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: May 03 2024 at 08:18 UTC