Theory Tarski

(*  Title:       Tarski's geometry
    Author:      Tim Makarios <tjm1983 at gmail.com>, 2012
    Maintainer:  Tim Makarios <tjm1983 at gmail.com>
*)

section "Tarski's geometry"

theory Tarski
  imports Complex_Main Miscellany Metric
begin

subsection "The axioms"
text ‹The axioms, and all theorems beginning with \emph{th}
  followed by a number, are based on corresponding axioms and
  theorems in cite"schwabhauser".›

locale tarski_first3 =
  fixes C :: "'p  'p  'p  'p  bool"     ("_ _ \<congruent> _ _" [99,99,99,99] 50)
  assumes A1: "a b. a b \<congruent> b a"
  and A2: "a b p q r s. a b \<congruent> p q  a b \<congruent> r s  p q \<congruent> r s"
  and A3: "a b c. a b \<congruent> c c  a = b"

locale tarski_first5 = tarski_first3 +
  fixes B :: "'p  'p  'p  bool"
  assumes A4: "q a b c. x. B q a x  a x \<congruent> b c"
  and A5: "a b c d a' b' c' d'. a  b  B a b c  B a' b' c'
                                                a b \<congruent> a' b'  b c \<congruent> b' c'  a d \<congruent> a' d'  b d \<congruent> b' d'
                                        c d \<congruent> c' d'"

locale tarski_absolute_space = tarski_first5 +
  assumes A6: "a b. B a b a  a = b"
  and A7: "a b c p q. B a p c  B b q c  (x. B p x b  B q x a)"
  and A11: "X Y. (a. x y. x  X  y  Y  B a x y)
                         (b. x y. x  X  y  Y  B x b y)"

locale tarski_absolute = tarski_absolute_space +
  assumes A8: "a b c. ¬ B a b c  ¬ B b c a  ¬ B c a b"
  and A9: "p q a b c. p  q  a p \<congruent> a q  b p \<congruent> b q  c p \<congruent> c q
                              B a b c  B b c a  B c a b"

locale tarski_space = tarski_absolute_space +
  assumes A10: "a b c d t. B a d t  B b d c  a  d 
                                     (x y. B a b x  B a c y  B x t y)"

locale tarski = tarski_absolute + tarski_space

subsection "Semimetric spaces satisfy the first three axioms"

context semimetric
begin
  definition smC :: "'p  'p  'p  'p  bool" ("_ _ \<congruent>sm _ _" [99,99,99,99] 50)
    where [simp]: "a b \<congruent>sm c d  dist a b = dist c d"
end

sublocale semimetric < tarski_first3 smC
proof
  from symm show "a b. a b \<congruent>sm b a" by simp
  show "a b p q r s. a b \<congruent>sm p q  a b \<congruent>sm r s  p q \<congruent>sm r s" by simp
  show "a b c. a b \<congruent>sm c c  a = b" by simp
qed

subsection "Some consequences of the first three axioms"

context tarski_first3
begin
  notation %invisible C ("_ _  _ _" [99,99,99,99] 50)
  lemma A1': "a b \<congruent> b a"
    by (simp add: A1)

  lemma A2': "a b \<congruent> p q; a b \<congruent> r s  p q \<congruent> r s"
  proof -
    assume "a b \<congruent> p q" and "a b \<congruent> r s"
    with A2 show ?thesis by blast
  qed

  lemma A3': "a b \<congruent> c c  a = b"
    by (simp add: A3)

  theorem th2_1: "a b \<congruent> a b"
  proof -
    from A2' [of b a a b a b] and A1' [of b a] show ?thesis by simp
  qed

  theorem th2_2: "a b \<congruent> c d  c d \<congruent> a b"
  proof -
    assume "a b \<congruent> c d"
    with A2' [of a b c d a b] and th2_1 [of a b] show ?thesis by simp
  qed

  theorem th2_3: "a b \<congruent> c d; c d \<congruent> e f  a b \<congruent> e f"
  proof -
    assume "a b \<congruent> c d"
    with th2_2 [of a b c d] have "c d \<congruent> a b" by simp
    assume "c d \<congruent> e f"
    with A2' [of c d a b e f] and c d \<congruent> a b show ?thesis by simp
  qed

  theorem th2_4: "a b \<congruent> c d  b a \<congruent> c d"
  proof -
    assume "a b \<congruent> c d"
    with th2_3 [of b a a b c d] and A1' [of b a] show ?thesis by simp
  qed

  theorem th2_5: "a b \<congruent> c d  a b \<congruent> d c"
  proof -
    assume "a b \<congruent> c d"
    with th2_3 [of a b c d d c] and A1' [of c d] show ?thesis by simp
  qed

  definition is_segment :: "'p set  bool" where
  "is_segment X  x y. X = {x, y}"

  definition segments :: "'p set set" where
  "segments = {X. is_segment X}"

  definition SC :: "'p set  'p set  bool" where
  "SC X Y  w x y z. X = {w, x}  Y = {y, z}  w x \<congruent> y z"

  definition SC_rel :: "('p set × 'p set) set" where
  "SC_rel = {(X, Y) | X Y. SC X Y}"

  lemma left_segment_congruence:
    assumes "{a, b} = {p, q}" and "p q \<congruent> c d"
    shows "a b \<congruent> c d"
  proof cases
    assume "a = p"
    with unordered_pair_element_equality [of a b p q] and {a, b} = {p, q}
      have "b = q" by simp
    with p q \<congruent> c d and a = p show ?thesis by simp
  next
    assume "a  p"
    with {a, b} = {p, q} have "a = q" by auto
    with unordered_pair_element_equality [of a b q p] and {a, b} = {p, q}
      have "b = p" by auto
    with p q \<congruent> c d and a = q have "b a \<congruent> c d" by simp
    with th2_4 [of b a c d] show ?thesis by simp
  qed

  lemma right_segment_congruence:
    assumes "{c, d} = {p, q}" and "a b \<congruent> p q"
    shows "a b \<congruent> c d"
  proof -
    from th2_2 [of a b p q] and a b \<congruent> p q have "p q \<congruent> a b" by simp
    with left_segment_congruence [of c d p q a b] and {c, d} = {p, q}
      have "c d \<congruent> a b" by simp
    with th2_2 [of c d a b] show ?thesis by simp
  qed

  lemma C_SC_equiv: "a b \<congruent> c d = SC {a, b} {c, d}"
  proof
    assume "a b \<congruent> c d"
    with SC_def [of "{a, b}" "{c, d}"] show "SC {a, b} {c, d}" by auto
  next
    assume "SC {a, b} {c, d}"
    with SC_def [of "{a, b}" "{c, d}"]
      obtain w x y z where "{a, b} = {w, x}" and "{c, d} = {y, z}" and "w x \<congruent> y z"
        by blast
    from left_segment_congruence [of a b w x y z] and
        {a, b} = {w, x} and
        w x \<congruent> y z
      have "a b \<congruent> y z" by simp
    with right_segment_congruence [of c d y z a b] and {c, d} = {y, z}
      show "a b \<congruent> c d" by simp
  qed

  lemmas SC_refl = th2_1 [simplified]

  lemma SC_rel_refl: "refl_on segments SC_rel"
  proof -
    note refl_on_def [of segments SC_rel]
    moreover
    { fix Z
      assume "Z  SC_rel"
      with SC_rel_def obtain X Y where "Z = (X, Y)" and "SC X Y" by auto
      from SC X Y and SC_def [of X Y]
        have "w x. X = {w, x}" and "y z. Y = {y, z}" by auto
      with is_segment_def [of X] and is_segment_def [of Y]
        have "is_segment X" and "is_segment Y" by auto
      with segments_def have "X  segments" and "Y  segments" by auto
      with Z = (X, Y) have "Z  segments × segments" by simp }
    hence "SC_rel  segments × segments" by auto
    moreover
    { fix X
      assume "X  segments"
      with segments_def have "is_segment X" by auto
      with is_segment_def [of X] obtain x y where "X = {x, y}" by auto
      with SC_def [of X X] and SC_refl have "SC X X" by (simp add: C_SC_equiv)
      with SC_rel_def have "(X, X)  SC_rel" by simp }
    hence "X. X  segments  (X, X)  SC_rel" by simp
    ultimately show ?thesis by simp
  qed

  lemma SC_sym:
    assumes "SC X Y"
    shows "SC Y X"
  proof -
    from SC_def [of X Y] and SC X Y
      obtain w x y z where "X = {w, x}" and "Y = {y, z}" and "w x \<congruent> y z"
        by auto
    from th2_2 [of w x y z] and w x \<congruent> y z have "y z \<congruent> w x" by simp
    with SC_def [of Y X] and X = {w, x} and Y = {y, z}
      show "SC Y X" by (simp add: C_SC_equiv)
  qed

  lemma SC_sym': "SC X Y = SC Y X"
  proof
    assume "SC X Y"
    with SC_sym [of X Y] show "SC Y X" by simp
  next
    assume "SC Y X"
    with SC_sym [of Y X] show "SC X Y" by simp
  qed

  lemma SC_rel_sym: "sym SC_rel"
  proof -
    { fix X Y
      assume "(X, Y)  SC_rel"
      with SC_rel_def have "SC X Y" by simp
      with SC_sym' have "SC Y X" by simp
      with SC_rel_def have "(Y, X)  SC_rel" by simp }
    with sym_def [of SC_rel] show ?thesis by blast
  qed

  lemma SC_trans:
    assumes "SC X Y" and "SC Y Z"
    shows "SC X Z"
  proof -
    from SC_def [of X Y] and SC X Y
      obtain w x y z where "X = {w, x}" and "Y = {y, z}" and "w x \<congruent> y z"
        by auto
    from SC_def [of Y Z] and SC Y Z
      obtain p q r s where "Y = {p, q}" and "Z = {r, s}" and "p q \<congruent> r s" by auto
    from Y = {y, z} and Y = {p, q} and p q \<congruent> r s
      have "y z \<congruent> r s" by (simp add: C_SC_equiv)
    with th2_3 [of w x y z r s] and w x \<congruent> y z have "w x \<congruent> r s" by simp
    with SC_def [of X Z] and X = {w, x} and Z = {r, s}
      show "SC X Z" by (simp add: C_SC_equiv)
  qed

  lemma SC_rel_trans: "trans SC_rel"
  proof -
    { fix X Y Z
      assume "(X, Y)  SC_rel" and "(Y, Z)  SC_rel"
      with SC_rel_def have "SC X Y" and "SC Y Z" by auto
      with SC_trans [of X Y Z] have "SC X Z" by simp
      with SC_rel_def have "(X, Z)  SC_rel" by simp }
    with trans_def [of SC_rel] show ?thesis by blast
  qed

  lemma A3_reversed:
    assumes "a a \<congruent> b c"
    shows "b = c"
  proof -
    from a a \<congruent> b c have "b c \<congruent> a a" by (rule th2_2)
    thus "b = c" by (rule A3')
  qed
  
  lemma equiv_segments_SC_rel: "equiv segments SC_rel"
    by (simp add: equiv_def SC_rel_refl SC_rel_sym SC_rel_trans)
    
end

subsection "Some consequences of the first five axioms"

context tarski_first5
begin
  lemma A4': "x. B q a x  a x \<congruent> b c"
    by (simp add: A4 [simplified])

  theorem th2_8: "a a \<congruent> b b"
  proof -
    from A4' [of _ a b b] obtain x where "a x \<congruent> b b" by auto
    with A3' [of a x b] have "x = a" by simp
    with a x \<congruent> b b show ?thesis by simp
  qed

  definition OFS :: "['p,'p,'p,'p,'p,'p,'p,'p]  bool" where
   "OFS a b c d a' b' c' d' 
      B a b c  B a' b' c'  a b \<congruent> a' b'  b c \<congruent> b' c'  a d \<congruent> a' d'  b d \<congruent> b' d'"

  lemma A5': "OFS a b c d a' b' c' d'; a  b  c d \<congruent> c' d'"
  proof -
    assume "OFS a b c d a' b' c' d'" and "a  b"
    with A5 and OFS_def show ?thesis by blast
  qed

  theorem th2_11:
    assumes hypotheses:
      "B a b c"
      "B a' b' c'"
      "a b \<congruent> a' b'"
      "b c \<congruent> b' c'"
    shows "a c \<congruent> a' c'"
  proof cases
    assume "a = b"
    with a b \<congruent> a' b' have "a' = b'" by (simp add: A3_reversed)
    with b c \<congruent> b' c' and a = b show ?thesis by simp
  next
    assume "a  b"
    moreover
      note A5' [of a b c a a' b' c' a'] and
        unordered_pair_equality [of a c] and
        unordered_pair_equality [of a' c']
    moreover
      from OFS_def [of a b c a a' b' c' a'] and
          hypotheses and
          th2_8 [of a a'] and
          unordered_pair_equality [of a b] and
          unordered_pair_equality [of a' b']
        have "OFS a b c a a' b' c' a'" by (simp add: C_SC_equiv)
    ultimately show ?thesis by (simp add: C_SC_equiv)
  qed

  lemma A4_unique:
    assumes "q  a" and "B q a x" and "a x \<congruent> b c"
    and "B q a x'" and "a x' \<congruent> b c"
    shows "x = x'"
  proof -
    from SC_sym' and SC_trans and C_SC_equiv and a x' \<congruent> b c and a x \<congruent> b c
      have "a x \<congruent> a x'" by blast
    with th2_11 [of q a x q a x'] and B q a x and B q a x' and SC_refl
      have "q x \<congruent> q x'" by simp
    with OFS_def [of q a x x q a x x'] and
        B q a x and
        SC_refl and
        a x \<congruent> a x'
      have "OFS q a x x q a x x'" by simp
    with A5' [of q a x x q a x x'] and q  a have "x x \<congruent> x x'" by simp
    thus "x = x'" by (rule A3_reversed)
  qed

  theorem th2_12:
    assumes "q  a"
    shows "∃!x. B q a x  a x \<congruent> b c"
    using q  a and A4' and A4_unique
    by blast
end

subsection "Simple theorems about betweenness"

theorem (in tarski_first5) th3_1: "B a b b"
proof -
  from A4 [rule_format, of a b b b] obtain x where "B a b x" and "b x \<congruent> b b" by auto
  from A3 [rule_format, of b x b] and b x \<congruent> b b have "b = x" by simp
  with B a b x show "B a b b" by simp
qed

context tarski_absolute_space
begin
  lemma A6':
    assumes "B a b a"
    shows "a = b"
  proof -
    from A6 and B a b a show "a = b" by simp
  qed
    
  lemma A7':
    assumes "B a p c" and "B b q c"
    shows "x. B p x b  B q x a"
  proof -
    from A7 and B a p c and B b q c show ?thesis by blast
  qed

  lemma A11':
    assumes " x y. x  X  y  Y  B a x y"
    shows " b.  x y. x  X  y  Y  B x b y"
  proof -
    from assms have " a.  x y. x  X  y  Y  B a x y" by (rule exI)
    thus " b.  x y. x  X  y  Y  B x b y" by (rule A11 [rule_format])
  qed

  theorem th3_2:
    assumes "B a b c"
    shows "B c b a"
  proof -
    from th3_1 have "B b c c" by simp
    with A7' and B a b c obtain x where "B b x b" and "B c x a" by blast
    from A6' and B b x b have "x = b" by auto
    with B c x a show "B c b a" by simp
  qed

  theorem th3_4:
    assumes "B a b c" and "B b a c"
    shows "a = b"
  proof -
    from B a b c and B b a c and A7' [of a b c b a]
    obtain x where "B b x b" and "B a x a" by auto
    hence "b = x" and "a = x" by (simp_all add: A6')
    thus "a = b" by simp
  qed

  theorem th3_5_1:
    assumes "B a b d" and "B b c d"
    shows "B a b c"
  proof -
    from B a b d and B b c d and A7' [of a b d b c]
    obtain x where "B b x b" and "B c x a" by auto
    from B b x b have "b = x" by (rule A6')
    with B c x a have "B c b a" by simp
    thus "B a b c" by (rule th3_2)
  qed

  theorem th3_6_1:
    assumes "B a b c" and "B a c d"
    shows "B b c d"
  proof -
    from B a c d and B a b c and th3_2 have "B d c a" and "B c b a" by fast+
    hence "B d c b" by (rule th3_5_1)
    thus "B b c d" by (rule th3_2)
  qed

  theorem th3_7_1:
    assumes "b  c" and "B a b c" and "B b c d"
    shows "B a c d"
  proof -
    from A4' obtain x where "B a c x" and "c x \<congruent> c d" by fast
    from B a b c and B a c x have "B b c x" by (rule th3_6_1)
    have "c d \<congruent> c d" by (rule th2_1)
    with b  c and B b c x and c x \<congruent> c d and B b c d
    have "x = d" by (rule A4_unique)
    with B a c x show "B a c d" by simp
  qed

  theorem th3_7_2:
    assumes "b  c" and "B a b c" and "B b c d"
    shows "B a b d"
  proof -
    from B b c d and B a b c and th3_2 have "B d c b" and "B c b a" by fast+
    with b  c and th3_7_1 [of c b d a] have "B d b a" by simp
    thus "B a b d" by (rule th3_2)
  qed
end

subsection "Simple theorems about congruence and betweenness"

definition (in tarski_first5) Col :: "'p  'p  'p  bool" where
  "Col a b c  B a b c  B b c a  B c a b"

end