Theory Gupta_Euclidean_Model_Tarski_Euclidean

(* IsageoCoq - Gupta_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 Gupta_Euclidean_Model_Tarski_Euclidean

imports 
  Tarski_Euclidean
  Gupta_Euclidean

begin
 
context Tarski_Euclidean

begin

interpretation Interpretation_Gupta_euclidean : Gupta_Euclidean 
  where GPA = TPA and GPB = TPB and GPC = TPC and BetG = Bet and CongG = Cong 
proof
  show "∀a b. Cong a b b a" 
    by (simp add: cong_pseudo_reflexivity)
  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" 
    using cong_diff by blast
  show "∀a b c q. ∃x. Bet q a x ∧ Cong a x b c" 
    using segment_construction by force
  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 c. Bet a b c ⟶ Bet c b a" 
    using between_symmetry by blast
  show "∀a b c d. Bet a b d ∧ Bet b c d ⟶ Bet a b c" 
    using between_inner_transitivity by blast
  show "∀a b c p q.
       Bet a p c ∧ Bet b q c ∧ a ≠ p ∧ c ≠ p ∧ b ≠ q ∧ c ≠ q ∧ 
         ¬ (Bet a b c ∨ Bet b c a ∨ Bet c a b) ⟶
       (∃x. Bet p x b ∧ Bet q x a)" 
    using inner_pasch by blast
  show "¬ (Bet TPA TPB TPC ∨ Bet TPB TPC TPA ∨ Bet TPC TPA TPB)" 
    by (simp add: lower_dim)
  show "∀A B C D T.
        Bet A D T ∧
        Bet B D C ∧ B ≠ D ∧ D ≠ C ∧ ¬ (Bet A B C ∨ Bet B C A ∨ Bet C A B) ⟶
        (∃x y. Bet A B x ∧ Bet A C y ∧ Bet x T y)" 
    using Bet_perm tarski_s_parallel_postulate_def tarski_s_parallel_postulate_thm by blast
qed

end
end