Theory Angles

(* ---------------------------------------------------------------------------- *)
subsection ‹Angle between two vectors›
(* ---------------------------------------------------------------------------- *)

text ‹In this section we introduce different measures of angle between two vectors (represented by complex numbers).›

theory Angles
imports More_Transcendental Canonical_Angle More_Complex
begin

(* ---------------------------------------------------------------------------- *)
subsubsection ‹Oriented angle›
(* ---------------------------------------------------------------------------- *)

text ‹Oriented angle between two vectors (it is always in the interval $(-\pi, \pi]$).›
definition ang_vec ("∠") where
  [simp]: "∠ z1 z2 ≡ ⇂Arg z2 - Arg z1⇃"

lemma ang_vec_bounded:
  shows "-pi < ∠ z1 z2 ∧ ∠ z1 z2 ≤ pi"
  by (simp add: canon_ang(1) canon_ang(2))

lemma ang_vec_sym:
  assumes "∠ z1 z2 ≠ pi"
  shows "∠ z1 z2 = - ∠ z2 z1"
  using assms
  unfolding ang_vec_def
  using canon_ang_uminus[of "Arg z2 - Arg z1"]
  by simp

lemma ang_vec_sym_pi:
  assumes "∠ z1 z2 = pi"
  shows "∠ z1 z2 = ∠ z2 z1"
  using assms
  unfolding ang_vec_def
  using canon_ang_uminus_pi[of "Arg z2 - Arg z1"]
  by simp

lemma ang_vec_plus_pi1:
  assumes "∠ z1 z2 > 0"
  shows "⇂∠ z1 z2 + pi⇃ = ∠ z1 z2 - pi"
proof (rule canon_ang_eqI)
  show "∃ x::int. ∠ z1 z2 - pi - (∠ z1 z2 + pi) = 2 * real_of_int x * pi"
    by (rule_tac x="-1" in exI) auto
next
  show "- pi < ∠ z1 z2 - pi ∧ ∠ z1 z2 - pi ≤ pi"
    using assms
    unfolding ang_vec_def
    using canon_ang(1)[of "Arg z2 - Arg z1"] canon_ang(2)[of "Arg z2 - Arg z1"]
    by auto
qed

lemma ang_vec_plus_pi2:
  assumes "∠ z1 z2 ≤ 0"
  shows "⇂∠ z1 z2 + pi⇃ = ∠ z1 z2 + pi"
proof (rule canon_ang_id)
  show "- pi < ∠ z1 z2 + pi ∧ ∠ z1 z2 + pi ≤ pi"
    using assms
    unfolding ang_vec_def
    using canon_ang(1)[of "Arg z2 - Arg z1"] canon_ang(2)[of "Arg z2 - Arg z1"]
    by auto
qed

lemma ang_vec_opposite1:
  assumes "z1 ≠ 0"
  shows "∠ (-z1) z2 = ⇂∠ z1 z2 - pi⇃"
proof-
  have "∠ (-z1) z2 = ⇂Arg z2 - (Arg z1 + pi)⇃"
    unfolding ang_vec_def
    using arg_uminus[OF assms] 
    using canon_ang_arg[of z2, symmetric]
    using canon_ang_diff[of "Arg z2" "Arg z1 + pi", symmetric]
    by simp
  moreover
  have "⇂∠ z1 z2 - pi⇃ = ⇂Arg z2 - Arg z1 - pi⇃"
    using canon_ang_id[of pi, symmetric]
    using canon_ang_diff[of "Arg z2 - Arg z1" "pi", symmetric]
    by simp_all
  ultimately
  show ?thesis
    by (simp add: field_simps)
qed

lemma ang_vec_opposite2:
  assumes "z2 ≠ 0"
  shows "∠ z1 (-z2) = ⇂∠ z1 z2 + pi⇃"
  unfolding ang_vec_def
  using arg_mult[of "-1" "z2"] assms
  using arg_complex_of_real_negative[of "-1"]
  using canon_ang_diff[of "Arg (-1) + Arg z2" "Arg z1", symmetric]
  using canon_ang_sum[of "Arg z2 - Arg z1" "pi", symmetric]
  using canon_ang_id[of pi] canon_ang_arg[of z1]
  by (auto simp: algebra_simps)
  

lemma ang_vec_opposite_opposite:
  assumes "z1 ≠ 0" and "z2 ≠ 0"
  shows "∠ (-z1) (-z2) = ∠ z1 z2"
proof-
  have "∠ (-z1) (-z2) = ⇂⇂∠ z1 z2 + pi⇃ - ⇂pi⇃⇃"
    using ang_vec_opposite1[OF assms(1)]
    using ang_vec_opposite2[OF assms(2)]
    using canon_ang_id[of pi, symmetric]
    by simp_all
  also have "... = ⇂∠ z1 z2⇃"
    by (subst canon_ang_diff[symmetric], simp)
  finally
  show ?thesis
    by (metis ang_vec_def canon_ang(1) canon_ang(2) canon_ang_id)
qed

lemma ang_vec_opposite_opposite':
  assumes "z1 ≠ z" and "z2 ≠ z"
  shows "∠ (z - z1) (z - z2) = ∠ (z1 - z) (z2 - z)"
using ang_vec_opposite_opposite[of "z - z1" "z - z2"] assms
by (simp add: field_simps del: ang_vec_def)

text ‹Cosine, scalar product and the law of cosines›

lemma cos_cmod_scalprod:
  shows "cmod z1 * cmod z2 * (cos (∠ z1 z2)) = Re (scalprod z1 z2)"
proof (cases "z1 = 0 ∨ z2 = 0")
  case True
  thus ?thesis
    by auto
next
  case False
  thus ?thesis
    by (simp add: cos_diff cos_arg sin_arg field_simps)
qed

lemma cos0_scalprod0:
  assumes "z1 ≠ 0" and "z2 ≠ 0"
  shows "cos (∠ z1 z2) = 0 ⟷ scalprod z1 z2 = 0"
  using assms
  using cnj_mix_real[of z1 z2]
  using cos_cmod_scalprod[of z1 z2]
  by (auto simp add: complex_eq_if_Re_eq)

lemma ortho_scalprod0:
  assumes "z1 ≠ 0" and "z2 ≠ 0"
  shows "∠ z1 z2 = pi/2 ∨ ∠ z1 z2 = -pi/2 ⟷ scalprod z1 z2 = 0"
  using cos0_scalprod0[OF assms]
  using ang_vec_bounded[of z1 z2]
  using cos_0_iff_canon[of "∠ z1 z2"]
  by (metis cos_minus cos_pi_half divide_minus_left)

lemma law_of_cosines:
  shows "(cdist B C)⇧2 = (cdist A C)⇧2 + (cdist A B)⇧2 - 2*(cdist A C)*(cdist A B)*(cos (∠ (C-A) (B-A)))"
proof-
  let ?a = "C-B" and ?b = "C-A" and ?c = "B-A"
  have "?a = ?b - ?c"
    by simp
  hence "(cmod ?a)⇧2 = (cmod (?b - ?c))⇧2"
    by metis
  also have "... = Re (scalprod (?b-?c) (?b-?c))"
    by (simp add: cmod_square)
  also have "... = (cmod ?b)⇧2 + (cmod ?c)⇧2 - 2*Re (scalprod ?b ?c)"
    by (simp add: cmod_square field_simps)
  finally
  show ?thesis
    using cos_cmod_scalprod[of ?b ?c]
    by simp
qed

(* ---------------------------------------------------------------------------- *)
subsubsection ‹Unoriented angle›
(* ---------------------------------------------------------------------------- *)

text ‹Convex unoriented angle between two vectors (it is always in the interval $[0, pi]$).›
definition ang_vec_c ("∠c") where
  [simp]:"∠c z1 z2 ≡ abs (∠ z1 z2)"

lemma ang_vec_c_sym:
  shows "∠c z1 z2 = ∠c z2 z1"
  unfolding ang_vec_c_def
  using ang_vec_sym_pi[of z1 z2] ang_vec_sym[of z1 z2]
  by (cases "∠ z1 z2 = pi") auto

lemma ang_vec_c_bounded: "0 ≤ ∠c z1 z2 ∧ ∠c z1 z2 ≤ pi"
  using canon_ang(1)[of "Arg z2 - Arg z1"] canon_ang(2)[of "Arg z2 - Arg z1"]
  by auto

text ‹Cosine and scalar product›

lemma cos_c_: "cos (∠c z1 z2) = cos (∠ z1 z2)"
  unfolding ang_vec_c_def
  by (smt cos_minus)

lemma ortho_c_scalprod0:
  assumes "z1 ≠ 0" and "z2 ≠ 0"
  shows "∠c z1 z2 = pi/2 ⟷ scalprod z1 z2 = 0"
proof-
  have "∠ z1 z2 = pi / 2 ∨ ∠ z1 z2 = - pi / 2 ⟷ ∠c z1 z2 = pi/2"
    unfolding ang_vec_c_def
    using arctan 
    by force
  thus ?thesis
    using ortho_scalprod0[OF assms]
    by simp
qed

(* ---------------------------------------------------------------------------- *)
subsubsection ‹Acute angle›
(* ---------------------------------------------------------------------------- *)

text ‹Acute or right angle (non-obtuse) between two vectors (it is always in the interval $[0, \frac{\pi}{2}$]).
We will use this to measure angle between two circles, since it can always be acute (or right).›

definition acute_ang where
  [simp]: "acute_ang α = (if α > pi / 2 then pi - α else α)"

definition ang_vec_a ("∠a") where
  [simp]: "∠a z1 z2 ≡ acute_ang (∠c z1 z2)"

lemma ang_vec_a_sym:
  "∠a z1 z2 = ∠a z2 z1"
  unfolding ang_vec_a_def
  using ang_vec_c_sym
  by auto

lemma ang_vec_a_opposite2:
  "∠a z1 z2 = ∠a z1 (-z2)"
proof(cases "z2  = 0")
  case True
  thus ?thesis
    by (metis minus_zero)
next
  case False
  thus ?thesis
  proof(cases "∠ z1 z2 < -pi / 2")
    case True
    hence "∠ z1 z2 < 0"
      using pi_not_less_zero
      by linarith
    have "∠a z1 z2 = pi + ∠ z1 z2"
      using True ‹∠ z1 z2 < 0›
      unfolding ang_vec_a_def ang_vec_c_def ang_vec_a_def abs_real_def
      by auto
    moreover
    have "∠a z1 (-z2) = pi + ∠ z1 z2"
      unfolding ang_vec_a_def ang_vec_c_def abs_real_def
      using canon_ang(1)[of "Arg z2 - Arg z1"] canon_ang(2)[of "Arg z2 - Arg z1"]
      using ang_vec_plus_pi2[of z1 z2] True ‹∠ z1 z2 < 0› ‹z2 ≠ 0›
      using ang_vec_opposite2[of z2 z1]
      by auto
    ultimately
    show ?thesis
      by auto
  next
    case False
    show ?thesis
    proof (cases "∠ z1 z2 ≤ 0")
      case True
      have "∠a z1 z2 = - ∠ z1 z2"
        using ‹¬ ∠ z1 z2 < - pi / 2› True
        unfolding ang_vec_a_def ang_vec_c_def ang_vec_a_def abs_real_def
        by auto
      moreover
      have "∠a z1 (-z2) = - ∠ z1 z2"
        using ‹¬ ∠ z1 z2 < - pi / 2› True
        unfolding ang_vec_a_def ang_vec_c_def abs_real_def
        using ang_vec_plus_pi2[of z1 z2]
        using canon_ang(1)[of "Arg z2 - Arg z1"] canon_ang(2)[of "Arg z2 - Arg z1"]
        using ‹z2 ≠ 0› ang_vec_opposite2[of z2 z1]
        by auto
      ultimately
      show ?thesis
        by simp
    next
      case False
      show ?thesis
      proof (cases "∠ z1 z2 < pi / 2")
        case True
        have "∠a z1 z2 = ∠ z1 z2"
          using ‹¬ ∠ z1 z2 ≤ 0› True
          unfolding ang_vec_a_def ang_vec_c_def ang_vec_a_def abs_real_def
          by auto
        moreover
        have "∠a z1 (-z2) = ∠ z1 z2"
          using ‹¬ ∠ z1 z2 ≤ 0› True
          unfolding ang_vec_a_def ang_vec_c_def abs_real_def
          using ang_vec_plus_pi1[of z1 z2]
          using canon_ang(1)[of "Arg z2 - Arg z1"] canon_ang(2)[of "Arg z2 - Arg z1"]
          using ‹z2 ≠ 0› ang_vec_opposite2[of z2 z1]
          by auto
        ultimately
        show ?thesis
          by simp
      next
        case False
        have "∠ z1 z2 > 0"
          using False
          by (metis less_linear less_trans pi_half_gt_zero)
        have "∠a z1 z2 = pi - ∠ z1 z2"
          using False ‹∠ z1 z2 > 0›
          unfolding ang_vec_a_def ang_vec_c_def ang_vec_a_def abs_real_def
          by auto
        moreover
        have "∠a z1 (-z2) = pi - ∠ z1 z2"
          unfolding ang_vec_a_def ang_vec_c_def abs_real_def
          using False ‹∠ z1 z2 > 0›
          using ang_vec_plus_pi1[of z1 z2]
          using canon_ang(1)[of "Arg z2 - Arg z1"] canon_ang(2)[of "Arg z2 - Arg z1"]
          using ‹z2 ≠ 0› ang_vec_opposite2[of z2 z1]
          by auto
        ultimately
        show ?thesis
          by auto
      qed
    qed
  qed
qed

lemma ang_vec_a_opposite1:
  shows "∠a z1 z2 = ∠a (-z1) z2"
  using ang_vec_a_sym[of "-z1" z2] ang_vec_a_opposite2[of z2 z1] ang_vec_a_sym[of z2 z1]
  by auto

lemma ang_vec_a_scale1:
  assumes "k ≠ 0"
  shows "∠a (cor k * z1) z2 = ∠a z1 z2"
proof (cases "k > 0")
  case True
  thus ?thesis
    unfolding ang_vec_a_def ang_vec_c_def ang_vec_def
    using arg_mult_real_positive[of k z1]
    by auto
next
  case False
  hence "k < 0"
    using assms
    by auto
  thus ?thesis
    using arg_mult_real_negative[of k z1]
    using ang_vec_a_opposite1[of z1 z2]
    unfolding ang_vec_a_def ang_vec_c_def ang_vec_def
    by simp
qed

lemma ang_vec_a_scale2:
  assumes "k ≠ 0"
  shows "∠a z1 (cor k * z2) = ∠a z1 z2"
  using ang_vec_a_sym[of z1 "complex_of_real k * z2"]
  using ang_vec_a_scale1[OF assms, of z2 z1]
  using ang_vec_a_sym[of z1 z2]
  by auto

lemma ang_vec_a_scale:
  assumes "k1 ≠ 0" and "k2 ≠ 0"
  shows "∠a (cor k1 * z1) (cor k2 * z2) = ∠a z1 z2"
  using ang_vec_a_scale1[OF assms(1)] ang_vec_a_scale2[OF assms(2)]
  by auto

lemma ang_a_cnj_cnj:
  shows "∠a z1 z2 = ∠a (cnj z1) (cnj z2)"
unfolding ang_vec_a_def ang_vec_c_def ang_vec_def
proof(cases "Arg z1 ≠ pi ∧ Arg z2 ≠ pi")
  case True
  thus "acute_ang ¦⇂Arg z2 - Arg z1⇃¦ = acute_ang ¦⇂Arg (cnj z2) - Arg (cnj z1)⇃¦"
    using arg_cnj_not_pi[of z1] arg_cnj_not_pi[of z2]
    apply (auto simp del:acute_ang_def)
    proof(cases "⇂Arg z2 - Arg z1⇃ = pi")
      case True
      thus "acute_ang ¦⇂Arg z2 - Arg z1⇃¦ = acute_ang ¦⇂Arg z1 - Arg z2⇃¦"
        using  canon_ang_uminus_pi[of "Arg z2 - Arg z1"]
        by (auto simp add:field_simps)
    next
      case False
      thus "acute_ang ¦⇂Arg z2 - Arg z1⇃¦ = acute_ang ¦⇂Arg z1 - Arg z2⇃¦"
        using  canon_ang_uminus[of "Arg z2 - Arg z1"]
        by (auto simp add:field_simps)
    qed
  next
    case False
    thus "acute_ang ¦⇂Arg z2 - Arg z1⇃¦ = acute_ang ¦⇂Arg (cnj z2) - Arg (cnj z1)⇃¦"
    proof(cases "Arg z1 = pi")
      case False
      hence "Arg z2 = pi"
        using ‹ ¬ (Arg z1 ≠ pi ∧ Arg z2 ≠ pi)›
        by auto
      thus ?thesis
        using False
        using arg_cnj_not_pi[of z1] arg_cnj_pi[of z2]
        apply (auto simp del:acute_ang_def)
      proof(cases "Arg z1 > 0")
          case True
          hence "-Arg z1 ≤ 0"
            by auto
          thus "acute_ang ¦⇂pi - Arg z1⇃¦ = acute_ang ¦⇂pi + Arg z1⇃¦"
            using True canon_ang_plus_pi1[of "Arg z1"]
            using Arg_bounded[of z1] canon_ang_plus_pi2[of "-Arg z1"]
            by (auto simp add:field_simps)
        next
          case False
          hence "-Arg z1 ≥ 0"
             by simp
          thus "acute_ang ¦⇂pi - Arg z1⇃¦ = acute_ang ¦⇂pi + Arg z1⇃¦"
          proof(cases "Arg z1 = 0")
            case True
            thus ?thesis
              by (auto simp del:acute_ang_def)
          next
            case False
            hence "-Arg z1 > 0"
              using ‹-Arg z1 ≥ 0›
              by auto
            thus ?thesis
            using False canon_ang_plus_pi1[of "-Arg z1"]
            using Arg_bounded[of z1] canon_ang_plus_pi2[of "Arg z1"]
            by (auto simp add:field_simps)
        qed
      qed
    next
      case True
      thus ?thesis
        using arg_cnj_pi[of z1]
        apply (auto simp del:acute_ang_def)
      proof(cases "Arg z2 = pi")
        case True
        thus "acute_ang ¦⇂Arg z2 - pi⇃¦ = acute_ang ¦⇂Arg (cnj z2) - pi⇃¦"
          using arg_cnj_pi[of z2]
          by auto
      next
        case False
        thus "acute_ang ¦⇂Arg z2 - pi⇃¦ = acute_ang ¦⇂Arg (cnj z2) - pi⇃¦"
          using arg_cnj_not_pi[of z2]
          apply (auto simp del:acute_ang_def)
        proof(cases "Arg z2 > 0")
          case True
          hence "-Arg z2 ≤ 0"
            by auto
          thus "acute_ang ¦⇂Arg z2 - pi⇃¦ = acute_ang ¦⇂- Arg z2 - pi⇃¦"
            using True canon_ang_minus_pi1[of "Arg z2"]
            using Arg_bounded[of z2] canon_ang_minus_pi2[of "-Arg z2"]
            by (auto simp add: field_simps)
        next
          case False
          hence "-Arg z2 ≥ 0"
             by simp
          thus "acute_ang ¦⇂Arg z2 - pi⇃¦ = acute_ang ¦⇂- Arg z2 - pi⇃¦"
          proof(cases "Arg z2 = 0")
            case True
            thus ?thesis
              by (auto simp del:acute_ang_def)
          next
            case False
            hence "-Arg z2 > 0"
              using ‹-Arg z2 ≥ 0›
              by auto
            thus ?thesis
            using False canon_ang_minus_pi1[of "-Arg z2"]
            using Arg_bounded[of z2] canon_ang_minus_pi2[of "Arg z2"]
            by (auto simp add:field_simps)
        qed
      qed
    qed
  qed
qed

text ‹Cosine and scalar product›

lemma ortho_a_scalprod0:
  assumes "z1 ≠ 0" and "z2 ≠ 0"
  shows "∠a z1 z2 = pi/2 ⟷ scalprod z1 z2 = 0"
  unfolding ang_vec_a_def
  using assms ortho_c_scalprod0[of z1 z2]
  by auto

declare ang_vec_c_def[simp del]

lemma cos_a_c: "cos (∠a z1 z2) = abs (cos (∠c z1 z2))"
proof-
  have "0 ≤ ∠c z1 z2" "∠c z1 z2 ≤ pi"
    using ang_vec_c_bounded[of z1 z2]
    by auto
  show ?thesis
  proof (cases "∠c z1 z2 = pi/2")
    case True
    thus ?thesis
      unfolding ang_vec_a_def acute_ang_def
      by (smt cos_pi_half pi_def pi_half)
  next
    case False
    show ?thesis
    proof (cases "∠c z1 z2 < pi / 2")
      case True
      thus ?thesis
        using ‹0 ≤ ∠c z1 z2›
        using cos_gt_zero_pi[of "∠c z1 z2"]
        unfolding ang_vec_a_def
        by simp
    next
      case False
      hence "∠c z1 z2 > pi/2"
        using ‹∠c z1 z2 ≠ pi/2›
        by simp
      hence "cos (∠c z1 z2) < 0"
        using ‹∠c z1 z2 ≤ pi›
        using cos_lt_zero_on_pi2_pi[of "∠c z1 z2"] 
        by simp
      thus ?thesis
        using ‹∠c z1 z2 > pi/2›
        unfolding ang_vec_a_def
        by simp
    qed
  qed
qed

end