*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle*From*: Bill Richter <richter at math.northwestern.edu>*Date*: Sun, 27 May 2012 03:18:30 -0500*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <alpine.LNX.2.00.1205251146380.8953@macbroy22.informatik.tu-muenchen.de> (message from Makarius on Fri, 25 May 2012 12:00:52 +0200 (CEST))*References*: <201204282058.q3SKw9NF008441@poisson.math.northwestern.edu> <CAFP4q14YwNi6RksUOkGNGWYYzkNi3ca92FH4kYW19kJeOBcT2Q@mail.gmail.com> <alpine.LNX.2.00.1204301125350.6594@macbroy21.informatik.tu-muenchen.de> <201205020207.q4227VoC013147@poisson.math.northwestern.edu> <4FA0A63C.7030904@jaist.ac.jp> <201205020409.q42497Ou014411@poisson.math.northwestern.edu> <4FA0BBE7.4060302@jaist.ac.jp> <201205030338.q433ciL9026861@poisson.math.northwestern.edu> <201205250512.q4P5Cgns004328@poisson.math.northwestern.edu> <alpine.LNX.2.00.1205251146380.8953@macbroy22.informatik.tu-muenchen.de>

Thanks, Makarius, I'll run your code and study it. Is this explained somewhere in the Isabelle dox, or could you explain it better: We are doing precise single step reasoning here, which means all the slots for the rules need to be filled in the correct order. This is not Mizar or any of the Mizar modes for HOL, which are centered around classic predicate logic with some builtin proof automation to bridge larger gaps. I would have said FOL instead of predicate logic, does that mean the same? I'm not an expert in FOL, but I think FOL proofs tend to be very tedious, and the builtin Mizar proof automation turns these FOL proofs into something that is a real pleasure to code up. Is that right? And Isabelle (Isar?) is doing something different from that? > Of course that's false (unless y = b). There's a whole circle of > such points x, with center b and radius length by. That is an informal argument. It merely motivates why something in the formalization had to be amended. Absolutely! In Mizar or miz3, it would have intruded the proof, and the mistake in your A5 would not have been discovered. I bet it would have been discovered! I wrote 1500 lines of Mizar proofs (slimmed down to 1000 miz3 lines), that's bound to shake out bugs in the axioms. (You did not have it in the miz3 version that you sent me, but in the Isabelle attempt.) Let me apologize again for sending you the busted A5 Isabelle code. This is why unguarded axiomatizations are so dangerous. Here we made a locale definition instead, and in the worst case the corresponding predicate tarski_first7 could turn out to be always False, not more no less. Yes, and thus locales are definitely a real advantage of Isabelle over HOL Light right now. Still, I wonder why one can't just define all the sets you'd want in HOL Light (only very lightly typed) to get something like a locale. That is, I think of your locale as something close to FOL Tarski axiomatic geometry proofs. But instead we could look at all models of Tarski's axioms, a model being some sets and functions with some properties. Can you do this in Isabelle too? -- Best, Bill

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

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

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

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

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

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

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

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

- Previous by Date: [isabelle] AFP 2012
- Next by Date: [isabelle] Isabelle/jEdit: Multiline Comments/Reparsing
- 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 May 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