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 "0h  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 "0h  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 "0h  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" "0h  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" "0h  circline_set l"
    "x  circline_set l  circline_set x_axis" "x  0h" "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 "0h" "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" "0h  circline_set l"
    "y  circline_set l  circline_set y_axis" "y  0h" "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 "0h" "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 = 0h" "moebius_pt M v  positive_x_axis"
    using ex_unit_disc_fix_to_zero_positive_x_axis[of u v]
    by auto
  moreover
  hence "{0h, moebius_pt M v}  circline_set x_axis"
    unfolding positive_x_axis_def
    by auto
  moreover
  have "moebius_pt M v  0h"
    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 *sm 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 *sm 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) *sm 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 = 0h")
  case True
  thus ?thesis
    by (rule_tac x="x_axis" in exI) simp
next
  case False
  thus ?thesis
    by (rule_tac x="poincare_line 0h 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  0h" "x  h"
  shows "poincare_line 0h x = x_axis"
  using assms
  using is_poincare_line_0_real_is_x_axis[of "poincare_line 0h x" x]
  by auto

lemma poincare_line_0_imag_is_y_axis:
  assumes "y  circline_set y_axis" "y  0h" "y  h"
  shows "poincare_line 0h y = y_axis"
  using assms
  using is_poincare_line_0_imag_is_y_axis[of "poincare_line 0h 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 "0h  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 0h (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 "0h"}

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 {0h, 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 "0h  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 {0h, 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 0h (of_complex x))"
    using assms
    using unique_poincare_line[of "0h" "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