Theory Tarski_Neutral_Model_Gupta_Neutral

(* IsageoCoq -  Tarski_Neutral_Model_Gupta_Neutral.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_Model_Gupta_Neutral

imports Gupta_Neutral

begin

context Gupta_neutral_dimensionless

begin

interpretation Interpretation_Tarski_neutral_dimensionless: Tarski_neutral_dimensionless 
where TPA = GPA and TPB = GPB and TPC = GPC and Bet = BetG and Cong = CongG 
proof 
show "∀a b. CongG a b b a" 
by (simp add: cong_pseudo_reflexivityG)
show "∀a b p q r s. CongG a b p q ∧ CongG a b r s ⟶ CongG p q r s" 
using cong_inner_transitivityG by blast
show "∀a b c. CongG a b c c ⟶ a = b" 
by (simp add: cong_identityG)
show "∀a b c q. ∃x. BetG q a x ∧ CongG a x b c" 
by (simp add: segment_constructionG)
show "∀a b c d a' b' c' d'. a ≠ b ∧ BetG a b c ∧ BetG a' b' c' ∧ 
CongG a b a' b' ∧ CongG b c b' c' ∧ CongG a d a' d' ∧ CongG b d b' d' ⟶
CongG c d c' d'" 
using five_segmentG by blast
show "∀a b. BetG a b a ⟶ a = b" 
by (simp add: between_identityT)
show "∀a b c p q. BetG a p c ∧ BetG b q c ⟶ (∃x. BetG p x b ∧ BetG q x a)" 
using inner_paschT by blast
show "¬ BetG GPA GPB GPC ∧ ¬ BetG GPB GPC GPA ∧ ¬ BetG GPC GPA GPB" 
using lower_dimG by blast
qed

subsection "Transport theorem from Tarski Neutral for Gupta Euclidean Model"

lemma g_l5_2: 
assumes "A ≠ B" and
"BetG A B C" and
"BetG A B D"
shows "BetG B C D ∨ BetG B D C" 
using Interpretation_Tarski_neutral_dimensionless.l5_2 assms(1) assms(2) assms(3) by blast

lemma g_l5_3:
assumes "BetG A B D" and
"BetG A C D"
shows "BetG A B C ∨ BetG A C B" 
using Interpretation_Tarski_neutral_dimensionless.l5_3 assms(1) assms(2) by blast

lemma g_between_exchange4:
assumes "BetG A B C" and
"BetG A C D"
shows "BetG A B D"
using assms(1) assms(2) 
Interpretation_Tarski_neutral_dimensionless.between_exchange4 by blast

lemma g_between_inner_transitivity:
assumes "BetG A B D" and
"BetG B C D"
shows "BetG A B C"
using assms(1) assms(2) 
Interpretation_Tarski_neutral_dimensionless.between_inner_transitivity by blast

lemma g_not_bet_distincts: 
assumes "¬ BetG A B C"
shows "A ≠ B ∧ B ≠ C"
using assms Interpretation_Tarski_neutral_dimensionless.not_bet_distincts by blast

lemma g_between_symmetry:
assumes "BetG A B C"
shows "BetG C B A"
using assms Interpretation_Tarski_neutral_dimensionless.between_symmetry by blast

lemma g_between_trivial:
shows "BetG A B B"
using Interpretation_Tarski_neutral_dimensionless.between_trivial by blast

end
end