Theory MobiusGeometry

theory MobiusGeometry
  imports MobiusGyroVectorSpace
begin

lemma mobius_collinear_u0v':
  assumes "v ≠ 0⇩m"
  shows "Mobius_pre_gyrovector_space.collinear u 0⇩m v ⟷ (∃ k::real. to_complex u = k * (to_complex v))"
  unfolding Mobius_pre_gyrovector_space.collinear_def gyroplus_PoincareDisc_def gyroinv_PoincareDisc_def
  using assms
proof transfer
  fix v u
  assume "cmod v < 1" "cmod u < 1" "v ≠ ozero_m'"
  then have "v ≠ 0"
    unfolding ozero_m'_def
    by simp
  have "(∃t. u = (otimes'_k t v) * v / cor (cmod v)) ⟷ (∃k :: real. u = k * v)" (is "?lhs ⟷ ?rhs")
  proof
    assume ?lhs
    then show ?rhs
      by (metis of_real_divide times_divide_eq_left)
  next
    assume ?rhs
    then obtain k::real where "u = k * v"
      by auto

    moreover

    have "abs (k * cmod v) < 1"
      by (metis ‹cmod u < 1› ‹u = cor k * v› abs_mult abs_norm_cancel norm_mult norm_of_real)

    have "artanh (cmod v) ≠ 0"
      using ‹v ≠ 0›
      by (simp add: ‹cmod v < 1› artanh_not_0)
    
    have "∃ t. (otimes'_k t v) / (cmod v) = k"
    proof-
      let ?t = "artanh(k * cmod v) / artanh (cmod v)"
      have "tanh (?t * artanh (cmod v)) = k * cmod v"
        using ‹artanh (cmod v) ≠ 0› tanh_artanh[of "k * cmod v"] ‹abs (k * cmod v) < 1›
        by (simp add: field_simps)
      then show ?thesis
        by (metis ‹cmod v < 1› ‹v ≠ 0› nonzero_mult_div_cancel_right norm_zero otimes'_k_tanh zero_less_norm_iff)
    qed
    ultimately
    show ?lhs
      by auto
  qed
  then show "(ozero_m' = v ∨ (∃t. u = oplus_m' ozero_m' (otimes' t (oplus_m' (ominus_m' ozero_m') v)))) ⟷
        (∃ k::real. u = k * v)"
    using ‹v ≠ 0›
    unfolding oplus_m'_def ozero_m'_def ominus_m'_def otimes'_def
    by simp
qed

lemma mobius_collinear_u0v:
  shows "Mobius_pre_gyrovector_space.collinear x 0⇩m v ⟷ 
         v = 0⇩m ∨ (∃ k::real. to_complex x = k * (to_complex v))"
  by (metis Mobius_pre_gyrovector_space.collinear_def mobius_collinear_u0v')

lemma mobius_between_0uv:
  shows "Mobius_pre_gyrovector_space.between 0⇩m u v ⟷ 
         (∃ k::real. 0 ≤ k ∧ k ≤ 1 ∧ to_complex u = k * to_complex v)"
proof (cases "v = 0⇩m")
  case True
  then show ?thesis
    using Mobius_pre_gyrovector_space.between_xyx[of "0⇩m" u]
    by auto
next
  case False
  then show ?thesis
    unfolding Mobius_pre_gyrovector_space.between_def gyroplus_PoincareDisc_def gyrozero_PoincareDisc_def gyroinv_PoincareDisc_def
  proof (transfer)
    fix x y
    assume "cmod y < 1" "y ≠ ozero_m'" "cmod x < 1"
    then have "y ≠ 0"
      by (simp add: ozero_m'_def)

    have "(∃t≥0. t ≤ 1 ∧ x = cor (otimes'_k t y) * y / cor (cmod y)) =
          (∃k≥0. k ≤ 1 ∧ x = cor k * y)" (is "?lhs = ?rhs")
    proof
      assume ?lhs
      then obtain t where "0 ≤ t" "t ≤ 1" "x = (otimes'_k t y / cmod y) * y"
        by auto
      moreover
      have "0 ≤ otimes'_k t y / cmod y" 
        unfolding otimes'_k_tanh[OF ‹cmod y < 1›]
        using ‹cmod y < 1› ‹t ≥ 0› tanh_artanh_nonneg 
        by auto
      moreover
      have "otimes'_k t y / cmod y ≤ 1"
        unfolding otimes'_k_tanh[OF ‹cmod y < 1›]
        using ‹cmod y < 1› ‹y ≠ 0› artanh_nonneg ‹t ≤ 1›
        by (smt (verit, best) divide_le_eq_1 mult_le_cancel_right2 norm_le_zero_iff strict_mono_less_eq tanh_artanh tanh_real_strict_mono)
      ultimately
      show ?rhs
        by auto
    next
      assume ?rhs
      then obtain k::real where "x = k * y"
        by auto

      moreover

      have "abs (k * cmod y) < 1"
        by (metis ‹cmod x < 1› ‹x = cor k * y› abs_mult abs_norm_cancel norm_mult norm_of_real)

      have "artanh (cmod y) ≠ 0"
        using ‹y ≠ 0›
        by (simp add: ‹cmod y < 1› artanh_not_0)
    
      have "∃ t. 0 ≤ t ∧ t ≤ 1 ∧ (otimes'_k t y) / (cmod y) = k"
      proof-
        let ?t = "artanh(k * cmod y) / artanh (cmod y)"
        have "tanh (?t * artanh (cmod y)) = k * cmod y"
          using ‹artanh (cmod y) ≠ 0› tanh_artanh[of "k * cmod y"] ‹abs (k * cmod y) < 1›
          by (simp add: field_simps)
        moreover
        have "?t ≥ 0"
          using ‹∃k≥0. k ≤ 1 ∧ x = cor k * y› ‹cmod y < 1› ‹x = cor k * y› ‹y ≠ 0›
          by (smt (verit, ccfv_SIG)  artanh_nonneg calculation divide_eq_0_iff mult_right_cancel norm_le_zero_iff of_real_eq_iff tanh_real_nonneg_iff zero_le_mult_iff)
        moreover
        have "?t ≤ 1"
          using ‹∃k≥0. k ≤ 1 ∧ x = cor k * y› ‹cmod y < 1› ‹x = cor k * y› ‹y ≠ 0›
          by (smt (verit, ccfv_SIG)  artanh_monotone artanh_nonneg calculation(1) less_divide_eq_1 nonzero_divide_eq_eq of_real_eq_iff tanh_artanh_nonneg zero_less_norm_iff)
        ultimately show ?thesis
          by (metis ‹cmod y < 1› ‹y ≠ 0› nonzero_mult_div_cancel_right norm_zero otimes'_k_tanh zero_less_norm_iff)
      qed
      ultimately
      show ?lhs
        by auto
    qed
    then show "(∃t≥0. t ≤ 1 ∧
                       x = oplus_m' ozero_m' (otimes' t (oplus_m' (ominus_m' ozero_m') y))) =
               (∃k≥0. k ≤ 1 ∧ x = cor k * y)"
      using ‹y ≠ 0›
      unfolding ozero_m'_def oplus_m'_def ominus_m'_def otimes'_def
      by simp
  qed
qed

(* ------------------------------------------------------------------- *)

abbreviation distance_m_expr :: "complex ⇒ complex ⇒ real" where
  "distance_m_expr u v ≡ 1 + 2 * (cmod (u - v))⇧2 / ((1 - (cmod u)⇧2) * (1 - (cmod v)⇧2))"

definition distance_m :: "complex ⇒ complex ⇒ real" where 
  "distance_m u v = arcosh (distance_m_expr u v)"

lemma arcosh_artanh_lemma:
  shows "(cmod (1 - cnj u * v))⇧2 - (cmod (u - v))⇧2 = (1 - (cmod u)⇧2) * (1 - (cmod v)⇧2)"
proof-
  have "cor ((cmod (1 - cnj u * v))⇧2 - (cmod (u - v))⇧2) = cor ((1 - (cmod u)⇧2) * (1 - (cmod v)⇧2))"
    unfolding of_real_diff of_real_mult complex_norm_square
    by (simp add: field_simps)
  then show ?thesis
    using of_real_eq_iff by blast
qed

lemma distance_m_expr_ge_1:
  fixes u v :: complex
  assumes "cmod u < 1" "cmod v < 1"
  shows "distance_m_expr u v ≥ 1"
proof-
  have "(cmod (u-v))⇧2 ≥ 0"
    using zero_le_power2 by blast
  moreover
  have "(1 - (cmod u)⇧2) *(1 - (cmod v)⇧2) > 0"
    using assms
    using cmod_def by force
  ultimately 
  show ?thesis
    by simp
qed

lemma arcosh_artanh:
  fixes u v :: complex
  assumes "cmod u <1" "cmod v < 1"
  shows "arcosh (distance_m_expr u v) =
         2 * artanh (cmod ((u-v) / (1 - (cnj u)*v)))"
proof-
  let ?u = "1 - (cmod u)⇧2" and ?v = "1 - (cmod v)⇧2" and ?uv = "(cmod (u - v))⇧2"

  have "arcosh (distance_m_expr u v) =
        ln (distance_m_expr u v + sqrt ((distance_m_expr u v)⇧2 - 1))"
    using arcosh_real_def[OF distance_m_expr_ge_1[OF assms]]
    by simp
  also have "… = ln (((cmod (1 - cnj u * v))⇧2 + 2 * cmod (1 - cnj u * v) * cmod (u - v) + ?uv) /
                      (?u * ?v))"
  proof-
    have "distance_m_expr u v = (?u * ?v + 2 * ?uv) / (?u * ?v)"
    proof-
      have "?u ≠ 0" "?v ≠ 0"
        using assms
        by (metis abs_norm_cancel order_less_irrefl real_sqrt_abs real_sqrt_one right_minus_eq)+  
      then show ?thesis 
        by (simp add: add_divide_distrib)
    qed
    then have *: "distance_m_expr u v = ((cmod (1 - cnj u * v))⇧2 + ?uv) / (?u * ?v)"
      using assms 
      by (smt (verit, ccfv_SIG) arcosh_artanh_lemma)
   
    have "sqrt ((distance_m_expr u v)⇧2 - 1) =
          sqrt (4 * (?uv / (?u * ?v)) + 4 * (?uv / (?u * ?v))⇧2)"
      by (smt (verit, best) add_divide_distrib four_x_squared inner_real_def one_power2 power2_diff real_inner_1_right)
    also have "… = sqrt (4 * ?uv * (1 / (?u * ?v) + (cmod (u - v) / (?u * ?v))⇧2))" (is "?lhs = sqrt (4 * ?A * ?B)")
      by (simp add: field_simps)
    also have "… = sqrt (4 * ?uv * (?u * ?v + ?uv) / (?u * ?v)⇧2)"
    proof-
      have "?B = (?u * ?v + ?uv) / (?u * ?v)⇧2"
        by (simp add: power_divide power2_eq_square add_divide_distrib)
      then show ?thesis
        by simp
    qed
    also have "… = 2 * cmod (u - v) * sqrt (?u * ?v + ?uv) / (?u * ?v)"
      using assms
      by (smt (verit, ccfv_SIG) four_x_squared mult_nonneg_nonneg norm_not_less_zero one_power2 power_mono real_root_divide real_root_mult real_sqrt_unique sqrt_def)
    also have "... = 2 * cmod (u - v) / (?u * ?v) * sqrt (?u * ?v + ?uv)"
      by simp
    finally have **: "sqrt ((distance_m_expr u v)⇧2 - 1) =  
                      2 * cmod (u - v) * cmod (1 - cnj u * v) / (?u * ?v)"
      by (smt (verit, del_insts) arcosh_artanh_lemma norm_ge_zero real_sqrt_abs times_divide_eq_left)

    show ?thesis
      using * **
      by (smt (verit, best) add_divide_distrib power2_sum)
  qed
  also have "… = ln ((1 + cmod (u - v) / cmod (1 - cnj u * v)) /
                      (1 - cmod (u - v) / cmod (1 - cnj u * v)))" (is "?lhs = ln (?nom / ?den)")
  proof-
    have *: "?nom = (cmod (u - v) + cmod (1 - cnj u * v)) / cmod (1 - cnj u * v)"
      using assms
      by (metis (no_types, opaque_lifting) add_diff_cancel_left' add_divide_distrib complex_mod_cnj diff_diff_eq2 diff_zero divide_self_if mult_closed_for_unit_disc norm_eq_zero norm_one order_less_irrefl)
    then have **: "?den = (cmod (1 - cnj u * v) - cmod (u - v)) / cmod (1 - cnj u * v)"
      using assms
      by (smt (verit, ccfv_SIG) add_divide_distrib)
    have "?nom / ?den =
          (cmod (u - v) + cmod (1 - cnj u * v)) / (cmod (1 - cnj u * v) - cmod (u - v))"
      using * **
      by force
    also have "… = (cmod (1 - cnj u * v) + cmod (u - v))⇧2 / (?u * ?v)" (is "?lhs = ?rhs")
    proof-
      let ?e = "cmod (1 - cnj u * v) + cmod (u - v)"
      have "?lhs = ?lhs * ?e/?e"
        by fastforce
      moreover
      have "(cmod (1 - cnj u * v) - cmod (u - v)) * ?e = ?u * ?v"
        using arcosh_artanh_lemma
        by (simp add: mult.commute power2_eq_square square_diff_square_factored)
      ultimately
      show ?thesis
        by (simp add: power2_eq_square)
    qed
    finally
    show ?thesis
      by (simp add: power2_eq_square field_simps)
  qed
  finally show ?thesis
    unfolding artanh_def
    by (simp add: norm_divide)
qed

definition distance⇩m :: "PoincareDisc ⇒ PoincareDisc ⇒ real" where
 "distance⇩m u v = 2 * artanh (Mobius_pre_gyrovector_space.distance u v)"

lemma distance⇩m_equiv:
  shows "distance⇩m u v = distance_m (to_complex u) (to_complex v)"
proof-
  have "(⟪⊖⇩m u ⊕⇩m v⟫) =
         (cmod ((to_complex u - to_complex v) / (1 - cnj (to_complex u) * (to_complex v))))"
    by transfer (simp add: oplus_m'_def ominus_m'_def norm_divide norm_minus_commute)
  then show ?thesis
  unfolding distance⇩m_def distance_m_def Mobius_pre_gyrovector_space.distance_def gyroinv_PoincareDisc_def gyroplus_PoincareDisc_def
  using arcosh_artanh norm_lt_one norm_p.rep_eq
  by force
qed

definition cong⇩m :: "PoincareDisc ⇒ PoincareDisc ⇒ PoincareDisc ⇒ PoincareDisc ⇒ bool" where
  "cong⇩m a b c d ⟷ distance⇩m a b = distance⇩m c d"

end