Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
On Sun, 27 May 2012, Bill Richter wrote:
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?
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
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.
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?
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and