Theory Oriented_Circlines
section ‹Oriented circlines›
theory Oriented_Circlines
imports Circlines
begin
subsection ‹Oriented circlines definition›
text ‹In this section we describe how the orientation is introduced for the circlines. Similarly as
the set of circline points, the set of disc points is introduced using the quadratic form induced by
the circline matrix --- the set of points of the circline disc is the set of points such that
satisfy that $A\cdot z\cdot \overline{z} + B\cdot \overline{z} + C\cdot z + D < 0$, where
$(A, B, C, D)$ is a circline matrix representative Hermitean matrix. As the
set of disc points must be invariant to the choice of representative, it is clear that oriented
circlines matrices are equivalent only if they are proportional by a positive real factor (recall
that unoriented circline allowed arbitrary non-zero real factors).›
definition ocircline_eq_cmat :: "complex_mat ⇒ complex_mat ⇒ bool" where
[simp]: "ocircline_eq_cmat A B ⟷(∃ k::real. k > 0 ∧ B = cor k *⇩s⇩m A)"
lift_definition ocircline_eq_clmat :: "circline_mat ⇒ circline_mat ⇒ bool" is ocircline_eq_cmat
done
lemma ocircline_eq_cmat_id [simp]:
shows "ocircline_eq_cmat H H"
by (simp, rule_tac x=1 in exI, simp)
quotient_type ocircline = circline_mat / ocircline_eq_clmat
proof (rule equivpI)
show "reflp ocircline_eq_clmat"
unfolding reflp_def
by transfer (auto, rule_tac x="1" in exI, simp)
next
show "symp ocircline_eq_clmat"
unfolding symp_def
by transfer (simp only: ocircline_eq_cmat_def, safe, rule_tac x="1/k" in exI, simp)
next
show "transp ocircline_eq_clmat"
unfolding transp_def
by transfer (simp only: ocircline_eq_cmat_def, safe, rule_tac x="k*ka" in exI, simp)
qed
subsection ‹Points on oriented circlines›
text ‹Boundary of the circline.›
lift_definition on_ocircline :: "ocircline ⇒ complex_homo ⇒ bool" is on_circline_clmat_hcoords
by transfer (simp del: quad_form_def, (erule exE)+, simp add: quad_form_scale_m quad_form_scale_v del: quad_form_def)
definition ocircline_set :: "ocircline ⇒ complex_homo set" where
"ocircline_set H = {z. on_ocircline H z}"
lemma ocircline_set_I [simp]:
assumes "on_ocircline H z"
shows "z ∈ ocircline_set H"
using assms
unfolding ocircline_set_def
by simp
subsection ‹Disc and disc complement - in and out points›
text ‹Interior and the exterior of an oriented circline.›
definition in_ocircline_cmat_cvec :: "complex_mat ⇒ complex_vec ⇒ bool" where
[simp]: "in_ocircline_cmat_cvec H z ⟷ Re (quad_form z H) < 0"
lift_definition in_ocircline_clmat_hcoords :: "circline_mat ⇒ complex_homo_coords ⇒ bool" is in_ocircline_cmat_cvec
done
lift_definition in_ocircline :: "ocircline ⇒ complex_homo ⇒ bool" is in_ocircline_clmat_hcoords
proof transfer
fix H H' z z'
assume hh: "hermitean H ∧ H ≠ mat_zero" and "hermitean H' ∧ H' ≠ mat_zero" and
"z ≠ vec_zero" and "z' ≠ vec_zero"
assume "ocircline_eq_cmat H H'" and "z ≈⇩v z'"
then obtain k k' where
*: "0 < k" "H' = cor k *⇩s⇩m H" "k' ≠ 0" "z' = k' *⇩s⇩v z"
by auto
hence "quad_form z' H' = cor k * cor ((cmod k')⇧2) * quad_form z H"
by (simp add: quad_form_scale_v quad_form_scale_m del: vec_cnj_sv quad_form_def)
hence "Re (quad_form z' H') = k * (cmod k')⇧2 * Re (quad_form z H)"
using hh quad_form_hermitean_real[of H]
by (simp add: power2_eq_square)
thus "in_ocircline_cmat_cvec H z = in_ocircline_cmat_cvec H' z'"
using ‹k > 0› ‹k' ≠ 0›
using mult_less_0_iff
by fastforce
qed
definition disc :: "ocircline ⇒ complex_homo set" where
"disc H = {z. in_ocircline H z}"
lemma disc_I [simp]:
assumes "in_ocircline H z"
shows "z ∈ disc H"
using assms
unfolding disc_def
by simp
definition out_ocircline_cmat_cvec :: "complex_mat ⇒ complex_vec ⇒ bool" where
[simp]: "out_ocircline_cmat_cvec H z ⟷ Re (quad_form z H) > 0"
lift_definition out_ocircline_clmat_hcoords :: "circline_mat ⇒ complex_homo_coords ⇒ bool" is out_ocircline_cmat_cvec
done
lift_definition out_ocircline :: "ocircline ⇒ complex_homo ⇒ bool" is out_ocircline_clmat_hcoords
proof transfer
fix H H' z z'
assume hh: "hermitean H ∧ H ≠ mat_zero" "hermitean H' ∧ H' ≠ mat_zero"
"z ≠ vec_zero" "z' ≠ vec_zero"
assume "ocircline_eq_cmat H H'" "z ≈⇩v z'"
then obtain k k' where
*: "0 < k" "H' = cor k *⇩s⇩m H" "k' ≠ 0" "z' = k' *⇩s⇩v z"
by auto
hence "quad_form z' H' = cor k * cor ((cmod k')⇧2) * quad_form z H"
by (simp add: quad_form_scale_v quad_form_scale_m del: vec_cnj_sv quad_form_def)
hence "Re (quad_form z' H') = k * (cmod k')⇧2 * Re (quad_form z H)"
using hh quad_form_hermitean_real[of H]
by (simp add: power2_eq_square)
thus "out_ocircline_cmat_cvec H z = out_ocircline_cmat_cvec H' z'"
using ‹k > 0› ‹k' ≠ 0›
using zero_less_mult_pos
by fastforce
qed
definition disc_compl :: "ocircline ⇒ complex_homo set" where
"disc_compl H = {z. out_ocircline H z}"
text ‹These three sets are mutually disjoint and they fill up the entire plane.›
lemma disc_compl_I [simp]:
assumes "out_ocircline H z"
shows "z ∈ disc_compl H"
using assms
unfolding disc_compl_def
by simp
lemma in_on_out:
shows "in_ocircline H z ∨ on_ocircline H z ∨ out_ocircline H z"
apply (transfer, transfer)
using quad_form_hermitean_real
using complex_eq_if_Re_eq
by auto
lemma in_on_out_univ:
shows "disc H ∪ disc_compl H ∪ ocircline_set H = UNIV"
unfolding disc_def disc_compl_def ocircline_set_def
using in_on_out[of H]
by auto
lemma disc_inter_disc_compl [simp]:
shows "disc H ∩ disc_compl H = {}"
unfolding disc_def disc_compl_def
by auto (transfer, transfer, simp)
lemma disc_inter_ocircline_set [simp]:
shows "disc H ∩ ocircline_set H = {}"
unfolding disc_def ocircline_set_def
by auto (transfer, transfer, simp)
lemma disc_compl_inter_ocircline_set [simp]:
shows "disc_compl H ∩ ocircline_set H = {}"
unfolding disc_compl_def ocircline_set_def
by auto (transfer, transfer, simp)
subsection ‹Opposite orientation›
text ‹Finding opposite circline is idempotent, and opposite circlines share the same set of points,
but exchange disc and its complement.›
definition opposite_ocircline_cmat :: "complex_mat ⇒ complex_mat" where
[simp]: "opposite_ocircline_cmat H = (-1) *⇩s⇩m H"
lift_definition opposite_ocircline_clmat :: "circline_mat ⇒ circline_mat" is opposite_ocircline_cmat
by (auto simp add: hermitean_def mat_adj_def mat_cnj_def)
lift_definition opposite_ocircline :: "ocircline ⇒ ocircline" is opposite_ocircline_clmat
by transfer auto
lemma opposite_ocircline_involution [simp]:
shows "opposite_ocircline (opposite_ocircline H) = H"
by (transfer, transfer) (auto, rule_tac x="1" in exI, simp)
lemma on_circline_opposite_ocircline_cmat [simp]:
assumes "hermitean H ∧ H ≠ mat_zero" and "z ≠ vec_zero"
shows "on_circline_cmat_cvec (opposite_ocircline_cmat H) z = on_circline_cmat_cvec H z"
using assms
by (simp add: quad_form_scale_m del: quad_form_def)
lemma on_circline_opposite_ocircline [simp]:
shows "on_ocircline (opposite_ocircline H) z ⟷ on_ocircline H z"
using on_circline_opposite_ocircline_cmat
by (transfer, transfer, simp)
lemma ocircline_set_opposite_ocircline [simp]:
shows "ocircline_set (opposite_ocircline H) = ocircline_set H"
unfolding ocircline_set_def
by auto
lemma disc_compl_opposite_ocircline [simp]:
shows "disc_compl (opposite_ocircline H) = disc H"
unfolding disc_def disc_compl_def
apply auto
apply (transfer, transfer)
apply (auto simp add: quad_form_scale_m simp del: quad_form_def)
apply (transfer ,transfer)
apply (auto simp add: quad_form_scale_m simp del: quad_form_def)
done
lemma disc_opposite_ocircline [simp]:
shows "disc (opposite_ocircline H) = disc_compl H"
using disc_compl_opposite_ocircline[of "opposite_ocircline H"]
by simp
subsection ‹Positive orientation. Conversion between unoriented and oriented circlines›
text ‹Given an oriented circline, one can trivially obtain its unoriented counterpart, and these two
share the same set of points.›
lift_definition of_ocircline :: "ocircline ⇒ circline" is "id::circline_mat ⇒ circline_mat"
by transfer (simp, erule exE, force)
lemma of_ocircline_opposite_ocircline [simp]:
shows "of_ocircline (opposite_ocircline H) = of_ocircline H"
by (transfer, transfer) (simp, erule exE, rule_tac x="-1" in exI, simp)
lemma on_ocircline_of_circline [simp]:
shows "on_circline (of_ocircline H) z ⟷ on_ocircline H z"
by (transfer, transfer, simp)
lemma circline_set_of_ocircline [simp]:
shows "circline_set (of_ocircline H) = ocircline_set H"
unfolding ocircline_set_def circline_set_def
by (safe) (transfer, simp)+
lemma inj_of_ocircline:
assumes "of_ocircline H = of_ocircline H'"
shows "H = H' ∨ H = opposite_ocircline H'"
using assms
by (transfer, transfer) (simp, metis linorder_neqE_linordered_idom minus_of_real_eq_of_real_iff mult_minus1 mult_sm_distribution neg_0_equal_iff_equal neg_less_0_iff_less)
lemma inj_ocircline_set:
assumes "ocircline_set H = ocircline_set H'" and "ocircline_set H ≠ {}"
shows "H = H' ∨ H = opposite_ocircline H'"
proof-
from assms
have "circline_set (of_ocircline H) = circline_set (of_ocircline H')"
"circline_set (of_ocircline H') ≠ {}"
by auto
hence "of_ocircline H = of_ocircline H'"
by (simp add: inj_circline_set)
thus ?thesis
by (rule inj_of_ocircline)
qed
text ‹Positive orientation.›
text ‹Given a representative Hermitean matrix of a circline, it represents exactly one of the two
possible oriented circlines. The choice of what should be called a positive orientation is
arbitrary. We follow Schwerdtfeger \<^cite>‹"schwerdtfeger"›, use the leading coefficient $A$ as the
first criterion, and say that circline matrices with $A > 0$ are called positively oriented, and
with $A < 0$ negatively oriented. However, Schwerdtfeger did not discuss the possible case of $A =
0$ (the case of lines), so we had to extend his definition to achieve a total characterization.›
definition pos_oriented_cmat :: "complex_mat ⇒ bool" where
[simp]: "pos_oriented_cmat H ⟷
(let (A, B, C, D) = H
in (Re A > 0 ∨ (Re A = 0 ∧ ((B ≠ 0 ∧ Arg B > 0) ∨ (B = 0 ∧ Re D > 0)))))"
lift_definition pos_oriented_clmat :: "circline_mat ⇒ bool" is pos_oriented_cmat
done
lift_definition pos_oriented :: "ocircline ⇒ bool" is pos_oriented_clmat
by transfer
(case_tac circline_mat1, case_tac circline_mat2, simp, erule exE, simp,
metis mult_pos_pos zero_less_mult_pos)
lemma pos_oriented:
shows "pos_oriented H ∨ pos_oriented (opposite_ocircline H)"
proof (transfer, transfer)
fix H
assume hh: "hermitean H ∧ H ≠ mat_zero"
obtain A B C D where HH: "H = (A, B, C, D)"
by (cases H) auto
moreover
hence "Re A = 0 ∧ Re D = 0 ⟶ B ≠ 0"
using hh hermitean_elems[of A B C D]
by (cases A, cases D) (auto simp add: Complex_eq)
moreover
have "B ≠ 0 ∧ ¬ 0 < Arg B ⟶ 0 < Arg (- B)"
using canon_ang_plus_pi2[of "Arg B"] Arg_bounded[of B]
by (auto simp add: arg_uminus)
ultimately
show "pos_oriented_cmat H ∨ pos_oriented_cmat (opposite_ocircline_cmat H)"
by auto
qed
lemma pos_oriented_opposite_ocircline_cmat [simp]:
assumes "hermitean H ∧ H ≠ mat_zero"
shows "pos_oriented_cmat (opposite_ocircline_cmat H) ⟷ ¬ pos_oriented_cmat H"
proof-
obtain A B C D where HH: "H = (A, B, C, D)"
by (cases H) auto
moreover
hence "Re A = 0 ∧ Re D = 0 ⟶ B ≠ 0"
using assms hermitean_elems[of A B C D]
by (cases A, cases D) (auto simp add: Complex_eq)
moreover
have "B ≠ 0 ∧ ¬ 0 < Arg B ⟶ 0 < Arg (- B)"
using canon_ang_plus_pi2[of "Arg B"] Arg_bounded[of B]
by (auto simp add: arg_uminus)
moreover
have "B ≠ 0 ∧ 0 < Arg B ⟶ ¬ 0 < Arg (- B)"
using canon_ang_plus_pi1[of "Arg B"] Arg_bounded[of B]
by (auto simp add: arg_uminus)
ultimately
show "pos_oriented_cmat (opposite_ocircline_cmat H) = (¬ pos_oriented_cmat H)"
by simp (metis not_less_iff_gr_or_eq)
qed
lemma pos_oriented_opposite_ocircline [simp]:
shows "pos_oriented (opposite_ocircline H) ⟷ ¬ pos_oriented H"
using pos_oriented_opposite_ocircline_cmat
by (transfer, transfer, simp)
lemma pos_oriented_circle_inf:
assumes "∞⇩h ∉ ocircline_set H"
shows "pos_oriented H ⟷ ∞⇩h ∉ disc H"
using assms
unfolding ocircline_set_def disc_def
apply simp
proof (transfer, transfer)
fix H
assume hh: "hermitean H ∧ H ≠ mat_zero"
obtain A B C D where HH: "H = (A, B, C, D)"
by (cases H) auto
hence "is_real A"
using hh hermitean_elems
by auto
assume "¬ on_circline_cmat_cvec H ∞⇩v"
thus "pos_oriented_cmat H = (¬ in_ocircline_cmat_cvec H ∞⇩v)"
using HH ‹is_real A›
by (cases A) (auto simp add: vec_cnj_def Complex_eq)
qed
lemma pos_oriented_euclidean_circle:
assumes "is_circle (of_ocircline H)"
"(a, r) = euclidean_circle (of_ocircline H)"
"circline_type (of_ocircline H) < 0"
shows "pos_oriented H ⟷ of_complex a ∈ disc H"
using assms
unfolding disc_def
apply simp
proof (transfer, transfer)
fix H a r
assume hh: "hermitean H ∧ H ≠ mat_zero"
obtain A B C D where HH: "H = (A, B, C, D)"
by (cases H) auto
hence "is_real A" "is_real D" "C = cnj B"
using hh hermitean_elems
by auto
assume *: "¬ circline_A0_cmat (id H)" "(a, r) = euclidean_circle_cmat (id H)" "circline_type_cmat (id H) < 0"
hence "A ≠ 0" "Re A ≠ 0"
using HH ‹is_real A›
by (case_tac[!] A) (auto simp add: Complex_eq)
have "Re (A*D - B*C) < 0"
using ‹circline_type_cmat (id H) < 0› HH
by simp
have **: "(A * (D * cnj A) - B * (C * cnj A)) / (A * cnj A) = (A*D - B*C) / A"
using ‹A ≠ 0›
by (simp add: field_simps)
hence ***: "0 < Re A ⟷ Re ((A * (D * cnj A) - B * (C * cnj A)) / (A * cnj A)) < 0"
using ‹is_real A› ‹A ≠ 0› ‹Re (A*D - B*C) < 0›
by (simp add: Re_divide_real divide_less_0_iff)
have "Re D - Re (cnj B * B / cnj A) < Re ((C - cnj B * A / cnj A) * B / A)" if "Re A > 0"
using HH * ‹is_real A› that
by simp (smt "**" "***" cnj.simps(1) cnj.simps(2) complex_eq diff_divide_distrib left_diff_distrib'
minus_complex.simps(1) mult.commute nonzero_mult_div_cancel_right)?
moreover have "Re A > 0" if "Re D - Re (cnj B * B / cnj A) < Re ((C - cnj B * A / cnj A) * B / A)"
using HH * ‹is_real A› that
by simp (smt "**" "***" cnj.simps(1) cnj.simps(2) complex_eq diff_divide_distrib left_diff_distrib'
minus_complex.simps(1) mult.commute nonzero_mult_div_cancel_right)?
ultimately show "pos_oriented_cmat H = in_ocircline_cmat_cvec H (of_complex_cvec a)"
using HH ‹Re A ≠ 0› * ‹is_real A› by (auto simp add: vec_cnj_def)
qed
text ‹Introduce positive orientation›
definition of_circline_cmat :: "complex_mat ⇒ complex_mat" where
[simp]: "of_circline_cmat H = (if pos_oriented_cmat H then H else opposite_ocircline_cmat H)"
lift_definition of_circline_clmat :: "circline_mat ⇒ circline_mat" is of_circline_cmat
by (auto simp add: hermitean_def mat_adj_def mat_cnj_def)
lemma of_circline_clmat_def':
shows "of_circline_clmat H = (if pos_oriented_clmat H then H else opposite_ocircline_clmat H)"
by transfer simp
lemma pos_oriented_cmat_mult_positive':
assumes
"hermitean H1 ∧ H1 ≠ mat_zero" and
"hermitean H2 ∧ H2 ≠ mat_zero" and
"∃k. k > 0 ∧ H2 = cor k *⇩s⇩m H1" and
"pos_oriented_cmat H1"
shows "pos_oriented_cmat H2"
proof-
obtain A1 B1 C1 D1 A2 B2 C2 D2
where HH: "H1 = (A1, B1, C1, D1)" "H2 = (A2, B2, C2, D2)"
by (cases H1, cases H2)
thus ?thesis
using assms
by fastforce
qed
lemma pos_oriented_cmat_mult_positive:
assumes
"hermitean H1 ∧ H1 ≠ mat_zero" and
"hermitean H2 ∧ H2 ≠ mat_zero" and
"∃k. k > 0 ∧ H2 = cor k *⇩s⇩m H1"
shows
"pos_oriented_cmat H1 ⟷ pos_oriented_cmat H2"
proof-
from assms(3) obtain k where "k > 0 ∧ H2 = cor k *⇩s⇩m H1"
by auto
hence "∃k. k > 0 ∧ H1 = cor k *⇩s⇩m H2"
by (rule_tac x="1/k" in exI, auto)
thus ?thesis
using assms pos_oriented_cmat_mult_positive'
by blast
qed
lemma pos_oriented_cmat_mult_negative:
assumes
"hermitean H1 ∧ H1 ≠ mat_zero" and
"hermitean H2 ∧ H2 ≠ mat_zero" and
"∃k. k < 0 ∧ H2 = cor k *⇩s⇩m H1"
shows
"pos_oriented_cmat H1 ⟷ ¬ pos_oriented_cmat H2"
using assms
proof-
obtain A B C D A1 B1 C1 D1
where *: "H1 = (A, B, C, D)" "H2 = (A1, B1, C1, D1)"
by (cases H1, cases H2) auto
hence **: "is_real A" "is_real D" "is_real A1" "is_real D1" "B = 0 ⟷ C = 0" "B1 = 0 ⟷ C1 = 0"
using assms hermitean_elems[of A B C D] hermitean_elems[of A1 B1 C1 D1]
by auto
show ?thesis
proof (rule iffI)
assume H1: "pos_oriented_cmat H1"
show "¬ pos_oriented_cmat H2"
proof (cases "Re A > 0")
case True
thus ?thesis
using assms * ** mult_neg_pos
by fastforce
next
case False
show ?thesis
proof (cases "B = 0")
case True
thus ?thesis
using assms * ** H1 ‹¬ Re A > 0› mult_neg_pos
by fastforce
next
case False
thus ?thesis
using arg_uminus_opposite_sign[of B] arg_mult_real_negative
using assms * ** H1 ‹¬ Re A > 0› mult_neg_pos
by fastforce
qed
qed
next
assume H2: "¬ pos_oriented_cmat H2"
show "pos_oriented_cmat H1"
proof (cases "Re A > 0")
case True
thus ?thesis
using * ** mult_neg_pos
by fastforce
next
case False
show ?thesis
proof (cases "B = 0")
case True
thus ?thesis
using assms * ** H2 ‹¬ Re A > 0›
by simp (smt arg_0_iff arg_complex_of_real_negative arg_complex_of_real_positive arg_mult_eq complex_of_real_Re mult.right_neutral mult_eq_0_iff of_real_0 of_real_1 zero_complex.simps(1))
next
case False
thus ?thesis
using assms ‹¬ Re A > 0› H2 * **
using arg_uminus_opposite_sign[of B]
by (cases "Re A = 0", auto simp add: mult_neg_neg)
qed
qed
qed
qed
lift_definition of_circline :: "circline ⇒ ocircline" is of_circline_clmat
proof transfer
fix H1 H2
assume hh:
"hermitean H1 ∧ H1 ≠ mat_zero"
"hermitean H2 ∧ H2 ≠ mat_zero"
assume "circline_eq_cmat H1 H2"
then obtain k where *: "k ≠ 0 ∧ H2 = cor k *⇩s⇩m H1"
by auto
show "ocircline_eq_cmat (of_circline_cmat H1) (of_circline_cmat H2)"
proof (cases "k > 0")
case True
hence "pos_oriented_cmat H1 = pos_oriented_cmat H2"
using * pos_oriented_cmat_mult_positive[OF hh]
by blast
thus ?thesis
using hh * ‹k > 0›
apply (simp del: pos_oriented_cmat_def)
apply (rule conjI)
apply (rule impI)
apply (simp, rule_tac x=k in exI, simp)
apply (rule impI)
apply (simp, rule_tac x=k in exI, simp)
done
next
case False
hence "k < 0"
using *
by simp
hence "pos_oriented_cmat H1 ⟷ ¬ (pos_oriented_cmat H2)"
using * pos_oriented_cmat_mult_negative[OF hh]
by blast
thus ?thesis
using hh * ‹k < 0›
apply (simp del: pos_oriented_cmat_def)
apply (rule conjI)
apply (rule impI)
apply (simp, rule_tac x="-k" in exI, simp)
apply (rule impI)
apply (simp, rule_tac x="-k" in exI, simp)
done
qed
qed
lemma pos_oriented_of_circline [simp]:
shows "pos_oriented (of_circline H)"
using pos_oriented_opposite_ocircline_cmat
by (transfer, transfer, simp)
lemma of_ocircline_of_circline [simp]:
shows "of_ocircline (of_circline H) = H"
apply (transfer, auto simp add: of_circline_clmat_def')
apply (transfer, simp, rule_tac x="-1" in exI, simp)
done
lemma of_circline_of_ocircline_pos_oriented [simp]:
assumes "pos_oriented H"
shows "of_circline (of_ocircline H) = H"
using assms
by (transfer, transfer, simp, rule_tac x=1 in exI, simp)
lemma inj_of_circline:
assumes "of_circline H = of_circline H'"
shows "H = H'"
using assms
proof (transfer, transfer)
fix H H'
assume "ocircline_eq_cmat (of_circline_cmat H) (of_circline_cmat H')"
then obtain k where "k > 0" "of_circline_cmat H' = cor k *⇩s⇩m of_circline_cmat H"
by auto
thus "circline_eq_cmat H H'"
using mult_sm_inv_l[of "-1" "H'" "cor k *⇩s⇩m H"]
using mult_sm_inv_l[of "-1" "H'" "(- (cor k)) *⇩s⇩m H"]
apply (simp split: if_split_asm)
apply (rule_tac x="k" in exI, simp)
apply (rule_tac x="-k" in exI, simp)
apply (rule_tac x="-k" in exI, simp)
apply (rule_tac x="k" in exI, simp)
done
qed
lemma of_circline_of_ocircline:
shows "of_circline (of_ocircline H') = H' ∨
of_circline (of_ocircline H') = opposite_ocircline H'"
proof (cases "pos_oriented H'")
case True
thus ?thesis
by auto
next
case False
hence "pos_oriented (opposite_ocircline H')"
using pos_oriented
by auto
thus ?thesis
using of_ocircline_opposite_ocircline[of H']
using of_circline_of_ocircline_pos_oriented [of "opposite_ocircline H'"]
by auto
qed
subsubsection ‹Set of points on oriented and unoriented circlines›
lemma ocircline_set_of_circline [simp]:
shows "ocircline_set (of_circline H) = circline_set H"
unfolding ocircline_set_def circline_set_def
proof (safe)
fix z
assume "on_ocircline (of_circline H) z"
thus "on_circline H z"
by (transfer, transfer, simp del: on_circline_cmat_cvec_def opposite_ocircline_cmat_def split: if_split_asm)
next
fix z
assume "on_circline H z"
thus "on_ocircline (of_circline H) z"
by (transfer, transfer, simp del: on_circline_cmat_cvec_def opposite_ocircline_cmat_def split: if_split_asm)
qed
subsection ‹Some special oriented circlines and discs›
lift_definition mk_ocircline :: "complex ⇒ complex ⇒ complex ⇒ complex ⇒ ocircline" is mk_circline_clmat
done
text ‹oriented unit circle and unit disc›
lift_definition ounit_circle :: "ocircline" is unit_circle_clmat
done
lemma pos_oriented_ounit_circle [simp]:
shows "pos_oriented ounit_circle"
by (transfer, transfer, simp)
lemma of_ocircline_ounit_circle [simp]:
shows "of_ocircline ounit_circle = unit_circle"
by (transfer, transfer, simp)
lemma of_circline_unit_circle [simp]:
shows "of_circline (unit_circle) = ounit_circle"
by (transfer, transfer, simp)
lemma ocircline_set_ounit_circle [simp]:
shows "ocircline_set ounit_circle = circline_set unit_circle"
apply (subst of_circline_unit_circle[symmetric])
apply (subst ocircline_set_of_circline)
apply simp
done
definition unit_disc :: "complex_homo set" where
"unit_disc = disc ounit_circle"
definition unit_disc_compl :: "complex_homo set" where
"unit_disc_compl = disc_compl ounit_circle"
definition unit_circle_set :: "complex_homo set" where
"unit_circle_set = circline_set unit_circle"
lemma zero_in_unit_disc [simp]:
shows "0⇩h ∈ unit_disc"
unfolding unit_disc_def disc_def
by (simp, transfer, transfer) (simp add: Let_def vec_cnj_def)
lemma one_notin_unit_dic [simp]:
shows "1⇩h ∉ unit_disc"
unfolding unit_disc_def disc_def
by (simp, transfer, transfer) (simp add: Let_def vec_cnj_def)
lemma inf_notin_unit_disc [simp]:
shows "∞⇩h ∉ unit_disc"
unfolding unit_disc_def disc_def
by (simp, transfer, transfer) (simp add: Let_def vec_cnj_def)
lemma unit_disc_iff_cmod_lt_1 [simp]:
shows "of_complex c ∈ unit_disc ⟷ cmod c < 1"
unfolding unit_disc_def disc_def
by (simp, transfer, transfer, simp add: vec_cnj_def cmod_def power2_eq_square)
lemma unit_disc_cmod_square_lt_1 [simp]:
assumes "z ∈ unit_disc"
shows "(cmod (to_complex z))⇧2 < 1"
using assms inf_or_of_complex[of z]
by (auto simp add: abs_square_less_1)
lemma unit_disc_to_complex_inj:
assumes "u ∈ unit_disc" and "v ∈ unit_disc"
assumes "to_complex u = to_complex v"
shows "u = v"
using assms
using inf_or_of_complex[of u] inf_or_of_complex[of v]
by auto
lemma inversion_unit_disc [simp]:
shows "inversion ` unit_disc = unit_disc_compl"
unfolding unit_disc_def unit_disc_compl_def disc_def disc_compl_def
proof safe
fix x
assume "in_ocircline ounit_circle x"
thus "out_ocircline ounit_circle (inversion x)"
unfolding inversion_def
by (transfer, transfer, auto simp add: vec_cnj_def)
next
fix x
assume *: "out_ocircline ounit_circle x"
show "x ∈ inversion ` Collect (in_ocircline ounit_circle)"
proof (rule image_eqI)
show "x = inversion (inversion x)"
by auto
next
show "inversion x ∈ Collect (in_ocircline ounit_circle)"
using *
unfolding inversion_def
by (simp, transfer, transfer, auto simp add: vec_cnj_def)
qed
qed
lemma inversion_unit_disc_compl [simp]:
shows "inversion ` unit_disc_compl = unit_disc"
proof-
have "inversion ` (inversion ` unit_disc) = unit_disc"
by (auto simp del: inversion_unit_disc simp add: image_iff)
thus ?thesis
by simp
qed
lemma inversion_noteq_unit_disc:
assumes "u ∈ unit_disc" and "v ∈ unit_disc"
shows "inversion u ≠ v"
proof-
from assms
have "inversion u ∈ unit_disc_compl"
by (metis image_eqI inversion_unit_disc)
thus ?thesis
using assms
unfolding unit_disc_def unit_disc_compl_def
using disc_inter_disc_compl
by fastforce
qed
lemma in_ocircline_ounit_circle_conjugate [simp]:
assumes "in_ocircline ounit_circle z"
shows "in_ocircline ounit_circle (conjugate z)"
using assms
by (transfer, transfer, auto simp add: vec_cnj_def)
lemma conjugate_unit_disc [simp]:
shows "conjugate ` unit_disc = unit_disc"
unfolding unit_disc_def disc_def
apply (auto simp add: image_iff)
apply (rule_tac x="conjugate x" in exI, simp)
done
lemma conjugate_in_unit_disc [simp]:
assumes "z ∈ unit_disc"
shows "conjugate z ∈ unit_disc"
using conjugate_unit_disc
using assms
by blast
lemma out_ocircline_ounit_circle_conjugate [simp]:
assumes "out_ocircline ounit_circle z"
shows "out_ocircline ounit_circle (conjugate z)"
using assms
by (transfer, transfer, auto simp add: vec_cnj_def)
lemma conjugate_unit_disc_compl [simp]:
shows "conjugate ` unit_disc_compl = unit_disc_compl"
unfolding unit_disc_compl_def disc_compl_def
apply (auto simp add: image_iff)
apply (rule_tac x="conjugate x" in exI, simp)
done
lemma conjugate_in_unit_disc_compl [simp]:
assumes "z ∈ unit_disc_compl"
shows "conjugate z ∈ unit_disc_compl"
using conjugate_unit_disc_compl
using assms
by blast
subsubsection ‹Oriented x axis and lower half plane›
lift_definition o_x_axis :: "ocircline" is x_axis_clmat
done
lemma o_x_axis_pos_oriented [simp]:
shows "pos_oriented o_x_axis"
by (transfer, transfer, simp)
lemma of_ocircline_o_x_axis [simp]:
shows "of_ocircline o_x_axis = x_axis"
by (transfer, transfer, simp)
lemma of_circline_x_axis [simp]:
shows "of_circline x_axis = o_x_axis"
using of_circline_of_ocircline_pos_oriented[of o_x_axis]
using o_x_axis_pos_oriented
by simp
lemma ocircline_set_circline_set_x_axis [simp]:
shows "ocircline_set o_x_axis = circline_set x_axis"
by (subst of_circline_x_axis[symmetric], subst ocircline_set_of_circline, simp)
lemma ii_in_disc_o_x_axis [simp]:
shows "ii⇩h ∉ disc o_x_axis"
unfolding disc_def
by simp (transfer, transfer, simp add: Let_def vec_cnj_def)
lemma ii_notin_disc_o_x_axis [simp]:
shows "ii⇩h ∈ disc_compl o_x_axis"
unfolding disc_compl_def
by simp (transfer, transfer, simp add: Let_def vec_cnj_def)
lemma of_complex_in_o_x_axis_disc [simp]:
shows "of_complex z ∈ disc o_x_axis ⟷ Im z < 0"
unfolding disc_def
by auto (transfer, transfer, simp add: vec_cnj_def)+
lemma inf_notin_disc_o_x_axis [simp]:
shows "∞⇩h ∉ disc o_x_axis"
unfolding disc_def
by simp (transfer, transfer, simp add: vec_cnj_def)
lemma disc_o_x_axis:
shows "disc o_x_axis = of_complex ` {z. Im z < 0}"
proof-
{
fix z
assume "z ∈ disc o_x_axis"
hence "∃ x. Im x < 0 ∧ z = of_complex x"
using inf_or_of_complex[of z]
by auto
}
thus ?thesis
by (auto simp add: image_iff)
qed
subsubsection ‹Oriented single point circline›
lift_definition o_circline_point_0 :: "ocircline" is circline_point_0_clmat
done
lemma of_ocircline_o_circline_point_0 [simp]:
shows "of_ocircline o_circline_point_0 = circline_point_0"
by (transfer, transfer, simp)
subsection ‹Möbius action on oriented circlines and discs›
text ‹Möbius action on an oriented circline is the same as on to an unoriented circline.›
lift_definition moebius_ocircline :: "moebius ⇒ ocircline ⇒ ocircline" is moebius_circline_mmat_clmat
apply (transfer, transfer)
apply simp
apply ((erule exE)+, (erule conjE)+)
apply (simp add: mat_inv_mult_sm)
apply (rule_tac x="ka / Re (k * cnj k)" in exI, auto simp add: complex_mult_cnj_cmod power2_eq_square)
done
text ‹Möbius action on (unoriented) circlines could have been defined using the action on oriented
circlines, but not the other way around.›
lemma moebius_circline_ocircline:
shows "moebius_circline M H = of_ocircline (moebius_ocircline M (of_circline H))"
apply (transfer, simp add: of_circline_clmat_def', safe)
apply (transfer, simp, rule_tac x="-1" in exI, simp)
done
lemma moebius_ocircline_circline:
shows "moebius_ocircline M H = of_circline (moebius_circline M (of_ocircline H)) ∨
moebius_ocircline M H = opposite_ocircline (of_circline (moebius_circline M (of_ocircline H)))"
apply (transfer, simp add: of_circline_clmat_def', safe)
apply (transfer, simp, rule_tac x="1" in exI, simp)
apply (transfer, simp, erule_tac x="1" in allE, simp)
done
text ‹Möbius action on oriented circlines have many nice properties as it was the case with
Möbius action on (unoriented) circlines. These transformations are injective and form group under
composition.›
lemma inj_moebius_ocircline [simp]:
shows "inj (moebius_ocircline M)"
unfolding inj_on_def
proof (safe)
fix H H'
assume "moebius_ocircline M H = moebius_ocircline M H'"
thus "H = H'"
proof (transfer, transfer)
fix M H H' :: complex_mat
assume "mat_det M ≠ 0"
let ?iM = "mat_inv M"
assume "ocircline_eq_cmat (moebius_circline_cmat_cmat M H) (moebius_circline_cmat_cmat M H')"
then obtain k where "congruence ?iM H' = congruence ?iM (cor k *⇩s⇩m H)" "k > 0"
by (auto simp del: congruence_def)
thus "ocircline_eq_cmat H H'"
using ‹mat_det M ≠ 0› inj_congruence[of ?iM H' "cor k *⇩s⇩m H"] mat_det_inv[of M]
by auto
qed
qed
lemma moebius_ocircline_id_moebius [simp]:
shows "moebius_ocircline id_moebius H = H"
by (transfer, transfer) (force simp add: mat_adj_def mat_cnj_def)
lemma moebius_ocircline_comp [simp]:
shows "moebius_ocircline (moebius_comp M1 M2) H = moebius_ocircline M1 (moebius_ocircline M2 H)"
by (transfer, transfer, simp, rule_tac x=1 in exI, simp add: mat_inv_mult_mm mult_mm_assoc)
lemma moebius_ocircline_comp_inv_left [simp]:
shows "moebius_ocircline (moebius_inv M) (moebius_ocircline M H) = H"
by (subst moebius_ocircline_comp[symmetric]) simp
lemma moebius_ocircline_comp_inv_right [simp]:
shows "moebius_ocircline M (moebius_ocircline (moebius_inv M) H) = H"
by (subst moebius_ocircline_comp[symmetric]) simp
lemma moebius_ocircline_opposite_ocircline [simp]:
shows "moebius_ocircline M (opposite_ocircline H) = opposite_ocircline (moebius_ocircline M H)"
by (transfer, transfer, simp, rule_tac x=1 in exI, simp)
text ‹Möbius action on oriented circlines preserve the set of points of the circline.›
lemma ocircline_set_moebius_ocircline [simp]:
shows "ocircline_set (moebius_ocircline M H) = moebius_pt M ` ocircline_set H" (is "?lhs = ?rhs")
proof-
have "?rhs = circline_set (moebius_circline M (of_ocircline H))"
by simp
thus ?thesis
using moebius_ocircline_circline[of M H]
by auto
qed
lemma ocircline_set_fix_iff_ocircline_fix:
assumes "ocircline_set H' ≠ {}"
shows "ocircline_set (moebius_ocircline M H) = ocircline_set H' ⟷
moebius_ocircline M H = H' ∨ moebius_ocircline M H = opposite_ocircline H'"
using assms
using inj_ocircline_set[of "moebius_ocircline M H" H']
by (auto simp del: ocircline_set_moebius_ocircline)
lemma disc_moebius_ocircline [simp]:
shows "disc (moebius_ocircline M H) = moebius_pt M ` (disc H)"
proof (safe)
fix z
assume "z ∈ disc H"
thus "moebius_pt M z ∈ disc (moebius_ocircline M H)"
unfolding disc_def
proof (safe)
assume "in_ocircline H z"
thus "in_ocircline (moebius_ocircline M H) (moebius_pt M z)"
proof (transfer, transfer)
fix H M :: complex_mat and z :: complex_vec
assume "mat_det M ≠ 0"
assume "in_ocircline_cmat_cvec H z"
thus "in_ocircline_cmat_cvec (moebius_circline_cmat_cmat M H) (moebius_pt_cmat_cvec M z)"
using ‹mat_det M ≠ 0› quad_form_congruence[of M z]
by simp
qed
qed
next
fix z
assume "z ∈ disc (moebius_ocircline M H)"
thus "z ∈ moebius_pt M ` disc H"
unfolding disc_def
proof(safe)
assume "in_ocircline (moebius_ocircline M H) z"
show "z ∈ moebius_pt M ` Collect (in_ocircline H)"
proof
show "z = moebius_pt M (moebius_pt (moebius_inv M) z)"
by simp
next
show "moebius_pt (moebius_inv M) z ∈ Collect (in_ocircline H)"
using ‹in_ocircline (moebius_ocircline M H) z›
proof (safe, transfer, transfer)
fix M H :: complex_mat and z :: complex_vec
assume "mat_det M ≠ 0"
hence "congruence (mat_inv (mat_inv M)) (congruence (mat_inv M) H) = H"
by (simp del: congruence_def)
hence "quad_form z (congruence (mat_inv M) H) = quad_form (mat_inv M *⇩m⇩v z) H"
using quad_form_congruence[of "mat_inv M" "z" "congruence (mat_inv M) H"]
using ‹mat_det M ≠ 0› mat_det_inv[of "M"]
by simp
moreover
assume "in_ocircline_cmat_cvec (moebius_circline_cmat_cmat M H) z"
ultimately
show "in_ocircline_cmat_cvec H (moebius_pt_cmat_cvec (moebius_inv_cmat M) z)"
by simp
qed
qed
qed
qed
lemma disc_compl_moebius_ocircline [simp]:
shows "disc_compl (moebius_ocircline M H) = moebius_pt M ` (disc_compl H)"
proof (safe)
fix z
assume "z ∈ disc_compl H"
thus "moebius_pt M z ∈ disc_compl (moebius_ocircline M H)"
unfolding disc_compl_def
proof (safe)
assume "out_ocircline H z"
thus "out_ocircline (moebius_ocircline M H) (moebius_pt M z)"
proof (transfer, transfer)
fix H M :: complex_mat and z :: complex_vec
assume "mat_det M ≠ 0"
assume "out_ocircline_cmat_cvec H z"
thus "out_ocircline_cmat_cvec (moebius_circline_cmat_cmat M H) (moebius_pt_cmat_cvec M z)"
using ‹mat_det M ≠ 0› quad_form_congruence[of M z]
by simp
qed
qed
next
fix z
assume "z ∈ disc_compl (moebius_ocircline M H)"
thus "z ∈ moebius_pt M ` disc_compl H"
unfolding disc_compl_def
proof(safe)
assume "out_ocircline (moebius_ocircline M H) z"
show "z ∈ moebius_pt M ` Collect (out_ocircline H)"
proof
show "z = moebius_pt M (moebius_pt (moebius_inv M) z)"
by simp
next
show "moebius_pt (moebius_inv M) z ∈ Collect (out_ocircline H)"
using ‹out_ocircline (moebius_ocircline M H) z›
proof (safe, transfer, transfer)
fix M H :: complex_mat and z :: complex_vec
assume "mat_det M ≠ 0"
hence "congruence (mat_inv (mat_inv M)) (congruence (mat_inv M) H) = H"
by (simp del: congruence_def)
hence "quad_form z (congruence (mat_inv M) H) = quad_form (mat_inv M *⇩m⇩v z) H"
using quad_form_congruence[of "mat_inv M" "z" "congruence (mat_inv M) H"]
using ‹mat_det M ≠ 0› mat_det_inv[of "M"]
by simp
moreover
assume "out_ocircline_cmat_cvec (moebius_circline_cmat_cmat M H) z"
ultimately
show "out_ocircline_cmat_cvec H (moebius_pt_cmat_cvec (moebius_inv_cmat M) z)"
by simp
qed
qed
qed
qed
subsection ‹Orientation after Möbius transformations›
text ‹All Euclidean similarities preserve circline orientation.›
lemma moebius_similarity_oriented_lines_to_oriented_lines:
assumes "a ≠ 0"
shows "∞⇩h ∈ ocircline_set H ⟷ ∞⇩h ∈ ocircline_set (moebius_ocircline (moebius_similarity a b) H)"
using moebius_similarity_lines_to_lines[OF ‹a ≠ 0›, of b "of_ocircline H"]
by simp
lemma moebius_similarity_preserve_orientation':
assumes "a ≠ 0" and "∞⇩h ∉ ocircline_set H" and "pos_oriented H"
shows "pos_oriented (moebius_ocircline (moebius_similarity a b) H)"
proof-
let ?M = "moebius_similarity a b"
let ?H = "moebius_ocircline ?M H"
have "∞⇩h ∉ ocircline_set ?H"
using ‹∞⇩h ∉ ocircline_set H› moebius_similarity_oriented_lines_to_oriented_lines[OF ‹a ≠ 0›]
by simp
have "∞⇩h ∈ disc_compl H"
using ‹∞⇩h ∉ ocircline_set H› ‹pos_oriented H› pos_oriented_circle_inf[of H] in_on_out
unfolding disc_def disc_compl_def ocircline_set_def
by auto
hence "∞⇩h ∈ disc_compl ?H"
using moebius_similarity_inf[OF ‹a ≠ 0›, of b]
by force
thus "pos_oriented ?H"
using pos_oriented_circle_inf[of ?H] disc_inter_disc_compl[of ?H] ‹∞⇩h ∉ ocircline_set ?H›
by auto
qed
lemma moebius_similarity_preserve_orientation:
assumes "a ≠ 0" and "∞⇩h ∉ ocircline_set H"
shows "pos_oriented H ⟷ pos_oriented(moebius_ocircline (moebius_similarity a b) H)"
proof-
let ?M = "moebius_similarity a b"
let ?H = "moebius_ocircline ?M H"
have "∞⇩h ∉ ocircline_set ?H"
using ‹∞⇩h ∉ ocircline_set H› moebius_similarity_oriented_lines_to_oriented_lines[OF ‹a ≠ 0›]
by simp
have *: "H = moebius_ocircline (- moebius_similarity a b) ?H"
by simp
show ?thesis
using ‹a ≠ 0›
using moebius_similarity_preserve_orientation' [OF ‹a ≠ 0› ‹∞⇩h ∉ ocircline_set H›]
using moebius_similarity_preserve_orientation'[OF _ ‹∞⇩h ∉ ocircline_set ?H›, of "1/a" "-b/a"]
using moebius_similarity_inv[of a b, OF ‹a ≠ 0›] *
by auto
qed
lemma reciprocal_preserve_orientation:
assumes "0⇩h ∈ disc_compl H"
shows "pos_oriented (moebius_ocircline moebius_reciprocal H)"
proof-
have "∞⇩h ∈ disc_compl (moebius_ocircline moebius_reciprocal H)"
using assms
by force
thus "pos_oriented (moebius_ocircline moebius_reciprocal H)"
using pos_oriented_circle_inf[of "moebius_ocircline moebius_reciprocal H"]
using disc_inter_disc_compl[of "moebius_ocircline moebius_reciprocal H"]
using disc_compl_inter_ocircline_set[of "moebius_ocircline moebius_reciprocal H"]
by auto
qed
lemma reciprocal_not_preserve_orientation:
assumes "0⇩h ∈ disc H"
shows "¬ pos_oriented (moebius_ocircline moebius_reciprocal H)"
proof-
let ?H = "moebius_ocircline moebius_reciprocal H"
have "∞⇩h ∈ disc ?H"
using assms
by force
thus "¬ pos_oriented ?H"
using pos_oriented_circle_inf[of ?H] disc_inter_ocircline_set[of ?H]
by auto
qed
text ‹Orientation of the image of a given oriented circline $H$ under a given Möbius transformation
$M$ depends on whether the pole of $M$ (the point that $M$ maps to $\infty_{hc}$) lies in the disc
or in the disc complement of $H$ (if it is on the set of $H$, then it maps onto a line and we do not
discuss the orientation).›
lemma pole_in_disc:
assumes "M = mk_moebius a b c d" and "c ≠ 0" and "a*d - b*c ≠ 0"
assumes "is_pole M z" "z ∈ disc H"
shows "¬ pos_oriented (moebius_ocircline M H)"
proof-
let ?t1 = "moebius_translation (a / c)"
let ?rd = "moebius_rotation_dilatation ((b * c - a * d) / (c * c))"
let ?r = "moebius_reciprocal"
let ?t2 = "moebius_translation (d / c)"
have "0⇩h = moebius_pt (moebius_translation (d/c)) z"
using pole_mk_moebius[of a b c d z] assms
by simp
have "z ∉ ocircline_set H"
using ‹z ∈ disc H› disc_inter_ocircline_set[of H]
by blast
hence "0⇩h ∉ ocircline_set (moebius_ocircline ?t2 H)"
using ‹0⇩h = moebius_pt ?t2 z›
using moebius_pt_neq_I[of z _ ?t2]
by force
hence *: "∞⇩h ∉ ocircline_set (moebius_ocircline (?r + ?t2) H)"
using ‹0⇩h = moebius_pt (moebius_translation (d / c)) z›
by (metis circline_set_moebius_circline circline_set_moebius_circline_iff circline_set_of_ocircline moebius_pt_comp moebius_reciprocal ocircline_set_moebius_ocircline plus_moebius_def reciprocal_zero)
hence **: "∞⇩h ∉ ocircline_set (moebius_ocircline (?rd + ?r + ?t2) H)"
using ‹a*d - b*c ≠ 0› ‹c ≠ 0›
unfolding moebius_rotation_dilatation_def
using moebius_similarity_oriented_lines_to_oriented_lines[of _ "moebius_ocircline (?r + ?t2) H"]
by (metis divide_eq_0_iff divisors_zero moebius_ocircline_comp plus_moebius_def right_minus_eq)
have "¬ pos_oriented (moebius_ocircline (?r + ?t2) H)"
using pole_mk_moebius[of a b c d z] assms
using reciprocal_not_preserve_orientation
by force
hence "¬ pos_oriented (moebius_ocircline (?rd + ?r + ?t2) H)"
using *
using ‹a*d - b*c ≠ 0› ‹c ≠ 0›
using moebius_similarity_preserve_orientation[of _ "moebius_ocircline (?r + ?t2) H"]
unfolding moebius_rotation_dilatation_def
by simp
hence "¬ pos_oriented (moebius_ocircline (?t1 + ?rd + ?r + ?t2) H)"
using **
using moebius_similarity_preserve_orientation[of _ "moebius_ocircline (?rd + ?r + ?t2) H"]
unfolding moebius_translation_def
by simp
thus ?thesis
using assms
by simp (subst moebius_decomposition, simp_all)
qed
lemma pole_in_disc_compl:
assumes "M = mk_moebius a b c d" and "c ≠ 0" and "a*d - b*c ≠ 0"
assumes "is_pole M z" and "z ∈ disc_compl H"
shows "pos_oriented (moebius_ocircline M H)"
proof-
let ?t1 = "moebius_translation (a / c)"
let ?rd = "moebius_rotation_dilatation ((b * c - a * d) / (c * c))"
let ?r = "moebius_reciprocal"
let ?t2 = "moebius_translation (d / c)"
have "0⇩h = moebius_pt (moebius_translation (d/c)) z"
using pole_mk_moebius[of a b c d z] assms
by simp
have "z ∉ ocircline_set H"
using ‹z ∈ disc_compl H› disc_compl_inter_ocircline_set[of H]
by blast
hence "0⇩h ∉ ocircline_set (moebius_ocircline ?t2 H)"
using ‹0⇩h = moebius_pt ?t2 z›
using moebius_pt_neq_I[of z _ ?t2]
by force
hence *: "∞⇩h ∉ ocircline_set (moebius_ocircline (?r + ?t2) H)"
using ‹0⇩h = moebius_pt (moebius_translation (d / c)) z›
by (metis circline_set_moebius_circline circline_set_moebius_circline_iff circline_set_of_ocircline moebius_pt_comp moebius_reciprocal ocircline_set_moebius_ocircline plus_moebius_def reciprocal_zero)
hence **: "∞⇩h ∉ ocircline_set (moebius_ocircline (?rd + ?r + ?t2) H)"
using ‹a*d - b*c ≠ 0› ‹c ≠ 0›
unfolding moebius_rotation_dilatation_def
using moebius_similarity_oriented_lines_to_oriented_lines[of _ "moebius_ocircline (?r + ?t2) H"]
by (metis divide_eq_0_iff divisors_zero moebius_ocircline_comp plus_moebius_def right_minus_eq)
have "pos_oriented (moebius_ocircline (?r + ?t2) H)"
using pole_mk_moebius[of a b c d z] assms
using reciprocal_preserve_orientation
by force
hence "pos_oriented (moebius_ocircline (?rd + ?r + ?t2) H)"
using *
using ‹a*d - b*c ≠ 0› ‹c ≠ 0›
using moebius_similarity_preserve_orientation[of _ "moebius_ocircline (?r + ?t2) H"]
unfolding moebius_rotation_dilatation_def
by simp
hence "pos_oriented (moebius_ocircline (?t1 + ?rd + ?r + ?t2) H)"
using **
using moebius_similarity_preserve_orientation[of _ "moebius_ocircline (?rd + ?r + ?t2) H"]
unfolding moebius_translation_def
by simp
thus ?thesis
using assms
by simp (subst moebius_decomposition, simp_all)
qed
subsection ‹Oriented circlines uniqueness›
lemma ocircline_01inf:
assumes "0⇩h ∈ ocircline_set H ∧ 1⇩h ∈ ocircline_set H ∧ ∞⇩h ∈ ocircline_set H"
shows "H = o_x_axis ∨ H = opposite_ocircline o_x_axis"
proof-
have "0⇩h ∈ circline_set (of_ocircline H) ∧ 1⇩h ∈ circline_set (of_ocircline H) ∧ ∞⇩h ∈ circline_set (of_ocircline H)"
using assms
by simp
hence "of_ocircline H = x_axis"
using unique_circline_01inf'
by auto
thus "H = o_x_axis ∨ H = opposite_ocircline o_x_axis"
by (metis inj_of_ocircline of_ocircline_o_x_axis)
qed
lemma unique_ocircline_01inf:
shows "∃! H. 0⇩h ∈ ocircline_set H ∧ 1⇩h ∈ ocircline_set H ∧ ∞⇩h ∈ ocircline_set H ∧ ii⇩h ∉ disc H"
proof
show "0⇩h ∈ ocircline_set o_x_axis ∧ 1⇩h ∈ ocircline_set o_x_axis ∧ ∞⇩h ∈ ocircline_set o_x_axis ∧ ii⇩h ∉ disc o_x_axis"
by simp
next
fix H
assume "0⇩h ∈ ocircline_set H ∧ 1⇩h ∈ ocircline_set H ∧ ∞⇩h ∈ ocircline_set H ∧ ii⇩h ∉ disc H"
hence "0⇩h ∈ ocircline_set H ∧ 1⇩h ∈ ocircline_set H ∧ ∞⇩h ∈ ocircline_set H" "ii⇩h ∉ disc H"
by auto
hence "H = o_x_axis ∨ H = opposite_ocircline o_x_axis"
using ocircline_01inf
by simp
thus "H = o_x_axis"
using ‹ii⇩h ∉ disc H›
by auto
qed
lemma unique_ocircline_set:
assumes "A ≠ B" and "A ≠ C" and "B ≠ C"
shows "∃! H. pos_oriented H ∧ (A ∈ ocircline_set H ∧ B ∈ ocircline_set H ∧ C ∈ ocircline_set H)"
proof-
obtain M where *: "moebius_pt M A = 0⇩h" "moebius_pt M B = 1⇩h" "moebius_pt M C = ∞⇩h"
using ex_moebius_01inf[OF assms]
by auto
let ?iM = "moebius_pt (moebius_inv M)"
have **: "?iM 0⇩h = A" "?iM 1⇩h = B" "?iM ∞⇩h = C"
using *
by (auto simp add: moebius_pt_invert)
let ?H = "moebius_ocircline (moebius_inv M) o_x_axis"
have 1: "A ∈ ocircline_set ?H" "B ∈ ocircline_set ?H" "C ∈ ocircline_set ?H"
using **
by auto
have 2: "⋀ H'. A ∈ ocircline_set H' ∧ B ∈ ocircline_set H' ∧ C ∈ ocircline_set H' ⟹ H' = ?H ∨ H' = opposite_ocircline ?H"
proof-
fix H'
let ?H' = "ocircline_set H'" and ?H'' = "ocircline_set (moebius_ocircline M H')"
assume "A ∈ ocircline_set H' ∧ B ∈ ocircline_set H' ∧ C ∈ ocircline_set H'"
hence "moebius_pt M A ∈ ?H''" "moebius_pt M B ∈ ?H''" "moebius_pt M C ∈ ?H''"
by auto
hence "0⇩h ∈ ?H''" "1⇩h ∈ ?H''" "∞⇩h ∈ ?H''"
using *
by auto
hence "moebius_ocircline M H' = o_x_axis ∨ moebius_ocircline M H' = opposite_ocircline o_x_axis"
using ocircline_01inf
by auto
hence "o_x_axis = moebius_ocircline M H' ∨ o_x_axis = opposite_ocircline (moebius_ocircline M H')"
by auto
thus "H' = ?H ∨ H' = opposite_ocircline ?H"
proof
assume *: "o_x_axis = moebius_ocircline M H'"
show "H' = moebius_ocircline (moebius_inv M) o_x_axis ∨ H' = opposite_ocircline (moebius_ocircline (moebius_inv M) o_x_axis)"
by (rule disjI1) (subst *, simp)
next
assume *: "o_x_axis = opposite_ocircline (moebius_ocircline M H')"
show "H' = moebius_ocircline (moebius_inv M) o_x_axis ∨ H' = opposite_ocircline (moebius_ocircline (moebius_inv M) o_x_axis)"
by (rule disjI2) (subst *, simp)
qed
qed
show ?thesis (is "∃! x. ?P x")
proof (cases "pos_oriented ?H")
case True
show ?thesis
proof
show "?P ?H"
using 1 True
by auto
next
fix H
assume "?P H"
thus "H = ?H"
using 1 2[of H] True
by auto
qed
next
case False
let ?OH = "opposite_ocircline ?H"
show ?thesis
proof
show "?P ?OH"
using 1 False
by auto
next
fix H
assume "?P H"
thus "H = ?OH"
using False 2[of H]
by auto
qed
qed
qed
lemma ocircline_set_0h:
assumes "ocircline_set H = {0⇩h}"
shows "H = o_circline_point_0 ∨ H = opposite_ocircline (o_circline_point_0)"
proof-
have "of_ocircline H = circline_point_0"
using assms
using unique_circline_type_zero_0' card_eq1_circline_type_zero[of "of_ocircline H"]
by auto
thus ?thesis
by (metis inj_of_ocircline of_ocircline_o_circline_point_0)
qed
end