Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
On 05/02/2012 11:07 AM, Bill Richter wrote:
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.)
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.
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
- 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,
This archive was generated by a fusion of
Pipermail (Mailman edition) and