Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
On Mon, 30 Apr 2012, Josef Urban wrote:
It might also be easier for you to first transform your code to HOL
Light's Mizar mode, because it does not have the keyword
incompatibilities that Isar introduced, and it has quite faithful
implementation of the Mizar "by" inference. In Isabelle, you could later
try to replace such calls with "metis" calls.
These are not "keyword incompatibilities", but fundamental differences in
the approach to structured proofs, and the meaning of the language
elements. It all follows Isabelle/Pure and its higher-order natural
deduction environment. Similarities with Mizar and other "declaritive
proof" modes are quite superficial. I never use the "declarative"
terminolgy for Isar, it does not quite fit what it actually is.
In particular, their is no built-in automation in Isar. Users can draw on
an existing repertoire of proof methods taken from the library, such as
"metis" in Isabelle/HOL, but they don't have to.
This archive was generated by a fusion of
Pipermail (Mailman edition) and