# Re: [isabelle] rigorous axiomatic geometry proof in Isabelle

```Makarius ported to Isabelle 100+ lines (below) of my HOL-Light/miz3
code I posted here on May 20, which is more or less a port of Julien
Narboux's Coq pseudo-code.  I'm thrilled the Isabelle maintainers took
such an interest in Tarski axiomatic geometry:

M> I've spent maybe 1 or 2 hours on the various versions of the Tarski
M> axiomatization by Bill, Julien Narboux, John Harrison, and
M> Wikipedia.  Bill had a slight divergence in some details in his 2
M> or 3 versions that I did not follow to the bottom.

Makarius's port proved a theorem that's false, the last theorem below,
C1.  The problem seems to be Makarius's axiom

A5: "a ≠ b ⟹ Bet a b c ⟹ Bet a' b' c' ⟹ a b c ≐≐ a' b' c' ⟹
b d ≐ b' d' ⟹ c d ≐ c' d'"

I think this is my error, from my Isabelle file 6Tarski.thy, which I
think I posted here.  My deepest apologies!  I should have written

and A5: "∀ a b c d a' b' c' d' . not(a = b) ∧ B a b d ∧ B a' b' d'
∧ a b ≡ a' b' ∧ b c ≡ b' c' ∧ a d ≡ a' d' ∧ b d ≡ b' d'
=⇒ c d ≡ c' d'"

which is basically Tarksi's version of the SAS axiom (which Tarski
cleverly defined without having angles!), which I got right in miz3

let A5 = new_axiom
`!a b c d a' b' c' d'.
~(a = b) /\ a,b,c cong a',b',c' /\
Between(a,b,d) /\ Between(a',b',d') /\ b,d === b',d'
==> c,d === c',d'`;;

Makarius, I think you needed
Bet a b d ⟹ Bet a' b' d',
but you sure did a whole better than I did!  I couldn't even get the
axiom locale to work, or prove anything.  I made the change, and now
jedit gives an error, with do-not-enters on the last 4 lines:

with neq Bet Bet have "y x ≐ y y" using `b x ≐ b y` by (rule A5)
then show ?thesis by (rule A3)
qed

end

So I uncommented the assumption
and "Bet a b x"
but I still get these 4 do-not-enters.  Uh, would you try try again?

defines "a b c ≐≐ x y z ≡ a b ≐ x y ∧ a c ≐ x z ∧ b c ≐ y z"

So ≡ means "if and only if", which in HOL-Light is <=>?

Two of Tarski's first 7 axioms are constructive (some point x exists),
A4 and A7, and you proved rules for them, using what I thought was a
very powerful automation tool blast:

lemma A4_rule: obtains x where "Bet q a x" and "a x ≐ b c"
using A4 by blast

and then used A4 by e.g. writing

obtain x where x: "Bet q a x" "a x ≐ a a" by (rule A4_rule)

Hmm, you don't have to do that in Mizar or Freek's miz3.

Now I ran your code in the spanking new Isabelle:

(poisson)Isabelle2012> ./Isabelle ../Tarski.thy &

I'm a newbie, but it sure looks to me that jedit thinks your code is
perfect.  Let me explain why your last result shouldn't be true:

lemma C1:
assumes neq: "a ≠ b"
and Bet: "Bet a b y"
(*  and "Bet a b x"    -- "FIXME unused"  *)
and "b x ≐ b y"
shows "y = x"
proof -
have 1: "a b ≐ a b" ..
have 2: "b y ≐ b y" ..
have "a b y ≐≐ a b y" ..
with neq Bet Bet have "y x ≐ y y" using `b x ≐ b y` by (rule A5)
then show ?thesis by (rule A3)
qed

Tarski's axioms hold in the plane R^2, in which the result means this.

Let `l' be the line containing two distinct points `a' and `b'.  Take
`y' to be a point on `l' so that b is between a and y.  (That means
that y can equal b.)   Now take a point x in the plane so that
length bx = length by.
Then x = y.

Of course that's false (unless y = b).  There's a whole circle of such
points x, with center b and radius length by.

--
Best,
Bill

theory Tarski
imports Main
begin

locale tarski_first7 =
fixes Cong :: "'p \<Rightarrow> 'p \<Rightarrow> 'p \<Rightarrow> 'p \<Rightarrow> bool"  ("_ _ \<doteq> _ _" [1000, 1000, 1000, 1000] 50)
fixes Cong3  ("_ _ _ \<doteq>\<doteq> _ _ _" [1000, 1000, 1000, 1000, 1000, 1000] 50)
defines "a b c \<doteq>\<doteq> x y z \<equiv> a b \<doteq> x y \<and> a c \<doteq> x z \<and> b c \<doteq> y z"
fixes Bet :: "'p \<Rightarrow> 'p \<Rightarrow> 'p \<Rightarrow> bool"
assumes A1: "a b \<doteq> b a"
and A2: "a b \<doteq> p q \<Longrightarrow> a b \<doteq> r s \<Longrightarrow> p q \<doteq> r s"
and A3: "a b \<doteq> c c \<Longrightarrow> a = b"
and A4: "\<exists>x. Bet q a x \<and> a x \<doteq> b c"
and A5: "a \<noteq> b \<Longrightarrow> Bet a b c \<Longrightarrow> Bet a' b' c' \<Longrightarrow> a b c \<doteq>\<doteq> a' b' c' \<Longrightarrow>
b d \<doteq> b' d' \<Longrightarrow> c d \<doteq> c' d'"
and A6: "Bet a b a \<Longrightarrow> a = b"
and A7: "Bet a p c \<Longrightarrow> Bet b q c \<Longrightarrow> \<exists>x. Bet p x b \<and> Bet q x a"
begin

definition "is_ordered a b c d \<longleftrightarrow>
Bet a b c \<and> Bet a b d \<and> Bet a c d \<and> Bet b c d"

definition on_line  ("_ on'_line _ _" [1000, 1000, 1000] 50)
where "x on_line a b \<longleftrightarrow>
a \<noteq> b \<and> (Bet a b x \<or> Bet a x b \<or> Bet x a b)"

definition equal_line  (" _ _ equal'_line _ _" [1000, 1000, 1000, 1000] 50)
where "a b equal_line x y \<longleftrightarrow>
a \<noteq> b \<and> x \<noteq> y \<and> (\<forall>c. c on_line a b \<longleftrightarrow> c on_line x y)"

lemma A4_rule: obtains x where "Bet q a x" and "a x \<doteq> b c"
using A4 by blast

lemma A7_rule:
assumes "Bet a p c" and "Bet b q c"
obtains x where "Bet p x b" and "Bet q x a"
using assms and A7 by blast

lemma Cong_refl [intro, simp]:
"a b \<doteq> a b"
proof -
have "b a \<doteq> a b" by (rule A1)
from this this show ?thesis by (rule A2)
qed

lemma Cong_sym [sym]:
assumes "a b \<doteq> c d"
shows "c d \<doteq> a b"
proof -
have "a b \<doteq> a b" ..
with assms show ?thesis by (rule A2)
qed

lemma Cong_trans [trans]:
assumes "p q \<doteq> a b"
and "a b \<doteq> r s"
shows "p q \<doteq> r s"
proof -
from `p q \<doteq> a b` [symmetric] and `a b \<doteq> r s`
show ?thesis by (rule A2)
qed

lemma Cong3I:
assumes "a b \<doteq> x y" and "a c \<doteq> x z" and "b c \<doteq> y z"
shows "a b c \<doteq>\<doteq> x y z"
using assms unfolding Cong3_def by blast

lemma Cong3E:
assumes "a b c \<doteq>\<doteq> x y z"
obtains "a b \<doteq> x y" and "a c \<doteq> x z" "b c \<doteq> y z"
using assms unfolding Cong3_def by blast

lemma Cong3_refl [intro, simp]:
"a b c \<doteq>\<doteq> a b c"
by (blast intro: Cong3I)

lemma Bet_aaa:
"Bet a a a" and "a a \<doteq> b b"
proof -
obtain x where x: "Bet a a x" "a x \<doteq> b b" by (rule A4_rule)
from x(2) have "a = x" by (rule A3)
from this [symmetric] and x show "Bet a a a" and "a a \<doteq> b b" by simp_all
qed

lemma Bqaa: "Bet q a a"
proof -
obtain x where x: "Bet q a x" "a x \<doteq> a a" by (rule A4_rule)
note `Bet q a x`
also have [symmetric]: "a = x" using `a x \<doteq> a a` by (rule A3)
finally show ?thesis .
qed

lemma C1:
assumes neq: "a \<noteq> b"
and Bet: "Bet a b y"
(*  and "Bet a b x"    -- "FIXME unused"  *)
and "b x \<doteq> b y"
shows "y = x"
proof -
have 1: "a b \<doteq> a b" ..
have 2: "b y \<doteq> b y" ..
have "a b y \<doteq>\<doteq> a b y" ..
with neq Bet Bet have "y x \<doteq> y y" using `b x \<doteq> b y` by (rule A5)
then show ?thesis by (rule A3)
qed

end

```

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