*To*: Bill Richter <richter at math.northwestern.edu>*Subject*: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle*From*: Josef Urban <josef.urban at gmail.com>*Date*: Mon, 30 Apr 2012 00:48:32 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <201204282058.q3SKw9NF008441@poisson.math.northwestern.edu>*References*: <201204282058.q3SKw9NF008441@poisson.math.northwestern.edu>

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 >

**Follow-Ups**:**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Bill Richter

**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Makarius

**References**:**[isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Bill Richter

- Previous by Date: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
- Next by Date: Re: [isabelle] Using Isar on Induction
- Previous by Thread: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
- Next by Thread: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
- Cl-isabelle-users April 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list