Theory Hilbert_Neutral_2D_Model_Tarski_Neutral_2D

(* IsageoCoq - Hilbert_Neutral_2D_Model_Tarski_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 Hilbert_Neutral_2D_Model_Tarski_Neutral_2D

imports 
  Tarski_Neutral_Hilbert
  Tarski_Neutral_2D
  Hilbert_Neutral_2D

begin

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

subsection "Interpretation"

context Tarski_neutral_2D

begin

interpretation Interpretation_Hilbert_neutral_dimensionless_pre: Hilbert_neutral_dimensionless_pre 
  where IncidL = IncidentL and 
    IncidP = IncidentP and
    EqL = EqTL and 
    EqP = EqTP and 
    IsL = isLine and 
    IsP = isPlane and
    BetH = Between_H and
    CongH = Cong and
    CongaH = CongA_H 
proof -
qed

interpretation Intrepretation_Hilbert_neutral_dimensionless: Hilbert_neutral_dimensionless
  where IncidL = IncidentL and 
    IncidP = IncidentP and
    EqL = EqTL and 
    EqP = EqTP and 
    IsL = isLine and 
    IsP = isPlane and
    BetH = Between_H and
    CongH = Cong and
    CongaH = CongA_H and
    PP = TPA and
    PQ = TPB and
    PR = TPC
proof

(* Begin Preliminaries *)
  have "∀ A B C. Interpretation_Hilbert_neutral_dimensionless_pre.ColH A B C ⟷ Col_H A B C" 
  proof -
    {
      fix A B C
      assume "Interpretation_Hilbert_neutral_dimensionless_pre.ColH A B C"
      hence "∃ l. isLine l ∧ IncidentL A l ∧ IncidentL B l ∧ IncidentL C l" 
        by (simp add: Hilbert_neutral_dimensionless_pre.ColH_def)
      hence "Col_H A B C" 
        using Col_H_def EqTL_def axiom_line_uniqueness cols_coincide_2 not_col_distincts by blast
    }
    moreover
    {
      fix A B C
      assume "Col_H A B C" 
      hence "∃ l. isLine l ∧ IncidentL A l ∧ IncidentL B l ∧ IncidentL C l" 
        using Col_H_def by blast
      have "Interpretation_Hilbert_neutral_dimensionless_pre.ColH A B C" 
        using Interpretation_Hilbert_neutral_dimensionless_pre.ColH_def 
          ‹∃l. isLine l ∧ IncidentL A l ∧ IncidentL B l ∧ IncidentL C l› by blast
    }
    ultimately show ?thesis
      by blast
  qed
  have "∀ A B C. Interpretation_Hilbert_neutral_dimensionless_pre.ColH A B C ⟷ Col A B C"
    using ‹∀A B C. Interpretation_Hilbert_neutral_dimensionless_pre.ColH A B C = Col_H A B C› 
      cols_coincide by blast
  have "∀ A B l. Interpretation_Hilbert_neutral_dimensionless_pre.same_side A B l
                 ⟷ same_side_H A B l" 
    by (simp add: Hilbert_neutral_dimensionless_pre.cut_def 
        Interpretation_Hilbert_neutral_dimensionless_pre.same_side_def cut_H_def same_side_H_def)
  have "∀ A B C D. Interpretation_Hilbert_neutral_dimensionless_pre.same_side' A B C D 
                   ⟷ same_side'_H A B C D" 
    by (simp add: Hilbert_neutral_dimensionless_pre.same_side'_def 
        ‹∀A B l. Interpretation_Hilbert_neutral_dimensionless_pre.same_side A B l 
                   = same_side_H A B l› 
        same_side'_H_def)

(* End Preliminaries *)

  show "⋀l. isLine l ⟶ l =l= l" 
    by (simp add: eq_reflexivity)
  show "⋀l1 l2. isLine l1 ∧ isLine l2 ∧ l1 =l= l2 ⟶ l2 =l= l1" 
    using eq_symmetry by blast
  show "⋀l1 l2 l3. l1 =l= l2 ∧ l2 =l= l3 ⟶ l1 =l= l3" 
    using eq_transitivity by blast
  show "⋀p. isPlane p ⟶ p =p= p" 
    by (simp add: eqp_reflexivity)
  show "⋀p1 p2. p1 =p= p2 ⟶ p2 =p= p1" 
    using eqp_symmetry by blast
  show "⋀p1 p2 p3. p1 =p= p2 ∧ p2 =p= p3 ⟶ p1 =p= p3" 
    using eqp_transitivity by blast
  show "⋀A B. A ≠ B ⟶ (∃l. isLine l ∧ IncidentL A l ∧ IncidentL B l)" 
    using axiom_line_existence by blast
  show "⋀A B l m.
       A ≠ B ∧ isLine l ∧ isLine m ∧
       IncidentL A l ∧ IncidentL B l ∧ IncidentL A m ∧ IncidentL B m ⟶
       l =l= m" 
    using axiom_line_uniqueness by blast
  show "∀l. isLine l ⟶ (∃ A B. IncidentL A l ∧ IncidentL B l ∧ A ≠ B)" 
    using axiom_two_points_on_line by blast
  show "TPA ≠ TPB ∧ TPB ≠ TPC ∧ TPA ≠ TPC ∧ 
           ¬ Interpretation_Hilbert_neutral_dimensionless_pre.ColH TPA TPB TPC" 
    using Bet_cases  between_trivial lower_dim third_point 
      ‹∀A B C. Interpretation_Hilbert_neutral_dimensionless_pre.ColH A B C = (Col A B C)›
    by blast
  show "∀A B C.
       ¬ Interpretation_Hilbert_neutral_dimensionless_pre.ColH A B C ⟶
       (∃p. isPlane p ∧ IncidentP A p ∧ IncidentP B p ∧ IncidentP C p)" 
    using bet__coplanar between_trivial2 cop_plane IncidentP_def by blast
  show "∀p. ∃A. isPlane p ⟶ IncidentP A p" 
    by (simp add: axiom_one_point_on_plane)
  show "⋀A B C p q.
       ¬ Interpretation_Hilbert_neutral_dimensionless_pre.ColH A B C ∧
       isPlane p ∧ isPlane q ∧
       IncidentP A p ∧
       IncidentP B p ∧
       IncidentP C p ∧ IncidentP A q ∧ IncidentP B q ∧ IncidentP C q ⟶
       p =p= q" 
    using Col_H_def Interpretation_Hilbert_neutral_dimensionless_pre.ColH_def 
      axiom_plane_uniqueness by blast
  show "∀A B l p.
       A ≠ B ∧ isLine l ∧ isPlane p ∧
       IncidentL A l ∧ IncidentL B l ∧ IncidentP A p ∧ IncidentP B p ⟶
       Interpretation_Hilbert_neutral_dimensionless_pre.IncidLP l p" 
    by (meson IncidentLP_def Interpretation_Hilbert_neutral_dimensionless_pre.IncidLP_def 
        axiom_line_on_plane)
  show "⋀A B C. Between_H A B C ⟶ A ≠ C" 
    using axiom_between_diff by blast
  show "⋀A B C. Between_H A B C ⟶ Interpretation_Hilbert_neutral_dimensionless_pre.ColH A B C" 
    by (meson Between_H_def Col_H_def Col_def 
        Interpretation_Hilbert_neutral_dimensionless_pre.ColH_def cols_coincide_2)
  show "⋀A B C. Between_H A B C ⟶ Between_H C B A" 
    using axiom_between_comm by blast
  show "⋀A B. A ≠ B ⟶ (∃C. Between_H A B C)" 
    by (simp add: axiom_between_out)
  show "⋀A B C. Between_H A B C ⟶ ¬ Between_H B C A" 
    using axiom_between_only_one by blast
  {
    fix A B C p l
    assume "¬ Interpretation_Hilbert_neutral_dimensionless_pre.ColH A B C" and
      "isLine l" and
      "IncidentP A p" and
      "IncidentP B p" and
      "IncidentP C p" and
      "Interpretation_Hilbert_neutral_dimensionless_pre.IncidLP l p" and
      "¬ IncidentL C l" and
      "Interpretation_Hilbert_neutral_dimensionless_pre.cut l A B"
    have "¬ Col A B C" 
      by (meson Col_H_def Interpretation_Hilbert_neutral_dimensionless_pre.ColH_def 
          ‹¬ Interpretation_Hilbert_neutral_dimensionless_pre.ColH A B C› cols_coincide_2)
    moreover have "cut_H l A B" 
      using Interpretation_Hilbert_neutral_dimensionless_pre.cut_def 
        ‹Interpretation_Hilbert_neutral_dimensionless_pre.cut l A B› cut_H_def by blast
    ultimately have "cut_H l A C ∨ cut_H l B C" 
      using axiom_pasch Interpretation_Hilbert_neutral_dimensionless_pre.IncidLP_def 
        ‹IncidentP A p› ‹IncidentP B p› ‹IncidentP C p› 
        ‹Interpretation_Hilbert_neutral_dimensionless_pre.IncidLP l p› ‹¬ IncidentL C l› 
        axiom_line_on_plane axiom_two_points_on_line cols_coincide_1 by meson
    hence "Interpretation_Hilbert_neutral_dimensionless_pre.cut l A C ∨
       Interpretation_Hilbert_neutral_dimensionless_pre.cut l B C"  
      by (simp add: Hilbert_neutral_dimensionless_pre.cut_def cut_H_def)
  }
  thus "⋀A B C p l.
       ¬ Interpretation_Hilbert_neutral_dimensionless_pre.ColH A B C ∧
       isLine l ∧ isPlane p ∧ IncidentP A p ∧ IncidentP B p ∧ IncidentP C p ∧
       Interpretation_Hilbert_neutral_dimensionless_pre.IncidLP l p ∧
       ¬ IncidentL C l ∧ Interpretation_Hilbert_neutral_dimensionless_pre.cut l A B ⟶
       Interpretation_Hilbert_neutral_dimensionless_pre.cut l A C ∨
       Interpretation_Hilbert_neutral_dimensionless_pre.cut l B C" 
    by blast
  {
    fix l 
    fix A B A' P::'a
    assume "A ≠ B" and
      "A' ≠ P" and
      "isLine l" and
      "IncidentL A' l" and
      "IncidentL P l"
    then obtain B' where "IncidentL B' l ∧ outH A' P B' ∧ Cong A' B' A B"  
      using axiom_hcong_1_existence by presburger
    hence "∃B'. IncidentL B' l ∧ 
               Interpretation_Hilbert_neutral_dimensionless_pre.outH A' P B' ∧ Cong A' B' A B" 
      using Interpretation_Hilbert_neutral_dimensionless_pre.outH_def outH_def by auto
  }
  thus "⋀l A B A' P. 
       A ≠ B ∧ A' ≠ P ∧ isLine l ∧ IncidentL A' l ∧ IncidentL P l ⟶
       (∃B'. IncidentL B' l ∧ 
             Interpretation_Hilbert_neutral_dimensionless_pre.outH A' P B' ∧ Cong A' B' A B)"
    by blast
  show "⋀A B C D E F. Cong A B C D ∧ Cong A B E F ⟶ Cong C D E F" 
    using cong_inner_transitivity by blast
  {
    fix A B C A' B' C'
    assume "Interpretation_Hilbert_neutral_dimensionless_pre.ColH A B C" and
      "Interpretation_Hilbert_neutral_dimensionless_pre.ColH A' B' C'" and
      "Interpretation_Hilbert_neutral_dimensionless_pre.disjoint A B B C" and
      "Interpretation_Hilbert_neutral_dimensionless_pre.disjoint A' B' B' C'" and
      "Cong A B A' B'" and
      "Cong B C B' C'" 
    have " (∃ l. IncidentL A l ∧ IncidentL B l ∧ IncidentL C l)" 
      using Interpretation_Hilbert_neutral_dimensionless_pre.ColH_def 
        ‹Interpretation_Hilbert_neutral_dimensionless_pre.ColH A B C› by force
    then obtain l where "IncidentL A l" and "IncidentL B l" and "IncidentL C l"
      by blast
    hence "Col A B C"
      using ‹Interpretation_Hilbert_neutral_dimensionless_pre.ColH A B C›
        ‹∀A B C. Interpretation_Hilbert_neutral_dimensionless_pre.ColH A B C = (Col A B C)› 
      by auto 
    moreover
    have " (∃ l. IncidentL A' l ∧ IncidentL B' l ∧ IncidentL C' l)" 
      using Interpretation_Hilbert_neutral_dimensionless_pre.ColH_def 
        ‹Interpretation_Hilbert_neutral_dimensionless_pre.ColH A' B' C'› by force
    then obtain l' where "IncidentL A' l'" and "IncidentL B' l'" and "IncidentL C' l'"
      by blast
    hence "Col A' B' C'"
      using ‹Interpretation_Hilbert_neutral_dimensionless_pre.ColH A' B' C'›
        ‹∀A B C. Interpretation_Hilbert_neutral_dimensionless_pre.ColH A B C = (Col A B C)›
      by blast 
    moreover
    have "¬ (∃ P. Between_H A P B ∧ Between_H B P C)" 
      using Interpretation_Hilbert_neutral_dimensionless_pre.disjoint_def 
        ‹Interpretation_Hilbert_neutral_dimensionless_pre.disjoint A B B C› by blast
    have "¬ (∃ P. Between_H A' P B' ∧ Between_H B' P C')" 
      using Interpretation_Hilbert_neutral_dimensionless_pre.disjoint_def 
        ‹Interpretation_Hilbert_neutral_dimensionless_pre.disjoint A' B' B' C'› by blast
    have "Col_H A B C" 
      using calculation(1) cols_coincide_2 by blast
    hence "Bet A B C" 
      using ‹∄P. Between_H A P B ∧ Between_H B P C› col_disjoint_bet disjoint_H_def by blast
    moreover
    have "Col_H A' B' C'" 
      by (simp add: calculation(2) cols_coincide_2)
    moreover
    hence "Bet A' B' C'" 
      by (simp add: ‹∄P. Between_H A' P B' ∧ Between_H B' P C'› col_disjoint_bet disjoint_H_def)
    ultimately
    have "Cong A C A' C'" 
      using Tarski_neutral_dimensionless.l2_11_b Tarski_neutral_dimensionless_axioms 
        ‹Cong A B A' B'› ‹Cong B C B' C'› by fastforce
  }
  thus "⋀A B C A' B' C'.
       Interpretation_Hilbert_neutral_dimensionless_pre.ColH A B C ∧
       Interpretation_Hilbert_neutral_dimensionless_pre.ColH A' B' C' ∧
       Interpretation_Hilbert_neutral_dimensionless_pre.disjoint A B B C ∧
       Interpretation_Hilbert_neutral_dimensionless_pre.disjoint A' B' B' C' ∧
       Cong A B A' B' ∧ Cong B C B' C' ⟶
       Cong A C A' C'" 
    by blast
  {
    fix A B C
    assume "¬ Interpretation_Hilbert_neutral_dimensionless_pre.ColH A B C"
    hence "¬ Col A B C" 
      using ‹∀A B C. Interpretation_Hilbert_neutral_dimensionless_pre.ColH A B C = (Col A B C)› 
      by blast
    hence "A B C CongA A B C" 
      by (metis conga_refl not_col_distincts)
    hence "CongA_H A B C A B C" 
      by (simp add: CongA_H_def)
  }
  thus "⋀A B C.
       ¬ Interpretation_Hilbert_neutral_dimensionless_pre.ColH A B C ⟶ CongA_H A B C A B C" 
    by blast
  show "⋀A B C.
       ¬ Interpretation_Hilbert_neutral_dimensionless_pre.ColH A B C ⟶ CongA_H A B C C B A" 
    using CongA_H_def 
      ‹⋀Ca Ba A. ¬ Interpretation_Hilbert_neutral_dimensionless_pre.ColH A Ba Ca 
                 ⟶ CongA_H A Ba Ca A Ba Ca› conga_right_comm by presburger
  show "⋀A B C D E F. CongA_H A B C D E F ⟶ CongA_H C B A F E D" 
    by (meson CongA_H_def axiom_conga_permlr)
  show "⋀A B C D E F A' C' D' F'.
       CongA_H A B C D E F ∧
       Interpretation_Hilbert_neutral_dimensionless_pre.outH B A A' ∧
       Interpretation_Hilbert_neutral_dimensionless_pre.outH B C C' ∧
       Interpretation_Hilbert_neutral_dimensionless_pre.outH E D D' ∧
       Interpretation_Hilbert_neutral_dimensionless_pre.outH E F F' ⟶
       CongA_H A' B C' D' E F'" 
    using axiom_congaH_outH_congaH CongA_H_def outH_def 
      Interpretation_Hilbert_neutral_dimensionless_pre.outH_def by force
  {
    fix P PO X A B C
    assume "¬ Interpretation_Hilbert_neutral_dimensionless_pre.ColH P PO X" and
      "¬ Interpretation_Hilbert_neutral_dimensionless_pre.ColH A B C" 
    have "¬ Col P PO X" 
      by (meson Col_H_def Interpretation_Hilbert_neutral_dimensionless_pre.ColH_def 
          ‹¬ Interpretation_Hilbert_neutral_dimensionless_pre.ColH P PO X› cols_coincide_2)
    moreover
    have "¬ Col A B C" 
      using Col_H_def Interpretation_Hilbert_neutral_dimensionless_pre.ColH_def 
        ‹¬ Interpretation_Hilbert_neutral_dimensionless_pre.ColH A B C› cols_coincide_2 by blast
    ultimately
    obtain Y where "A B C CongA X PO Y" and "same_side'_H P Y PO X" 
      using axiom_hcong_4_existence cols_coincide_1 by blast 
    hence "PO ≠ X ∧ (∀ l. isLine l ⟶ (IncidentL PO l ∧ IncidentL X l) ⟶ same_side_H P Y l)"
      using same_side'_H_def by auto
    have "∃Y. CongA_H A B C X PO Y ∧ 
              Interpretation_Hilbert_neutral_dimensionless_pre.same_side' P Y PO X"
    proof -
      have "CongA_H A B C X PO Y" 
        by (simp add: CongA_H_def ‹A B C CongA X PO Y›)
      moreover 
      have "Interpretation_Hilbert_neutral_dimensionless_pre.same_side' P Y PO X" 
        by (simp add: 
            ‹∀A B C D. Interpretation_Hilbert_neutral_dimensionless_pre.same_side' A B C D 
                         = same_side'_H A B C D› ‹same_side'_H P Y PO X›)
      ultimately show ?thesis
        by blast
    qed
  }
  thus "⋀P PO X A B C.
       ¬ Interpretation_Hilbert_neutral_dimensionless_pre.ColH P PO X ∧
       ¬ Interpretation_Hilbert_neutral_dimensionless_pre.ColH A B C ⟶
       (∃Y. CongA_H A B C X PO Y ∧
            Interpretation_Hilbert_neutral_dimensionless_pre.same_side' P Y PO X)" 
    by blast
  {
    fix P PO X A B C Y Y'
    assume "¬ Interpretation_Hilbert_neutral_dimensionless_pre.ColH P PO X" and
      "¬ Interpretation_Hilbert_neutral_dimensionless_pre.ColH A B C" and
      "CongA_H A B C X PO Y" and
      "CongA_H A B C X PO Y'" and
      "Interpretation_Hilbert_neutral_dimensionless_pre.same_side' P Y PO X" and
      "Interpretation_Hilbert_neutral_dimensionless_pre.same_side' P Y' PO X" 
    have "¬ Col P PO X" 
      by (meson Col_H_def Interpretation_Hilbert_neutral_dimensionless_pre.ColH_def 
          ‹¬ Interpretation_Hilbert_neutral_dimensionless_pre.ColH P PO X› cols_coincide_2)
    moreover
    have "¬ Col A B C" 
      using Col_H_def Interpretation_Hilbert_neutral_dimensionless_pre.ColH_def 
        ‹¬ Interpretation_Hilbert_neutral_dimensionless_pre.ColH A B C› cols_coincide_2 by blast
    moreover
    have "A B C CongA X PO Y" 
      using CongA_H_def ‹CongA_H A B C X PO Y› by blast
    moreover
    have "A B C CongA X PO Y'" 
      using CongA_H_def ‹CongA_H A B C X PO Y'› by auto
    ultimately
    have "Interpretation_Hilbert_neutral_dimensionless_pre.outH PO Y Y'" 
      using ‹Interpretation_Hilbert_neutral_dimensionless_pre.same_side' P Y PO X› 
        ‹Interpretation_Hilbert_neutral_dimensionless_pre.same_side' P Y' PO X› 
        axiom_hcong_4_uniqueness cols_coincide_1 
      by (metis Interpretation_Hilbert_neutral_dimensionless_pre.outH_def 
          ‹∀A B C D. Interpretation_Hilbert_neutral_dimensionless_pre.same_side' A B C D 
                      = same_side'_H A B C D› 
          outH_def)
  }
  thus "⋀P PO X A B C Y Y'.
       ¬ Interpretation_Hilbert_neutral_dimensionless_pre.ColH P PO X ∧
       ¬ Interpretation_Hilbert_neutral_dimensionless_pre.ColH A B C ∧
       CongA_H A B C X PO Y ∧
       CongA_H A B C X PO Y' ∧
       Interpretation_Hilbert_neutral_dimensionless_pre.same_side' P Y PO X ∧
       Interpretation_Hilbert_neutral_dimensionless_pre.same_side' P Y' PO X ⟶
       Interpretation_Hilbert_neutral_dimensionless_pre.outH PO Y Y'" 
    by blast
  {
    fix A B C A' B' C'
    assume "¬ Interpretation_Hilbert_neutral_dimensionless_pre.ColH A B C" and
      "¬ Interpretation_Hilbert_neutral_dimensionless_pre.ColH A' B' C'" and
      "Cong A B A' B'" and
      "Cong A C A' C'" and
      "CongA_H B A C B' A' C'"
    have "¬ Col_H A B C" 
      using ‹∀A B C. Interpretation_Hilbert_neutral_dimensionless_pre.ColH A B C = Col_H A B C› 
        ‹¬ Interpretation_Hilbert_neutral_dimensionless_pre.ColH A B C› by auto
    moreover
    have "¬ Col_H A' B' C'" 
      using ‹∀A B C. Interpretation_Hilbert_neutral_dimensionless_pre.ColH A B C = Col_H A B C› 
        ‹¬ Interpretation_Hilbert_neutral_dimensionless_pre.ColH A' B' C'› by blast
    have "¬ Col A B C" 
      using Col_H_def Interpretation_Hilbert_neutral_dimensionless_pre.ColH_def 
        ‹¬ Interpretation_Hilbert_neutral_dimensionless_pre.ColH A B C› cols_coincide_2 by blast
    moreover
    have "¬ Col A' B' C'" 
      using Col_H_def Interpretation_Hilbert_neutral_dimensionless_pre.ColH_def 
        ‹¬ Interpretation_Hilbert_neutral_dimensionless_pre.ColH A' B' C'› cols_coincide_2 by blast
    moreover
    have "B A C CongA B' A' C'" 
      using CongA_H_def ‹CongA_H B A C B' A' C'› by auto
    ultimately
    have "CongA_H A B C A' B' C'" 
      using CongA_H_def ‹Cong A B A' B'› ‹Cong A C A' C'› l11_49 not_col_distincts by blast
  }
  thus "⋀A B C A' B' C'.
       ¬ Interpretation_Hilbert_neutral_dimensionless_pre.ColH A B C ∧
       ¬ Interpretation_Hilbert_neutral_dimensionless_pre.ColH A' B' C' ∧
       Cong A B A' B' ∧ Cong A C A' C' ∧ CongA_H B A C B' A' C' ⟶
       CongA_H A B C A' B' C'" 
    by blast
  show "⋀A B C D. Cong A B C D ⟶ Cong A B D C" 
    using not_cong_1243 by blast
  show "⋀l m P. isLine l ∧ isLine m ∧ IncidentL P l ∧ l =l= m ⟶ IncidentL P m" 
    using axiom_Incidl_morphism by blast
  show "⋀p q M. isPlane p ∧ isPlane q ∧ IncidentP M p ∧ p =p= q ⟶ IncidentP M q" 
    using axiom_Incidp_morphism by blast
  show "⋀P l. IncidentL P l ⟶ isLine l" 
    using IncidentL_def by blast
  show "⋀P p. IncidentP P p ⟶ isPlane p" 
    using IncidentP_def by blast
qed

interpretation Intrepretation_Hilbert_neutral_2D: Hilbert_neutral_2D
  where IncidL = IncidentL and 
    IncidP = IncidentP and
    EqL = EqTL and 
    EqP = EqTP and 
    IsL = isLine and 
    IsP = isPlane and
    BetH = Between_H and
    CongH = Cong and
    CongaH = CongA_H and
    PP = TPA and
    PQ = TPB and
    PR = TPC
proof
  {
    fix l A B C
    assume "isLine l" and
      "¬ Interpretation_Hilbert_neutral_dimensionless_pre.ColH A B C" and
      "¬ IncidentL C l" and
      "Interpretation_Hilbert_neutral_dimensionless_pre.cut l A B"
    have "¬ Col A B C" 
      by (meson Col_H_def Interpretation_Hilbert_neutral_dimensionless_pre.ColH_def 
          ‹¬ Interpretation_Hilbert_neutral_dimensionless_pre.ColH A B C› cols_coincide_2)
    have "cut_H l A B" 
      using Interpretation_Hilbert_neutral_dimensionless_pre.cut_def
        ‹Interpretation_Hilbert_neutral_dimensionless_pre.cut l A B› cut_H_def by auto
    hence "isLine l ∧ ¬ IncidentL A l ∧ ¬ IncidentL B l ∧ (∃ I. IncidentL I l ∧ Between_H A I B)"
      using cut_H_def by blast
    then obtain I where "IncidentL I l" and "Between_H A I B"
      by blast
    hence "Bet A I B ∧ A ≠ B ∧ B ≠ C ∧ A ≠ C" 
      using Between_H_def ‹¬ Col A B C› col_trivial_2 col_trivial_3 by force
    have "Coplanar A B (fst l) (snd l)" 
      using ‹cut_H l A B› cut_two_sides ncoplanar_perm_16 ts__coplanar by blast
    have "Col I (fst l) (snd l)" 
      using IncidentL_def ‹IncidentL I l› by auto
    let ?p = "Plane A B C"
    have "isPlane ?p" 
      using EqTP_def ‹¬ Col A B C› axiom_plane_existence cols_coincide incidentp_eqp by blast
    moreover have "IncidentP A ?p" 
      using IncidentP_def calculation coplanar_trivial by blast
    moreover have "IncidentP B ?p" 
      using IncidentP_def calculation(1) ncop_distincts by blast
    moreover have "IncidentP C ?p" 
      using IncidentP_def calculation(1) ncop_distincts by blast
    moreover have "IncidentLP l ?p"
    proof -
      have "isLine l" 
        by (simp add: ‹isLine l›)
      moreover have "isPlane ?p" 
        using ‹isPlane (Plane A B C)› by blast
      moreover 
      {
        fix AA
        assume "IncidentL AA l" 
        hence "Col AA (fst l) (snd l)" 
          by (simp add: incident_col)
        hence "Coplanar AA A (fst l) (snd l)" 
          using ncop__ncols by blast
        have "Coplanar AA B (fst l) (snd l)" 
          using ‹Col AA (fst l) (snd l)› ncop__ncols by blast
        have "Coplanar AA I (fst l) (snd l)" 
          using ‹Col I (fst l) (snd l)› ncop__ncols by blast
        have "isPlane ?p" 
          using ‹isPlane (Plane A B C)› by blast
        moreover 
        have "Coplanar AA A B C" 
          using all_coplanar by blast
        hence "∃ P Q R. ?p = Plane P Q R ∧ Coplanar AA P Q R" 
          by blast
        ultimately have "IncidentP AA ?p"
          using IncidentP_def by blast
      }
      hence "∀ A. IncidentL A l ⟶ IncidentP A ?p" 
        by blast
      ultimately show ?thesis
        using IncidentLP_def by blast
    qed
    moreover have "¬ IncidentL C l" 
      using ‹¬ IncidentL C l› by blast
    ultimately have "Interpretation_Hilbert_neutral_dimensionless_pre.cut l A C ∨
       Interpretation_Hilbert_neutral_dimensionless_pre.cut l B C" 
      by (meson IncidentLP_def Interpretation_Hilbert_neutral_dimensionless_pre.IncidLP_def 
          Intrepretation_Hilbert_neutral_dimensionless.pasch 
          ‹Interpretation_Hilbert_neutral_dimensionless_pre.cut l A B› 
          ‹¬ Interpretation_Hilbert_neutral_dimensionless_pre.ColH A B C›)
  }
  thus "⋀l A B C.
       isLine l ∧
       ¬ Interpretation_Hilbert_neutral_dimensionless_pre.ColH A B C ∧
       ¬ IncidentL C l ∧ Interpretation_Hilbert_neutral_dimensionless_pre.cut l A B ⟶
       Interpretation_Hilbert_neutral_dimensionless_pre.cut l A C ∨
       Interpretation_Hilbert_neutral_dimensionless_pre.cut l B C" 
    by blast
qed

end
end