*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle*From*: Bill Richter <richter at math.northwestern.edu>*Date*: Fri, 25 May 2012 00:12:42 -0500*In-reply-to*: Bill Richter*References*: <201204282058.q3SKw9NF008441@poisson.math.northwestern.edu> <CAFP4q14YwNi6RksUOkGNGWYYzkNi3ca92FH4kYW19kJeOBcT2Q@mail.gmail.com> <alpine.LNX.2.00.1204301125350.6594@macbroy21.informatik.tu-muenchen.de> <201205020207.q4227VoC013147@poisson.math.northwestern.edu> <4FA0A63C.7030904@jaist.ac.jp> <201205020409.q42497Ou014411@poisson.math.northwestern.edu> <4FA0BBE7.4060302@jaist.ac.jp> <201205030338.q433ciL9026861@poisson.math.northwestern.edu>

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

**Follow-Ups**:**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Makarius

**References**:**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Bill Richter

**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Christian Sternagel

**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Bill Richter

**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Christian Sternagel

**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Bill Richter

- Previous by Date: [isabelle] Announcing Isabelle2012
- Next by Date: [isabelle] avoid rechecking an imported theory
- Previous by Thread: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
- Next by Thread: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
- Cl-isabelle-users May 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list