Re: [isabelle] rigorous axiomatic geometry proof in Isabelle



Dear Bill,

On 05/02/2012 11:07 AM, Bill Richter wrote:
I ran the executable ./Isabelle and up popped jedit.  I pasted in
Isabelle code from Tim's master's thesis into Scratch.thy.  There's
extensive jedit help on the Help menu, but I couldn't figure out how
to compile my buffer.
As soon as you open a theory file (extension ".thy") with jEdit, it is constantly "checked" (even in parallel, for lemmas that are not dependent in a linear fashion). (There is a thin column next to the main text buffer, where the total progress or errors are indicated. Furthermore, errors are marked by red wavy lines inside the text buffer.)

On a more general note. In principle I would strongly suggest to start with trivial proofs in order to get acquainted with the mechanisms of Isabelle. And only afterwards try to formalize something serious.

Concerning some of the points you mentioned:

- PDFs or HTML sites that are generated from Isabelle theory files often use slightly different symbols/notation than is actually used as input. A good way to get "the real thing" is having a look (e.g., with jEdit) at the example theory files that are located in <Isabelle directory>/src/HOL/ex/.

- In parallel to referring to reference manuals (like isar-ref) it is a good idea to read more tutorial-like texts, e.g., tutorial.pdf and isar-overview.pdf, that are part of the documentation of Isabelle.

- It is mostly your own decision how big the steps of a proof are. You can do single steps (using the "rule" method) which results in huge undigestable proofs. Or you can use methods like "simp" (equational reasoning), "blast" (logical reasoning which should succeed on many first-order proofs), "auto" (somewhat a combination of the previous two), "induction" (for ... well, induction), "cases" (for case analysis). (In courses it is often done that students are only allowed to use certain rules in order to proof a statement, since the automatic tools would outright solve many typical examples.)

hope this helps,

chris





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