-
Notifications
You must be signed in to change notification settings - Fork 0
/
Highschool2.thy
4699 lines (4534 loc) · 174 KB
/
Highschool2.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
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
(* IsageoCoq2_R1
Highschool2.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 Highschool2
imports
Tarski_Continuity_Neutral
Highschool1
Tarski_Euclidean
begin
section "Niveau école secondaire - Géométrie euclidienne, sans dimension"
context Tarski_Euclidean
begin
lemma triangle_mid_par_strict_cong_aux: (*midpoint_theorems a besoin de
quadrilaterals_inter_dec qui est dans isabel/hol quadrilaterals2*)
assumes "\<not> Col A B C" and
"P Midpoint B C" and
"Q Midpoint A C" and
"R Midpoint A B"
shows "A B ParStrict Q P \<and> Cong A R P Q \<and> Cong B R P Q"
proof -
have "Col B P C"
by (simp add: assms(2) bet_col midpoint_bet)
have "Col A Q C"
by (simp add: assms(3) bet_col midpoint_bet)
have "Col A R B"
using Midpoint_def assms(4) bet_col by blast
have "Cong B P C P"
using Midpoint_def assms(2) not_cong_1243 by blast
have "Cong A Q C Q"
using Midpoint_def assms(3) not_cong_1243 by blast
have "Cong A R B R"
using Midpoint_def assms(4) not_cong_1243 by blast
obtain x where "Q Midpoint P x"
using symmetric_point_construction by blast
hence "Cong P Q x Q"
using Cong_perm midpoint_cong by blast
have "Col P Q x"
by (meson \<open>Q Midpoint P x\<close> bet_col midpoint_bet)
{
assume "Col A P C"
hence "Col A B C"
by (metis \<open>Col B P C\<close> assms(2) col2__eq
col_permutation_5 midpoint_distinct_2)
hence False
using assms(1) by blast
}
hence "\<not> Col A P C"
by blast
hence "A \<noteq> P"
using col_trivial_1 by force
have "ParallelogramStrict A P C x"
using \<open>Q Midpoint P x\<close> \<open>\<not> Col A P C\<close> assms(3) mid_plgs by force
have "Cong A P C x"
by (metis l7_13 \<open>Q Midpoint P x\<close> assms(3) cong_4321)
have "Cong A x P C"
by (metis l7_13 \<open>Q Midpoint P x\<close> assms(3) l7_2 not_cong_2134)
have "Cong A x B P"
by (meson \<open>Cong A x P C\<close> \<open>Cong B P C P\<close> cong_4312 cong_inner_transitivity)
have "A x Par B P"
by (metis (full_types) Par_cases \<open>A \<noteq> P\<close> \<open>Col B P C\<close> \<open>Cong A P C x\<close>
\<open>ParallelogramStrict A P C x\<close> \<open>Q Midpoint P x\<close> assms(2) assms(3)
col_par l12_17 l12_20 midpoint_distinct_1 par_not_par plgs_two_sides)
have "Parallelogram A x B P \<or> Parallelogram A x P B"
using par_cong_plg_2 by (simp add: \<open>A x Par B P\<close> \<open>Cong A x B P\<close>)
hence "Cong A R P Q"
by (metis Cong_cases \<open>Col A Q C\<close> \<open>Col A R B\<close> \<open>Q Midpoint P x\<close>
assms(1) assms(4) col_transitivity_1 cong_cong_half_1 l7_17_bis
midpoint_distinct_3 plg_cong_2 plg_mid_2)
moreover
have "Cong B R P Q"
using \<open>Cong A R B R\<close> calculation cong_inner_transitivity by blast
ultimately
show ?thesis
using assms(1) assms(2) assms(3) triangle_mid_par_strict by blast
qed
lemma triangle_par_mid:
assumes "\<not> Col A B C" and
"P Midpoint B C" and
"A B Par Q P" and
"Col Q A C"
shows "Q Midpoint A C"
proof -
have "playfair_s_postulate \<longrightarrow> midpoint_converse_postulate"
using playfair_s_postulate_implies_midpoint_converse_postulate by blast
thus ?thesis
using assms(1) assms(2) assms(3) assms(4) midpoint_converse_postulate_def
not_col_permutation_2 parallel_uniqueness playfair_s_postulate_def by blast
qed
lemma triangle_mid_par_strict_cong_1:
assumes "\<not> Col A B C" and
"P Midpoint B C" and
"Q Midpoint A C" and
"R Midpoint A B"
shows "A B ParStrict Q P \<and> Cong A R P Q"
using assms(1) assms(2) assms(3) assms(4) triangle_mid_par_strict_cong_aux by blast
lemma triangle_mid_par_strict_cong_2:
assumes "\<not> Col A B C" and
"P Midpoint B C" and
"Q Midpoint A C" and
"R Midpoint A B"
shows "A B ParStrict Q P \<and> Cong B R P Q"
using assms(1) assms(2) assms(3) assms(4) triangle_mid_par_strict_cong_aux by blast
lemma triangle_mid_par_strict_cong_simp:
assumes "\<not> Col A B C" and
"P Midpoint B C" and
"Q Midpoint A C"
shows "A B ParStrict Q P"
using assms(1) assms(2) assms(3) triangle_mid_par_strict by blast
lemma triangle_mid_par_strict_cong:
assumes "\<not> Col A B C" and
"P Midpoint B C" and
"Q Midpoint A C" and
"R Midpoint A B"
shows "A B ParStrict Q P \<and> A C ParStrict P R \<and>
B C ParStrict Q R \<and> Cong A R P Q \<and>
Cong B R P Q \<and> Cong A Q P R \<and>
Cong C Q P R \<and> Cong B P Q R \<and> Cong C P Q R"
by (meson assms(1) assms(2) assms(3) assms(4) l7_2 not_col_permutation_1
not_col_permutation_5 par_strict_right_comm triangle_mid_par_strict_cong_aux)
lemma triangle_mid_par_flat_cong_aux:
assumes "A \<noteq> B" and
"Col A B C" and
"P Midpoint B C" and
"Q Midpoint A C" and
"R Midpoint A B"
shows "A B Par Q P \<and> Cong A R P Q \<and> Cong B R P Q"
proof (cases "A = C")
case True
thus ?thesis
by (metis Cong_cases assms(1) assms(3) assms(4) assms(5)
cong_cong_half_1 l7_17_bis l8_20_2 mid_par_cong2
midpoint_col not_col_permutation_2 not_par_not_col)
next
case False
show ?thesis
proof (cases "B = C")
case True
thus ?thesis
by (metis assms(1) assms(2) assms(3) assms(4) assms(5) col_transitivity_1
col_trivial_3 cong_inner_transitivity cong_right_commutativity
l7_17 l7_2 midpoint_col midpoint_cong midpoint_distinct_2
not_par_inter_uniqueness)
next
case False
hence "B \<noteq> C"
by blast
show ?thesis
proof (cases "A = P")
case True
hence "Col A B Q"
by (metis assms(2) assms(4) col2__eq midpoint_col
midpoint_distinct_2 not_col_permutation_4)
have "A B Par Q A"
by (metis True \<open>Col A B Q\<close> assms(1) assms(3) assms(4) midpoint_distinct_1
not_par_not_col par_right_comm)
moreover have "Cong A R A Q"
by (metis True assms(1) assms(3) assms(4) assms(5)
cong_cong_half_1 l7_3_2 mid_par_cong1)
moreover have "Cong B R A Q"
by (metis True assms(3) assms(4) assms(5) cong_cong_half_1 l7_2 midpoint_cong)
ultimately show ?thesis
using True by force
next
case False
obtain x where "Q Midpoint P x"
using symmetric_point_construction by blast
show ?thesis
proof (cases "P = x")
case True
thus ?thesis
by (metis \<open>Q Midpoint P x\<close> assms(1) assms(3) assms(4) l8_20_2 sym_preserve_diff)
next
case False
hence "Parallelogram A P C x"
using \<open>Q Midpoint P x\<close> assms(4) mid_plg by blast
hence "Cong A x B P"
by (meson assms(3) cong_symmetry cong_transitivity midpoint_cong plg_cong_2)
have "P Q Par A B "
proof -
have "P \<noteq> Q"
using False \<open>Q Midpoint P x\<close> is_midpoint_id by fastforce
moreover have "Col P x Q"
using \<open>Q Midpoint P x\<close> col_permutation_1 midpoint_col by blast
have "Parallelogram A x B P \<or> Parallelogram A x P B"
proof -
have "Cong A x B P"
using \<open>Cong A x B P\<close> by auto
moreover
have "A x Par B P"
proof -
{
assume "B = P"
hence "B = C"
using Midpoint_def assms(3) cong_diff_3 by blast
hence False using \<open>B\<noteq> C\<close> by blast
}
moreover have "A x Par P C"
by (metis \<open>B \<noteq> C\<close> \<open>Q Midpoint P x\<close> assms(3)
assms(4) mid_par_cong mid_par_cong2
midpoint_cong_uniqueness midpoint_distinct_1
not_col_distincts par_right_comm)
moreover have "Col P C B"
using assms(3) col_permutation_5 midpoint_col by blast
moreover have "Col P C P"
by (simp add: col_trivial_3)
ultimately show ?thesis
using par_col2_par by blast
qed
ultimately show ?thesis
using par_cong_plg_2 by blast
qed
moreover
have "P x Par A B"
proof -
have "Parallelogram A x B P \<or> Parallelogram A x P B"
by (simp add: calculation(2))
moreover
have "Parallelogram A x B P \<longrightarrow> P x Par A B"
by (metis Par_cases \<open>Q Midpoint P x\<close> assms(1) assms(3) assms(4) assms(5)
l12_17 l7_17_bis l8_20_2 midpoint_distinct_1 plg_mid_2)
moreover
have "Parallelogram A x P B \<longrightarrow> P x Par A B"
by (metis False Plg_perm \<open>Parallelogram A x B P \<longrightarrow> P x Par A B\<close> plg_par)
ultimately show ?thesis
by blast
qed
ultimately show ?thesis
using \<open>Col P x Q\<close> par_col_par_2 by blast
qed
hence "A B Par Q P"
using Par_cases by auto
moreover
have "Cong P Q A R"
proof -
have "Parallelogram A x B P \<longrightarrow> Cong P Q A R"
by (metis Plg_perm \<open>B \<noteq> C\<close> \<open>Parallelogram A P C x\<close> plg_uniqueness)
moreover
have "Parallelogram A x P B \<longrightarrow> Cong P Q A R"
by (meson \<open>Q Midpoint P x\<close> assms(5) cong_cong_half_1 not_cong_3421 plg_cong_2)
moreover
have "Parallelogram A x B P \<or> Parallelogram A x P B"
proof -
have "Cong A x B P"
using \<open>Cong A x B P\<close> by auto
moreover
have "A x Par B P"
proof -
{
assume "B = P"
hence "B = C"
using Midpoint_def assms(3) cong_diff_3 by blast
hence False using \<open>B\<noteq> C\<close> by blast
}
moreover have "A x Par P C"
by (metis Par_cases \<open>Q Midpoint P x\<close> assms(3)
assms(4) calculation is_midpoint_id_2
l12_17 l7_2)
moreover have "Col P C B"
using assms(3) col_permutation_5 midpoint_col by blast
moreover have "Col P C P"
by (simp add: col_trivial_3)
ultimately show ?thesis
using par_col2_par by blast
qed
ultimately show ?thesis
using par_cong_plg_2 by blast
qed
ultimately show ?thesis
by blast
qed
hence "Cong A R P Q"
using cong_symmetry by presburger
moreover have "Cong B R P Q"
using assms(5) calculation(2) cong_transitivity
midpoint_cong not_cong_3421 by blast
ultimately show ?thesis
by blast
qed
qed
qed
qed
lemma triangle_mid_par_flat_cong_1:
assumes "A \<noteq> B" and
"Col A B C" and
"P Midpoint B C" and
"Q Midpoint A C" and
"R Midpoint A B"
shows "A B Par Q P \<and> Cong A R P Q"
using assms(1) assms(2) assms(3) assms(4) assms(5)
triangle_mid_par_flat_cong_aux by blast
lemma triangle_mid_par_flat_cong_2:
assumes "A \<noteq> B" and
"Col A B C" and
"P Midpoint B C" and
"Q Midpoint A C" and
"R Midpoint A B"
shows "A B Par Q P \<and> Cong B R P Q"
using assms(1) assms(2) assms(3) assms(4) assms(5)
triangle_mid_par_flat_cong_aux by blast
lemma triangle_mid_par_flat_cong:
assumes "A \<noteq> B" and
"A \<noteq> C" and
"B \<noteq> C" and
"Col A B C" and
"P Midpoint B C" and
"Q Midpoint A C" and
"R Midpoint A B"
shows "A B Par Q P \<and> A C Par P R \<and> B C Par Q R \<and>
Cong A R P Q \<and> Cong B R P Q \<and> Cong A Q P R \<and>
Cong C Q P R \<and> Cong B P Q R \<and> Cong C P Q R"
by (meson assms(1) assms(2) assms(3) assms(4) assms(5)
assms(6) assms(7) l7_2 not_col_permutation_2
not_col_permutation_5 par_right_comm triangle_mid_par_flat_cong_aux)
lemma triangle_mid_par_flat:
assumes "A \<noteq> B" and
"Col A B C" and
"P Midpoint B C" and
"Q Midpoint A C"
shows "A B Par Q P"
using assms(1) assms(2) assms(3) assms(4) midpoint_existence
triangle_mid_par_flat_cong_aux by blast
lemma triangle_mid_par:
assumes "A \<noteq> B" and
"P Midpoint B C" and
"Q Midpoint A C"
shows "A B Par Q P"
proof (cases "Col A B C")
case True
thus ?thesis
using assms(1) assms(2) assms(3) triangle_mid_par_flat by blast
next
case False
hence "A B ParStrict Q P"
by (simp add: assms(2) assms(3) triangle_mid_par_strict_cong_simp)
thus ?thesis
using Par_def by blast
qed
lemma triangle_mid_par_cong:
assumes "A \<noteq> B" and
"A \<noteq> C" and
"B \<noteq> C" and
"P Midpoint B C" and
"Q Midpoint A C" and
"R Midpoint A B"
shows "A B Par Q P \<and> A C Par P R \<and> B C Par Q R \<and>
Cong A R P Q \<and> Cong B R P Q \<and> Cong A Q P R \<and>
Cong C Q P R \<and> Cong B P Q R \<and> Cong C P Q R"
proof (cases "Col A B C")
case True
thus ?thesis
using assms(1) assms(2) assms(3) assms(4) assms(5) assms(6)
triangle_mid_par_flat_cong by blast
next
case False
have "A B ParStrict Q P \<and> A C ParStrict P R \<and>
B C ParStrict Q R \<and> Cong A R P Q \<and> Cong B R P Q \<and>
Cong A Q P R \<and> Cong C Q P R \<and> Cong B P Q R \<and> Cong C P Q R"
using triangle_mid_par_strict_cong False assms(4) assms(5) assms(6) by blast
thus ?thesis
using par_strict_par by presburger
qed
lemma triangle_mid_par_cong_1:
assumes "B \<noteq> C" and
"P Midpoint B C" and
"Q Midpoint A C" and
"R Midpoint A B"
shows "B C Par Q R \<and> Cong B P Q R"
proof (cases "Col A B C")
case True
thus ?thesis
by (meson assms(1) assms(2) assms(3) assms(4) col_permutation_1
l7_2 par_right_comm triangle_mid_par_flat_cong_aux)
next
case False
thus ?thesis
using assms(2) assms(3) assms(4) not_col_distincts
triangle_mid_par_cong by blast
qed
lemma midpoint_thales:
assumes "\<not> Col A B C" and
"P Midpoint A B" and
"Cong P A P C"
shows "Per A C B"
using assms(1) assms(2) assms(3) cong_sac__per
hypothesis_of_right_saccheri_quadrilaterals_def
plg_cong sac_plg t22_17__rah by blast
lemma midpoint_thales_reci:
assumes "Per A C B" and
"P Midpoint A B"
shows "Cong P A P B \<and> Cong P B P C"
proof (cases "Col A B C")
case True
thus ?thesis
by (metis Cong_cases assms(1) assms(2) cong_pseudo_reflexivity
l8_9 midpoint_cong not_col_permutation_5)
next
case False
have "Cong P A P B"
using Midpoint_def assms(2) not_cong_2134 by blast
moreover
have "Cong P B P C"
proof -
obtain X where "X Midpoint A C"
using MidR_uniq_aux by blast
hence "C B Par X P"
by (meson False Mid_cases assms(2) col_permutation_3
par_strict_par triangle_mid_par_strict_cong_simp)
have "C B Perp C A"
by (metis False Perp_perm assms(1) not_col_distincts per_perp)
have "Coplanar X P C A"
by (meson \<open>X Midpoint A C\<close> bet__coplanar coplanar_perm_11 midpoint_bet)
hence "X P Perp C A"
using \<open>C B Par X P\<close> \<open>C B Perp C A\<close> cop_par_perp__perp by blast
hence "C X Perp P X"
by (metis Perp_cases \<open>X Midpoint A C\<close> col_per_perp l8_16_1
midpoint_col midpoint_distinct_2 not_col_distincts
not_col_permutation_2)
hence "Per P X C"
using Perp_perm perp_per_2 by blast
thus ?thesis
by (meson \<open>X Midpoint A C\<close> calculation cong_symmetry
cong_transitivity l7_2 per_double_cong)
qed
ultimately
show ?thesis
by simp
qed
lemma midpoint_thales_reci_1:
assumes "Per A C B" and
"P Midpoint A B"
shows "Cong P A P B"
using midpoint_thales_reci assms(1) assms(2) by blast
lemma midpoint_thales_reci_2:
assumes "Per A C B" and
"P Midpoint A B"
shows "Cong P B P C"
using midpoint_thales_reci assms(1) assms(2) by blast
lemma Per_mid_rectangle:
assumes "A \<noteq> B" and
"B \<noteq> C" and
"Per B A C" and
"I Midpoint B C" and
"J Midpoint A C" and
"K Midpoint A B"
shows "Rectangle A J I K"
proof (cases "A = C")
case True
thus ?thesis
by (metis Rectangle_triv assms(1) assms(4) assms(5) assms(6) l7_17_bis l8_20_2)
next
case False
have H1: "A B Par J I \<and> A C Par I K \<and> B C Par J K \<and>
Cong A K I J \<and> Cong B K I J \<and> Cong A J I K \<and>
Cong C J I K \<and> Cong B I J K \<and> Cong C I J K"
using False assms(1) assms(2) assms(4) assms(5) assms(6)
triangle_mid_par_cong by blast
have "Plg A J I K"
proof (cases "Col A B C")
case True
thus ?thesis
using False assms(1) assms(3) col_permutation_2 l8_2 l8_9 by blast
next
case False
hence "\<not> Col A B C"
by simp
have "A B ParStrict J I \<and> A C ParStrict I K \<and>
B C ParStrict J K \<and> Cong A K I J \<and> Cong B K I J \<and>
Cong A J I K \<and> Cong C J I K \<and> Cong B I J K \<and> Cong C I J K"
using False assms(4) assms(5) assms(6) triangle_mid_par_strict_cong by blast
hence "A J ParStrict I K"
by (metis Col_perm assms(5) midpoint_col midpoint_distinct_1
par_strict_col_par_strict par_strict_symmetry)
moreover
have "A K Par J I"
by (metis Col_def Midpoint_def H1 assms(1) assms(6) cong_diff_3
not_par_not_col par_trans)
ultimately
show ?thesis
using pars_par_plg by blast
qed
moreover
have "Per K A J"
proof -
have "Per C A B"
by (simp add: assms(3) l8_2)
moreover
have "Col A C J"
using assms(5) col_permutation_1 midpoint_col by blast
moreover
have "Col A B K"
using assms(6) col_permutation_1 midpoint_col by blast
ultimately
show ?thesis
by (metis False assms(1) l8_2 per_col)
qed
hence "Per K A J \<or> Per I J A \<or> Per A K I \<or> Per J I K"
by blast
ultimately
show ?thesis
by (simp add: plg_per_rect)
qed
(** This is the usual proof presented in classroom based on
the midpoint theorem but this proof suffers from two problems.
It needs the fact that IJK are not collinear,
which is not always the case when the quadrilateral is not convex.
It also needs the fact that A is different from C, and B is different from D.
The original proof by Varignon suffer from the same problem.
The original proof can be found page 138, Corollary IV:
http://polib.univ-lille3.fr/documents/B590092101_000000011.489_IMT.pdf
*)
lemma varignon:
assumes "A \<noteq> C" and
"B \<noteq> D" and
"\<not> Col I J K" and
"I Midpoint A B" and
"J Midpoint B C" and
"K Midpoint C D" and
"L Midpoint A D"
shows "Parallelogram I J K L"
proof -
have "I L Par J K"
proof -
have "I L Par B D"
by (metis Mid_cases Par_perm assms(2) assms(4) assms(7) triangle_mid_par)
moreover
have "J K Par B D"
by (meson Mid_cases assms(2) assms(5) assms(6) par_symmetry triangle_mid_par)
ultimately
show ?thesis
using not_par_one_not_par by blast
qed
moreover
have "I J Par K L"
proof -
have "I J Par A C"
by (meson Mid_cases assms(1) assms(4) assms(5) par_symmetry triangle_mid_par)
moreover
have "L K Par A C"
by (meson assms(1) assms(6) assms(7) par_symmetry triangle_mid_par)
ultimately
show ?thesis
by (meson not_par_one_not_par par_left_comm)
qed
ultimately
show ?thesis
by (simp add: assms(3) par_2_plg)
qed
lemma varignon_aux_aux:
assumes "A \<noteq> C" and
"J \<noteq> L" and
"I Midpoint A B" and
"J Midpoint B C" and
"K Midpoint C D" and
"L Midpoint A D"
shows "Parallelogram I J K L"
proof (cases "B = D")
case True
thus ?thesis
by (metis assms(2) assms(3) assms(4) assms(5) assms(6)
l7_17 l7_17_bis plg_trivial)
next
case False
obtain X where "X Midpoint B D"
using MidR_uniq_aux by blast
have "B D Par L I \<and> Cong B X L I"
using False \<open>X Midpoint B D\<close> assms(3) assms(6)
triangle_mid_par_cong_1 by blast
have "B D Par K J \<and> Cong B X K J"
using False \<open>X Midpoint B D\<close> triangle_mid_par_cong_1 assms(4)
assms(5) l7_2 by blast
have "I L Par J K"
using Par_cases \<open>B D Par K J \<and> Cong B X K J\<close> \<open>B D Par L I \<and> Cong B X L I\<close>
not_par_one_not_par by blast
have "Cong I L J K"
by (meson \<open>B D Par K J \<and> Cong B X K J\<close> \<open>B D Par L I \<and> Cong B X L I\<close>
cong_inner_transitivity cong_right_commutativity)
obtain X' where "X' Midpoint A C"
using MidR_uniq_aux by blast
have "A C Par J I \<and> Cong A X' J I"
using False \<open>X' Midpoint A C\<close> triangle_mid_par_cong_1 assms(1)
assms(3) assms(4) l7_2 by blast
have "A C Par K L \<and> Cong A X' K L"
using False \<open>X' Midpoint A C\<close> triangle_mid_par_cong_1 assms(1)
assms(5) assms(6) l7_2 by blast
have "I J Par K L"
using Par_cases \<open>A C Par J I \<and> Cong A X' J I\<close> \<open>A C Par K L \<and> Cong A X' K L\<close>
not_par_one_not_par by blast
have "Cong I J K L"
by (meson \<open>A C Par J I \<and> Cong A X' J I\<close> \<open>A C Par K L \<and> Cong A X' K L\<close>
cong_inner_transitivity cong_right_commutativity)
thus ?thesis
by (meson Cong_cases \<open>Cong I L J K\<close> \<open>I J Par K L\<close> \<open>I L Par J K\<close>
assms(2) par_par_cong_cong_parallelogram par_symmetry)
qed
lemma varignon_aux:
assumes (*"A \<noteq> C \<or> B \<noteq> D" and*)
"J \<noteq> L" and
"I Midpoint A B" and
"J Midpoint B C" and
"K Midpoint C D" and
"L Midpoint A D"
shows "Parallelogram I J K L"
by (metis assms(2) assms(3) assms(4) assms(5) assms(1) l7_17
l7_17_bis plg_trivial1 varignon_aux_aux)
lemma varignon_bis:
assumes "A \<noteq> C \<or> B \<noteq> D" and
"I Midpoint A B" and
"J Midpoint B C" and
"K Midpoint C D" and
"L Midpoint A D"
shows "Parallelogram I J K L"
proof -
have "Bet A I B"
using assms(2) midpoint_bet by blast
have "Cong A I I B"
by (simp add: assms(2) midpoint_cong)
have "Bet B J C"
using assms(3) midpoint_bet by blast
have "Cong B J J C"
by (simp add: assms(3) midpoint_cong)
have "Bet C K D"
using assms(4) midpoint_bet by blast
have "Cong C K K D"
by (simp add: assms(4) midpoint_cong)
have "Bet A L D"
using assms(5) midpoint_bet by blast
have "Cong A L L D"
by (simp add: assms(5) midpoint_cong)
show "Parallelogram I J K L"
proof (cases "J = L")
case True
hence "J = L"
by auto
have "ParallelogramFlat I J K L"
proof -
obtain X where "X Midpoint B D"
using MidR_uniq_aux by blast
have "Cong B X X D"
using \<open>X Midpoint B D\<close> midpoint_cong by auto
have "Bet B X D"
by (simp add: \<open>X Midpoint B D\<close> midpoint_bet)
have "Cong K C K D"
using \<open>Cong C K K D\<close> not_cong_2134 by blast
have "Col I L K \<and> Col I L L \<and> Cong I L K L \<and> (I \<noteq> K \<or> L \<noteq> L)"
proof (cases "A = B")
case True
hence "I = A \<and> I = B"
using assms(2) l8_20_2 by blast
hence "C = D"
using \<open>J = L\<close> \<open>A = B\<close> assms(3) assms(5) symmetric_point_uniqueness by blast
hence "K = C"
using \<open>Bet C K D\<close> bet_neq12__neq by blast
hence "K = D"
using \<open>C = D\<close> by auto
have "X = L"
using True \<open>X Midpoint B D\<close> assms(5) l7_17 by blast
have "X Midpoint I K"
using assms(5) by (simp add: \<open>I = A \<and> I = B\<close> \<open>K = D\<close> \<open>X = L\<close>)
hence "Cong X I X K"
by (meson midpoint_cong not_cong_2134)
have "I \<noteq> K \<or> L \<noteq> L"
using \<open>I = A \<and> I = B\<close> \<open>K = C\<close> \<open>K = D\<close> assms(1) by blast
thus ?thesis
using \<open>Cong X I X K\<close> \<open>X = L\<close> \<open>X Midpoint I K\<close> col_permutation_4
col_trivial_2 midpoint_col not_cong_2143 by blast
next
case False
hence "A \<noteq> B"
by auto
show ?thesis
proof (cases "A = D")
case True
hence "X Midpoint L B"
using True \<open>X Midpoint B D\<close> assms(2) assms(5) l7_17_bis l8_20_2 by blast
have "A = L \<and> L = D"
using True \<open>Bet A L D\<close> bet_neq12__neq by blast
have "L \<noteq> C \<or> B \<noteq> L"
using False True \<open>Bet A L D\<close> bet_neq12__neq by blast
have "L Midpoint B C"
using \<open>J = L\<close> assms(3) by auto
have "Cong K C K L"
using \<open>A = L \<and> L = D\<close> \<open>Cong K C K D\<close> by blast
have "K Midpoint C L"
using \<open>A = L \<and> L = D\<close> assms(4) by force
have "Cong X L X B"
using Cong_cases \<open>A = L \<and> L = D\<close> \<open>Cong B X X D\<close> by blast
have "L \<noteq> B"
using False \<open>A = L \<and> L = D\<close> by auto
have "B \<noteq> C"
using \<open>Bet B J C\<close> \<open>J = L\<close> \<open>L \<noteq> B\<close> bet_neq12__neq by blast
show ?thesis
proof (cases "X = K")
case True
hence "X = K"
by auto
thus ?thesis
using \<open>A = L \<and> L = D\<close> \<open>J = L\<close> \<open>L \<noteq> B\<close> \<open>X Midpoint L B\<close>
assms(3) assms(4) l7_9_bis midpoint_distinct_3 by blast
next
case False
hence "X \<noteq> K"
by auto
have "C \<noteq> L"
using \<open>B \<noteq> C\<close> \<open>L Midpoint B C\<close> is_midpoint_id_2 by blast
hence "B L Par L K \<and> B C Par K X \<and> L C Par L X \<and>
Cong B X K L \<and> Cong L X K L \<and> Cong B L K X \<and>
Cong C L K X \<and> Cong L K L X \<and> Cong C K L X"
by (metis \<open>B \<noteq> C\<close> \<open>K Midpoint C L\<close> \<open>L Midpoint B C\<close> \<open>L \<noteq> B\<close>
\<open>X Midpoint B D\<close> assms(4) mid_par_cong par_distincts
symmetric_point_construction triangle_mid_par_cong)
hence "Cong X L K L"
using Cong_cases by blast
moreover
have "Col X L K"
by (metis Bet_cases \<open>A = L \<and> L = D\<close>
\<open>B L Par L K \<and> B C Par K X \<and> L C Par L X \<and>
Cong B X K L \<and> Cong L X K L \<and> Cong B L K X \<and>
Cong C L K X \<and> Cong L K L X \<and> Cong C K L X\<close>
assms(4) bet_col col_cong2_bet1 midpoint_bet par_id_1)
moreover
have "Col X L L"
using col_trivial_2 by auto
have "X \<noteq> K \<or> K \<noteq> K"
by (simp add: False)
moreover
have "X = I"
using \<open>A = L \<and> L = D\<close> \<open>X Midpoint L B\<close> assms(2) l7_17 by blast
hence "Cong I L K L"
using calculation(1) by auto
ultimately
show ?thesis
using \<open>Col X L L\<close> \<open>X = I\<close> by fastforce
qed
next
case False
hence "A \<noteq> D"
by simp
show ?thesis
proof (cases "B = D")
case True
hence "B = D"
by simp
thus ?thesis
using \<open>J = L\<close> assms(1) assms(3) assms(5) l7_9_bis by force
next
case False
hence "B \<noteq> D"
by simp
have H1: "A B Par L X \<and> A D Par X I \<and> B D Par L I \<and>
Cong A I X L \<and> Cong B I X L \<and> Cong A L X I \<and>
Cong D L X I \<and> Cong B X L I \<and> Cong D X L I"
using triangle_mid_par_flat_cong False \<open>A \<noteq> B\<close> \<open>A \<noteq> D\<close>
\<open>X Midpoint B D\<close> assms(2) assms(5) triangle_mid_par_cong by blast
hence "L Midpoint I K"
proof (cases "C = D")
case True
thus ?thesis
using \<open>A \<noteq> B\<close> \<open>J = L\<close> assms(3) assms(5) l7_9 by blast
next
case False
hence "C \<noteq> D"
by simp
show ?thesis
proof (cases "B = C")
case True
show ?thesis
proof -
have "I \<noteq> X"
using H1 par_neq2 by blast
moreover have "Col I L X"
by (metis H1 True \<open>Bet B X D\<close> \<open>J = L\<close> assms(3) bet_col
between_symmetry col_cong2_bet1 l8_20_2 par_id_1)
moreover have "Cong I L L X"
by (metis True H1 \<open>J = L\<close> assms(3)
midpoint_distinct_2 not_cong_3421)
ultimately show ?thesis
using MidR_uniq_aux True \<open>X Midpoint B D\<close>
assms(4) cong_col_mid by blast
qed
next
case False
hence "B \<noteq> C"
by simp
have H2: "B C Par X K \<and> B D Par K L \<and> C D Par X L \<and>
Cong B L K X \<and> Cong C L K X \<and> Cong B X K L \<and>
Cong D X K L \<and> Cong C K X L \<and> Cong D K X L"
using triangle_mid_par_flat_cong False True \<open>B \<noteq> D\<close> \<open>C \<noteq> D\<close>
\<open>X Midpoint B D\<close> assms(3) assms(4) triangle_mid_par_cong by blast
show ?thesis
proof (cases "I = K")
case True
hence "I = K"
by simp
have "Parallelogram A D B C"
using mid_plg True \<open>A \<noteq> B\<close> assms(2) assms(4) l7_2 by blast
hence "Parallelogram B D A C"
by (meson Plg_perm)
moreover
have "Parallelogram A B D C"
using \<open>A \<noteq> D\<close> \<open>J = L\<close> assms(3) assms(5) mid_plg by blast
hence "Parallelogram B D C A"
using Plg_perm by blast
ultimately
have False
using \<open>B \<noteq> D\<close> plg_not_comm_1 by blast
thus ?thesis
by blast
next
case False
hence "I \<noteq> K"
by auto
moreover
have "I L Par K L"
proof -
have "I L Par B D"
using Par_perm H1 by blast
moreover
have "B D Par K L"
using H2 by blast
ultimately
show ?thesis
using par_not_par by blast
qed
hence "Col I L K"
using par_comm par_id_1 by blast
moreover
have "Cong I L L K"
by (meson H1 H2 cong_inner_transitivity not_cong_4321)
ultimately
show ?thesis
using cong_col_mid by blast
qed
qed
qed
thus ?thesis
by (metis Cong_cases False H1 col_permutation_4
col_trivial_2 cong_diff midpoint_col midpoint_cong
midpoint_distinct_3)
qed
qed
qed
thus ?thesis
using ParallelogramFlat_def True by blast
qed
thus ?thesis
by (metis Mid_cases ParallelogramFlat_def assms(2) assms(3) assms(4)
assms(5) plg_comm2 varignon_aux)
next
case False
thus ?thesis
using assms(2) assms(3) assms(4) assms(5) varignon_aux by blast
qed
qed
lemma quadrileral_midpoints:
assumes "\<not> Col I J K" and
"I Midpoint A B" and
"J Midpoint B C" and
"K Midpoint C D" and
"L Midpoint A D" and
"X Midpoint I K" and
"Y Midpoint J L"
shows "X = Y"
proof -
have "Parallelogram I J K L"
by (metis assms(1) assms(2) assms(3) assms(4) assms(5) l7_17
not_col_distincts varignon_bis)
hence "X Midpoint J L"
using assms(6) plg_mid_2 by blast
thus ?thesis
using assms(7) l7_17 by blast
qed
definition IsCircumcenter ::
"[TPoint,TPoint,TPoint,TPoint] \<Rightarrow> bool"
("_ IsCircumcenter _ _ _" [99,99,99,99] 50)
where
"G IsCircumcenter A B C \<equiv>
Cong A G B G \<and>
Cong B G C G \<and>
Coplanar G A B C"
lemma is_circumcenter_coplanar:
assumes "G IsCircumcenter A B C"
shows "Coplanar G A B C"
using IsCircumcenter_def assms by blast
lemma circumcenter_cong_1:
assumes "G IsCircumcenter A B C"
shows "Cong A G B G"
using IsCircumcenter_def assms by blast
lemma circumcenter_cong_2:
assumes "G IsCircumcenter A B C"
shows "Cong B G C G"
using IsCircumcenter_def assms by blast
lemma circumcenter_cong_3:
assumes "G IsCircumcenter A B C"
shows "Cong C G A G"
by (meson assms circumcenter_cong_1 circumcenter_cong_2
cong_4312 cong_transitivity)
lemma circumcenter_cong:
assumes "G IsCircumcenter A B C"
shows "Cong A G B G \<and> Cong B G C G \<and> Cong C G A G"
by (meson assms circumcenter_cong_1 circumcenter_cong_2 circumcenter_cong_3)
lemma is_circumcenter_perm_1:
assumes "G IsCircumcenter A B C"
shows"G IsCircumcenter A C B"
by (meson IsCircumcenter_def assms circumcenter_cong_3
cong_transitivity coplanar_perm_1)
lemma is_circumcenter_perm_2:
assumes "G IsCircumcenter A B C"
shows"G IsCircumcenter B A C"
using Cong_cases IsCircumcenter_def assms circumcenter_cong_3
coplanar_perm_2 by metis
lemma is_circumcenter_perm_3:
assumes "G IsCircumcenter A B C"
shows"G IsCircumcenter B C A"
using assms is_circumcenter_perm_1 is_circumcenter_perm_2 by blast
lemma is_circumcenter_perm_4:
assumes "G IsCircumcenter A B C"
shows"G IsCircumcenter C A B"
by (simp add: assms is_circumcenter_perm_3)
lemma is_circumcenter_perm_5:
assumes "G IsCircumcenter A B C"
shows"G IsCircumcenter C B A"
using assms is_circumcenter_perm_1 is_circumcenter_perm_4 by blast
lemma is_circumcenter_perm:
assumes "G IsCircumcenter A B C"
shows"G IsCircumcenter A B C \<and> G IsCircumcenter A C B \<and>
G IsCircumcenter B A C \<and> G IsCircumcenter B C A \<and>
G IsCircumcenter C A B \<and> G IsCircumcenter C B A"
using assms is_circumcenter_perm_4 is_circumcenter_perm_5 by blast
lemma is_circumcenter_cases: