-
Notifications
You must be signed in to change notification settings - Fork 0
/
Highschool3.thy
77 lines (65 loc) · 2.69 KB
/
Highschool3.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
(* IsageoCoq2_R1
Highschool3.thy
Version 2.2.0 IsaGeoCoq2_R1, Port part of GeoCoq 3.4.0
Version 2.1.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 Highschool3
imports
Highschool2
Tarski_Euclidean_2D
begin
lemma (in Tarski_Euclidean_2D) NewEX1:
assumes "Square A B C D" and
"Cong K A K C" and
"Cong K A A C"
shows "Col B K D"
proof -
obtain M where "M Midpoint A C"
using MidR_uniq_aux by blast
have "Cong B A B C"
using Cong_cases Square_def assms(1) by auto
hence "Per A M B"
using Per_def \<open>M Midpoint A C\<close> l8_2 by blast
hence "A M Perp M B"
by (metis Square_def Square_not_triv_3 \<open>M Midpoint A C\<close> assms(1)
cong_diff_2 is_midpoint_id l8_7 midpoint_thales_reci per_perp rect_per)
have "Cong D A D C"
using Square_def assms(1)
by (meson Square_Rhombus cong_inner_transitivity not_cong_4312 rmb_cong)
hence "Per A M D"
using Per_def Per_perm \<open>M Midpoint A C\<close> cong_left_commutativity by blast
hence "A M Perp M D"
by (metis Cong_cases Square_def \<open>A M Perp M B\<close> \<open>M Midpoint A C\<close>
assms(1) between_cong between_trivial2 midpoint_cong
midpoint_thales_reci_2 per_perp rect_per)
moreover
have "Per A M K"
using Per_def \<open>M Midpoint A C\<close> assms(2) l8_2 by blast
hence "A M Perp M K"
by (metis \<open>A M Perp M B\<close> \<open>M Midpoint A C\<close> assms(3)
between_cong midpoint_bet midpoint_distinct_2
not_cong_2134 per_perp perp_distinct)
ultimately
show ?thesis
by (metis Col_def \<open>Cong B A B C\<close> \<open>Cong D A D C\<close> assms(2) assms(3)
cong_diff perp2__col perp_not_col upper_dim)
qed
end