Theory Poincare_Perpendicular

theory Poincare_Perpendicular
  imports Poincare_Lines_Axis_Intersections
begin

(* ------------------------------------------------------------------ *)
section‹H-perpendicular h-lines in the Poincar\'e model›
(* ------------------------------------------------------------------ *)

definition perpendicular_to_x_axis_cmat :: "complex_mat ⇒ bool" where
 [simp]: "perpendicular_to_x_axis_cmat H ⟷ (let (A, B, C, D) = H in is_real B)"

lift_definition perpendicular_to_x_axis_clmat :: "circline_mat ⇒ bool" is perpendicular_to_x_axis_cmat
  done

lift_definition perpendicular_to_x_axis :: "circline ⇒ bool" is perpendicular_to_x_axis_clmat
  by transfer auto

lemma perpendicular_to_x_axis:
  assumes "is_poincare_line H"
  shows "perpendicular_to_x_axis H ⟷ perpendicular x_axis H"
  using assms
  unfolding perpendicular_def
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" "(cmod B)⇧2 > (cmod A)⇧2" "H = (A, B, cnj B, A)"
    using hermitean_elems[of A B C D] hh
    by auto
  thus "perpendicular_to_x_axis_cmat H =
        (cos_angle_cmat (of_circline_cmat x_axis_cmat) (of_circline_cmat H) = 0)"
    using cmod_square[of B] cmod_square[of A]
    by simp
qed

lemma perpendicular_to_x_axis_y_axis:
  assumes "perpendicular_to_x_axis (poincare_line 0⇩h (of_complex z))" "z ≠ 0"
  shows "is_imag z"
  using assms
  by (transfer, transfer, simp)


lemma wlog_perpendicular_axes:
  assumes in_disc: "u ∈ unit_disc" "v ∈ unit_disc" "z ∈ unit_disc"
  assumes perpendicular: "is_poincare_line H1" "is_poincare_line H2" "perpendicular H1 H2"
  assumes "z ∈ circline_set H1 ∩ circline_set H2" "u ∈ circline_set H1" "v ∈ circline_set H2"
  assumes axes: "⋀ x y. ⟦is_real x; 0 ≤ Re x; Re x < 1; is_imag y; 0 ≤ Im y; Im y < 1⟧ ⟹ P 0⇩h (of_complex x) (of_complex y)"
  assumes moebius: "⋀ M u v w. ⟦unit_disc_fix M; u ∈ unit_disc; v ∈ unit_disc; w ∈ unit_disc; P (moebius_pt M u) (moebius_pt M v) (moebius_pt M w) ⟧ ⟹ P u v w"
  assumes conjugate: "⋀ u v w. ⟦u ∈ unit_disc; v ∈ unit_disc; w ∈ unit_disc; P (conjugate u) (conjugate v) (conjugate w) ⟧ ⟹ P u v w"
  shows "P z u v"
proof-
  have "∀ v H1 H2. is_poincare_line H1 ∧ is_poincare_line H2 ∧ perpendicular H1 H2 ∧
                   z ∈ circline_set H1 ∩ circline_set H2 ∧ u ∈ circline_set H1 ∧ v ∈ circline_set H2 ∧ v ∈ unit_disc ⟶ P z u v" (is "?P z u")
  proof (rule wlog_x_axis[where P="?P"])
    fix x
    assume x: "is_real x" "Re x ≥ 0" "Re x < 1"
    have "of_complex x ∈ unit_disc"
      using x
      by (simp add: cmod_eq_Re)

    show "?P 0⇩h (of_complex x)"
    proof safe
      fix v H1 H2
      assume "v ∈ unit_disc"
      then obtain y where y: "v = of_complex y"
        using inf_or_of_complex[of v]
        by auto

      assume 1: "is_poincare_line H1" "is_poincare_line H2" "perpendicular H1 H2"
      assume 2: "0⇩h ∈ circline_set H1" "0⇩h ∈ circline_set H2" "of_complex x ∈ circline_set H1" "v ∈ circline_set H2"

      show "P 0⇩h (of_complex x) v"
      proof (cases "of_complex x = 0⇩h")
        case True
        show "P 0⇩h (of_complex x) v"
        proof (cases "v = 0⇩h")
          case True
          thus ?thesis
            using ‹of_complex x = 0⇩h›
            using axes[of 0 0]
            by simp
        next
          case False
          show ?thesis
          proof (rule wlog_rotation_to_positive_y_axis)
            show "v ∈ unit_disc" "v ≠ 0⇩h"
              by fact+
          next
            fix y
            assume "is_imag y" "0 < Im y" "Im y < 1"
            thus "P 0⇩h (of_complex x) (of_complex y)"
              using x axes[of x y]
              by simp
          next
            fix φ u
            assume "u ∈ unit_disc" "u ≠ 0⇩h"
                   "P 0⇩h (of_complex x) (moebius_pt (moebius_rotation φ) u)"
            thus "P 0⇩h (of_complex x) u"
              using ‹of_complex x = 0⇩h›
              using moebius[of "moebius_rotation φ"  "0⇩h" "0⇩h" u]
              by simp
          qed
        qed
      next
        case False
        hence *: "poincare_line 0⇩h (of_complex x) = x_axis"
          using x poincare_line_0_real_is_x_axis[of "of_complex x"]
          unfolding circline_set_x_axis
          by auto
        hence "H1 = x_axis"
          using unique_poincare_line[of "0⇩h" "of_complex x" H1] 1 2
          using ‹of_complex x ∈ unit_disc› False
          by simp
        have "is_imag y"
        proof (cases "y = 0")
          case True
          thus ?thesis
            by simp
        next
          case False
          hence "0⇩h ≠ of_complex y"
            using of_complex_zero_iff[of y]
            by metis
          hence "H2 = poincare_line 0⇩h (of_complex y)"
            using 1 2 ‹v ∈ unit_disc›
            using unique_poincare_line[of "0⇩h" "of_complex y" H2] y
            by simp
          thus ?thesis
            using 1 ‹H1 = x_axis›
            using perpendicular_to_x_axis_y_axis[of y] False
            using perpendicular_to_x_axis[of H2]
            by simp
        qed
        show "P 0⇩h (of_complex x) v"
        proof (cases "Im y ≥ 0")
          case True
          thus ?thesis
            using axes[of x y] x y ‹is_imag y› ‹v ∈ unit_disc›
            by (simp add: cmod_eq_Im)
        next
          case False
          show ?thesis
          proof (rule conjugate)
            have "Im (cnj y) < 1"
              using ‹v ∈ unit_disc› y ‹is_imag y› eq_minus_cnj_iff_imag[of y]
              by (simp add: cmod_eq_Im)
            thus "P (conjugate 0⇩h) (conjugate (of_complex x)) (conjugate v)"
              using ‹is_real x› eq_cnj_iff_real[of x] y ‹is_imag y›
              using axes[OF x, of "cnj y"] False
              by simp
            show "0⇩h ∈ unit_disc" "of_complex x ∈ unit_disc" "v ∈ unit_disc"
              by (simp, fact+)
          qed
        qed
      qed
    qed
  next
    show "z ∈ unit_disc" "u ∈ unit_disc"
      by fact+
  next
    fix M u v
    assume *: "unit_disc_fix M" "u ∈ unit_disc" "v ∈ unit_disc"
    assume **: "?P (moebius_pt M u) (moebius_pt M v)"
    show "?P u v"
    proof safe
      fix w H1 H2
      assume ***: "is_poincare_line H1" "is_poincare_line H2" "perpendicular H1 H2"
                  "u ∈ circline_set H1" "u ∈ circline_set H2"
                  "v ∈ circline_set H1" "w ∈ circline_set H2" "w ∈ unit_disc"
      thus "P u v w"
        using moebius[of M u v w] *
        using **[rule_format, of "moebius_circline M H1" "moebius_circline M H2" "moebius_pt M w"]
        by simp
    qed
  qed
  thus ?thesis
    using assms
    by blast
qed

lemma wlog_perpendicular_foot:
  assumes in_disc: "u ∈ unit_disc" "v ∈ unit_disc" "w ∈ unit_disc" "z ∈ unit_disc"
  assumes perpendicular: "u ≠ v" "is_poincare_line H" "perpendicular (poincare_line u v) H"
  assumes "z ∈ circline_set (poincare_line u v) ∩ circline_set H" "w ∈ circline_set H"
  assumes axes: "⋀ u v w. ⟦is_real u; 0 < Re u; Re u < 1; is_real v; -1 < Re v; Re v < 1; Re u ≠ Re v; is_imag w; 0 ≤ Im w; Im w < 1⟧ ⟹ P 0⇩h (of_complex u) (of_complex v) (of_complex w)"
  assumes moebius: "⋀ M z u v w. ⟦unit_disc_fix M; u ∈ unit_disc; v ∈ unit_disc; w ∈ unit_disc; z ∈ unit_disc; P (moebius_pt M z) (moebius_pt M u) (moebius_pt M v) (moebius_pt M w) ⟧ ⟹ P z u v w"
  assumes conjugate: "⋀ z u v w. ⟦u ∈ unit_disc; v ∈ unit_disc; w ∈ unit_disc; P (conjugate z) (conjugate u) (conjugate v) (conjugate w) ⟧ ⟹ P z u v w"
  assumes perm: "P z v u w ⟹ P z u v w"
  shows "P z u v w"
proof-
  obtain m n where mn: "m = u ∨ m = v" "n = u ∨ n = v" "m ≠ n" "m ≠ z"
    using ‹u ≠ v›
    by auto

  have "n ∈ circline_set (poincare_line z m)"
    using ‹z ∈ circline_set (poincare_line u v) ∩ circline_set H›
    using mn
    using unique_poincare_line[of z m "poincare_line u v", symmetric] in_disc
    by auto

  have "∀ n. n ∈ unit_disc ∧ m ≠ n ∧ n ∈ circline_set (poincare_line z m) ∧ m ≠ z ⟶ P z m n w" (is "?Q z m w")
  proof (rule wlog_perpendicular_axes[where P="?Q"])
    show "is_poincare_line (poincare_line u v)"
      using ‹u ≠ v›
      by auto
  next
    show "is_poincare_line H"
      by fact
  next
    show "m ∈ unit_disc" "m ∈ circline_set (poincare_line u v)"
      using mn in_disc
      by auto
  next
    show "w ∈ unit_disc" "z ∈ unit_disc"
      by fact+
  next
    show "z ∈ circline_set (poincare_line u v) ∩ circline_set H"
      by fact
  next
    show "perpendicular (poincare_line u v) H"
      by fact
  next
    show "w ∈ circline_set H"
      by fact
  next
    fix x y
    assume xy: "is_real x" "0 ≤ Re x" "Re x < 1" "is_imag y" "0 ≤ Im y" "Im y < 1"
    show "?Q 0⇩h (of_complex x) (of_complex y)"
    proof safe
      fix n
      assume "n ∈ unit_disc" "of_complex x ≠ n"
      assume "n ∈ circline_set (poincare_line 0⇩h (of_complex x))" "of_complex x ≠ 0⇩h"
      hence "n ∈ circline_set x_axis"
        using poincare_line_0_real_is_x_axis[of "of_complex x"] xy
        by (auto simp add: circline_set_x_axis)
      then obtain n' where n': "n = of_complex n'"
        using inf_or_of_complex[of n] ‹n ∈ unit_disc›
        by auto
      hence "is_real n'"
        using ‹n ∈ circline_set x_axis›
        using of_complex_inj
        unfolding circline_set_x_axis
        by auto
      hence "-1 < Re n'" "Re n' < 1"
        using ‹n ∈ unit_disc› n'
        by (auto simp add: cmod_eq_Re)

      have "Re n' ≠ Re x"
        using complex.expand[of n' x] ‹is_real n'› ‹is_real x› ‹of_complex x ≠ n› n'
        by auto

      have "Re x > 0"
        using xy ‹of_complex x ≠ 0⇩h›
        by (cases "Re x = 0", auto simp add: complex.expand)

      show "P 0⇩h (of_complex x) n (of_complex y)"
        using axes[of x n' y] xy n' ‹Re x > 0› ‹is_real n'› ‹-1 < Re n'› ‹Re n' < 1› ‹Re n' ≠ Re x›
        by simp
    qed
  next
    fix M u v w
    assume 1: "unit_disc_fix M" "u ∈ unit_disc" "v ∈ unit_disc" "w ∈ unit_disc"
    assume 2: "?Q (moebius_pt M u) (moebius_pt M v) (moebius_pt M w)"
    show "?Q u v w"
    proof safe
      fix n
      assume "n ∈ unit_disc" "v ≠ n" "n ∈ circline_set (poincare_line u v)" "v ≠ u"
      thus "P u v n w"
        using moebius[of M v n w u] 1 2[rule_format, of "moebius_pt M n"]
        by fastforce
    qed
  next
    fix u v w
    assume 1: "u ∈ unit_disc" "v ∈ unit_disc" "w ∈ unit_disc"
    assume 2: "?Q (conjugate u) (conjugate v) (conjugate w)"
    show "?Q u v w"
    proof safe
      fix n
      assume "n ∈ unit_disc" "v ≠ n" "n ∈ circline_set (poincare_line u v)" "v ≠ u"
      thus "P u v n w"
        using conjugate[of v n w u] 1 2[rule_format, of "conjugate n"]
        using conjugate_inj
        by auto
    qed
  qed
  thus ?thesis
    using mn in_disc ‹n ∈ circline_set (poincare_line z m)› perm
    by auto
qed

lemma perpendicular_to_x_axis_intersects_x_axis:
  assumes "is_poincare_line H" "perpendicular_to_x_axis H"
  shows "intersects_x_axis H"
  using assms hermitean_elems
  by (transfer, transfer, auto simp add: cmod_eq_Re)


lemma perpendicular_intersects:
  assumes "is_poincare_line H1" "is_poincare_line H2"
  assumes "perpendicular H1 H2"
  shows "∃ z. z ∈ unit_disc ∧ z ∈ circline_set H1 ∩ circline_set H2" (is "?P' H1 H2")
proof-
  have "∀ H2. is_poincare_line H2 ∧ perpendicular H1 H2 ⟶ ?P' H1 H2" (is "?P H1")
  proof (rule wlog_line_x_axis)
    show "?P x_axis"
    proof safe
      fix H2
      assume "is_poincare_line H2" "perpendicular x_axis H2"
      thus "∃z. z ∈ unit_disc ∧ z ∈ circline_set x_axis ∩ circline_set H2"
        using perpendicular_to_x_axis[of H2]
        using perpendicular_to_x_axis_intersects_x_axis[of H2]
        using intersects_x_axis_iff[of H2]
        by auto
    qed
  next
    fix M
    assume "unit_disc_fix M"
    assume *: "?P (moebius_circline M H1)"
    show "?P H1"
    proof safe
      fix H2
      assume "is_poincare_line H2" "perpendicular H1 H2"
      then obtain z where "z ∈ unit_disc" "z ∈ circline_set (moebius_circline M H1) ∧ z ∈ circline_set (moebius_circline M H2)"
        using *[rule_format, of "moebius_circline M H2"] ‹unit_disc_fix M›
        by auto
      thus "∃z. z ∈ unit_disc ∧ z ∈ circline_set H1 ∩ circline_set H2"
        using ‹unit_disc_fix M›
        by (rule_tac x="moebius_pt (-M) z" in exI)
           (metis IntI add.inverse_inverse circline_set_moebius_circline_iff moebius_pt_comp_inv_left uminus_moebius_def unit_disc_fix_discI unit_disc_fix_moebius_uminus)
    qed
  next
    show "is_poincare_line H1"
      by fact
  qed
  thus ?thesis
    using assms
    by auto
qed


definition calc_perpendicular_to_x_axis_cmat :: "complex_vec ⇒ complex_mat" where
 [simp]: "calc_perpendicular_to_x_axis_cmat z =
     (let (z1, z2) = z
       in if z1*cnj z2 + z2*cnj z1 = 0 then
          (0, 1, 1, 0)
       else
          let A = z1*cnj z2 + z2*cnj z1;
              B = -(z1*cnj z1 + z2*cnj z2)
           in (A, B, B, A)
     )"

lift_definition calc_perpendicular_to_x_axis_clmat :: "complex_homo_coords ⇒ circline_mat" is calc_perpendicular_to_x_axis_cmat
  by (auto simp add: hermitean_def mat_adj_def mat_cnj_def Let_def split: if_split_asm)

lift_definition calc_perpendicular_to_x_axis :: "complex_homo ⇒ circline" is calc_perpendicular_to_x_axis_clmat
proof (transfer)
  fix z w
  assume "z ≠ vec_zero" "w ≠ vec_zero"
  obtain z1 z2 w1 w2 where zw: "z = (z1, z2)" "w = (w1, w2)"
    by (cases z, cases w, auto)
  assume "z ≈⇩v w"
  then obtain k where *: "k ≠ 0" "w1 = k*z1" "w2 = k*z2"
    using zw
    by auto
  have "w1 * cnj w2 + w2 * cnj w1 = (k * cnj k) * (z1 * cnj z2 + z2 * cnj z1)"
    using *
    by (auto simp add: field_simps)
  moreover
  have "w1 * cnj w1 + w2 * cnj w2 = (k * cnj k) * (z1 * cnj z1 + z2 * cnj z2)"
    using *
    by (auto simp add: field_simps)
  ultimately
  show "circline_eq_cmat (calc_perpendicular_to_x_axis_cmat z) (calc_perpendicular_to_x_axis_cmat w)"
    using zw *
    apply (auto simp add: Let_def)
    apply (rule_tac x="Re (k * cnj k)" in exI, auto simp add: complex.expand field_simps)
    done
qed

lemma calc_perpendicular_to_x_axis:
  assumes "z ≠ of_complex 1" "z ≠ of_complex (-1)"
  shows "z ∈ circline_set (calc_perpendicular_to_x_axis z) ∧
         is_poincare_line (calc_perpendicular_to_x_axis z) ∧
         perpendicular_to_x_axis (calc_perpendicular_to_x_axis z)"
  using assms
  unfolding circline_set_def perpendicular_def
proof (simp, transfer, transfer)
  fix z :: complex_vec
  obtain z1 z2 where z: "z = (z1, z2)"
    by (cases z, auto)
  assume **: "¬ z ≈⇩v of_complex_cvec 1" "¬ z ≈⇩v of_complex_cvec (- 1)"
  show "on_circline_cmat_cvec (calc_perpendicular_to_x_axis_cmat z) z ∧
        is_poincare_line_cmat (calc_perpendicular_to_x_axis_cmat z) ∧
        perpendicular_to_x_axis_cmat (calc_perpendicular_to_x_axis_cmat z)"
  proof (cases "z1*cnj z2 + z2*cnj z1 = 0")
    case True
    thus ?thesis
      using z
      by (simp add: vec_cnj_def hermitean_def mat_adj_def mat_cnj_def mult.commute)
  next
    case False
    hence "z2 ≠ 0"
      using z
      by auto
    hence "Re (z2 * cnj z2) ≠ 0"
      using ‹z2 ≠ 0›
      by (auto simp add: complex.expand)

    have "z1 ≠ -z2 ∧ z1 ≠ z2"
    proof (rule ccontr)
      assume "¬ ?thesis"
      hence "z ≈⇩v of_complex_cvec 1 ∨ z ≈⇩v of_complex_cvec (-1)"
        using z ‹z2 ≠ 0›
        by auto
      thus False
        using **
        by auto
    qed

    let ?A = "z1*cnj z2 + z2*cnj z1" and ?B = "-(z1*cnj z1 + z2*cnj z2)"
    have "Re(z1*cnj z1 + z2*cnj z2) ≥ 0"
      by auto
    hence "Re ?B ≤ 0"
      by (smt uminus_complex.simps(1))
    hence "abs (Re ?B) = - Re ?B"
      by auto
    also have "... = (Re z1)⇧2 + (Im z1)⇧2 + (Re z2)⇧2 + (Im z2)⇧2"
      by (simp add: power2_eq_square[symmetric])
    also have "... > abs (Re ?A)"
    proof (cases "Re ?A ≥ 0")
      case False
      have "(Re z1 + Re z2)⇧2 + (Im z1 + Im z2)⇧2 > 0"
        using ‹z1 ≠ -z2 ∧ z1 ≠ z2›
        by (metis add.commute add.inverse_unique complex_neq_0 plus_complex.code plus_complex.simps)
      thus ?thesis
        using False
        by (simp add: power2_sum power2_eq_square field_simps)
    next
      case True
      have "(Re z1 - Re z2)⇧2 + (Im z1 - Im z2)⇧2 > 0"
        using ‹z1 ≠ -z2 ∧ z1 ≠ z2›
        by (meson complex_eq_iff right_minus_eq sum_power2_gt_zero_iff)
      thus ?thesis
        using True
        by (simp add: power2_sum power2_eq_square field_simps)
    qed
    finally
    have "abs (Re ?B) > abs (Re ?A)"
      .
    moreover
    have "cmod ?B = abs (Re ?B)" "cmod ?A = abs (Re ?A)"
      by (simp_all add: cmod_eq_Re)
    ultimately
    have "(cmod ?B)⇧2 > (cmod ?A)⇧2"
      by (smt power2_le_imp_le)
    thus ?thesis
      using z False
      by (simp_all add: Let_def hermitean_def mat_adj_def mat_cnj_def cmod_eq_Re vec_cnj_def field_simps)
  qed
qed

lemma ex_perpendicular:
  assumes "is_poincare_line H" "z ∈ unit_disc"
  shows "∃ H'. is_poincare_line H' ∧ perpendicular H H' ∧ z ∈ circline_set H'" (is "?P' H z")
proof-
  have "∀ z. z ∈ unit_disc ⟶ ?P' H z" (is "?P H")
  proof (rule wlog_line_x_axis)
    show "?P x_axis"
    proof safe
      fix z
      assume "z ∈ unit_disc"
      then have "z ≠ of_complex 1" "z ≠ of_complex (-1)"
        by auto
      thus "?P' x_axis z"
        using ‹z ∈ unit_disc›
        using calc_perpendicular_to_x_axis[of z] perpendicular_to_x_axis
        by (rule_tac x = "calc_perpendicular_to_x_axis z" in exI, auto)
    qed
  next
    fix M
    assume "unit_disc_fix M"
    assume *: "?P (moebius_circline M H)"
    show "?P H"
    proof safe
      fix z
      assume "z ∈ unit_disc"
      hence "moebius_pt M z ∈ unit_disc"
        using ‹unit_disc_fix M›
        by auto
      then obtain H' where *: "is_poincare_line H'" "perpendicular (moebius_circline M H) H'" "moebius_pt M z ∈ circline_set H'"
        using *
        by auto
      have h: "H = moebius_circline (-M) (moebius_circline M H)"   
        by auto
      show "?P' H z"
        using * ‹unit_disc_fix M›
        apply (subst h)
        apply (rule_tac x="moebius_circline (-M) H'" in exI)
        apply (simp del: moebius_circline_comp_inv_left)
        done
    qed
  qed fact
  thus ?thesis
    using assms
    by simp
qed

lemma ex_perpendicular_foot:
  assumes "is_poincare_line H" "z ∈ unit_disc"
  shows "∃ H'. is_poincare_line H' ∧ z ∈ circline_set H' ∧ perpendicular H H' ∧
              (∃ z' ∈ unit_disc. z' ∈ circline_set H' ∩ circline_set H)"
  using assms
  using ex_perpendicular[OF assms]
  using perpendicular_intersects[of H]
  by blast

lemma Pythagoras:
  assumes in_disc: "u ∈ unit_disc" "v ∈ unit_disc" "w ∈ unit_disc" "v ≠ w"
  assumes "distinct[u, v, w] ⟶ perpendicular (poincare_line u v) (poincare_line u w)"
  shows "cosh (poincare_distance v w) = cosh (poincare_distance u v) * cosh (poincare_distance u w)" (is "?P' u v w")
proof (cases "distinct [u, v, w]")
  case False
  thus "?thesis"
    using in_disc
    by (auto simp add: poincare_distance_sym)
next
  case True
  have "distinct [u, v, w] ⟶ ?P' u v w" (is "?P u v w")
  proof (rule wlog_perpendicular_axes[where P="?P"])
    show "is_poincare_line (poincare_line u v)" "is_poincare_line (poincare_line u w)"
      using ‹distinct [u, v, w]›
      by simp_all
  next
    show "perpendicular (poincare_line u v) (poincare_line u w)"
      using True assms
      by simp
  next
    show "u ∈ unit_disc" "v ∈ unit_disc" "w ∈ unit_disc"
      by fact+
  next
    show "v ∈ circline_set (poincare_line u v)" "w ∈ circline_set (poincare_line u w)"
         "u ∈ circline_set (poincare_line u v) ∩ circline_set (poincare_line u w)"
      using ‹distinct [u, v, w]›
      by auto
  next
    fix x y
    assume x: "is_real x" "0 ≤ Re x" "Re x < 1"
    assume y: "is_imag y" "0 ≤ Im y" "Im y < 1"

    have "of_complex x ∈ unit_disc" "of_complex y ∈ unit_disc"
      using x y
      by (simp_all add: cmod_eq_Re cmod_eq_Im)

    show "?P 0⇩h (of_complex x) (of_complex y)"
    proof
      assume "distinct [0⇩h, of_complex x, of_complex y]"
      hence "x ≠ 0" "y ≠ 0"
        by auto

      let ?den1 = "1 - (cmod x)⇧2" and ?den2 = "1 - (cmod y)⇧2"
      have "?den1 > 0" "?den2 > 0"
        using x y
        by (simp_all add: cmod_eq_Re cmod_eq_Im abs_square_less_1)

      let ?d1 = "1 + 2 * (cmod x)⇧2 / ?den1"
      have "cosh (poincare_distance 0⇩h (of_complex x)) = ?d1"
        using ‹?den1 > 0›
        using poincare_distance_formula[of "0⇩h" "of_complex x"] ‹of_complex x ∈ unit_disc›
        by simp

      moreover

      let ?d2 = "1 + 2 * (cmod y)⇧2 / ?den2"
      have "cosh (poincare_distance 0⇩h (of_complex y)) = ?d2"
        using ‹?den2 > 0› ‹of_complex y ∈ unit_disc›
        using poincare_distance_formula[of "0⇩h" "of_complex y"]
        by simp

      moreover
      let ?den = "?den1 * ?den2"
      let ?d3 = "1 + 2 * (cmod (x - y))⇧2 / ?den"
      have "cosh (poincare_distance (of_complex x) (of_complex y)) = ?d3"
        using ‹of_complex x ∈ unit_disc› ‹of_complex y ∈ unit_disc›
        using ‹?den1 > 0› ‹?den2 > 0›
        using poincare_distance_formula[of "of_complex x" "of_complex y"]
        by simp
      moreover
      have "?d1 * ?d2 = ?d3"
      proof-
        have "?d3 = ((1 - (cmod x)⇧2) * (1 - (cmod y)⇧2) + 2 * (cmod (x - y))⇧2) / ?den"
          using ‹?den1 > 0› ‹?den2 > 0›
          by (subst add_num_frac, simp, simp)
        also have "... = (Re ((1 - x * cnj x) * (1 - y * cnj y) + 2 * (x - y)*cnj (x - y)) / ?den)"
          using ‹is_real x› ‹is_imag y›
          by ((subst cmod_square)+, simp)
        also have "... = Re (1 + x * cnj x * y * cnj y
                               + x * cnj x - 2 * y * cnj x - 2 * x * cnj y + y * cnj y) / ?den"
          by (simp add: field_simps)
        also have "... = Re ((1 + y * cnj y) * (1 + x * cnj x)) / ?den"
          using ‹is_real x› ‹is_imag y›
          by (simp add: field_simps)
        finally
        show ?thesis
          using ‹?den1 > 0› ‹?den2 > 0›
          apply (subst add_num_frac, simp)
          apply (subst add_num_frac, simp)
          apply simp
          apply (subst cmod_square)+
          apply (simp add: field_simps)
          done
      qed
      ultimately
      show "?P' 0⇩h (of_complex x) (of_complex y)"
        by simp
    qed
  next
    fix M u v w
    assume 1: "unit_disc_fix M" "u ∈ unit_disc" "v ∈ unit_disc" "w ∈ unit_disc"
    assume 2: "?P (moebius_pt M u) (moebius_pt M v) (moebius_pt M w)"
    show "?P u v w"
      using 1 2
      by auto
  next
    fix u v w
    assume 1:  "u ∈ unit_disc" "v ∈ unit_disc" "w ∈ unit_disc"
    assume 2: "?P (conjugate u) (conjugate v) (conjugate w)"
    show "?P u v w"
      using 1 2
      by (auto simp add: conjugate_inj)
  qed
  thus ?thesis
    using True
    by simp
qed

end