Re: [isabelle] rigorous axiomatic geometry proof in Isabelle



Thanks, Makarius, and I really like your posts on hol info.  I'd be
happy for you to post there about miz3 ocaml dirty code cache issues.

   The Isabelle/Pure framework is centered around higher-order natural
   deduction, and Isabelle/Isar as a proof language continues these
   ideas. To understand these things properly, you should first blot
   out "FOL", then get used to Pure + Isar, then add HOL as
   object-logic, and then rediscover what predicate logic (including
   FOL) will do for you here via some add-on tools.

I'm not opposed to learning Pure + Isar, but it would be a whole lot
easier for me to learn if I knew in advance how it related to FOL,
which as a mathematician I have a rudimentary (but not practical)
understanding of.  Let me make a rudimentary FOL point:

I think writing down strict axiomatic FOL proofs would really be
tedious because e.g. you have manually substitute variables every time
you want to use an axiom.  I don't have a full list of the tedium
strict FOL can cause.  But I'm only willing to write up FOL-type
proofs if the proof assistant will automate that tedium.  Do similar
issues arise with Pure + Isar?

Also, as you may have observed on hol info, I know next to nothing
about HOL.  Basically I understand the 20 pages of set theory John
explains in his reference manual.  Isn't Isabelle HOL much the same as
HOL as in HOL Light HOL?  Where is a good place to learn about HOL?

   > 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.

   In principle any of the HOL systems could provide their own locale
   mechanism, or something similar.  It is not possible to "just" do
   it, though.  Isabelle has required 10+ years to get this all done
   right. It is also a matter of culture.  John Harrison would
   certainly not add such complexity to his system.  You have to use
   Isabelle or Coq for such sophisticated module concepts, or maybe
   Mizar.

Sure, but I really dislike the Mizar type system, and I want to
lightly typed sets to avoid any hard typing.  More below: 


   > 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?

   If this means you want to study the meta-theory of Tarski axioms,
   then any of the HOL systems -- Isabelle/HOL included -- can do this
   for you, if you define the syntax and inference system more
   concretely (via datatypes and inductive relations).

Great, but I don't know what meta-theory means.  A model of Tarski's
geometry axioms is be a set S (of points), a 3-ary relation Between on
S and a 4-ary relation Equiv on S satisfying Tarski's axioms (so far I
only use his first 7 axioms, and you coded them up in Isabelle).  So
there might be a predicate TarskiModel(S, Between, Equiv), and
theorems in a Tarski model would begin

assume TarskiModel(S, Between, Equiv)...

I don't understand HOL well enough to actually pull this off, but John
explained how to get started.  My point is that I don't think any
typing is involved here, beyond maybe something rudimentary like

new_type("point",0);;
new_type_abbrev("TarskiPlane",`:point->bool`);;

-- 
Best,
Bill 





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