Re: [isabelle] rigorous axiomatic geometry proof in Isabelle

Jeremy, if you or anyone else wants to talk about Euclid off-line, I'd
be happy to talk.  As I try to explain in my paper, I love the Elements
It's very creative and forms the basis of non-Euclidean geometry.

Thanks, Chris, that's very helpful.  I'll look for the red wavy error
lines in jedit.  I'll look at /src/HOL/ex/.  I've looked at
tutorial.pdf, but I'll look again, and isar-overview.pdf sounds good.
Thanks for explaining simp, blast etc, although I don't really know
what you mean.  Is there somewhere an FOL example, with a long
(perhaps indigestible) single step "rule" method proof, which is
shortened with simp, and then shortened even more with blast & auto?

   (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.)

Wow!  Can you point me to any of these courses?  That sounds like what
I need to know.  As I posted earlier, I'm mostly trying to cite some
good code for my geometry paper above (which I'll then submit).  I
don't have to write the code myself, although I did
Examples of real classroom situations where students hand in Isabelle
proofs would be fantastic!  Dunno about Europe, but US public schools
are really gungho about computer applications.


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