*To*: Bill Richter <richter at math.northwestern.edu>*Subject*: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle*From*: Makarius <makarius at sketis.net>*Date*: Fri, 25 May 2012 12:00:52 +0200 (CEST)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <201205250512.q4P5Cgns004328@poisson.math.northwestern.edu>*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> <201205250512.q4P5Cgns004328@poisson.math.northwestern.edu>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Fri, 25 May 2012, Bill Richter wrote:

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

I made the change, and now jedit gives an error, with do-not-enters onthe 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?

Here is my proof with the amended locale definition: lemma C1: assumes neq: "a ≠ b" and Bet1: "Bet a b y" and Bet2: "Bet a b x" and b: "b x ≐ b y" shows "y = x" proof - have "y x ≐ y y" using neq Bet2 Bet1 _ b proof (rule A5) show "a b y ≐≐ a b y" .. qed then show ?thesis by (rule A3) qed

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.

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 suchpoints x, with center b and radius length by.

Makarius

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

**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

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

- Previous by Date: Re: [isabelle] avoid rechecking an imported theory
- Next by Date: [isabelle] Add abbreviations in jEdit
- 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