[isabelle] rigorous axiomatic geometry proof in Isabelle

Hi, I'm a mathematician writing a rigorous axiomatic geometry paper
using Hilbert's axioms.  I want to cite geometry proofs nicely coded
and checked by proof-checker like Isabelle.  I've written Mizar code
and I want to port it to Isabelle, which Freek Wiedijk seems to
suggest is an improvement.  Makarius has been helping me, and he said
I should ask here about formalizations of geometry.  My feeling, which
could be mistaken, is that Coq and HOL Light are primarily
theorem-provers (procedural) and require considerable tweaking to
allow folks to type in readable axiomatic geometry (declarative)
proofs, but that Isabelle is both procedural and declarative.  

My Mizar code is a largely a port of Julien Narboux's Coq pseudo-code
http://dpt-info.u-strasbg.fr/~narboux/tarski.html.  I partially prove
the theorem of the 1983 book Metamathematische Methoden in der
Geometrie by Schwabhäuser, Szmielew, and Tarski, that Tarski's
(extremely weak!) plane geometry axioms imply Hilbert's axioms.  I get
about as far as Narboux, with Gupta's amazing proof which implies
Hilbert's axiom I1 that two points determine a line.  I don't think my
Mizar code is that great, but it's a lot more readable than Julien's
Coq pseudo-code.  No doubt some Mizar experts could improve my code,
but I'm putting them off as a last resort, because Mizar seems
unsuitable as a language to use in a high school math class.

So I'd appreciate your Isabelle help, including the easiest way run
Isabelle programs.  Do I really need Proof General?  I'll also accept
geometry help!  I haven't seen Schwabhäuser's book, and I can't see
how to go any farther with Tarski's axioms.  I'm basically missing
Hilbert's Pasch Betweenness axiom (Tarski's axiom is about 1/3 of it)
and Hilbert's angle construction axiom.


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