Theory Tarski_Neutral_Model_Hilbert_Neutral

(* IsageoCoq - Tarski_Neutral_Model_Hilbert_Neutral.thy
Port part of GeoCoq 3.4.0 (https://geocoq.github.io/GeoCoq/)

Version 2.0.0 IsaGeoCoq
Copyright (C) 2021-2025 Roland Coghetto roland.coghetto ( a t ) cafr-msa2p.be

History
Version 1.0.0 IsaGeoCoq
Port part of GeoCoq 3.4.0 (https://geocoq.github.io/GeoCoq/) in Isabelle/Hol (Isabelle2021)
Copyright (C) 2021  Roland Coghetto roland_coghetto (at) hotmail.com

License: LGPL

This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 2.1 of the License, or (at your option) any later version.

This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
Lesser General Public License for more details.

You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA  02110-1301  USA
*)

theory Tarski_Neutral_Model_Hilbert_Neutral

imports 
  Tarski_Postulate_Parallels 
  Hilbert_Neutral
  Gupta_Neutral

begin

section "Tarski Neutral Model Hilbert Neutral"

context Hilbert_neutral_dimensionless

begin

interpretation Interp_Gupta_of_Tarski_neutral_dimensionless: 
  Gupta_neutral_dimensionless
  where BetG = Bet and
    CongG = Cong and
    GPA = PP and
    GPB = PQ  and
    GPC = PR
proof 
  show "∀a b. Cong a b b a" 
    by (simp add: cong_permT)
  show "∀a b p q r s. Cong a b p q ∧ Cong a b r s ⟶ Cong p q r s" 
    using cong_inner_transitivity by blast
  show "∀a b c. Cong a b c c ⟶ a = b" 
    by (simp add: cong_identity)
  show "∀a b c q. ∃x. Bet q a x ∧ Cong a x b c" 
    by (simp add: segment_construction)
  show "∀a b c d a' b' c' d'. a ≠ b ∧ Bet a b c ∧ Bet a' b' c' ∧
          Cong a b a' b' ∧ Cong b c b' c' ∧ Cong a d a' d' ∧ Cong b d b' d' ⟶
          Cong c d c' d'" 
    using five_segment by blast
  show "∀a b c. Bet a b c ⟶ Bet c b a" 
    using bet_comm by blast
  show "∀a b c d. Bet a b d ∧ Bet b c d ⟶ Bet a b c" 
    using bet_trans by blast
  show "∀a b c p q. Bet a p c ∧ Bet b q c ∧ a ≠ p ∧ c ≠ p ∧ b ≠ q ∧ 
          c ≠ q ∧ ¬ (Bet a b c ∨ Bet b c a ∨ Bet c a b) ⟶
          (∃x. Bet p x b ∧ Bet q x a)" 
    using pasch_general_case by auto
  show "¬ (Bet PP PQ PR ∨ Bet PQ PR PP ∨ Bet PR PP PQ)" 
    using lower_dim_l by blast
qed

interpretation H_to_T : Tarski_neutral_dimensionless
  where Bet = Bet and
    Cong = Cong and
    TPA = PP and
    TPB = PQ  and
    TPC = PR
proof 
  show "∀a b. Cong a b b a" 
    by (simp add: 
        Interp_Gupta_of_Tarski_neutral_dimensionless.cong_pseudo_reflexivityG)
  show "∀a b p q r s. Cong a b p q ∧ Cong a b r s ⟶ Cong p q r s" 
    using cong_inner_transitivity by blast
  show "∀a b c. Cong a b c c ⟶ a = b" 
    by (simp add: 
        Interp_Gupta_of_Tarski_neutral_dimensionless.cong_identityG)
  show "∀a b c q. ∃x. Bet q a x ∧ Cong a x b c" 
    by (simp add: 
        Interp_Gupta_of_Tarski_neutral_dimensionless.segment_constructionG)
  show "∀a b c d a' b' c' d'. a ≠ b ∧ Bet a b c ∧ Bet a' b' c' ∧
Cong a b a' b' ∧ Cong b c b' c' ∧ Cong a d a' d' ∧ Cong b d b' d' ⟶
Cong c d c' d'" 
    using Interp_Gupta_of_Tarski_neutral_dimensionless.five_segmentG by blast
  show "∀a b. Bet a b a ⟶ a = b" 
    by (simp add: bet_identity)
  show "∀a b c p q. Bet a p c ∧ Bet b q c ⟶ (∃x. Bet p x b ∧ Bet q x a)" 
    using Interp_Gupta_of_Tarski_neutral_dimensionless.inner_paschT by blast
  show "¬ Bet PP PQ PR ∧ ¬ Bet PQ PR PP ∧ ¬ Bet PR PP PQ" 
    using lower_dim_l by blast
qed

lemma MidH__Mid:
  assumes "M Midpoint A B"
  shows "H_to_T.Midpoint M A B"
proof -
  have "Bet A M B" 
    using Midpoint_def assms by blast
  moreover
  have "Cong A M M B" 
    using Midpoint_def assms by blast
  ultimately show ?thesis
    using H_to_T.Midpoint_def by blast
qed

lemma Mid__MidH:
  assumes "H_to_T.Midpoint M A B"
  shows "M Midpoint A B"
proof -
  have "Bet A M B" 
    using H_to_T.Midpoint_def assms by blast
  moreover
  have "Cong A M M B" 
    using H_to_T.Midpoint_def assms by blast
  ultimately show ?thesis
    by (simp add: Midpoint_def)
qed

lemma col_colh_1:
  assumes "H_to_T.Col A B C" 
  shows "ColH A B C" 
proof -
  have "Bet A B C ∨ Bet B C A ∨ Bet C A B"
    using assms H_to_T.Col_def by blast
  thus ?thesis 
    using bet_colH colH_permut_312 by blast
qed

lemma col_colh_2:
  assumes "ColH A B C" 
  shows "H_to_T.Col A B C"
proof -
  have "Bet A B C ∨ Bet B C A ∨ Bet C A B"
    by (simp add: ColH_bets assms)
  thus ?thesis 
    using H_to_T.Col_def by presburger
qed

lemma col_colh:
  shows "H_to_T.Col A B C ⟷ ColH A B C" 
  using col_colh_1 col_colh_2 by blast

lemma line_col:
  assumes "IsL l" and (**AJOUT**)
    "IncidL A l" and
    "IncidL B l" and 
    "IncidL C l"
  shows "H_to_T.Col A B C"
proof -
  have "ColH A B C" 
    using ColH_def assms(1) assms(2) assms(3) assms(4) by blast
  thus ?thesis
    by (simp add: col_colh_2)
qed

lemma bet__beth: 
  assumes "A ≠ B" and
    "B ≠ C" and
    "Bet A B C"
  shows "BetH A B C" 
  using Bet_def assms(1) assms(2) assms(3) by blast

lemma coplanar_plane0:
  assumes "ColH A B X" and 
    "ColH C D X"
  shows "∃ p. IncidP A p ∧ IncidP B p ∧ IncidP C p ∧ IncidP D p" 
proof -
  obtain l where "IsL l" and "IncidL A l" and "IncidL B l" and "IncidL X l" 
    using ColH_def assms(1) by blast
  obtain m where "IsL m" and "IncidL C m" and "IncidL D m" and "IncidL X m" 
    using ColH_def assms(2) by blast
  obtain Y where "X ≠ Y" and "IncidL Y l" 
    using ‹IncidL X l› other_point_on_line by blast
  {
    assume "EqL m l" 
    obtain Z where "¬ ColH X Y Z" 
      using ‹X ≠ Y› ncolH_exists by blast
    obtain p where "IsP p" and "IncidP X p" and "IncidP Y p" and "IncidP Z p" 
      using ‹¬ ColH X Y Z› plan_existence by blast
    hence "IncidLP l p" 
      using ‹IncidL X l› ‹IncidL Y l› ‹IsL l› ‹X ≠ Y› line_on_plane by blast
    hence ?thesis 
      using IncidLP_def IncidL_morphism ‹EqL m l› ‹IncidL A l› ‹IncidL B l› 
        ‹IncidL C m› ‹IncidL D m› ‹IsL m› by blast
  }
  moreover
  {
    assume "¬ EqL m l" 
    obtain Z where "X ≠ Z" and "IncidL Z m" 
      using ‹IncidL X m› other_point_on_line by blast
    have "¬ ColH X Y Z" 
      using IncidL_not_IncidL__not_colH ‹IncidL X l› ‹IncidL X m› ‹IncidL Y l› 
        ‹IncidL Z m› ‹IsL l› ‹IsL m› ‹X ≠ Y› ‹X ≠ Z› ‹¬ EqL m l› line_uniqueness by blast
    then obtain p where "IsP p" and "IncidP X p" and "IncidP Y p" and "IncidP Z p" 
      using plan_existence by blast
    hence "IncidLP l p" 
      using ‹IncidL X l› ‹IncidL Y l› ‹IsL l› ‹X ≠ Y› line_on_plane by blast
    moreover have "IncidLP m p" 
      using ‹IncidL X m› ‹IncidL Z m› ‹IncidP X p› ‹IncidP Z p› ‹IsL m› 
        ‹IsP p› ‹X ≠ Z› line_on_plane by blast
    ultimately have ?thesis 
      using IncidLP_def ‹IncidL A l› ‹IncidL B l› ‹IncidL C m› ‹IncidL D m› by blast
  }
  ultimately show ?thesis
    by blast
qed

lemma coplanar_plane1:
  assumes "Bet A B X ∨ Bet B X A ∨ Bet X A B" and
    "Bet C D X ∨ Bet D X C ∨ Bet X C D"
  shows "∃ p. IsP p ∧ IncidP A p ∧ IncidP B p ∧ IncidP C p ∧ IncidP D p" 
proof -
  have "ColH A B X"     
    by (meson assms(1) bet_colH colH_permut_312)
  moreover have "ColH C D X"     
    by (simp add: H_to_T.Col_def assms(2) col_colh_1)
  ultimately show ?thesis
    using Is_plane coplanar_plane0 by blast
qed

lemma coplanar_plane:
  assumes "H_to_T.Coplanar A B C D" 
  shows "∃ p. IsP p ∧ IncidP A p ∧ IncidP B p ∧ IncidP C p ∧ IncidP D p" 
proof -
  obtain X where H1: "(H_to_T.Col A B X ∧ H_to_T.Col C D X) ∨
                         (H_to_T.Col A C X ∧ H_to_T.Col B D X) ∨
                         (H_to_T.Col A D X ∧ H_to_T.Col B C X)" 
    using H_to_T.Coplanar_def assms by auto
  moreover have "(H_to_T.Col A B X ∧ H_to_T.Col C D X) ⟶ ?thesis" 
    using H_to_T.Col_def coplanar_plane1 by force
  moreover {
    assume "H_to_T.Col A C X" and
      "H_to_T.Col B D X"
    have "Bet A C X ∨ Bet C X A ∨ Bet X A C" 
      using H_to_T.Col_def ‹H_to_T.Col A C X› by presburger
    moreover have "Bet B D X ∨ Bet D X B ∨ Bet X B D" 
      using H1 H_to_T.Col_def ‹H_to_T.Col B D X› by blast
    ultimately have ?thesis 
      using coplanar_plane1 by blast
  }
  moreover {
    assume "H_to_T.Col A D X" and
      "H_to_T.Col B C X"
    have "Bet A D X ∨ Bet D X A ∨ Bet X A D" 
      using H_to_T.Col_def ‹H_to_T.Col A D X› by auto
    moreover have "Bet B C X ∨ Bet C X B ∨ Bet X B C" 
      using H_to_T.Col_def ‹H_to_T.Col B C X› by auto
    ultimately have ?thesis 
      using coplanar_plane1 by blast
  }
  ultimately show ?thesis
    by blast
qed

lemma plane_coplanar:
  assumes "IncidP A p" and
    "IncidP B p" and
    "IncidP C p" and
    "IncidP D p"
  shows "H_to_T.Coplanar A B C D"
proof -
  {
    assume "ColH A B C"
    hence "H_to_T.Col A B C" 
      using col_colh_2 by blast
    hence ?thesis 
      using H_to_T.ncop__ncols by blast
  }
  moreover
  {
    assume "¬ ColH A B C"
    hence "A ≠ B" 
      by (simp add: ncolH_distincts)
    obtain M where "M Midpoint A B"
      using H_to_T.midpoint_existence Mid__MidH by blast
    have "M ≠ A" 
      using Cong_def Hilbert_neutral_dimensionless_pre.Midpoint_def 
        ‹A ≠ B› ‹M Midpoint A B› by force
    have "M ≠ B" 
      using Midpoint_def Interp_Gupta_of_Tarski_neutral_dimensionless.cong_identityG 
        ‹A ≠ B› ‹M Midpoint A B› by blast
    have "ColH A B M" 
      using Midpoint_def ‹M Midpoint A B› bet_colH colH_permut_132 by blast
    then obtain m where "IsL m" and "IncidL A m" and "IncidL B m" and "IncidL M m" 
      using ColH_def by blast
    {
      assume "D = M" 
      hence ?thesis 
        using H_to_T.ncop__ncols col_colh_2 ‹ColH A B M› by blast
    }
    moreover
    {
      assume "D ≠ M" 
      obtain l where "IsL l" and" IncidL D l" and "IncidL M l" 
        using ‹D ≠ M› line_existence by blast
      {
        assume "IncidL A l" 
        hence "EqL m l" 
          using ‹IncidL A m› ‹IncidL M l› ‹IncidL M m› ‹IsL l› ‹IsL m› ‹M ≠ A› 
            line_uniqueness by presburger
        have "H_to_T.Col A B A ∧ H_to_T.Col C D A ∨ H_to_T.Col A C A ∧ H_to_T.Col B D A ∨ 
              H_to_T.Col A D A ∧ H_to_T.Col B C A" 
          by (meson ColH_def H_to_T.not_col_distincts IncidL_morphism Is_line 
              ‹EqL m l› ‹IncidL A l› ‹IncidL B m› ‹IncidL D l› col_colh_2)
        hence ?thesis 
          using H_to_T.Coplanar_def by blast
      }
      moreover
      {
        assume "¬ IncidL A l"
        {
          assume "IncidL B l" 
          hence "EqL l m" 
            using ‹IncidL B m› ‹IncidL M l› ‹IncidL M m› ‹IsL l› ‹IsL m› 
              ‹M ≠ B› line_uniqueness by blast
          hence False 
            using ‹IncidL A m› ‹IncidL B l› ‹IncidL B m› ‹IncidL M l› 
              ‹IncidL M m› ‹M ≠ B› ‹¬ IncidL A l› inter_incid_uniquenessH by blast
        }
        {
          assume "IncidL C l" 
          hence "H_to_T.Col A B M ∧ H_to_T.Col C D M ∨ H_to_T.Col A C M ∧ H_to_T.Col B D M ∨ 
                    H_to_T.Col A D M ∧ H_to_T.Col B C M" 
            using Hilbert_neutral_dimensionless_pre.ColH_def ‹ColH A B M› 
              ‹IncidL D l› ‹IncidL M l› ‹IsL l› col_colh by fastforce
          hence ?thesis 
            using H_to_T.Coplanar_def by blast
        }
        moreover
        {
          assume "¬ IncidL C l"
          have "IncidP M p" 
            using ‹A ≠ B› ‹ColH A B M› assms(1) assms(2) line_on_plane' by blast
          have
            "¬ ColH A B C ∧ IsL l ∧ IsP p ∧ IncidP A p ∧ IncidP B p ∧ 
             IncidP C p ∧ IncidLP l p ∧ ¬ IncidL C l ∧ (cut l A B)
        ⟶
        (cut l A C) ∨ (cut l B C)" 
            using pasch by blast
          moreover
          {
            assume "cut l A C"
            then obtain I where "IncidL I l" and "BetH A I C" 
              using local.cut_def by blast
            {
              assume "H_to_T.Col I A B"
              have "A ≠ I" 
                using ‹IncidL I l› ‹¬ IncidL A l› by auto
              moreover have "ColH A I A" 
                by (simp add: colH_trivial121)
              moreover have "ColH A I C" 
                by (simp add: ‹BetH A I C› between_col)
              ultimately have False
                using ‹¬ ColH A B C› colH_trans ‹H_to_T.Col I A B› 
                  colH_permut_213 col_colh_1 by blast
            }
            hence "¬ H_to_T.Col I A B" 
              by blast
            moreover have "H_to_T.Coplanar I A B C" 
              using H_to_T.bet__coplanar H_to_T.ncoplanar_perm_7 ‹BetH A I C›
                betH_to_bet by blast
            moreover 
            have "H_to_T.Col I D M" 
              using ColH_def ‹IncidL D l› ‹IncidL I l› ‹IncidL M l› ‹IsL l› col_colh by auto
            have "H_to_T.Col A B M" 
              using ‹ColH A B M› col_colh_2 by fastforce
            hence "H_to_T.Col I A M ∧ H_to_T.Col B D M ∨ H_to_T.Col I B M ∧ H_to_T.Col A D M ∨
                    H_to_T.Col I D M ∧ H_to_T.Col A B M" 
              using ‹H_to_T.Col I D M› by auto
            hence "H_to_T.Coplanar I A B D" 
              using H_to_T.Coplanar_def by blast
            ultimately have ?thesis 
              using H_to_T.coplanar_trans_1 by blast
          }
          moreover 
          {
            assume "cut l B C"
            then obtain I where "IncidL I l" and "BetH B I C" 
              using local.cut_def by blast
            {
              assume "H_to_T.Col I B A"
              have "B ≠ I" 
                using ‹IncidL B l ⟹ False› ‹IncidL I l› by fastforce
              moreover have "ColH B I A" 
                using ‹H_to_T.Col I B A› colH_permut_213 col_colh by blast
              moreover have "ColH B I B" 
                by (simp add: colH_trivial121)
              ultimately have False
                using ‹BetH B I C› ‹¬ ColH A B C› between_col colH_trans by blast
            }
            hence "¬ H_to_T.Col I B A" 
              by blast
            moreover have "H_to_T.Coplanar I B A C" 
              using H_to_T.bet__coplanar H_to_T.ncoplanar_perm_7 ‹BetH B I C›
                betH_to_bet by blast
            moreover 
            have "H_to_T.Col I D M" 
              using ColH_def ‹IncidL D l› ‹IncidL I l› ‹IncidL M l› ‹IsL l› col_colh by auto
            have "H_to_T.Col B A M" 
              by (metis Bet_def H_to_T.Col_def ‹ColH A B M› between_comm between_one)
            hence "H_to_T.Col I B M ∧ H_to_T.Col A D M ∨ H_to_T.Col I A M ∧ H_to_T.Col B D M ∨
                    H_to_T.Col I D M ∧ H_to_T.Col B A M" 
              using ‹H_to_T.Col I D M› by auto
            hence "H_to_T.Coplanar I B A D" 
              using H_to_T.Coplanar_def by blast
            ultimately have ?thesis 
              using H_to_T.coplanar_trans_1 H_to_T.ncoplanar_perm_6 by blast
          }
          ultimately have ?thesis                 
            by (metis (mono_tags, lifting) Bet_def line_on_plane Is_plane Midpoint_def
                ‹ColH A B C ⟹ H_to_T.Coplanar A B C D› ‹D = M ⟹ H_to_T.Coplanar A B C D›
                ‹IncidL B l ⟹ False› ‹IncidL D l› ‹IncidL M l› ‹IncidP M p› ‹IsL l›
                ‹M Midpoint A B› ‹¬ IncidL A l› ‹¬ IncidL C l› assms(1) assms(2)
                assms(3) assms(4) local.cut_def)
        }
        ultimately have ?thesis 
          by blast
      }
      ultimately have ?thesis 
        by blast
    }
    ultimately have ?thesis 
      by blast
  }
  ultimately show ?thesis
    by blast
qed

lemma pars__para:
  assumes "IncidL A l" and
    "IncidL B l" and
    "IncidL C m" and
    "IncidL D m" and
    "H_to_T.ParStrict A B C D"
  shows "Para l m" 
proof -
  have "A ≠ B" 
    using H_to_T.par_strict_neq1 assms(5) by auto
  have "C ≠ D" 
    using H_to_T.par_strict_distinct assms(5) by presburger
  have "IsL l" 
    using Is_line assms(1) by blast
  moreover have "IsL m" 
    using Is_line assms(4) by blast
  moreover 
  {
    fix X
    assume "IncidL X l" and "IncidL X m"
    hence "H_to_T.Col X A B" 
      using assms(1) assms(2) Is_line line_col by blast
    moreover have "H_to_T.Col X C D" 
      using assms(1) assms(2) Is_line line_col ‹IncidL X m› assms(3) assms(4) by auto
    ultimately have False 
      using H_to_T.par_not_col assms(5) by blast
  }
  moreover
  obtain p where "IsP p" and "IncidP A p" and "IncidP B p" and "IncidP C p" and "IncidP D p" 
    using H_to_T.pars__coplanar assms(5) coplanar_plane by blast
  have "∃ p. IncidLP l p ∧ IncidLP m p" 
  proof -
    have "IncidLP l p" 
      using ‹A ≠ B› ‹IncidP A p› ‹IncidP B p› ‹IsP p› assms(1) assms(2) 
        calculation(1) line_on_plane by blast
    moreover have "IncidLP m p" 
      using ‹C ≠ D› ‹IncidP C p› ‹IncidP D p› ‹IsP p› assms(3) assms(4) 
        line_on_plane ‹IsL m› by blast
    ultimately show ?thesis 
      by blast
  qed
  ultimately show ?thesis 
    using Para_def by blast
qed

lemma par__or_eq_para:
  assumes "IncidL A l" and
    "IncidL B l" and
    "IncidL C m" and
    "IncidL D m" and
    "H_to_T.Par A B C D"
  shows "Para l m ∨ EqL l m" 
proof -
  {
    assume "H_to_T.ParStrict A B C D" 
    hence ?thesis 
      using assms(1) assms(2) assms(3) assms(4) pars__para by blast
  }
  moreover
  {
    assume "A ≠ B" and
      "C ≠ D" and
      "H_to_T.Col A C D" and
      "H_to_T.Col B C D"
    hence ?thesis 
      by (meson IncidL_not_IncidL__not_colH Is_line assms(1) assms(2) assms(3) 
          assms(4) colH_permut_231 col_colh_1 line_uniqueness)
  }
  ultimately show ?thesis 
    using H_to_T.Par_def assms(5) by presburger
qed

lemma tarski_upper_dim:
  assumes 
    plane_intersection_assms: "∀ A p q. IsP p ∧ IsP q ∧ IncidP A p ∧ IncidP A q 
                                ⟶ (∃ B. IncidP B p ∧ IncidP B q ∧ A ≠ B)" and 
    lower_dim_3_assms: "¬ (∃ p. IsP p ∧ IncidP HS1 p ∧ IncidP HS2 p ∧ 
                                IncidP HS3 p ∧ IncidP HS4 p)" and
    "P ≠ Q" and
    "Q ≠ R" and
    "P ≠ R" and
    "Cong A P A Q" and
    "Cong B P B Q" and
    "Cong C P C Q" and
    "Cong A P A R" and
    "Cong B P B R" and
    "Cong C P C R"
  shows "Bet A B C ∨ Bet B C A ∨ Bet C A B" 
proof -
  have "H_to_T.upper_dim_3_axiom ⟶ ?thesis" 
    using H_to_T.upper_dim_3_axiom_def assms(10) assms(11) assms(3) assms(4) 
      assms(5) assms(6) assms(7) assms(8) assms(9) by blast
  moreover
  have "H_to_T.plane_intersection_axiom ⟶ H_to_T.upper_dim_3_axiom" 
    using H_to_T.upper_dim_3_equivalent_axioms by force
  moreover
  {
    fix A B C D E F P
    assume "H_to_T.Coplanar A B C P" and
      "H_to_T.Coplanar D E F P"
    obtain p where "IsP p" and "IncidP A p" and "IncidP B p" and "IncidP C p" and "IncidP P p" 
      using ‹H_to_T.Coplanar A B C P› coplanar_plane by blast
    obtain q where "IsP q" and "IncidP D q" and "IncidP E q" and "IncidP F q" and "IncidP P q" 
      using ‹H_to_T.Coplanar D E F P› coplanar_plane by blast
    obtain Q where "IncidP Q p" and "IncidP Q q" and "P ≠ Q" 
      using plane_intersection_assms Is_plane ‹IncidP P p› ‹IncidP P q› by blast   
    have "H_to_T.Coplanar A B C Q" 
      using ‹IncidP A p› ‹IncidP B p› ‹IncidP C p› ‹IncidP Q p› plane_coplanar by force
    moreover have "H_to_T.Coplanar D E F Q" 
      using ‹IncidP D q› ‹IncidP E q› ‹IncidP F q› ‹IncidP Q q› plane_coplanar by force
    ultimately have "∃ Q. H_to_T.Coplanar A B C Q ∧ H_to_T.Coplanar D E F Q ∧ P ≠ Q" 
      using ‹P ≠ Q› by blast
  }
  hence "H_to_T.plane_intersection_axiom" 
    using H_to_T.plane_intersection_axiom_def by force
  ultimately show ?thesis
    by simp
qed

lemma Col__ColH:
  assumes "H_to_T.Col A B C"
  shows "ColH A B C" 
  using assms col_colh by blast

lemma ColH__Col: 
  assumes "ColH A B C"
  shows "H_to_T.Col A B C" 
  using assms ColH_bets col_colh by blast

lemma playfair_s_postulateH: 
  assumes euclid_uniqueness: "∀ l P m1 m2. IsL l ∧ IsL m1 ∧ IsL m2 ∧
     ¬ IncidL P l ∧ Para l m1 ∧ IncidL P m1 ∧ Para l m2 ∧ IncidL P m2 ⟶
     EqL m1 m2"
  shows "H_to_T.playfair_s_postulate" 
proof -
  {
    fix A1 A2 B1 B2 C1 C2 P
    assume "H_to_T.Par A1 A2 B1 B2" and
      "H_to_T.Col P B1 B2" and
      "H_to_T.Par A1 A2 C1 C2" and
      "H_to_T.Col P C1 C2"
    have "A1 ≠ A2" 
      using H_to_T.par_distinct ‹H_to_T.Par A1 A2 B1 B2› by blast
    then obtain l where "IsL l" and "IncidL A1 l" and "IncidL A2 l" 
      using line_existence by fastforce
    have "B1 ≠ B2" 
      using H_to_T.par_distinct ‹H_to_T.Par A1 A2 B1 B2› by blast
    then obtain m1 where "IsL m1" and "IncidL B1 m1" and "IncidL B2 m1" 
      using line_existence by fastforce
    have "C1 ≠ C2" 
      using H_to_T.par_distinct ‹H_to_T.Par A1 A2 C1 C2› by blast
    then obtain m2 where "IsL m2" and "IncidL C1 m2" and "IncidL C2 m2" 
      using line_existence by fastforce
    {
      assume "IncidL P l" 
      have "ColH A1 A2 P" 
        using ColH_def Is_line ‹IncidL A1 l› ‹IncidL A2 l› ‹IncidL P l› by blast
      hence "H_to_T.Col A1 A2 P" 
        by (simp add: col_colh)
      have "H_to_T.Col A1 B1 B2" 
        by (metis H_to_T.col3 H_to_T.not_col_distincts H_to_T.not_strict_par1
            H_to_T.not_strict_par2 ‹A1 ≠ A2› ‹H_to_T.Col A1 A2 P› ‹H_to_T.Col P B1 B2›
            ‹H_to_T.Par A1 A2 B1 B2›)
      have "H_to_T.Col A2 B1 B2"
        using H_to_T.Par_def H_to_T.not_col_permutation_2 H_to_T.par_strict_not_col_3 
          ‹H_to_T.Col A1 B1 B2› ‹H_to_T.Par A1 A2 B1 B2› by blast
      have "H_to_T.ParStrict A1 A2 C1 C2 ⟶ H_to_T.Col C1 B1 B2 ∧ H_to_T.Col C2 B1 B2" 
        using H_to_T.Col_cases H_to_T.par_not_col ‹H_to_T.Col A1 A2 P› 
          ‹H_to_T.Col P C1 C2› by blast
      moreover have "A1 ≠ A2 ∧ C1 ≠ C2 ∧ H_to_T.Col A1 C1 C2 ∧ H_to_T.Col A2 C1 C2 
                       ⟶ H_to_T.Col C1 B1 B2 ∧ H_to_T.Col C2 B1 B2" 
      proof -
        have "A1 ≠ A2 ∧ C1 ≠ C2 ∧ H_to_T.Col A1 C1 C2 ∧ H_to_T.Col A2 C1 C2 
               ⟶ H_to_T.Col C1 B1 B2" 
          by (meson H_to_T.col_permutation_1 H_to_T.l6_21 ‹H_to_T.Col A1 B1 B2›
              ‹H_to_T.Col A2 B1 B2›)
        moreover have "A1 ≠ A2 ∧ C1 ≠ C2 ∧ H_to_T.Col A1 C1 C2 ∧ H_to_T.Col A2 C1 C2 
                         ⟶ H_to_T.Col C2 B1 B2"
          using H_to_T.col_permutation_1 H_to_T.l6_21 
          by (metis H_to_T.col_permutation_1 H_to_T.colx ‹H_to_T.Col A1 B1 B2›
              ‹H_to_T.Col A2 B1 B2› calculation)
        ultimately show ?thesis
          by blast
      qed
      ultimately have "H_to_T.Col C1 B1 B2 ∧ H_to_T.Col C2 B1 B2" 
        using H_to_T.Par_def ‹H_to_T.Par A1 A2 C1 C2› by force
    }
    moreover
    {
      assume "¬ IncidL P l" 
      have "¬ ColH A1 A2 P" 
        using IncidL_not_IncidL__not_colH ‹A1 ≠ A2› ‹IncidL A1 l› ‹IncidL A2 l› 
          ‹¬ IncidL P l› by blast
      hence "¬ H_to_T.Col A1 A2 P" 
        using col_colh by blast
      have "Para l m1" 
      proof -
        have "H_to_T.ParStrict A1 A2 B1 B2" 
          using H_to_T.col_permutation_2 H_to_T.par_not_col_strict 
            ‹H_to_T.Col P B1 B2› ‹H_to_T.Par A1 A2 B1 B2› ‹¬ H_to_T.Col A1 A2 P› by blast
        moreover have "H_to_T.ParStrict A1 A2 B1 B2 ⟶ Para l m1" 
          using ‹IncidL A1 l› ‹IncidL A2 l› ‹IncidL B1 m1› ‹IncidL B2 m1› pars__para by blast
        ultimately show ?thesis 
          by blast
      qed
      have "Para l m2" 
      proof -
        have "H_to_T.ParStrict A1 A2 C1 C2" 
          using H_to_T.not_col_permutation_2 H_to_T.par_not_col_strict 
            ‹H_to_T.Col P C1 C2› ‹H_to_T.Par A1 A2 C1 C2› ‹¬ H_to_T.Col A1 A2 P› by blast
        moreover have "H_to_T.ParStrict A1 A2 C1 C2 ⟶ Para l m2" 
          using ‹IncidL A1 l› ‹IncidL A2 l› ‹IncidL C1 m2› ‹IncidL C2 m2› pars__para by auto
        ultimately show ?thesis 
          by blast
      qed
      have "IncidL P m1" 
        using H_to_T.not_col_permutation_2 IncidL_not_IncidL__not_colH ‹B1 ≠ B2› 
          ‹H_to_T.Col P B1 B2› ‹IncidL B1 m1› ‹IncidL B2 m1› col_colh by blast
      have "IncidL P m2" 
        using H_to_T.not_col_permutation_2 IncidL_not_IncidL__not_colH ‹C1 ≠ C2› 
          ‹H_to_T.Col P C1 C2› ‹IncidL C1 m2› ‹IncidL C2 m2› col_colh by blast
      have "EqL m1 m2" 
        using ‹IncidL P m1› ‹IncidL P m2› ‹IsL l› ‹IsL m1› ‹IsL m2› ‹Para l m1› 
          ‹Para l m2› ‹¬ IncidL P l› assms by blast
      hence "H_to_T.Col C1 B1 B2 ∧ H_to_T.Col C2 B1 B2" 
        by (meson IncidL_morphism ‹IncidL B1 m1› ‹IncidL B2 m1› ‹IncidL C1 m2› 
            ‹IncidL C2 m2› ‹IsL m1› ‹IsL m2› line_col)
    }
    ultimately have "H_to_T.Col C1 B1 B2 ∧ H_to_T.Col C2 B1 B2" 
      by blast
  }
  thus ?thesis 
    using H_to_T.playfair_s_postulate_def by blast       
qed

lemma tarski_s_euclid_aux: 
  assumes euclid_uniqueness: "∀ l P m1 m2. IsL l ∧ IsL m1 ∧ IsL m2 ∧ 
     ¬ IncidL P l ∧ Para l m1 ∧ IncidL P m1 ∧ Para l m2 ∧ IncidL P m2 ⟶
     EqL m1 m2"
  shows "H_to_T.tarski_s_parallel_postulate" 
proof -
  have "H_to_T.playfair_s_postulate ⟶ H_to_T.tarski_s_parallel_postulate" 
    using H_to_T.InterAx5 H_to_T.Postulate01_def H_to_T.Postulate02_def by blast
  moreover
  have "H_to_T.playfair_s_postulate" 
    using playfair_s_postulateH assms(1) by blast
  ultimately show ?thesis 
    by blast
qed

lemma tarski_s_euclid: 
  assumes euclid_uniqueness: "∀ l P m1 m2. IsL l ∧ IsL m1 ∧ IsL m2 ∧
           ¬ IncidL P l ∧ Para l m1 ∧ IncidL P m1 ∧ Para l m2 ∧ IncidL P m2 ⟶
           EqL m1 m2"
  shows 
    "∀A B C D T. Bet A D T ∧ Bet B D C ∧ A ≠ D ⟶ (∃X Y. Bet A B X ∧ Bet A C Y ∧ Bet X T Y)"
  using assms(1) tarski_s_euclid_aux H_to_T.tarski_s_parallel_postulate_def by blast

end
end