Theory Euclid_Tarski

(*  Title:       Real Euclidean space and Tarski's axioms
    Author:      Tim Makarios <tjm1983 at gmail.com>, 2012
    Maintainer:  Tim Makarios <tjm1983 at gmail.com>
*)

section "Real Euclidean space and Tarski's axioms"

theory Euclid_Tarski
imports Tarski
begin

subsection "Real Euclidean space satisfies the first five axioms"

abbreviation
  real_euclid_C :: "[real^('n::finite), real^('n), real^('n), real^('n)] ⇒ bool"
  ("_ _ \<congruent>ℝ _ _" [99,99,99,99] 50) where
    "real_euclid_C ≡ norm_metric.smC"

definition real_euclid_B :: "[real^('n::finite), real^('n), real^('n)] ⇒ bool"
  ("Bℝ _ _ _" [99,99,99] 50) where
    "Bℝ a b c ≡ ∃l. 0 ≤ l ∧ l ≤ 1 ∧ b - a = l *R (c - a)"

interpretation real_euclid: tarski_first5 real_euclid_C real_euclid_B
proof
  txt ‹By virtue of being a semimetric space,
    real Euclidean space is already known to satisfy the first three axioms.›
  { fix q a b c
    have "∃x. Bℝ q a x ∧ a x \<congruent>ℝ b c"
    proof cases
      assume "q = a"
      let ?x = "a + c - b"
      have "Bℝ q a ?x"
      proof -
        let ?l = "0 :: real"
        note real_euclid_B_def [of q a ?x]
        moreover
          have "?l ≥ 0" and "?l ≤ 1" by auto
        moreover
          from ‹q = a› have "a - q = 0" by simp
          hence "a - q = ?l *R (?x - q)" by simp
        ultimately show ?thesis by auto
      qed
      moreover
        have "a - ?x = b - c" by simp
        hence "a ?x \<congruent>ℝ b c" by (simp add: field_simps)
      ultimately show ?thesis by blast
    next
      assume "q ≠ a"
      hence "norm_dist q a > 0" by simp
      let ?k = "norm_dist b c / norm_dist q a"
      let ?x = "a + ?k *R (a - q)"
      have "Bℝ q a ?x"
      proof -
        let ?l = "1 / (1 + ?k)"
        have "?l > 0" by (simp add: add_pos_nonneg)
        note real_euclid_B_def [of q a ?x]
        moreover
          have "?l ≥ 0" and "?l ≤ 1" by (auto simp add: add_pos_nonneg)
        moreover
          from scaleR_left_distrib [of 1 ?k "a - q"]
            have "(1 + ?k) *R (a - q) = ?x - q" by simp
          hence "?l *R ((1 + ?k) *R (a - q)) = ?l *R (?x - q)" by simp
          with ‹?l > 0› and scaleR_right_diff_distrib [of ?l ?x q]
            have "a - q = ?l *R (?x - q)" by simp
        ultimately show "Bℝ q a ?x" by blast
      qed
      moreover
        have "a ?x \<congruent>ℝ b c"
        proof -
          from norm_scaleR [of ?k "a - q"] have
            "norm_dist a ?x = ¦?k¦ * norm (a - q)" by simp
          also have
            "… = ?k * norm (a - q)" by simp
          also from norm_metric.symm [of q a] have
            "… = ?k * norm_dist q a" by simp
          finally have
            "norm_dist a ?x = norm_dist b c / norm_dist q a * norm_dist q a" .
          with ‹norm_dist q a > 0› show "a ?x \<congruent>ℝ b c" by auto
        qed
      ultimately show ?thesis by blast
    qed }
  thus "∀q a b c. ∃x. Bℝ q a x ∧ a x \<congruent>ℝ b c" by auto
  { fix a b c d a' b' c' d'
    assume "a ≠ b" and
      "Bℝ a b c" and
      "Bℝ a' b' c'" and
      "a b \<congruent>ℝ a' b'" and
      "b c \<congruent>ℝ b' c'" and
      "a d \<congruent>ℝ a' d'" and
      "b d \<congruent>ℝ b' d'"
    have "c d \<congruent>ℝ c' d'"
    proof -
      { fix m
        fix p q r :: "real^('n::finite)"
        assume "0 ≤ m" and
          "m ≤ 1" and
          "p ≠ q" and
          "q - p = m *R (r - p)"
        from ‹p ≠ q› and ‹q - p = m *R (r - p)› have "m ≠ 0"
        proof -
          { assume "m = 0"
            with ‹q - p = m *R (r - p)› have "q - p = 0" by simp
            with ‹p ≠ q› have False by simp }
          thus ?thesis ..
        qed
        with ‹m ≥ 0› have "m > 0" by simp
        from ‹q - p = m *R (r - p)› and
            scaleR_right_diff_distrib [of m r p]
          have "q - p = m *R r - m *R p" by simp
        hence "q - p - q + p - m *R r =
            m *R r - m *R p - q + p - m *R r"
          by simp
        with scaleR_left_diff_distrib [of 1 m p] and
            scaleR_left_diff_distrib [of 1 m q]
          have "(1 - m) *R p - (1 - m) *R q = m *R q - m *R r" by auto
        with scaleR_right_diff_distrib [of "1 - m" p q] and
            scaleR_right_diff_distrib [of m q r]
          have "(1 - m) *R (p - q) = m *R (q - r)" by simp
        with norm_scaleR [of "1 - m" "p - q"] and norm_scaleR [of m "q - r"]
          have "¦1 - m¦ * norm (p - q) = ¦m¦ * norm (q - r)" by simp
        with ‹m > 0› and ‹m ≤ 1›
          have "norm (q - r) = (1 - m) / m * norm (p - q)" by simp
        moreover from ‹p ≠ q› have "norm (p - q) ≠ 0" by simp
        ultimately
          have "norm (q - r) / norm (p - q) = (1 - m) / m" by simp
        with ‹m ≠ 0› have
          "norm_dist q r / norm_dist p q = (1 - m) / m" and "m ≠ 0" by auto }
      note linelemma = this
      from real_euclid_B_def [of a b c] and ‹Bℝ a b c›
        obtain l where "0 ≤ l" and "l ≤ 1" and  "b - a = l *R (c - a)" by auto
      from real_euclid_B_def [of a' b' c'] and ‹Bℝ a' b' c'›
        obtain l' where"0 ≤ l'" and "l' ≤ 1" and  "b' - a' = l' *R (c' - a')" by auto
      from ‹a ≠ b› and ‹a b \<congruent>ℝ a' b'› have "a' ≠ b'" by auto
      from linelemma [of l a b c] and
          ‹l ≥ 0› and
          ‹l ≤ 1› and
          ‹a ≠ b› and
          ‹b - a = l *R (c - a)›
        have "l ≠ 0" and "(1 - l) / l = norm_dist b c / norm_dist a b" by auto
      from ‹(1 - l) / l = norm_dist b c / norm_dist a b› and
          ‹a b \<congruent>ℝ a' b'› and
          ‹b c \<congruent>ℝ b' c'›
        have "(1 - l) / l = norm_dist b' c' / norm_dist a' b'" by simp
      with linelemma [of l' a' b' c'] and
          ‹l' ≥ 0› and
          ‹l' ≤ 1› and
          ‹a' ≠ b'› and
          ‹b' - a' = l' *R (c' - a')›
        have "l' ≠ 0" and "(1 - l) / l = (1 - l') / l'" by auto
      from ‹(1 - l) / l = (1 - l') / l'›
        have "(1 - l) / l * l * l' = (1 - l') / l' * l * l'" by simp
      with ‹l ≠ 0› and ‹l' ≠ 0› have "(1 - l) * l' = (1 - l') * l" by simp
      with left_diff_distrib [of 1 l l'] and left_diff_distrib [of 1 l' l]
        have "l = l'" by simp
      { fix m
        fix p q r s :: "real^('n::finite)"
        assume "m ≠ 0" and
          "q - p = m *R (r - p)"
        with scaleR_scaleR have "r - p = (1/m) *R (q - p)" by simp
        with cosine_rule [of r s p]
          have "(norm_dist r s)2 = (norm_dist r p)2 + (norm_dist p s)2 +
              2 * (((1/m) *R (q - p)) ∙ (p - s))"
            by simp
        also from inner_scaleR_left [of "1/m" "q - p" "p - s"]
          have "… =
              (norm_dist r p)2 + (norm_dist p s)2 + 2/m * ((q - p) ∙ (p - s))"
            by simp
        also from ‹m ≠ 0› and cosine_rule [of q s p]
          have "… = (norm_dist r p)2 + (norm_dist p s)2 +
              1/m * ((norm_dist q s)2 - (norm_dist q p)2 - (norm_dist p s)2)"
            by simp
        finally have "(norm_dist r s)2 = (norm_dist r p)2 + (norm_dist p s)2 +
          1/m * ((norm_dist q s)2 - (norm_dist q p)2 - (norm_dist p s)2)" .
        moreover
        { from norm_dist_dot [of r p] and ‹r - p = (1/m) *R (q - p)›
            have "(norm_dist r p)2 = ((1/m) *R (q - p)) ∙ ((1/m) *R (q - p))"
              by simp
          also from inner_scaleR_left [of "1/m" "q - p"] and
              inner_scaleR_right [of _ "1/m" "q - p"]
            have "… = 1/m2 * ((q - p) ∙ (q - p))"
              by (simp add: power2_eq_square)
          also from norm_dist_dot [of q p] have "… = 1/m2 * (norm_dist q p)2"
            by simp
          finally have "(norm_dist r p)2 = 1/m2 * (norm_dist q p)2" . }
        ultimately have
          "(norm_dist r s)2 = 1/m2 * (norm_dist q p)2 + (norm_dist p s)2 +
            1/m * ((norm_dist q s)2 - (norm_dist q p)2 - (norm_dist p s)2)"
          by simp
        with norm_metric.symm [of q p]
          have "(norm_dist r s)2 = 1/m2 * (norm_dist p q)2 + (norm_dist p s)2 +
              1/m * ((norm_dist q s)2 - (norm_dist p q)2 - (norm_dist p s)2)"
            by simp }
      note fiveseglemma = this
      from fiveseglemma [of l b a c d] and ‹l ≠ 0› and ‹b - a = l *R (c - a)›
        have "(norm_dist c d)2 = 1/l2 * (norm_dist a b)2 + (norm_dist a d)2 +
            1/l * ((norm_dist b d)2 - (norm_dist a b)2 - (norm_dist a d)2)"
          by simp
      also from ‹l = l'› and
          ‹a b \<congruent>ℝ a' b'› and
          ‹a d \<congruent>ℝ a' d'› and
          ‹b d \<congruent>ℝ b' d'›
        have "… = 1/l'2 * (norm_dist a' b')2 + (norm_dist a' d')2 +
            1/l' * ((norm_dist b' d')2 - (norm_dist a' b')2 - (norm_dist a' d')2)"
          by simp
      also from fiveseglemma [of l' b' a' c' d'] and
          ‹l' ≠ 0› and
          ‹b' - a' = l' *R (c' - a')›
        have "… = (norm_dist c' d')2" by simp
      finally have "(norm_dist c d)2 = (norm_dist c' d')2" .
      hence "sqrt ((norm_dist c d)2) = sqrt ((norm_dist c' d')2)" by simp
      with real_sqrt_abs show "c d \<congruent>ℝ c' d'" by simp
    qed }
  thus "∀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'"
    by blast
qed

subsection "Real Euclidean space also satisfies axioms 6, 7, and 11"

lemma rearrange_real_euclid_B:
  fixes w y z :: "real^('n)" and h
  shows "y - w = h *R (z - w) ⟷ y = h *R z + (1 - h) *R w"
proof
  assume "y - w = h *R (z - w)"
  hence "y - w + w = h *R (z - w) + w" by simp
  hence "y = h *R (z - w) + w" by simp
  with scaleR_right_diff_distrib [of h z w]
    have "y = h *R z + w - h *R w" by simp
  with scaleR_left_diff_distrib [of 1 h w]
    show "y = h *R z + (1 - h) *R w" by simp
next
  assume "y = h *R z + (1 - h) *R w"
  with scaleR_left_diff_distrib [of 1 h w]
    have "y = h *R z + w - h *R w" by simp
  with scaleR_right_diff_distrib [of h z w]
    have "y = h *R (z - w) + w" by simp
  hence "y - w + w = h *R (z - w) + w" by simp
  thus "y - w = h *R (z - w)" by simp
qed

interpretation real_euclid: tarski_absolute_space real_euclid_C real_euclid_B
proof
  { fix a b
    assume "Bℝ a b a"
    with real_euclid_B_def [of a b a]
      obtain l where "b - a = l *R (a - a)" by auto
    hence "a = b" by simp }
  thus "∀a b. Bℝ a b a ⟶ a = b" by auto
  { fix a b c p q
    assume "Bℝ a p c" and "Bℝ b q c"
    from real_euclid_B_def [of a p c] and ‹Bℝ a p c›
      obtain i where "i ≥ 0" and "i ≤ 1" and "p - a = i *R (c - a)" by auto
    have "∃x. Bℝ p x b ∧ Bℝ q x a"
    proof cases
      assume "i = 0"
      with ‹p - a = i *R (c - a)› have "p = a" by simp
      hence "p - a = 0 *R (b - p)" by simp
      moreover have "(0::real) ≥ 0" and "(0::real) ≤ 1" by auto
      moreover note real_euclid_B_def [of p a b]
      ultimately have "Bℝ p a b" by auto
      moreover
      { have "a - q = 1 *R (a - q)" by simp
        moreover have "(1::real) ≥ 0" and "(1::real) ≤ 1" by auto
        moreover note real_euclid_B_def [of q a a]
        ultimately have "Bℝ q a a" by blast }
      ultimately have "Bℝ p a b ∧ Bℝ q a a" by simp
      thus "∃x. Bℝ p x b ∧ Bℝ q x a" by auto
    next
      assume "i ≠ 0"
      from real_euclid_B_def [of b q c] and ‹Bℝ b q c›
        obtain j where "j ≥ 0" and "j ≤ 1" and "q - b = j *R (c - b)" by auto
      from ‹i ≥ 0› and ‹i ≤ 1›
        have "1 - i ≥ 0" and "1 - i ≤ 1" by auto
      from ‹j ≥ 0› and ‹1 - i ≥ 0›
        have "j * (1 - i) ≥ 0" by auto
      with ‹i ≥ 0› and ‹i ≠ 0› have "i + j * (1 - i) > 0" by simp
      hence "i + j * (1 - i) ≠ 0" by simp
      let ?l = "j * (1 - i) / (i + j * (1 - i))"
      from diff_divide_distrib [of "i + j * (1 - i)" "j * (1 - i)" "i + j * (1 - i)"] and
          ‹i + j * (1 - i) ≠ 0›
        have "1 - ?l = i / (i + j * (1 - i))" by simp
      let ?k = "i * (1 - j) / (j + i * (1 - j))"
      from right_diff_distrib [of i 1 j] and
          right_diff_distrib [of j 1 i] and
          mult.commute [of i j] and
          add.commute [of i j]
        have "j + i * (1 - j) = i + j * (1 - i)" by simp
      with ‹i + j * (1 - i) ≠ 0› have "j + i * (1 - j) ≠ 0" by simp
      with diff_divide_distrib [of "j + i * (1 - j)" "i * (1 - j)" "j + i * (1 - j)"]
        have "1 - ?k = j / (j + i * (1 - j))" by simp
      with ‹1 - ?l = i / (i + j * (1 - i))› and
          ‹j + i * (1 - j) = i + j * (1 - i)› and
          times_divide_eq_left [of _ "i + j * (1 - i)"] and
          mult.commute [of i j]
        have "(1 - ?l) * j = (1 - ?k) * i" by simp
      moreover
      { from ‹1 - ?k = j / (j + i * (1 - j))› and
            ‹j + i * (1 - j) = i + j * (1 - i)›
          have "?l = (1 - ?k) * (1 - i)" by simp }
      moreover
      { from ‹1 - ?l = i / (i + j * (1 - i))› and
            ‹j + i * (1 - j) = i + j * (1 - i)›
          have "(1 - ?l) * (1 - j) = ?k" by simp }
      ultimately
        have "?l *R a + ((1 - ?l) * j) *R c + ((1 - ?l) * (1 - j)) *R b =
            ?k *R b + ((1 - ?k) * i) *R c + ((1 - ?k) * (1 - i)) *R a"
          by simp
      with scaleR_scaleR
        have "?l *R a + (1 - ?l) *R j *R c + (1 - ?l) *R (1 - j) *R b =
            ?k *R b + (1 - ?k) *R i *R c + (1 - ?k) *R (1 - i) *R a"
          by simp
      with scaleR_right_distrib [of "(1 - ?l)" "j *R c" "(1 - j) *R b"] and
          scaleR_right_distrib [of "(1 - ?k)" "i *R c" "(1 - i) *R a"] and
          add.assoc [of "?l *R a" "(1 - ?l) *R j *R c" "(1 - ?l) *R (1 - j) *R b"] and
          add.assoc [of "?k *R b" "(1 - ?k) *R i *R c" "(1 - ?k) *R (1 - i) *R a"]
        have "?l *R a + (1 - ?l) *R (j *R c + (1 - j) *R b) =
            ?k *R b + (1 - ?k) *R (i *R c + (1 - i) *R a)"
          by arith
      from ‹?l *R a + (1 - ?l) *R (j *R c + (1 - j) *R b) =
            ?k *R b + (1 - ?k) *R (i *R c + (1 - i) *R a)› and
          ‹p - a = i *R (c - a)› and
          ‹q - b = j *R (c - b)› and
          rearrange_real_euclid_B [of p a i c] and
          rearrange_real_euclid_B [of q b j c]
        have "?l *R a + (1 - ?l) *R q = ?k *R b + (1 - ?k) *R p" by simp
      let ?x = "?l *R a + (1 - ?l) *R q"
      from rearrange_real_euclid_B [of ?x q ?l a]
        have "?x - q = ?l *R (a - q)" by simp
      from ‹?x = ?k *R b + (1 - ?k) *R p› and
          rearrange_real_euclid_B [of ?x p ?k b]
        have "?x - p = ?k *R (b - p)" by simp
      from ‹i + j * (1 - i) > 0› and
          ‹j * (1 - i) ≥ 0› and
          zero_le_divide_iff [of "j * (1 - i)" "i + j * (1 - i)"]
        have "?l ≥ 0" by simp
      from ‹i + j * (1 - i) > 0› and
          ‹i ≥ 0› and
          zero_le_divide_iff [of i "i + j * (1 - i)"] and
          ‹1 - ?l = i / (i + j * (1 - i))›
        have "1 - ?l ≥ 0" by simp
      hence "?l ≤ 1" by simp
      with ‹?l ≥ 0› and
          ‹?x - q = ?l *R (a - q)› and
          real_euclid_B_def [of q ?x a]
        have "Bℝ q ?x a" by auto
      from ‹j ≤ 1› have "1 - j ≥ 0" by simp
      with ‹1 - ?l ≥ 0› and
          ‹(1 - ?l) * (1 - j) = ?k› and
          zero_le_mult_iff [of "1 - ?l" "1 - j"]
        have "?k ≥ 0" by simp
      from ‹j ≥ 0› have "1 - j ≤ 1" by simp
      from ‹?l ≥ 0› have "1 - ?l ≤ 1" by simp
      with ‹1 - j ≤ 1› and
          ‹1 - j ≥ 0› and
          mult_mono [of "1 - ?l" 1 "1 - j" 1] and
          ‹(1 - ?l) * (1 - j) = ?k›
        have "?k ≤ 1" by simp
      with ‹?k ≥ 0› and
          ‹?x - p = ?k *R (b - p)› and
          real_euclid_B_def [of p ?x b]
        have "Bℝ p ?x b" by auto
      with ‹Bℝ q ?x a› show ?thesis by auto
    qed }
  thus "∀a b c p q. Bℝ a p c ∧ Bℝ b q c ⟶ (∃x. Bℝ p x b ∧ Bℝ q x a)" by auto
  { fix X Y
    assume "∃a. ∀x y. x ∈ X ∧ y ∈ Y ⟶ Bℝ a x y"
    then obtain a where "∀x y. x ∈ X ∧ y ∈ Y ⟶ Bℝ a x y" by auto
    have "∃b. ∀x y. x ∈ X ∧ y ∈ Y ⟶ Bℝ x b y"
    proof cases
      assume "X ⊆ {a} ∨ Y = {}"
      let ?b = a
      { fix x y
        assume "x ∈ X" and "y ∈ Y"
        with ‹X ⊆ {a} ∨ Y = {}› have "x = a" by auto
        from ‹∀x y. x ∈ X ∧ y ∈ Y ⟶ Bℝ a x y› and ‹x ∈ X› and ‹y ∈ Y›
          have "Bℝ a x y" by simp
        with ‹x = a› have "Bℝ x ?b y" by simp }
      hence "∀x y. x ∈ X ∧ y ∈ Y ⟶ Bℝ x ?b y" by simp
      thus ?thesis by auto
    next
      assume "¬(X ⊆ {a} ∨ Y = {})"
      hence "X - {a} ≠ {}" and "Y ≠ {}" by auto
      from ‹X - {a} ≠ {}› obtain c where "c ∈ X" and "c ≠ a" by auto
      from ‹c ≠ a› have "c - a ≠ 0" by simp
      { fix y
        assume "y ∈ Y"
        with ‹∀x y. x ∈ X ∧ y ∈ Y ⟶ Bℝ a x y› and ‹c ∈ X›
          have "Bℝ a c y" by simp
        with real_euclid_B_def [of a c y]
          obtain l where "l ≥ 0" and "l ≤ 1" and "c - a = l *R (y - a)" by auto
        from ‹c - a = l *R (y - a)› and ‹c - a ≠ 0› have "l ≠ 0" by simp
        with ‹l ≥ 0› have "l > 0" by simp
        with ‹c - a = l *R (y - a)› have "y - a = (1/l) *R (c - a)" by simp
        from ‹l > 0› and ‹l ≤ 1› have "1/l ≥ 1" by simp
        with ‹y - a = (1/l) *R (c - a)›
          have "∃j≥1. y - a = j *R (c - a)" by auto }
      note ylemma = this
      from ‹Y ≠ {}› obtain d where "d ∈ Y" by auto
      with ylemma [of d]
        obtain "jd" where "jd ≥ 1" and "d - a = jd *R (c - a)" by auto
      { fix x
        assume "x ∈ X"
        with ‹∀x y. x ∈ X ∧ y ∈ Y ⟶ Bℝ a x y› and ‹d ∈ Y›
          have "Bℝ a x d" by simp
        with real_euclid_B_def [of a x d]
          obtain l where "l ≥ 0" and "x - a = l *R (d - a)" by auto
        from ‹x - a = l *R (d - a)› and
            ‹d - a = jd *R (c - a)› and
            scaleR_scaleR
          have "x - a = (l * jd) *R (c - a)" by simp
        hence "∃i. x - a = i *R (c - a)" by auto }
      note xlemma = this
      let ?S = "{j. j ≥ 1 ∧ (∃y∈Y. y - a = j *R (c - a))}"
      from ‹d ∈ Y› and ‹jd ≥ 1› and ‹d - a = jd *R (c - a)›
        have "?S ≠ {}" by auto
      let ?k = "Inf ?S"
      let ?b = "?k *R c + (1 - ?k) *R a"
      from rearrange_real_euclid_B [of ?b a ?k c]
        have "?b - a = ?k *R (c - a)" by simp
      { fix x y
        assume "x ∈ X" and "y ∈ Y"
        from xlemma [of x] and ‹x ∈ X›
          obtain i where "x - a = i *R (c - a)" by auto
        from ylemma [of y] and ‹y ∈ Y›
          obtain j where "j ≥ 1" and "y - a = j *R (c - a)" by auto
        with ‹y ∈ Y› have "j ∈ ?S" by auto
        then have "?k ≤ j" by (auto intro: cInf_lower)
        { fix h
          assume "h ∈ ?S"
          hence "h ≥ 1" by simp
          from ‹h ∈ ?S›
            obtain z where "z ∈ Y" and "z - a = h *R (c - a)" by auto
          from ‹∀x y. x ∈ X ∧ y ∈ Y ⟶ Bℝ a x y› and ‹x ∈ X› and ‹z ∈ Y›
            have "Bℝ a x z" by simp
          with real_euclid_B_def [of a x z]
            obtain l where "l ≤ 1" and "x - a = l *R (z - a)" by auto
          with ‹z - a = h *R (c - a)› and scaleR_scaleR
            have "x - a = (l * h) *R (c - a)" by simp
          with ‹x - a = i *R (c - a)›
            have "i *R (c - a) = (l * h) *R (c - a)" by auto
          with scaleR_cancel_right and ‹c - a ≠ 0› have "i = l * h" by blast
          with ‹l ≤ 1› and ‹h ≥ 1› have "i ≤ h" by simp }
        with ‹?S ≠ {}› and cInf_greatest [of ?S] have "i ≤ ?k" by simp
        have "y - x = (y - a) - (x - a)" by simp
        with ‹y - a = j *R (c - a)› and ‹x - a = i *R (c - a)›
          have "y - x = j *R (c - a) - i *R (c - a)" by simp
        with scaleR_left_diff_distrib [of j i "c - a"]
          have "y - x = (j - i) *R (c - a)" by simp
        have "?b - x = (?b - a) - (x - a)" by simp
        with ‹?b - a = ?k *R (c - a)› and ‹x - a = i *R (c - a)›
          have "?b - x = ?k *R (c - a) - i *R (c - a)" by simp
        with scaleR_left_diff_distrib [of ?k i "c - a"]
          have "?b - x = (?k - i) *R (c - a)" by simp
        have "Bℝ x ?b y"
        proof cases
          assume "i = j"
          with ‹i ≤ ?k› and ‹?k ≤ j› have "?k = i" by simp
          with ‹?b - x = (?k - i) *R (c - a)› have "?b - x = 0" by simp
          hence "?b - x = 0 *R (y - x)" by simp
          with real_euclid_B_def [of x ?b y] show "Bℝ x ?b y" by auto
        next
          assume "i ≠ j"
          with ‹i ≤ ?k› and ‹?k ≤ j› have "j - i > 0" by simp
          with ‹y - x = (j - i) *R (c - a)› and scaleR_scaleR
            have "c - a = (1 / (j - i)) *R (y - x)" by simp
          with ‹?b - x = (?k - i) *R (c - a)› and scaleR_scaleR
            have "?b - x = ((?k - i) / (j - i)) *R (y - x)" by simp
          let ?l = "(?k - i) / (j - i)"
          from ‹?k ≤ j› have "?k - i ≤ j - i" by simp
          with ‹j - i > 0› have "?l ≤ 1" by simp
          from ‹i ≤ ?k› and ‹j - i > 0› and pos_le_divide_eq [of "j - i" 0 "?k - i"]
            have "?l ≥ 0" by simp
          with real_euclid_B_def [of x ?b y] and
              ‹?l ≤ 1› and
              ‹?b - x = ?l *R (y - x)›
            show "Bℝ x ?b y" by auto
        qed }
      thus "∃b. ∀x y. x ∈ X ∧ y ∈ Y ⟶ Bℝ x b y" by auto
    qed }
  thus "∀X Y. (∃a. ∀x y. x ∈ X ∧ y ∈ Y ⟶ Bℝ a x y) ⟶
          (∃b. ∀x y. x ∈ X ∧ y ∈ Y ⟶ Bℝ x b y)"
    by auto
qed

subsection "Real Euclidean space satisfies the Euclidean axiom"

lemma rearrange_real_euclid_B_2:
  fixes a b c :: "real^('n::finite)"
  assumes "l ≠ 0"
  shows "b - a = l *R (c - a) ⟷ c = (1/l) *R b + (1 - 1/l) *R a"
proof
  from scaleR_right_diff_distrib [of "1/l" b a]
    have "(1/l) *R (b - a) = c - a ⟷ (1/l) *R b - (1/l) *R a + a = c" by auto
  also with scaleR_left_diff_distrib [of 1 "1/l" a]
    have "… ⟷ c = (1/l) *R b + (1 - 1/l) *R a" by auto
  finally have eq:
    "(1/l) *R (b - a) = c - a ⟷ c = (1/l) *R b + (1 - 1/l) *R a" .
  { assume "b - a = l *R (c - a)"
    with ‹l ≠ 0› have "(1/l) *R (b - a) = c - a" by simp
    with eq show "c = (1/l) *R b + (1 - 1/l) *R a" .. }
  { assume "c = (1/l) *R b + (1 - 1/l) *R a"
    with eq have "(1/l) *R (b - a) = c - a" ..
    hence "l *R (1/l) *R (b - a) = l *R (c - a)" by simp
    with ‹l ≠ 0› show "b - a = l *R (c - a)" by simp }
qed

interpretation real_euclid: tarski_space real_euclid_C real_euclid_B
proof
  { fix a b c d t
    assume "Bℝ a d t" and "Bℝ b d c" and "a ≠ d"
    from real_euclid_B_def [of a d t] and ‹Bℝ a d t›
      obtain j where "j ≥ 0" and "j ≤ 1" and "d - a = j *R (t - a)" by auto
    from ‹d - a = j *R (t - a)› and ‹a ≠ d› have "j ≠ 0" by auto
    with ‹d - a = j *R (t - a)› and rearrange_real_euclid_B_2
      have "t = (1/j) *R d + (1 - 1/j) *R a" by auto
    let ?x = "(1/j) *R b + (1 - 1/j) *R a"
    let ?y = "(1/j) *R c + (1 - 1/j) *R a"
    from ‹j ≠ 0› and rearrange_real_euclid_B_2 have
      "b - a = j *R (?x - a)" and "c - a = j *R (?y - a)" by auto
    with real_euclid_B_def and ‹j ≥ 0› and ‹j ≤ 1› have
      "Bℝ a b ?x" and "Bℝ a c ?y" by auto
    from real_euclid_B_def and ‹Bℝ b d c› obtain k where
      "k ≥ 0" and "k ≤ 1" and "d - b = k *R (c - b)" by blast
    from ‹t = (1/j) *R d + (1 - 1/j) *R a› have
      "t - ?x = (1/j) *R d - (1/j) *R b" by simp
    also from scaleR_right_diff_distrib [of "1/j" d b] have
      "… = (1/j) *R (d - b)" by simp
    also from ‹d - b = k *R (c - b)› have
      "… = k *R (1/j) *R (c - b)" by simp
    also from scaleR_right_diff_distrib [of "1/j" c b] have
      "… = k *R (?y - ?x)" by simp
    finally have "t - ?x = k *R (?y - ?x)" .
    with real_euclid_B_def and ‹k ≥ 0› and ‹k ≤ 1› have "Bℝ ?x t ?y" by blast
    with ‹Bℝ a b ?x› and ‹Bℝ a c ?y› have
      "∃x y. Bℝ a b x ∧ Bℝ a c y ∧ Bℝ x t y" by auto }
  thus "∀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)"
    by auto
qed

subsection "The real Euclidean plane"

lemma Col_dep2:
  "real_euclid.Col a b c ⟷ dep2 (b - a) (c - a)"
proof -
  from real_euclid.Col_def have
    "real_euclid.Col a b c ⟷ Bℝ a b c ∨ Bℝ b c a ∨ Bℝ c a b" by auto
  moreover from dep2_def have
    "dep2 (b - a) (c - a) ⟷ (∃w r s. b - a = r *R w ∧ c - a = s *R w)"
    by auto
  moreover
  { assume "Bℝ a b c ∨ Bℝ b c a ∨ Bℝ c a b"
    moreover
    { assume "Bℝ a b c"
      with real_euclid_B_def obtain l where "b - a = l *R (c - a)" by blast
      moreover have "c - a = 1 *R (c - a)" by simp
      ultimately have "∃w r s. b - a = r *R w ∧ c - a = s *R w" by blast }
    moreover
    { assume "Bℝ b c a"
      with real_euclid_B_def obtain l where "c - b = l *R (a - b)" by blast
      moreover have "c - a = (c - b) - (a - b)" by simp
      ultimately have "c - a = l *R (a - b) - (a - b)" by simp
      with scaleR_left_diff_distrib [of l 1 "a - b"] have
        "c - a = (l - 1) *R (a - b)" by simp
      moreover from scaleR_minus_left [of 1 "a - b"] have
        "b - a = (-1) *R (a - b)" by simp
      ultimately have "∃w r s. b - a = r *R w ∧ c - a = s *R w" by blast }
    moreover
    { assume "Bℝ c a b"
      with real_euclid_B_def obtain l where "a - c = l *R (b - c)" by blast
      moreover have "c - a = -(a - c)" by simp
      ultimately have "c - a = -(l *R (b - c))" by simp
      with scaleR_minus_left have "c - a = (-l) *R (b - c)" by simp
      moreover have "b - a = (b - c) + (c - a)" by simp
      ultimately have "b - a = 1 *R (b - c) + (-l) *R (b - c)" by simp
      with scaleR_left_distrib [of 1 "-l" "b - c"] have
        "b - a = (1 + (-l)) *R (b - c)" by simp
      with ‹c - a = (-l) *R (b - c)› have
        "∃w r s. b - a = r *R w ∧ c - a = s *R w" by blast }
    ultimately have "∃w r s. b - a = r *R w ∧ c - a = s *R w" by auto }
  moreover
  { assume "∃w r s. b - a = r *R w ∧ c - a = s *R w"
    then obtain w r s where "b - a = r *R w" and "c - a = s *R w" by auto
    have "Bℝ a b c ∨ Bℝ b c a ∨ Bℝ c a b"
    proof cases
      assume "s = 0"
      with ‹c - a = s *R w› have "a = c" by simp
      with real_euclid.th3_1 have "Bℝ b c a" by simp
      thus ?thesis by simp
    next
      assume "s ≠ 0"
      with ‹c - a = s *R w› have "w = (1/s) *R (c - a)" by simp
      with ‹b - a = r *R w› have "b - a = (r/s) *R (c - a)" by simp
      have "r/s < 0 ∨ (r/s ≥ 0 ∧ r/s ≤ 1) ∨ r/s > 1" by arith
      moreover
      { assume "r/s ≥ 0 ∧ r/s ≤ 1"
        with real_euclid_B_def and ‹b - a = (r/s) *R (c - a)› have "Bℝ a b c"
          by auto
        hence ?thesis by simp }
      moreover
      { assume "r/s > 1"
        with ‹b - a = (r/s) *R (c - a)› have "c - a = (s/r) *R (b - a)" by auto
        from ‹r/s > 1› and le_imp_inverse_le [of 1 "r/s"] have
          "s/r ≤ 1" by simp
        from ‹r/s > 1› and inverse_positive_iff_positive [of "r/s"] have
          "s/r ≥ 0" by simp
        with real_euclid_B_def
          and ‹c - a = (s/r) *R (b - a)›
          and ‹s/r ≤ 1›
        have "Bℝ a c b" by auto
        with real_euclid.th3_2 have "Bℝ b c a" by auto
        hence ?thesis by simp }
      moreover
      { assume "r/s < 0"
        have "b - c = (b - a) + (a - c)" by simp
        with ‹b - a = (r/s) *R (c - a)› have
          "b - c = (r/s) *R (c - a) + (a - c)" by simp
        have "c - a = -(a - c)" by simp
        with scaleR_minus_right [of "r/s" "a - c"] have
          "(r/s) *R (c - a) = -((r/s) *R (a - c))" by arith
        with ‹b - c = (r/s) *R (c - a) + (a - c)› have
          "b - c = -(r/s) *R (a - c) + (a - c)" by simp
        with scaleR_left_distrib [of "-(r/s)" 1 "a - c"] have
          "b - c = (-(r/s) + 1) *R (a - c)" by simp
        moreover from ‹r/s < 0› have "-(r/s) + 1 > 1" by simp
        ultimately have "a - c = (1 / (-(r/s) + 1)) *R (b - c)" by auto
        let ?l = "1 / (-(r/s) + 1)"
        from ‹-(r/s) + 1 > 1› and le_imp_inverse_le [of 1 "-(r/s) + 1"] have
          "?l ≤ 1" by simp
        from ‹-(r/s) + 1 > 1›
          and inverse_positive_iff_positive [of "-(r/s) + 1"]
        have
          "?l ≥ 0" by simp
        with real_euclid_B_def and ‹?l ≤ 1› and ‹a - c = ?l *R (b - c)› have
          "Bℝ c a b" by blast
        hence ?thesis by simp }
      ultimately show ?thesis by auto
    qed }
  ultimately show ?thesis by blast
qed

lemma non_Col_example:
  "¬(real_euclid.Col 0 (vector [1/2,0] :: real^2) (vector [0,1/2]))"
  (is "¬ (real_euclid.Col ?a ?b ?c)")
proof -
  { assume "dep2 (?b - ?a) (?c - ?a)"
    with dep2_def [of "?b - ?a" "?c - ?a"] obtain w r s where
      "?b - ?a = r *R w" and "?c - ?a = s *R w" by auto
    have "?b$1 = 1/2" by simp
    with ‹?b - ?a = r *R w› have "r * (w$1) = 1/2" by simp
    hence "w$1 ≠ 0" by auto
    have "?c$1 = 0" by simp
    with ‹?c - ?a = s *R w› have "s * (w$1) = 0" by simp
    with ‹w$1 ≠ 0› have "s = 0" by simp
    have "?c$2 = 1/2" by simp
    with ‹?c - ?a = s *R w› have "s * (w$2) = 1/2" by simp
    with ‹s = 0› have False by simp }
  hence "¬(dep2 (?b - ?a) (?c - ?a))" by auto
  with Col_dep2 show "¬(real_euclid.Col ?a ?b ?c)" by blast
qed

interpretation real_euclid:
  tarski "real_euclid_C::([real^2, real^2, real^2, real^2] ⇒ bool)" real_euclid_B
proof
  { let ?a = "0 :: real^2"
    let ?b = "vector [1/2, 0] :: real^2"
    let ?c = "vector [0, 1/2] :: real^2"
    from non_Col_example and real_euclid.Col_def have
      "¬ Bℝ ?a ?b ?c ∧ ¬ Bℝ ?b ?c ?a ∧ ¬ Bℝ ?c ?a ?b" by auto }
  thus "∃a b c :: real^2. ¬ Bℝ a b c ∧ ¬ Bℝ b c a ∧ ¬ Bℝ c a b"
    by auto
  { fix p q a b c :: "real^2"
    assume "p ≠ q" and "a p \<congruent>ℝ  a q" and "b p \<congruent>ℝ b q" and "c p \<congruent>ℝ c q"
    let ?m = "(1/2) *R (p + q)"
    from scaleR_right_distrib [of "1/2" p q] and
      scaleR_right_diff_distrib [of "1/2" q p] and
      scaleR_left_diff_distrib [of "1/2" 1 p]
    have "?m - p = (1/2) *R (q - p)" by simp
    with ‹p ≠ q› have "?m - p ≠ 0" by simp
    from scaleR_right_distrib [of "1/2" p q] and
      scaleR_right_diff_distrib [of "1/2" p q] and
      scaleR_left_diff_distrib [of "1/2" 1 q]
    have "?m - q = (1/2) *R (p - q)" by simp
    with ‹?m - p = (1/2) *R (q - p)›
      and scaleR_minus_right [of "1/2" "q - p"]
    have "?m - q = -(?m - p)" by simp
    with norm_minus_cancel [of "?m - p"] have
      "(norm (?m - q))2 = (norm (?m - p))2" by (simp only: norm_minus_cancel)
    { fix d
      assume "d p \<congruent>ℝ d q"
      hence "(norm (d - p))2 = (norm (d - q))2" by simp
      have "(d - ?m) ∙ (?m - p) = 0"
      proof -
        have "d + (-q) = d - q" by simp
        have "d + (-p) = d - p" by simp
        with dot_norm [of "d - ?m" "?m - p"] have
          "(d - ?m) ∙ (?m - p) =
          ((norm (d - p))2 - (norm (d - ?m))2 - (norm(?m - p))2) / 2"
          by simp
        also from ‹(norm (d - p))2 = (norm (d - q))2›
          and ‹(norm (?m - q))2 = (norm (?m - p))2›
        have
          "… = ((norm (d - q))2 - (norm (d - ?m))2 - (norm(?m - q))2) / 2"
          by simp
        also from dot_norm [of "d - ?m" "?m - q"]
          and ‹d + (-q) = d - q›
        have
          "… = (d - ?m) ∙ (?m - q)" by simp
        also from inner_minus_right [of "d - ?m" "?m - p"]
          and ‹?m - q = -(?m - p)›
        have
          "… = -((d - ?m) ∙ (?m - p))" by (simp only: inner_minus_left)
        finally have "(d - ?m) ∙ (?m - p) = -((d - ?m) ∙ (?m - p))" .
        thus "(d - ?m) ∙ (?m - p) = 0" by arith
      qed }
    note m_lemma = this
    with ‹a p \<congruent>ℝ a q› have "(a - ?m) ∙ (?m - p) = 0" by simp
    { fix d
      assume "d p \<congruent>ℝ d q"
      with m_lemma have "(d - ?m) ∙ (?m - p) = 0" by simp
      with dot_left_diff_distrib [of "d - ?m" "a - ?m" "?m - p"]
        and ‹(a - ?m) ∙ (?m - p) = 0›
      have "(d - a) ∙ (?m - p) = 0" by (simp add: inner_diff_left inner_diff_right) }
    with ‹b p \<congruent>ℝ b q› and ‹c p \<congruent>ℝ c q› have
      "(b - a) ∙ (?m - p) = 0" and "(c - a) ∙ (?m - p) = 0" by simp+
    with real2_orthogonal_dep2 and ‹?m - p ≠ 0› have "dep2 (b - a) (c - a)"
      by blast
    with Col_dep2 have "real_euclid.Col a b c" by auto
    with real_euclid.Col_def have "Bℝ a b c ∨ Bℝ b c a ∨ Bℝ c a b" by auto }
  thus "∀p q a b c :: real^2.
          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"
    by blast
qed

subsection ‹Special cases of theorems of Tarski's geometry›

lemma real_euclid_B_disjunction:
  assumes "l ≥ 0" and "b - a = l *R (c - a)"
  shows "Bℝ a b c ∨ Bℝ a c b"
proof cases
  assume "l ≤ 1"
  with ‹l ≥ 0› and ‹b - a = l *R (c - a)›
  have "Bℝ a b c" by (unfold real_euclid_B_def) (simp add: exI [of _ l])
  thus "Bℝ a b c ∨ Bℝ a c b" ..
next
  assume "¬ (l ≤ 1)"
  hence "1/l ≤ 1" by simp

  from ‹l ≥ 0› have "1/l ≥ 0" by simp

  from ‹b - a = l *R (c - a)›
  have "(1/l) *R (b - a) = (1/l) *R (l *R (c - a))" by simp
  with ‹¬ (l ≤ 1)› have "c - a = (1/l) *R (b - a)" by simp
  with ‹1/l ≥ 0› and ‹1/l ≤ 1›
  have "Bℝ a c b" by (unfold real_euclid_B_def) (simp add: exI [of _ "1/l"])
  thus "Bℝ a b c ∨ Bℝ a c b" ..
qed

text ‹The following are true in Tarski's geometry,
  but to prove this would require much more development of it,
  so only the Euclidean case is proven here.›

theorem real_euclid_th5_1:
  assumes "a ≠ b" and "Bℝ a b c" and "Bℝ a b d"
  shows "Bℝ a c d ∨ Bℝ a d c"
proof -
  from ‹Bℝ a b c› and ‹Bℝ a b d›
  obtain l and m where "l ≥ 0" and "b - a = l *R (c - a)"
    and "m ≥ 0" and "b - a = m *R (d - a)"
    by (unfold real_euclid_B_def) auto
  from ‹b - a = m *R (d - a)› and ‹a ≠ b› have "m ≠ 0" by auto

  from ‹l ≥ 0› and ‹m ≥ 0› have "l/m ≥ 0" by (simp add: zero_le_divide_iff)

  from ‹b - a = l *R (c - a)› and ‹b - a = m *R (d - a)›
  have "m *R (d - a) = l *R (c - a)" by simp
  hence "(1/m) *R (m *R (d - a)) = (1/m) *R (l *R (c - a))" by simp
  with ‹m ≠ 0› have "d - a = (l/m) *R (c - a)" by simp
  with ‹l/m ≥ 0› and real_euclid_B_disjunction
  show "Bℝ a c d ∨ Bℝ a d c" by auto
qed

theorem real_euclid_th5_3:
  assumes "Bℝ a b d" and "Bℝ a c d"
  shows "Bℝ a b c ∨ Bℝ a c b"
proof -
  from ‹Bℝ a b d› and ‹Bℝ a c d›
  obtain l and m where "l ≥ 0" and "b - a = l *R (d - a)"
    and "m ≥ 0" and "c - a = m *R (d - a)"
    by (unfold real_euclid_B_def) auto

  show "Bℝ a b c ∨ Bℝ a c b"
  proof cases
    assume "l = 0"
    with ‹b - a = l *R (d - a)› have "b - a = l *R (c - a)" by simp
    with ‹l = 0›
    have "Bℝ a b c" by (unfold real_euclid_B_def) (simp add: exI [of _ l])
    thus "Bℝ a b c ∨ Bℝ a c b" ..
  next
    assume "l ≠ 0"

    from ‹l ≥ 0› and ‹m ≥ 0› have "m/l ≥ 0" by (simp add: zero_le_divide_iff)

    from ‹b - a = l *R (d - a)›
    have "(1/l) *R (b - a) = (1/l) *R (l *R (d - a))" by simp
    with ‹l ≠ 0› have "d - a = (1/l) *R (b - a)" by simp
    with ‹c - a = m *R (d - a)› have "c - a = (m/l) *R (b - a)" by simp
    with ‹m/l ≥ 0› and real_euclid_B_disjunction
    show "Bℝ a b c ∨ Bℝ a c b" by auto
  qed
qed

end