Theory TarskiIsomorphism

theory TarskiIsomorphism
  imports Poincare_Disc.Tarski
begin

locale TarskiAbsoluteIso = TarskiAbsolute + 
  fixes φ :: "'a ⇒ 'b"
  fixes cong' :: "'b ⇒ 'b ⇒ 'b ⇒ 'b ⇒ bool"
  fixes betw' :: "'b ⇒ 'b ⇒ 'b ⇒ bool"
  assumes φbij: "bij φ"
  assumes φcong: "⋀ x y z w. cong' (φ x) (φ y) (φ z) (φ w) ⟷ cong x y z w"
  assumes φbetw: "⋀ x y z. betw' (φ x) (φ y) (φ z) ⟷ betw x y z"

sublocale TarskiAbsoluteIso ⊆ TA: TarskiAbsolute cong' betw'
proof
  fix x y
  show "cong' x y y x"
    by (smt (verit) φcong  φbij bij_iff cong_reflexive)
next
  fix x y z u v w
  show "cong' x y z u ∧ cong' x y v w ⟶ cong' z u v w"
    by (smt (verit) φcong φbij bij_iff cong_transitive)
next
  fix x y z
  show "cong' x y z z ⟶ x = y"
    by (smt (verit) φcong φbij bij_iff cong_identity)
next
  fix x y a b
  show "∃ z. betw' x y z ∧ cong' y z a b"
    by (smt (verit) φcong φbetw φbij bij_iff segment_construction)
next
  fix x y z x' y' z' u u'
  show "x ≠ y ∧ betw' x y z ∧ betw' x' y' z' ∧ cong' x y x' y' ∧ cong' y z y' z' ∧ cong' x u x' u' ∧ cong' y u y' u' ⟶
        cong' z u z' u'"
    by (smt (verit) φcong φbetw φbij bij_iff five_segment)
next
  fix x y 
  show "betw' x y x ⟶ x = y"
    by (metis φbetw φbij betw_identity bij_pointE)
next
  fix x u z y v
  show "betw' x u z ∧ betw' y v z ⟶ (∃a. betw' u a y ∧ betw' x a v)"
    by (smt (verit) φbetw φbij Pasch bij_pointE)
next
  show "∃ a b c. ¬ betw' a b c ∧ ¬ betw' b c a ∧ ¬ betw' c a b"
    by (smt (verit) φbetw φbij lower_dimension bij_pointE)
next
  fix x u v y z
  show "cong' x u x v ∧ cong' y u y v ∧ cong' z u z v ∧ u ≠ v ⟶ betw' x y z ∨ betw' y z x ∨ betw' z x y"
    by (smt (verit) φcong φbetw φbij upper_dimension bij_pointE)
qed

context TarskiAbsoluteIso
begin
lemma φon_line: 
  shows "TA.on_line (φ p) (φ a) (φ b) ⟷ on_line p a b"
  using TA.on_line_def φbetw on_line_def 
  by presburger

lemma φon_ray: 
  shows "TA.on_ray (φ p) (φ a) (φ b) ⟷ on_ray p a b"
  using TA.on_ray_def φbetw on_ray_def 
  by presburger

lemma φin_angle: 
  shows "TA.in_angle (φ p) (φ a) (φ b) (φ c) ⟷ in_angle p a b c"
proof
  assume "in_angle p a b c"
  then show "TA.in_angle (φ p) (φ a) (φ b) (φ c)"
    by (smt (verit, best) TA.in_angle_def in_angle_def φbetw φbij φon_ray bij_is_inj inj_eq)
next
  assume "TA.in_angle (φ p) (φ a) (φ b) (φ c)"
  then obtain x where "φ b ≠ φ a ∧ φ b ≠ φ c ∧ φ p ≠ φ b" "betw' (φ a) (φ x) (φ c) ∧ φ x ≠ φ a ∧ φ x ≠ φ c" "TA.on_ray (φ p) (φ b) (φ x)"
    by (smt (verit, ccfv_threshold) TA.in_angle_def φbij bij_pointE)
  then show "in_angle p a b c"
    unfolding in_angle_def
    using φbetw φon_ray by auto
qed

lemma φray_meets_line: 
  shows "TA.ray_meets_line (φ ra) (φ rb) (φ la) (φ lb) ⟷
         ray_meets_line ra rb la lb"
  unfolding TA.ray_meets_line_def ray_meets_line_def
  by (metis φbij φon_line φon_ray bij_pointE)

end

locale TarskiHyperbolicIso = TarskiHyperbolic + 
  fixes φ :: "'a ⇒ 'b"
  fixes cong' :: "'b ⇒ 'b ⇒ 'b ⇒ 'b ⇒ bool"
  fixes betw' :: "'b ⇒ 'b ⇒ 'b ⇒ bool"
  assumes φbij: "bij φ"
  assumes φcong: "⋀ x y z w. cong' (φ x) (φ y) (φ z) (φ w) ⟷ cong x y z w"
  assumes φbetw: "⋀ x y z. betw' (φ x) (φ y) (φ z) ⟷ betw x y z"

sublocale TarskiHyperbolicIso ⊆ TAI: TarskiAbsoluteIso
  by (simp add: TarskiAbsoluteIso.intro TarskiAbsoluteIso_axioms_def TarskiAbsolute_axioms φbetw φbij φcong)

sublocale TarskiHyperbolicIso ⊆ TarskiHyperbolic cong' betw'
proof
  show "∃a b c d t. betw' a d t ∧ betw' b d c ∧ a ≠ d ∧ (∀x y. betw' a b x ∧ betw' a c y ⟶ ¬ betw' x t y)"
    by (smt (verit) φbetw φbij euclid_negation bij_pointE)
next
  fix a x1 x2
  assume "¬ TAI.TA.on_line a x1 x2"
  then have *: "¬ on_line (inv φ a) (inv φ x1) (inv φ x2)"
    by (metis φbij TAI.φon_line bij_inv_eq_iff)
  obtain a1 a2 where *: 
    "¬ on_line (inv φ a) (inv φ a1) (inv φ a2)"
    "¬ ray_meets_line (inv φ a) (inv φ a1) (inv φ x1) (inv φ x2)"
    "¬ ray_meets_line (inv φ a) (inv φ a2) (inv φ x1) (inv φ x2)"
    "(∀a'. in_angle a' (inv φ a1) (inv φ a) (inv φ a2) ⟶ ray_meets_line (inv φ a) a' (inv φ x1) (inv φ x2))"
    using limiting_parallels[OF *] 
    by (smt (verit, ccfv_threshold) φbij bij_inv_eq_iff)
  then have "¬ TAI.TA.on_line a a1 a2 ∧ ¬ TAI.TA.ray_meets_line a a1 x1 x2 ∧ ¬ TAI.TA.ray_meets_line a a2 x1 x2"
    by (metis φbij TAI.φon_line TAI.φray_meets_line bij_is_surj surj_f_inv_f)
  moreover
  have "∀a'. TAI.TA.in_angle a' a1 a a2 ⟶ TAI.TA.ray_meets_line a a' x1 x2"
  proof safe
    fix a'
    assume "TAI.TA.in_angle a' a1 a a2"
    then have "ray_meets_line (inv φ a) (inv φ a') (inv φ x1) (inv φ x2)"
      using *(4) TAI.φray_meets_line TAI.φin_angle φbij bij_pointE
      by (smt (verit, ccfv_SIG) bij_is_surj surj_f_inv_f)
    then show "TAI.TA.ray_meets_line a a' x1 x2"
      by (metis φbij TAI.φray_meets_line bij_is_surj surj_f_inv_f)
  qed
  ultimately show "∃a1 a2.
          ¬ TAI.TA.on_line a a1 a2 ∧
          ¬ TAI.TA.ray_meets_line a a1 x1 x2 ∧
          ¬ TAI.TA.ray_meets_line a a2 x1 x2 ∧
          (∀a'. TAI.TA.in_angle a' a1 a a2 ⟶ TAI.TA.ray_meets_line a a' x1 x2)"
    by blast
qed

locale ElementaryTarskiHyperbolicIso = ElementaryTarskiHyperbolic + 
  fixes φ :: "'a ⇒ 'b"
  fixes cong' :: "'b ⇒ 'b ⇒ 'b ⇒ 'b ⇒ bool"
  fixes betw' :: "'b ⇒ 'b ⇒ 'b ⇒ bool"
  assumes φbij: "bij φ"
  assumes φcong: "⋀ x y z w. cong' (φ x) (φ y) (φ z) (φ w) ⟷ cong x y z w"
  assumes φbetw: "⋀ x y z. betw' (φ x) (φ y) (φ z) ⟷ betw x y z"

sublocale ElementaryTarskiHyperbolicIso ⊆ THI: TarskiHyperbolicIso
  by (simp add: TarskiHyperbolicIso.intro TarskiHyperbolicIso_axioms_def TarskiHyperbolic_axioms φbetw φbij φcong)

sublocale ElementaryTarskiHyperbolicIso ⊆ ElementaryTarskiHyperbolic cong' betw'
proof
  fix Φ Ψ
  assume "∃a. ∀x y. Φ x ∧ Ψ y ⟶ betw' a x y"
  then have "∃a. ∀x y. (Φ ∘ φ) x ∧ (Ψ ∘ φ) y ⟶ betw a x y"
    by (metis (no_types, opaque_lifting) φbetw φbij bij_pointE comp_eq_dest_lhs)
  then have "∃b. ∀x y. (Φ ∘ φ) x ∧ (Ψ ∘ φ) y ⟶ betw x b y"
    using continuity
    by simp
  then show "∃b. ∀x y. Φ x ∧ Ψ y ⟶ betw' x b y"
    by (metis (no_types, opaque_lifting) φbetw φbij bij_pointE comp_eq_dest_lhs)    
qed


end