Theory Poincare_Lines
section ‹H-lines in the Poincar\'e model›
theory Poincare_Lines
imports Complex_Geometry.Unit_Circle_Preserving_Moebius Complex_Geometry.Circlines_Angle
begin
subsection ‹Definition and basic properties of h-lines›
text ‹H-lines in the Poincar\'e model are either line segments passing trough the origin or
segments (within the unit disc) of circles that are perpendicular to the unit circle. Algebraically
these are circlines that are represented by Hermitean matrices of
the form
$$H = \left(
\begin{array}{cc}
A & B\\
\overline{B} & A
\end{array}
\right),$$
for $A \in \mathbb{R}$, and $B \in \mathbb{C}$, and $|B|^2 > A^2$,
where the circline equation is the usual one: $z^*Hz = 0$, for homogenous coordinates $z$.›
definition is_poincare_line_cmat :: "complex_mat ⇒ bool" where
[simp]: "is_poincare_line_cmat H ⟷
(let (A, B, C, D) = H
in hermitean (A, B, C, D) ∧ A = D ∧ (cmod B)⇧2 > (cmod A)⇧2)"
lift_definition is_poincare_line_clmat :: "circline_mat ⇒ bool" is is_poincare_line_cmat
done
text ‹We introduce the predicate that checks if a given complex matrix is a matrix of a h-line in
the Poincar\'e model, and then by means of the lifting package lift it to the type of non-zero
Hermitean matrices, and then to circlines (that are equivalence classes of such matrices).›
lift_definition is_poincare_line :: "circline ⇒ bool" is is_poincare_line_clmat
proof (transfer, transfer)
fix H1 H2 :: complex_mat
assume hh: "hermitean H1 ∧ H1 ≠ mat_zero" "hermitean H2 ∧ H2 ≠ mat_zero"
assume "circline_eq_cmat H1 H2"
thus "is_poincare_line_cmat H1 ⟷ is_poincare_line_cmat H2"
using hh
by (cases H1, cases H2) (auto simp: norm_mult power_mult_distrib)
qed
lemma is_poincare_line_mk_circline:
assumes "(A, B, C, D) ∈ hermitean_nonzero"
shows "is_poincare_line (mk_circline A B C D) ⟷ (cmod B)⇧2 > (cmod A)⇧2 ∧ A = D"
using assms
by (transfer, transfer, auto simp add: Let_def)
text‹Abstract characterisation of @{term is_poincare_line} predicate: H-lines in the Poincar\'e
model are real circlines (circlines with the negative determinant) perpendicular to the unit
circle.›
lemma is_poincare_line_iff:
shows "is_poincare_line H ⟷ circline_type H = -1 ∧ perpendicular H unit_circle"
unfolding perpendicular_def
proof (simp, transfer, transfer)
fix H
assume hh: "hermitean H ∧ H ≠ mat_zero"
obtain A B C D where *: "H = (A, B, C, D)"
by (cases H, auto)
have **: "is_real A" "is_real D" "C = cnj B"
using hh * hermitean_elems
by auto
hence "(Re A = Re D ∧ cmod A * cmod A < cmod B * cmod B) =
(Re A * Re D < Re B * Re B + Im B * Im B ∧ (Re D = Re A ∨ Re A * Re D = Re B * Re B + Im B * Im B))"
using *
by (smt cmod_power2 power2_eq_square zero_power2)+
thus "is_poincare_line_cmat H ⟷
circline_type_cmat H = - 1 ∧ cos_angle_cmat (of_circline_cmat H) unit_circle_cmat = 0"
using * **
by (auto simp add: sgn_1_neg complex_eq_if_Re_eq cmod_square power2_eq_square simp del: pos_oriented_cmat_def)
qed
text‹The @{term x_axis} is an h-line.›
lemma is_poincare_line_x_axis [simp]:
shows "is_poincare_line x_axis"
by (transfer, transfer) (auto simp add: hermitean_def mat_adj_def mat_cnj_def)
text‹The @{term unit_circle} is not an h-line.›
lemma not_is_poincare_line_unit_circle [simp]:
shows "¬ is_poincare_line unit_circle"
by (transfer, transfer, simp)
subsubsection ‹Collinear points›
text‹Points are collinear if they all belong to an h-line. ›
definition poincare_collinear :: "complex_homo set ⇒ bool" where
"poincare_collinear S ⟷ (∃ p. is_poincare_line p ∧ S ⊆ circline_set p)"
subsubsection ‹H-lines and inversion›
text‹Every h-line in the Poincar\'e model contains the inverse (wrt.~the unit circle) of each of its
points (note that at most one of them belongs to the unit disc).›
lemma is_poincare_line_inverse_point:
assumes "is_poincare_line H" "u ∈ circline_set H"
shows "inversion u ∈ circline_set H"
using assms
unfolding is_poincare_line_iff circline_set_def perpendicular_def inversion_def
apply simp
proof (transfer, transfer)
fix u H
assume hh: "hermitean H ∧ H ≠ mat_zero" "u ≠ vec_zero" and
aa: "circline_type_cmat H = - 1 ∧ cos_angle_cmat (of_circline_cmat H) unit_circle_cmat = 0" "on_circline_cmat_cvec H u"
obtain A B C D u1 u2 where *: "H = (A, B, C, D)" "u = (u1, u2)"
by (cases H, cases u, auto)
have "is_real A" "is_real D" "C = cnj B"
using * hh hermitean_elems
by auto
moreover
have "A = D"
using aa(1) * ‹is_real A› ‹is_real D›
by (auto simp del: pos_oriented_cmat_def simp add: complex.expand split: if_split_asm)
thus "on_circline_cmat_cvec H (conjugate_cvec (reciprocal_cvec u))"
using aa(2) *
by (simp add: vec_cnj_def field_simps)
qed
text‹Every h-line in the Poincar\'e model and is invariant under unit circle inversion.›
lemma circline_inversion_poincare_line:
assumes "is_poincare_line H"
shows "circline_inversion H = H"
proof-
obtain u v w where *: "u ≠ v" "v ≠ w" "u ≠ w" "{u, v, w} ⊆ circline_set H"
using assms is_poincare_line_iff[of H]
using circline_type_neg_card_gt3[of H]
by auto
hence "{inversion u, inversion v, inversion w} ⊆ circline_set (circline_inversion H)"
"{inversion u, inversion v, inversion w} ⊆ circline_set H"
using is_poincare_line_inverse_point[OF assms]
by auto
thus ?thesis
using * unique_circline_set[of "inversion u" "inversion v" "inversion w"]
by (metis insert_subset inversion_involution)
qed
subsubsection ‹Classification of h-lines into Euclidean segments and circles›
text‹If an h-line contains zero, than it also contains infinity (the inverse point of zero) and is by
definition an Euclidean line.›
lemma is_poincare_line_trough_zero_trough_infty [simp]:
assumes "is_poincare_line l" and "0⇩h ∈ circline_set l"
shows "∞⇩h ∈ circline_set l"
using is_poincare_line_inverse_point[OF assms]
by simp
lemma is_poincare_line_trough_zero_is_line:
assumes "is_poincare_line l" and "0⇩h ∈ circline_set l"
shows "is_line l"
using assms
using inf_in_circline_set is_poincare_line_trough_zero_trough_infty
by blast
text‹If an h-line does not contain zero, than it also does not contain infinity (the inverse point of
zero) and is by definition an Euclidean circle.›
lemma is_poincare_line_not_trough_zero_not_trough_infty [simp]:
assumes "is_poincare_line l"
assumes "0⇩h ∉ circline_set l"
shows "∞⇩h ∉ circline_set l"
using assms
using is_poincare_line_inverse_point[OF assms(1), of "∞⇩h"]
by auto
lemma is_poincare_line_not_trough_zero_is_circle:
assumes "is_poincare_line l" "0⇩h ∉ circline_set l"
shows "is_circle l"
using assms
using inf_in_circline_set is_poincare_line_not_trough_zero_not_trough_infty
by auto
subsubsection‹Points on h-line›
text‹Each h-line in the Poincar\'e model contains at least two different points within the unit
disc.›
text‹First we prove an auxiliary lemma.›
lemma ex_is_poincare_line_points':
assumes i12: "i1 ∈ circline_set H ∩ unit_circle_set"
"i2 ∈ circline_set H ∩ unit_circle_set"
"i1 ≠ i2"
assumes a: "a ∈ circline_set H" "a ∉ unit_circle_set"
shows "∃ b. b ≠ i1 ∧ b ≠ i2 ∧ b ≠ a ∧ b ≠ inversion a ∧ b ∈ circline_set H"
proof-
have "inversion a ∉ unit_circle_set"
using ‹a ∉ unit_circle_set›
unfolding unit_circle_set_def circline_set_def
by (metis inversion_id_iff_on_unit_circle inversion_involution mem_Collect_eq)
have "a ≠ inversion a"
using ‹a ∉ unit_circle_set› inversion_id_iff_on_unit_circle[of a]
unfolding unit_circle_set_def circline_set_def
by auto
have "a ≠ i1" "a ≠ i2" "inversion a ≠ i1" "inversion a ≠ i2"
using assms ‹inversion a ∉ unit_circle_set›
by auto
then obtain b where cr2: "cross_ratio b i1 a i2 = of_complex 2"
using ‹i1 ≠ i2›
using ex_cross_ratio[of i1 a i2]
by blast
have distinct_b: "b ≠ i1" "b ≠ i2" "b ≠ a"
using ‹i1 ≠ i2› ‹a ≠ i1› ‹a ≠ i2›
using ex1_cross_ratio[of i1 a i2]
using cross_ratio_0[of i1 a i2] cross_ratio_1[of i1 a i2] cross_ratio_inf[of i1 i2 a]
using cr2
by auto
hence "b ∈ circline_set H"
using assms four_points_on_circline_iff_cross_ratio_real[of b i1 a i2] cr2
using unique_circline_set[of i1 i2 a]
by auto
moreover
have "b ≠ inversion a"
proof (rule ccontr)
assume *: "¬ ?thesis"
have "inversion i1 = i1" "inversion i2 = i2"
using i12
unfolding unit_circle_set_def
by auto
hence "cross_ratio (inversion a) i1 a i2 = cross_ratio a i1 (inversion a) i2"
using * cross_ratio_inversion[of i1 a i2 b] ‹a ≠ i1› ‹a ≠ i2› ‹i1 ≠ i2› ‹b ≠ i1›
using four_points_on_circline_iff_cross_ratio_real[of b i1 a i2]
using i12 distinct_b conjugate_id_iff[of "cross_ratio b i1 a i2"]
using i12 a ‹b ∈ circline_set H›
by auto
hence "cross_ratio (inversion a) i1 a i2 ≠ of_complex 2"
using cross_ratio_commute_13[of "inversion a" i1 a i2]
using reciprocal_id_iff
using of_complex_inj
by force
thus False
using * cr2
by simp
qed
ultimately
show ?thesis
using assms ‹b ≠ i1› ‹b ≠ i2› ‹b ≠ a›
by auto
qed
text‹Now we can prove the statement.›
lemma ex_is_poincare_line_points:
assumes "is_poincare_line H"
shows "∃ u v. u ∈ unit_disc ∧ v ∈ unit_disc ∧ u ≠ v ∧ {u, v} ⊆ circline_set H"
proof-
obtain u v w where *: "u ≠ v" "v ≠ w" "u ≠ w" "{u, v, w} ⊆ circline_set H"
using assms is_poincare_line_iff[of H]
using circline_type_neg_card_gt3[of H]
by auto
have "¬ {u, v, w} ⊆ unit_circle_set"
using unique_circline_set[of u v w] *
by (metis assms insert_subset not_is_poincare_line_unit_circle unit_circle_set_def)
hence "H ≠ unit_circle"
unfolding unit_circle_set_def
using *
by auto
show ?thesis
proof (cases "(u ∈ unit_disc ∧ v ∈ unit_disc) ∨
(u ∈ unit_disc ∧ w ∈ unit_disc) ∨
(v ∈ unit_disc ∧ w ∈ unit_disc)")
case True
thus ?thesis
using *
by auto
next
case False
have "∃ a b. a ≠ b ∧ a ≠ inversion b ∧ a ∈ circline_set H ∧ b ∈ circline_set H ∧ a ∉ unit_circle_set ∧ b ∉ unit_circle_set"
proof (cases "(u ∈ unit_circle_set ∧ v ∈ unit_circle_set) ∨
(u ∈ unit_circle_set ∧ w ∈ unit_circle_set) ∨
(v ∈ unit_circle_set ∧ w ∈ unit_circle_set)")
case True
then obtain i1 i2 a where *:
"i1 ∈ unit_circle_set ∩ circline_set H" "i2 ∈ unit_circle_set ∩ circline_set H"
"a ∈ circline_set H" "a ∉ unit_circle_set"
"i1 ≠ i2" "i1 ≠ a" "i2 ≠ a"
using * ‹¬ {u, v, w} ⊆ unit_circle_set›
by auto
then obtain b where "b ∈ circline_set H" "b ≠ i1" "b ≠ i2" "b ≠ a" "b ≠ inversion a"
using ex_is_poincare_line_points'[of i1 H i2 a]
by blast
hence "b ∉ unit_circle_set"
using * ‹H ≠ unit_circle› unique_circline_set[of i1 i2 b]
unfolding unit_circle_set_def
by auto
thus ?thesis
using * ‹b ∈ circline_set H› ‹b ≠ a› ‹b ≠ inversion a›
by auto
next
case False
then obtain f g h where
*: "f ≠ g" "f ∈ circline_set H" "f ∉ unit_circle_set"
"g ∈ circline_set H" "g ∉ unit_circle_set"
"h ∈ circline_set H" "h ≠ f" "h ≠ g"
using *
by auto
show ?thesis
proof (cases "f = inversion g")
case False
thus ?thesis
using *
by auto
next
case True
show ?thesis
proof (cases "h ∈ unit_circle_set")
case False
thus ?thesis
using * ‹f = inversion g›
by auto
next
case True
obtain m where cr2: "cross_ratio m h f g = of_complex 2"
using ex_cross_ratio[of h f g] * ‹f ≠ g› ‹h ≠ f› ‹h ≠ g›
by auto
hence "m ≠ h" "m ≠ f" "m ≠ g"
using ‹h ≠ f› ‹h ≠ g› ‹f ≠ g›
using ex1_cross_ratio[of h f g]
using cross_ratio_0[of h f g] cross_ratio_1[of h f g] cross_ratio_inf[of h g f]
using cr2
by auto
hence "m ∈ circline_set H"
using four_points_on_circline_iff_cross_ratio_real[of m h f g] cr2
using ‹h ≠ f› ‹h ≠ g› ‹f ≠ g› *
using unique_circline_set[of h f g]
by auto
show ?thesis
proof (cases "m ∈ unit_circle_set")
case False
thus ?thesis
using ‹m ≠ f› ‹m ≠ g› ‹f = inversion g› * ‹m ∈ circline_set H›
by auto
next
case True
then obtain n where "n ≠ h" "n ≠ m" "n ≠ f" "n ≠ inversion f" "n ∈ circline_set H"
using ex_is_poincare_line_points'[of h H m f] * ‹m ∈ circline_set H› ‹h ∈ unit_circle_set› ‹m ≠ h›
by auto
hence "n ∉ unit_circle_set"
using * ‹H ≠ unit_circle› unique_circline_set[of m n h]
using ‹m ≠ h› ‹m ∈ unit_circle_set› ‹h ∈ unit_circle_set› ‹m ∈ circline_set H›
unfolding unit_circle_set_def
by auto
thus ?thesis
using * ‹n ∈ circline_set H› ‹n ≠ f› ‹n ≠ inversion f›
by auto
qed
qed
qed
qed
then obtain a b where ab: "a ≠ b" "a ≠ inversion b" "a ∈ circline_set H" "b ∈ circline_set H" "a ∉ unit_circle_set" "b ∉ unit_circle_set"
by blast
have "∀ x. x ∈ circline_set H ∧ x ∉ unit_circle_set ⟶ (∃ x'. x' ∈ circline_set H ∩ unit_disc ∧ (x' = x ∨ x' = inversion x))"
proof safe
fix x
assume x: "x ∈ circline_set H" "x ∉ unit_circle_set"
show "∃ x'. x' ∈ circline_set H ∩ unit_disc ∧ (x' = x ∨ x' = inversion x)"
proof (cases "x ∈ unit_disc")
case True
thus ?thesis
using x
by auto
next
case False
hence "x ∈ unit_disc_compl"
using x in_on_out_univ[of "ounit_circle"]
unfolding unit_circle_set_def unit_disc_def unit_disc_compl_def
by auto
hence "inversion x ∈ unit_disc"
using inversion_unit_disc_compl
by blast
thus ?thesis
using is_poincare_line_inverse_point[OF assms, of x] x
by auto
qed
qed
then obtain a' b' where
*: "a' ∈ circline_set H" "a' ∈ unit_disc" "b' ∈ circline_set H" "b' ∈ unit_disc" and
**: "a' = a ∨ a' = inversion a" "b' = b ∨ b' = inversion b"
using ab
by blast
have "a' ≠ b'"
using ‹a ≠ b› ‹a ≠ inversion b› ** *
by (metis inversion_involution)
thus ?thesis
using *
by auto
qed
qed
subsubsection ‹H-line uniqueness›
text‹There is no more than one h-line that contains two different h-points (in the disc).›
lemma unique_is_poincare_line:
assumes in_disc: "u ∈ unit_disc" "v ∈ unit_disc" "u ≠ v"
assumes pl: "is_poincare_line l1" "is_poincare_line l2"
assumes on_l: "{u, v} ⊆ circline_set l1 ∩ circline_set l2"
shows "l1 = l2"
proof-
have "u ≠ inversion u" "v ≠ inversion u"
using in_disc
using inversion_noteq_unit_disc[of u v]
using inversion_noteq_unit_disc[of u u]
by auto
thus ?thesis
using on_l
using unique_circline_set[of u "inversion u" "v"] ‹u ≠ v›
using is_poincare_line_inverse_point[of l1 u]
using is_poincare_line_inverse_point[of l2 u]
using pl
by auto
qed
text‹For the rest of our formalization it is often useful to consider points on h-lines that are not
within the unit disc. Many lemmas in the rest of this section will have such generalizations.›
text‹There is no more than one h-line that contains two different and not mutually inverse points
(not necessary in the unit disc).›
lemma unique_is_poincare_line_general:
assumes different: "u ≠ v" "u ≠ inversion v"
assumes pl: "is_poincare_line l1" "is_poincare_line l2"
assumes on_l: "{u, v} ⊆ circline_set l1 ∩ circline_set l2"
shows "l1 = l2"
proof (cases "u ≠ inversion u")
case True
thus ?thesis
using unique_circline_set[of u "inversion u" "v"]
using assms
using is_poincare_line_inverse_point by force
next
case False
show ?thesis
proof (cases "v ≠ inversion v")
case True
thus ?thesis
using unique_circline_set[of u "inversion v" "v"]
using assms
using is_poincare_line_inverse_point by force
next
case False
have "on_circline unit_circle u" "on_circline unit_circle v"
using ‹¬ u ≠ inversion u› ‹¬ v ≠ inversion v›
using inversion_id_iff_on_unit_circle
by fastforce+
thus ?thesis
using pl on_l ‹u ≠ v›
unfolding circline_set_def
apply simp
proof (transfer, transfer, safe)
fix u1 u2 v1 v2 A1 B1 C1 D1 A2 B2 C2 D2 :: complex
let ?u = "(u1, u2)" and ?v = "(v1, v2)" and ?H1 = "(A1, B1, C1, D1)" and ?H2 = "(A2, B2, C2, D2)"
assume *: "?u ≠ vec_zero" "?v ≠ vec_zero"
"on_circline_cmat_cvec unit_circle_cmat ?u" "on_circline_cmat_cvec unit_circle_cmat ?v"
"is_poincare_line_cmat ?H1" "is_poincare_line_cmat ?H2"
"hermitean ?H1" "?H1 ≠ mat_zero" "hermitean ?H2" "?H2 ≠ mat_zero"
"on_circline_cmat_cvec ?H1 ?u" "on_circline_cmat_cvec ?H1 ?v"
"on_circline_cmat_cvec ?H2 ?u" "on_circline_cmat_cvec ?H2 ?v"
"¬ (u1, u2) ≈⇩v (v1, v2)"
have **: "A1 = D1" "A2 = D2" "C1 = cnj B1" "C2 = cnj B2" "is_real A1" "is_real A2"
using ‹is_poincare_line_cmat ?H1› ‹is_poincare_line_cmat ?H2›
using ‹hermitean ?H1› ‹?H1 ≠ mat_zero› ‹hermitean ?H2› ‹?H2 ≠ mat_zero›
using hermitean_elems
by auto
have uv: "u1 ≠ 0" "u2 ≠ 0" "v1 ≠ 0" "v2 ≠ 0"
using *(1-4)
by (auto simp add: vec_cnj_def)
have u: "cor ((Re (u1/u2))⇧2) + cor ((Im (u1/u2))⇧2) = 1"
using ‹on_circline_cmat_cvec unit_circle_cmat ?u› uv
apply (subst of_real_add[symmetric])
apply (subst complex_mult_cnj[symmetric])
apply (simp add: vec_cnj_def mult.commute)
done
have v: "cor ((Re (v1/v2))⇧2) + cor ((Im (v1/v2))⇧2) = 1"
using ‹on_circline_cmat_cvec unit_circle_cmat ?v› uv
apply (subst of_real_add[symmetric])
apply (subst complex_mult_cnj[symmetric])
apply (simp add: vec_cnj_def mult.commute)
done
have
"A1 * (cor ((Re (u1/u2))⇧2) + cor ((Im (u1/u2))⇧2) + 1) + cor (Re B1) * cor(2 * Re (u1/u2)) + cor (Im B1) * cor(2 * Im (u1/u2)) = 0"
"A2 * (cor ((Re (u1/u2))⇧2) + cor ((Im (u1/u2))⇧2) + 1) + cor (Re B2) * cor(2 * Re (u1/u2)) + cor (Im B2) * cor(2 * Im (u1/u2)) = 0"
"A1 * (cor ((Re (v1/v2))⇧2) + cor ((Im (v1/v2))⇧2) + 1) + cor (Re B1) * cor(2 * Re (v1/v2)) + cor (Im B1) * cor(2 * Im (v1/v2)) = 0"
"A2 * (cor ((Re (v1/v2))⇧2) + cor ((Im (v1/v2))⇧2) + 1) + cor (Re B2) * cor(2 * Re (v1/v2)) + cor (Im B2) * cor(2 * Im (v1/v2)) = 0"
using circline_equation_quadratic_equation[of A1 "u1/u2" B1 D1 "Re (u1/u2)" "Im (u1 / u2)" "Re B1" "Im B1"]
using circline_equation_quadratic_equation[of A2 "u1/u2" B2 D2 "Re (u1/u2)" "Im (u1 / u2)" "Re B2" "Im B2"]
using circline_equation_quadratic_equation[of A1 "v1/v2" B1 D1 "Re (v1/v2)" "Im (v1 / v2)" "Re B1" "Im B1"]
using circline_equation_quadratic_equation[of A2 "v1/v2" B2 D2 "Re (v1/v2)" "Im (v1 / v2)" "Re B2" "Im B2"]
using ‹on_circline_cmat_cvec ?H1 ?u› ‹on_circline_cmat_cvec ?H2 ?u›
using ‹on_circline_cmat_cvec ?H1 ?v› ‹on_circline_cmat_cvec ?H2 ?v›
using ** uv
by (simp_all add: vec_cnj_def field_simps)
hence
"A1 + cor (Re B1) * cor(Re (u1/u2)) + cor (Im B1) * cor(Im (u1/u2)) = 0"
"A1 + cor (Re B1) * cor(Re (v1/v2)) + cor (Im B1) * cor(Im (v1/v2)) = 0"
"A2 + cor (Re B2) * cor(Re (u1/u2)) + cor (Im B2) * cor(Im (u1/u2)) = 0"
"A2 + cor (Re B2) * cor(Re (v1/v2)) + cor (Im B2) * cor(Im (v1/v2)) = 0"
using u v
by simp_all algebra+
hence
"cor (Re A1 + Re B1 * Re (u1/u2) + Im B1 * Im (u1/u2)) = 0"
"cor (Re A2 + Re B2 * Re (u1/u2) + Im B2 * Im (u1/u2)) = 0"
"cor (Re A1 + Re B1 * Re (v1/v2) + Im B1 * Im (v1/v2)) = 0"
"cor (Re A2 + Re B2 * Re (v1/v2) + Im B2 * Im (v1/v2)) = 0"
using ‹is_real A1› ‹is_real A2›
by simp_all
hence
"Re A1 + Re B1 * Re (u1/u2) + Im B1 * Im (u1/u2) = 0"
"Re A1 + Re B1 * Re (v1/v2) + Im B1 * Im (v1/v2) = 0"
"Re A2 + Re B2 * Re (u1/u2) + Im B2 * Im (u1/u2) = 0"
"Re A2 + Re B2 * Re (v1/v2) + Im B2 * Im (v1/v2) = 0"
using of_real_eq_0_iff
by blast+
moreover
have "Re(u1/u2) ≠ Re(v1/v2) ∨ Im(u1/u2) ≠ Im(v1/v2)"
proof (rule ccontr)
assume "¬ ?thesis"
hence "u1/u2 = v1/v2"
using complex_eqI by blast
thus False
using uv ‹¬ (u1, u2) ≈⇩v (v1, v2)›
using "*"(1) "*"(2) complex_cvec_eq_mix[OF *(1) *(2)]
by (auto simp add: field_simps)
qed
moreover
have "Re A1 ≠ 0 ∨ Re B1 ≠ 0 ∨ Im B1 ≠ 0"
using ‹?H1 ≠ mat_zero› **
by (metis complex_cnj_zero complex_of_real_Re mat_zero_def of_real_0)
ultimately
obtain k where
k: "Re A2 = k * Re A1" "Re B2 = k * Re B1" "Im B2 = k * Im B1"
using linear_system_homogenous_3_2[of "λx y z. 1 * x + Re (u1 / u2) * y + Im (u1 / u2) * z" 1 "Re (u1/u2)" "Im (u1/u2)"
"λx y z. 1 * x + Re (v1 / v2) * y + Im (v1 / v2) * z" 1 "Re (v1/v2)" "Im (v1/v2)"
"Re A2" "Re B2" "Im B2" "Re A1" "Re B1" "Im B1"]
by (auto simp add: field_simps)
have "Re A2 ≠ 0 ∨ Re B2 ≠ 0 ∨ Im B2 ≠ 0"
using ‹?H2 ≠ mat_zero› **
by (metis complex_cnj_zero complex_of_real_Re mat_zero_def of_real_0)
hence "k ≠ 0"
using k
by auto
show "circline_eq_cmat ?H1 ?H2"
using ** k ‹k ≠ 0›
by (auto simp add: vec_cnj_def) (rule_tac x="k" in exI, auto simp add: complex.expand)
qed
qed
qed
text ‹The only h-line that goes trough zero and a non-zero point on the x-axis is the x-axis.›
lemma is_poincare_line_0_real_is_x_axis:
assumes "is_poincare_line l" "0⇩h ∈ circline_set l"
"x ∈ circline_set l ∩ circline_set x_axis" "x ≠ 0⇩h" "x ≠ ∞⇩h"
shows "l = x_axis"
using assms
using is_poincare_line_trough_zero_trough_infty[OF assms(1-2)]
using unique_circline_set[of x "0⇩h" "∞⇩h"]
by auto
text ‹The only h-line that goes trough zero and a non-zero point on the y-axis is the y-axis.›
lemma is_poincare_line_0_imag_is_y_axis:
assumes "is_poincare_line l" "0⇩h ∈ circline_set l"
"y ∈ circline_set l ∩ circline_set y_axis" "y ≠ 0⇩h" "y ≠ ∞⇩h"
shows "l = y_axis"
using assms
using is_poincare_line_trough_zero_trough_infty[OF assms(1-2)]
using unique_circline_set[of y "0⇩h" "∞⇩h"]
by auto
subsubsection‹H-isometries preserve h-lines›
text‹\emph{H-isometries} are defined as homographies (actions of Möbius transformations) and
antihomographies (compositions of actions of Möbius transformations with conjugation) that fix the
unit disc (map it onto itself). They also map h-lines onto h-lines›
text‹We prove a bit more general lemma that states that all Möbius transformations that fix the
unit circle (not necessary the unit disc) map h-lines onto h-lines›
lemma unit_circle_fix_preserve_is_poincare_line [simp]:
assumes "unit_circle_fix M" "is_poincare_line H"
shows "is_poincare_line (moebius_circline M H)"
using assms
unfolding is_poincare_line_iff
proof (safe)
let ?H' = "moebius_ocircline M (of_circline H)"
let ?U' = "moebius_ocircline M ounit_circle"
assume ++: "unit_circle_fix M" "perpendicular H unit_circle"
have ounit: "ounit_circle = moebius_ocircline M ounit_circle ∨
ounit_circle = moebius_ocircline M (opposite_ocircline ounit_circle)"
using ++(1) unit_circle_fix_iff[of M]
by (simp add: inj_of_ocircline moebius_circline_ocircline)
show "perpendicular (moebius_circline M H) unit_circle"
proof (cases "pos_oriented ?H'")
case True
hence *: "of_circline (of_ocircline ?H') = ?H'"
using of_circline_of_ocircline_pos_oriented
by blast
from ounit show ?thesis
proof
assume **: "ounit_circle = moebius_ocircline M ounit_circle"
show ?thesis
using ++
unfolding perpendicular_def
by (simp, subst moebius_circline_ocircline, subst *, subst **) simp
next
assume **: "ounit_circle = moebius_ocircline M (opposite_ocircline ounit_circle)"
show ?thesis
using ++
unfolding perpendicular_def
by (simp, subst moebius_circline_ocircline, subst *, subst **) simp
qed
next
case False
hence *: "of_circline (of_ocircline ?H') = opposite_ocircline ?H'"
by (metis of_circline_of_ocircline pos_oriented_of_circline)
from ounit show ?thesis
proof
assume **: "ounit_circle = moebius_ocircline M ounit_circle"
show ?thesis
using ++
unfolding perpendicular_def
by (simp, subst moebius_circline_ocircline, subst *, subst **) simp
next
assume **: "ounit_circle = moebius_ocircline M (opposite_ocircline ounit_circle)"
show ?thesis
using ++
unfolding perpendicular_def
by (simp, subst moebius_circline_ocircline, subst *, subst **) simp
qed
qed
qed simp
lemma unit_circle_fix_preserve_is_poincare_line_iff [simp]:
assumes "unit_circle_fix M"
shows "is_poincare_line (moebius_circline M H) ⟷ is_poincare_line H"
using assms
using unit_circle_fix_preserve_is_poincare_line[of M H]
using unit_circle_fix_preserve_is_poincare_line[of "moebius_inv M" "moebius_circline M H"]
by (auto simp del: unit_circle_fix_preserve_is_poincare_line)
text‹Since h-lines are preserved by transformations that fix the unit circle, so is collinearity.›
lemma unit_disc_fix_preserve_poincare_collinear [simp]:
assumes "unit_circle_fix M" "poincare_collinear A"
shows "poincare_collinear (moebius_pt M ` A)"
using assms
unfolding poincare_collinear_def
by (auto, rule_tac x="moebius_circline M p" in exI, auto)
lemma unit_disc_fix_preserve_poincare_collinear_iff [simp]:
assumes "unit_circle_fix M"
shows "poincare_collinear (moebius_pt M ` A) ⟷ poincare_collinear A"
using assms
using unit_disc_fix_preserve_poincare_collinear[of M A]
using unit_disc_fix_preserve_poincare_collinear[of "moebius_inv M" "moebius_pt M ` A"]
by (auto simp del: unit_disc_fix_preserve_poincare_collinear)
lemma unit_disc_fix_preserve_poincare_collinear3 [simp]:
assumes "unit_disc_fix M"
shows "poincare_collinear {moebius_pt M u, moebius_pt M v, moebius_pt M w} ⟷
poincare_collinear {u, v, w}"
using assms unit_disc_fix_preserve_poincare_collinear_iff[of M "{u, v, w}"]
by simp
text‹Conjugation is also an h-isometry and it preserves h-lines.›
lemma is_poincare_line_conjugate_circline [simp]:
assumes "is_poincare_line H"
shows "is_poincare_line (conjugate_circline H)"
using assms
by (transfer, transfer, auto simp add: mat_cnj_def hermitean_def mat_adj_def)
lemma is_poincare_line_conjugate_circline_iff [simp]:
shows "is_poincare_line (conjugate_circline H) ⟷ is_poincare_line H"
using is_poincare_line_conjugate_circline[of "conjugate_circline H"]
by auto
text‹Since h-lines are preserved by conjugation, so is collinearity.›
lemma conjugate_preserve_poincare_collinear [simp]:
assumes "poincare_collinear A"
shows "poincare_collinear (conjugate ` A)"
using assms
unfolding poincare_collinear_def
by auto (rule_tac x="conjugate_circline p" in exI, auto)
lemma conjugate_conjugate [simp]: "conjugate ` conjugate ` A = A"
by (auto simp add: image_iff)
lemma conjugate_preserve_poincare_collinear_iff [simp]:
shows "poincare_collinear (conjugate ` A) ⟷ poincare_collinear A"
using conjugate_preserve_poincare_collinear[of "A"]
using conjugate_preserve_poincare_collinear[of "conjugate ` A"]
by (auto simp del: conjugate_preserve_poincare_collinear)
subsubsection‹Mapping h-lines to x-axis›
text‹Each h-line in the Poincar\'e model can be mapped onto the x-axis (by a unit-disc preserving
Möbius transformation).›
lemma ex_unit_disc_fix_is_poincare_line_to_x_axis:
assumes "is_poincare_line l"
shows "∃ M. unit_disc_fix M ∧ moebius_circline M l = x_axis"
proof-
from assms obtain u v where "u ≠ v" "u ∈ unit_disc" "v ∈ unit_disc" and "{u, v} ⊆ circline_set l"
using ex_is_poincare_line_points
by blast
then obtain M where *: "unit_disc_fix M" "moebius_pt M u = 0⇩h" "moebius_pt M v ∈ positive_x_axis"
using ex_unit_disc_fix_to_zero_positive_x_axis[of u v]
by auto
moreover
hence "{0⇩h, moebius_pt M v} ⊆ circline_set x_axis"
unfolding positive_x_axis_def
by auto
moreover
have "moebius_pt M v ≠ 0⇩h"
using ‹u ≠ v› *
by (metis moebius_pt_neq_I)
moreover
have "moebius_pt M v ≠ ∞⇩h"
using ‹unit_disc_fix M› ‹v ∈ unit_disc›
using unit_disc_fix_discI
by fastforce
ultimately
show ?thesis
using ‹is_poincare_line l› ‹{u, v} ⊆ circline_set l› ‹unit_disc_fix M›
using is_poincare_line_0_real_is_x_axis[of "moebius_circline M l" "moebius_pt M v"]
by (rule_tac x="M" in exI, force)
qed
text ‹When proving facts about h-lines, without loss of generality it can be assumed that h-line is
the x-axis (if the property being proved is invariant under Möbius transformations that fix the
unit disc).›
lemma wlog_line_x_axis:
assumes is_line: "is_poincare_line H"
assumes x_axis: "P x_axis"
assumes preserves: "⋀ M. ⟦unit_disc_fix M; P (moebius_circline M H)⟧ ⟹ P H"
shows "P H"
using assms
using ex_unit_disc_fix_is_poincare_line_to_x_axis[of H]
by auto
subsection‹Construction of the h-line between the two given points›
text‹Next we show how to construct the (unique) h-line between the two given points in the Poincar\'e model›
text‹
Geometrically, h-line can be constructed by finding the inverse point of one of the two points and
by constructing the circle (or line) trough it and the two given points.
Algebraically, for two given points $u$ and $v$ in $\mathbb{C}$, the h-line matrix coefficients can
be $A = i\cdot(u\overline{v}-v\overline{u})$ and $B = i\cdot(v(|u|^2+1) - u(|v|^2+1))$.
We need to extend this to homogenous coordinates. There are several degenerate cases.
- If $\{z, w\} = \{0_h, \infty_h\}$ then there is no unique h-line (any line trough zero is an h-line).
- If z and w are mutually inverse, then the construction fails (both geometric and algebraic).
- If z and w are different points on the unit circle, then the standard construction fails (only geometric).
- None of this problematic cases occur when z and w are inside the unit disc.
We express the construction algebraically, and construct the Hermitean circline matrix for the two
points given in homogenous coordinates. It works correctly in all cases except when the two points
are the same or are mutually inverse.
›
definition mk_poincare_line_cmat :: "real ⇒ complex ⇒ complex_mat" where
[simp]: "mk_poincare_line_cmat A B = (cor A, B, cnj B, cor A)"
lemma mk_poincare_line_cmat_zero_iff:
"mk_poincare_line_cmat A B = mat_zero ⟷ A = 0 ∧ B = 0"
by auto
lemma mk_poincare_line_cmat_hermitean
[simp]: "hermitean (mk_poincare_line_cmat A B)"
by simp
lemma mk_poincare_line_cmat_scale:
"cor k *⇩s⇩m mk_poincare_line_cmat A B = mk_poincare_line_cmat (k * A) (k * B)"
by simp
definition poincare_line_cvec_cmat :: "complex_vec ⇒ complex_vec ⇒ complex_mat" where
[simp]: "poincare_line_cvec_cmat z w =
(let (z1, z2) = z;
(w1, w2) = w;
nom = w1*cnj w2*(z1*cnj z1 + z2*cnj z2) - z1*cnj z2*(w1*cnj w1 + w2*cnj w2);
den = z1*cnj z2*cnj w1*w2 - w1*cnj w2*cnj z1*z2
in if den ≠ 0 then
mk_poincare_line_cmat (Re(𝗂*den)) (𝗂*nom)
else if z1*cnj z2 ≠ 0 then
mk_poincare_line_cmat 0 (𝗂*z1*cnj z2)
else if w1*cnj w2 ≠ 0 then
mk_poincare_line_cmat 0 (𝗂*w1*cnj w2)
else
mk_poincare_line_cmat 0 𝗂)"
lemma poincare_line_cvec_cmat_AeqD:
assumes "poincare_line_cvec_cmat z w = (A, B, C, D)"
shows "A = D"
using assms
by (cases z, cases w) (auto split: if_split_asm)
lemma poincare_line_cvec_cmat_hermitean [simp]:
shows "hermitean (poincare_line_cvec_cmat z w)"
by (cases z, cases w) (auto split: if_split_asm simp del: mk_poincare_line_cmat_def)
lemma poincare_line_cvec_cmat_nonzero [simp]:
assumes "z ≠ vec_zero" "w ≠ vec_zero"
shows "poincare_line_cvec_cmat z w ≠ mat_zero"
proof-
obtain z1 z2 w1 w2 where *: "z = (z1, z2)" "w = (w1, w2)"
by (cases z, cases w, auto)
let ?den = "z1*cnj z2*cnj w1*w2 - w1*cnj w2*cnj z1*z2"
show ?thesis
proof (cases "?den ≠ 0")
case True
have "is_real (𝗂 * ?den)"
using eq_cnj_iff_real[of "𝗂 *?den"]
by (simp add: field_simps)
hence "Re (𝗂 * ?den) ≠ 0"
using ‹?den ≠ 0›
by (metis complex_i_not_zero complex_surj mult_eq_0_iff zero_complex.code)
thus ?thesis
using * ‹?den ≠ 0›
by (simp del: mk_poincare_line_cmat_def mat_zero_def add: mk_poincare_line_cmat_zero_iff)
next
case False
thus ?thesis
using *
by (simp del: mk_poincare_line_cmat_def mat_zero_def add: mk_poincare_line_cmat_zero_iff)
qed
qed
lift_definition poincare_line_hcoords_clmat :: "complex_homo_coords ⇒ complex_homo_coords ⇒ circline_mat" is poincare_line_cvec_cmat
using poincare_line_cvec_cmat_hermitean poincare_line_cvec_cmat_nonzero
by simp
lift_definition poincare_line :: "complex_homo ⇒ complex_homo ⇒ circline" is poincare_line_hcoords_clmat
proof transfer
fix za zb wa wb
assume "za ≠ vec_zero" "zb ≠ vec_zero" "wa ≠ vec_zero" "wb ≠ vec_zero"
assume "za ≈⇩v zb" "wa ≈⇩v wb"
obtain za1 za2 zb1 zb2 wa1 wa2 wb1 wb2 where
*: "(za1, za2) = za" "(zb1, zb2) = zb"
"(wa1, wa2) = wa" "(wb1, wb2) = wb"
by (cases za, cases zb, cases wa, cases wb, auto)
obtain kz kw where
**: "kz ≠ 0" "kw ≠ 0" "zb1 = kz * za1" "zb2 = kz * za2" "wb1 = kw * wa1" "wb2 = kw * wa2"
using ‹za ≈⇩v zb› ‹wa ≈⇩v wb› *[symmetric]
by auto
let ?nom = "λ z1 z2 w1 w2. w1*cnj w2*(z1*cnj z1 + z2*cnj z2) - z1*cnj z2*(w1*cnj w1 + w2*cnj w2)"
let ?den = "λ z1 z2 w1 w2. z1*cnj z2*cnj w1*w2 - w1*cnj w2*cnj z1*z2"
show "circline_eq_cmat (poincare_line_cvec_cmat za wa)
(poincare_line_cvec_cmat zb wb)"
proof-
have "∃k. k ≠ 0 ∧
poincare_line_cvec_cmat (zb1, zb2) (wb1, wb2) = cor k *⇩s⇩m poincare_line_cvec_cmat (za1, za2) (wa1, wa2)"
proof (cases "?den za1 za2 wa1 wa2 ≠ 0")
case True
hence "?den zb1 zb2 wb1 wb2 ≠ 0"
using **
by (simp add: field_simps)
let ?k = "kz * cnj kz * kw * cnj kw"
have "?k ≠ 0"
using **
by simp
have "is_real ?k"
using eq_cnj_iff_real[of ?k]
by auto
have "cor (Re ?k) = ?k"
using ‹is_real ?k›
using complex_of_real_Re
by blast
have "Re ?k ≠ 0"
using ‹?k ≠ 0› ‹cor (Re ?k) = ?k›
by (metis of_real_0)
have arg1: "Re (𝗂 * ?den zb1 zb2 wb1 wb2) = Re ?k * Re (𝗂 * ?den za1 za2 wa1 wa2)"
apply (subst **)+
apply (subst Re_mult_real[symmetric, OF ‹is_real ?k›])
apply (rule arg_cong[where f=Re])
apply (simp add: field_simps)
done
have arg2: "𝗂 * ?nom zb1 zb2 wb1 wb2 = ?k * 𝗂 * ?nom za1 za2 wa1 wa2"
using **
by (simp add: field_simps)
have "mk_poincare_line_cmat (Re (𝗂*?den zb1 zb2 wb1 wb2)) (𝗂*?nom zb1 zb2 wb1 wb2) =
cor (Re ?k) *⇩s⇩m mk_poincare_line_cmat (Re (𝗂*?den za1 za2 wa1 wa2)) (𝗂*?nom za1 za2 wa1 wa2)"
using ‹cor (Re ?k) = ?k› ‹is_real ?k›
apply (subst mk_poincare_line_cmat_scale)
apply (subst arg1, subst arg2)
apply (subst ‹cor (Re ?k) = ?k›)+
apply simp
done
thus ?thesis
using ‹?den za1 za2 wa1 wa2 ≠ 0› ‹?den zb1 zb2 wb1 wb2 ≠ 0›
using ‹Re ?k ≠ 0› ‹cor (Re ?k) = ?k›
by (rule_tac x="Re ?k" in exI, simp)
next
case False
hence "?den zb1 zb2 wb1 wb2 = 0"
using **
by (simp add: field_simps)
show ?thesis
proof (cases "za1*cnj za2 ≠ 0")
case True
hence "zb1*cnj zb2 ≠ 0"
using **
by (simp add: field_simps)
let ?k = "kz * cnj kz"
have "?k ≠ 0" "is_real ?k"
using **
using eq_cnj_iff_real[of ?k]
by auto
thus ?thesis
using ‹za1 * cnj za2 ≠ 0› ‹zb1 * cnj zb2 ≠ 0›
using ‹¬ (?den za1 za2 wa1 wa2 ≠ 0)› ‹?den zb1 zb2 wb1 wb2 = 0› **
by (rule_tac x="Re (kz * cnj kz)" in exI, auto simp add: complex.expand)
next
case False
hence "zb1 * cnj zb2 = 0"
using **
by (simp add: field_simps)
show ?thesis
proof (cases "wa1 * cnj wa2 ≠ 0")
case True
hence "wb1*cnj wb2 ≠ 0"
using **
by (simp add: field_simps)
let ?k = "kw * cnj kw"
have "?k ≠ 0" "is_real ?k"
using **
using eq_cnj_iff_real[of ?k]
by auto
thus ?thesis
using ‹¬ (za1 * cnj za2 ≠ 0)›
using ‹wa1 * cnj wa2 ≠ 0› ‹wb1 * cnj wb2 ≠ 0›
using ‹¬ (?den za1 za2 wa1 wa2 ≠ 0)› ‹?den zb1 zb2 wb1 wb2 = 0› **
by (rule_tac x="Re (kw * cnj kw)" in exI)
(auto simp add: complex.expand)
next
case False
hence "wb1 * cnj wb2 = 0"
using **
by (simp add: field_simps)
thus ?thesis
using ‹¬ (za1 * cnj za2 ≠ 0)› ‹zb1 * cnj zb2 = 0›
using ‹¬ (wa1 * cnj wa2 ≠ 0)› ‹wb1 * cnj wb2 = 0›
using ‹¬ (?den za1 za2 wa1 wa2 ≠ 0)› ‹?den zb1 zb2 wb1 wb2 = 0› **
by simp
qed
qed
qed
thus ?thesis
using *[symmetric]
by simp
qed
qed
subsubsection ‹Correctness of the construction›
text‹For finite points, our definition matches the classic algebraic definition for points in
$\mathbb{C}$ (given in ordinary, not homogenous coordinates).›
lemma poincare_line_non_homogenous:
assumes "u ≠ ∞⇩h" "v ≠ ∞⇩h" "u ≠ v" "u ≠ inversion v"
shows "let u' = to_complex u; v' = to_complex v;
A = 𝗂 * (u' * cnj v' - v' * cnj u');
B = 𝗂 * (v' * ((cmod u')⇧2 + 1) - u' * ((cmod v')⇧2 + 1))
in poincare_line u v = mk_circline A B (cnj B) A"
using assms
unfolding unit_disc_def disc_def inversion_def
apply (simp add: Let_def)
proof (transfer, transfer, safe)
fix u1 u2 v1 v2
assume uv: "(u1, u2) ≠ vec_zero" "(v1, v2) ≠ vec_zero"
"¬ (u1, u2) ≈⇩v ∞⇩v" "¬ (v1, v2) ≈⇩v ∞⇩v"
"¬ (u1, u2) ≈⇩v (v1, v2)" "¬ (u1, u2) ≈⇩v conjugate_cvec (reciprocal_cvec (v1, v2))"
let ?u = "to_complex_cvec (u1, u2)" and ?v = "to_complex_cvec (v1, v2)"
let ?A = "𝗂 * (?u * cnj ?v - ?v * cnj ?u)"
let ?B = "𝗂 * (?v * ((cor (cmod ?u))⇧2 + 1) - ?u * ((cor (cmod ?v))⇧2 + 1))"
let ?C = "- (𝗂 * (cnj ?v * ((cor (cmod ?u))⇧2 + 1) - cnj ?u * ((cor (cmod ?v))⇧2 + 1)))"
let ?D = ?A
let ?H = "(?A, ?B, ?C, ?D)"
let ?den = "u1 * cnj u2 * cnj v1 * v2 - v1 * cnj v2 * cnj u1 * u2"
have "u2 ≠ 0" "v2 ≠ 0"
using uv
using inf_cvec_z2_zero_iff
by blast+
have "¬ (u1, u2) ≈⇩v (cnj v2, cnj v1)"
using uv(6)
by (simp add: vec_cnj_def)
moreover
have "(cnj v2, cnj v1) ≠ vec_zero"
using uv(2)
by auto
ultimately
have *: "u1 * cnj v1 ≠ u2 * cnj v2" "u1 * v2 ≠ u2 * v1"
using uv(5) uv(1) uv(2) ‹u2 ≠ 0› ‹v2 ≠ 0›
using complex_cvec_eq_mix
by blast+
show "circline_eq_cmat (poincare_line_cvec_cmat (u1, u2) (v1, v2))
(mk_circline_cmat ?A ?B ?C ?D)"
proof (cases "?den ≠ 0")
case True
let ?nom = "v1 * cnj v2 * (u1 * cnj u1 + u2 * cnj u2) - u1 * cnj u2 * (v1 * cnj v1 + v2 * cnj v2)"
let ?H' = "mk_poincare_line_cmat (Re (𝗂 * ?den)) (𝗂 * ?nom)"
have "circline_eq_cmat ?H ?H'"
proof-
let ?k = "(u2 * cnj v2) * (v2 * cnj u2)"
have "is_real ?k"
using eq_cnj_iff_real
by fastforce
hence "cor (Re ?k) = ?k"
using complex_of_real_Re
by blast
have "Re (𝗂 * ?den) = Re ?k * ?A"
proof-
have "?A = cnj ?A"
by (simp add: field_simps)
hence "is_real ?A"
using eq_cnj_iff_real
by fastforce
moreover
have "𝗂 * ?den = cnj (𝗂 * ?den)"
by (simp add: field_simps)
hence "is_real (𝗂 * ?den)"
using eq_cnj_iff_real
by fastforce
hence "cor (Re (𝗂 * ?den)) = 𝗂 * ?den"
using complex_of_real_Re
by blast
ultimately
show ?thesis
using ‹cor (Re ?k) = ?k›
by (simp add: field_simps)
qed
moreover
have "𝗂 * ?nom = Re ?k * ?B"
using ‹cor (Re ?k) = ?k› ‹u2 ≠ 0› ‹v2 ≠ 0› complex_mult_cnj_cmod[symmetric]
by (auto simp add: field_simps)
moreover
have "?k ≠ 0"
using ‹u2 ≠ 0› ‹v2 ≠ 0›
by simp
hence "Re ?k ≠ 0"
using ‹is_real ?k›
by (metis ‹cor (Re ?k) = ?k› of_real_0)
ultimately
show ?thesis
by simp (rule_tac x="Re ?k" in exI, simp add: mult.commute)
qed
moreover
have "poincare_line_cvec_cmat (u1, u2) (v1, v2) = ?H'"
using ‹?den ≠ 0›
unfolding poincare_line_cvec_cmat_def
by (simp add: Let_def)
moreover
hence "hermitean ?H' ∧ ?H' ≠ mat_zero"
by (metis mk_poincare_line_cmat_hermitean poincare_line_cvec_cmat_nonzero uv(1) uv(2))
hence "hermitean ?H ∧ ?H ≠ mat_zero"
using ‹circline_eq_cmat ?H ?H'›
using circline_eq_cmat_hermitean_nonzero[of ?H' ?H] symp_circline_eq_cmat
unfolding symp_def
by metis
hence "mk_circline_cmat ?A ?B ?C ?D = ?H"
by simp
ultimately
have "circline_eq_cmat (mk_circline_cmat ?A ?B ?C ?D)
(poincare_line_cvec_cmat (u1, u2) (v1, v2))"
by simp
thus ?thesis
using symp_circline_eq_cmat
unfolding symp_def
by blast
next
case False
let ?d = "v1 * (u1 * cnj u1 / (u2 * cnj u2) + 1) / v2 - u1 * (v1 * cnj v1 / (v2 * cnj v2) + 1) / u2"
let ?cd = "cnj v1 * (u1 * cnj u1 / (u2 * cnj u2) + 1) / cnj v2 - cnj u1 * (v1 * cnj v1 / (v2 * cnj v2) + 1) / cnj u2"
have "cnj ?d = ?cd"
by (simp add: mult.commute)
let ?d1 = "(v1 / v2) * (cnj u1 / cnj u2) - 1"
let ?d2 = "u1 / u2 - v1 / v2"
have **: "?d = ?d1 * ?d2"
using ‹¬ ?den ≠ 0› ‹u2 ≠ 0› ‹v2 ≠ 0›
by(simp add: field_simps)
hence "?d ≠ 0"
using ‹¬ ?den ≠ 0› ‹u2 ≠ 0› ‹v2 ≠ 0› *
by auto (simp add: field_simps)+
have "is_real ?d1"
proof-
have "cnj ?d1 = ?d1"
using ‹¬ ?den ≠ 0› ‹u2 ≠ 0› ‹v2 ≠ 0› *
by (simp add: field_simps)
thus ?thesis
using eq_cnj_iff_real
by blast
qed
show ?thesis
proof (cases "u1 * cnj u2 ≠ 0")
case True
let ?nom = "u1 * cnj u2"
let ?H' = "mk_poincare_line_cmat 0 (𝗂 * ?nom)"
have "circline_eq_cmat ?H ?H'"
proof-
let ?k = "(u1 * cnj u2) / ?d"
have "is_real ?k"
proof-
have "is_real ((u1 * cnj u2) / ?d2)"
proof-
let ?rhs = "(u2 * cnj u2) / (1 - (v1*u2)/(u1*v2))"
have 1: "(u1 * cnj u2) / ?d2 = ?rhs"
using ‹¬ ?den ≠ 0› ‹u2 ≠ 0› ‹v2 ≠ 0› * ‹u1 * cnj u2 ≠ 0›
by (simp add: field_simps)
moreover
have "cnj ?rhs = ?rhs"
proof-
have "cnj (1 - v1 * u2 / (u1 * v2)) = 1 - v1 * u2 / (u1 * v2)"
using ‹¬ ?den ≠ 0› ‹u2 ≠ 0› ‹v2 ≠ 0› * ‹u1 * cnj u2 ≠ 0›
by (simp add: field_simps)
moreover
have "cnj (u2 * cnj u2) = u2 * cnj u2"
by simp
ultimately
show ?thesis
by simp
qed
ultimately
show ?thesis
using eq_cnj_iff_real
by fastforce
qed
thus ?thesis
using ** ‹is_real ?d1›
by (metis complex_cnj_divide divide_divide_eq_left' eq_cnj_iff_real)
qed
have "?k ≠ 0"
using ‹?d ≠ 0› ‹u1 * cnj u2 ≠ 0›
by simp
have "cnj ?k = ?k"
using ‹is_real ?k›
using eq_cnj_iff_real by blast
have "Re ?k ≠ 0"
using ‹?k ≠ 0› ‹is_real ?k›
by (metis complex.expand zero_complex.simps(1) zero_complex.simps(2))
have "u1 * cnj u2 = ?k * ?d"
using ‹?d ≠ 0›
by simp
moreover
hence "cnj u1 * u2 = cnj ?k * cnj ?d"
by (metis complex_cnj_cnj complex_cnj_mult)
hence "cnj u1 * u2 = ?k * ?cd"
using ‹cnj ?k = ?k› ‹cnj ?d = ?cd›
by metis
ultimately
show ?thesis
using ‹~ ?den ≠ 0› ‹u1 * cnj u2 ≠ 0› ‹u2 ≠ 0› ‹v2 ≠ 0› ‹Re ?k ≠ 0› ‹is_real ?k› ‹?d ≠ 0›
using complex_mult_cnj_cmod[symmetric, of u1]
using complex_mult_cnj_cmod[symmetric, of v1]
using complex_mult_cnj_cmod[symmetric, of u2]
using complex_mult_cnj_cmod[symmetric, of v2]
apply (simp add: power_divide norm_mult norm_divide)
apply (rule_tac x="Re ?k" in exI)
apply simp
apply (simp add: field_simps)
done
qed
moreover
have "poincare_line_cvec_cmat (u1, u2) (v1, v2) = ?H'"
using ‹¬ ?den ≠ 0› ‹u1 * cnj u2 ≠ 0›
unfolding poincare_line_cvec_cmat_def
by (simp add: Let_def)
moreover
hence "hermitean ?H' ∧ ?H' ≠ mat_zero"
by (metis mk_poincare_line_cmat_hermitean poincare_line_cvec_cmat_nonzero uv(1) uv(2))
hence "hermitean ?H ∧ ?H ≠ mat_zero"
using ‹circline_eq_cmat ?H ?H'›
using circline_eq_cmat_hermitean_nonzero[of ?H' ?H] symp_circline_eq_cmat
unfolding symp_def
by metis
hence "mk_circline_cmat ?A ?B ?C ?D = ?H"
by simp
ultimately
have "circline_eq_cmat (mk_circline_cmat ?A ?B ?C ?D)
(poincare_line_cvec_cmat (u1, u2) (v1, v2))"
by simp
thus ?thesis
using symp_circline_eq_cmat
unfolding symp_def
by blast
next
case False
show ?thesis
proof (cases "v1 * cnj v2 ≠ 0")
case True
let ?nom = "v1 * cnj v2"
let ?H' = "mk_poincare_line_cmat 0 (𝗂 * ?nom)"
have "circline_eq_cmat ?H ?H'"
proof-
let ?k = "(v1 * cnj v2) / ?d"
have "is_real ?k"
proof-
have "is_real ((v1 * cnj v2) / ?d2)"
proof-
let ?rhs = "(v2 * cnj v2) / ((u1*v2)/(u2*v1) - 1)"
have 1: "(v1 * cnj v2) / ?d2 = ?rhs"
using ‹¬ ?den ≠ 0› ‹u2 ≠ 0› ‹v2 ≠ 0› * ‹v1 * cnj v2 ≠ 0›
by (simp add: field_simps)
moreover
have "cnj ?rhs = ?rhs"
proof-
have "cnj (u1 * v2 / (u2 * v1) - 1) = u1 * v2 / (u2 * v1) - 1"
using ‹¬ ?den ≠ 0› ‹u2 ≠ 0› ‹v2 ≠ 0› * ‹v1 * cnj v2 ≠ 0›
by (simp add: field_simps)
moreover
have "cnj (v2 * cnj v2) = v2 * cnj v2"
by simp
ultimately
show ?thesis
by simp
qed
ultimately
show ?thesis
using eq_cnj_iff_real
by fastforce
qed
thus ?thesis
using ** ‹is_real ?d1›
by (metis complex_cnj_divide divide_divide_eq_left' eq_cnj_iff_real)
qed
have "?k ≠ 0"
using ‹?d ≠ 0› ‹v1 * cnj v2 ≠ 0›
by simp
have "cnj ?k = ?k"
using ‹is_real ?k›
using eq_cnj_iff_real by blast
have "Re ?k ≠ 0"
using ‹?k ≠ 0› ‹is_real ?k›
by (metis complex.expand zero_complex.simps(1) zero_complex.simps(2))
have "v1 * cnj v2 = ?k * ?d"
using ‹?d ≠ 0›
by simp
moreover
hence "cnj v1 * v2 = cnj ?k * cnj ?d"
by (metis complex_cnj_cnj complex_cnj_mult)
hence "cnj v1 * v2 = ?k * ?cd"
using ‹cnj ?k = ?k› ‹cnj ?d = ?cd›
by metis
ultimately
show ?thesis
using ‹~ ?den ≠ 0› ‹v1 * cnj v2 ≠ 0› ‹u2 ≠ 0› ‹v2 ≠ 0› ‹Re ?k ≠ 0› ‹is_real ?k› ‹?d ≠ 0›
using complex_mult_cnj_cmod[symmetric, of u1]
using complex_mult_cnj_cmod[symmetric, of v1]
using complex_mult_cnj_cmod[symmetric, of u2]
using complex_mult_cnj_cmod[symmetric, of v2]
apply (simp add: power_divide norm_mult norm_divide)
apply (rule_tac x="Re ?k" in exI)
apply simp
apply (simp add: field_simps)
done
qed
moreover
have "poincare_line_cvec_cmat (u1, u2) (v1, v2) = ?H'"
using ‹¬ ?den ≠ 0› ‹¬ u1 * cnj u2 ≠ 0› ‹v1 * cnj v2 ≠ 0›
unfolding poincare_line_cvec_cmat_def
by (simp add: Let_def)
moreover
hence "hermitean ?H' ∧ ?H' ≠ mat_zero"
by (metis mk_poincare_line_cmat_hermitean poincare_line_cvec_cmat_nonzero uv(1) uv(2))
hence "hermitean ?H ∧ ?H ≠ mat_zero"
using ‹circline_eq_cmat ?H ?H'›
using circline_eq_cmat_hermitean_nonzero[of ?H' ?H] symp_circline_eq_cmat
unfolding symp_def
by metis
hence "mk_circline_cmat ?A ?B ?C ?D = ?H"
by simp
ultimately
have "circline_eq_cmat (mk_circline_cmat ?A ?B ?C ?D)
(poincare_line_cvec_cmat (u1, u2) (v1, v2))"
by simp
thus ?thesis
using symp_circline_eq_cmat
unfolding symp_def
by blast
next
case False
hence False
using ‹¬ ?den ≠ 0› ‹¬ u1 * cnj u2 ≠ 0› uv
by (simp add: ‹u2 ≠ 0› ‹v2 ≠ 0›)
thus ?thesis
by simp
qed
qed
qed
qed
text‹Our construction (in homogenous coordinates) always yields an h-line that contain two starting
points (this also holds for all degenerate cases except when points are the same).›
lemma poincare_line [simp]:
assumes "z ≠ w"
shows "on_circline (poincare_line z w) z"
"on_circline (poincare_line z w) w"
proof-
have "on_circline (poincare_line z w) z ∧ on_circline (poincare_line z w) w"
using assms
proof (transfer, transfer)
fix z w
assume vz: "z ≠ vec_zero" "w ≠ vec_zero"
obtain z1 z2 w1 w2 where
zw: "(z1, z2) = z" "(w1, w2) = w"
by (cases z, cases w, auto)
let ?den = "z1*cnj z2*cnj w1*w2 - w1*cnj w2*cnj z1*z2"
have *: "cor (Re (𝗂 * ?den)) = 𝗂 * ?den"
proof-
have "cnj ?den = -?den"
by auto
hence "is_imag ?den"
using eq_minus_cnj_iff_imag[of ?den]
by simp
thus ?thesis
using complex_of_real_Re[of "𝗂 * ?den"]
by simp
qed
show "on_circline_cmat_cvec (poincare_line_cvec_cmat z w) z ∧
on_circline_cmat_cvec (poincare_line_cvec_cmat z w) w"
unfolding poincare_line_cvec_cmat_def mk_poincare_line_cmat_def
apply (subst zw[symmetric])+
unfolding Let_def prod.case
apply (subst *)+
by (auto simp add: vec_cnj_def field_simps)
qed
thus "on_circline (poincare_line z w) z" "on_circline (poincare_line z w) w"
by auto
qed
lemma poincare_line_circline_set [simp]:
assumes "z ≠ w"
shows "z ∈ circline_set (poincare_line z w)"
"w ∈ circline_set (poincare_line z w)"
using assms
by (auto simp add: circline_set_def)
text‹When the points are different, the constructed line matrix always has a negative determinant›
lemma poincare_line_type:
assumes "z ≠ w"
shows "circline_type (poincare_line z w) = -1"
proof-
have "∃ a b. a ≠ b ∧ {a, b} ⊆ circline_set (poincare_line z w)"
using poincare_line[of z w] assms
unfolding circline_set_def
by (rule_tac x=z in exI, rule_tac x=w in exI, simp)
thus ?thesis
using circline_type[of "poincare_line z w"]
using circline_type_pos_card_eq0[of "poincare_line z w"]
using circline_type_zero_card_eq1[of "poincare_line z w"]
by auto
qed
text‹The constructed line is an h-line in the Poincar\'e model (in all cases when the two points are
different)›
lemma is_poincare_line_poincare_line [simp]:
assumes "z ≠ w"
shows "is_poincare_line (poincare_line z w)"
using poincare_line_type[of z w, OF assms]
proof (transfer, transfer)
fix z w
assume vz: "z ≠ vec_zero" "w ≠ vec_zero"
obtain A B C D where *: "poincare_line_cvec_cmat z w = (A, B, C, D)"
by (cases "poincare_line_cvec_cmat z w") auto
assume "circline_type_cmat (poincare_line_cvec_cmat z w) = - 1"
thus "is_poincare_line_cmat (poincare_line_cvec_cmat z w)"
using vz *
using poincare_line_cvec_cmat_hermitean[of z w]
using poincare_line_cvec_cmat_nonzero[of z w]
using poincare_line_cvec_cmat_AeqD[of z w A B C D]
using hermitean_elems[of A B C D]
using cmod_power2[of D] cmod_power2[of C]
unfolding is_poincare_line_cmat_def
by (simp del: poincare_line_cvec_cmat_def add: sgn_1_neg power2_eq_square)
qed
text ‹When the points are different, the constructed h-line between two points also contains their inverses›
lemma poincare_line_inversion:
assumes "z ≠ w"
shows "on_circline (poincare_line z w) (inversion z)"
"on_circline (poincare_line z w) (inversion w)"
using assms
using is_poincare_line_poincare_line[OF ‹z ≠ w›]
using is_poincare_line_inverse_point
unfolding circline_set_def
by auto
text ‹When the points are different, the onstructed h-line between two points contains the inverse of its every point›
lemma poincare_line_inversion_full:
assumes "u ≠ v"
assumes "on_circline (poincare_line u v) x"
shows "on_circline (poincare_line u v) (inversion x)"
using is_poincare_line_inverse_point[of "poincare_line u v" x]
using is_poincare_line_poincare_line[OF ‹u ≠ v›] assms
unfolding circline_set_def
by simp
subsubsection ‹Existence of h-lines›
text‹There is an h-line trough every point in the Poincar\'e model›
lemma ex_poincare_line_one_point:
shows "∃ l. is_poincare_line l ∧ z ∈ circline_set l"
proof (cases "z = 0⇩h")
case True
thus ?thesis
by (rule_tac x="x_axis" in exI) simp
next
case False
thus ?thesis
by (rule_tac x="poincare_line 0⇩h z" in exI) auto
qed
lemma poincare_collinear_singleton [simp]:
assumes "u ∈ unit_disc"
shows "poincare_collinear {u}"
using assms
using ex_poincare_line_one_point[of u]
by (auto simp add: poincare_collinear_def)
text‹There is an h-line trough every two points in the Poincar\'e model›
lemma ex_poincare_line_two_points:
assumes "z ≠ w"
shows "∃ l. is_poincare_line l ∧ z ∈ circline_set l ∧ w ∈ circline_set l"
using assms
by (rule_tac x="poincare_line z w" in exI, simp)
lemma poincare_collinear_doubleton [simp]:
assumes "u ∈ unit_disc" "v ∈ unit_disc"
shows "poincare_collinear {u, v}"
using assms
using ex_poincare_line_one_point[of u]
using ex_poincare_line_two_points[of u v]
by (cases "u = v") (simp_all add: poincare_collinear_def)
subsubsection ‹Uniqueness of h-lines›
text ‹The only h-line between two points is the one obtained by the line-construction.›
text ‹First we show this only for two different points inside the disc.›
lemma unique_poincare_line:
assumes in_disc: "u ≠ v" "u ∈ unit_disc" "v ∈ unit_disc"
assumes on_l: "u ∈ circline_set l" "v ∈ circline_set l" "is_poincare_line l"
shows "l = poincare_line u v"
using assms
using unique_is_poincare_line[of u v l "poincare_line u v"]
unfolding circline_set_def
by auto
text‹The assumption that the points are inside the disc can be relaxed.›
lemma unique_poincare_line_general:
assumes in_disc: "u ≠ v" "u ≠ inversion v"
assumes on_l: "u ∈ circline_set l" "v ∈ circline_set l" "is_poincare_line l"
shows "l = poincare_line u v"
using assms
using unique_is_poincare_line_general[of u v l "poincare_line u v"]
unfolding circline_set_def
by auto
text‹The explicit line construction enables us to prove that there exists a unique h-line through any
given two h-points (uniqueness part was already shown earlier).›
text ‹First we show this only for two different points inside the disc.›
lemma ex1_poincare_line:
assumes "u ≠ v" "u ∈ unit_disc" "v ∈ unit_disc"
shows "∃! l. is_poincare_line l ∧ u ∈ circline_set l ∧ v ∈ circline_set l"
proof (rule ex1I)
let ?l = "poincare_line u v"
show "is_poincare_line ?l ∧ u ∈ circline_set ?l ∧ v ∈ circline_set ?l"
using assms
unfolding circline_set_def
by auto
next
fix l
assume "is_poincare_line l ∧ u ∈ circline_set l ∧ v ∈ circline_set l"
thus "l = poincare_line u v"
using unique_poincare_line assms
by auto
qed
text ‹The assumption that the points are in the disc can be relaxed.›
lemma ex1_poincare_line_general:
assumes "u ≠ v" "u ≠ inversion v"
shows "∃! l. is_poincare_line l ∧ u ∈ circline_set l ∧ v ∈ circline_set l"
proof (rule ex1I)
let ?l = "poincare_line u v"
show "is_poincare_line ?l ∧ u ∈ circline_set ?l ∧ v ∈ circline_set ?l"
using assms
unfolding circline_set_def
by auto
next
fix l
assume "is_poincare_line l ∧ u ∈ circline_set l ∧ v ∈ circline_set l"
thus "l = poincare_line u v"
using unique_poincare_line_general assms
by auto
qed
subsubsection ‹Some consequences of line uniqueness›
text‹H-line $uv$ is the same as the h-line $vu$.›
lemma poincare_line_sym:
assumes "u ∈ unit_disc" "v ∈ unit_disc" "u ≠ v"
shows "poincare_line u v = poincare_line v u"
using assms
using unique_poincare_line[of u v "poincare_line v u"]
by simp
lemma poincare_line_sym_general:
assumes "u ≠ v" "u ≠ inversion v"
shows "poincare_line u v = poincare_line v u"
using assms
using unique_poincare_line_general[of u v "poincare_line v u"]
by simp
text‹Each h-line is the h-line constructed out of its two arbitrary different points.›
lemma ex_poincare_line_points:
assumes "is_poincare_line H"
shows "∃ u v. u ∈ unit_disc ∧ v ∈ unit_disc ∧ u ≠ v ∧ H = poincare_line u v"
using assms
using ex_is_poincare_line_points
using unique_poincare_line[where l=H]
by fastforce
text‹If an h-line contains two different points on x-axis/y-axis then it is the x-axis/y-axis.›
lemma poincare_line_0_real_is_x_axis:
assumes "x ∈ circline_set x_axis" "x ≠ 0⇩h" "x ≠ ∞⇩h"
shows "poincare_line 0⇩h x = x_axis"
using assms
using is_poincare_line_0_real_is_x_axis[of "poincare_line 0⇩h x" x]
by auto
lemma poincare_line_0_imag_is_y_axis:
assumes "y ∈ circline_set y_axis" "y ≠ 0⇩h" "y ≠ ∞⇩h"
shows "poincare_line 0⇩h y = y_axis"
using assms
using is_poincare_line_0_imag_is_y_axis[of "poincare_line 0⇩h y" y]
by auto
lemma poincare_line_x_axis:
assumes "x ∈ unit_disc" "y ∈ unit_disc" "x ∈ circline_set x_axis" "y ∈ circline_set x_axis" "x ≠ y"
shows "poincare_line x y = x_axis"
using assms
using unique_poincare_line
by auto
lemma poincare_line_minus_one_one [simp]:
shows "poincare_line (of_complex (-1)) (of_complex 1) = x_axis"
proof-
have "0⇩h ∈ circline_set (poincare_line (of_complex (-1)) (of_complex 1))"
unfolding circline_set_def
by simp (transfer, transfer, simp add: vec_cnj_def)
hence "poincare_line 0⇩h (of_complex 1) = poincare_line (of_complex (-1)) (of_complex 1)"
by (metis is_poincare_line_poincare_line is_poincare_line_trough_zero_trough_infty not_zero_on_unit_circle of_complex_inj of_complex_one one_neq_neg_one one_on_unit_circle poincare_line_0_real_is_x_axis poincare_line_circline_set(2) reciprocal_involution reciprocal_one reciprocal_zero unique_circline_01inf')
thus ?thesis
using poincare_line_0_real_is_x_axis[of "of_complex 1"]
by auto
qed
subsubsection ‹Transformations of constructed lines›
text‹Unit dics preserving Möbius transformations preserve the h-line construction›
lemma unit_disc_fix_preserve_poincare_line [simp]:
assumes "unit_disc_fix M" "u ∈ unit_disc" "v ∈ unit_disc" "u ≠ v"
shows "poincare_line (moebius_pt M u) (moebius_pt M v) = moebius_circline M (poincare_line u v)"
proof (rule unique_poincare_line[symmetric])
show "moebius_pt M u ≠ moebius_pt M v"
using ‹u ≠ v›
by auto
next
show "moebius_pt M u ∈ circline_set (moebius_circline M (poincare_line u v))"
"moebius_pt M v ∈ circline_set (moebius_circline M (poincare_line u v))"
unfolding circline_set_def
using moebius_circline[of M "poincare_line u v"] ‹u ≠ v›
by auto
next
from assms(1) have "unit_circle_fix M"
by simp
thus "is_poincare_line (moebius_circline M (poincare_line u v))"
using unit_circle_fix_preserve_is_poincare_line assms
by auto
next
show "moebius_pt M u ∈ unit_disc" "moebius_pt M v ∈ unit_disc"
using assms(2-3) unit_disc_fix_iff[OF assms(1)]
by auto
qed
text‹Conjugate preserve the h-line construction›
lemma conjugate_preserve_poincare_line [simp]:
assumes "u ∈ unit_disc" "v ∈ unit_disc" "u ≠ v"
shows "poincare_line (conjugate u) (conjugate v) = conjugate_circline (poincare_line u v)"
proof-
have "conjugate u ≠ conjugate v"
using ‹u ≠ v›
by (auto simp add: conjugate_inj)
moreover
have "conjugate u ∈ unit_disc" "conjugate v ∈ unit_disc"
using assms
by auto
moreover
have "conjugate u ∈ circline_set (conjugate_circline (poincare_line u v))"
"conjugate v ∈ circline_set (conjugate_circline (poincare_line u v))"
using ‹u ≠ v›
by simp_all
moreover
have "is_poincare_line (conjugate_circline (poincare_line u v))"
using is_poincare_line_poincare_line[OF ‹u ≠ v›]
by simp
ultimately
show ?thesis
using unique_poincare_line[of "conjugate u" "conjugate v" "conjugate_circline (poincare_line u v)"]
by simp
qed
subsubsection ‹Collinear points and h-lines›
lemma poincare_collinear3_poincare_line_general:
assumes "poincare_collinear {a, a1, a2}" "a1 ≠ a2" "a1 ≠ inversion a2"
shows "a ∈ circline_set (poincare_line a1 a2)"
using assms
using poincare_collinear_def unique_poincare_line_general
by auto
lemma poincare_line_poincare_collinear3_general:
assumes "a ∈ circline_set (poincare_line a1 a2)" "a1 ≠ a2"
shows "poincare_collinear {a, a1, a2}"
using assms
unfolding poincare_collinear_def
by (rule_tac x="poincare_line a1 a2" in exI, simp)
lemma poincare_collinear3_poincare_lines_equal_general:
assumes "poincare_collinear {a, a1, a2}" "a ≠ a1" "a ≠ a2" "a ≠ inversion a1" "a ≠ inversion a2"
shows "poincare_line a a1 = poincare_line a a2"
using assms
using unique_poincare_line_general[of a a2 "poincare_line a a1"]
by (simp add: insert_commute poincare_collinear3_poincare_line_general)
subsubsection ‹Points collinear with @{term "0⇩h"}›
lemma poincare_collinear_zero_iff:
assumes "of_complex y' ∈ unit_disc" and "of_complex z' ∈ unit_disc" and
"y' ≠ z'" and "y' ≠ 0" and "z' ≠ 0"
shows "poincare_collinear {0⇩h, of_complex y', of_complex z'} ⟷
y'*cnj z' = cnj y'*z'" (is "?lhs ⟷ ?rhs")
proof-
have "of_complex y' ≠ of_complex z'"
using assms
using of_complex_inj
by blast
show ?thesis
proof
assume ?lhs
hence "0⇩h ∈ circline_set (poincare_line (of_complex y') (of_complex z'))"
using unique_poincare_line[of "of_complex y'" "of_complex z'"]
using assms ‹of_complex y' ≠ of_complex z'›
unfolding poincare_collinear_def
by auto
moreover
let ?mix = "y' * cnj z' - cnj y' * z'"
have "is_real (𝗂 * ?mix)"
using eq_cnj_iff_real[of ?mix]
by auto
hence "y' * cnj z' = cnj y' * z' ⟷ Re (𝗂 * ?mix) = 0"
using complex.expand[of "𝗂 * ?mix" 0]
by (metis complex_i_not_zero eq_iff_diff_eq_0 mult_eq_0_iff zero_complex.simps(1) zero_complex.simps(2))
ultimately
show ?rhs
using ‹y' ≠ z'› ‹y' ≠ 0› ‹z' ≠ 0›
unfolding circline_set_def
by simp (transfer, transfer, auto simp add: vec_cnj_def split: if_split_asm, metis Re_complex_of_real Re_mult_real Im_complex_of_real)
next
assume ?rhs
thus ?lhs
using assms ‹of_complex y' ≠ of_complex z'›
unfolding poincare_collinear_def
unfolding circline_set_def
apply (rule_tac x="poincare_line (of_complex y') (of_complex z')" in exI)
apply auto
apply (transfer, transfer, simp add: vec_cnj_def)
done
qed
qed
lemma poincare_collinear_zero_polar_form:
assumes "poincare_collinear {0⇩h, of_complex x, of_complex y}" and
"x ≠ 0" and "y ≠ 0" and "of_complex x ∈ unit_disc" and "of_complex y ∈ unit_disc"
shows "∃ φ rx ry. x = cor rx * cis φ ∧ y = cor ry * cis φ ∧ rx ≠ 0 ∧ ry ≠ 0"
proof-
from ‹x ≠ 0› ‹y ≠ 0› obtain φ φ' rx ry where
polar: "x = cor rx * cis φ" "y = cor ry * cis φ'" and "φ = Arg x" "φ' = Arg y"
by (metis cmod_cis)
hence "rx ≠ 0" "ry ≠ 0"
using ‹x ≠ 0› ‹y ≠ 0›
by auto
have "of_complex y ∈ circline_set (poincare_line 0⇩h (of_complex x))"
using assms
using unique_poincare_line[of "0⇩h" "of_complex x"]
unfolding poincare_collinear_def
unfolding circline_set_def
using of_complex_zero_iff
by fastforce
hence "cnj x * y = x * cnj y"
using ‹x ≠ 0› ‹y ≠ 0›
unfolding circline_set_def
by simp (transfer, transfer, simp add: vec_cnj_def field_simps)
hence "cis(φ' - φ) = cis(φ - φ')"
using polar ‹rx ≠ 0› ‹ry ≠ 0›
by (simp add: cis_mult)
hence "sin (φ' - φ) = 0"
using cis_diff_cis_opposite[of "φ' - φ"]
by simp
then obtain k :: int where "φ' - φ = k * pi"
using sin_zero_iff_int2[of "φ' - φ"]
by auto
hence *: "φ' = φ + k * pi"
by simp
show ?thesis
proof (cases "even k")
case True
then obtain k' where "k = 2*k'"
using evenE by blast
hence "cis φ = cis φ'"
using * cos_periodic_int sin_periodic_int
by (simp add: cis.ctr field_simps)
thus ?thesis
using polar ‹rx ≠ 0› ‹ry ≠ 0›
by (rule_tac x=φ in exI, rule_tac x=rx in exI, rule_tac x=ry in exI) simp
next
case False
then obtain k' where "k = 2*k' + 1"
using oddE by blast
hence "cis φ = - cis φ'"
using * cos_periodic_int sin_periodic_int
by (simp add: cis.ctr complex_minus field_simps)
thus ?thesis
using polar ‹rx ≠ 0› ‹ry ≠ 0›
by (rule_tac x=φ in exI, rule_tac x=rx in exI, rule_tac x="-ry" in exI) simp
qed
qed
end