Theory Tarski_Non_Euclidean

(* IsaGeoCoq - Tarski_Non_Euclidean.thy

Port part of GeoCoq 3.4.0 (https://geocoq.github.io/GeoCoq/) in Isabelle/Hol 

Copyright (C) 2021-2025  Roland Coghetto roland.coghetto (at) cafr-msa2p.be

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_Non_Euclidean

imports
  Tarski_Postulate_Parallels

begin

section "Tarski Non Euclidean"

subsection "Definitions"

locale Tarski_Non_Euclidean = Tarski_neutral_dimensionless +
  fixes A0 B0 C0 D0 T0
  assumes NERule1: "Bet A0 D0 T0" 
    and NERule2: "Bet B0 D0 C0" 
    and NERule3: "A0 ≠ D0" 
    and not_tarski_s_parallel_postulate_aux: 
    "∀ X Y. ((Bet A0 B0 X ∧ Bet A0 C0 Y) ⟶ ¬ Bet X T0 Y)" 

context Tarski_Non_Euclidean

begin

subsection "Propositions"

lemma Tarski_Pre_Non_Euclidean_aux:
  shows "∃ A B C D T. ¬ ((Bet A D T ∧ Bet B D C ∧ A ≠ D) 
                         ⟶
                      (∃ X Y. Bet A B X ∧ Bet A C Y ∧ Bet X T Y))" 
  using NERule1 NERule2 NERule3 not_tarski_s_parallel_postulate_aux by blast

lemma NPost01:
  shows "¬ Postulate01" 
  using Postulate01_def Tarski_Pre_Non_Euclidean_aux tarski_s_parallel_postulate_def by blast

lemma NPost02:
  shows "¬ Postulate02" 
  using InterAx5 NPost01 by blast

lemma NPost05:
  shows "¬ Postulate05" 
  using NPost02 Postulate02_def Postulate05_def par_trans_implies_playfair by blast

lemma NPost06:
  shows "¬ Postulate06" 
  by (simp add: NPost02 equivalent_postulates_without_decidability_of_intersection_of_lines)

lemma NPost07:
  shows "¬ Postulate07" 
  using NPost02 equivalent_postulates_without_decidability_of_intersection_of_lines by blast

lemma NPost08:
  shows "¬ Postulate08" 
  using NPost06 equivalent_postulates_without_decidability_of_intersection_of_lines by blast

lemma NPost09:
  shows "¬ Postulate09" 
  by (simp add: NPost02 equivalent_postulates_without_decidability_of_intersection_of_lines)

lemma NPost10:
  shows "¬ Postulate10" 
  using NPost05 equivalent_postulates_without_decidability_of_intersection_of_lines by blast

lemma NPost11:
  shows "¬ Postulate11" 
  using NPost02 equivalent_postulates_without_decidability_of_intersection_of_lines by fastforce

lemma NPost12:
  shows "¬ Postulate12" 
  using NPost02 Postulate02_def Postulate12_def playfair_bis__playfair by blast

lemma NPost13:
  shows "¬ Postulate13" 
  using Cycle_2 NPost01 by blast

lemma NPost14:
  shows "¬ Postulate14" 
  using Cycle_2 NPost13 by blast

lemma NPost15:
  shows "¬ Postulate15" 
  using Cycle_1 NPost02 by blast

lemma NPost16:
  shows "¬ Postulate16" 
  using Cycle_2 NPost01 by blast

lemma NPost17:
  shows "¬ Postulate17" 
  using Cycle_2 NPost01 by blast

lemma NPost18:
  shows "¬ Postulate18" 
  using Cycle_2 NPost01 by blast

lemma NPost19:
  shows "¬ Postulate19" 
  using Cycle_2 NPost01 by blast

lemma NPost20:
  shows "¬ Postulate20" 
  using Cycle_2 NPost01 by blast

theorem not_tarski_s_parallel_postulate_thm:
  shows "∃ A B C D T. (Bet A D T ∧ Bet B D C ∧ A ≠ D ∧ 
                      (∀ X Y. (Bet A B X ∧ Bet A C Y) ⟶ ¬ Bet X T Y))" 
  using Tarski_Pre_Non_Euclidean_aux by blast

theorem not_playfair_s_postulate_thm:
  shows "∃ A1 A2 B1 B2 C1 C2 P. A1 A2 Par B1 B2 ∧ 
                                Col P B1 B2 ∧ A1 A2 Par C1 C2 ∧ Col P C1 C2 ∧
                                (¬ Col C1 B1 B2 ∨ ¬ Col C2 B1 B2)" 
  using NPost02 Postulate02_def playfair_s_postulate_def by blast

theorem not_postulate_of_transitivity_of_parallelism_thm:
  shows "∃ A1 A2 B1 B2 C1 C2. A1 A2 Par B1 B2 ∧ B1 B2 Par C1 C2 ∧ ¬ (A1 A2 Par C1 C2)" 
  using NPost05 Postulate05_def
    postulate_of_transitivity_of_parallelism_def by blast

theorem not_midpoint_converse_postulate_thm:
  shows "∃ A B C P Q. ¬ Col A B C ∧ P Midpoint B C ∧ A B Par Q P ∧ Col A C Q ∧ ¬ Q Midpoint A C" 
  using NPost06 midpoint_converse_postulate_def 
    Postulate06_def by blast

theorem not_alternate_interior_angles_postulate_thm:
  shows "∃ A B C D. A C TS B D ∧ A B Par C D ∧ ¬ B A C CongA D C A"
  using NPost07 Postulate07_def alternate_interior_angles_postulate_def by blast

theorem not_consecutive_interior_angles_postulate_thm:
  shows "∃ A B C D. B C OS A D ∧ A B Par C D ∧ ¬ A B C SuppA B C D" 
  using NPost08 Postulate08_def consecutive_interior_angles_postulate_def by blast

theorem not_perpendicular_transversal_postulate_thm:
  shows "∃ A B C D P Q. A B Par C D ∧ A B Perp P Q ∧ Coplanar C D P Q ∧ ¬ C D Perp P Q" 
  using NPost09 Postulate09_def perpendicular_transversal_postulate_def by blast

theorem not_postulate_of_parallelism_of_perpendicular_transversals_thm:
  shows "∃ A1 A2 B1 B2 C1 C2 D1 D2.
   A1 A2 Par B1 B2 ∧ A1 A2 Perp C1 C2 ∧ B1 B2 Perp D1 D2 ∧
   Coplanar A1 A2 C1 D1 ∧ Coplanar A1 A2 C1 D2 ∧
   Coplanar A1 A2 C2 D1 ∧ Coplanar A1 A2 C2 D2 ∧ ¬ C1 C2 Par D1 D2" 
  using NPost10 Postulate10_def 
    postulate_of_parallelism_of_perpendicular_transversals_def by blast

theorem not_universal_posidonius_postulate:
  shows "∃ A1 A2 A3 A4 B1 B2 B3 B4.
   A1 A2 Par B1 B2 ∧ Col A1 A2 A3 ∧ Col B1 B2 B3 ∧ A1 A2 Perp A3 B3 ∧
   Col A1 A2 A4 ∧ Col B1 B2 B4 ∧ A1 A2 Perp A4 B4 ∧ ¬ Cong A3 B3 A4 B4" 
  using NPost11 Postulate11_def universal_posidonius_postulate_def by blast

theorem not_alternative_playfair_s_postulate_thm:
  shows "∃ A1 A2 B1 B2 C1 C2 P.
     P Perp2 A1 A2 B1 B2 ∧ ¬ Col A1 A2 P ∧ Col P B1 B2 ∧ 
     Coplanar A1 A2 B1 B2 ∧ A1 A2 Par C1 C2 ∧ Col P C1 C2 ∧ 
     (¬ Col C1 B1 B2 ∨ ¬ Col C2 B1 B2)" 
  using NPost02 Postulate02_def alternative_playfair_s_postulate_def 
    playfair_bis__playfair by blast

theorem not_proclus_postulate_thm:
  shows "∃ A B C D P Q. (∀ Y. A B Par C D ∧ Col A B P ∧ 
                        ¬ Col A B Q ∧ Coplanar C D P Q ∧ (¬ Col P Q Y ∨ ¬ Col C D Y))" 
  using NPost13 proclus_postulate_def Postulate13_def by blast

theorem not_alternative_proclus_postulate_thm:
  shows "∃ A B C D P Q. (∀ Y. P Perp2 A B C D ∧ ¬ Col C D P ∧ Coplanar A B C D ∧ Col A B P ∧ 
    ¬ Col A B Q ∧ Coplanar C D P Q ∧ (¬ Col P Q Y ∨ ¬ Col C D Y))"
  using NPost14 alternative_proclus_postulate_def Postulate14_def by blast

theorem not_triangle_circumscription_principle_thm:
  shows "∃ A B C. ∀ D. (¬ Col A B C ∧ (¬ Cong A D B D ∨ ¬ Cong A D C D ∨ ¬ Coplanar A B C D))" 
  using NPost15 Postulate15_def 
    triangle_circumscription_principle_def by blast

theorem not_inverse_projection_postulate_thm:
  shows "∃ A B C P Q. ∀ Y.
     Acute A B C ∧ B Out A P ∧ P ≠ Q ∧ Per B P Q ∧ Coplanar A B C Q ∧ 
     (¬ B Out C Y ∨ ¬ Col P Q Y)" 
  using NPost16 Postulate16_def inverse_projection_postulate_def by blast

theorem not_euclid_5_thm:
  shows "∃ P Q R S T U. ∀ I.
     BetS P T Q ∧ BetS R T S ∧ BetS Q U R ∧ ¬ Col P Q S ∧ 
     Cong P T Q T ∧ Cong R T S T ∧ (¬ BetS S Q I ∨ ¬ BetS P U I)"
  using NPost17 Postulate17_def euclid_5_def by blast

theorem not_strong_parallel_postulate_thm:
  shows "∃ P Q R S T U. ∀ I.
    BetS P T Q ∧ BetS R T S ∧ ¬ Col P R U ∧ Coplanar P Q R U ∧ 
    Cong P T Q T ∧ Cong R T S T ∧ (¬ Col S Q I ∨ ¬ Col P U I)" 
  using NPost18 Postulate18_def strong_parallel_postulate_def by blast

theorem not_alternative_strong_parallel_postulate_thm:
  shows "∃ A B C D P Q R. ∀ Y.
   B C OS A D ∧ A B C B C D SumA P Q R ∧ ¬ Bet P Q R ∧ (¬ Col B A Y ∨ ¬ Col C D Y)" 
  using NPost19 Postulate19_def alternative_strong_parallel_postulate_def by blast

theorem not_euclid_s_parallel_postulate_thm:
  shows "∃ A B C D P Q R. ∀ Y.
     B C OS A D ∧ SAMS A B C B C D ∧ A B C B C D SumA P Q R ∧ 
     ¬ Bet P Q R ∧ (¬ B Out A Y ∨ ¬ C Out D Y)" 
  using NPost20 Postulate20_def euclid_s_parallel_postulate_def by blast

end
end