Theory Poincare_Lines_Ideal_Points

theory Poincare_Lines_Ideal_Points
imports Poincare_Lines
begin

(* ------------------------------------------------------------------ *)
subsection‹Ideal points of h-lines›
(* ------------------------------------------------------------------ *)

(* TODO: Introduce ideal points for the oriented circline - 
   it would be a list, not a set of two points *)

text‹\emph{Ideal points} of an h-line are points where the h-line intersects the unit disc.›

(* ------------------------------------------------------------------ *)
subsubsection ‹Calculation of ideal points›
(* ------------------------------------------------------------------ *)

text ‹We decided to define ideal points constructively, i.e., we calculate the coordinates of ideal
points for a given h-line explicitly. Namely, if the h-line is determined by $A$ and $B$, the two
intersection points are $$\frac{B}{|B|^2}\left(-A \pm i\cdot \sqrt{|B|^2 - A^2}\right).$$›

definition calc_ideal_point1_cvec :: "complex ⇒ complex ⇒ complex_vec" where
 [simp]:  "calc_ideal_point1_cvec A B =
    (let discr = Re ((cmod B)2 - (Re A)2) in
         (B*(-A - 𝗂*sqrt(discr)), (cmod B)2))"

definition calc_ideal_point2_cvec :: "complex ⇒ complex ⇒ complex_vec" where
  [simp]: "calc_ideal_point2_cvec A B =
    (let discr = Re ((cmod B)2 - (Re A)2) in
         (B*(-A + 𝗂*sqrt(discr)), (cmod B)2))"

definition calc_ideal_points_cmat_cvec :: "complex_mat ⇒ complex_vec set" where
 [simp]:  "calc_ideal_points_cmat_cvec H =
    (if is_poincare_line_cmat H then
        let (A, B, C, D) = H
         in {calc_ideal_point1_cvec A B, calc_ideal_point2_cvec A B}
     else
        {(-1, 1), (1, 1)})"

lift_definition calc_ideal_points_clmat_hcoords :: "circline_mat ⇒ complex_homo_coords set" is calc_ideal_points_cmat_cvec
  by (auto simp add: Let_def split: if_split_asm)

lift_definition calc_ideal_points :: "circline ⇒ complex_homo set" is calc_ideal_points_clmat_hcoords
proof transfer
  fix H1 H2
  assume hh: "hermitean H1 ∧ H1 ≠ mat_zero" "hermitean H2 ∧ H2 ≠ mat_zero"
  obtain A1 B1 C1 D1 A2 B2 C2 D2 where *: "H1 = (A1, B1, C1, D1)" "H2 = (A2, B2, C2, D2)"
    by (cases H1, cases H2, auto)
  assume "circline_eq_cmat H1 H2"
  then obtain k where k: "k ≠ 0" "H2 = cor k *sm H1"
    by auto
  thus "rel_set (≈v) (calc_ideal_points_cmat_cvec H1) (calc_ideal_points_cmat_cvec H2)"
  proof (cases "is_poincare_line_cmat H1")
    case True
    hence "is_poincare_line_cmat H2"
      using k * hermitean_mult_real[of H1 k] hh
      by (auto simp add: power2_eq_square norm_mult)
    have **: "sqrt (¦k¦ * cmod B1 * (¦k¦ * cmod B1) - k * Re D1 * (k * Re D1)) =
         ¦k¦ * sqrt(cmod B1 * cmod B1 - Re D1 * Re D1)"
    proof-
      have "¦k¦ * cmod B1 * (¦k¦ * cmod B1) - k * Re D1 * (k * Re D1) =
            k2 * (cmod B1 * cmod B1 - Re D1 * Re D1)"
        by (simp add: power2_eq_square field_simps)
      thus ?thesis
        by (simp add: real_sqrt_mult)
    qed
    show ?thesis
      using ‹is_poincare_line_cmat H1› ‹is_poincare_line_cmat H2›
      using * k
      apply (simp add: Let_def)
      apply safe
      apply (simp add: power2_eq_square rel_set_def norm_mult)
      apply safe
         apply (cases "k > 0")
          apply (rule_tac x="(cor k)2" in exI)
          apply (subst **)
          apply (simp add: power2_eq_square field_simps)
         apply (erule notE, rule_tac x="(cor k)2" in exI)
         apply (subst **)
         apply (simp add: power2_eq_square field_simps)
        apply (cases "k > 0")
        apply (erule notE, rule_tac x="(cor k)2" in exI)
        apply (subst **)
        apply (simp add: power2_eq_square field_simps)
        apply (rule_tac x="(cor k)2" in exI)
        apply (subst **)
        apply (simp add: power2_eq_square field_simps)
       apply (cases "k > 0")
        apply (rule_tac x="(cor k)2" in exI)
        apply (subst **)
        apply (simp add: power2_eq_square field_simps)
       apply (erule notE, rule_tac x="(cor k)2" in exI)
       apply (subst **)
       apply (simp add: power2_eq_square field_simps)
      apply (rule_tac x="(cor k)2" in exI)
      apply (cases "k > 0")
       apply (erule notE, rule_tac x="(cor k)2" in exI)
       apply (subst **)
       apply (simp add: power2_eq_square field_simps)
      apply (subst **)
      apply (simp add: power2_eq_square field_simps)
      done
  next
    case False
    hence "¬ is_poincare_line_cmat H2"
      using k * hermitean_mult_real[of H1 k] hh
      by (auto simp add: power2_eq_square norm_mult)
    have "rel_set (≈v) {(- 1, 1), (1, 1)} {(- 1, 1), (1, 1)}"
      by (simp add: rel_set_def)
    thus ?thesis
      using ‹¬ is_poincare_line_cmat H1› ‹¬ is_poincare_line_cmat H2›
      using *
      by (auto simp add: Let_def)
  qed
qed

text ‹Correctness of the calculation›

text‹We show that for every h-line its two calculated ideal points are different and are on the
intersection of that line and the unit circle.›

text ‹Calculated ideal points are on the unit circle›

lemma calc_ideal_point_1_unit:
  assumes "is_real A" "(cmod B)2 > (cmod A)2"
  assumes "(z1, z2) = calc_ideal_point1_cvec A B"
  shows "z1 * cnj z1 = z2 * cnj z2"
proof-
  let ?discr = "Re ((cmod B)2 - (Re A)2)"
  have "?discr > 0"
    using assms
    by (simp add: cmod_power2)
  have "(B*(-A - 𝗂*sqrt(?discr))) * cnj (B*(-A - 𝗂*sqrt(?discr))) = (B * cnj B) * (A2 + cor (abs ?discr))"
    using ‹is_real A› eq_cnj_iff_real[of A]
    by (simp add: field_simps power2_eq_square)
  also have "... = (B * cnj B) * (cmod B)2"
    using ‹?discr > 0›
    using assms
    using complex_of_real_Re[of "(cmod B)2 - (Re A)2"] complex_of_real_Re[of A] ‹is_real A›
    by (simp add: power2_eq_square)
  also have "... = (cmod B)2 * cnj ((cmod B)2)"
    using complex_cnj_complex_of_real complex_mult_cnj_cmod
    by presburger
  finally show ?thesis
    using assms
    by simp
qed

lemma calc_ideal_point_2_unit:
  assumes "is_real A" "(cmod B)2 > (cmod A)2"
  assumes "(z1, z2) = calc_ideal_point2_cvec A B"
  shows "z1 * cnj z1 = z2 * cnj z2"
proof-
  let ?discr = "Re ((cmod B)2 - (Re A)2)"
  have "?discr > 0"
    using assms
    by (simp add: cmod_power2)
  have "(B*(-A + 𝗂*sqrt(?discr))) * cnj (B*(-A + 𝗂*sqrt(?discr))) = (B * cnj B) * (A2 + cor (abs ?discr))"
    using ‹is_real A› eq_cnj_iff_real[of A]
    by (simp add: field_simps power2_eq_square)
  also have "... = (B * cnj B) * (cmod B)2"
    using ‹?discr > 0›
    using assms
    using complex_of_real_Re[of "(cmod B)2 - (Re A)2"] complex_of_real_Re[of A] ‹is_real A›
    by (simp add: power2_eq_square)
  also have "... = (cmod B)2 * cnj ((cmod B)2)"
    using complex_cnj_complex_of_real complex_mult_cnj_cmod
    by presburger
  finally show ?thesis
    using assms
    by simp
qed

lemma calc_ideal_points_on_unit_circle:
  shows "∀ z ∈ calc_ideal_points H. z ∈ circline_set unit_circle"
  unfolding circline_set_def
  apply simp
proof (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 "∀ (z1, z2) ∈ calc_ideal_points_cmat_cvec H. z1 * cnj z1 = z2 * cnj z2"
    using hermitean_elems[of A B C D]
    unfolding calc_ideal_points_cmat_cvec_def
    using calc_ideal_point_1_unit[of A B]
    using calc_ideal_point_2_unit[of A B]
    using hh *
    apply (cases "calc_ideal_point1_cvec A B", cases "calc_ideal_point2_cvec A B")
    apply (auto simp add: Let_def simp del: calc_ideal_point1_cvec_def calc_ideal_point2_cvec_def)
    done
  thus "Ball (calc_ideal_points_cmat_cvec H) (on_circline_cmat_cvec unit_circle_cmat)"
    using on_circline_cmat_cvec_unit
    by (auto simp del: on_circline_cmat_cvec_def calc_ideal_points_cmat_cvec_def)
qed

text ‹Calculated ideal points are on the h-line›

lemma calc_ideal_point1_sq:
  assumes "(z1, z2) = calc_ideal_point1_cvec A B" "is_real A" "(cmod B)2 > (cmod A)2"
  shows "z1 * cnj z1 + z2 * cnj z2 = 2 * (B * cnj B)2"
proof-
  let ?discr = "Re ((cmod B)2 - (Re A)2)"
  have "?discr > 0"
    using assms
    by (simp add: cmod_power2)
  have "z1 * cnj z1 = (B * cnj B) * (-A + 𝗂*sqrt(?discr))*(-A - 𝗂*sqrt(?discr))"
    using assms eq_cnj_iff_real[of A]
    by (simp)
  also have "... = (B * cnj B) * (A2 + ?discr)"
    using complex_of_real_Re[of A] ‹is_real A› ‹?discr > 0›
    by (simp add: power2_eq_square field_simps)
  finally
  have "z1 * cnj z1 = (B * cnj B)2"
    using complex_of_real_Re[of "(cmod B)2 - (Re A)2"] complex_of_real_Re[of A] ‹is_real A›
    using complex_mult_cnj_cmod[of B]
    by (simp add: power2_eq_square)
  moreover
  have "z2 * cnj z2 = (B * cnj B)2"
    using assms
    by simp
  ultimately
  show ?thesis
    by simp
qed

lemma calc_ideal_point2_sq:
  assumes "(z1, z2) = calc_ideal_point2_cvec A B" "is_real A" "(cmod B)2 > (cmod A)2"
  shows "z1 * cnj z1 + z2 * cnj z2 = 2 * (B * cnj B)2"
proof-
  let ?discr = "Re ((cmod B)2 - (Re A)2)"
  have "?discr > 0"
    using assms
    by (simp add: cmod_power2)
  have "z1 * cnj z1 = (B * cnj B) * (-A + 𝗂*sqrt(?discr))*(-A - 𝗂*sqrt(?discr))"
    using assms eq_cnj_iff_real[of A]
    by simp
  also have "... = (B * cnj B) * (A2 + ?discr)"
    using complex_of_real_Re[of A] ‹is_real A› ‹?discr > 0›
    by (simp add: power2_eq_square field_simps)
  finally
  have "z1 * cnj z1 = (B * cnj B)2"
    using complex_of_real_Re[of "(cmod B)2 - (Re A)2"] complex_of_real_Re[of A] ‹is_real A›
    using complex_mult_cnj_cmod[of B]
    by (simp add: power2_eq_square)
  moreover
  have "z2 * cnj z2 = (B * cnj B)2"
    using assms
    by simp
  ultimately
  show ?thesis
    by simp
qed

lemma calc_ideal_point1_mix:
  assumes "(z1, z2) = calc_ideal_point1_cvec A B" "is_real A" "(cmod B)2 > (cmod A)2"
  shows "B * cnj z1 * z2 + cnj B * z1 * cnj z2 = - 2 * A * (B * cnj B)2 "
proof-
  have "B*cnj z1 + cnj B*z1 = -2*A*B*cnj B"
    using assms eq_cnj_iff_real[of A]
    by (simp, simp add: field_simps)
  moreover
  have "cnj z2 = z2"
    using assms
    by simp
  hence "B*cnj z1*z2 + cnj B*z1*cnj z2 = (B*cnj z1 + cnj B*z1)*z2"
    by (simp add: field_simps)
  ultimately
  have "B*cnj z1*z2 + cnj B*z1*cnj z2 = -2*A*(B* cnj B)*z2"
    by simp
  also have "… = -2*A*(B * cnj B)2"
    using assms
    using complex_mult_cnj_cmod[of B]
    by (simp add: power2_eq_square)
  finally
  show ?thesis
    .
qed

lemma calc_ideal_point2_mix:
  assumes "(z1, z2) = calc_ideal_point2_cvec A B" "is_real A" "(cmod B)2 > (cmod A)2"
  shows "B * cnj z1 * z2 + cnj B * z1 * cnj z2 = - 2 * A * (B * cnj B)2 "
proof-
  have "B*cnj z1 + cnj B*z1 = -2*A*B*cnj B"
    using assms eq_cnj_iff_real[of A]
    by (simp, simp add: field_simps)
  moreover
  have "cnj z2 = z2"
    using assms
    by simp
  hence "B*cnj z1*z2 + cnj B*z1*cnj z2 = (B*cnj z1 + cnj B*z1)*z2"
    by (simp add: field_simps)
  ultimately
  have "B*cnj z1*z2 + cnj B*z1*cnj z2 = -2*A*(B* cnj B)*z2"
    by simp
  also have "… = -2*A*(B * cnj B)2"
    using assms
    using complex_mult_cnj_cmod[of B]
    by (simp add: power2_eq_square)
  finally
  show ?thesis
    .
qed

lemma calc_ideal_point1_on_circline:
  assumes "(z1, z2) = calc_ideal_point1_cvec A B" "is_real A" "(cmod B)2 > (cmod A)2"
  shows "A*z1*cnj z1 + B*cnj z1*z2 + cnj B*z1*cnj z2 + A*z2*cnj z2 = 0" (is "?lhs = 0")
proof-
  have "?lhs = A * (z1 * cnj z1 + z2 * cnj z2) + (B * cnj z1 * z2 + cnj B * z1 * cnj z2)"
    by (simp add: field_simps)
  also have "... = 2*A*(B*cnj B)2 + (-2*A*(B*cnj B)2)"
    using calc_ideal_point1_sq[OF assms]
    using calc_ideal_point1_mix[OF assms]
    by simp
  finally
  show ?thesis
    by simp
qed

lemma calc_ideal_point2_on_circline:
  assumes "(z1, z2) = calc_ideal_point2_cvec A B" "is_real A" "(cmod B)2 > (cmod A)2"
  shows "A*z1*cnj z1 + B*cnj z1*z2 + cnj B*z1*cnj z2 + A*z2*cnj z2 = 0" (is "?lhs = 0")
proof-
  have "?lhs = A * (z1 * cnj z1 + z2 * cnj z2) + (B * cnj z1 * z2 + cnj B * z1 * cnj z2)"
    by (simp add: field_simps)
  also have "... = 2*A*(B*cnj B)2 + (-2*A*(B*cnj B)2)"
    using calc_ideal_point2_sq[OF assms]
    using calc_ideal_point2_mix[OF assms]
    by simp
  finally
  show ?thesis
    by simp
qed

lemma calc_ideal_points_on_circline:
  assumes "is_poincare_line H"
  shows "∀ z ∈ calc_ideal_points H. z ∈ circline_set H"
  using assms
  unfolding circline_set_def
  apply simp
proof (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)
  obtain z11 z12 z21 z22 where **: "(z11, z12) = calc_ideal_point1_cvec A B" "(z21, z22) = calc_ideal_point2_cvec A B"
    by (cases "calc_ideal_point1_cvec A B", cases "calc_ideal_point2_cvec A B") auto

  assume "is_poincare_line_cmat H"
  hence "∀ (z1, z2) ∈ calc_ideal_points_cmat_cvec H. A*z1*cnj z1 + B*cnj z1*z2 + C*z1*cnj z2 + D*z2*cnj z2 = 0"
    using * ** hh
    using hermitean_elems[of A B C D]
    using calc_ideal_point1_on_circline[of z11 z12 A B]
    using calc_ideal_point2_on_circline[of z21 z22 A B]
    by (auto simp del: calc_ideal_point1_cvec_def calc_ideal_point2_cvec_def)
  thus "Ball (calc_ideal_points_cmat_cvec H) (on_circline_cmat_cvec H)"
    using on_circline_cmat_cvec_circline_equation *
    by (auto simp del: on_circline_cmat_cvec_def calc_ideal_points_cmat_cvec_def simp add: field_simps)
qed

text ‹Calculated ideal points of an h-line are different›

lemma calc_ideal_points_cvec_different [simp]:
  assumes "(cmod B)2 > (cmod A)2" "is_real A"
  shows "¬ (calc_ideal_point1_cvec A B ≈v calc_ideal_point2_cvec A B)"
  using assms
  by (auto) (auto simp add: cmod_def)

lemma calc_ideal_points_different:
  assumes "is_poincare_line H"
  shows  "∃ i1 ∈ (calc_ideal_points H). ∃ i2 ∈ (calc_ideal_points H). i1 ≠ i2"
  using assms
proof (transfer, transfer)
  fix H
  assume hh: "hermitean H ∧ H ≠ mat_zero" "is_poincare_line_cmat H"
  obtain A B C D where *: "H = (A, B, C, D)"
    by (cases H, auto)
  hence "is_real A" using hh hermitean_elems by auto
  thus "∃i1∈calc_ideal_points_cmat_cvec H. ∃i2∈calc_ideal_points_cmat_cvec H. ¬ i1 ≈v i2"
    using * hh calc_ideal_points_cvec_different[of A B]
    apply (rule_tac x="calc_ideal_point1_cvec A B" in bexI)
    apply (rule_tac x="calc_ideal_point2_cvec A B" in bexI)
    by auto
qed

lemma two_calc_ideal_points [simp]:
  assumes "is_poincare_line H"                
  shows "card (calc_ideal_points H) = 2"
proof-
  have  "∃ x ∈ calc_ideal_points H. ∃ y ∈ calc_ideal_points H. ∀ z ∈ calc_ideal_points H. z = x ∨ z = y"
    by (transfer, transfer, case_tac H, simp del: calc_ideal_point1_cvec_def calc_ideal_point2_cvec_def)
  then obtain x y where *: "calc_ideal_points H = {x, y}"
    by auto
  moreover
  have "x ≠ y"
    using calc_ideal_points_different[OF assms] *
    by auto
  ultimately
  show ?thesis
    by auto
qed

subsubsection ‹Ideal points›

text ‹Next we give a genuine definition of ideal points -- these are the intersections of the h-line with the unit circle›

definition ideal_points :: "circline ⇒ complex_homo set" where
  "ideal_points H = circline_intersection H unit_circle"

text ‹Ideal points are on the unit circle and on the h-line›
lemma ideal_points_on_unit_circle:
  shows "∀ z ∈ ideal_points H. z ∈ circline_set unit_circle"
  unfolding ideal_points_def circline_intersection_def circline_set_def
  by simp

lemma ideal_points_on_circline:
  shows "∀ z ∈ ideal_points H. z ∈ circline_set H"
  unfolding ideal_points_def circline_intersection_def circline_set_def
  by simp


text ‹For each h-line there are exactly two ideal points›
lemma two_ideal_points:
  assumes "is_poincare_line H"
  shows "card (ideal_points H) = 2"
proof-
  have "H ≠ unit_circle"
    using assms not_is_poincare_line_unit_circle
    by auto
  let ?int = "circline_intersection H unit_circle"
  obtain i1 i2 where "i1 ∈ ?int" "i2 ∈ ?int" "i1 ≠ i2"
    using calc_ideal_points_on_circline[OF assms]
    using calc_ideal_points_on_unit_circle[of H]
    using calc_ideal_points_different[OF assms]
    unfolding circline_intersection_def circline_set_def
    by auto
  thus ?thesis
    unfolding ideal_points_def
    using circline_intersection_at_most_2_points[OF ‹H ≠ unit_circle›]
    using card_geq_2_iff_contains_2_elems[of ?int]
    by auto
qed

text ‹They are exactly the two points that our calculation finds›
lemma ideal_points_unique:
  assumes "is_poincare_line H"
  shows "ideal_points H = calc_ideal_points H"
proof-
  have "calc_ideal_points H ⊆ ideal_points H"
    using calc_ideal_points_on_circline[OF assms]
    using calc_ideal_points_on_unit_circle[of H]
    unfolding ideal_points_def circline_intersection_def circline_set_def
    by auto
  moreover
  have "H ≠ unit_circle"
    using not_is_poincare_line_unit_circle assms
    by auto
  hence "finite (ideal_points H)"
    using circline_intersection_at_most_2_points[of H unit_circle]
    unfolding ideal_points_def
    by auto
  ultimately
  show ?thesis
    using card_subset_eq[of "ideal_points H" "calc_ideal_points H"]
    using two_calc_ideal_points[OF assms]
    using two_ideal_points[OF assms]
    by auto
qed

text ‹For each h-line we can obtain two different ideal points›
lemma obtain_ideal_points:
  assumes "is_poincare_line H"
  obtains i1 i2 where "i1 ≠ i2" "ideal_points H = {i1, i2}"
  using two_ideal_points[OF assms] card_eq_2_iff_doubleton[of "ideal_points H"]
  by blast

text ‹Ideal points of each h-line constructed from two points in the disc are different than those two points›
lemma ideal_points_different:
  assumes "u ∈ unit_disc" "v ∈ unit_disc" "u ≠ v"
  assumes "ideal_points (poincare_line u v) = {i1, i2}"
  shows "i1 ≠ i2" "u ≠ i1" "u ≠ i2" "v ≠ i1" "v ≠ i2"
proof-
  have "i1 ∈ ocircline_set ounit_circle" "i2 ∈ ocircline_set ounit_circle"
    using assms(3) assms(4) ideal_points_on_unit_circle is_poincare_line_poincare_line
    by fastforce+
  thus "u ≠ i1" "u ≠ i2" "v ≠ i1" "v ≠ i2"
    using assms(1-2)
    using disc_inter_ocircline_set[of ounit_circle]
    unfolding unit_disc_def
    by auto
  show "i1 ≠ i2"
    using assms
    by (metis doubleton_eq_iff is_poincare_line_poincare_line obtain_ideal_points)
qed

text ‹H-line is uniquely determined by its ideal points›
lemma ideal_points_line_unique:        
  assumes "is_poincare_line H" "ideal_points H = {i1, i2}"
  shows "H = poincare_line i1 i2"
  by (smt assms(1) assms(2) calc_ideal_points_on_unit_circle circline_set_def ex_poincare_line_points ideal_points_different(1) ideal_points_on_circline ideal_points_unique insertI1 insert_commute inversion_unit_circle mem_Collect_eq unique_poincare_line_general)

text ‹Ideal points of some special h-lines›

text‹Ideal points of @{term x_axis}›
lemma ideal_points_x_axis
  [simp]: "ideal_points x_axis = {of_complex (-1), of_complex 1}"
proof (subst ideal_points_unique, simp)
  have "calc_ideal_points_clmat_hcoords x_axis_clmat = {of_complex_hcoords (- 1), of_complex_hcoords 1}"
    by transfer auto
  thus "calc_ideal_points x_axis = {of_complex (- 1), of_complex 1}"
    by (simp add: calc_ideal_points.abs_eq of_complex.abs_eq x_axis_def)
qed

text ‹Ideal points are proportional vectors only if h-line is a line segment passing trough zero›
lemma ideal_points_proportional:
  assumes "is_poincare_line H" "ideal_points H = {i1, i2}" "to_complex i1 = cor k * to_complex i2"
  shows "0h ∈ circline_set H"
proof-
  have "i1 ≠ i2"
    using ‹ideal_points H = {i1, i2}›
    using ‹is_poincare_line H› ex_poincare_line_points ideal_points_different(1) by blast

  have "i1 ∈ circline_set unit_circle" "i2 ∈ circline_set unit_circle"
    using assms calc_ideal_points_on_unit_circle ideal_points_unique 
    by blast+

  hence "cmod (cor k) = 1"
    using ‹to_complex i1 = cor k * to_complex i2›
    by (metis (mono_tags, lifting) circline_set_unit_circle imageE mem_Collect_eq mult.right_neutral norm_mult to_complex_of_complex unit_circle_set_def)
  hence "k = -1"
    using ‹to_complex i1 = cor k * to_complex i2› ‹i1 ≠ i2›
    using ‹i1 ∈ circline_set unit_circle› ‹i2 ∈ circline_set unit_circle›
    by (smt (verit, best) mult_cancel_right1 norm_of_real not_inf_on_unit_circle'' of_complex_to_complex of_real_1) 

  have "∀ i1 ∈ calc_ideal_points H. ∀ i2 ∈ calc_ideal_points H. is_poincare_line H ∧ i1 ≠ i2 ∧ to_complex i1 = - to_complex i2 ⟶ 
           0h ∈ circline_set H"
    unfolding circline_set_def
  proof (simp, transfer, transfer, safe)
    fix A B C D i11 i12 i21 i22 k
    assume H:"hermitean (A, B, C, D)" "(A, B, C, D) ≠ mat_zero" 
    assume line: "is_poincare_line_cmat (A, B, C, D)"
    assume i1: "(i11, i12) ∈ calc_ideal_points_cmat_cvec (A, B, C, D)"
    assume i2:"(i21, i22) ∈ calc_ideal_points_cmat_cvec (A, B, C, D)"
    assume "¬ (i11, i12) ≈v (i21, i22)"
    assume opposite: "to_complex_cvec (i11, i12) = - to_complex_cvec (i21, i22)"


    let ?discr =  "sqrt ((cmod B)2 - (Re D)2)"
    let ?den = "(cmod B)2"
    let ?i1 = "B * (- D - 𝗂 * ?discr)"
    let ?i2 = "B * (- D + 𝗂 * ?discr)"

    have "i11 = ?i1 ∨ i11 = ?i2" "i12 = ?den"
      "i21 = ?i1 ∨ i21 = ?i2" "i22 = ?den"  
      using i1 i2 H line
      by (auto split: if_split_asm)
    hence i: "i11 = ?i1 ∧ i21 = ?i2 ∨ i11 = ?i2 ∧ i21 = ?i1"
      using ‹¬ (i11, i12) ≈v (i21, i22)›
      by auto

    have "?den ≠ 0"
      using line
      by auto

    hence "i11 = - i21"
      using opposite ‹i12 = ?den› ‹i22 = ?den›
      by (simp add: nonzero_neg_divide_eq_eq2)

    hence "?i1 = - ?i2"
      using i 
      by (metis add.inverse_inverse)

    hence "D = 0"
      using ‹?den ≠ 0›
      by (simp add: field_simps)

    thus "on_circline_cmat_cvec (A, B, C, D) 0v"
      by (simp add: vec_cnj_def)
  qed

  thus ?thesis
    using assms ‹k = -1›
    using calc_ideal_points_different ideal_points_unique
    by fastforce
qed

text ‹Transformations of ideal points›

text ‹Möbius transformations that fix the unit disc when acting on h-lines map their ideal points to ideal points.›
lemma ideal_points_moebius_circline [simp]:
  assumes  "unit_circle_fix M" "is_poincare_line H"
  shows "ideal_points (moebius_circline M H) = (moebius_pt M) ` (ideal_points H)" (is "?I' = ?M ` ?I")
proof-
  obtain i1 i2 where *: "i1 ≠ i2" "?I = {i1, i2}"
    using assms(2)
    by (rule obtain_ideal_points)
  let ?Mi1 = "?M i1" and ?Mi2 = "?M i2"
  have "?Mi1 ∈ ?M ` (circline_set H)"
       "?Mi2 ∈ ?M ` (circline_set H)"
       "?Mi1 ∈ ?M ` (circline_set unit_circle)"
       "?Mi2 ∈ ?M ` (circline_set unit_circle)"
    using *
    unfolding ideal_points_def circline_intersection_def circline_set_def
    by blast+
  hence "?Mi1 ∈ ?I'"
        "?Mi2 ∈ ?I'"
    using unit_circle_fix_iff[of M] assms
    unfolding ideal_points_def circline_intersection_def circline_set_def
    by (metis mem_Collect_eq moebius_circline)+
  moreover
  have "?Mi1 ≠ ?Mi2"
    using bij_moebius_pt[of M] *
    using moebius_pt_invert by blast
  moreover
  have "is_poincare_line (moebius_circline M H)"
    using assms unit_circle_fix_preserve_is_poincare_line
    by simp
  ultimately
  have "?I' = {?Mi1, ?Mi2}"
    using two_ideal_points[of "moebius_circline M H"]
    using card_eq_2_doubleton[of ?I' ?Mi1 ?Mi2]
    by simp
  thus ?thesis
    using *(2)
    by auto
qed

lemma ideal_points_poincare_line_moebius [simp]:
  assumes "unit_disc_fix M"  "u ∈ unit_disc" "v ∈ unit_disc" "u ≠ v"
  assumes "ideal_points (poincare_line u v) = {i1, i2}"
  shows "ideal_points (poincare_line (moebius_pt M u) (moebius_pt M v)) = {moebius_pt M i1, moebius_pt M i2}"
  using assms
  by auto

text ‹Conjugation also maps ideal points to ideal points›
lemma ideal_points_conjugate [simp]:
  assumes "is_poincare_line H"
  shows "ideal_points (conjugate_circline H) = conjugate ` (ideal_points H)" (is "?I' = ?M ` ?I")
proof-
  obtain i1 i2 where *: "i1 ≠ i2" "?I = {i1, i2}"
    using assms
    by (rule obtain_ideal_points)
  let ?Mi1 = "?M i1" and ?Mi2 = "?M i2"
  have "?Mi1 ∈ ?M ` (circline_set H)"
       "?Mi2 ∈ ?M ` (circline_set H)"
       "?Mi1 ∈ ?M ` (circline_set unit_circle)"
       "?Mi2 ∈ ?M ` (circline_set unit_circle)"
    using *
    unfolding ideal_points_def circline_intersection_def circline_set_def
    by blast+                                   
  hence "?Mi1 ∈ ?I'"
        "?Mi2 ∈ ?I'"
    unfolding ideal_points_def circline_intersection_def circline_set_def
    using circline_set_conjugate_circline circline_set_def conjugate_unit_circle_set 
    by blast+
  moreover
  have "?Mi1 ≠ ?Mi2"
    using ‹i1 ≠ i2›
    by (auto simp add: conjugate_inj)
  moreover
  have "is_poincare_line (conjugate_circline H)"
    using assms
    by simp
  ultimately
  have "?I' = {?Mi1, ?Mi2}"
    using two_ideal_points[of "conjugate_circline H"]
    using card_eq_2_doubleton[of ?I' ?Mi1 ?Mi2]
    by simp
  thus ?thesis
    using *(2)
    by auto
qed

lemma ideal_points_poincare_line_conjugate [simp]:
  assumes"u ∈ unit_disc" "v ∈ unit_disc" "u ≠ v"
  assumes "ideal_points (poincare_line u v) = {i1, i2}"
  shows "ideal_points (poincare_line (conjugate u) (conjugate v)) = {conjugate i1, conjugate i2}"
  using assms
  by auto

end