Theory Hilbert_Euclidean_Model_Tarski_Euclidean

(* IsageoCoq - Hilbert_Euclidean_Model_Tarski_Euclidean.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_Euclidean_Model_Tarski_Euclidean

imports Hilbert_Euclidean

begin

section "Hilbert Euclidean - Tarski Euclidean Model"

subsection "Interpretation"

context Tarski_Euclidean

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 blast 
    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 Tarski_neutral_dimensionless.conga_refl 
          Tarski_neutral_dimensionless.not_col_distincts Tarski_neutral_dimensionless_axioms)
    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 Tarski_neutral_dimensionless.axiom_conga_permlr
        Tarski_neutral_dimensionless_axioms)
  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_euclidean: Hilbert_Euclidean
  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 
  show "∀ l P m1 m2. isLine l ∧ isLine m1 ∧ isLine m2 ∧
        ¬ IncidentL P l ∧ Interpretation_Hilbert_neutral_dimensionless_pre.Para l m1 ∧
        IncidentL P m1 ∧ Interpretation_Hilbert_neutral_dimensionless_pre.Para l m2 ∧ 
        IncidentL P m2 ⟶ m1 =l= m2" 
    using IncidentLP_def Interpretation_Hilbert_neutral_dimensionless_pre.IncidLP_def 
      Interpretation_Hilbert_neutral_dimensionless_pre.Para_def 
      Para_H_def axiom_euclid_uniqueness by force
qed

end
end