-
Notifications
You must be signed in to change notification settings - Fork 0
/
Gupta_Euclidean_Tarski_Model.thy
80 lines (65 loc) · 3.03 KB
/
Gupta_Euclidean_Tarski_Model.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
(* IsageoCoq2_R1
Gupta_Euclidean_Tarski_Model.thy
Version 2.2.0 IsaGeoCoq2_R1, Port part of GeoCoq 3.4.0
Copyright (C) 2021-2023 Roland Coghetto roland.coghetto ( a t ) cafr-msa2p.be
License: LGPGL
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_Tarski_Model
imports
Tarski_Euclidean
Gupta_Tarski_Model
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 "\<forall>a b. Cong a b b a"
by (simp add: cong_pseudo_reflexivity)
show "\<forall>a b p q r s. Cong a b p q \<and> Cong a b r s \<longrightarrow> Cong p q r s"
using cong_inner_transitivity by blast
show "\<forall>a b c. Cong a b c c \<longrightarrow> a = b"
using cong_diff by blast
show "\<forall>a b c q. \<exists>x. Bet q a x \<and> Cong a x b c"
using segment_construction by force
show "\<forall>a b c d a' b' c' d'. a \<noteq> b \<and> Bet a b c \<and> Bet a' b' c' \<and> Cong a b a' b' \<and>
Cong b c b' c' \<and> Cong a d a' d' \<and> Cong b d b' d' \<longrightarrow>
Cong c d c' d'"
using five_segment by blast
show "\<forall>a b c. Bet a b c \<longrightarrow> Bet c b a"
using between_symmetry by blast
show "\<forall>a b c d. Bet a b d \<and> Bet b c d \<longrightarrow> Bet a b c"
using between_inner_transitivity by blast
show "\<forall>a b c p q.
Bet a p c \<and> Bet b q c \<and> a \<noteq> p \<and> c \<noteq> p \<and> b \<noteq> q \<and> c \<noteq> q \<and>
\<not> (Bet a b c \<or> Bet b c a \<or> Bet c a b) \<longrightarrow>
(\<exists>x. Bet p x b \<and> Bet q x a)"
using inner_pasch by blast
show "\<not> (Bet TPA TPB TPC \<or> Bet TPB TPC TPA \<or> Bet TPC TPA TPB)"
by (simp add: lower_dim)
show "\<forall>A B C D T.
Bet A D T \<and>
Bet B D C \<and> B \<noteq> D \<and> D \<noteq> C \<and> \<not> (Bet A B C \<or> Bet B C A \<or> Bet C A B) \<longrightarrow>
(\<exists>x y. Bet A B x \<and> Bet A C y \<and> Bet x T y)"
using Bet_perm tarski_s_parallel_postulate_def tarski_s_parallel_postulate_thm by blast
qed
end
end