Re: [isabelle] rigorous axiomatic geometry proof in Isabelle



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 





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