Theory Tarski_Neutral_3D

(* IsaGeoCoq - Tarski_Neutral_3D

Port part of GeoCoq 3.4.0 (https://geocoq.github.io/GeoCoq/) in Isabelle/Hol 

Copyright (C) 2021-2025  Roland Coghetto roland.coghetto (at) cafr-msa2p.be

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_3D

imports
  Tarski_Neutral

begin

section "Tarski's axiom system for neutral geometry: 3D"

subsection "Definitions"

locale Tarski_neutral_3D = Tarski_neutral_dimensionless +
  fixes TS1 and TS2 and TS3 and TS4 
  assumes lower_dim_3: "¬ (∃ X.
   ((Bet TS1 TS2 X ∨ Bet TS2 X TS1 ∨ Bet X TS1 TS2) ∧ 
         (Bet TS3 TS4 X ∨ Bet TS4 X TS3 ∨ Bet X TS3 TS4) ∨
   (Bet TS1 TS3 X ∨ Bet TS3 X TS1 ∨ Bet X TS1 TS3) ∧ 
         (Bet TS2 TS4 X ∨ Bet TS4 X TS2 ∨ Bet X TS2 TS4) ∨
   (Bet TS1 TS4 X ∨ Bet TS4 X TS1 ∨ Bet X TS1 TS4) ∧ 
         (Bet TS2 TS3 X ∨ Bet TS3 X TS2 ∨ Bet X TS2 TS3)))"
  assumes upper_dim_3: "∀ A B C P Q R.
   P ≠ Q ∧ Q ≠ R ∧ P ≠ R ∧
   Cong A P A Q ∧ Cong B P B Q ∧ Cong C P C Q ∧
   Cong A P A R ∧ Cong B P B R ∧ Cong C P C R ⟶
   (Bet A B C ∨ Bet B C A ∨ Bet C A B)"

context Tarski_neutral_3D

begin

subsection "Propositions"

lemma not_coplanar_S1_S2_S3_S4:
  shows "¬ Coplanar TS1 TS2 TS3 TS4" 
proof -
  {
    assume "Coplanar TS1 TS2 TS3 TS4"
    then obtain X where "(Col TS1 TS2 X ∧ Col TS3 TS4 X) ∨
            (Col TS1 TS3 X ∧ Col TS2 TS4 X) ∨
            (Col TS1 TS4 X ∧ Col TS2 TS3 X)" 
      using Coplanar_def by auto
    hence False using lower_dim_3 Col_def by blast
  }
  thus ?thesis 
    by blast
qed

end
end