Re: [isabelle] rigorous axiomatic geometry proof in Isabelle



Hi Bill,

transforming the raw Mizar texts is often painful. Depending on
the application, it is often better to transform the XML layer or
even the Prolog (MPTP) layer. A simple XSL stylesheet that
implements your mizar->isar function is now at
https://raw.github.com/JUrban/xsl4mizar/master/ISA/isa_main.xsl .

Use it as follows:

git clone git://github.com/JUrban/xsl4mizar.git

mizf joe.miz
xsltproc xsl4mizar/addabsrefs.xsl joe.xml > joe.xml1
xsltproc --param display_thesis \'0\' xsl4mizar/ISA/isa_main.xsl
joe.xml1 | html2text

You can extend it by overloading in isa_main.xsltxt the other
printing functions from MHTML/. The API description is at
http://mizar.org/version/current/doc/xml/Mizar.html . I can
probably help with some harder parts if this leads somewhere.

This can only get you so far. For the general issues with
transforming the Mizar dependent type system to HOL-like systems,
see Ondrej Kuncar's paper:
http://ktiml.mff.cuni.cz/~kuncar/kuncar-wds10.pdf .

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. If you are
interested in Coq, it also has a declarative Mizar-like mode, but it
is much less used than Isar.

And one more translation alternative: You could also ask the OMDoc
people (Florian Rabe I guess) about OMDoc->Isabelle export. They
do have quite fresh import of Mizar (using the XML layer).

Best,
Josef

On Sat, Apr 28, 2012 at 10:58 PM, Bill Richter
<richter at math.northwestern.edu> wrote:
> Hi, I'm a mathematician writing a rigorous axiomatic geometry paper
> http://www.math.northwestern.edu/~richter/hilbert.pdf
> using Hilbert's axioms.  I want to cite geometry proofs nicely coded
> and checked by proof-checker like Isabelle.  I've written Mizar code
> http://www.math.northwestern.edu/~richter/RichterTarskiMizar.tar
> 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.
>
> --
> Best,
> Bill
>





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