Theory Tarski

section‹Tarski axioms›

text ‹In this section we introduce axioms of Tarski \<^cite>‹"tarski"› trough a series of locales.›

theory Tarski
imports Main
begin

text ‹The first locale assumes all Tarski axioms except for the Euclid's axiom and the continuity
axiom and corresponds to absolute geometry.›

locale TarskiAbsolute =
  fixes cong :: "'p ⇒ 'p ⇒ 'p ⇒ 'p ⇒ bool"
  fixes betw :: "'p ⇒ 'p ⇒ 'p ⇒ bool"
  assumes cong_reflexive:  "cong x y y x"
  assumes cong_transitive: "cong x y z u ∧ cong x y v w ⟶ cong z u v w"
  assumes cong_identity:   "cong x y z z ⟶ x = y"
  assumes segment_construction: "∃ z. betw x y z ∧ cong y z a b"
  assumes five_segment:    "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'"
  assumes betw_identity:   "betw x y x ⟶ x = y"
  assumes Pasch:           "betw x u z ∧ betw y v z ⟶ (∃ a. betw u a y ∧ betw x a v)"
  assumes lower_dimension: "∃ a. ∃ b. ∃ c. ¬ betw a b c ∧ ¬ betw b c a ∧ ¬ betw c a b"
  assumes upper_dimension: "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"
begin

text ‹The following definitions are used to specify axioms in the following locales.›

text ‹Point $p$ is on line $ab$.›
definition on_line where
  "on_line p a b ⟷ betw p a b ∨ betw a p b ∨ betw a b p"

text ‹Point $p$ is on ray $ab$.›
definition on_ray where 
  "on_ray p a b ⟷ betw a p b ∨ betw a b p"

text ‹Point $p$ is inside angle $abc$.›
definition in_angle where
  "in_angle p a b c ⟷ b ≠ a ∧ b ≠ c ∧ p ≠ b ∧ (∃ x. betw a x c ∧ x ≠ a ∧ x ≠ c ∧ on_ray p b x)"

text ‹Ray $r_ar_b$ meets the line $l_al_b$.›
definition ray_meets_line where
  "ray_meets_line ra rb la lb ⟷ (∃ x. on_ray x ra rb ∧ on_line x la lb)"

end

text‹The second locales adds the negation of Euclid's axiom and limiting parallels and corresponds
to hyperbolic geometry.›

locale TarskiHyperbolic = TarskiAbsolute + 
  assumes euclid_negation: "∃ 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)"
  assumes limiting_parallels: "¬ on_line a x1 x2 ⟹ 
      (∃ a1 a2. ¬ on_line a a1 a2 ∧
                ¬ ray_meets_line a a1 x1 x2 ∧
                ¬ ray_meets_line a a2 x1 x2 ∧
                (∀ a'. in_angle a' a1 a a2 ⟶ ray_meets_line a a' x1 x2))"

text‹The third locale adds the continuity axiom and corresponds to elementary hyperbolic geometry.›
locale ElementaryTarskiHyperbolic = TarskiHyperbolic +
  assumes continuity: "⟦∃ a. ∀ x. ∀ y. φ x ∧ ψ y ⟶ betw a x y⟧ ⟹ ∃ b. ∀ x. ∀ y. φ x ∧ ψ y ⟶ betw x b y"

end