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.


	Makarius






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