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
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" ..
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and