Theory Tarski_Neutral_Hilbert

(* IsageoCoq - Tarski_Neutral_Hilbert.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_Hilbert

imports 
  Tarski_Neutral 
  Hilbert_Neutral

begin

section "Tarski neutral dimensionless - Hilbert"

context Tarski_neutral_dimensionless

begin

subsection "Definition"

definition isLine:: "'p×'p⇒bool" where
  "isLine l ≡ (fst l ≠ snd l)"

definition Line :: "'p ⇒'p ⇒'p×'p" where
  "Line A B = (if A ≠ B then (Pair A B) else undefined)"

definition IncidentL ::"'p⇒'p×'p⇒bool" where
  "IncidentL A l ≡ isLine l ∧ Col A (fst l) (snd l)"

definition EqTL:: "'p×'p⇒'p×'p⇒bool" 
  ("_ =l= _" [99,99] 50) where
  "l1 =l= l2 ≡ isLine l1 ∧ isLine l2 ∧ (∀ X. (IncidentL X l1 ⟷ IncidentL X l2))"

definition  Col_H:: "'p⇒'p⇒'p⇒bool" where
  "Col_H A B C ≡ ∃ l. (isLine l ∧ IncidentL A l ∧ IncidentL B l ∧ IncidentL C l)"

definition isPlane :: "'p×'p×'p⇒bool" where
  "isPlane pl ≡ (∀ P Q R::'p. pl = (P,Q,R) ⟶ ¬ Col P Q R)"

definition Plane :: "'p⇒'p⇒'p⇒'p×'p×'p" where
  "Plane A B C = (A,B,C)"

definition IncidentP ::"'p⇒'p×'p×'p⇒bool" 
  where
    "IncidentP A pl ≡ (isPlane pl) ∧ (∃ P Q R. pl = Plane P Q R ∧ Coplanar A P Q R)"

definition EqTP:: "'p×'p×'p⇒'p×'p×'p⇒bool" ("_ =p= _" [99,99] 50) where
  "p1 =p= p2  ≡ isPlane p1 ∧ isPlane p2 ∧ (∀ X. (IncidentP X p1 ⟷ IncidentP X p2))"

definition IncidentLP ::"'p×'p⇒'p×'p×'p⇒bool" where
  "IncidentLP l p ≡ isLine l ∧ isPlane p ∧ (∀ A. IncidentL A l ⟶ IncidentP A p)"

definition Between_H :: "'p⇒'p⇒'p⇒bool" where
  "Between_H A B C ≡ Bet A B C ∧ A ≠ B ∧ B ≠ C ∧ A ≠ C"

definition cut_H :: "'p×'p⇒'p⇒'p⇒bool" where
  "cut_H l A B ≡  isLine l ∧ ¬ IncidentL A l ∧ ¬ IncidentL B l ∧ 
                  (∃ I. IncidentL I l ∧ Between_H A I B)"

definition outH :: "'p⇒'p⇒'p⇒bool" where
  "outH P A B ≡ Between_H P A B ∨ Between_H P B A ∨ (P ≠ A ∧ A = B)"

definition same_side_scott :: "'p⇒'p⇒'p⇒bool" 
  where "same_side_scott E A B ≡ E ≠ A ∧ E ≠ B ∧ Col_H E A B ∧ ¬ Between_H A E B"

definition disjoint_H :: "'p⇒'p⇒'p⇒'p⇒bool" 
  where "disjoint_H A B C D ≡ ¬ (∃ P. Between_H A P B ∧ Between_H C P D)"

definition same_side_H :: "'p⇒'p⇒'p×'p⇒bool" 
  where "same_side_H A B l ≡ isLine l ∧ (∃ P. cut_H l A P ∧ cut_H l B P)"

definition same_side'_H :: "'p⇒'p⇒'p⇒'p⇒bool" 
  where
    "same_side'_H A B X Y ≡ X ≠ Y ∧ (∀ l. isLine l ∧ (IncidentL X l ∧ IncidentL Y l) 
                                         ⟶ same_side_H A B l)"

definition CongA_H :: "'p⇒'p⇒'p⇒'p⇒'p⇒'p⇒bool" where
  "CongA_H A B C D E F ≡ A B C CongA D E F"

definition Para_H :: "'p×'p ⇒ 'p×'p ⇒bool" where
  "Para_H l m ≡ isLine l ∧ isLine m ∧ (¬(∃ X. IncidentL X l ∧ IncidentL X m)) ∧ 
                                       (∃ p. IncidentLP l p ∧ IncidentLP m p)"

subsection "Propositions"

lemma EqL__diff_left:
  assumes "l1 =l= l1" 
  shows "fst l1 ≠ snd l1" 
  using EqTL_def assms isLine_def by blast

lemma EqL__diff_right:
  assumes "l1 =l= l2" 
  shows "(fst l2) ≠ (snd l2)" 
  using EqTL_def assms isLine_def by blast

lemma axiom_line_existence:
  assumes "A ≠ B"
  shows "∃ l. isLine l ∧ IncidentL A l ∧ IncidentL B l" 
proof -
  let ?l = "Pair A B"
  have "isLine ?l" 
    by (simp add: assms isLine_def)
  moreover have "IncidentL A ?l" 
    by (simp add: IncidentL_def ‹isLine (A, B)› col_trivial_1)
  moreover have "IncidentL B ?l" 
    by (simp add: IncidentL_def ‹isLine (A, B)› col_trivial_3)
  ultimately show ?thesis 
    by blast
qed

lemma incident_eq: 
  assumes "A ≠ B" and
    "IncidentL A l" and 
    "IncidentL B l"
  shows "Line A B =l= l" 
proof -
  have "Col A (fst l) (snd l)" 
    using IncidentL_def assms(2) by presburger
  have "Col B (fst l) (snd l)" 
    using IncidentL_def assms(3) by blast

  have "isLine (Line A B)" 
    by (simp add: Line_def assms(1) isLine_def)
  moreover have "isLine l" 
    using IncidentL_def assms(2) by blast
  {
    fix X
    assume "IncidentL X (Line A B)"
    hence "Col X A B" 
      by (simp add: IncidentL_def Line_def assms(1))
    have "Col X (fst l) (snd l)" 
      by (meson ‹Col A (fst l) (snd l)› ‹Col B (fst l) (snd l)› ‹Col X A B› 
          assms(1) col_permutation_1 colx)
    hence "IncidentL X l" 
      by (simp add: IncidentL_def ‹isLine l›)
  }
  moreover
  {
    fix X 
    assume "IncidentL X l" 
    have "Col X A B" 
      by (metis (no_types, lifting) IncidentL_def ‹Col A (fst l) (snd l)› 
          ‹Col B (fst l) (snd l)› ‹IncidentL X l› col_permutation_5 isLine_def l6_16_1)
    have "IncidentL X (Line A B)" 
      using IncidentL_def Line_def ‹Col X A B› assms(1) calculation(1) by auto
  }
  ultimately show ?thesis 
    using EqTL_def ‹isLine l› by blast
qed

lemma eq_transitivity: 
  assumes "l =l= m" and 
    "m =l= n"
  shows "l =l= n" 
  using EqTL_def assms(1) assms(2) by presburger

lemma eq_reflexivity: 
  assumes "isLine l"
  shows "l =l= l" 
  using EqTL_def assms by auto

lemma eq_symmetry:
  assumes "l =l= m"
  shows "m =l= l" 
  using EqTL_def assms by blast

(** The equality is compatible with IncidentL *)

lemma eq_incident: 
  assumes "l =l= m" 
  shows "IncidentL A l ⟷ IncidentL A m" 
  using EqTL_def assms by blast

lemma axiom_Incidl_morphism:
  assumes "IncidentL P l" and
    "l =l= m"
  shows "IncidentL P m" 
  using assms(1) assms(2) eq_incident by blast

(** There is only one line going through two points. *)

lemma axiom_line_uniqueness:
  assumes "A ≠ B" and
    "IncidentL A l" and "IncidentL B l" and
    "IncidentL A m" and "IncidentL B m" 
  shows "l =l= m" 
proof -
  have "Line A B =l= l" 
    by (simp add: assms(1) assms(2) assms(3) incident_eq)
  moreover have "Line A B =l= m" 
    by (simp add: assms(1) assms(4) assms(5) incident_eq)
  ultimately show ?thesis 
    using eq_symmetry eq_transitivity by blast
qed
  (** Every line contains at least two points. *)

lemma axiom_two_points_on_line: 
  assumes "isLine l"
  shows "∃ A B. IncidentL B l ∧ IncidentL A l ∧ A ≠ B" 
proof -
  let ?A = "fst l"
  let ?B = "snd l"
  have "IncidentL ?B l" 
    by (simp add: IncidentL_def assms col_trivial_3)
  moreover have "IncidentL ?A l" 
    by (simp add: IncidentL_def assms col_trivial_1)
  moreover have "?A ≠ ?B" 
    using assms isLine_def by blast
  ultimately show ?thesis 
    by blast
qed

(** We show that the notion of collinearity we just defined is equivalent to the
 notion of collinearity of Tarski. *)

lemma cols_coincide_1: 
  assumes "Col_H A B C"
  shows "Col A B C"  
proof -
  obtain l where "IncidentL A l" and "IncidentL B l" and "IncidentL C l"
    using Col_H_def assms by blast
  have "(fst l) ≠ (snd l)" 
    using IncidentL_def ‹IncidentL B l› isLine_def by blast
  have "Col A (fst l) (snd l)" 
    using IncidentL_def ‹IncidentL A l› by auto
  moreover have "Col B (fst l) (snd l)" 
    using IncidentL_def ‹IncidentL B l› by auto
  moreover have "Col C (fst l) (snd l)" 
    using IncidentL_def ‹IncidentL C l› by auto
  ultimately show ?thesis 
    by (metis ‹fst l ≠ snd l› col2__eq col_permutation_4 col_transitivity_1)
qed

lemma cols_coincide_2: 
  assumes "Col A B C"
  shows "Col_H A B C" 
proof (cases "A = B")
  case True
  thus ?thesis 
    by (metis Col_H_def axiom_line_existence diff_col_ex)
next
  case False
  let ?l = "Line A B"
  have "isLine ?l" 
    by (simp add: False Line_def isLine_def)
  moreover have "IncidentL A ?l" 
    using False IncidentL_def Line_def calculation col_trivial_1 by auto
  moreover have "IncidentL B ?l" 
    using False IncidentL_def Line_def calculation(1) col_trivial_3 by auto
  moreover have "IncidentL C ?l" 
    by (metis Col_perm False IncidentL_def Line_def assms calculation(1) 
        fst_def prod.simps(2) snd_def)
  ultimately show ?thesis 
    using Col_H_def by blast
qed

lemma cols_coincide: 
  shows "Col A B C ⟷ Col_H A B C" 
  using cols_coincide_1 cols_coincide_2 by blast

lemma ncols_coincide: 
  shows "¬ Col A B C ⟷ ¬ Col_H A B C" 
  by (simp add: cols_coincide)

lemma lower_dim':
  shows "∃ PA PB PC. PA ≠ PB ∧ PB ≠ PC ∧
 PA ≠ PC ∧ ¬ Col_H PA PB PC" 
  by (metis col_trivial_2 col_trivial_3 cols_coincide_1 not_col_exists 
      point_construction_different)

lemma axiom_plane_existence:
  assumes "¬ Col_H A B C"
  shows "∃ p. IncidentP A p ∧ IncidentP B p ∧ IncidentP C p" 
proof -
  let ?p = "Plane A B C"
  have "isPlane ?p" 
    by (simp add: Plane_def assms isPlane_def ncols_coincide)
  have "IncidentP A ?p" 
    using IncidentP_def ‹isPlane (Plane A B C)› ncop_distincts by blast
  moreover have "IncidentP B ?p" 
    using IncidentP_def ‹isPlane (Plane A B C)› ncop_distincts by blast
  moreover have "IncidentP C ?p" 
    using IncidentP_def ‹isPlane (Plane A B C)› ncop_distincts by blast
  ultimately show ?thesis 
    by blast
qed

lemma incidentp_eqp:
  assumes "¬ Col_H A B C"  and
    "IncidentP A p" and 
    "IncidentP B p" and
    "IncidentP C p" 
  shows "(Plane A B C) =p= p" 
proof -
  have "isPlane (Plane A B C)" 
    using Plane_def Tarski_neutral_dimensionless.cols_coincide_2 
      Tarski_neutral_dimensionless_axioms assms(1) isPlane_def by fastforce
  have "isPlane p" 
    using IncidentP_def assms(3) by blast
  obtain PA QA RA where "p = Plane PA QA RA" and 
    "Coplanar A PA QA RA" 
    using assms(2) IncidentP_def by blast
  hence "p = (PA,QA,RA)" 
    by (simp add: Plane_def)
  hence "Coplanar B PA QA RA" 
    using IncidentP_def Plane_def assms(3) by auto
  have "Coplanar C PA QA RA" 
    using IncidentP_def Plane_def assms(4) by (simp add: ‹p = (PA, QA, RA)›)
  have "¬ Col PA QA RA" 
    using Plane_def ‹isPlane p› ‹p = (PA, QA, RA)› isPlane_def by blast
  have "¬ Col A B C" 
    using Plane_def by (simp add: assms(1) ncols_coincide)
  {   
    fix X
    assume "IncidentP X (Plane A B C)"
    hence "isPlane (Plane A B C)" 
      by (simp add: ‹isPlane (Plane A B C)›)
    obtain  P Q R where "(Plane A B C) = Plane P Q R" and "Coplanar X P Q R" 
      using IncidentP_def ‹IncidentP X (Plane A B C)› by blast
    hence "A = P ∧ B = Q ∧ C = R" 
      using Plane_def by simp
    hence "Coplanar X A B C" 
      using ‹Coplanar X P Q R› by auto
    moreover
    have "Coplanar PA A B C" 
      by (meson ‹Coplanar A PA QA RA› ‹Coplanar B PA QA RA› ‹Coplanar C PA QA RA› 
          ‹¬ Col PA QA RA› coplanar_perm_9 coplanar_pseudo_trans ncop_distincts)
    moreover have "Coplanar QA A B C" 
      by (meson ‹Coplanar A PA QA RA› ‹Coplanar B PA QA RA› ‹Coplanar C PA QA RA› 
          ‹¬ Col PA QA RA› coplanar_perm_9 coplanar_pseudo_trans ncop_distincts)
    moreover have "Coplanar RA A B C" 
      by (meson ‹Coplanar A PA QA RA› ‹Coplanar B PA QA RA› ‹Coplanar C PA QA RA› 
          ‹¬ Col PA QA RA› coplanar_perm_9 coplanar_pseudo_trans ncop_distincts)
    ultimately
    have "Coplanar X PA QA RA" 
      by (meson ‹¬ Col A B C› coplanar_perm_9 coplanar_pseudo_trans)
    hence "∃ P Q R. p = Plane P Q R ∧ Coplanar X P Q R" 
      using ‹p = Plane PA QA RA› by blast
  } 
  moreover
  {
    fix X
    assume "IncidentP X p"
    hence "isPlane p" 
      by (simp add: ‹isPlane p›)
    obtain P Q R where "p = Plane P Q R" and
      "Coplanar X P Q R" 
      using IncidentP_def ‹IncidentP X p› by blast
    have "P = PA ∧ Q = QA ∧ R = RA" 
      using Plane_def ‹p = (PA, QA, RA)› ‹p = Plane P Q R› by auto
    hence "Coplanar X PA QA RA" 
      using ‹Coplanar X P Q R› by auto
    hence "Coplanar X A B C" 
      by (meson ‹Coplanar A PA QA RA› ‹Coplanar B PA QA RA› ‹Coplanar C PA QA RA› 
          ‹¬ Col PA QA RA› coplanar_perm_9 coplanar_pseudo_trans)
    hence "IncidentP X (Plane A B C)" 
      using IncidentP_def ‹isPlane (Plane A B C)› by blast
  }
  ultimately show ?thesis 
    by (metis EqTP_def IncidentP_def ‹isPlane (Plane A B C)› ‹isPlane p›)
qed

(** Our equality is an equivalence relation. *)

lemma eqp_transitivity: 
  assumes "p =p= q" and 
    "q =p= r"
  shows "p =p= r" 
  using EqTP_def assms(1) assms(2) by presburger

lemma eqp_reflexivity: 
  assumes "isPlane p"
  shows "p =p= p" 
  by (simp add: EqTP_def assms)

lemma eqp_symmetry: 
  assumes "p =p= q"
  shows "q =p= p" 
  using EqTP_def assms by presburger

(** The equality is compatible with IncidentL *)

lemma eqp_incidentp: 
  assumes "p =p= q"
  shows "IncidentP A p ⟷ IncidentP A q" 
  using EqTP_def assms by blast

lemma axiom_Incidp_morphism :
  assumes "IncidentP M p" and
    "EqTP p q"
  shows "IncidentP M q" 
  using assms(1) assms(2) eqp_incidentp by blast

(** There is only one plane going through three non collinear points. *)

lemma axiom_plane_uniqueness: 
  assumes "¬ Col_H A B C" and
    "IncidentP A p" and
    "IncidentP B p" and
    "IncidentP C p" and
    "IncidentP A q" and
    "IncidentP B q" and
    "IncidentP C q" 
  shows "p =p= q" 
proof -
  have "Plane A B C =p= p"   
    using assms(1) assms(2) assms(3) assms(4) incidentp_eqp by auto
  moreover have "Plane A B C =p= q"   
    using assms(1) assms(5) assms(6) assms(7) incidentp_eqp by auto
  ultimately show ?thesis
    using eqp_symmetry eqp_transitivity by blast
qed

(** Every plane contains at least one point. *)

lemma axiom_one_point_on_plane:
  assumes "isPlane p"
  shows "∃ A. IncidentP A p" 
proof -
  obtain A B C where "p = Plane A B C" 
    by (metis Plane_def surj_pair)
  thus ?thesis 
    using IncidentP_def assms coplanar_trivial by blast
qed

lemma axiom_line_on_plane:
  assumes "A ≠ B" and
    "IncidentL A l" and 
    "IncidentL B l" and 
    "IncidentP A p" and
    "IncidentP B p"
  shows "IncidentLP l p" 
proof -
  have "isLine l ∧ Col A (fst l) (snd l)" 
    using IncidentL_def assms(2) by blast
  let ?U = "(fst l)"
  let ?V = "(snd l)"
  have "l = Line ?U ?V" 
    by (metis IncidentL_def Line_def assms(2) isLine_def prod.exhaust_sel)
  hence "Col A ?U ?V" 
    by (metis IncidentL_def assms(2))
  have "Col B ?U ?V" 
    by (metis IncidentL_def assms(3))
  have "isLine l" 
    using IncidentL_def assms(3) by blast
  hence "fst l ≠ snd l" 
    by (simp add: isLine_def)
  hence "?U ≠ ?V"
    by blast
  have "Col A B ?U" 
    using ‹Col A (fst l) (snd l)› ‹Col B (fst l) (snd l)› ‹fst l ≠ snd l› 
      col2__eq col_permutation_5 by blast
  have "Col A B ?V" 
    by (metis Col_cases ‹Col A B (fst l)› ‹Col A (fst l) (snd l)› 
        ‹Col B (fst l) (snd l)› col_transitivity_1)
  obtain PA QA RA where "p = Plane PA QA RA" and "Coplanar A PA QA RA" 
    using IncidentP_def assms(4) by blast
  hence "¬ Col PA QA RA" 
    using IncidentP_def Plane_def assms(4) isPlane_def by blast
  obtain PB QB RB where "p = Plane PB QB RB" and "Coplanar B PB QB RB" 
    using IncidentP_def assms(5) by blast
  hence "¬ Col PB QB RB" 
    using IncidentP_def Plane_def assms(5) isPlane_def by auto
  have "Coplanar B PA QA RA" 
    using Plane_def ‹Coplanar B PB QB RB› ‹p = Plane PA QA RA› ‹p = Plane PB QB RB› by force
  have "Coplanar ?U PA QA RA" 
    using ‹Coplanar A PA QA RA› ‹Coplanar B PA QA RA› 
      ncoplanar_perm_23 ‹Col A B (fst l)› assms(1) col_cop2__cop by blast
  have "Coplanar ?V PA QA RA" 
    by (meson ncoplanar_perm_23 ‹Col A B (snd l)› ‹Coplanar A PA QA RA› 
        ‹Coplanar B PA QA RA› assms(1) col_cop2__cop)
  have "isLine l" 
    using IncidentL_def assms(3) by blast
  moreover have "isPlane p" 
    using IncidentP_def assms(5) by blast
  moreover
  {
    fix A'
    assume "IncidentL A' l"
    hence "Col A' ?U ?V" 
      using IncidentL_def by blast
    have "Coplanar A' PA QA RA" 
      by (meson ncoplanar_perm_23 IncidentL_def ‹Coplanar (fst l) PA QA RA› 
          ‹Coplanar (snd l) PA QA RA› ‹IncidentL A' l› 
          col_cop2__cop isLine_def not_col_permutation_2)
    hence "∃ P Q R. p = Plane P Q R ∧ Coplanar A' P Q R" 
      using ‹p = Plane PA QA RA› by blast
    hence "IncidentP A' p" 
      by (simp add: IncidentP_def calculation(2))
  }
  ultimately show ?thesis
    using IncidentLP_def by blast
qed

(** * Group II Order *)

(** Definition of the Between predicate of Hilbert.
    Note that it is different from the Between of Tarski.
    The Between of Hilbert is strict. *)

lemma axiom_between_col:
  assumes "Between_H A B C"
  shows "Col_H A B C" 
  using Between_H_def Col_def assms cols_coincide_2 by presburger

lemma axiom_between_diff:
  assumes "Between_H A B C"
  shows "A ≠ C" 
  using Between_H_def assms by auto

(** If B is between A and C, it is also between C and A. *)

lemma axiom_between_comm: 
  assumes "Between_H A B C"
  shows "Between_H C B A" 
  by (metis Between_H_def assms between_symmetry)

lemma axiom_between_out:
  assumes "A ≠ B" 
  shows "∃ C. Between_H A B C" 
  by (metis Between_H_def assms bet_neq12__neq point_construction_different)

lemma axiom_between_only_one:
  assumes "Between_H A B C"
  shows "¬ Between_H B C A" 
  by (metis Bet_cases Between_H_def assms between_equality)

lemma between_one:
  assumes "A ≠ B" and
    "A ≠ C" and
    "B ≠ C" and
    "Col A B C" 
  shows "Between_H A B C ∨ Between_H B C A ∨ Between_H B A C" 
  using Bet_cases Between_H_def Col_def assms(1) assms(2) assms(3) assms(4) by auto

lemma axiom_between_one:
  assumes "A ≠ B" and
    "A ≠ C" and
    "B ≠ C" and
    "Col_H A B C" 
  shows "Between_H A B C ∨ Between_H B C A ∨ Between_H B A C" 
  by (simp add: assms(1) assms(2) assms(3) assms(4) between_one cols_coincide_1)


(** Axiom of Pasch, (Hilbert version). *)

(** First we define a predicate which means that the line l intersects the segment AB. *)


(** We show that this definition is equivalent to the predicate TS of Tarski. *)

lemma cut_two_sides: 
  shows "cut_H l A B ⟷ (fst l) (snd l) TS A B"
proof -
  {
    assume "cut_H l A B"
    have "(fst l) (snd l) TS A B" 
      by (meson Between_H_def TS_def IncidentL_def ‹cut_H l A B› cut_H_def)
  }
  moreover
  {
    assume "(fst l) (snd l) TS A B"
    then obtain T where "Col T (fst l) (snd l)" and "Bet A T B" 
      using TS_def by blast
    have "¬ IncidentL A l" 
      using IncidentL_def TS_def ‹(fst l) (snd l) TS A B› by auto
    moreover have "¬ IncidentL B l" 
      using IncidentL_def TS_def ‹(fst l) (snd l) TS A B› by blast
    moreover have "∃ I. isLine l ∧ IncidentL I l ∧ Between_H A I B" 
      by (metis Between_H_def IncidentL_def TS_def ‹(fst l) (snd l) TS A B› 
          isLine_def ts_distincts)
    ultimately have "cut_H l A B"
      using cut_H_def by presburger
  }
  ultimately show ?thesis 
    by blast
qed

lemma cop_plane_aux: 
  assumes "Coplanar A B C D" and 
    "A ≠ B" 
  shows "∃ p. IncidentP A p ∧ IncidentP B p ∧ IncidentP C p ∧ IncidentP D p" 
proof -
  obtain X where "(Col A B X ∧ Col C D X) ∨
            (Col A C X ∧ Col B D X) ∨
            (Col A D X ∧ Col B C X)" 
    using Coplanar_def assms(1) by auto
  {
    assume "Col A B C"
    have "∃ p. IncidentP A p ∧ IncidentP B p ∧ IncidentP C p ∧ IncidentP D p" 
    proof (cases "Col A B D")
      case True
      hence "Col A B D" 
        by blast
      obtain E where "¬ Col A B E" 
        using assms(2) not_col_exists by auto
      hence "¬ Col_H A B E" 
        using cols_coincide_1 by blast
      let ?p = "Plane A B E" 
      have "IncidentP A ?p" 
        using EqTP_def ‹¬ Col_H A B E› axiom_plane_existence incidentp_eqp by blast
      moreover have "IncidentP B ?p" 
        using IncidentP_def calculation ncop_distincts by blast
      moreover have "IncidentP C ?p" 
        by (meson Col_cases IncidentP_def ‹Col A B C› calculation(1) ncop__ncols)
      moreover have "IncidentP D ?p" 
        by (meson Col_cases IncidentP_def True calculation(3) ncop__ncols)
      ultimately show ?thesis 
        by blast
    next
      case False
      hence "¬ Col_H A B D" 
        using cols_coincide_1 by blast
      let ?p = "Plane A B D" 
      have "IncidentP A ?p" 
        by (meson EqTP_def ‹¬ Col_H A B D› axiom_plane_existence incidentp_eqp)
      moreover have "IncidentP B ?p" 
        using IncidentP_def calculation ncop_distincts by blast
      moreover have "IncidentP C ?p" 
        using IncidentP_def assms(1) calculation(1) coplanar_perm_12 by blast
      moreover have "IncidentP D ?p" 
        using IncidentP_def calculation(3) ncop_distincts by blast
      ultimately show ?thesis 
        by blast
    qed
  }
  moreover
  {
    assume "¬ Col A B C"
    let ?p = "Plane A B C"
    have "IncidentP A ?p" 
      by (simp add: IncidentP_def Plane_def ‹¬ Col A B C› coplanar_trivial isPlane_def)
    moreover have "IncidentP B ?p" 
      using IncidentP_def calculation ncop_distincts by blast
    moreover have "IncidentP C ?p" 
      using IncidentP_def calculation(2) ncop_distincts by blast
    moreover have "IncidentP D ?p" 
      using IncidentP_def assms(1) calculation(3) coplanar_perm_18 by blast
    ultimately have "∃ p. IncidentP A p ∧ IncidentP B p ∧ IncidentP C p ∧ IncidentP D p" 
      by blast
  }
  ultimately show ?thesis 
    by blast
qed

lemma cop_plane:
  assumes "Coplanar A B C D"
  shows "∃ p. IncidentP A p ∧ IncidentP B p ∧ IncidentP C p ∧ IncidentP D p" 
  by (metis assms cop_plane_aux coplanar_trivial diff_col_ex ncoplanar_perm_22)

lemma plane_cop:
  assumes "IncidentP A p" and 
    "IncidentP B p" and
    "IncidentP C p" and
    "IncidentP D p" 
  shows "Coplanar A B C D" 
proof -
  obtain PA QA RA where "p = Plane PA QA RA" and "Coplanar A PA QA RA" 
    using IncidentP_def assms(1) by auto
  hence "p = (PA,QA,RA)" 
    using Plane_def by blast
  moreover
  obtain PB QB RB where "p = Plane PB QB RB" and "Coplanar B PB QB RB" 
    using IncidentP_def assms(2) by auto
  hence "p = (PB,QB,RB)" 
    using Plane_def by blast
  moreover
  obtain PC QC RC where "p = Plane PC QC RC" and "Coplanar C PC QC RC" 
    using IncidentP_def assms(3) by auto
  hence "p = (PC,QC,RC)" 
    using Plane_def by blast
  moreover
  obtain PD QD RD where "p = Plane PD QD RD" and "Coplanar D PD QD RD" 
    using IncidentP_def assms(4) by auto
  hence "p = (PD,QD,RD)" 
    using Plane_def by blast
  ultimately have "Coplanar B PA QA RA ∧ Coplanar C PA QA RA ∧ Coplanar D PA QA RA" 
    using ‹Coplanar B PB QB RB› ‹Coplanar C PC QC RC› ‹Coplanar D PD QD RD› by fastforce
  have "isPlane p" 
    using IncidentP_def assms(1) by blast
  hence "¬ Col PA QA RA" 
    using isPlane_def ‹p = (PA, QA, RA)› by blast
  thus ?thesis 
    by (meson ‹Coplanar A PA QA RA› coplanar_perm_18 coplanar_pseudo_trans
        ‹Coplanar B PA QA RA ∧ Coplanar C PA QA RA ∧ Coplanar D PA QA RA› )
qed

lemma axiom_pasch:
  assumes "¬ Col_H A B C" and
    "IncidentP A p" and 
    "IncidentP B p" and 
    "IncidentP C p" and
    "IncidentLP l p" and
    "¬ IncidentL C l" and
    "cut_H l A B"
  shows "cut_H l A C ∨ cut_H l B C" 
proof -
  let ?A = "(fst l)"
  let ?B = "(snd l)"
  have "?A ?B TS A B" 
    using assms(7) cut_two_sides by auto
  hence 1: "¬ Col A ?A ?B ∧ ¬ Col B ?A ?B ∧ (∃ T. Col T ?A ?B ∧ Bet A T B)"
    using TS_def by blast
  hence "¬ Col A ?A ?B" 
    by blast
  have "¬ Col B ?A ?B" 
    by (simp add: 1)
  obtain T where "Col T ?A ?B" and "Bet A T B" 
    using 1 by auto
  have "¬ Col A B C" 
    using assms(1) cols_coincide_2 by blast
  have "¬ Col C ?A ?B" 
    using IncidentLP_def IncidentL_def assms(5) assms(6) by blast
  have "Coplanar ?A ?B A C"
  proof (rule plane_cop, insert assms(2) assms(4))
    show "IncidentP (fst l) p" 
      using IncidentLP_def IncidentL_def assms(5) col_trivial_1 by blast
    show "IncidentP (snd l) p" 
      using IncidentLP_def IncidentL_def assms(5) col_trivial_3 by blast
  qed
  have "?A ?B TS A C ∨ ?A ?B OS A C" 
    using ‹Coplanar ?A ?B A C› 1 ‹¬ Col C ?A ?B› cop_nos__ts by blast
  moreover
  {
    assume "?A ?B TS A C" 
    have "cut_H l A C ∨ cut_H l B C" 
      by (simp add: ‹?A ?B TS A C› cut_two_sides)
  } 
  moreover
  {
    assume "?A ?B OS A C" 
    have "cut_H l A C ∨ cut_H l B C" 
      using ‹?A ?B OS A C› ‹?A ?B TS A B› cut_two_sides l9_2 l9_8_2 by blast
  } 
  ultimately show ?thesis
    by blast
qed

lemma Incid_line:
  assumes "A ≠ B" and
    "IncidentL A l" and
    "IncidentL B l" and
    "Col P A B"
  shows "IncidentL P l" 
  by (meson Col_H_def assms(1) assms(2) assms(3) assms(4) cols_coincide_2 
      eq_incident incident_eq)

(** * Group III Congruence *)

(** The cong predicate of Hilbert is the same as the one of Tarski: *)

lemma out_outH: 
  assumes "P Out A B" 
  shows "outH P A B" 
  using Between_H_def Out_def assms outH_def by auto

lemma axiom_hcong_1_existence:
  assumes "A ≠ B" and
    "A' ≠ P" and
    "IncidentL A' l" and
    "IncidentL P l" 
  shows "∃ B'. IncidentL B' l ∧ outH A' P B' ∧ Cong A' B' A B"
proof -
  obtain B' where "A' Out B' P ∧ Cong A' B' A B" 
    using assms(1) assms(2) l6_11_existence by presburger
  have "IncidentL B' l" 
    using Col_perm Incid_line ‹A' Out B' P ∧ Cong A' B' A B› assms(2) assms(3) 
      assms(4) out_col by blast
  moreover have "outH A' P B'" 
    by (simp add: ‹A' Out B' P ∧ Cong A' B' A B› l6_6 out_outH)
  ultimately show ?thesis 
    using ‹A' Out B' P ∧ Cong A' B' A B› by blast
qed

lemma axiom_hcong_1_uniqueness:
  assumes (*"A ≠ B" and*)
    "IncidentL M l" and
    "IncidentL A' l" and 
    (*"IncidentL B' l" and*)
    "IncidentL A'' l" and
    (*"IncidentL B'' l" and*)
    "Between_H A' M B'" and
    "Cong M A' A B" and
    "Cong M B' A B" and
    "Between_H A'' M B''" and
    "Cong M A'' A B" and
    "Cong M B'' A B"
  shows "(A' = A'' ∧ B' = B'') ∨ (A' = B'' ∧ B' = A'')" 
proof -
  let ?A = "fst l"
  let ?B = "snd l"
  have "A'' ≠ M" 
    using Between_H_def assms(7)by blast
  {
    assume "M Out A' A''"
    have "M Out A'' A''" 
      by (simp add: ‹A'' ≠ M› out_trivial)
    hence "A' = A''" 
      using l6_11_uniqueness ‹M Out A' A''› assms(5) assms(8) by blast
    hence "A' = A'' ∧ B' = B''" 
      by (metis Between_H_def assms(7) assms(9) assms(4) assms(6) construction_uniqueness)
  }
  moreover
  {
    assume "¬ M Out A' A''"
    have "Col A' M A''" 
      using col3 [where ?X = "?A" and ?Y = "?B"] 
      by (meson Col_H_def IncidentL_def assms(1) assms(2) assms(3) ncols_coincide)
    hence "Bet A' M A''" 
      using not_out_bet ‹¬ M Out A' A''› by blast
    have "A' = B''" 
      by (metis Between_H_def ‹Bet A' M A''› assms(7) assms(9) assms(5) 
          between_symmetry construction_uniqueness)
    hence "A' = B'' ∧ B' = A''" 
      by (metis Between_H_def ‹Bet A' M A''› assms(8) assms(4) assms(6) construction_uniqueness)
  }
  ultimately show ?thesis
    by blast
qed

(** As a remark we also prove another version of this axiom as formalized in Isabelle by
Phil Scott. *)

lemma axiom_hcong_scott:
  assumes "A ≠ C" and 
    "P ≠ Q"
  shows "∃ B. same_side_scott A B C ∧ Cong P Q A B"
proof -
  obtain X where "A Out X C" and "Cong A X P Q" 
    using assms(1) assms(2) l6_11_existence by metis
  have "A ≠ X" 
    using ‹A Out X C› l6_3_1 by blast
  moreover have "Col_H A X C" 
    by (simp add: ‹A Out X C› cols_coincide_2 out_col)
  moreover have "¬ Between_H X A C" 
    using Between_H_def ‹A Out X C› not_bet_and_out by force
  moreover have "Cong P Q A X" 
    using Cong_cases ‹Cong A X P Q› by blast
  ultimately show ?thesis
    using assms(1) same_side_scott_def by blast
qed

(** We define when two segments do not intersect. *)


(** Note that two disjoint segments may share one of their extremities. *)

lemma col_disjoint_bet:
  assumes "Col_H A B C" and
    "disjoint_H A B B C"
  shows "Bet A B C" 
proof -
  have "Col A B C" 
    by (simp add: assms(1) cols_coincide_1)
  show ?thesis 
  proof (cases "A = B")
    case True
    thus ?thesis 
      by (simp add: between_trivial2)
  next
    case False
    hence "A ≠ B" 
      by blast
    show ?thesis 
    proof (cases "B = C")
      case True
      thus ?thesis 
        by (simp add: between_trivial)
    next
      case False
      hence "B ≠ C" 
        by blast
      {
        assume "Bet B C A"
        obtain M where "M Midpoint B C" 
          using midpoint_existence by blast
        have "Between_H A M B" 
          by (metis Between_H_def False Midpoint_def ‹A ≠ B› ‹Bet B C A› 
              ‹M Midpoint B C› axiom_between_comm between_equality_2 between_exchange4
              midpoint_not_midpoint midpoint_out out_diff1)
        moreover have "Between_H B M C" 
          by (metis Between_H_def False Midpoint_def ‹M Midpoint B C› 
              calculation is_midpoint_id_2)
        ultimately have "∃ P. Between_H A P B ∧ Between_H B P C" 
          by blast
        hence False 
          using assms(2) disjoint_H_def by blast
      }
      moreover
      {
        assume "Bet C A B"
        obtain M where "M Midpoint A B"
          using midpoint_existence by blast
        have "Between_H A M B" 
          by (metis Between_H_def ‹A ≠ B› ‹M Midpoint A B› midpoint_bet midpoint_distinct_1)
        moreover have "Between_H B M C" 
          by (metis Bet_cases Between_H_def False ‹Bet B C A ⟹ False› ‹Bet C A B› 
              between_exchange2 calculation)
        ultimately
        have "∃ P. Between_H A P B ∧ Between_H B P C" 
          by blast
        hence False  
          using assms(2) disjoint_H_def by blast
      }
      ultimately show ?thesis 
        using ‹Col A B C› Col_def by blast
    qed
  qed
qed

lemma axiom_hcong_3:
  assumes "Col_H A B C" and
    "Col_H A' B' C'" and
    "disjoint_H A B B C" and
    "disjoint_H A' B' B' C'" and
    "Cong A B A' B'" and
    "Cong B C B' C'"
  shows "Cong A C A' C'" 
  by (meson assms(1) assms(2) assms(3) assms(4) assms(5) assms(6) col_disjoint_bet l2_11_b)

lemma exists_not_incident: 
  assumes "A ≠ B" 
  shows "∃ C. ¬ IncidentL C (Line A B)" 
  using Col_H_def IncidentL_def lower_dim' by blast

(** Same side predicate corresponds to OS of Tarski. *)

lemma same_side_one_side: 
  assumes "same_side_H A B l"
  shows "(fst l) (snd l) OS A B" 
  by (meson OS_def cut_two_sides assms same_side_H_def)

lemma one_side_same_side: 
  assumes "(fst l)(snd l) OS A B"
  shows "same_side_H A B l"
proof -
  have "isLine l" 
    using assms isLine_def os_distincts by presburger
  thus ?thesis
    using OS_def assms cut_two_sides same_side_H_def by presburger
qed

lemma OS_distinct:
  assumes "P Q OS A B"
  shows "P ≠ Q" 
  using assms os_distincts by auto

lemma OS_same_side':
  assumes "P Q OS A B"
  shows "same_side'_H A B P Q" 
proof -
  have "P ≠ Q" 
    using assms os_distincts by blast
  moreover
  {
    fix l
    assume "IncidentL P l" and
      "IncidentL Q l"
    hence "isLine l" 
      using IncidentL_def by auto
    have "(fst l) ≠ (snd l)" 
      using ‹isLine l› isLine_def by auto
    have "Col P (fst l) (snd l)" 
      using IncidentL_def ‹IncidentL P l› by auto
    have "Col Q (fst l) (snd l)" 
      using IncidentL_def ‹IncidentL Q l› by auto
    have "(fst l) (snd l) OS A B" 
      by (metis (no_types, lifting) ‹Col P (fst l) (snd l)› ‹Col Q (fst l) (snd l)› 
          ‹(fst l) ≠ (snd l)› assms col2_os__os l6_16_1 not_col_permutation_5)
    hence "same_side_H A B l" 
      using one_side_same_side by blast
  }
  ultimately show ?thesis 
    using same_side'_H_def by auto
qed

lemma same_side_OS:
  assumes "same_side'_H P Q A B"
  shows "A B OS P Q" 
proof -
  obtain X where "IncidentL A X" and "IncidentL B X" 
    using assms axiom_line_existence same_side'_H_def by blast
  hence "same_side_H P Q X" 
    using EqTL_def assms incident_eq same_side'_H_def by blast
  thus ?thesis
    by (metis IncidentL_def assms axiom_line_existence col2_os__os col_permutation_1 
        same_side'_H_def same_side_one_side)
qed

(** This is equivalent to the out predicate of Tarski. *)

lemma outH_out: 
  assumes "outH P A B"
  shows "P Out A B" 
  using Between_H_def Out_def assms outH_def out_trivial by force

(** The 2D version of the fourth congruence axiom **)

lemma incident_col: 
  assumes "IncidentL M l"
  shows "Col M (fst l)(snd l)" 
  using IncidentL_def assms by auto

lemma col_incident:
  assumes "(fst l) ≠ (snd l)" and (** ROLL: EXPLICIT ADD **)
    "Col M (fst l)(snd l)"
  shows "IncidentL M l"   
  by (simp add: IncidentL_def assms(1) assms(2) isLine_def)

lemma Bet_Between_H: 
  assumes "Bet A B C" and
    "A ≠ B" and
    "B ≠ C" 
  shows "Between_H A B C" 
  using Between_H_def assms(1) assms(2) assms(3) bet_neq12__neq by presburger

lemma axiom_cong_5':
  assumes (*"¬ Col_H A B C" and*)
    "¬ Col_H A' B' C'" and
    "Cong A B A' B'" and
    "Cong A C A' C'" and
    "B A C CongA B' A' C'"
  shows "A B C CongA A' B' C'" 
  by (metis assms(2) assms(3) assms(4) assms(1) cols_coincide_2 cong_diff_4 
      l11_49 not_col_distincts)

lemma axiom_cong_5'_bis:
  assumes "¬ Col_H A B C" and
    (*"¬ Col_H A' B' C'" and*)
    "Cong A B A' B'" and
    "Cong A C A' C'" and
    "B A C CongA B' A' C'"
  shows "A B C CongA A' B' C'" 
  using assms(1) assms(3) assms(4) assms(2) col_trivial_2 cols_coincide_2 l11_49 by blast

lemma axiom_hcong_4_existence:
  assumes "¬ Col_H P PO X" and
    "¬ Col_H A B C" 
  shows "∃ Y. (A B C CongA X PO Y ∧ same_side'_H P Y PO X)" 
proof -
  have "¬ Col P PO X"   
    by (simp add: assms(1) ncols_coincide)
  have "¬ Col A B C"   
    using assms(2) cols_coincide_2 by blast
  have "¬ Col X PO P" 
    using ‹¬ Col P PO X› not_col_permutation_3 by blast
  obtain Y where "A B C CongA X PO Y" and "X PO OS Y P" 
    using ‹¬ Col A B C› ‹¬ Col X PO P› angle_construction_1 by blast
  thus ?thesis 
    using OS_same_side' invert_one_side one_side_symmetry by blast
qed

lemma same_side_trans:
  assumes "same_side_H A B l" and
    "same_side_H B C l"
  shows "same_side_H A C l" 
  using assms(1) assms(2) one_side_same_side one_side_transitivity same_side_one_side by blast

lemma same_side_sym:
  assumes "same_side_H A B l"
  shows "same_side_H B A l" 
  by (meson assms same_side_H_def)

lemma axiom_hcong_4_uniqueness:
  assumes "¬ Col_H P PO X" and
    "¬ Col_H A B C" and
    "A B C CongA X PO Y" and
    "A B C CongA X PO Y'" and
    "same_side'_H P Y PO X" and
    "same_side'_H P Y' PO X"
  shows "outH PO Y Y'" 
proof -
  have "¬ Col P PO X"   
    using assms(1) cols_coincide_2 by blast
  have "¬ Col A B C"   
    using assms(2) cols_coincide_2 by blast
  have "X PO Y CongA X PO Y'" 
    using assms(3) assms(4) conga_sym not_conga by blast
  moreover
  have "X PO OS Y Y'" 
    by (meson assms(5) assms(6) invert_one_side one_side_symmetry 
        one_side_transitivity same_side_OS)
  ultimately have "PO Out Y Y'" 
    by (simp add: conga_os__out)
  thus ?thesis 
    by (simp add: out_outH)
qed

lemma axiom_conga_comm:
  assumes "¬ Col_H A B C" 
  shows "A B C CongA C B A" 
  by (metis assms col_trivial_1 col_trivial_2 cols_coincide_2 conga_pseudo_refl)

lemma axiom_congaH_outH_congaH:
  assumes "A B C CongA D E F" and
    "Between_H B A A' ∨ Between_H B A' A ∨ B ≠ A ∧ A = A'" and
    "Between_H B C C' ∨ Between_H B C' C ∨ B ≠ C ∧ C = C'" and
    "Between_H E D D' ∨ Between_H E D' D ∨ E ≠ D ∧ D = D'" and
    "Between_H E F F' ∨ Between_H E F' F ∨ E ≠ F ∧ F = F'"
  shows "A' B C' CongA D' E F'" 
proof (rule l11_10 [where ?A = "A" and ?C = "C" and ?D = "D" and ?F = "F"], insert assms(1))
  show "B Out A' A" 
    using Between_H_def Out_def assms(2) out_trivial by force
  show "B Out C' C" 
    using assms(3) outH_def outH_out by blast
  show "E Out D' D" 
    using assms(4) outH_def outH_out by blast
  show "E Out F' F" 
    using assms(5) outH_def outH_out by blast
qed

lemma axiom_conga_permlr:
  assumes "A B C CongA D E F"
  shows "C B A CongA F E D" 
  by (simp add: assms conga_comm)

lemma axiom_conga_refl: 
  assumes "¬ Col_H A B C"
  shows "A B C CongA A B C" 
  using assms axiom_conga_comm conga_right_comm by blast

end
end