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