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? 

A few things confuse me about your code, e.g.

  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.