Theory Tarski_Neutral_2D_Model_Hilbert_Neutral_2D

(* IsageoCoq - Tarski_Neutral_2D_Model_Hilbert_Neutral_2D.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_2D_Model_Hilbert_Neutral_2D

imports 
  Tarski_Neutral_2D
  Hilbert_Neutral_2D

begin

section "Tarski Neutral 2D - Hilbert Neutral 2D Model"

context Hilbert_neutral_2D

begin

lemma plane_separation_2D:
  assumes "¬ ColH A X Y" and
    "¬ ColH B X Y" 
  shows "cut' A B X Y ∨ same_side' A B X Y" 
proof -
  have "X ≠ Y" 
    using assms(2) colH_trivial122 by blast
  obtain l where "IsL l" and "IncidL X l" and "IncidL Y l" 
    using ‹X ≠ Y› line_existence by blast
  obtain C where "cut l A C" 
    using ColH_def ‹IncidL X l› ‹IncidL Y l› ‹IsL l› assms(1) cut_exists by blast
  {
    assume "A = B"
    hence "same_side' A B X Y" 
      using assms(1) colH_permut_312 same_side_prime_refl by blast
    hence ?thesis 
      by blast
  }
  moreover
  {
    assume "A ≠ B"
    have "A ≠ C" 
      using ‹local.cut l A C› cut_distinct by blast
    {
      assume "B = C"
      obtain m where "IsL m" and "IncidL X m" and "IncidL Y m" 
        using Is_line ‹IncidL X l› ‹IncidL Y l› by blast
      obtain I where "IncidL I l" and "BetH A I C" 
        using ‹local.cut l A C› local.cut_def by blast
      {
        fix m
        assume "IsL m" and "IncidL X m" and "IncidL Y m"
        hence "cut m A B" 
          by (metis ColH_def ‹B = C› ‹IncidL X l› ‹IncidL Y l› ‹X ≠ Y› 
              ‹⋀thesis. (⋀I. ⟦IncidL I l; BetH A I C⟧ ⟹ thesis) ⟹ thesis› assms(1) 
              assms(2) inter_incid_uniquenessH local.cut_def)
      }
      hence "cut' A C X Y" 
        using ‹X ≠ Y› ‹B = C› cut'_def by auto
      hence ?thesis 
        using ‹B = C› by blast
    }
    moreover
    {
      assume "B ≠ C"
      {
        assume "ColH A C B"
        obtain I where "IncidL I l" and "BetH A I C" 
          using ‹local.cut l A C› local.cut_def by blast
        hence "ColH A I C" 
          using betH_colH by blast
        hence "ColH A I B" 
          by (meson colH_permut_132 colH_trans colH_trivial121 ‹A ≠ C› ‹ColH A C B›)
        hence "BetH A I B ∨ BetH I B A ∨ BetH I A B" 
          using ColH_def ‹A ≠ B› ‹BetH A I C› ‹IncidL I l› ‹IncidL X l› 
            ‹IncidL Y l› ‹IsL l› assms(2) betH_colH between_one by blast
        have "¬ IncidL A l" 
          using ‹local.cut l A C› local.cut_def by auto
        {
          assume "BetH A I B"
          {
            fix m
            assume "IsL m" and "IncidL X m" and "IncidL Y m" 
            have "¬ IncidL B m" 
              using ColH_def ‹IncidL X m› ‹IncidL Y m› ‹IsL m› assms(2) by blast
            moreover have "∃ I0. IncidL I0 m ∧ BetH A I0 B" 
              using ‹BetH A I B› ‹IncidL I l› ‹IncidL X l› ‹IncidL X m› 
                ‹IncidL Y l› ‹IncidL Y m› ‹X ≠ Y› inter_incid_uniquenessH by blast
            ultimately have "cut m A B" 
              using ‹IncidL X l› ‹IncidL X m› ‹IncidL Y l› ‹IncidL Y m› ‹IsL m› 
                ‹X ≠ Y› ‹¬ IncidL A l› inter_incid_uniquenessH local.cut_def by blast
          }
          hence "cut' A B X Y" 
            by (simp add: ‹X ≠ Y› cut'_def)
        }
        moreover have "BetH I B A ⟶ same_side' A B X Y" 
          using ‹IncidL I l› ‹IncidL X l› ‹IncidL Y l› ‹X ≠ Y› ‹¬ IncidL A l› 
            outH_def out_same_side' by auto
        moreover have "BetH I A B ⟶ same_side' A B X Y" 
          using ‹IncidL I l› ‹IncidL X l› ‹IncidL Y l› ‹X ≠ Y› ‹¬ IncidL A l›
            outH_def out_same_side' by auto
        ultimately have ?thesis 
          using ‹BetH A I B ∨ BetH I B A ∨ BetH I A B› by fastforce
      }
      moreover
      {
        assume "¬ ColH A C B"
        have "¬ IncidL B l" 
          using ColH_def Is_line ‹IncidL X l› ‹IncidL Y l› assms(2) by blast
        moreover {
          assume "cut l A B"
          {
            fix m
            assume "IsL m" and "IncidL X m" and "IncidL Y m"
            hence "EqL m l" 
              using ‹IncidL X l› ‹IncidL Y l› ‹IsL l› ‹IsL m› ‹X ≠ Y› 
                line_uniqueness by blast
            hence "cut m A B" 
              by (meson ‹IsL m› ‹local.cut l A B› local.cut_def morph)
          }
          hence "cut' A B X Y"
            using ‹X ≠ Y› cut'_def by auto
        }
        {
          assume "cut l C B"
          {
            fix m
            assume "IsL m" and "IncidL X m" and "IncidL Y m"
            hence "EqL m l" 
              using ‹IncidL X l› ‹IncidL Y l› ‹IsL l› ‹X ≠ Y› line_uniqueness by blast
            have "cut m A C" 
              by (meson ‹IncidL X l› ‹IncidL X m› ‹IncidL Y l› ‹IncidL Y m›
                  ‹IsL m› ‹X ≠ Y› ‹local.cut l A C› inter_incid_uniquenessH local.cut_def)
            moreover have "cut m B C" 
              by (meson ‹EqL m l› ‹IsL m› ‹local.cut l C B› cut_comm local.cut_def morph)
            ultimately have "same_side A B m" 
              using ‹IsL m› same_side_def by blast
          }
          hence "same_side' A B X Y" 
            by (simp add: ‹X ≠ Y› same_side'_def)
          have ?thesis
            using ‹IsL l› ‹¬ ColH A C B› ‹local.cut l A C› pasch_2D 
              ‹same_side' A B X Y› by blast
        }
        ultimately have ?thesis 
          using ‹IsL l› ‹¬ ColH A C B› ‹local.cut l A B ⟹ cut' A B X Y›
            ‹local.cut l A C› pasch_2D by blast
      }
      ultimately have ?thesis 
        by blast
    }
    ultimately have ?thesis 
      by blast
  }
  ultimately show ?thesis 
    by blast
qed

lemma col_upper_dim:
  assumes "ColH A P Q" and
    "P ≠ Q" and
    "A ≠ B" and
    "A ≠ C" and
    "B ≠ C" and
    "A ≠ P" and
    "A ≠ Q" and
    "B ≠ P" and
    "B ≠ Q" and
    "C ≠ P" and
    "C ≠ Q" and
    "CongH A P A Q" and
    "CongH B P B Q" and
    "CongH C P C Q"
  shows "Bet A B C ∨ Bet B C A ∨ Bet C A B" 
proof -
  {
    assume "ColH B P Q"
    hence "BetH P B Q" 
      using assms(13) assms(2) assms(8) assms(9) congH_colH_betH by auto
    {
      assume "BetH P A B"
      hence "BetH Q B A" 
        using ‹BetH P B Q› betH_trans0 between_comm by blast
      hence False 
        using ‹BetH P A B› assms(12) assms(13) assms(7) assms(9) 
          betH_congH2__False congH_permlr by blast
    }
    moreover
    {
      assume "BetH P B A"
      hence "BetH Q A B" 
        by (metis assms(1) assms(12) assms(2) assms(6) assms(7) 
            betH_trans0 between_comm congH_colH_betH)
      hence False 
        using ‹BetH P B A› assms(12) assms(13) assms(7) assms(9) 
          betH_congH2__False congH_permlr by blast
    }
    ultimately have False 
      by (metis ‹BetH P B Q› assms(1) assms(12) assms(2) assms(3) 
          assms(6) betH2_out congH_colH_betH)
  }
  hence "¬ ColH B P Q" 
    by blast
  {
    assume "ColH C P Q"
    hence "BetH P C Q" 
      using assms(10) assms(11) assms(14) assms(2) congH_colH_betH by force
    {
      assume "BetH P A C"
      hence "BetH Q C A" 
        using ‹BetH P C Q› betH_trans0 between_comm by blast
      hence False 
        using ‹BetH P A C› assms(11) assms(12) assms(14) assms(7) 
          betH_congH2__False congH_permlr by blast
    }
    moreover
    {
      assume "BetH P C A"
      hence "BetH Q A C" 
        by (metis assms(1) assms(12) assms(2) assms(6) assms(7) 
            betH_trans0 between_comm congH_colH_betH)
      hence False 
        using ‹BetH P C A› assms(10) assms(11) assms(12) assms(14) 
          assms(6) assms(7) betH_congH2__False congH_perms by blast
    }
    ultimately have False 
      by (metis congH_colH_betH ‹BetH P C Q› assms(1) assms(12) assms(2) 
          assms(4) assms(6) betH2_out)
  }
  hence "¬ ColH C P Q" 
    by blast
  {
    assume "cut' B C P Q"
    obtain l where "IsL l" and "IncidL P l" and "IncidL Q l" 
      using assms(2) line_existence by blast
    have "cut l B C" 
      using ‹IncidL P l› ‹IncidL Q l› ‹IsL l› ‹cut' B C P Q› cut'_def by auto
    obtain I where "IncidL I l" and "BetH B I C" 
      using ‹local.cut l B C› local.cut_def by blast
    {
      assume "P = I"
      hence "ColH B Q C" 
        by (metis ‹BetH B I C› assms(11) assms(13) assms(14) assms(5)
            congH_permlr congH_refl cong_preserves_col)
      hence False 
        by (metis betH2_out ‹BetH B I C› ‹P = I› ‹¬ ColH B P Q› assms(13) 
            assms(14) assms(2) assms(9) betH_colH bet_cong3_bet colH_permut_132 
            congH_permlr congH_refl)
    }
    hence "P ≠ I" by blast
    {
      assume "Q = I"
      hence "ColH B P C" 
        by (metis ‹BetH B I C› assms(10) assms(11) assms(13) assms(14) 
            assms(5) assms(8) congH_perms congH_refl congH_sym cong_preserves_col)
      hence False 
        by (metis Hilbert_neutral_dimensionless_pre.Bet_def ‹BetH B I C› 
            ‹IncidL P l› ‹Q = I› ‹¬ ColH B P Q› ‹local.cut l B C› betH2_out bet_colH 
            between_one colH_permut_132 local.cut_def outH_def out_same_side same_side_not_cut)
    }
    hence "Q ≠ I"
      by blast
    have "ColH P Q I" 
      using ColH_def ‹IncidL I l› ‹IncidL P l› ‹IncidL Q l› ‹IsL l› by blast
    have "CongaH I B P I B Q" 
    proof -
      have "CongaH C B P C B Q" 
      proof -
        have "¬ ColH B C P" 
          by (metis (full_types) ‹BetH B I C› ‹ColH B P Q ⟹ False› 
              ‹ColH P Q I› ‹P = I ⟹ False› colH_permut_312 colH_trivial121 
              inter_uniquenessH outH_def outH_expand)
        moreover have "¬ ColH B C Q" 
          by (meson assms(10) assms(11) assms(13) assms(14) assms(5) 
              assms(8) assms(9) calculation congH_refl congH_sym cong_preserves_col_stronger)
        moreover have "CongH B C B C" 
          by (simp add: assms(5) congH_refl)
        moreover have "CongH B P B Q" 
          by (simp add: assms(13))
        moreover have "CongH C P C Q" 
          by (simp add: assms(14))
        ultimately show ?thesis 
          using th18_aux by blast
      qed
      moreover have "outH B C I" 
        by (simp add: ‹BetH B I C› outH_def)
      moreover have "outH B P P" 
        by (simp add: assms(8) outH_def)
      moreover have "outH B Q Q" 
        by (simp add: assms(9) outH_def)
      ultimately show ?thesis 
        using conga_out_conga by blast
    qed
    have "CongH I P I Q" 
    proof -
      have "¬ ColH B I P" 
        by (metis ‹ColH P Q I› ‹P = I ⟹ False› ‹¬ ColH B P Q› 
            colH_permut_312 colH_trivial122 inter_uniquenessH)
      moreover have "¬ ColH B I Q" 
        using IncidL_not_IncidL__not_colH ‹IncidL I l› ‹IncidL Q l› 
          ‹Q = I ⟹ False› ‹local.cut l B C› colH_permut_321 local.cut_def by blast
      moreover have "CongH B I B I" 
        using ‹BetH B I C› betH_distincts congH_refl by auto
      moreover have "CongH B P B Q" 
        by (simp add: assms(13))
      moreover have "CongaH I B P I B Q" 
        by (simp add: ‹CongaH I B P I B Q›)
      ultimately show ?thesis  
        using th12 by blast
    qed
    have "A = I ⟶ ?thesis" 
      using Bet_def ‹BetH B I C› between_comm by blast
    moreover 
    {
      assume "A ≠ I" 
      have "ColH I P Q" 
        by (simp add: ‹ColH P Q I› colH_permut_312)
      hence "BetH P I Q" 
        by (simp add: ‹CongH I P I Q› ‹P ≠ I› ‹Q ≠ I› assms(2) congH_colH_betH)
      {
        assume "BetH P A I"
        hence "BetH Q I A" 
          using ‹BetH P I Q› betH_trans0 between_comm by blast
        hence False 
          by (metis ‹BetH P A I› ‹CongH I P I Q› ‹Q ≠ I› assms(12) assms(7)
              betH_congH2__False congH_permlr)
      }
      moreover {
        assume "BetH P I A"
        hence "BetH Q A I" 
          by (metis assms(1) assms(12) assms(2) assms(6) assms(7) betH_trans0 
              between_comm congH_colH_betH)
        hence False 
          by (metis ‹BetH P I A› ‹CongH I P I Q› ‹Q = I ⟹ False› assms(12) 
              assms(7) betH_congH2__False congH_permlr)
      }
      ultimately have ?thesis 
        by (metis ‹A = I ⟶ Bet A B C ∨ Bet B C A ∨ Bet C A B› ‹BetH P I Q› 
            assms(1) assms(12) assms(2) assms(6) betH2_out congH_colH_betH)
    }
    ultimately have ?thesis 
      by blast
  }
  moreover
  {
    assume "same_side' B C P Q"
    {
      assume "ColH P B C"
      have "ColH C P B" 
        by (simp add: ‹ColH P B C› colH_permut_312)
      have "ColH B C Q" 
        by (metis colH_permut_312 ‹ColH C P B› assms(10) assms(13) assms(14) 
            assms(5) assms(8) congH_perm congH_perms cong_preserves_col_stronger)
      have "BetH P B Q" 
        using ColH_def ‹ColH B C Q› ‹ColH C P Q ⟹ False› ‹ColH P B C› 
          assms(5) colH_IncidL__IncidL by blast
      have "BetH P C Q" 
        using ‹BetH P B Q› ‹¬ ColH B P Q› between_col colH_permut_213 by blast
      {
        assume "BetH P B C"
        hence "BetH Q C B" 
          using ‹BetH P C Q› betH_trans0 between_comm by blast
        hence False 
          using ‹BetH P B Q› ‹¬ ColH B P Q› betH_expand colH_permut_213 by blast
      }
      moreover
      {
        assume "BetH P C B"
        hence "BetH B Q C" 
          using ‹BetH P B Q› ‹¬ ColH B P Q› betH_expand colH_permut_213 by blast
        hence False 
          using ‹BetH P C Q› ‹ColH C P Q ⟹ False› betH_expand colH_permut_213 by blast
      }
      ultimately have False 
        using ‹BetH P B Q› ‹BetH P C Q› assms(5) betH2_out by blast
    }
    hence "¬ ColH P B C"
      by blast
    {
      assume "ColH Q B C"
      hence "ColH B C P" 
        by (metis (full_types) ‹¬ ColH P B C› assms(10) assms(11) assms(13) 
            assms(14) assms(5) assms(8) assms(9) between_one colH_permut_213 congH_perms 
            congH_refl cong_preserves_col)
      hence False 
        using ‹¬ ColH P B C› colH_permut_312 by blast
    }
    hence "¬ ColH Q B C"
      by blast
    {
      assume "cut' P Q B C" 
      obtain lBC where "IsL lBC" and "IncidL B lBC" and "IncidL C lBC" 
        using assms(5) line_existence by blast
      {
        assume "¬ IncidL P lBC" and
          "¬ IncidL Q lBC" and
          "∃ I. IncidL I lBC ∧ BetH P I Q"
        then obtain I where "IncidL I lBC" and "BetH P I Q" 
          by blast
        have "ColH B I C" 
          using ColH_def ‹IncidL B lBC› ‹IncidL C lBC› ‹IncidL I lBC› ‹IsL lBC› by auto
        {
          assume "BetH B I C"
          obtain lPQ where "IncidL P lPQ" and "IncidL Q lPQ" and "¬ cut lPQ B C" 
            by (metis ‹same_side' B C P Q› line_existence same_side'_def same_side_not_cut)
          have "cut lPQ B C" 
          proof -
            have "¬ IncidL C lPQ" 
              using Hilbert_neutral_dimensionless_pre.ColH_def Is_line 
                ‹ColH C P Q ⟹ False› ‹IncidL P lPQ› ‹IncidL Q lPQ› by fastforce
            moreover have "IncidL I lPQ" 
              using ‹BetH P I Q› ‹IncidL P lPQ› ‹IncidL Q lPQ› assms(2) betH_line
                inter_incid_uniquenessH by blast
            ultimately show ?thesis 
              using ‹BetH B I C› Is_line ‹ColH B I C› betH_distincts 
                colH_IncidL__IncidL local.cut_def by blast
          qed
          hence "?thesis" 
            using ‹¬ local.cut lPQ B C› by blast
        }
        moreover {
          assume "BetH I C B"
          have "CongaH P C I Q C I"
          proof -
            have "¬ ColH B C P" 
              using ‹¬ ColH P B C› colH_permut_312 by blast
            moreover have "¬ ColH B C Q" 
              using ‹¬ ColH Q B C› colH_permut_312 by blast
            moreover have "CongaH B C P B C Q" 
              using ‹BetH P I Q› ‹ColH B I C› assms(13) assms(14) calculation(1)
                calculation(2) th17 by blast
            moreover have "BetH B C I" 
              by (simp add: ‹BetH I C B› between_comm)
            ultimately show ?thesis 
              using th14 by blast
          qed
          have "CongH I P I Q"
          proof -
            have "¬ ColH C P I" 
              by (metis IncidL_not_IncidL__not_colH ‹BetH P I Q› ‹IncidL C lBC›
                  ‹IncidL I lBC› ‹¬ ColH C P Q› ‹¬ IncidL P lBC› betH_colH colH_permut_132 colH_permut_213)
            moreover have "¬ ColH C Q I" 
              using ‹BetH I C B› ‹IncidL C lBC› ‹IncidL I lBC› ‹¬ IncidL Q lBC› 
                betH_distincts colH_IncidL__IncidL colH_permut_312 by blast
            moreover have "CongH C P C Q" 
              by (simp add: assms(14))
            moreover have "CongH C I C I" 
              by (metis ‹BetH I C B› betH_distincts congH_refl)
            ultimately show ?thesis
              using ‹CongaH P C I Q C I› 
              using congH_permlr ncolH_expand th12 by presburger
          qed
          have "A = I ⟶ ?thesis" 
            using Bet_def ‹BetH I C B› bet_comm by blast
          moreover {
            assume "A ≠ I"
            have "ColH I P Q" 
              by (simp add: ‹BetH P I Q› betH_colH colH_permut_213)
            {
              assume "BetH P A I"
              hence "BetH Q I A" 
                using ‹BetH P I Q› betH_trans0 between_comm by blast
              hence False 
                by (metis betH_expand ‹BetH P A I› ‹CongH I P I Q› assms(12) 
                    betH_congH2__False congH_perms)
            }
            moreover {
              assume "BetH P I A"
              hence "BetH Q A I" 
                by (metis assms(1) assms(12) assms(2) assms(6) assms(7) betH_trans0
                    between_comm congH_colH_betH)
              hence False 
                by (metis ‹BetH P I A› ‹CongH I P I Q› assms(12) betH_congH2__False
                    betH_distincts congH_permlr)
            }
            ultimately have ?thesis 
              by (metis ‹A = I ⟶ Bet A B C ∨ Bet B C A ∨ Bet C A B› ‹BetH P I Q› 
                  assms(1) assms(12) assms(2) assms(6) betH2_out congH_colH_betH)
          }
          ultimately have ?thesis 
            by blast
        }
        moreover {
          assume "BetH I B C"
          have "CongaH P B I Q B I"
          proof -
            have "¬ ColH C B P" 
              using ‹¬ ColH P B C› colH_permut_321 by blast
            moreover have "¬ ColH C B Q" 
              using ‹¬ ColH Q B C› colH_permut_321 by blast
            moreover have "CongaH C B P C B Q" 
              using colH_permut_321 ‹BetH P I Q› ‹ColH B I C› assms(13) 
                assms(14) calculation(1) calculation(2) th17 by blast
            moreover have "BetH C B I" 
              by (simp add: ‹BetH I B C› between_comm)
            ultimately show ?thesis 
              using th14 by blast
          qed
          have "CongH I P I Q"
          proof -
            have "¬ ColH B P I" 
              using ‹BetH I B C› ‹IncidL B lBC› ‹IncidL I lBC› ‹¬ IncidL P lBC› 
                betH_distincts colH_IncidL__IncidL colH_permut_312 by blast
            moreover have "¬ ColH B Q I" 
              using ‹BetH I B C› ‹IncidL B lBC› ‹IncidL I lBC› ‹¬ IncidL Q lBC› 
                betH_distincts colH_IncidL__IncidL colH_permut_312 by blast
            moreover have "CongH B P B Q" 
              using assms(13) by auto
            moreover have "CongH B I B I" 
              by (metis ‹BetH I B C› betH_distincts congH_refl)
            ultimately show ?thesis
              using ‹CongaH P B I Q B I› 
              by (metis ‹IncidL I lBC› ‹¬ IncidL Q lBC› congH_permlr th12)
          qed
          have "A = I ⟶ ?thesis" 
            using Bet_def ‹BetH I B C› by blast
          moreover
          {
            assume "A ≠ I"
            have "ColH I P Q" 
              using ‹BetH P I Q› betH_expand colH_permut_213 by blast
            {
              assume "BetH P A I"
              hence "BetH Q I A" 
                using ‹BetH P I Q› betH_trans0 between_comm by blast
              hence False 
                by (metis betH_expand ‹BetH P A I› ‹CongH I P I Q› assms(12) 
                    betH_congH2__False congH_permlr)
            }
            moreover
            {
              assume "BetH P I A"
              hence "BetH Q A I" 
                by (metis assms(1) assms(12) assms(2) assms(6) assms(7) 
                    betH_trans0 between_comm congH_colH_betH)
              hence False 
                by (metis betH_expand ‹BetH P I A› ‹CongH I P I Q› assms(12) 
                    betH_congH2__False congH_perms)
            }
            ultimately have ?thesis 
              by (metis ‹A = I ⟶ Bet A B C ∨ Bet B C A ∨ Bet C A B› 
                  ‹BetH P I Q› assms(1) assms(12) assms(2) assms(6) betH2_out congH_colH_betH)
          }
          ultimately have ?thesis 
            by blast
        }
        ultimately have ?thesis 
          by (metis ‹BetH P I Q› ‹ColH B I C› ‹ColH B P Q ⟹ False› 
              ‹ColH C P Q ⟹ False› assms(5) between_col between_one colH_permut_213)
      }
      hence ?thesis 
        using ‹IncidL B lBC› ‹IncidL C lBC› ‹IsL lBC› ‹cut' P Q B C› cut'_def 
          local.cut_def by auto
    }
    moreover
    {
      assume "same_side' P Q B C" 
      have "outH B P Q" 
      proof -
        have "¬ ColH P B C" 
          by (simp add: ‹¬ ColH P B C›)
        moreover have "¬ ColH C B P" 
          using calculation colH_permut_321 by blast
        moreover have "CongaH C B P C B P" 
          by (simp add: calculation(2) conga_refl)
        moreover have "CongaH C B P C B Q" 
          by (metis ‹¬ ColH Q B C› assms(13) assms(14) assms(5) calculation(2) 
              colH_permut_213 colH_permut_312 congH_refl th18_aux)
        moreover have "same_side' P P B C" 
          using calculation(2) colH_permut_213 same_side_prime_refl by blast
        ultimately show ?thesis 
          using ‹same_side' P Q B C› cong_4_uniqueness by blast
      qed
      hence ?thesis 
        using ‹¬ ColH B P Q› outH_expand by blast
    }
    ultimately have ?thesis 
      using ‹¬ ColH P B C› ‹¬ ColH Q B C› plane_separation_2D by blast
  }
  ultimately show ?thesis 
    using ‹¬ ColH B P Q› ‹¬ ColH C P Q› plane_separation_2D by blast
qed

lemma TS_upper_dim: 
  assumes "cut' A B P Q" and
    "P ≠ Q" and
    "A ≠ B" and
    "A ≠ C" and
    "B ≠ C" and
    "A ≠ P" and
    "A ≠ Q" and
    "B ≠ P" and
    "B ≠ Q" and
    "C ≠ P" and
    "C ≠ Q" and
    "CongH A P A Q" and
    "CongH B P B Q" and
    "CongH C P C Q"
  shows "Bet A B C ∨ Bet B C A ∨ Bet C A B" 
proof -
  obtain l where "IsL l" and "IncidL P l" and "IncidL Q l" 
    using assms(2) line_existence by blast
  have "cut l A B" 
    using ‹IncidL P l› ‹IncidL Q l› ‹IsL l› assms(1) cut'_def by auto
  have "ColH A P Q ⟶ ?thesis" 
    by (simp add: assms(10) assms(11) assms(12) assms(13) assms(14) assms(2) 
        assms(3) assms(4) assms(5) assms(6) assms(7) assms(8) assms(9) col_upper_dim)
  moreover
  {
    assume "¬ ColH A P Q"
    have "ColH B P Q ⟶ ?thesis" 
      by (metis assms(10) assms(11) assms(12) assms(13) assms(14) assms(2) 
          assms(3) assms(4) assms(5) assms(6) assms(7) assms(8) assms(9) col_upper_dim)
    moreover 
    {
      assume "¬ ColH B P Q"
      obtain I where "IncidL I l" and "BetH A I B" 
        using ‹local.cut l A B› local.cut_def by blast
      have "ColH P Q I" 
        using ColH_def Is_line ‹IncidL I l› ‹IncidL P l› ‹IncidL Q l› by blast
      {
        assume "P = I"
        hence "ColH A Q B" 
          by (metis ‹BetH A I B› assms(12) assms(13) assms(3) assms(9) congH_permlr 
              congH_refl cong_preserves_col)
        hence False 
          by (metis colH_permut_312 colH_trans colH_trivial121 ‹BetH A I B› 
              ‹P = I› ‹¬ ColH B P Q› assms(3) between_col)
      }
      hence "P ≠ I"
        by blast
      {
        assume "Q = I"
        hence "ColH A P B" 
          by (metis ‹BetH A I B› assms(12) assms(13) assms(3) assms(6) assms(8) 
              assms(9) congH_perms congH_refl congH_sym cong_preserves_col)
        have "ColH A P I" 
          by (metis ‹BetH A I B› ‹ColH A P B› assms(3) colH_trans ncolH_expand 
              outH_col outH_def)
        hence False 
          using ‹Q = I› ‹¬ ColH A P Q› by blast
      }
      hence "Q ≠ I"
        by blast
      have "CongaH I A P I A Q" 
      proof -
        have "CongaH B A P B A Q" 
        proof -
          have "¬ ColH A B P" 
            by (metis (full_types) ‹BetH A I B› ‹ColH P Q I› ‹P = I ⟹ False› 
                ‹¬ ColH A P Q› colH_permut_312 colH_trivial121 inter_uniquenessH 
                outH_def outH_expand)
          moreover have "¬ ColH A B Q" 
            by (meson assms(12) assms(13) assms(3) assms(6) assms(7) assms(8) 
                assms(9) calculation congH_refl congH_sym cong_preserves_col_stronger)
          moreover have "CongH A B A B" 
            using assms(3) congH_refl by blast
          moreover have "CongH A P A Q" 
            by (simp add: assms(12))
          moreover have "CongH B P B Q" 
            using assms(13) by auto
          ultimately show ?thesis
            using th18_aux by blast
        qed
        moreover have "outH A B I" 
          by (simp add: ‹BetH A I B› outH_def)
        moreover have "outH A P P" 
          by (simp add: assms(6) outH_def)
        moreover have "outH A B I" 
          by (simp add: calculation(2))
        moreover have "outH A Q Q" 
          by (simp add: assms(7) outH_def)
        ultimately show ?thesis 
          using conga_out_conga by fastforce
      qed
      have "CongH I P I Q"
      proof -
        have "¬ ColH A I P" 
          by (metis ‹ColH P Q I› ‹P ≠ I› ‹¬ ColH A P Q› colH_permut_231 
              colH_trans colH_trivial122)
        moreover have "¬ ColH A I Q" 
          using ColH_def ‹IncidL I l› ‹IncidL P l› ‹IncidL Q l› ‹Q = I ⟹ False›
            calculation inter_incid_uniquenessH by auto
        moreover have "CongH A I A I" 
          using ‹BetH A I B› betH_distincts congH_refl by presburger
        ultimately show ?thesis
          using ‹CongaH I A P I A Q› assms(12)
          using th12 by blast
      qed
      have "ColH A B C" 
      proof -
        have "C = I ⟶ ?thesis" 
          by (simp add: ‹BetH A I B› between_col colH_permut_132)
        moreover 
        {
          assume "C ≠ I"
          have "ColH A C I" 
            by (metis colH_permut_231 ‹BetH A I B› ‹C ≠ I› ‹ColH P Q I› 
                ‹CongH I P I Q› ‹P ≠ I› ‹Q ≠ I› assms(10) assms(11) assms(12) assms(14) 
                assms(2) assms(4) assms(6) assms(7) betH_to_bet bet_colH col_upper_dim)
          hence ?thesis 
            using ColH_def IncidL_not_IncidL__not_colH ‹BetH A I B› betH_colH by blast
        }
        ultimately show ?thesis 
          by blast
      qed
      have "BetH A B C ⟶ ?thesis" 
        by (simp add: ColH_bets ‹ColH A B C›)
      moreover have "BetH B C A ⟶ ?thesis" 
        using ColH_bets ‹ColH A B C› by blast
      moreover have "BetH B A C ⟶ ?thesis" 
        by (simp add: ColH_bets ‹ColH A B C›)
      ultimately have ?thesis 
        using ColH_bets ‹ColH A B C› by blast
    }
    ultimately have ?thesis 
      by blast
  }
  ultimately show ?thesis 
    by blast
qed

lemma cut'_comm: 
  assumes "cut' A B X Y" 
  shows  "cut' B A X Y" 
  by (metis assms cut'_def cut_comm)

lemma TS_upper_dim_bis:
  assumes "BetH P I Q" and
    "BetH I B A" and
    "P ≠ Q" and
    "A ≠ B" and
    "A ≠ C" and
    "B ≠ C" and
    "A ≠ P" and
    "A ≠ Q" and
    "B ≠ P" and
    "B ≠ Q" and
    "C ≠ P" and
    "C ≠ Q" and
    "CongH A P A Q" and
    "CongH B P B Q" and
    "CongH C P C Q"
  shows "Bet A B C ∨ Bet B C A ∨ Bet C A B" 
proof -
  have "ColH A P Q ⟶ ?thesis" 
    by (simp add: assms(10) assms(11) assms(12) assms(13) assms(14) assms(15) 
        assms(3) assms(4) assms(5) assms(6) assms(7) assms(8) assms(9) col_upper_dim)
  moreover
  {
    assume "¬ ColH A P Q"
    have "ColH B P Q ⟶ ?thesis" 
      by (metis assms(10) assms(11) assms(12) assms(13) assms(14) assms(15) 
          assms(3) assms(4) assms(5) assms(6) assms(7) assms(8) assms(9) col_upper_dim)
    moreover
    {
      assume "¬ ColH B P Q"
      have "CongaH P B I Q B I"
      proof -
        have "P ≠ I" 
          using assms(1) betH_expand by blast
        have "Q ≠ I" 
          using assms(1) betH_colH by blast
        {
          assume "ColH A B P"
          have "¬ ColH P Q A" 
            using ‹¬ ColH A P Q› colH_permut_312 by blast
          moreover have "ColH P Q P" 
            by (simp add: colH_trivial121)
          moreover have "ColH P Q I" 
            by (simp add: assms(1) betH_colH colH_permut_132)
          moreover have "ColH A B I" 
            by (simp add: assms(2) betH_colH between_comm)
          ultimately
          have "P = I" 
            using assms(4) ‹ColH A B P› inter_uniquenessH by blast
          hence False 
            by (simp add: ‹P ≠ I›)
        }
        hence "¬ ColH A B P" 
          by blast
        moreover 
        {
          assume "ColH A B Q"
          have "¬ ColH Q P A" 
            using ‹¬ ColH A P Q› colH_permut_321 by blast
          moreover have "ColH Q P Q" 
            by (simp add: colH_trivial121)
          moreover have "ColH Q P I" 
            using assms(1) betH_colH colH_permut_312 by blast
          moreover have "ColH A B I" 
            using assms(2) between_col colH_permut_321 by blast
          ultimately
          have "Q = I" 
            using assms(4) ‹ColH A B Q› inter_uniquenessH by blast
          hence False 
            by (simp add: ‹Q ≠ I›)
        }
        hence "¬ ColH A B Q" 
          by blast
        moreover have "CongaH A B P A B Q" 
        proof -
          have "¬ ColH B A P" 
            using calculation(1) colH_permut_213 by blast
          moreover have "¬ ColH B A Q" 
            using ‹¬ ColH A B Q› colH_permut_213 by blast
          moreover have "CongH B A B A" 
            using assms(4) congH_refl by auto
          ultimately show ?thesis 
            using assms(13) assms(14) th18_aux by presburger
        qed
        ultimately show ?thesis 
          by (simp add: assms(2) between_comm th14)
      qed
      have "CongH I P I Q" 
        by (metis assms(1) assms(10) assms(13) assms(14) assms(2) assms(7) 
            assms(8) assms(9) axiom_five_segmentsH between_comm between_only_one congH_refl)
      have "ColH A B C" 
      proof -
        have "ColH A B I" 
          by (simp add: assms(2) between_col colH_permut_321)
        have "C = I ⟶ ?thesis" 
          using ‹ColH A B I› by blast
        moreover
        {
          assume "C ≠ I"
          have "ColH I B A" 
            by (simp add: assms(2) betH_colH)
          hence "ColH A C I" 
            by (metis (mono_tags, lifting) betH_to_bet bet_colH colH_permut_213 
                colH_permut_312 ‹C ≠ I› ‹CongH I P I Q› assms(1) assms(11) assms(12) 
                assms(13) assms(15) assms(2) assms(5) assms(7) assms(8) col_upper_dim)
          have "ColH P I Q" 
            by (simp add: assms(1) betH_colH)
          hence ?thesis 
            by (metis betH_distincts colH_permut_312 colH_trans colH_trivial121 
                ‹ColH A C I› ‹ColH I B A› assms(2))
        }
        ultimately show ?thesis
          by blast
      qed
      have "BetH B A C ⟶ ?thesis" 
        using ColH_bets ‹ColH A B C› by blast
      hence ?thesis 
        using ColH_bets ‹ColH A B C› by blast
    }
    ultimately have ?thesis
      by blast
  }
  ultimately show ?thesis by blast
qed

lemma upper_dim:
  assumes "P ≠ Q" and
    "A ≠ B" and
    "A ≠ C" and
    "B ≠ C" and
    "Cong A P A Q" and
    "Cong B P B Q" and
    "Cong C P C Q"
  shows "Bet A B C ∨ Bet B C A ∨ Bet C A B" 
proof -
  have "C = P ∧ C = Q ⟶ ?thesis" 
    using assms(1) by blast
  have "B = P ∧ B = Q ⟶ ?thesis" 
    using assms(1) by blast
  have "A = P ∧ A = Q ⟶ ?thesis" 
    using assms(1) by blast
  have "CongH A P A Q" 
    using Cong_def assms(1) assms(5) by auto
  have "CongH B P B Q" 
    using Cong_def assms(1) assms(6) by blast
  have "CongH C P C Q" 
    using Cong_def assms(1) assms(7) by blast
  have "A ≠ P" 
    using Cong_def assms(1) assms(5) by presburger
  have "A ≠ Q" 
    using Cong_def assms(1) assms(5) by presburger
  have "B ≠ P" 
    using Cong_def assms(1) assms(6) by force
  have "B ≠ Q" 
    using Cong_def assms(1) assms(6) by presburger
  have "C ≠ P" 
    using Cong_def assms(1) assms(7) by presburger
  have "C ≠ Q" 
    using Cong_def assms(1) assms(7) by presburger
  have "ColH A P Q ⟶ ?thesis" 
    by (simp add: ‹A ≠ P› ‹A ≠ Q› ‹B ≠ P› ‹B ≠ Q› ‹C ≠ P› ‹C ≠ Q› 
        ‹CongH A P A Q› ‹CongH B P B Q› ‹CongH C P C Q› assms(1) assms(2) assms(3) 
        assms(4) col_upper_dim)
  moreover
  {
    assume "¬ ColH A P Q"
    have "ColH B P Q ⟶ ?thesis" 
      by (metis ‹A ≠ P› ‹A ≠ Q› ‹B ≠ P› ‹B ≠ Q› ‹C ≠ P› ‹C ≠ Q› 
          ‹CongH A P A Q› ‹CongH B P B Q› ‹CongH C P C Q› assms(1) assms(2) assms(3) 
          assms(4) col_upper_dim)
    moreover
    {
      assume "¬ ColH B P Q"
      have "ColH C P Q ⟶ ?thesis" 
        by (metis ‹A ≠ P› ‹A ≠ Q› ‹B ≠ P› ‹B ≠ Q› ‹C ≠ P› ‹C ≠ Q› 
            ‹CongH A P A Q› ‹CongH B P B Q› ‹CongH C P C Q› assms(1) assms(2) 
            assms(3) assms(4) col_upper_dim)
      moreover
      {
        assume "¬ ColH C P Q"
        have "cut' A B P Q ⟶ ?thesis" 
          by (simp add: TS_upper_dim ‹A ≠ P› ‹A ≠ Q› ‹B ≠ P› ‹B ≠ Q› ‹C ≠ P› 
              ‹C ≠ Q› ‹CongH A P A Q› ‹CongH B P B Q› ‹CongH C P C Q› assms(1) 
              assms(2) assms(3) assms(4))
        moreover
        {
          assume "same_side' A B P Q"
          have "cut' A C P Q ⟶ ?thesis" 
            using TS_upper_dim ‹A ≠ P› ‹A ≠ Q› ‹B ≠ P› ‹B ≠ Q› ‹C ≠ P› ‹C ≠ Q› 
              ‹CongH A P A Q› ‹CongH B P B Q› ‹CongH C P C Q› assms(1) assms(2) assms(3) 
              assms(4) bet_comm by blast
          moreover
          {
            assume "same_side' A C P Q"
            {
              assume "ColH P A B" 
              hence "ColH B P A" 
                by (simp add: colH_permut_312)
              have "ColH A B Q" 
                by (meson ‹A ≠ P› ‹B ≠ P› ‹ColH B P A› ‹CongH A P A Q› ‹CongH B P B Q› 
                    assms(2) colH_permut_312 congH_refl cong_preserves_col_stronger)
              hence False
                by (metis ‹ColH B P A› ‹¬ ColH A P Q› assms(2) colH_trans ncolH_distincts)
            }
            hence "¬ ColH P A B" 
              by blast
            {
              assume "ColH Q A B"
              hence "ColH A B P" 
                by (meson ‹A ≠ P› ‹A ≠ Q› ‹B ≠ P› ‹B ≠ Q› ‹CongH A P A Q› 
                    ‹CongH B P B Q› assms(2) colH_permut_231 congH_refl congH_sym 
                    cong_preserves_col_stronger)            
              hence False 
                using ‹¬ ColH P A B› colH_permut_312 by blast
            }
            hence "¬ ColH Q A B" 
              by blast
            {
              assume "same_side' P Q A B"
              have "outH A P Q" 
              proof -
                have "¬ ColH P A B" 
                  by (simp add: ‹¬ ColH P A B›)
                moreover have "¬ ColH B A P" 
                  using calculation colH_permut_321 by blast
                moreover have "CongaH B A P B A P" 
                  using calculation(2) conga_refl by blast
                moreover have "CongaH B A P B A Q" 
                  by (metis ‹CongH A P A Q› ‹CongH B P B Q› ‹¬ ColH Q A B› assms(2) 
                      calculation(2) colH_permut_213 colH_permut_312 congH_refl th18_aux)
                moreover have "same_side' P P A B" 
                  using calculation(1) colH_permut_312 same_side_prime_refl by blast
                ultimately show ?thesis 
                  using ‹same_side' P Q A B› 
                  using cong_4_uniqueness by blast
              qed
              hence ?thesis 
                using ‹¬ ColH A P Q› outH_expand by blast
            }
            moreover
            {
              assume "cut' P Q A B"
              obtain lAB where "IsL lAB" and "IncidL A lAB" and "IncidL B lAB" 
                using assms(2) line_existence by blast
              then obtain I where "IncidL I lAB" and "BetH P I Q"  
                using ‹cut' P Q A B› cut'_def local.cut_def by auto
              hence "ColH A I B" 
                using ColH_def ‹IncidL A lAB› ‹IncidL B lAB› ‹IsL lAB› by auto
              {
                assume "BetH A I B"
                obtain lPQ where "IsL lPQ" and "IncidL P lPQ" and "IncidL Q lPQ" 
                  using assms(1) line_existence by blast
                hence "¬ cut lPQ A B" 
                  using ‹same_side' A B P Q› same_side'_def same_side_not_cut by auto
                have "cut lPQ A B" 
                proof -
                  have "¬ IncidL B lPQ" 
                    using Hilbert_neutral_dimensionless_pre.ColH_def ‹IncidL P lPQ› 
                      ‹IncidL Q lPQ› ‹IsL lPQ› ‹¬ ColH B P Q› by fastforce
                  moreover have "IncidL I lPQ" 
                    using ‹BetH P I Q› ‹IncidL P lPQ› ‹IncidL Q lPQ› assms(1) 
                      betH_line inter_incid_uniquenessH by blast
                  ultimately show ?thesis 
                    using ‹BetH A I B› 
                    using Is_line ‹ColH A I B› betH_distincts colH_IncidL__IncidL 
                      local.cut_def by blast
                qed
                hence False 
                  using ‹¬ local.cut lPQ A B› by blast
                hence ?thesis 
                  by blast
              }
              moreover have "BetH I B A ⟶ ?thesis" 
                using TS_upper_dim_bis ‹A ≠ P› ‹A ≠ Q› ‹B ≠ P› ‹B ≠ Q› ‹BetH P I Q› 
                  ‹C ≠ P› ‹C ≠ Q› ‹CongH A P A Q› ‹CongH B P B Q› ‹CongH C P C Q› 
                  assms(1) assms(2) assms(3) assms(4) by blast
              moreover have "BetH I A B ⟶ ?thesis" 
                using TS_upper_dim_bis ‹A ≠ P› ‹A ≠ Q› ‹B ≠ P› ‹B ≠ Q› ‹BetH P I Q› 
                  ‹C ≠ P› ‹C ≠ Q› ‹CongH A P A Q› ‹CongH B P B Q› ‹CongH C P C Q› 
                  assms(1) assms(2) assms(3) assms(4) bet_comm by blast
              ultimately have ?thesis 
                by (metis ‹BetH P I Q› ‹ColH A I B› ‹¬ ColH A P Q› ‹¬ ColH B P Q› 
                    assms(2) betH_colH between_one colH_permut_213)
            }
            ultimately have ?thesis 
              using ‹¬ ColH P A B› ‹¬ ColH Q A B› plane_separation_2D by blast
          }
          ultimately have ?thesis 
            using ‹¬ ColH A P Q› ‹¬ ColH C P Q›
              ‹cut' A C P Q ⟶ Bet A B C ∨ Bet B C A ∨ Bet C A B› 
              ‹same_side' A C P Q ⟹ Bet A B C ∨ Bet B C A ∨ Bet C A B› 
              plane_separation_2D by blast
        }
        ultimately have ?thesis 
          using ‹¬ ColH A P Q› ‹¬ ColH B P Q› plane_separation_2D by blast
      }
      ultimately have ?thesis 
        by blast
    }
    ultimately have ?thesis
      by blast
  }
  ultimately show ?thesis 
    by blast
qed

interpretation H2D_to_T2D : Tarski_neutral_2D
  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: 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. 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)" 
  proof -
    {
      fix a b c p q
      assume "Bet a p c" and "Bet b q c" and
        "Bet a b c ∨ Bet b c a ∨ Bet c a b" 
      hence "∃x. Bet p x b ∧ Bet q x a" 
        using Bet_def bet_comm bet_trans by metis
    }
    moreover
    {
      fix a b c p q
      assume "Bet a p c" and "Bet b q c" and
        "¬ (Bet a b c ∨ Bet b c a ∨ Bet c a b)" and
        "a = p ∨ p = c ∨ b = q ∨ q = c" 
      hence "∃x. Bet p x b ∧ Bet q x a" 
        by (metis Hilbert_neutral_dimensionless_pre.Bet_def bet_comm)
    }
    moreover
    {
      fix a b c p q
      assume "Bet a p c" and "Bet b q c" and
        "¬ (Bet a b c ∨ Bet b c a ∨ Bet c a b)" and
        "a ≠ p" and "p ≠ c" and "b ≠ q" and "q ≠ c" 
      hence "∃x. Bet p x b ∧ Bet q x a" 
        using pasch_general_case by blast
    }
    ultimately show ?thesis
      by blast
  qed
  show "¬ Bet PP PQ PR ∧ ¬ Bet PQ PR PP ∧ ¬ Bet PR PP PQ" 
    using lower_dim_l by blast
  show "∀a b c p q.
       p ≠ q ∧ Cong a p a q ∧ Cong b p b q ∧ Cong c p c q ⟶
       Bet a b c ∨ Bet b c a ∨ Bet c a b" 
    by (metis Bet_def upper_dim)
qed

end
end