Re: [isabelle] Proof by analogy and proof stability in Isabelle



On Fri, 30 Apr 2010, Dave Thayer wrote:

What is the correct invocation to produce such a proof object?

Here is a minimal example:

  ML "proofs := 2"

  lemma a: "A --> A" by auto

  prf a
  full_prf a

Proof General also privides a menu item for setting "Full Proofs" -- it switches between "proofs := 0" and "proofs := 2".

If the system complains about "minimal proof object" you refer to lemmas within a proof that do not carry a full proof object themselves. The download image for Isabelle/HOL from the official Isabelle2009-1 distribution contains full proof objects for everything, but the flag is disabled in the very end, in order not to degrade user performance by default.


A nicer proof of "A --> A" can be produced like this:

  lemma b: "A --> A" ..

  prf b
  full_prf b

This also works for less trivial structered proofs, e.g. see the proofs in src/HOL/Isar_Examples/Knaster_Tarski.thy -- the proof terms still make sense. The Isar proof language does not involve any "magic" by itself, but allows to appeal to arbitrary complex proof tools in clearly isolated positions, e.g. the "by auto" above.


	Makarius






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