Theory Poincare_Tarski
section ‹Poincar\'e model satisfies Tarski axioms›
theory Poincare_Tarski
imports Poincare Poincare_Lines_Axis_Intersections Tarski
begin
subsection‹Pasch axiom›
lemma Pasch_fun_mono:
fixes r1 r2 :: real
assumes "0 < r1" and "r1 ≤ r2" and "r2 < 1"
shows "r1 + 1/r1 ≥ r2 + 1/r2"
proof (cases "r1 = r2")
case True
thus ?thesis
by simp
next
case False
hence "r2 - r1 > 0"
using assms
by simp
have "r1 * r2 < 1"
using assms
by (smt mult_le_cancel_left1)
hence "1 / (r1 * r2) > 1"
using assms
by simp
hence "(r2 - r1) / (r1 * r2) > (r2 - r1)"
using ‹r2 - r1 > 0›
using mult_less_cancel_left_pos[of "r2 - r1" 1 "1 / (r1 * r2)"]
by simp
hence "1 / r1 - 1 / r2 > r2 - r1"
using assms
by (simp add: field_simps)
thus ?thesis
by simp
qed
text‹Pasch axiom, non-degenerative case.›
lemma Pasch_nondeg:
assumes "x ∈ unit_disc" and "y ∈ unit_disc" and "z ∈ unit_disc" and "u ∈ unit_disc" and "v ∈ unit_disc"
assumes "distinct [x, y, z, u, v]"
assumes "¬ poincare_collinear {x, y, z}"
assumes "poincare_between x u z" and "poincare_between y v z"
shows "∃ a. a ∈ unit_disc ∧ poincare_between u a y ∧ poincare_between x a v"
proof-
have "∀ y z u. distinct [x, y, z, u, v] ∧ ¬ poincare_collinear {x, y, z} ∧ y ∈ unit_disc ∧ z ∈ unit_disc ∧ u ∈ unit_disc ∧
poincare_between x u z ∧ poincare_between y v z ⟶ (∃ a. a ∈ unit_disc ∧ poincare_between u a y ∧ poincare_between x a v)" (is "?P x v")
proof (rule wlog_positive_x_axis[where P="?P"])
fix v
assume v: "is_real v" "0 < Re v" "Re v < 1"
hence "of_complex v ∈ unit_disc"
by (auto simp add: cmod_eq_Re)
show "?P 0⇩h (of_complex v)"
proof safe
fix y z u
assume distinct: "distinct [0⇩h, y, z, u, of_complex v]"
assume in_disc: "y ∈ unit_disc" "z ∈ unit_disc" "u ∈ unit_disc"
then obtain y' z' u'
where *: "y = of_complex y'" "z = of_complex z'" "u = of_complex u'"
using inf_or_of_complex inf_notin_unit_disc
by metis
have "y' ≠ 0" "z' ≠ 0" "u' ≠ 0" "v ≠ 0" "y' ≠ z'" "y' ≠ u'" "z' ≠ u'" "y ≠ z" "y ≠ u" "z ≠ u"
using of_complex_inj distinct *
by auto
note distinct = distinct this
assume "¬ poincare_collinear {0⇩h, y, z}"
hence nondeg_yz: "y'*cnj z' ≠ cnj y' * z'"
using * poincare_collinear_zero_iff[of y' z'] in_disc distinct
by auto
assume "poincare_between 0⇩h u z"
hence "Arg u' = Arg z'" "cmod u' ≤ cmod z'"
using * poincare_between_0uv[of u z] distinct in_disc
by auto
then obtain φ ru rz where
uz_polar: "u' = cor ru * cis φ" "z' = cor rz * cis φ" "0 < ru" "ru ≤ rz" "0 < rz" and
"φ = Arg u'" "φ = Arg z'"
using * ‹u' ≠ 0› ‹z' ≠ 0›
by (smt cmod_cis norm_le_zero_iff)
obtain θ ry where
y_polar: "y' = cor ry * cis θ" "ry > 0" and "θ = Arg y'"
using ‹y' ≠ 0›
by (smt cmod_cis norm_le_zero_iff)
from in_disc * ‹u' = cor ru * cis φ› ‹z' = cor rz * cis φ› ‹y' = cor ry * cis θ›
have "ru < 1" "rz < 1" "ry < 1"
by (auto simp: norm_mult)
note polar = this y_polar uz_polar
have nondeg: "cis θ * cis (- φ) ≠ cis (- θ) * cis φ"
using nondeg_yz polar
by simp
let ?yz = "poincare_line y z"
let ?v = "calc_x_axis_intersection ?yz"
assume "poincare_between y (of_complex v) z"
hence "of_complex v ∈ circline_set ?yz"
using in_disc ‹of_complex v ∈ unit_disc›
using distinct poincare_between_poincare_collinear[of y "of_complex v" z]
using unique_poincare_line[of y z]
by (auto simp add: poincare_collinear_def)
moreover
have "of_complex v ∈ circline_set x_axis"
using ‹is_real v›
unfolding circline_set_x_axis
by auto
moreover
have "?yz ≠ x_axis"
proof (rule ccontr)
assume "¬ ?thesis"
hence "{0⇩h, y, z} ⊆ circline_set (poincare_line y z)"
unfolding circline_set_def
using distinct poincare_line[of y z]
by auto
hence "poincare_collinear {0⇩h, y, z}"
unfolding poincare_collinear_def
using distinct
by force
thus False
using ‹¬ poincare_collinear {0⇩h, y, z}›
by simp
qed
ultimately
have "?v = of_complex v" "intersects_x_axis ?yz"
using unique_calc_x_axis_intersection[of "poincare_line y z" "of_complex v"]
using intersects_x_axis_iff[of ?yz]
using distinct ‹of_complex v ∈ unit_disc›
by (metis IntI is_poincare_line_poincare_line)+
have "intersects_x_axis_positive ?yz"
using ‹Re v > 0› ‹of_complex v ∈ unit_disc›
using ‹of_complex v ∈ circline_set ?yz› ‹of_complex v ∈ circline_set x_axis›
using intersects_x_axis_positive_iff[of ?yz] ‹y ≠ z› ‹?yz ≠ x_axis›
unfolding positive_x_axis_def
by force
have "y ∉ circline_set x_axis"
proof (rule ccontr)
assume "¬ ?thesis"
moreover
hence "poincare_line y (of_complex v) = x_axis"
using distinct ‹of_complex v ∈ circline_set x_axis›
using in_disc ‹of_complex v ∈ unit_disc›
using unique_poincare_line[of y "of_complex v" x_axis]
by simp
moreover
have "z ∈ circline_set (poincare_line y (of_complex v))"
using ‹of_complex v ∈ circline_set ?yz›
using unique_poincare_line[of y "of_complex v" "poincare_line y z"]
using in_disc ‹of_complex v ∈ unit_disc› distinct
using poincare_line[of y z]
unfolding circline_set_def
by (metis distinct_length_2_or_more is_poincare_line_poincare_line mem_Collect_eq)
ultimately
have "y ∈ circline_set x_axis" "z ∈ circline_set x_axis"
by auto
hence "poincare_collinear {0⇩h, y, z}"
unfolding poincare_collinear_def
by force
thus False
using ‹¬ poincare_collinear {0⇩h, y, z}›
by simp
qed
moreover
have "z ∉ circline_set x_axis"
proof (rule ccontr)
assume "¬ ?thesis"
moreover
hence "poincare_line z (of_complex v) = x_axis"
using distinct ‹of_complex v ∈ circline_set x_axis›
using in_disc ‹of_complex v ∈ unit_disc›
using unique_poincare_line[of z "of_complex v" x_axis]
by simp
moreover
have "y ∈ circline_set (poincare_line z (of_complex v))"
using ‹of_complex v ∈ circline_set ?yz›
using unique_poincare_line[of z "of_complex v" "poincare_line y z"]
using in_disc ‹of_complex v ∈ unit_disc› distinct
using poincare_line[of y z]
unfolding circline_set_def
by (metis distinct_length_2_or_more is_poincare_line_poincare_line mem_Collect_eq)
ultimately
have "y ∈ circline_set x_axis" "z ∈ circline_set x_axis"
by auto
hence "poincare_collinear {0⇩h, y, z}"
unfolding poincare_collinear_def
by force
thus False
using ‹¬ poincare_collinear {0⇩h, y, z}›
by simp
qed
ultimately
have "φ * θ < 0"
using ‹poincare_between y (of_complex v) z›
using poincare_between_x_axis_intersection[of y z "of_complex v"]
using in_disc ‹of_complex v ∈ unit_disc› distinct
using ‹of_complex v ∈ circline_set ?yz› ‹of_complex v ∈ circline_set x_axis›
using ‹φ = Arg z'› ‹θ = Arg y'› *
by (simp add: field_simps)
have "φ ≠ pi" "φ ≠ 0"
using ‹z ∉ circline_set x_axis› * polar cis_pi
unfolding circline_set_x_axis
by auto
have "θ ≠ pi" "θ ≠ 0"
using ‹y ∉ circline_set x_axis› * polar cis_pi
unfolding circline_set_x_axis
by auto
have phi_sin: "φ > 0 ⟷ sin φ > 0" "φ < 0 ⟷ sin φ < 0"
using ‹φ = Arg z'› ‹φ ≠ 0› ‹φ ≠ pi›
using Arg_bounded[of z']
by (smt sin_gt_zero sin_le_zero sin_pi_minus sin_0_iff_canon sin_ge_zero)+
have theta_sin: "θ > 0 ⟷ sin θ > 0" "θ < 0 ⟷ sin θ < 0"
using ‹θ = Arg y'› ‹θ ≠ 0› ‹θ ≠ pi›
using Arg_bounded[of y']
by (smt sin_gt_zero sin_le_zero sin_pi_minus sin_0_iff_canon sin_ge_zero)+
have "sin φ * sin θ < 0"
using ‹φ * θ < 0› phi_sin theta_sin
by (simp add: mult_less_0_iff)
have "sin (φ - θ) ≠ 0"
proof (rule ccontr)
assume "¬ ?thesis"
hence "sin (φ - θ) = 0"
by simp
have "- 2 * pi < φ - θ" "φ - θ < 2 * pi"
using ‹φ = Arg z'› ‹θ = Arg y'› Arg_bounded[of z'] Arg_bounded[of y'] ‹φ ≠ pi› ‹θ ≠ pi›
by auto
hence "φ - θ = -pi ∨ φ - θ = 0 ∨ φ - θ = pi"
using ‹sin (φ - θ) = 0›
by (smt sin_0_iff_canon sin_periodic_pi2)
moreover
{
assume "φ - θ = - pi"
hence "φ = θ - pi"
by simp
hence False
using nondeg_yz
using ‹y' = cor ry * cis θ› ‹z' = cor rz * cis φ› ‹rz > 0› ‹ry > 0›
by auto
}
moreover
{
assume "φ - θ = 0"
hence "φ = θ"
by simp
hence False
using ‹y' = cor ry * cis θ› ‹z' = cor rz * cis φ› ‹rz > 0› ‹ry > 0›
using nondeg_yz
by auto
}
moreover
{
assume "φ - θ = pi"
hence "φ = θ + pi"
by simp
hence False
using ‹y' = cor ry * cis θ› ‹z' = cor rz * cis φ› ‹rz > 0› ‹ry > 0›
using nondeg_yz
by auto
}
ultimately
show False
by auto
qed
have "u ∉ circline_set x_axis"
proof-
have "¬ is_real u'"
using * polar in_disc
using ‹φ ≠ 0› ‹φ = Arg u'› ‹φ ≠ pi› phi_sin(1) phi_sin(2)
by (metis is_real_arg2)
moreover
have "u ≠ ∞⇩h"
using in_disc
by auto
ultimately
show ?thesis
using * of_complex_inj[of u']
unfolding circline_set_x_axis
by auto
qed
let ?yu = "poincare_line y u"
have nondeg_yu: "y' * cnj u' ≠ cnj u' * u'"
using nondeg_yz polar ‹ru > 0› ‹rz > 0› distinct
by auto
{
fix r :: real
assume "r > 0"
have den: "cor ry * cis θ * cnj 1 * cnj (cor r * cis φ) * 1 - cor r * cis φ * cnj 1 * cnj (cor ry * cis θ) * 1 ≠ 0"
using ‹0 < r› ‹0 < ry› nondeg
by auto
let ?A = "2 * r * ry * sin(φ - θ)"
let ?B = "𝗂 * (r * cis φ * (1 + ry⇧2) - ry * cis θ * (1 + r⇧2))"
let ?ReB = "ry * (1 + r⇧2) * sin θ - r * (1 + ry⇧2) * sin φ"
have "Re (𝗂 * (r * cis (-φ) * ry * cis (θ) - ry * cis (-θ) * r * cis (φ))) = ?A"
by (simp add: sin_diff field_simps)
moreover
have "cor ry * cis (- θ) * (cor ry * cis θ) = ry⇧2" "cor r * cis (- φ) * (cor r * cis φ) = r⇧2"
by (metis cis_inverse cis_neq_zero divide_complex_def cor_squared nonzero_mult_div_cancel_right power2_eq_square semiring_normalization_rules(15))+
ultimately
have 1: "poincare_line_cvec_cmat (of_complex_cvec (cor ry * cis θ)) (of_complex_cvec (cor r * cis φ)) = (?A, ?B, cnj ?B, ?A)"
using den
unfolding poincare_line_cvec_cmat_def of_complex_cvec_def Let_def prod.case
by (simp add: field_simps)
have 2: "is_real ?A"
by simp
let ?mix = "cis θ * cis (- φ) - cis (- θ) * cis φ"
have "is_imag ?mix"
using eq_minus_cnj_iff_imag[of ?mix]
by simp
hence "Im ?mix ≠ 0"
using nondeg
using complex.expand[of ?mix 0]
by auto
hence 3: "Re ?A ≠ 0"
using ‹r > 0› ‹ry > 0›
by (simp add: sin_diff field_simps)
have "?A ≠ 0"
using 2 3
by auto
hence 4: "cor ?A ≠ 0"
using 2 3
by (metis zero_complex.simps(1))
have 5: "?ReB / ?A = (sin θ) / (2 * sin(φ - θ)) * (1/r + r) - (sin φ) / (2 * sin (φ - θ)) * (1/ry + ry)"
using ‹ry > 0› ‹r > 0›
apply (subst diff_divide_distrib)
apply (subst add_frac_num, simp)
apply (subst add_frac_num, simp)
apply (simp add: power2_eq_square mult.commute)
apply (simp add: field_simps)
done
have "poincare_line_cvec_cmat (of_complex_cvec (cor ry * cis θ)) (of_complex_cvec (cor r * cis φ)) = (?A, ?B, cnj ?B, ?A) ∧
is_real ?A ∧ Re ?A ≠ 0 ∧ ?A ≠ 0 ∧ cor ?A ≠ 0 ∧
Re ?B = ?ReB ∧
?ReB / ?A = (sin θ) / (2 * sin(φ - θ)) * (1/r + r) - (sin φ) / (2 * sin (φ - θ)) * (1/ry + ry)"
using 1 2 3 4 5
by auto
}
note ** = this
let ?Ayz = "2 * rz * ry * sin (φ - θ)"
let ?Byz = "𝗂 * (rz * cis φ * (1 + ry⇧2) - ry * cis θ * (1 + rz⇧2))"
let ?ReByz = "ry * (1 + rz⇧2) * sin θ - rz * (1 + ry⇧2) * sin φ"
let ?Kz = "(sin θ) / (2 * sin(φ - θ)) * (1/rz + rz) - (sin φ) / (2 * sin (φ - θ)) * (1/ry + ry)"
have yz: "poincare_line_cvec_cmat (of_complex_cvec (cor ry * cis θ)) (of_complex_cvec (cor rz * cis φ)) = (?Ayz, ?Byz, cnj ?Byz, ?Ayz)"
"is_real ?Ayz" "Re ?Ayz ≠ 0" "?Ayz ≠ 0" "cor ?Ayz ≠ 0" "Re ?Byz = ?ReByz" and Kz: "?ReByz / ?Ayz = ?Kz"
using **[OF ‹0 < rz›]
by auto
let ?Ayu = "2 * ru * ry * sin (φ - θ)"
let ?Byu = "𝗂 * (ru * cis φ * (1 + ry⇧2) - ry * cis θ * (1 + ru⇧2))"
let ?ReByu = "ry * (1 + ru⇧2) * sin θ - ru * (1 + ry⇧2) * sin φ"
let ?Ku = "(sin θ) / (2 * sin(φ - θ)) * (1/ru + ru) - (sin φ) / (2 * sin (φ - θ)) * (1/ry + ry)"
have yu: "poincare_line_cvec_cmat (of_complex_cvec (cor ry * cis θ)) (of_complex_cvec (cor ru * cis φ)) = (?Ayu, ?Byu, cnj ?Byu, ?Ayu)"
"is_real ?Ayu" "Re ?Ayu ≠ 0" "?Ayu ≠ 0" "cor ?Ayu ≠ 0" "Re ?Byu = ?ReByu" and Ku: "?ReByu / ?Ayu = ?Ku"
using **[OF ‹0 < ru›]
by auto
have "?Ayz ≠ 0"
using ‹sin (φ - θ) ≠ 0› ‹ry > 0› ‹rz > 0›
by auto
have "Re ?Byz / ?Ayz < -1"
using ‹intersects_x_axis_positive ?yz›
* ‹y' = cor ry * cis θ› ‹z' = cor rz * cis φ› ‹u' = cor ru * cis φ›
apply simp
apply (transfer fixing: ry rz ru θ φ)
apply (transfer fixing: ry rz ru θ φ)
proof-
assume "intersects_x_axis_positive_cmat (poincare_line_cvec_cmat (of_complex_cvec (cor ry * cis θ)) (of_complex_cvec (cor rz * cis φ)))"
thus "(ry * sin θ * (1 + rz⇧2) - rz * sin φ * (1 + ry⇧2)) / (2 * rz * ry * sin (φ - θ)) < - 1"
using yz
by simp
qed
have "?ReByz / ?Ayz ≥ ?ReByu / ?Ayu"
proof (cases "sin φ > 0")
case True
hence "sin θ < 0"
using ‹sin φ * sin θ < 0›
by (smt mult_nonneg_nonneg)
have "?ReByz < 0"
proof-
have "ry * (1 + rz⇧2) * sin θ < 0"
using ‹ry > 0› ‹rz > 0›
using ‹sin θ < 0›
by (smt mult_pos_neg mult_pos_pos zero_less_power)
moreover
have "rz * (1 + ry⇧2) * sin φ > 0"
using ‹ry > 0› ‹rz > 0›
using ‹sin φ > 0›
by (smt mult_pos_neg mult_pos_pos zero_less_power)
ultimately
show ?thesis
by simp
qed
have "?Ayz > 0"
using ‹Re ?Byz / ?Ayz < -1› ‹Re ?Byz = ?ReByz› ‹?ReByz < 0›
by (smt divide_less_0_iff)
hence "sin (φ - θ) > 0"
using ‹ry > 0› ‹rz > 0›
by (smt mult_pos_pos zero_less_mult_pos)
have "1 / ru + ru ≥ 1 / rz + rz"
using Pasch_fun_mono[of ru rz] ‹0 < ru› ‹ru ≤ rz› ‹rz < 1›
by simp
hence "sin θ * (1 / ru + ru) ≤ sin θ * (1 / rz + rz)"
using ‹sin θ < 0›
by auto
thus ?thesis
using ‹ru > 0› ‹rz > 0› ‹ru ≤ rz› ‹rz < 1› ‹?Ayz > 0› ‹sin (φ - θ) > 0›
using divide_right_mono[of "sin θ * (1 / ru + ru)" "sin θ * (1 / rz + rz)" "2 * sin (φ - θ)"]
by (subst Kz, subst Ku) simp
next
assume "¬ sin φ > 0"
hence "sin φ < 0"
using ‹sin φ * sin θ < 0›
by (cases "sin φ = 0", simp_all)
hence "sin θ > 0"
using ‹sin φ * sin θ < 0›
by (smt mult_nonpos_nonpos)
have "?ReByz > 0"
proof-
have "ry * (1 + rz⇧2) * sin θ > 0"
using ‹ry > 0› ‹rz > 0›
using ‹sin θ > 0›
by (smt mult_pos_neg mult_pos_pos zero_less_power)
moreover
have "rz * (1 + ry⇧2) * sin φ < 0"
using ‹ry > 0› ‹rz > 0›
using ‹sin φ < 0›
by (smt mult_pos_neg mult_pos_pos zero_less_power)
ultimately
show ?thesis
by simp
qed
have "?Ayz < 0"
using ‹Re ?Byz / ?Ayz < -1› ‹?Ayz ≠ 0› ‹Re ?Byz = ?ReByz› ‹?ReByz > 0›
by (smt divide_less_0_iff)
hence "sin (φ - θ) < 0"
using ‹ry > 0› ‹rz > 0›
by (smt mult_nonneg_nonneg)
have "1 / ru + ru ≥ 1 / rz + rz"
using Pasch_fun_mono[of ru rz] ‹0 < ru› ‹ru ≤ rz› ‹rz < 1›
by simp
hence "sin θ * (1 / ru + ru) ≥ sin θ * (1 / rz + rz)"
using ‹sin θ > 0›
by auto
thus ?thesis
using ‹ru > 0› ‹rz > 0› ‹ru ≤ rz› ‹rz < 1› ‹?Ayz < 0› ‹sin (φ - θ) < 0›
using divide_right_mono_neg[of "sin θ * (1 / rz + rz)" "sin θ * (1 / ru + ru)" "2 * sin (φ - θ)"]
by (subst Kz, subst Ku) simp
qed
have "intersects_x_axis_positive ?yu"
using * ‹y' = cor ry * cis θ› ‹z' = cor rz * cis φ› ‹u' = cor ru * cis φ›
apply simp
apply (transfer fixing: ry rz ru θ φ)
apply (transfer fixing: ry rz ru θ φ)
proof-
have "Re ?Byu / ?Ayu < -1"
using ‹Re ?Byz / ?Ayz < -1› ‹?ReByz / ?Ayz ≥ ?ReByu / ?Ayu›
by (subst (asm) ‹Re ?Byz = ?ReByz›, subst ‹Re ?Byu = ?ReByu›) simp
thus "intersects_x_axis_positive_cmat (poincare_line_cvec_cmat (of_complex_cvec (cor ry * cis θ)) (of_complex_cvec (cor ru * cis φ)))"
using yu
by simp
qed
let ?a = "calc_x_axis_intersection ?yu"
have "?a ∈ positive_x_axis" "?a ∈ circline_set ?yu" "?a ∈ unit_disc"
using ‹intersects_x_axis_positive ?yu›
using intersects_x_axis_positive_iff'[of ?yu] ‹y ≠ u›
by auto
then obtain a' where a': "?a = of_complex a'" "is_real a'" "Re a' > 0" "Re a' < 1"
unfolding positive_x_axis_def circline_set_x_axis
by (auto simp add: cmod_eq_Re)
have "intersects_x_axis ?yz" "intersects_x_axis ?yu"
using ‹intersects_x_axis_positive ?yz› ‹intersects_x_axis_positive ?yu›
by auto
show "∃a. a ∈ unit_disc ∧ poincare_between u a y ∧ poincare_between 0⇩h a (of_complex v)"
proof (rule_tac x="?a" in exI, safe)
show "poincare_between u ?a y"
using poincare_between_x_axis_intersection[of y u ?a]
using calc_x_axis_intersection[OF is_poincare_line_poincare_line[OF ‹y ≠ u›] ‹intersects_x_axis ?yu›]
using calc_x_axis_intersection_in_unit_disc[OF is_poincare_line_poincare_line[OF ‹y ≠ u›] ‹intersects_x_axis ?yu›]
using in_disc ‹y ≠ u› ‹y ∉ circline_set x_axis› ‹u ∉ circline_set x_axis›
using * ‹φ = Arg u'› ‹θ = Arg y'› ‹φ * θ < 0›
by (subst poincare_between_rev, auto simp add: mult.commute)
next
show "poincare_between 0⇩h ?a (of_complex v)"
proof-
have "-?ReByz / ?Ayz ≤ -?ReByu / ?Ayu"
using ‹?ReByz / ?Ayz ≥ ?ReByu / ?Ayu›
by linarith
have "outward ?yz ?yu"
using * ‹y' = cor ry * cis θ› ‹z' = cor rz * cis φ› ‹u' = cor ru * cis φ›
apply simp
apply (transfer fixing: ry rz ru θ φ)
apply (transfer fixing: ry rz ru θ φ)
apply (subst yz yu)+
unfolding outward_cmat_def
apply (simp only: Let_def prod.case)
apply (subst yz yu)+
using ‹-?ReByz / ?Ayz ≤ -?ReByu / ?Ayu›
by simp
hence "Re a' ≤ Re v"
using ‹?v = of_complex v›
using ‹?a = of_complex a'›
using ‹intersects_x_axis_positive ?yz› ‹intersects_x_axis_positive ?yu›
using outward[OF is_poincare_line_poincare_line[OF ‹y ≠ z›] is_poincare_line_poincare_line[OF ‹y ≠ u›]]
by simp
thus ?thesis
using ‹?v = of_complex v›
using poincare_between_x_axis_0uv[of "Re a'" "Re v"] a' v
by simp
qed
next
show "?a ∈ unit_disc"
by fact
qed
qed
next
show "x ∈ unit_disc" "v ∈ unit_disc" "x ≠ v"
using assms
by auto
next
fix M x v
let ?Mx = "moebius_pt M x" and ?Mv = "moebius_pt M v"
assume 1: "unit_disc_fix M" "x ∈ unit_disc" "v ∈ unit_disc" "x ≠ v"
assume 2: "?P ?Mx ?Mv"
show "?P x v"
proof safe
fix y z u
let ?My = "moebius_pt M y" and ?Mz = "moebius_pt M z" and ?Mu = "moebius_pt M u"
assume "distinct [x, y, z, u, v]" "¬ poincare_collinear {x, y, z}" "y ∈ unit_disc" "z ∈ unit_disc" "u ∈ unit_disc"
"poincare_between x u z" "poincare_between y v z"
hence "∃ Ma. Ma ∈ unit_disc ∧ poincare_between ?Mu Ma ?My ∧ poincare_between ?Mx Ma ?Mv"
using 1 2[rule_format, of ?My ?Mz ?Mu]
by simp
then obtain Ma where Ma: "Ma ∈ unit_disc" "poincare_between ?Mu Ma ?My ∧ poincare_between ?Mx Ma ?Mv"
by blast
let ?a = "moebius_pt (-M) Ma"
let ?Ma = "moebius_pt M ?a"
have "?Ma = Ma"
by (metis moebius_pt_invert uminus_moebius_def)
hence "?Ma ∈ unit_disc" "poincare_between ?Mu ?Ma ?My ∧ poincare_between ?Mx ?Ma ?Mv"
using Ma
by auto
thus "∃a. a ∈ unit_disc ∧ poincare_between u a y ∧ poincare_between x a v"
using unit_disc_fix_moebius_inv[OF ‹unit_disc_fix M›] ‹unit_disc_fix M› ‹Ma ∈ unit_disc›
using ‹u ∈ unit_disc› ‹v ∈ unit_disc› ‹x ∈ unit_disc› ‹y ∈ unit_disc›
by (rule_tac x="?a" in exI, simp del: moebius_pt_comp_inv_right)
qed
qed
thus ?thesis
using assms
by auto
qed
text‹Pasch axiom, only degenerative cases.›
lemma Pasch_deg:
assumes "x ∈ unit_disc" and "y ∈ unit_disc" and "z ∈ unit_disc" and "u ∈ unit_disc" and "v ∈ unit_disc"
assumes "¬ distinct [x, y, z, u, v] ∨ poincare_collinear {x, y, z}"
assumes "poincare_between x u z" and "poincare_between y v z"
shows "∃ a. a ∈ unit_disc ∧ poincare_between u a y ∧ poincare_between x a v"
proof(cases "poincare_collinear {x, y, z}")
case True
hence "poincare_between x y z ∨ poincare_between y x z ∨ poincare_between y z x"
using assms(1, 2, 3) poincare_collinear3_between poincare_between_rev by blast
show ?thesis
proof(cases "poincare_between x y z")
case True
have "poincare_between x y v"
using True assms poincare_between_transitivity
by (meson poincare_between_rev)
thus ?thesis
using assms(2)
by (rule_tac x="y" in exI, simp)
next
case False
hence "poincare_between y x z ∨ poincare_between y z x"
using ‹poincare_between x y z ∨ poincare_between y x z ∨ poincare_between y z x›
by simp
show ?thesis
proof(cases "poincare_between y x z")
case True
hence "poincare_between u x y"
using assms
by (meson poincare_between_rev poincare_between_transitivity)
thus ?thesis
using assms
by (rule_tac x="x" in exI, simp)
next
case False
hence "poincare_between y z x"
using ‹poincare_between y x z ∨ poincare_between y z x›
by auto
hence "poincare_between x z v"
using assms
by (meson poincare_between_rev poincare_between_transitivity)
hence "poincare_between x u v"
using assms poincare_between_transitivity poincare_between_rev
by (smt poincare_between_sum_distances)
thus ?thesis
using assms
by (rule_tac x="u" in exI, simp)
qed
qed
next
case False
hence "¬ distinct [x, y, z, u, v]"
using assms(6) by auto
show ?thesis
proof(cases "u=z")
case True
thus ?thesis
using assms
apply(rule_tac x="v" in exI)
by(simp add:poincare_between_rev)
next
case False
hence "x ≠ z"
using assms poincare_between_sandwich by blast
show ?thesis
proof(cases "v=z")
case True
thus ?thesis
using assms
by (rule_tac x="u" in exI, simp)
next
case False
hence "y ≠ z"
using assms poincare_between_sandwich by blast
show ?thesis
proof(cases "u = x")
case True
thus ?thesis
using assms
by (rule_tac x="x" in exI, simp)
next
case False
have "x ≠ y"
using assms ‹¬ poincare_collinear {x, y, z}›
by fastforce
have "x ≠ v"
using assms ‹¬ poincare_collinear {x, y, z}›
by (metis insert_commute poincare_between_poincare_collinear)
have "u ≠ y"
using assms ‹¬ poincare_collinear {x, y, z}›
using poincare_between_poincare_collinear by blast
have "u ≠ v"
proof(rule ccontr)
assume "¬ u ≠ v"
hence "poincare_between x v z"
using assms by auto
hence "x ∈ circline_set (poincare_line z v)"
using poincare_between_rev[of x v z]
using poincare_between_poincare_line_uvz[of z v x]
using assms ‹v ≠ z›
by auto
have "y ∈ circline_set (poincare_line z v)"
using assms ‹¬ u ≠ v›
using poincare_between_rev[of y v z]
using poincare_between_poincare_line_uvz[of z v y]
using assms ‹v ≠ z›
by auto
have "z ∈ circline_set (poincare_line z v)"
using ex_poincare_line_two_points[of z v] ‹v ≠ z›
by auto
have "is_poincare_line (poincare_line z v)"
using ‹v ≠ z›
by auto
hence "poincare_collinear {x, y, z}"
using ‹x ∈ circline_set (poincare_line z v)›
using ‹y ∈ circline_set (poincare_line z v)›
using ‹z ∈ circline_set (poincare_line z v)›
unfolding poincare_collinear_def
by (rule_tac x="poincare_line z v" in exI, simp)
thus False
using ‹¬ poincare_collinear {x, y, z}› by simp
qed
have "v = y"
using ‹u ≠ v› ‹u ≠ y› ‹x ≠ v› ‹x ≠ y› ‹u ≠ x› ‹y ≠ z› ‹v ≠ z› ‹x ≠ z› ‹u ≠ z›
using ‹¬ distinct [x, y, z, u, v]›
by auto
thus ?thesis
using assms
by (rule_tac x="y" in exI, simp)
qed
qed
qed
qed
text ‹Axiom of Pasch›
lemma Pasch:
assumes "x ∈ unit_disc" and "y ∈ unit_disc" and "z ∈ unit_disc" and "u ∈ unit_disc" and "v ∈ unit_disc"
assumes "poincare_between x u z" and "poincare_between y v z"
shows "∃ a. a ∈ unit_disc ∧ poincare_between u a y ∧ poincare_between x a v"
proof(cases "distinct [x, y, z, u, v] ∧ ¬ poincare_collinear {x, y, z}")
case True
thus ?thesis
using assms Pasch_nondeg by auto
next
case False
thus ?thesis
using assms Pasch_deg by auto
qed
subsection‹Segment construction axiom›
lemma segment_construction:
assumes "x ∈ unit_disc" and "y ∈ unit_disc"
assumes "a ∈ unit_disc" and "b ∈ unit_disc"
shows "∃ z. z ∈ unit_disc ∧ poincare_between x y z ∧ poincare_distance y z = poincare_distance a b"
proof-
obtain d where d: "d = poincare_distance a b"
by auto
have "d ≥ 0"
using assms
by (simp add: d poincare_distance_ge0)
have "∃ z. z ∈ unit_disc ∧ poincare_between x y z ∧ poincare_distance y z = d" (is "?P x y")
proof (cases "x = y")
case True
have "∃ z. z ∈ unit_disc ∧ poincare_distance x z = d"
proof (rule wlog_zero)
show "∃ z. z ∈ unit_disc ∧ poincare_distance 0⇩h z = d"
using ex_x_axis_poincare_distance_negative[of d] ‹d ≥ 0›
by blast
next
show "x ∈ unit_disc"
by fact
next
fix a u
assume "u ∈ unit_disc" "cmod a < 1"
assume "∃z. z ∈ unit_disc ∧ poincare_distance (moebius_pt (blaschke a) u) z = d"
then obtain z where *: "z ∈ unit_disc" "poincare_distance (moebius_pt (blaschke a) u) z = d"
by auto
obtain z' where z': "z = moebius_pt (blaschke a) z'" "z' ∈ unit_disc"
using ‹z ∈ unit_disc›
using unit_disc_fix_iff[of "blaschke a"] ‹cmod a < 1›
using blaschke_unit_disc_fix[of a]
by blast
show "∃z. z ∈ unit_disc ∧ poincare_distance u z = d"
using * z' ‹u : unit_disc›
using blaschke_unit_disc_fix[of a] ‹cmod a < 1›
by (rule_tac x=z' in exI, simp)
qed
thus ?thesis
using ‹x = y›
unfolding poincare_between_def
by auto
next
case False
show ?thesis
proof (rule wlog_positive_x_axis[where P="λ y x. ?P x y"])
fix x
assume "is_real x" "0 < Re x" "Re x < 1"
then obtain z where z: "is_real z" "Re z ≤ 0" "- 1 < Re z" "of_complex z ∈ unit_disc"
"of_complex z ∈ unit_disc" "of_complex z ∈ circline_set x_axis" "poincare_distance 0⇩h (of_complex z) = d"
using ex_x_axis_poincare_distance_negative[of d] ‹d ≥ 0›
by auto
have "poincare_between (of_complex x) 0⇩h (of_complex z)"
proof (cases "z = 0")
case True
thus ?thesis
unfolding poincare_between_def
by auto
next
case False
have "x ≠ 0"
using ‹is_real x› ‹Re x > 0›
by auto
thus ?thesis
using poincare_between_x_axis_u0v[of x z]
using z ‹is_real x› ‹x ≠ 0› ‹Re x > 0› False
using complex_eq_if_Re_eq mult_pos_neg
by fastforce
qed
thus "?P (of_complex x) 0⇩h"
using ‹poincare_distance 0⇩h (of_complex z) = d› ‹of_complex z ∈ unit_disc›
by blast
next
show "x ∈ unit_disc" "y ∈ unit_disc"
by fact+
next
show "y ≠ x" using ‹x ≠ y› by simp
next
fix M u v
assume "unit_disc_fix M" "u ∈ unit_disc" "v ∈ unit_disc" "u ≠ v"
assume "?P (moebius_pt M v) (moebius_pt M u)"
then obtain z where *: "z ∈ unit_disc" "poincare_between (moebius_pt M v) (moebius_pt M u) z" "poincare_distance (moebius_pt M u) z = d"
by auto
obtain z' where z': "z = moebius_pt M z'" "z' ∈ unit_disc"
using ‹z ∈ unit_disc›
using unit_disc_fix_iff[of M] ‹unit_disc_fix M›
by blast
thus "?P v u"
using * ‹u ∈ unit_disc› ‹v ∈ unit_disc› ‹unit_disc_fix M›
by auto
qed
qed
thus ?thesis
using assms d
by auto
qed
subsection‹Five segment axiom›
lemma five_segment_axiom:
assumes
in_disc: "x ∈ unit_disc" "y ∈ unit_disc" "z ∈ unit_disc" "u ∈ unit_disc" and
in_disc': "x' ∈ unit_disc" "y' ∈ unit_disc" "z' ∈ unit_disc" "u' ∈ unit_disc" and
"x ≠ y" and
betw: "poincare_between x y z" "poincare_between x' y' z'" and
xy: "poincare_distance x y = poincare_distance x' y'" and
xu: "poincare_distance x u = poincare_distance x' u'" and
yu: "poincare_distance y u = poincare_distance y' u'" and
yz: "poincare_distance y z = poincare_distance y' z'"
shows
"poincare_distance z u = poincare_distance z' u'"
proof-
from assms obtain M where
M: "unit_disc_fix_f M" "M x = x'" "M u = u'" "M y = y'"
using unit_disc_fix_f_congruent_triangles[of x y u]
by blast
have "M z = z'"
proof (rule unique_poincare_distance_on_ray[where u=x' and v=y' and y="M z" and z=z' and d="poincare_distance x z"])
show "0 ≤ poincare_distance x z"
using poincare_distance_ge0 in_disc
by simp
next
show "x' ≠ y'"
using M ‹x ≠ y›
using in_disc in_disc' poincare_distance_eq_0_iff xy
by auto
next
show "poincare_distance x' (M z) = poincare_distance x z"
using M in_disc
unfolding unit_disc_fix_f_def
by auto
next
show "M z ∈ unit_disc"
using M in_disc
unfolding unit_disc_fix_f_def
by auto
next
show "poincare_distance x' z' = poincare_distance x z"
using xy yz betw
using poincare_between_sum_distances[of x y z]
using poincare_between_sum_distances[of x' y' z']
using in_disc in_disc'
by auto
next
show "poincare_between x' y' (M z)"
using M
using in_disc betw
unfolding unit_disc_fix_f_def
by auto
qed fact+
thus ?thesis
using ‹unit_disc_fix_f M›
using in_disc in_disc'
‹M u = u'›
unfolding unit_disc_fix_f_def
by auto
qed
subsection‹Upper dimension axiom›
lemma upper_dimension_axiom:
assumes in_disc: "x ∈ unit_disc" "y ∈ unit_disc" "z ∈ unit_disc" "u ∈ unit_disc" "v ∈ unit_disc"
assumes "poincare_distance x u = poincare_distance x v"
"poincare_distance y u = poincare_distance y v"
"poincare_distance z u = poincare_distance z v"
"u ≠ v"
shows "poincare_between x y z ∨ poincare_between y z x ∨ poincare_between z x y"
proof (cases "x = y ∨ y = z ∨ x = z")
case True
thus ?thesis
using in_disc
by auto
next
case False
hence "x ≠ y" "x ≠ z" "y ≠ z"
by auto
let ?cong = "λ a b a' b'. poincare_distance a b = poincare_distance a' b'"
have "∀ z u v. z ∈ unit_disc ∧ u ∈ unit_disc ∧ v ∈ unit_disc ∧
?cong x u x v ∧ ?cong y u y v ∧ ?cong z u z v ∧ u ≠ v ⟶
poincare_collinear {x, y, z}" (is "?P x y")
proof (rule wlog_positive_x_axis[where P="?P"])
fix x
assume x: "is_real x" "0 < Re x" "Re x < 1"
hence "x ≠ 0"
by auto
have "0⇩h ∈ circline_set x_axis"
by simp
show "?P 0⇩h (of_complex x)"
proof safe
fix z u v
assume in_disc: "z ∈ unit_disc" "u ∈ unit_disc" "v ∈ unit_disc"
then obtain z' u' v' where zuv: "z = of_complex z'" "u = of_complex u'" "v = of_complex v'"
using inf_or_of_complex[of z] inf_or_of_complex[of u] inf_or_of_complex[of v]
by auto
assume cong: "?cong 0⇩h u 0⇩h v" "?cong (of_complex x) u (of_complex x) v" "?cong z u z v" "u ≠ v"
let ?r0 = "poincare_distance 0⇩h u" and
?rx = "poincare_distance (of_complex x) u"
have "?r0 > 0" "?rx > 0"
using in_disc cong
using poincare_distance_eq_0_iff[of "0⇩h" u] poincare_distance_ge0[of "0⇩h" u]
using poincare_distance_eq_0_iff[of "0⇩h" v] poincare_distance_ge0[of "0⇩h" v]
using poincare_distance_eq_0_iff[of "of_complex x" u] poincare_distance_ge0[of "of_complex x" u]
using poincare_distance_eq_0_iff[of "of_complex x" v] poincare_distance_ge0[of "of_complex x" v]
using x
by (auto simp add: cmod_eq_Re)
let ?pc0 = "poincare_circle 0⇩h ?r0" and
?pcx = "poincare_circle (of_complex x) ?rx"
have "u ∈ ?pc0 ∩ ?pcx" "v ∈ ?pc0 ∩ ?pcx"
using in_disc cong
by (auto simp add: poincare_circle_def)
hence "u = conjugate v"
using intersect_poincare_circles_x_axis[of 0 x ?r0 ?rx u v]
using x ‹x ≠ 0› ‹u ≠ v› ‹?r0 > 0› ‹?rx > 0›
by simp
let ?ru = "poincare_distance u z"
have "?ru > 0"
using poincare_distance_ge0[of u z] in_disc
using cong
using poincare_distance_eq_0_iff[of z u] poincare_distance_eq_0_iff[of z v]
using poincare_distance_eq_0_iff
by force
have "z ∈ poincare_circle u ?ru ∩ poincare_circle v ?ru"
using cong in_disc
unfolding poincare_circle_def
by (simp add: poincare_distance_sym)
hence "is_real z'"
using intersect_poincare_circles_conjugate_centers[of u v ?ru z] ‹u = conjugate v› zuv
using in_disc ‹u ≠ v› ‹?ru > 0›
by simp
thus "poincare_collinear {0⇩h, of_complex x, z}"
using poincare_line_0_real_is_x_axis[of "of_complex x"] x ‹x ≠ 0› zuv ‹0⇩h ∈ circline_set x_axis›
unfolding poincare_collinear_def
by (rule_tac x=x_axis in exI, auto simp add: circline_set_x_axis)
qed
next
fix M x y
assume 1: "unit_disc_fix M" "x ∈ unit_disc" "y ∈ unit_disc" "x ≠ y"
assume 2: "?P (moebius_pt M x) (moebius_pt M y)"
show "?P x y"
proof safe
fix z u v
assume "z ∈ unit_disc" "u ∈ unit_disc" "v ∈ unit_disc"
"?cong x u x v" "?cong y u y v" "?cong z u z v" "u ≠ v"
hence "poincare_collinear {moebius_pt M x, moebius_pt M y, moebius_pt M z}"
using 1 2[rule_format, of "moebius_pt M z" "moebius_pt M u" "moebius_pt M v"]
by simp
then obtain p where "is_poincare_line p" "{moebius_pt M x, moebius_pt M y, moebius_pt M z} ⊆ circline_set p"
unfolding poincare_collinear_def
by auto
thus "poincare_collinear {x, y, z}"
using ‹unit_disc_fix M›
unfolding poincare_collinear_def
by (rule_tac x="moebius_circline (-M) p" in exI, auto)
qed
qed fact+
thus ?thesis
using assms
using poincare_collinear3_between[of x y z]
using poincare_between_rev
by auto
qed
subsection‹Lower dimension axiom›
lemma lower_dimension_axiom:
shows "∃ a ∈ unit_disc. ∃ b ∈ unit_disc. ∃ c ∈ unit_disc.
¬ poincare_between a b c ∧ ¬ poincare_between b c a ∧ ¬ poincare_between c a b"
proof-
let ?u = "of_complex (1/2)" and ?v = "of_complex (𝗂/2)"
have 1: "0⇩h ∈ unit_disc" and 2: "?u ∈ unit_disc" and 3: "?v ∈ unit_disc"
by simp_all
have *: "¬ poincare_collinear {0⇩h, ?u, ?v}"
proof (rule ccontr)
assume "¬ ?thesis"
then obtain p where "is_poincare_line p" "{0⇩h, ?u, ?v} ⊆ circline_set p"
unfolding poincare_collinear_def
by auto
moreover
have "of_complex (1 / 2) ≠ of_complex (𝗂 / 2)"
using of_complex_inj
by fastforce
ultimately
have "0⇩h ∈ circline_set (poincare_line ?u ?v)"
using unique_poincare_line[of ?u ?v p]
by auto
thus False
unfolding circline_set_def
by simp (transfer, transfer, simp add: vec_cnj_def)
qed
show ?thesis
apply (rule_tac x="0⇩h" in bexI, rule_tac x="?u" in bexI, rule_tac x="?v" in bexI)
apply (rule ccontr, auto)
using *
using poincare_between_poincare_collinear[OF 1 2 3]
using poincare_between_poincare_collinear[OF 2 3 1]
using poincare_between_poincare_collinear[OF 3 1 2]
by (metis insert_commute)+
qed
subsection‹Negated Euclidean axiom›
lemma negated_euclidean_axiom_aux:
assumes "on_circline H (of_complex (1/2 + 𝗂/2))" and "is_poincare_line H"
assumes "intersects_x_axis_positive H"
shows "¬ intersects_y_axis_positive H"
using assms
proof (transfer, transfer)
fix H
assume hh: "hermitean H ∧ H ≠ mat_zero" "is_poincare_line_cmat H"
obtain A B C D where "H = (A, B, C, D)"
by (cases H, auto)
hence *: "is_real A" "H = (A, B, cnj B, A)" "(cmod B)⇧2 > (cmod A)⇧2"
using hermitean_elems[of A B C D] hh
by auto
assume "intersects_x_axis_positive_cmat H"
hence "Re A ≠ 0" "Re B / Re A < - 1"
using *
by auto
assume "on_circline_cmat_cvec H (of_complex_cvec (1 / 2 + 𝗂 / 2))"
hence "6*A + 4*Re B + 4*Im B = 0"
using *
unfolding of_real_mult
apply (subst Re_express_cnj[of B])
apply (subst Im_express_cnj[of B])
apply (simp add: vec_cnj_def)
apply (simp add: field_simps)
done
hence "Re (6*A + 4*Re B + 4*Im B) = 0"
by simp
hence "3*Re A + 2*Re B + 2*Im B = 0"
using ‹is_real A›
by simp
hence "3/2 + Re B/Re A + Im B/Re A = 0"
using ‹Re A ≠ 0›
by (simp add: field_simps)
hence "-Im B/Re A - 3/2 < -1"
using ‹Re B / Re A < -1›
by simp
hence "Im B/Re A > -1/2"
by (simp add: field_simps)
thus "¬ intersects_y_axis_positive_cmat H"
using *
by simp
qed
lemma negated_euclidean_axiom:
shows "∃ a b c d t.
a ∈ unit_disc ∧ b ∈ unit_disc ∧ c ∈ unit_disc ∧ d ∈ unit_disc ∧ t ∈ unit_disc ∧
poincare_between a d t ∧ poincare_between b d c ∧ a ≠ d ∧
(∀ x y. x ∈ unit_disc ∧ y ∈ unit_disc ∧
poincare_between a b x ∧ poincare_between x t y ⟶ ¬ poincare_between a c y)"
proof-
let ?a = "0⇩h"
let ?b = "of_complex (1/2)"
let ?c = "of_complex (𝗂/2)"
let ?dl = "(5 - sqrt 17) / 4"
let ?d = "of_complex (?dl + 𝗂*?dl)"
let ?t = "of_complex (1/2 + 𝗂/2)"
have "?dl ≠ 0"
proof-
have "(sqrt 17)⇧2 ≠ 5⇧2"
by simp
hence "sqrt 17 ≠ 5"
by force
thus ?thesis
by simp
qed
have "?d ≠ ?a"
proof (rule ccontr)
assume "¬ ?thesis"
hence "?dl + 𝗂*?dl = 0"
by simp
hence "Re (?dl + 𝗂*?dl) = 0"
by simp
thus False
using ‹?dl ≠ 0›
by simp
qed
have "?dl > 0"
proof-
have "(sqrt 17)⇧2 < 5⇧2"
by (simp add: power2_eq_square)
hence "sqrt 17 < 5"
by (rule power2_less_imp_less, simp)
thus ?thesis
by simp
qed
have "?a ≠ ?b"
by (metis divide_eq_0_iff of_complex_zero_iff zero_neq_numeral zero_neq_one)
have "?a ≠ ?c"
by (metis complex_i_not_zero divide_eq_0_iff of_complex_zero_iff zero_neq_numeral)
show ?thesis
proof (rule_tac x="?a" in exI, rule_tac x="?b" in exI, rule_tac x="?c" in exI, rule_tac x="?d" in exI, rule_tac x="?t" in exI, safe)
show "?a ∈ unit_disc" "?b ∈ unit_disc" "?c ∈ unit_disc" "?t ∈ unit_disc"
by (auto simp add: cmod_def power2_eq_square)
have cmod_d: "cmod (?dl + 𝗂*?dl) = ?dl * sqrt 2"
using ‹?dl > 0›
unfolding cmod_def
by (simp add: real_sqrt_mult)
show "?d ∈ unit_disc"
proof-
have "?dl < 1 / sqrt 2"
proof-
have "17⇧2 < (5 * sqrt 17)⇧2"
by (simp add: field_simps)
hence "17 < 5 * sqrt 17"
by (rule power2_less_imp_less, simp)
hence "?dl⇧2 < (1 / sqrt 2)⇧2"
by (simp add: power2_eq_square field_simps)
thus "?dl < 1 / sqrt 2"
by (rule power2_less_imp_less, simp)
qed
thus ?thesis
using cmod_d
by (simp add: field_simps)
qed
have cmod_d: "1 - (cmod (to_complex ?d))⇧2 = (-17 + 5*sqrt 17) / 4" (is "_ = ?cmod_d")
apply (simp only: to_complex_of_complex)
apply (subst cmod_d)
apply (simp add: power_mult_distrib)
apply (simp add: power2_eq_square field_simps)
done
have cmod_d_c: "(cmod (to_complex ?d - to_complex ?c))⇧2 = (17 - 4*sqrt 17) / 4" (is "_ = ?cmod_dc")
unfolding cmod_square
by (simp add: field_simps)
have cmod_c: "1 - (cmod (to_complex ?c))⇧2 = 3/4" (is "_ = ?cmod_c")
by (simp add: power2_eq_square)
have xx: "⋀ x::real. x + x = 2*x"
by simp
have "cmod ((to_complex ?b) - (to_complex ?d)) = cmod ((to_complex ?d) - (to_complex ?c))"
by (simp add: cmod_def power2_eq_square field_simps)
moreover
have "cmod (to_complex ?b) = cmod (to_complex ?c)"
by simp
ultimately
have *: "poincare_distance_formula' (to_complex ?b) (to_complex ?d) =
poincare_distance_formula' (to_complex ?d) (to_complex ?c)"
unfolding poincare_distance_formula'_def
by simp
have **: "poincare_distance_formula' (to_complex ?d) (to_complex ?c) = (sqrt 17) / 3"
unfolding poincare_distance_formula'_def
proof (subst cmod_d, subst cmod_c, subst cmod_d_c)
have "(sqrt 17 * 15)⇧2 ≠ 51⇧2"
by simp
hence "sqrt 17 * 15 ≠ 51"
by force
hence "sqrt 17 * 15 - 51 ≠ 0"
by simp
have "(5 * sqrt 17)⇧2 ≠ 17⇧2"
by simp
hence "5 * sqrt 17 ≠ 17"
by force
hence "?cmod_d * ?cmod_c ≠ 0"
by simp
hence "1 + 2 * (?cmod_dc / (?cmod_d * ?cmod_c)) = (?cmod_d * ?cmod_c + 2 * ?cmod_dc) / (?cmod_d * ?cmod_c)"
using add_frac_num[of "?cmod_d * ?cmod_c" "2 * ?cmod_dc" 1]
by (simp add: field_simps)
also have "... = (64 * (85 - sqrt 17 * 17)) / (64 * (sqrt 17 * 15 - 51))"
by (simp add: field_simps)
also have "... = (85 - sqrt 17 * 17) / (sqrt 17 * 15 - 51)"
by (rule mult_divide_mult_cancel_left, simp)
also have "... = sqrt 17 / 3"
by (subst frac_eq_eq, fact, simp, simp add: field_simps)
finally
show "1 + 2 * (?cmod_dc / (?cmod_d * ?cmod_c)) = sqrt 17 / 3"
.
qed
have "sqrt 17 ≥ 3"
proof-
have "(sqrt 17)⇧2 ≥ 3⇧2"
by simp
thus ?thesis
by (rule power2_le_imp_le, simp)
qed
thus "poincare_between ?b ?d ?c"
unfolding poincare_between_sum_distances[OF ‹?b ∈ unit_disc› ‹?d ∈ unit_disc› ‹?c ∈ unit_disc›]
unfolding poincare_distance_formula[OF ‹?b ∈ unit_disc› ‹?d ∈ unit_disc›]
unfolding poincare_distance_formula[OF ‹?d ∈ unit_disc› ‹?c ∈ unit_disc›]
unfolding poincare_distance_formula[OF ‹?b ∈ unit_disc› ‹?c ∈ unit_disc›]
unfolding poincare_distance_formula_def
apply (subst *, subst xx, subst **, subst arcosh_double)
apply (simp_all add: cmod_def power2_eq_square)
done
show "poincare_between ?a ?d ?t"
proof (subst poincare_between_0uv[OF ‹?d ∈ unit_disc› ‹?t ∈ unit_disc› ‹?d ≠ ?a›])
show "?t ≠ 0⇩h"
proof (rule ccontr)
assume "¬ ?thesis"
hence "1/2 + 𝗂/2 = 0"
by simp
hence "Re (1/2 + 𝗂/2) = 0"
by simp
thus False
by simp
qed
next
have "19⇧2 ≤ (5 * sqrt 17)⇧2"
by simp
hence "19 ≤ 5 * sqrt 17"
by (rule power2_le_imp_le, simp)
hence "cmod (to_complex ?d) ≤ cmod (to_complex ?t)"
by (simp add: Let_def cmod_def power2_eq_square field_simps)
moreover
have "Arg (to_complex ?d) = Arg (to_complex ?t)"
proof-
have 1: "to_complex ?d = ((5 - sqrt 17) / 4) * (1 + 𝗂)"
by (simp add: field_simps)
have 2: "to_complex ?t = (cor (1/2)) * (1 + 𝗂)"
by (simp add: field_simps)
have "(sqrt 17)⇧2 < 5⇧2"
by simp
hence "sqrt 17 < 5"
by (rule power2_less_imp_less, simp)
hence 3: "(5 - sqrt 17) / 4 > 0"
by simp
have 4: "(1::real) / 2 > 0"
by simp
show ?thesis
apply (subst 1, subst 2)
apply (subst arg_mult_real_positive[OF 3])
apply (subst arg_mult_real_positive[OF 4])
by simp
qed
ultimately
show "let d' = to_complex ?d; t' = to_complex ?t in Arg d' = Arg t' ∧ cmod d' ≤ cmod t'"
by simp
qed
show "?a = ?d ⟹ False"
using ‹?d ≠ ?a›
by simp
fix x y
assume "x ∈ unit_disc" "y ∈ unit_disc"
assume abx: "poincare_between ?a ?b x"
hence "x ∈ circline_set x_axis"
using poincare_between_poincare_line_uvz[of ?a ?b x] ‹x ∈ unit_disc› ‹?a ≠ ?b›
using poincare_line_0_real_is_x_axis[of ?b]
by (auto simp add: circline_set_x_axis)
have "x ≠ 0⇩h"
using abx poincare_between_sandwich[of ?a ?b] ‹?a ≠ ?b›
by auto
have "x ∈ positive_x_axis"
using ‹x ∈ circline_set x_axis› ‹x ≠ 0⇩h› ‹x ∈ unit_disc›
using abx poincare_between_x_axis_0uv[of "1/2" "Re (to_complex x)"]
unfolding circline_set_x_axis positive_x_axis_def
by (auto simp add: cmod_eq_Re abs_less_iff complex_eq_if_Re_eq)
assume acy: "poincare_between ?a ?c y"
hence "y ∈ circline_set y_axis"
using poincare_between_poincare_line_uvz[of ?a ?c y] ‹y ∈ unit_disc› ‹?a ≠ ?c›
using poincare_line_0_imag_is_y_axis[of ?c]
by (auto simp add: circline_set_y_axis)
have "y ≠ 0⇩h"
using acy poincare_between_sandwich[of ?a ?c] ‹?a ≠ ?c›
by auto
have "y ∈ positive_y_axis"
proof-
have " ⋀x. ⟦x ≠ 0; poincare_between 0⇩h (of_complex (𝗂 / 2)) (of_complex x); is_imag x; - 1 < Im x⟧ ⟹ 0 < Im x"
by (smt add.left_neutral complex.expand divide_complex_def complex_eq divide_less_0_1_iff divide_less_eq_1_pos imaginary_unit.simps(1) mult.left_neutral of_real_1 of_real_add of_real_divide of_real_eq_0_iff one_add_one poincare_between_y_axis_0uv zero_complex.simps(1) zero_complex.simps(2) zero_less_divide_1_iff)
thus ?thesis
using ‹y ∈ circline_set y_axis› ‹y ≠ 0⇩h› ‹y ∈ unit_disc›
using acy
unfolding circline_set_y_axis positive_y_axis_def
by (auto simp add: cmod_eq_Im abs_less_iff)
qed
have "x ≠ y"
using ‹x ∈ positive_x_axis› ‹y ∈ positive_y_axis›
unfolding positive_x_axis_def positive_y_axis_def circline_set_x_axis circline_set_y_axis
by auto
assume xty: "poincare_between x ?t y"
let ?xy = "poincare_line x y"
have "?t ∈ circline_set ?xy"
using xty poincare_between_poincare_line_uzv[OF ‹x ≠ y› ‹x ∈ unit_disc› ‹y ∈ unit_disc› ‹?t ∈ unit_disc›]
by simp
moreover
have "?xy ≠ x_axis"
using poincare_line_circline_set[OF ‹x ≠ y›] ‹y ∈ positive_y_axis›
by (auto simp add: circline_set_x_axis positive_y_axis_def)
hence "intersects_x_axis_positive ?xy"
using intersects_x_axis_positive_iff[of "?xy"] ‹x ≠ y› ‹x ∈ unit_disc› ‹x ∈ positive_x_axis›
by auto
moreover
have "?xy ≠ y_axis"
using poincare_line_circline_set[OF ‹x ≠ y›] ‹x ∈ positive_x_axis›
by (auto simp add: circline_set_y_axis positive_x_axis_def)
hence "intersects_y_axis_positive ?xy"
using intersects_y_axis_positive_iff[of "?xy"] ‹x ≠ y› ‹y ∈ unit_disc› ‹y ∈ positive_y_axis›
by auto
ultimately
show False
using negated_euclidean_axiom_aux[of ?xy] ‹x ≠ y›
unfolding circline_set_def
by auto
qed
qed
text ‹Alternate form of the Euclidean axiom -- this one is much easier to prove›
lemma negated_euclidean_axiom':
shows "∃ a b c.
a ∈ unit_disc ∧ b ∈ unit_disc ∧ c ∈ unit_disc ∧ ¬(poincare_collinear {a, b, c}) ∧
¬(∃ x. x ∈ unit_disc ∧
poincare_distance a x = poincare_distance b x ∧
poincare_distance a x = poincare_distance c x)"
proof-
let ?a = "of_complex (𝗂/2)"
let ?b = "of_complex (-𝗂/2)"
let ?c = "of_complex (1/5)"
have "(𝗂/2) ≠ (-𝗂/2)"
by simp
hence "?a ≠ ?b"
by (metis to_complex_of_complex)
have "(𝗂/2) ≠ (1/5)"
by simp
hence "?a ≠ ?c"
by (metis to_complex_of_complex)
have "(-𝗂/2) ≠ (1/5)"
by (simp add: minus_equation_iff)
hence "?b ≠ ?c"
by (metis to_complex_of_complex)
have "?a ∈ unit_disc" "?b ∈ unit_disc" "?c ∈ unit_disc"
by auto
moreover
have "¬(poincare_collinear {?a, ?b, ?c})"
unfolding poincare_collinear_def
proof(rule ccontr)
assume " ¬ (∄p. is_poincare_line p ∧ {?a, ?b, ?c} ⊆ circline_set p)"
then obtain p where "is_poincare_line p ∧ {?a, ?b, ?c} ⊆ circline_set p"
by auto
let ?ab = "poincare_line ?a ?b"
have "p = ?ab"
using ‹is_poincare_line p ∧ {?a, ?b, ?c} ⊆ circline_set p›
using unique_poincare_line[of ?a ?b] ‹?a ≠ ?b› ‹?a ∈ unit_disc› ‹?b ∈ unit_disc›
by auto
have "?c ∉ circline_set ?ab"
proof(rule ccontr)
assume "¬ ?c ∉ circline_set ?ab"
have "poincare_between ?a 0⇩h ?b"
unfolding poincare_between_def
using cross_ratio_0inf by auto
hence "0⇩h ∈ circline_set ?ab"
using ‹?a ≠ ?b› ‹?a ∈ unit_disc› ‹?b ∈ unit_disc›
using poincare_between_poincare_line_uzv zero_in_unit_disc
by blast
hence "?ab = poincare_line 0⇩h ?a"
using unique_poincare_line[of ?a ?b] ‹?a ≠ ?b› ‹?a ∈ unit_disc› ‹?b ∈ unit_disc›
using ‹is_poincare_line p ∧ {?a, ?b, ?c} ⊆ circline_set p›
using ‹p = ?ab› poincare_line_circline_set(1) unique_poincare_line
by (metis add.inverse_neutral divide_minus_left of_complex_zero_iff zero_in_unit_disc)
hence "(𝗂/2) * cnj(1/5) = cnj(𝗂/2) * (1/5)"
using poincare_collinear_zero_iff[of "(𝗂/2)" "(1/5)"]
using ‹?a ≠ ?c› ‹¬ ?c ∉ circline_set ?ab› ‹?a ∈ unit_disc› ‹?c ∈ unit_disc› ‹p = ?ab›
using ‹0⇩h ∈ circline_set ?ab› ‹is_poincare_line p ∧ {?a, ?b, ?c} ⊆ circline_set p›
using poincare_collinear_def by auto
thus False
by simp
qed
thus False
using ‹p = ?ab› ‹is_poincare_line p ∧ {?a, ?b, ?c} ⊆ circline_set p›
by auto
qed
moreover
have "¬(∃ x. x ∈ unit_disc ∧
poincare_distance ?a x = poincare_distance ?b x ∧
poincare_distance ?a x = poincare_distance ?c x)"
proof(rule ccontr)
assume "¬ ?thesis"
then obtain x where "x ∈ unit_disc" "poincare_distance ?a x = poincare_distance ?b x"
"poincare_distance ?a x = poincare_distance ?c x"
by blast
let ?x = "to_complex x"
have "poincare_distance_formula' (𝗂/2) ?x = poincare_distance_formula' (-𝗂/2) ?x"
using ‹poincare_distance ?a x = poincare_distance ?b x›
using ‹x ∈ unit_disc› ‹?a ∈ unit_disc› ‹?b ∈ unit_disc›
by (metis cosh_dist to_complex_of_complex)
hence "(cmod (𝗂 / 2 - ?x))⇧2 = (cmod (- 𝗂 / 2 - ?x))⇧2"
unfolding poincare_distance_formula'_def
apply (simp add:field_simps)
using ‹x ∈ unit_disc› unit_disc_cmod_square_lt_1 by fastforce
hence "Im ?x = 0"
unfolding cmod_def
by (simp add: power2_eq_iff)
have "1 - (Re ?x)⇧2 ≠ 0"
using ‹x ∈ unit_disc› unit_disc_cmod_square_lt_1
using cmod_power2 by force
hence "24 - 24 * (Re ?x)⇧2 ≠ 0"
by simp
have "poincare_distance_formula' (𝗂/2) ?x = poincare_distance_formula' (1/5) ?x"
using ‹poincare_distance ?a x = poincare_distance ?c x›
using ‹x ∈ unit_disc› ‹?a ∈ unit_disc› ‹?c ∈ unit_disc›
by (metis cosh_dist to_complex_of_complex)
hence "(2 + 8 * (Re ?x)⇧2) /(3 - 3 * (Re ?x)⇧2) = 2 * (1 - Re ?x * 5)⇧2 / (24 - 24 * (Re ?x)⇧2)" (is "?lhs = ?rhs")
unfolding poincare_distance_formula'_def
apply (simp add:field_simps)
unfolding cmod_def
using ‹Im ?x = 0›
by (simp add:field_simps)
hence *: "?lhs * (24 - 24 * (Re ?x)⇧2) = ?rhs * (24 - 24 * (Re ?x)⇧2) "
using ‹(24 - 24 * (Re ?x)⇧2) ≠ 0›
by simp
have "?lhs * (24 - 24 * (Re ?x)⇧2) = (2 + 8 * (Re ?x)⇧2) * 8"
using ‹(24 - 24 * (Re ?x)⇧2) ≠ 0› ‹1 - (Re ?x)⇧2 ≠ 0›
by (simp add:field_simps)
have "?rhs * (24 - 24 * (Re ?x)⇧2) = 2 * (1 - Re ?x * 5)⇧2"
using ‹(24 - 24 * (Re ?x)⇧2) ≠ 0› ‹1 - (Re ?x)⇧2 ≠ 0›
by (simp add:field_simps)
hence "(2 + 8 * (Re ?x)⇧2) * 8 = 2 * (1 - Re ?x * 5)⇧2"
using * ‹?lhs * (24 - 24 * (Re ?x)⇧2) = (2 + 8 * (Re ?x)⇧2) * 8›
by simp
hence "7 * (Re ?x)⇧2 + 10 * (Re ?x) + 7 = 0"
by (simp add:field_simps comm_ring_1_class.power2_diff)
thus False
using discriminant_iff[of 7 "Re (to_complex x)" 10 7] discrim_def[of 7 10 7]
by auto
qed
ultimately show ?thesis
apply (rule_tac x="?a" in exI)
apply (rule_tac x="?b" in exI)
apply (rule_tac x="?c" in exI)
by auto
qed
subsection‹Continuity axiom›
text ‹The set $\phi$ is on the left of the set $\psi$›
abbreviation set_order where
"set_order A φ ψ ≡ ∀x∈ unit_disc. ∀y∈ unit_disc. φ x ∧ ψ y ⟶ poincare_between A x y"
text ‹The point $B$ is between the sets $\phi$ and $\psi$›
abbreviation point_between_sets where
"point_between_sets φ B ψ ≡ ∀x∈ unit_disc. ∀y∈ unit_disc. φ x ∧ ψ y ⟶ poincare_between x B y"
lemma continuity:
assumes "∃ A ∈ unit_disc. set_order A φ ψ"
shows "∃ B ∈ unit_disc. point_between_sets φ B ψ"
proof (cases "(∃ x0 ∈ unit_disc. φ x0) ∧ (∃ y0 ∈ unit_disc. ψ y0)")
case False
thus ?thesis
using assms by blast
next
case True
then obtain Y0 where "ψ Y0" "Y0 ∈ unit_disc"
by auto
obtain A where *: "A ∈ unit_disc" "set_order A φ ψ"
using assms
by auto
show ?thesis
proof(cases "∀ x ∈ unit_disc. φ x ⟶ x = A")
case True
thus ?thesis
using ‹A ∈ unit_disc›
using poincare_between_nonstrict(1) by blast
next
case False
then obtain X0 where "φ X0" "X0 ≠ A" "X0 ∈ unit_disc"
by auto
have "Y0 ≠ A"
proof(rule ccontr)
assume "¬ Y0 ≠ A"
hence "∀ x ∈ unit_disc. φ x ⟶ poincare_between A x A"
using * ‹ψ Y0›
by (cases A) force
hence "∀ x ∈ unit_disc. φ x ⟶ x = A"
using * poincare_between_sandwich by blast
thus False
using False by auto
qed
show ?thesis
proof (cases "∃ B ∈ unit_disc. φ B ∧ ψ B")
case True
then obtain B where "B ∈ unit_disc" "φ B" "ψ B"
by auto
hence "∀ x ∈ unit_disc. φ x ⟶ poincare_between A x B"
using * by auto
have "∀ y ∈ unit_disc. ψ y ⟶ poincare_between A B y"
using * ‹B ∈ unit_disc› ‹φ B›
by auto
show ?thesis
proof(rule+)
show "B ∈ unit_disc"
by fact
next
fix x y
assume "x ∈ unit_disc" "y ∈ unit_disc" "φ x ∧ ψ y"
hence "poincare_between A x B" "poincare_between A B y"
using ‹∀ x ∈ unit_disc. φ x ⟶ poincare_between A x B›
using ‹∀ y ∈ unit_disc. ψ y ⟶ poincare_between A B y›
by simp+
thus "poincare_between x B y"
using ‹x ∈ unit_disc› ‹y ∈ unit_disc› ‹B ∈ unit_disc› ‹A ∈ unit_disc›
using poincare_between_transitivity[of A x B y]
by simp
qed
next
case False
have "poincare_between A X0 Y0"
using ‹φ X0› ‹ψ Y0› * ‹Y0 ∈ unit_disc› ‹X0 ∈ unit_disc›
by auto
have "∀ φ. ∀ ψ. set_order A φ ψ ∧ ¬ (∃ B ∈ unit_disc. φ B ∧ ψ B) ∧ φ X0 ∧
(∃ y ∈ unit_disc. ψ y) ∧ (∃ x ∈ unit_disc. φ x)
⟶ (∃ B ∈ unit_disc. point_between_sets φ B ψ)"
(is "?P A X0")
proof (rule wlog_positive_x_axis[where P="?P"])
show "A ∈ unit_disc"
by fact
next
show "X0 ∈ unit_disc"
by fact
next
show "A ≠ X0"
using ‹X0 ≠ A› by simp
next
fix M u v
let ?M = "λ x. moebius_pt M x"
let ?Mu = "?M u" and ?Mv = "?M v"
assume hip: "unit_disc_fix M" "u ∈ unit_disc" "v ∈ unit_disc" "u ≠ v"
"?P ?Mu ?Mv"
show "?P u v"
proof safe
fix φ ψ x y
assume "set_order u φ ψ" "¬ (∃B∈unit_disc. φ B ∧ ψ B)" "φ v"
"y ∈ unit_disc" "ψ y" "x ∈ unit_disc" "φ x"
let ?Mφ = "λ X'. ∃ X. φ X ∧ ?M X = X'"
let ?Mψ = "λ X'. ∃ X. ψ X ∧ ?M X = X'"
obtain Mφ where "Mφ = ?Mφ" by simp
obtain Mψ where "Mψ = ?Mψ" by simp
have "Mφ ?Mv"
using ‹φ v› using ‹Mφ = ?Mφ›
by blast
moreover
have "¬ (∃ B ∈unit_disc. Mφ B ∧ Mψ B)"
using ‹¬ (∃B∈unit_disc. φ B ∧ ψ B)›
using ‹Mφ = ?Mφ› ‹Mψ = ?Mψ›
by (metis hip(1) moebius_pt_invert unit_disc_fix_discI unit_disc_fix_moebius_inv)
moreover
have "∃ y ∈ unit_disc. Mψ y"
using ‹y ∈ unit_disc› ‹ψ y› ‹Mψ = ?Mψ› ‹unit_disc_fix M›
by auto
moreover
have "set_order ?Mu ?Mφ ?Mψ"
proof ((rule ballI)+, rule impI)
fix Mx My
assume "Mx ∈ unit_disc" "My ∈ unit_disc" "?Mφ Mx ∧ ?Mψ My"
then obtain x y where "φ x ∧ ?M x = Mx" "ψ y ∧ ?M y = My"
by blast
hence "x ∈ unit_disc" "y ∈ unit_disc"
using ‹Mx ∈ unit_disc› ‹My ∈ unit_disc› ‹unit_disc_fix M›
by (metis moebius_pt_comp_inv_left unit_disc_fix_discI unit_disc_fix_moebius_inv)+
hence "poincare_between u x y"
using ‹set_order u φ ψ›
using ‹Mx ∈ unit_disc› ‹My ∈ unit_disc› ‹φ x ∧ ?M x = Mx› ‹ψ y ∧ ?M y = My›
by blast
then show "poincare_between ?Mu Mx My"
using ‹φ x ∧ ?M x = Mx› ‹ψ y ∧ ?M y = My›
using ‹x ∈ unit_disc› ‹y ∈ unit_disc› ‹u ∈ unit_disc› ‹unit_disc_fix M›
using unit_disc_fix_moebius_preserve_poincare_between by blast
qed
hence "set_order ?Mu Mφ Mψ"
using ‹Mφ = ?Mφ› ‹Mψ = ?Mψ›
by simp
ultimately
have "∃ Mb ∈ unit_disc. point_between_sets Mφ Mb Mψ"
using hip(5)
by blast
then obtain Mb where bbb:
"Mb ∈ unit_disc" "point_between_sets ?Mφ Mb ?Mψ"
using ‹Mφ = ?Mφ› ‹Mψ = ?Mψ›
by auto
let ?b = "moebius_pt (moebius_inv M) Mb"
show "∃ b ∈ unit_disc. point_between_sets φ b ψ"
proof (rule_tac x="?b" in bexI, (rule ballI)+, rule impI)
fix x y
assume "x ∈ unit_disc" "y ∈ unit_disc" "φ x ∧ ψ y"
hence "poincare_between u x y"
using ‹set_order u φ ψ›
by blast
let ?Mx = "?M x" and ?My = "?M y"
have "?Mφ ?Mx" "?Mψ ?My"
using ‹φ x ∧ ψ y›
by blast+
have "?Mx ∈ unit_disc" "?My ∈ unit_disc"
using ‹x ∈ unit_disc› ‹unit_disc_fix M› ‹y ∈ unit_disc›
by auto
hence "poincare_between ?Mx Mb ?My"
using ‹?Mφ ?Mx› ‹?Mψ ?My› ‹?Mx ∈ unit_disc› ‹?My ∈ unit_disc› bbb
by auto
then show "poincare_between x ?b y"
using ‹unit_disc_fix M›
using ‹x ∈ unit_disc› ‹y ∈ unit_disc› ‹Mb ∈ unit_disc› ‹?Mx ∈ unit_disc› ‹?My ∈ unit_disc›
using unit_disc_fix_moebius_preserve_poincare_between[of M x ?b y]
by auto
next
show "?b ∈ unit_disc"
using bbb ‹unit_disc_fix M›
by auto
qed
qed
next
fix X
assume xx: "is_real X" "0 < Re X" "Re X < 1"
let ?X = "of_complex X"
show "?P 0⇩h ?X"
proof ((rule allI)+, rule impI, (erule conjE)+)
fix φ ψ
assume "set_order 0⇩h φ ψ" "¬ (∃B∈unit_disc. φ B ∧ ψ B)" "φ ?X"
"∃y∈unit_disc. ψ y" "∃x∈unit_disc. φ x"
have "?X ∈ unit_disc"
using xx
by (simp add: cmod_eq_Re)
have ψpos: "∀ y ∈ unit_disc. ψ y ⟶ (is_real (to_complex y) ∧ Re (to_complex y) > 0)"
proof(rule ballI, rule impI)
fix y
let ?y = "to_complex y"
assume "y ∈ unit_disc" "ψ y"
hence "poincare_between 0⇩h ?X y"
using ‹set_order 0⇩h φ ψ›
using ‹?X ∈ unit_disc› ‹φ ?X›
by auto
thus "is_real ?y ∧ 0 < Re ?y"
using xx ‹?X ∈ unit_disc› ‹y ∈ unit_disc›
by (metis (mono_tags, opaque_lifting) arg_0_iff of_complex_zero_iff poincare_between_0uv poincare_between_sandwich to_complex_of_complex unit_disc_to_complex_inj zero_in_unit_disc)
qed
have φnoneg: "∀ x ∈ unit_disc. φ x ⟶ (is_real (to_complex x) ∧ Re (to_complex x) ≥ 0)"
proof(rule ballI, rule impI)
fix x
assume "x ∈ unit_disc" "φ x"
obtain y where "y ∈ unit_disc" "ψ y"
using ‹∃ y ∈ unit_disc. ψ y› by blast
let ?x = "to_complex x" and ?y = "to_complex y"
have "is_real ?y" "Re ?y > 0"
using ψpos ‹ψ y› ‹y ∈ unit_disc›
by auto
have "poincare_between 0⇩h x y"
using ‹set_order 0⇩h φ ψ›
using ‹x ∈ unit_disc› ‹φ x› ‹y∈unit_disc› ‹ψ y›
by auto
thus "is_real ?x ∧ 0 ≤ Re ?x"
using ‹x ∈ unit_disc› ‹y ∈ unit_disc› ‹is_real (to_complex y)› ‹ψ y›
using ‹set_order 0⇩h φ ψ›
using ‹φ ?X› ‹?X ∈ unit_disc› ‹Re ?y > 0›
by (metis arg_0_iff le_less of_complex_zero poincare_between_0uv to_complex_of_complex zero_complex.simps(1) zero_complex.simps(2))
qed
have φlessψ: "∀x∈unit_disc. ∀y∈unit_disc. φ x ∧ ψ y ⟶ Re (to_complex x) < Re (to_complex y)"
proof((rule ballI)+, rule impI)
fix x y
let ?x = "to_complex x" and ?y = "to_complex y"
assume "x ∈ unit_disc" "y ∈ unit_disc" "φ x ∧ ψ y"
hence "poincare_between 0⇩h x y"
using ‹set_order 0⇩h φ ψ›
by auto
moreover
have "is_real ?x" "Re ?x ≥ 0"
using φnoneg
using ‹x ∈ unit_disc› ‹φ x ∧ ψ y› by auto
moreover
have "is_real ?y" "Re ?y > 0"
using ψpos
using ‹y ∈ unit_disc› ‹φ x ∧ ψ y› by auto
ultimately
have "Re ?x ≤ Re ?y"
using ‹x ∈ unit_disc› ‹y ∈ unit_disc›
by (metis Re_complex_of_real arg_0_iff le_less of_complex_zero poincare_between_0uv rcis_cmod_Arg rcis_zero_arg to_complex_of_complex)
have "Re ?x ≠ Re ?y"
using ‹φ x ∧ ψ y› ‹is_real ?x› ‹is_real ?y›
using ‹¬ (∃B∈unit_disc. φ B ∧ ψ B)› ‹x ∈ unit_disc› ‹y ∈ unit_disc›
by (metis complex.expand unit_disc_to_complex_inj)
thus "Re ?x < Re ?y"
using ‹Re ?x ≤ Re ?y› by auto
qed
have "∃ b ∈ unit_disc. ∀ x ∈ unit_disc. ∀ y ∈ unit_disc.
is_real (to_complex b) ∧
(φ x ∧ ψ y ⟶ (Re (to_complex x) ≤ Re (to_complex b) ∧ Re (to_complex b) ≤ Re (to_complex y)))"
proof-
let ?Phi = "{x. (of_complex (cor x)) ∈ unit_disc ∧ φ (of_complex (cor x))}"
have "∀ x ∈ unit_disc. φ x ⟶ Re (to_complex x) ≤ Sup ?Phi"
proof(safe)
fix x
let ?x = "to_complex x"
assume "x ∈ unit_disc" "φ x"
hence "is_real ?x" "Re ?x ≥ 0"
using φnoneg
by auto
hence "cor (Re ?x) = ?x"
using complex_of_real_Re by blast
hence "of_complex (cor (Re ?x)) ∈ unit_disc"
using ‹x ∈ unit_disc›
by (metis inf_notin_unit_disc of_complex_to_complex)
moreover
have "φ (of_complex (cor (Re ?x)))"
using ‹cor (Re ?x) = ?x› ‹φ x› ‹x ∈ unit_disc›
by (metis inf_notin_unit_disc of_complex_to_complex)
ultimately
have "Re ?x ∈ ?Phi"
by auto
have "∃M. ∀x ∈ ?Phi. x ≤ M"
using φlessψ
using ‹∃ y ∈ unit_disc. ψ y›
by (metis (mono_tags, lifting) Re_complex_of_real le_less mem_Collect_eq to_complex_of_complex)
thus "Re ?x ≤ Sup ?Phi"
using cSup_upper[of "Re ?x" ?Phi]
unfolding bdd_above_def
using ‹Re ?x ∈ ?Phi›
by auto
qed
have "∀ y ∈ unit_disc. ψ y ⟶ Sup ?Phi ≤ Re (to_complex y)"
proof (safe)
fix y
let ?y = "to_complex y"
assume "ψ y" "y ∈ unit_disc"
show "Sup ?Phi ≤ Re ?y"
proof (rule ccontr)
assume "¬ ?thesis"
hence "Re ?y < Sup ?Phi"
by auto
have "∃ x. φ (of_complex (cor x)) ∧ (of_complex (cor x)) ∈ unit_disc"
proof -
obtain x' where "x' ∈ unit_disc" "φ x'"
using ‹∃ x ∈ unit_disc. φ x› by blast
let ?x' = "to_complex x'"
have "is_real ?x'"
using ‹x' ∈ unit_disc› ‹φ x'›
using φnoneg
by auto
hence "cor (Re ?x') = ?x'"
using complex_of_real_Re by blast
hence "x' = of_complex (cor (Re ?x'))"
using ‹x' ∈ unit_disc›
by (metis inf_notin_unit_disc of_complex_to_complex)
show ?thesis
apply (rule_tac x="Re ?x'" in exI)
using ‹x' ∈ unit_disc›
apply (subst (asm) ‹x' = of_complex (cor (Re ?x'))›, simp)
using ‹φ x'›
by (subst (asm) (2) ‹x' = of_complex (cor (Re ?x'))›, simp)
qed
hence "?Phi ≠ {}"
by auto
then obtain x where "φ (of_complex (cor x))" "Re ?y < x"
"(of_complex (cor x)) ∈ unit_disc"
using ‹Re ?y < Sup ?Phi›
using less_cSupE[of "Re ?y" ?Phi]
by auto
moreover
have "Re ?y < Re (to_complex (of_complex (cor x)))"
using ‹Re ?y < x›
by simp
ultimately
show False
using φlessψ
using ‹ψ y› ‹y ∈ unit_disc›
by (metis less_not_sym)
qed
qed
thus ?thesis
using ‹∀ x ∈ unit_disc. φ x ⟶ Re (to_complex x) ≤ Sup ?Phi›
apply (rule_tac x="(of_complex (cor (Sup ?Phi)))" in bexI, simp)
using ‹∃y∈unit_disc. ψ y› ‹φ ?X› ‹?X ∈ unit_disc›
using ‹∀y∈unit_disc. ψ y ⟶ is_real (to_complex y) ∧ 0 < Re (to_complex y)›
by (smt complex_of_real_Re inf_notin_unit_disc norm_of_real of_complex_to_complex to_complex_of_complex unit_disc_iff_cmod_lt_1 xx(2))
qed
then obtain B where "B ∈ unit_disc" "is_real (to_complex B)"
"∀x∈unit_disc. ∀y∈unit_disc. φ x ∧ ψ y ⟶ Re (to_complex x) ≤ Re (to_complex B) ∧
Re (to_complex B) ≤ Re (to_complex y)"
by blast
show "∃ b ∈ unit_disc. point_between_sets φ b ψ"
proof (rule_tac x="B" in bexI)
show "B ∈ unit_disc"
by fact
next
show "point_between_sets φ B ψ"
proof ((rule ballI)+, rule impI)
fix x y
let ?x = "to_complex x" and ?y = "to_complex y" and ?B = "to_complex B"
assume "x ∈ unit_disc" "y ∈ unit_disc" "φ x ∧ ψ y"
hence "Re ?x ≤ Re ?B ∧ Re ?B ≤ Re ?y"
using ‹∀x∈unit_disc. ∀y∈unit_disc. φ x ∧ ψ y ⟶ Re (to_complex x) ≤ Re ?B ∧
Re (to_complex B) ≤ Re (to_complex y)›
by auto
moreover
have "is_real ?x" "Re ?x ≥ 0"
using φnoneg
using ‹x ∈ unit_disc› ‹φ x ∧ ψ y›
by auto
moreover
have "is_real ?y" "Re ?y > 0"
using ψpos
using ‹y ∈ unit_disc› ‹φ x ∧ ψ y›
by auto
moreover
have "cor (Re ?x) = ?x"
using complex_of_real_Re ‹is_real ?x› by blast
hence "x = of_complex (cor (Re ?x))"
using ‹x ∈ unit_disc›
by (metis inf_notin_unit_disc of_complex_to_complex)
moreover
have "cor (Re ?y) = ?y"
using complex_of_real_Re ‹is_real ?y› by blast
hence "y = of_complex (cor (Re ?y))"
using ‹y ∈ unit_disc›
by (metis inf_notin_unit_disc of_complex_to_complex)
moreover
have "cor (Re ?B) = ?B"
using complex_of_real_Re ‹is_real (to_complex B)› by blast
hence "B = of_complex (cor (Re ?B))"
using ‹B ∈ unit_disc›
by (metis inf_notin_unit_disc of_complex_to_complex)
ultimately
show "poincare_between x B y"
using ‹is_real (to_complex B)› ‹x ∈ unit_disc› ‹y ∈ unit_disc› ‹B ∈ unit_disc›
using poincare_between_x_axis_uvw[of "Re (to_complex x)" "Re (to_complex B)" "Re (to_complex y)"]
by (smt Re_complex_of_real arg_0_iff poincare_between_nonstrict(1) rcis_cmod_Arg rcis_zero_arg unit_disc_iff_cmod_lt_1)
qed
qed
qed
qed
thus ?thesis
using False ‹φ X0› ‹ψ Y0› * ‹Y0 ∈ unit_disc› ‹X0 ∈ unit_disc›
by auto
qed
qed
qed
subsection‹Limiting parallels axiom›
text ‹Auxiliary definitions›
definition poincare_on_line where
"poincare_on_line p a b ⟷ poincare_collinear {p, a, b}"
definition poincare_on_ray where
"poincare_on_ray p a b ⟷ poincare_between a p b ∨ poincare_between a b p"
definition poincare_in_angle where
"poincare_in_angle p a b c ⟷
b ≠ a ∧ b ≠ c ∧ p ≠ b ∧ (∃ x ∈ unit_disc. poincare_between a x c ∧ x ≠ a ∧ x ≠ c ∧ poincare_on_ray p b x)"
definition poincare_ray_meets_line where
"poincare_ray_meets_line a b c d ⟷ (∃ x ∈ unit_disc. poincare_on_ray x a b ∧ poincare_on_line x c d)"
text ‹All points on ray are collinear›
lemma poincare_on_ray_poincare_collinear:
assumes "p ∈ unit_disc" and "a ∈ unit_disc" and "b ∈ unit_disc" and "poincare_on_ray p a b"
shows "poincare_collinear {p, a, b}"
using assms poincare_between_poincare_collinear
unfolding poincare_on_ray_def
by (metis insert_commute)
text ‹H-isometries preserve all defined auxiliary relations›
lemma unit_disc_fix_preserves_poincare_on_line [simp]:
assumes "unit_disc_fix M" and "p ∈ unit_disc" "a ∈ unit_disc" "b ∈ unit_disc"
shows "poincare_on_line (moebius_pt M p) (moebius_pt M a) (moebius_pt M b) ⟷ poincare_on_line p a b"
using assms
unfolding poincare_on_line_def
by auto
lemma unit_disc_fix_preserves_poincare_on_ray [simp]:
assumes "unit_disc_fix M" "p ∈ unit_disc" "a ∈ unit_disc" "b ∈ unit_disc"
shows "poincare_on_ray (moebius_pt M p) (moebius_pt M a) (moebius_pt M b) ⟷ poincare_on_ray p a b"
using assms
unfolding poincare_on_ray_def
by auto
lemma unit_disc_fix_preserves_poincare_in_angle [simp]:
assumes "unit_disc_fix M" "p ∈ unit_disc" "a ∈ unit_disc" "b ∈ unit_disc" "c ∈ unit_disc"
shows "poincare_in_angle (moebius_pt M p) (moebius_pt M a) (moebius_pt M b) (moebius_pt M c) ⟷ poincare_in_angle p a b c" (is "?lhs ⟷ ?rhs")
proof
assume "?lhs"
then obtain Mx where *: "Mx ∈ unit_disc"
"poincare_between (moebius_pt M a) Mx (moebius_pt M c)"
"Mx ≠ moebius_pt M a" "Mx ≠ moebius_pt M c" "poincare_on_ray (moebius_pt M p) (moebius_pt M b) Mx"
"moebius_pt M b ≠ moebius_pt M a" "moebius_pt M b ≠ moebius_pt M c" "moebius_pt M p ≠ moebius_pt M b"
unfolding poincare_in_angle_def
by auto
obtain x where "Mx = moebius_pt M x" "x ∈ unit_disc"
by (metis "*"(1) assms(1) image_iff unit_disc_fix_iff)
thus ?rhs
using * assms
unfolding poincare_in_angle_def
by auto
next
assume ?rhs
then obtain x where *: "x ∈ unit_disc"
"poincare_between a x c"
"x ≠ a" "x ≠ c" "poincare_on_ray p b x"
"b ≠ a" "b ≠ c" "p ≠ b"
unfolding poincare_in_angle_def
by auto
thus ?lhs
using assms
unfolding poincare_in_angle_def
by auto (rule_tac x="moebius_pt M x" in bexI, auto)
qed
lemma unit_disc_fix_preserves_poincare_ray_meets_line [simp]:
assumes "unit_disc_fix M" "a ∈ unit_disc" "b ∈ unit_disc" "c ∈ unit_disc" "d ∈ unit_disc"
shows "poincare_ray_meets_line (moebius_pt M a) (moebius_pt M b) (moebius_pt M c) (moebius_pt M d) ⟷ poincare_ray_meets_line a b c d" (is "?lhs ⟷ ?rhs")
proof
assume ?lhs
then obtain Mx where *: "Mx ∈ unit_disc" "poincare_on_ray Mx (moebius_pt M a) (moebius_pt M b)"
"poincare_on_line Mx (moebius_pt M c) (moebius_pt M d)"
unfolding poincare_ray_meets_line_def
by auto
obtain x where "Mx = moebius_pt M x" "x ∈ unit_disc"
by (metis "*"(1) assms(1) image_iff unit_disc_fix_iff)
thus ?rhs
using assms *
unfolding poincare_ray_meets_line_def poincare_on_line_def
by auto
next
assume ?rhs
then obtain x where *: "x ∈ unit_disc" "poincare_on_ray x a b"
"poincare_on_line x c d"
unfolding poincare_ray_meets_line_def
by auto
thus ?lhs
using assms *
unfolding poincare_ray_meets_line_def poincare_on_line_def
by auto (rule_tac x="moebius_pt M x" in bexI, auto)
qed
text ‹H-lines that intersect on the absolute do not meet (they do not share a common h-point)›
lemma tangent_not_meet:
assumes "x1 ∈ unit_disc" and "x2 ∈ unit_disc" and "x1 ≠ x2" and "¬ poincare_collinear {0⇩h, x1, x2}"
assumes "i ∈ ideal_points (poincare_line x1 x2)" "a ∈ unit_disc" "a ≠ 0⇩h" "poincare_collinear {0⇩h, a, i}"
shows "¬ poincare_ray_meets_line 0⇩h a x1 x2"
proof (rule ccontr)
assume "¬ ?thesis"
then obtain x where "x ∈ unit_disc" "poincare_on_ray x 0⇩h a" "poincare_collinear {x, x1, x2}"
unfolding poincare_ray_meets_line_def poincare_on_line_def
by auto
have "poincare_collinear {0⇩h, a, x}"
using ‹poincare_on_ray x 0⇩h a› ‹x ∈ unit_disc› ‹a ∈ unit_disc›
by (meson poincare_between_poincare_collinear poincare_between_rev poincare_on_ray_def poincare_on_ray_poincare_collinear zero_in_unit_disc)
have "x ≠ 0⇩h"
using ‹¬ poincare_collinear {0⇩h, x1, x2}› ‹poincare_collinear {x, x1, x2}›
unfolding poincare_collinear_def
by (auto simp add: assms(2) assms(3) poincare_between_rev)
let ?l1 = "poincare_line 0⇩h a"
let ?l2 = "poincare_line x1 x2"
have "i ∈ circline_set unit_circle"
using ‹i ∈ ideal_points (poincare_line x1 x2)›
using assms(3) ideal_points_on_unit_circle is_poincare_line_poincare_line by blast
have "i ∈ circline_set ?l1"
using ‹poincare_collinear {0⇩h, a, i}›
unfolding poincare_collinear_def
using ‹a ∈ unit_disc› ‹a ≠ 0⇩h›
by (metis insert_subset unique_poincare_line zero_in_unit_disc)
moreover
have "x ∈ circline_set ?l1"
using ‹a ∈ unit_disc› ‹a ≠ 0⇩h› ‹poincare_collinear {0⇩h, a, x}› ‹x ∈ unit_disc›
by (metis poincare_collinear3_between poincare_between_poincare_line_uvz poincare_between_poincare_line_uzv poincare_line_sym zero_in_unit_disc)
moreover
have "inversion x ∈ circline_set ?l1"
using ‹poincare_collinear {0⇩h, a, x}›
using poincare_line_inversion_full[of "0⇩h" a x] ‹a ∈ unit_disc› ‹a ≠ 0⇩h› ‹x ∈ unit_disc›
by (metis poincare_collinear3_between is_poincare_line_inverse_point is_poincare_line_poincare_line poincare_between_poincare_line_uvz poincare_between_poincare_line_uzv poincare_line_sym zero_in_unit_disc)
moreover
have "x ∈ circline_set ?l2"
using ‹poincare_collinear {x, x1, x2}› ‹x1 ≠ x2› ‹x1 ∈ unit_disc› ‹x2 ∈ unit_disc› ‹x ∈ unit_disc›
by (metis insert_commute inversion_noteq_unit_disc poincare_between_poincare_line_uvz poincare_between_poincare_line_uzv poincare_collinear3_iff poincare_line_sym_general)
moreover
hence "inversion x ∈ circline_set ?l2"
using ‹x1 ≠ x2› ‹x1 ∈ unit_disc› ‹x2 ∈ unit_disc› ‹x ∈ unit_disc›
using poincare_line_inversion_full[of x1 x2 x]
unfolding circline_set_def
by auto
moreover
have "i ∈ circline_set ?l2"
using ‹x1 ≠ x2› ‹x1 ∈ unit_disc› ‹x2 ∈ unit_disc›
using ‹i ∈ ideal_points ?l2›
by (simp add: ideal_points_on_circline)
moreover
have "x ≠ inversion x"
using ‹x ∈ unit_disc›
using inversion_noteq_unit_disc by fastforce
moreover
have "x ≠ i"
using ‹x ∈ unit_disc›
using ‹i ∈ circline_set unit_circle› circline_set_def inversion_noteq_unit_disc
by fastforce+
moreover
have "inversion x ≠ i"
using ‹i ∈ circline_set unit_circle› ‹x ≠ i› circline_set_def inversion_unit_circle
by fastforce
ultimately
have "?l1 = ?l2"
using unique_circline_set[of x "inversion x" i]
by blast
hence "0⇩h ∈ circline_set ?l2"
by (metis ‹a ≠ 0⇩h› poincare_line_circline_set(1))
thus False
using ‹¬ poincare_collinear {0⇩h, x1, x2}›
unfolding poincare_collinear_def
using ‹poincare_collinear {x, x1, x2}› ‹x1 ≠ x2› ‹x1 ∈ unit_disc› ‹x2 ∈ unit_disc› poincare_collinear_def unique_poincare_line
by auto
qed
lemma limiting_parallels:
assumes "a ∈ unit_disc" and "x1 ∈ unit_disc" and "x2 ∈ unit_disc" and "¬ poincare_on_line a x1 x2"
shows "∃a1∈unit_disc. ∃a2∈unit_disc.
¬ poincare_on_line a a1 a2 ∧
¬ poincare_ray_meets_line a a1 x1 x2 ∧ ¬ poincare_ray_meets_line a a2 x1 x2 ∧
(∀a'∈unit_disc. poincare_in_angle a' a1 a a2 ⟶ poincare_ray_meets_line a a' x1 x2)" (is "?P a x1 x2")
proof-
have "¬ poincare_collinear {a, x1, x2}"
using ‹¬ poincare_on_line a x1 x2›
unfolding poincare_on_line_def
by simp
have "∀ x1 x2. x1 ∈ unit_disc ∧ x2 ∈ unit_disc ∧ ¬ poincare_collinear {a, x1, x2} ⟶ ?P a x1 x2" (is "?Q a")
proof (rule wlog_zero[OF ‹a ∈ unit_disc›])
fix a u
assume *: "u ∈ unit_disc" "cmod a < 1"
hence uf: "unit_disc_fix (blaschke a)"
by simp
assume **: "?Q (moebius_pt (blaschke a) u)"
show "?Q u"
proof safe
fix x1 x2
let ?M = "moebius_pt (blaschke a)"
assume xx: "x1 ∈ unit_disc" "x2 ∈ unit_disc" "¬ poincare_collinear {u, x1, x2}"
hence MM: "?M x1 ∈ unit_disc ∧ ?M x2∈ unit_disc ∧ ¬ poincare_collinear {?M u, ?M x1, ?M x2}"
using *
by auto
show "?P u x1 x2" (is "∃a1∈unit_disc. ∃a2∈unit_disc. ?P' a1 a2 u x1 x2")
proof-
obtain Ma1 Ma2 where MM: "Ma1 ∈ unit_disc" "Ma2 ∈ unit_disc" "?P' Ma1 Ma2 (?M u) (?M x1) (?M x2)"
using **[rule_format, OF MM]
by blast
hence MM': "∀a'∈unit_disc. poincare_in_angle a' Ma1 (?M u) Ma2 ⟶ poincare_ray_meets_line (?M u) a' (?M x1) (?M x2)"
by auto
obtain a1 a2 where a: "a1 ∈ unit_disc" "a2 ∈ unit_disc" "?M a1 = Ma1" "?M a2 = Ma2"
using uf
by (metis ‹Ma1 ∈ unit_disc› ‹Ma2 ∈ unit_disc› image_iff unit_disc_fix_iff)
have "∀a'∈unit_disc. poincare_in_angle a' a1 u a2 ⟶ poincare_ray_meets_line u a' x1 x2"
proof safe
fix a'
assume "a' ∈ unit_disc" "poincare_in_angle a' a1 u a2"
thus "poincare_ray_meets_line u a' x1 x2"
using MM(1-2) MM'[rule_format, of "?M a'"] * uf a xx
by (meson unit_disc_fix_discI unit_disc_fix_preserves_poincare_in_angle unit_disc_fix_preserves_poincare_ray_meets_line)
qed
hence "?P' a1 a2 u x1 x2"
using MM * uf xx a
by auto
thus ?thesis
using ‹a1 ∈ unit_disc› ‹a2 ∈ unit_disc›
by blast
qed
qed
next
show "?Q 0⇩h"
proof safe
fix x1 x2
assume "x1 ∈ unit_disc" "x2 ∈ unit_disc"
assume "¬ poincare_collinear {0⇩h, x1, x2}"
show "?P 0⇩h x1 x2"
proof-
let ?lx = "poincare_line x1 x2"
have "x1 ≠ x2"
using ‹x1 ∈ unit_disc› ‹x2 ∈ unit_disc›‹¬ poincare_collinear {0⇩h, x1, x2}›
using poincare_collinear3_between
by auto
have lx: "is_poincare_line ?lx"
using is_poincare_line_poincare_line[OF ‹x1 ≠ x2›]
by simp
obtain i1 i2 where "ideal_points ?lx = {i1, i2}"
by (meson ‹x1 ≠ x2› is_poincare_line_poincare_line obtain_ideal_points)
let ?li = "poincare_line i1 i2"
let ?i1 = "to_complex i1"
let ?i2 = "to_complex i2"
have "i1 ∈ unit_circle_set" "i2 ∈ unit_circle_set"
using lx ‹ideal_points ?lx = {i1, i2}›
unfolding unit_circle_set_def
by (metis ideal_points_on_unit_circle insertI1, metis ideal_points_on_unit_circle insertI1 insertI2)
have "i1 ≠ i2"
using ‹ideal_points ?lx = {i1, i2}› ‹x1 ∈ unit_disc› ‹x1 ≠ x2› ‹x2 ∈ unit_disc› ideal_points_different(1)
by blast
let ?a1 = "of_complex (?i1 / 2)"
let ?a2 = "of_complex (?i2 / 2)"
let ?la = "poincare_line ?a1 ?a2"
have "?a1 ∈ unit_disc" "?a2 ∈ unit_disc"
using ‹i1 ∈ unit_circle_set› ‹i2 ∈ unit_circle_set›
unfolding unit_circle_set_def unit_disc_def disc_def circline_set_def
by auto (transfer, transfer, case_tac i1, case_tac i2, simp add: vec_cnj_def)+
have "?a1 ≠ 0⇩h" "?a2 ≠ 0⇩h"
using ‹i1 ∈ unit_circle_set› ‹i2 ∈ unit_circle_set›
unfolding unit_circle_set_def
by auto
have "?a1 ≠ ?a2"
using ‹i1 ≠ i2›
by (metis ‹i1 ∈ unit_circle_set› ‹i2 ∈ unit_circle_set› circline_set_def divide_cancel_right inversion_infty inversion_unit_circle mem_Collect_eq of_complex_to_complex of_complex_zero to_complex_of_complex unit_circle_set_def zero_neq_numeral)
have "poincare_collinear {0⇩h, ?a1, i1}"
unfolding poincare_collinear_def
using ‹?a1 ≠ 0⇩h›[symmetric] is_poincare_line_poincare_line[of "0⇩h" ?a1]
unfolding circline_set_def
apply (rule_tac x="poincare_line 0⇩h ?a1" in exI, auto)
apply (transfer, transfer, auto simp add: vec_cnj_def)
done
have "poincare_collinear {0⇩h, ?a2, i2}"
unfolding poincare_collinear_def
using ‹?a2 ≠ 0⇩h›[symmetric] is_poincare_line_poincare_line[of "0⇩h" ?a2]
unfolding circline_set_def
apply (rule_tac x="poincare_line 0⇩h ?a2" in exI, auto)
apply (transfer, transfer, auto simp add: vec_cnj_def)
done
have "¬ poincare_ray_meets_line 0⇩h ?a1 x1 x2"
using tangent_not_meet[of x1 x2 i1 ?a1]
using ‹x1 ∈ unit_disc› ‹x2 ∈ unit_disc› ‹?a1 ∈ unit_disc› ‹x1 ≠ x2› ‹¬ poincare_collinear {0⇩h, x1, x2}›
using ‹ideal_points ?lx = {i1, i2}› ‹?a1 ≠ 0⇩h› ‹poincare_collinear {0⇩h, ?a1, i1}›
by simp
moreover
have "¬ poincare_ray_meets_line 0⇩h ?a2 x1 x2"
using tangent_not_meet[of x1 x2 i2 ?a2]
using ‹x1 ∈ unit_disc› ‹x2 ∈ unit_disc› ‹?a2 ∈ unit_disc› ‹x1 ≠ x2› ‹¬ poincare_collinear {0⇩h, x1, x2}›
using ‹ideal_points ?lx = {i1, i2}› ‹?a2 ≠ 0⇩h› ‹poincare_collinear {0⇩h, ?a2, i2}›
by simp
moreover
have "∀a' ∈ unit_disc. poincare_in_angle a' ?a1 0⇩h ?a2 ⟶ poincare_ray_meets_line 0⇩h a' x1 x2"
unfolding poincare_in_angle_def
proof safe
fix a' a
assume *: "a' ∈ unit_disc" "a ∈ unit_disc" "poincare_on_ray a' 0⇩h a" "a' ≠ 0⇩h"
"poincare_between ?a1 a ?a2" "a ≠ ?a1" "a ≠ ?a2"
show "poincare_ray_meets_line 0⇩h a' x1 x2"
proof-
have "∀ a' a1 a2 x1 x2 i1 i2.
a' ∈ unit_disc ∧ x1 ∈ unit_disc ∧ x2 ∈ unit_disc ∧ x1 ≠ x2 ∧
¬ poincare_collinear {0⇩h, x1, x2} ∧ ideal_points (poincare_line x1 x2) = {i1, i2} ∧
a1 = of_complex (to_complex i1 / 2) ∧ a2 = of_complex (to_complex i2 / 2) ∧
i1 ≠ i2 ∧ a1 ≠ a2 ∧ poincare_collinear {0⇩h, a1, i1} ∧ poincare_collinear {0⇩h, a2, i2} ∧
a1 ∈ unit_disc ∧ a2 ∈ unit_disc ∧ i1 ∈ unit_circle_set ∧ i2 ∈ unit_circle_set ∧
poincare_on_ray a' 0⇩h a ∧ a' ≠ 0⇩h ∧ poincare_between a1 a a2 ∧ a ≠ a1 ∧ a ≠ a2 ⟶
poincare_ray_meets_line 0⇩h a' x1 x2" (is "∀ a' a1 a2 x1 x2 i1 i2. ?R 0⇩h a' a1 a2 x1 x2 i1 i2 a")
proof (rule wlog_rotation_to_positive_x_axis[OF ‹a ∈ unit_disc›])
let ?R' = "λ a zero. ∀ a' a1 a2 x1 x2 i1 i2. ?R zero a' a1 a2 x1 x2 i1 i2 a"
fix xa
assume xa: "is_real xa" "0 < Re xa" "Re xa < 1"
let ?a = "of_complex xa"
show "?R' ?a 0⇩h"
proof safe
fix a' a1 a2 x1 x2 i1 i2
let ?i1 = "to_complex i1" and ?i2 = "to_complex i2"
let ?a1 = "of_complex (?i1 / 2)" and ?a2 = "of_complex (?i2 / 2)"
let ?la = "poincare_line ?a1 ?a2" and ?lx = "poincare_line x1 x2" and ?li = "poincare_line i1 i2"
assume "a' ∈ unit_disc" "x1 ∈ unit_disc" "x2 ∈ unit_disc" "x1 ≠ x2"
assume "¬ poincare_collinear {0⇩h, x1, x2}" "ideal_points ?lx = {i1, i2}"
assume "poincare_on_ray a' 0⇩h ?a" "a' ≠ 0⇩h"
assume "poincare_between ?a1 ?a ?a2" "?a ≠ ?a1" "?a ≠ ?a2"
assume "i1 ≠ i2" "?a1 ≠ ?a2" "poincare_collinear {0⇩h, ?a1, i1}" "poincare_collinear {0⇩h, ?a2, i2}"
assume "?a1 ∈ unit_disc" "?a2 ∈ unit_disc"
assume "i1 ∈ unit_circle_set" "i2 ∈ unit_circle_set"
show "poincare_ray_meets_line 0⇩h a' x1 x2"
proof-
have "?lx = ?li"
using ‹ideal_points ?lx = {i1, i2}› ‹x1 ≠ x2› ideal_points_line_unique
by auto
have lx: "is_poincare_line ?lx"
using is_poincare_line_poincare_line[OF ‹x1 ≠ x2›]
by simp
have "x1 ∈ circline_set ?lx" "x2 ∈ circline_set ?lx"
using lx ‹x1 ≠ x2›
by auto
have "?lx ≠ x_axis"
using ‹¬ poincare_collinear {0⇩h, x1, x2}› ‹x1 ∈ circline_set ?lx› ‹x2 ∈ circline_set ?lx› lx
unfolding poincare_collinear_def
by auto
have "0⇩h ∉ circline_set ?lx"
using ‹¬ poincare_collinear {0⇩h, x1, x2}› lx ‹x1 ∈ circline_set ?lx› ‹x2 ∈ circline_set ?lx›
unfolding poincare_collinear_def
by auto
have "xa ≠ 0" "?a ≠ 0⇩h"
using xa
by auto
hence "0⇩h ≠ ?a"
by metis
have "?a ∈ positive_x_axis"
using xa
unfolding positive_x_axis_def
by simp
have "?a ∈ unit_disc"
using xa
by (auto simp add: cmod_eq_Re)
have "?a ∈ circline_set ?la"
using ‹poincare_between ?a1 ?a ?a2›
using ‹?a1 ≠ ?a2› ‹?a ∈ unit_disc› ‹?a1 ∈ unit_disc› ‹?a2 ∈ unit_disc› poincare_between_poincare_line_uzv
by blast
have "?a1 ∈ circline_set ?la" "?a2 ∈ circline_set ?la"
by (auto simp add: ‹?a1 ≠ ?a2›)
have la: "is_poincare_line ?la"
using is_poincare_line_poincare_line[OF ‹?a1 ≠ ?a2›]
by simp
have inv: "inversion i1 = i1" "inversion i2 = i2"
using ‹i1 ∈ unit_circle_set› ‹i2 ∈ unit_circle_set›
by (auto simp add: circline_set_def unit_circle_set_def)
have "i1 ≠ ∞⇩h" "i2 ≠ ∞⇩h"
using inv
by auto
have "?a1 ∉ circline_set x_axis ∧ ?a2 ∉ circline_set x_axis"
proof (rule ccontr)
assume "¬ ?thesis"
hence "?a1 ∈ circline_set x_axis ∨ ?a2 ∈ circline_set x_axis"
by auto
hence "?la = x_axis"
proof
assume "?a1 ∈ circline_set x_axis"
hence "{?a, ?a1} ⊆ circline_set ?la ∩ circline_set x_axis"
using ‹?a ∈ circline_set ?la› ‹?a1 ∈ circline_set ?la›‹?a ∈ positive_x_axis›
using circline_set_x_axis_I xa(1)
by blast
thus "?la = x_axis"
using unique_is_poincare_line[of ?a ?a1 ?la x_axis]
using ‹?a1 ∈ unit_disc› ‹?a ∈ unit_disc› la ‹?a ≠ ?a1›
by auto
next
assume "?a2 ∈ circline_set x_axis"
hence "{?a, ?a2} ⊆ circline_set ?la ∩ circline_set x_axis"
using ‹?a ∈ circline_set ?la› ‹?a2 ∈ circline_set ?la› ‹?a ∈ positive_x_axis›
using circline_set_x_axis_I xa(1)
by blast
thus "?la = x_axis"
using unique_is_poincare_line[of ?a ?a2 ?la x_axis]
using ‹?a2 ∈ unit_disc› ‹?a ∈ unit_disc› la ‹?a ≠ ?a2›
by auto
qed
hence "i1 ∈ circline_set x_axis ∧ i2 ∈ circline_set x_axis"
using ‹?a1 ∈ circline_set ?la› ‹?a2 ∈ circline_set ?la›
by (metis ‹i1 ≠ ∞⇩h› ‹i2 ≠ ∞⇩h› ‹of_complex (to_complex i1 / 2) ∈ unit_disc› ‹of_complex (to_complex i2 / 2) ∈ unit_disc› ‹poincare_collinear {0⇩h, of_complex (to_complex i1 / 2), i1}› ‹poincare_collinear {0⇩h, of_complex (to_complex i2 / 2), i2}› divide_eq_0_iff inf_not_of_complex inv(1) inv(2) inversion_noteq_unit_disc of_complex_to_complex of_complex_zero_iff poincare_collinear3_poincare_lines_equal_general poincare_line_0_real_is_x_axis poincare_line_circline_set(2) zero_in_unit_disc zero_neq_numeral)
thus False
using ‹?lx ≠ x_axis› unique_is_poincare_line_general[of i1 i2 ?li x_axis] ‹i1 ≠ i2› inv ‹?lx = ?li›
by auto
qed
hence "?la ≠ x_axis"
using ‹?a1 ≠ ?a2› poincare_line_circline_set(1)
by fastforce
have "intersects_x_axis_positive ?la"
using intersects_x_axis_positive_iff[of ?la] ‹?la ≠ x_axis› ‹?a ∈ circline_set ?la› la
using ‹?a ∈ unit_disc› ‹?a ∈ positive_x_axis›
by auto
have "intersects_x_axis ?lx"
proof-
have "Arg (to_complex ?a1) * Arg (to_complex ?a2) < 0"
using ‹poincare_between ?a1 ?a ?a2› ‹?a1 ∈ unit_disc› ‹?a2 ∈ unit_disc›
using poincare_between_x_axis_intersection[of ?a1 ?a2 "of_complex xa"]
using ‹?a1 ≠ ?a2› ‹?a ∈ unit_disc› ‹?a1 ∉ circline_set x_axis ∧ ?a2 ∉ circline_set x_axis› ‹?a ∈ positive_x_axis›
using ‹?a ∈ circline_set ?la›
unfolding positive_x_axis_def
by simp
moreover
have "⋀ x y x' y' :: real. ⟦sgn x' = sgn x; sgn y' = sgn y⟧ ⟹ x*y < 0 ⟷ x'*y' < 0"
by (metis sgn_less sgn_mult)
ultimately
have "Im (to_complex ?a1) * Im (to_complex ?a2) < 0"
using arg_Im_sgn[of "to_complex ?a1"] arg_Im_sgn[of "to_complex ?a2"]
using ‹?a1 ∈ unit_disc› ‹?a2 ∈ unit_disc› ‹?a1 ∉ circline_set x_axis ∧ ?a2 ∉ circline_set x_axis›
using inf_or_of_complex[of ?a1] inf_or_of_complex[of ?a2] circline_set_x_axis
by (metis circline_set_x_axis_I to_complex_of_complex)
thus ?thesis
using ideal_points_intersects_x_axis[of ?lx i1 i2]
using ‹ideal_points ?lx = {i1, i2}› lx ‹?lx ≠ x_axis›
by simp
qed
have "intersects_x_axis_positive ?lx"
proof-
have "cmod ?i1 = 1" "cmod ?i2 = 1"
using ‹i1 ∈ unit_circle_set› ‹i2 ∈ unit_circle_set›
unfolding unit_circle_set_def
by auto
let ?a1' = "?i1 / 2" and ?a2' = "?i2 / 2"
let ?Aa1 = "𝗂 * (?a1' * cnj ?a2' - ?a2' * cnj ?a1')" and
?Ba1 = "𝗂 * (?a2' * cor ((cmod ?a1')⇧2 + 1) - ?a1' * cor ((cmod ?a2')⇧2 + 1))"
have "?Aa1 ≠ 0 ∨ ?Ba1 ≠ 0"
using ‹cmod (to_complex i1) = 1› ‹cmod (to_complex i2) = 1› ‹?a1 ≠ ?a2›
by (auto simp add: power_divide complex_mult_cnj_cmod)
have "is_real ?Aa1"
by simp
have "?a1 ≠ inversion ?a2"
using ‹?a1 ∈ unit_disc› ‹?a2 ∈ unit_disc› inversion_noteq_unit_disc by fastforce
hence "Re ?Ba1 / Re ?Aa1 < -1"
using ‹intersects_x_axis_positive ?la› ‹?a1 ≠ ?a2›
using intersects_x_axis_positive_mk_circline[of ?Aa1 ?Ba1] ‹?Aa1 ≠ 0 ∨ ?Ba1 ≠ 0› ‹is_real ?Aa1›
using poincare_line_non_homogenous[of ?a1 ?a2]
by (simp add: Let_def)
moreover
let ?i1' = "to_complex i1" and ?i2' = "to_complex i2"
let ?Ai1 = "𝗂 * (?i1' * cnj ?i2' - ?i2' * cnj ?i1')" and
?Bi1 = "𝗂 * (?i2' * cor ((cmod ?i1')⇧2 + 1) - ?i1' * cor ((cmod ?i2')⇧2 + 1))"
have "?Ai1 ≠ 0 ∨ ?Bi1 ≠ 0"
using ‹cmod (to_complex i1) = 1› ‹cmod (to_complex i2) = 1› ‹?a1 ≠ ?a2›
by (auto simp add: power_divide complex_mult_cnj_cmod)
have "is_real ?Ai1"
by simp
have "sgn (Re ?Bi1 / Re ?Ai1) = sgn (Re ?Ba1 / Re ?Aa1)"
proof-
have "Re ?Bi1 / Re ?Ai1 = (Im ?i1 * 2 - Im ?i2 * 2) /
(Im ?i2 * (Re ?i1 * 2) - Im ?i1 * (Re ?i2 * 2))"
using ‹cmod ?i1 = 1› ‹cmod ?i2 = 1›
by (auto simp add: complex_mult_cnj_cmod field_simps)
also have "... = (Im ?i1 - Im ?i2) /
(Im ?i2 * (Re ?i1) - Im ?i1 * (Re ?i2))" (is "... = ?expr")
apply (subst left_diff_distrib[symmetric])
apply (subst semiring_normalization_rules(18))+
apply (subst left_diff_distrib[symmetric])
by (metis mult.commute mult_divide_mult_cancel_left_if zero_neq_numeral)
finally have 1: "Re ?Bi1 / Re ?Ai1 = (Im ?i1 - Im ?i2) / (Im ?i2 * (Re ?i1) - Im ?i1 * (Re ?i2))"
.
have "Re ?Ba1 / Re ?Aa1 = (Im ?i1 * 20 - Im ?i2 * 20) /
(Im ?i2 * (Re ?i1 * 16) - Im ?i1 * (Re ?i2 * 16))"
using ‹cmod (to_complex i1) = 1› ‹cmod (to_complex i2) = 1›
by (auto simp add: complex_mult_cnj_cmod field_simps)
also have "... = (20 / 16) * ((Im ?i1 - Im ?i2) /
(Im ?i2 * (Re ?i1) - Im ?i1 * (Re ?i2)))"
apply (subst left_diff_distrib[symmetric])+
apply (subst semiring_normalization_rules(18))+
apply (subst left_diff_distrib[symmetric])+
by (metis (no_types, opaque_lifting) field_class.field_divide_inverse mult.commute times_divide_times_eq)
finally have 2: "Re ?Ba1 / Re ?Aa1 = (5 / 4) * ((Im ?i1 - Im ?i2) / (Im ?i2 * (Re ?i1) - Im ?i1 * (Re ?i2)))"
by simp
have "?expr ≠ 0"
using ‹Re ?Ba1 / Re ?Aa1 < -1›
apply (subst (asm) 2)
by linarith
thus ?thesis
apply (subst 1, subst 2)
apply (simp only: sgn_mult)
by simp
qed
moreover
have "i1 ≠ inversion i2"
by (simp add: ‹i1 ≠ i2› inv(2))
have "(Re ?Bi1 / Re ?Ai1)⇧2 > 1"
proof-
have "?Ai1 = 0 ∨ (Re ?Bi1)⇧2 > (Re ?Ai1)⇧2"
using ‹intersects_x_axis ?lx›
using ‹i1 ≠ i2› ‹i1 ≠ ∞⇩h› ‹i2 ≠ ∞⇩h› ‹i1 ≠ inversion i2›
using intersects_x_axis_mk_circline[of ?Ai1 ?Bi1] ‹?Ai1 ≠ 0 ∨ ?Bi1 ≠ 0› ‹is_real ?Ai1›
using poincare_line_non_homogenous[of i1 i2] ‹?lx = ?li›
by metis
moreover
have "?Ai1 ≠ 0"
proof (rule ccontr)
assume "¬ ?thesis"
hence "0⇩h ∈ circline_set ?li"
unfolding circline_set_def
apply simp
apply (transfer, transfer, case_tac i1, case_tac i2)
by (auto simp add: vec_cnj_def field_simps)
thus False
using ‹0⇩h ∉ circline_set ?lx› ‹?lx = ?li›
by simp
qed
ultimately
have "(Re ?Bi1)⇧2 > (Re ?Ai1)⇧2"
by auto
moreover
have "Re ?Ai1 ≠ 0"
using ‹is_real ?Ai1› ‹?Ai1 ≠ 0›
by (simp add: complex_eq_iff)
ultimately
show ?thesis
by (simp add: power_divide)
qed
moreover
{
fix x1 x2 :: real
assume "sgn x1 = sgn x2" "x1 < -1" "x2⇧2 > 1"
hence "x2 < -1"
by (smt one_power2 real_sqrt_abs real_sqrt_less_iff sgn_neg sgn_pos)
}
ultimately
have "Re ?Bi1 / Re ?Ai1 < -1"
by metis
thus ?thesis
using ‹i1 ≠ i2› ‹i1 ≠ ∞⇩h› ‹i2 ≠ ∞⇩h› ‹i1 ≠ inversion i2›
using intersects_x_axis_positive_mk_circline[of ?Ai1 ?Bi1] ‹?Ai1 ≠ 0 ∨ ?Bi1 ≠ 0› ‹is_real ?Ai1›
using poincare_line_non_homogenous[of i1 i2] ‹?lx = ?li›
by (simp add: Let_def)
qed
then obtain x where x: "x ∈ unit_disc" "x ∈ circline_set ?lx ∩ positive_x_axis"
using intersects_x_axis_positive_iff[OF lx ‹?lx ≠ x_axis›]
by auto
have "poincare_on_ray x 0⇩h a' ∧ poincare_collinear {x1, x2, x}"
proof
show "poincare_collinear {x1, x2, x}"
using x lx ‹x1 ∈ circline_set ?lx› ‹x2 ∈ circline_set ?lx›
unfolding poincare_collinear_def
by auto
next
show "poincare_on_ray x 0⇩h a'"
unfolding poincare_on_ray_def
proof-
have "a' ∈ circline_set x_axis"
using ‹poincare_on_ray a' 0⇩h ?a› xa ‹0⇩h ≠ ?a› ‹xa ≠ 0› ‹a' ∈ unit_disc›
unfolding poincare_on_ray_def
using poincare_line_0_real_is_x_axis[of "of_complex xa"]
using poincare_between_poincare_line_uvz[of "0⇩h" "of_complex xa" a']
using poincare_between_poincare_line_uzv[of "0⇩h" "of_complex xa" a']
by (auto simp add: cmod_eq_Re)
then obtain xa' where xa': "a' = of_complex xa'" "is_real xa'"
using ‹a' ∈ unit_disc›
using circline_set_def on_circline_x_axis
by auto
hence "-1 < Re xa'" "Re xa' < 1" "xa' ≠ 0"
using ‹a' ∈ unit_disc› ‹a' ≠ 0⇩h›
by (auto simp add: cmod_eq_Re)
hence "Re xa' > 0" "Re xa' < 1" "is_real xa'"
using ‹poincare_on_ray a' 0⇩h (of_complex xa)›
using poincare_between_x_axis_0uv[of "Re xa'" "Re xa"]
using poincare_between_x_axis_0uv[of "Re xa" "Re xa'"]
using circline_set_positive_x_axis_I[of "Re xa'"]
using xa xa' complex_of_real_Re
unfolding poincare_on_ray_def
by (smt of_real_0, linarith, blast)
moreover
obtain xx where "is_real xx" "Re xx > 0" "Re xx < 1" "x = of_complex xx"
using x
unfolding positive_x_axis_def
using circline_set_def cmod_eq_Re on_circline_x_axis
by auto
ultimately
show "poincare_between 0⇩h x a' ∨ poincare_between 0⇩h a' x"
using ‹a' = of_complex xa'›
by (smt ‹a' ∈ unit_disc› arg_0_iff poincare_between_0uv poincare_between_def to_complex_of_complex x(1))
qed
qed
thus ?thesis
using ‹x ∈ unit_disc›
unfolding poincare_ray_meets_line_def poincare_on_line_def
by (metis insert_commute)
qed
qed
next
show "a ≠ 0⇩h"
proof (rule ccontr)
assume "¬ ?thesis"
then obtain k where "k<0" "to_complex ?a1 = cor k * to_complex ?a2"
using poincare_between_u0v[OF ‹?a1 ∈ unit_disc› ‹?a2 ∈ unit_disc› ‹?a1 ≠ 0⇩h› ‹?a2 ≠ 0⇩h›]
using ‹poincare_between ?a1 a ?a2›
by auto
hence "to_complex i1 = cor k * to_complex i2" "k < 0"
by auto
hence "0⇩h ∈ circline_set (poincare_line x1 x2)"
using ideal_points_proportional[of "poincare_line x1 x2" i1 i2 k] ‹ideal_points (poincare_line x1 x2) = {i1, i2}›
using is_poincare_line_poincare_line[OF ‹x1 ≠ x2›]
by simp
thus False
using ‹¬ poincare_collinear {0⇩h, x1, x2}›
using is_poincare_line_poincare_line[OF ‹x1 ≠ x2›]
unfolding poincare_collinear_def
by (meson ‹x1 ≠ x2› empty_subsetI insert_subset poincare_line_circline_set(1) poincare_line_circline_set(2))
qed
next
fix φ u
let ?R' = "λ a zero. ∀ a' a1 a2 x1 x2 i1 i2. ?R zero a' a1 a2 x1 x2 i1 i2 a"
let ?M = "moebius_pt (moebius_rotation φ)"
assume *: "u ∈ unit_disc" "u ≠ 0⇩h" and **: "?R' (?M u) 0⇩h"
have uf: "unit_disc_fix (moebius_rotation φ)"
by simp
have "?M 0⇩h = 0⇩h"
by auto
hence **: "?R' (?M u) (?M 0⇩h)"
using **
by simp
show "?R' u 0⇩h"
proof (rule allI)+
fix a' a1 a2 x1 x2 i1 i2
have i1: "i1 ∈ unit_circle_set ⟶ moebius_pt (moebius_rotation φ) (of_complex (to_complex i1 / 2)) = of_complex (to_complex (moebius_pt (moebius_rotation φ) i1) / 2)"
using unit_circle_set_def by force
have i2: "i2 ∈ unit_circle_set ⟶ moebius_pt (moebius_rotation φ) (of_complex (to_complex i2 / 2)) = of_complex (to_complex (moebius_pt (moebius_rotation φ) i2) / 2)"
using unit_circle_set_def by force
show "?R 0⇩h a' a1 a2 x1 x2 i1 i2 u"
using **[rule_format, of "?M a'" "?M x1" "?M x2" "?M i1" "?M i2" "?M a1" "?M a2"] uf *
apply (auto simp del: moebius_pt_moebius_rotation_zero moebius_pt_moebius_rotation)
using i1 i2
by simp
qed
qed
thus ?thesis
using ‹a' ∈ unit_disc› ‹x1 ∈ unit_disc› ‹x2 ∈ unit_disc› ‹x1 ≠ x2›
using ‹¬ poincare_collinear {0⇩h, x1, x2}› ‹ideal_points ?lx = {i1, i2}› ‹i1 ≠ i2›
using ‹?a1 ≠ ?a2› ‹poincare_collinear {0⇩h, ?a1, i1}› ‹poincare_collinear {0⇩h, ?a2, i2}›
using ‹?a1 ∈ unit_disc› ‹?a2 ∈ unit_disc› ‹i1 ∈ unit_circle_set› ‹i2 ∈ unit_circle_set›
using ‹poincare_on_ray a' 0⇩h a› ‹a' ≠ 0⇩h› ‹poincare_between ?a1 a ?a2› ‹a ≠ ?a1› ‹a ≠ ?a2›
by blast
qed
qed
moreover
have "¬ poincare_on_line 0⇩h ?a1 ?a2"
proof
assume *: "poincare_on_line 0⇩h ?a1 ?a2"
hence "poincare_collinear {0⇩h, ?a1, ?a2}"
unfolding poincare_on_line_def
by simp
hence "poincare_line 0⇩h ?a1 = poincare_line 0⇩h ?a2"
using poincare_collinear3_poincare_lines_equal_general[of "0⇩h" ?a1 ?a2]
using ‹?a1 ∈ unit_disc› ‹?a1 ≠ 0⇩h› ‹?a2 ∈ unit_disc› ‹?a2 ≠ 0⇩h›
by (metis inversion_noteq_unit_disc zero_in_unit_disc)
have "i1 ∈ circline_set (poincare_line 0⇩h ?a1)"
using ‹poincare_collinear {0⇩h, ?a1, i1}›
using poincare_collinear3_poincare_line_general[of i1 "0⇩h" ?a1]
using ‹?a1 ∈ unit_disc› ‹?a1 ≠ 0⇩h›
by (metis insert_commute inversion_noteq_unit_disc zero_in_unit_disc)
moreover
have "i2 ∈ circline_set (poincare_line 0⇩h ?a1)"
using ‹poincare_collinear {0⇩h, ?a2, i2}›
using poincare_collinear3_poincare_line_general[of i2 "0⇩h" ?a2]
using ‹?a2 ∈ unit_disc› ‹?a2 ≠ 0⇩h› ‹poincare_line 0⇩h ?a1 = poincare_line 0⇩h ?a2›
by (metis insert_commute inversion_noteq_unit_disc zero_in_unit_disc)
ultimately
have "poincare_collinear {0⇩h, i1, i2}"
using ‹?a1 ∈ unit_disc› ‹?a1 ≠ 0⇩h› ‹poincare_collinear {0⇩h, ?a1, i1}›
by (smt insert_subset poincare_collinear_def unique_poincare_line zero_in_unit_disc)
hence "0⇩h ∈ circline_set (poincare_line i1 i2)"
using poincare_collinear3_poincare_line_general[of "0⇩h" i1 i2]
using ‹i1 ≠ i2› ‹i2 ∈ unit_circle_set› unit_circle_set_def
by force
moreover
have "?lx = ?li"
using ‹ideal_points ?lx = {i1, i2}› ‹x1 ≠ x2› ideal_points_line_unique
by auto
ultimately
show False
using ‹¬ poincare_collinear {0⇩h, x1, x2}›
using ‹x1 ≠ x2› poincare_line_poincare_collinear3_general
by auto
qed
ultimately
show ?thesis
using ‹?a1 ∈ unit_disc› ‹?a2 ∈ unit_disc›
by blast
qed
qed
qed
thus ?thesis
using ‹x1 ∈ unit_disc› ‹x2 ∈ unit_disc› ‹¬ poincare_collinear {a, x1, x2}›
by blast
qed
subsection‹Interpretation of locales›
global_interpretation PoincareTarskiAbsolute: TarskiAbsolute where cong = p_congruent and betw = p_between
defines p_on_line = PoincareTarskiAbsolute.on_line and
p_on_ray = PoincareTarskiAbsolute.on_ray and
p_in_angle = PoincareTarskiAbsolute.in_angle and
p_ray_meets_line = PoincareTarskiAbsolute.ray_meets_line
proof-
show "TarskiAbsolute p_congruent p_between"
proof
text‹ 1. Reflexivity of congruence ›
fix x y
show "p_congruent x y y x"
unfolding p_congruent_def
by transfer (simp add: poincare_distance_sym)
next
text‹ 2. Transitivity of congruence ›
fix x y z u v w
show "p_congruent x y z u ∧ p_congruent x y v w ⟶ p_congruent z u v w"
by (transfer, simp)
next
text‹ 3. Identity of congruence ›
fix x y z
show "p_congruent x y z z ⟶ x = y"
unfolding p_congruent_def
by transfer (simp add: poincare_distance_eq_0_iff)
next
text‹ 4. Segment construction ›
fix x y a b
show "∃ z. p_between x y z ∧ p_congruent y z a b"
using segment_construction
unfolding p_congruent_def
by transfer (simp, blast)
next
text‹ 5. Five segment ›
fix x y z x' y' z' u u'
show "x ≠ y ∧ p_between x y z ∧ p_between x' y' z' ∧
p_congruent x y x' y' ∧ p_congruent y z y' z' ∧
p_congruent x u x' u' ∧ p_congruent y u y' u' ⟶
p_congruent z u z' u'"
unfolding p_congruent_def
apply transfer
using five_segment_axiom
by meson
next
text‹ 6. Identity of betweeness ›
fix x y
show "p_between x y x ⟶ x = y"
by transfer (simp add: poincare_between_sum_distances poincare_distance_eq_0_iff poincare_distance_sym)
next
text‹ 7. Pasch ›
fix x y z u v
show "p_between x u z ∧ p_between y v z ⟶ (∃ a. p_between u a y ∧ p_between x a v)"
apply transfer
using Pasch
by blast
next
text‹ 8. Lower dimension ›
show "∃ a. ∃ b. ∃ c. ¬ p_between a b c ∧ ¬ p_between b c a ∧ ¬ p_between c a b"
apply (transfer)
using lower_dimension_axiom
by simp
next
text‹ 9. Upper dimension ›
fix x y z u v
show "p_congruent x u x v ∧ p_congruent y u y v ∧ p_congruent z u z v ∧ u ≠ v ⟶
p_between x y z ∨ p_between y z x ∨ p_between z x y"
unfolding p_congruent_def
by (transfer, simp add: upper_dimension_axiom)
qed
qed
interpretation PoincareTarskiHyperbolic: TarskiHyperbolic
where cong = p_congruent and betw = p_between
proof
text‹ 10. Euclid negation ›
show "∃ a b c d t. p_between a d t ∧ p_between b d c ∧ a ≠ d ∧
(∀ x y. p_between a b x ∧ p_between a c y ⟶ ¬ p_between x t y)"
using negated_euclidean_axiom
by transfer (auto, blast)
next
fix a x1 x2
assume "¬ TarskiAbsolute.on_line p_between a x1 x2"
hence "¬ p_on_line a x1 x2"
using TarskiAbsolute.on_line_def[OF PoincareTarskiAbsolute.TarskiAbsolute_axioms]
using PoincareTarskiAbsolute.on_line_def
by simp
text‹ 11. Limiting parallels ›
thus "∃a1 a2.
¬ TarskiAbsolute.on_line p_between a a1 a2 ∧
¬ TarskiAbsolute.ray_meets_line p_between a a1 x1 x2 ∧
¬ TarskiAbsolute.ray_meets_line p_between a a2 x1 x2 ∧
(∀a'. TarskiAbsolute.in_angle p_between a' a1 a a2 ⟶ TarskiAbsolute.ray_meets_line p_between a a' x1 x2)"
unfolding TarskiAbsolute.in_angle_def[OF PoincareTarskiAbsolute.TarskiAbsolute_axioms]
unfolding TarskiAbsolute.on_ray_def[OF PoincareTarskiAbsolute.TarskiAbsolute_axioms]
unfolding TarskiAbsolute.ray_meets_line_def[OF PoincareTarskiAbsolute.TarskiAbsolute_axioms]
unfolding TarskiAbsolute.on_ray_def[OF PoincareTarskiAbsolute.TarskiAbsolute_axioms]
unfolding TarskiAbsolute.on_line_def[OF PoincareTarskiAbsolute.TarskiAbsolute_axioms]
unfolding PoincareTarskiAbsolute.on_line_def
apply transfer
proof-
fix a x1 x2
assume *: "a ∈ unit_disc" "x1 ∈ unit_disc" "x2 ∈ unit_disc"
"¬ (poincare_between a x1 x2 ∨ poincare_between x1 a x2 ∨ poincare_between x1 x2 a)"
hence "¬ poincare_on_line a x1 x2"
using poincare_collinear3_iff[of a x1 x2]
using poincare_between_rev poincare_on_line_def by blast
hence "∃a1∈unit_disc.
∃a2∈unit_disc.
¬ poincare_on_line a a1 a2 ∧
¬ poincare_ray_meets_line a a1 x1 x2 ∧
¬ poincare_ray_meets_line a a2 x1 x2 ∧
(∀a'∈unit_disc.
poincare_in_angle a' a1 a a2 ⟶
poincare_ray_meets_line a a' x1 x2)"
using limiting_parallels[of a x1 x2] *
by blast
then obtain a1 a2 where **: "a1∈unit_disc" "a2∈unit_disc" "¬ poincare_on_line a a1 a2"
"¬ poincare_ray_meets_line a a2 x1 x2"
"¬ poincare_ray_meets_line a a1 x1 x2"
"∀a'∈unit_disc.
poincare_in_angle a' a1 a a2 ⟶
poincare_ray_meets_line a a' x1 x2"
by blast
have "¬ (∃x∈{z. z ∈ unit_disc}.
(poincare_between a x a1 ∨
poincare_between a a1 x) ∧
(poincare_between x x1 x2 ∨
poincare_between x1 x x2 ∨
poincare_between x1 x2 x))"
using ‹¬ poincare_ray_meets_line a a1 x1 x2›
unfolding poincare_on_line_def poincare_ray_meets_line_def poincare_on_ray_def
using poincare_collinear3_iff[of _ x1 x2] poincare_between_rev *(2, 3)
by auto
moreover
have "¬ (∃x∈{z. z ∈ unit_disc}.
(poincare_between a x a2 ∨
poincare_between a a2 x) ∧
(poincare_between x x1 x2 ∨
poincare_between x1 x x2 ∨
poincare_between x1 x2 x))"
using ‹¬ poincare_ray_meets_line a a2 x1 x2›
unfolding poincare_on_line_def poincare_ray_meets_line_def poincare_on_ray_def
using poincare_collinear3_iff[of _ x1 x2] poincare_between_rev *(2, 3)
by auto
moreover
have "¬ (poincare_between a a1 a2 ∨ poincare_between a1 a a2 ∨ poincare_between a1 a2 a)"
using ‹¬ poincare_on_line a a1 a2› poincare_collinear3_iff[of a a1 a2]
using *(1) **(1-2)
unfolding poincare_on_line_def
by simp
moreover
have "(∀a'∈{z. z ∈ unit_disc}.
a ≠ a1 ∧
a ≠ a2 ∧
a' ≠ a ∧
(∃x∈{z. z ∈ unit_disc}.
poincare_between a1 x a2 ∧
x ≠ a1 ∧
x ≠ a2 ∧
(poincare_between a a' x ∨
poincare_between a x a')) ⟶
(∃x∈{z. z ∈ unit_disc}.
(poincare_between a x a' ∨
poincare_between a a' x) ∧
(poincare_between x x1 x2 ∨
poincare_between x1 x x2 ∨
poincare_between x1 x2 x)))"
using **(6)
unfolding poincare_on_line_def poincare_in_angle_def poincare_ray_meets_line_def poincare_on_ray_def
using poincare_collinear3_iff[of _ x1 x2] poincare_between_rev *(2, 3)
by auto
ultimately
show "∃a1∈{z. z ∈ unit_disc}.
∃a2∈{z. z ∈ unit_disc}.
¬ (poincare_between a a1 a2 ∨ poincare_between a1 a a2 ∨ poincare_between a1 a2 a) ∧
¬ (∃x∈{z. z ∈ unit_disc}.
(poincare_between a x a1 ∨
poincare_between a a1 x) ∧
(poincare_between x x1 x2 ∨
poincare_between x1 x x2 ∨
poincare_between x1 x2 x)) ∧
¬ (∃x∈{z. z ∈ unit_disc}.
(poincare_between a x a2 ∨
poincare_between a a2 x) ∧
(poincare_between x x1 x2 ∨
poincare_between x1 x x2 ∨
poincare_between x1 x2 x)) ∧
(∀a'∈{z. z ∈ unit_disc}.
a ≠ a1 ∧
a ≠ a2 ∧
a' ≠ a ∧
(∃x∈{z. z ∈ unit_disc}.
poincare_between a1 x a2 ∧
x ≠ a1 ∧
x ≠ a2 ∧
(poincare_between a a' x ∨
poincare_between a x a')) ⟶
(∃x∈{z. z ∈ unit_disc}.
(poincare_between a x a' ∨
poincare_between a a' x) ∧
(poincare_between x x1 x2 ∨
poincare_between x1 x x2 ∨
poincare_between x1 x2 x)))"
using **(1, 2)
by auto
qed
qed
interpretation PoincareElementaryTarskiHyperbolic: ElementaryTarskiHyperbolic p_congruent p_between
proof
text‹ 12. Continuity ›
fix φ ψ
assume "∃ a. ∀ x. ∀ y. φ x ∧ ψ y ⟶ p_between a x y"
thus "∃ b. ∀ x. ∀ y. φ x ∧ ψ y ⟶ p_between x b y"
apply transfer
using continuity
by auto
qed
end