Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
On Wed, 30 May 2012, Bill Richter wrote:
I'd be happy for you to post there about miz3 ocaml dirty code cache
Better not. I did not really follow that detail of this highly complex
thread. It is part of the miz3 philosophy to do things in a certain way,
and Freek has a right to take his preferred way.
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)
In my rough "education plan" above, the relation to FOL was the last step,
not the first one. It is easier to get started with a clear mind.
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?
I can only guess what you mean by "strict axiomatic FOL proof". There are
many ways to define what a logical inference system is, and how proofs are
In Isabelle Pure it is done over lambda-calculus as syntax, and via
backchaining of natural deduction rules with implicit unification to solve
the instantiation problems arising here. BTW, Isar means "Intelligible
semi-automated reasoning", because the only proof automation built into
the proof language is unification, which is typically used together with
implicit selection of rules from the context (library etc.) as determined
from the structure of the text. That's the whole secret of it.
Any other proof automation is quoted explicitly in the Isar text, via
"proof methods": blast, simp, auto, metis, smt, ... ad infinitum. You go
to the store and order the kind of washing machine you prefer, or do
things purely by hand ...
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?
You should not spend to much time with that. If you take HOL as a
simplified version of set-theory with explicit syntactic types it is OK as
a start. Foundationally, HOL is not so interesting than it was in 1940 or
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
Sure, but I really dislike the Mizar type system, and I want to
lightly typed sets to avoid any hard typing.
Note that HOL typing is particularly hard. Every type is its own isolated
universe, although a rather small one. You need explicit morphisms to
travel between such distinct worlds.
> 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
You get such a predicate already from the locale tarski_first7 that I've
produced for you. It is called "tarski_first7" and can be used within the
The system will check that and print the most general type for it:
"('a ⇒ 'a ⇒ 'a ⇒ 'a ⇒ bool) ⇒ ('a ⇒ 'a ⇒ 'a ⇒ bool) ⇒ bool". You
can also hover over the formal term to get it explained.
Note that the type is naturally curried as everything by default in
Isabelle Pure -- just like in good HOL families.
Moreover your carrier set S is actually modeled as a type here, in the
usual manner in HOL. You can relativize it to a set over the base type,
but that is a different story of the larger HOL family.
assume TarskiModel(S, Between, Equiv)...
This is what the locale context "begin" does for you implicitly, and then
you start to define derived things and state theorems and do proofs from
it. This means you are developing a concrete "theory", but this is not
Meta theory means you speak about things, by stepping aside or outside
from it. Here is an arbitrary example from AFP, which I have happened to
have browsed two weeks ago with a student:
The example develops the logical inference system and semantics of a
version of first-order logic in the usual way, almost literally from the
book (I don't know which one). There are just the usual formalization
tweaks to represent it as concrete formal things inside HOL (and a slight
tendency of redundant copies of basic mathematical HOL concepts used in
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
That is a global axiomatic theory. In Isabelle/HOL is would look like
Cong :: "point ⇒ point ⇒ point ⇒ point ⇒ bool" ("_ _ ≐ _ _" [1000,
1000, 1000, 1000] 50) and
Cong3 ("_ _ _ ≐≐ _ _ _" [1000, 1000, 1000, 1000, 1000, 1000] 50) and
Bet :: "point ⇒ point ⇒ point ⇒ bool"
Cong3_def: "a b c ≐≐ x y z ≡ a b ≐ x y ∧ a c ≐ x z ∧ b c ≐ y z"
and A1: "a b ≐ b a"
and A2: "a b ≐ p q ⟹ a b ≐ r s ⟹ p q ≐ r s"
and A3: "a b ≐ c c ⟹ a = b"
and A4: "∃x. Bet q a x ∧ a x ≐ b c"
and A5: "a ≠ b ⟹ Bet a b d ⟹ Bet a' b' d' ⟹ a b c ≐≐ a' b' c' ⟹
b d ≐ b' d' ⟹ c d ≐ c' d'"
and A6: "Bet a b a ⟹ a = b"
and A7: "Bet a p c ⟹ Bet b q c ⟹ ∃x. Bet p x b ∧ Bet q x a"
Showing that publicly on isabelle-users, most people should frown upun it
-- shudder. There are all these sophisticated ways to make things local
in Isabelle ...
This archive was generated by a fusion of
Pipermail (Mailman edition) and