Theory Complex_Geometry.Canonical_Angle

(* -------------------------------------------------------------------------- *)
subsection ‹Canonical angle› 
(* -------------------------------------------------------------------------- *)

text ‹Canonize any angle to $(-\pi, \pi]$ (taking account of $2\pi$ periodicity of @{term sin} and
@{term cos}). With this function, for example, multiplicative properties of @{term arg} for complex
numbers can easily be expressed and proved.›

theory Canonical_Angle
imports More_Transcendental
begin


abbreviation canon_ang_P where
 "canon_ang_P α α'  (-pi < α'  α'  pi)  ( k::int. α - α' = 2*k*pi)"

definition canon_ang :: "real  real" ("_") where
  "α = (THE α'. canon_ang_P α α')"

text ‹There is a canonical angle for every angle.›
lemma canon_ang_ex:
  shows " α'. canon_ang_P α α'"
proof-
  have ***: " α::real.  α'. 0 < α'  α'  1  ( k::int. α' = α - k)"
  proof
    fix α::real
    show "α'>0. α'  1  (k::int. α' = α - k)"
    proof (cases "α = floor α")
      case True
      thus ?thesis
        by (rule_tac x="α - floor α + 1" in exI, auto) (rule_tac x="floor α - 1" in exI, auto)
    next
      case False
      thus ?thesis
        using real_of_int_floor_ge_diff_one[of "α"]
        using of_int_floor_le[of "α"]
        by (rule_tac x="α - floor α" in exI) smt
    qed
  qed

  have **: " α::real.  α'. 0 < α'  α'  2  ( k::int. α - α' = 2*k - 1)"
  proof
    fix α::real
    from ***[rule_format, of "(α + 1) /2"]
    obtain α' and k::int where "0 < α'" "α'  1" "α' = (α + 1)/2 - k"
      by force
    hence "0 < α'" "α'  1" "α' = α/2 - k + 1/2"
      by auto
    thus "α'>0. α'  2  (k::int. α - α' = real_of_int (2 * k - 1))"
      by (rule_tac x="2*α'" in exI) auto
  qed
  have *: " α::real.  α'. -1 < α'  α'  1  ( k::int. α - α' = 2*k)"
  proof
    fix α::real
    from ** obtain α' and k :: int where
      "0 < α'  α'  2  α - α' = 2*k - 1"
      by force
    thus "α'>-1. α'  1  (k. α - α' = real_of_int (2 * (k::int)))"
      by (rule_tac x="α' - 1" in exI) (auto simp add: field_simps)
  qed
  obtain α' k where 1: "α' >- 1  α'  1" and 2: "α / pi - α' = real_of_int (2 * k)"
    using *[rule_format, of "α / pi"]
    by auto
  have "α'*pi > -pi  α'*pi  pi" 
    using 1
    by (smt mult.commute mult_le_cancel_left1 mult_minus_right pi_gt_zero)
  moreover
  have "α - α'*pi = 2 * real_of_int k * pi"
    using 2
    by (auto simp add: field_simps)
  ultimately
  show ?thesis
    by auto
qed

text ‹Canonical angle of any angle is unique.›
lemma canon_ang_unique:
  assumes "canon_ang_P α α1" and "canon_ang_P α α2"
  shows "α1 = α2"
proof-
  obtain k1::int where "α - α1 = 2*k1*pi"
    using assms(1)
    by auto
  obtain k2::int where "α - α2 = 2*k2*pi"
    using assms(2)
    by auto
  hence *: "-α1 + α2 = 2*(k1 - k2)*pi"
    using α - α1 = 2*k1*pi
    by (simp add:field_simps)
  moreover
  have "-α1 + α2 < 2 * pi" "-α1 + α2 > -2*pi"
    using assms
    by auto
  ultimately
  have "-α1 + α2 = 0"
    using mult_less_cancel_right[of "-2" pi "real_of_int(2 * (k1 - k2))"]
    by auto
  thus ?thesis
    by auto
qed

text ‹Canonical angle is always in $(-\pi, \pi]$ and differs from the starting angle by $2k\pi$.›
lemma canon_ang:
  shows "-pi < α" and "α  pi" and " k::int. α - α = 2*k*pi"
proof-
  obtain α' where "canon_ang_P α α'"
    using canon_ang_ex[of α]
    by auto
  have "canon_ang_P α α"
    unfolding canon_ang_def
  proof (rule theI[where a="α'"])
    show "canon_ang_P α α'"
      by fact
  next
    fix α''
    assume "canon_ang_P α α''"
    thus "α'' = α'"
      using canon_ang_P α α'
      using canon_ang_unique[of α' α α'']
      by simp
  qed
  thus "-pi < α" "α  pi" " k::int. α - α = 2*k*pi"
    by auto
qed

text ‹Angles in $(-\pi, \pi]$ are already canonical.›
lemma canon_ang_id:
  assumes  "-pi < α  α  pi"
  shows "α = α"
  using assms
  using canon_ang_unique[of "canon_ang α" α α] canon_ang[of α]
  by auto

text ‹Angles that differ by $2k\pi$ have equal canonical angles.›
lemma canon_ang_eq:
  assumes " k::int. α1 - α2 = 2*k*pi"
  shows "α1 = α2"
proof-
  obtain k'::int where *: "- pi < α1" "α1  pi" "α1 - α1 = 2 * k' * pi"
    using canon_ang[of α1]
    by auto

  obtain k''::int where **: "- pi < α2" "α2  pi" "α2 - α2 = 2 * k'' * pi"
    using canon_ang[of α2]
    by auto

  obtain k::int where ***: "α1 - α2 = 2*k*pi"
    using assms
    by auto

  have "m::int. α1 - α2 = 2 * m * pi"
    using **(3) ***
    by (rule_tac x="k+k''" in exI) (auto simp add: field_simps)

  thus ?thesis
    using canon_ang_unique[of "α1" α1 "α2"] * **
    by auto
qed

text ‹Introduction and elimination rules›
lemma canon_ang_eqI:
  assumes "k::int. α' - α = 2 * k * pi" and "- pi < α'  α'  pi"
  shows "α = α'"
  using assms
  using canon_ang_eq[of α' α]
  using canon_ang_id[of α']
  by auto

lemma canon_ang_eqE:
  assumes "α1 = α2"
  shows " (k::int). α1 - α2 = 2 *k * pi"
proof-
  obtain k1 k2 :: int where
    "α1 - α1 = 2 * k1 * pi"
    "α2 - α2 = 2 * k2 * pi"
    using canon_ang[of α1] canon_ang[of α2]
    by auto
  thus ?thesis
    using assms
    by (rule_tac x="k1 - k2" in exI) (auto simp add: field_simps)
qed

text ‹Canonical angle of opposite angle›

lemma canon_ang_uminus:
  assumes "α  pi"
  shows "-α = -α"
proof (rule canon_ang_eqI)
  show "x::int. - α - - α = 2 * x * pi"
    using canon_ang(3)[of α]
    by (metis minus_diff_eq minus_diff_minus)
next
  show "- pi < - α  - α  pi"
    using canon_ang(1)[of α] canon_ang(2)[of α] assms
    by auto
qed

lemma canon_ang_uminus_pi:
  assumes "α = pi"
  shows "-α = α"
proof (rule canon_ang_eqI)
  obtain k::int where "α - α = 2 * k * pi"
    using canon_ang(3)[of α]
    by auto
  thus "x::int. α - - α = 2 * x * pi"
    using assms
    by (rule_tac x="k+(1::int)" in exI) (auto simp add: field_simps)
next
  show "- pi < α  α  pi"
    using assms
    by auto
qed

text ‹Canonical angle of difference of two angles›
lemma canon_ang_diff:
  shows "α - β = α - β"
proof (rule canon_ang_eq)
  show "x::int. α - β - (α - β) = 2 * x * pi"
  proof-
    obtain k1::int where "α - α = 2*k1*pi"
      using canon_ang(3)
      by auto
    moreover
    obtain k2::int where "β - β = 2*k2*pi"
      using canon_ang(3)
      by auto
    ultimately
    show ?thesis
      by (rule_tac x="k1 - k2" in exI) (auto simp add: field_simps)
  qed
qed

text ‹Canonical angle of sum of two angles›
lemma canon_ang_sum:
  shows "α + β = α + β"
proof (rule canon_ang_eq)
  show "x::int. α + β - (α + β) = 2 * x * pi"
  proof-
    obtain k1::int where "α - α = 2*k1*pi"
      using canon_ang(3)
      by auto
    moreover
    obtain k2::int where "β - β = 2*k2*pi"
      using canon_ang(3)
      by auto
    ultimately
    show ?thesis
      by (rule_tac x="k1 + k2" in exI) (auto simp add: field_simps)
  qed
qed

text ‹Canonical angle of angle from $(0, 2\pi]$ shifted by $\pi$›

lemma canon_ang_plus_pi1:
  assumes "0 < α" and "α  2*pi"
  shows "α + pi = α - pi"
proof (rule canon_ang_eqI)
  show " x::int. α - pi - (α + pi) = 2 * x * pi"
    by (rule_tac x="-1" in exI) auto
next
  show "- pi < α - pi  α - pi  pi"
    using assms
    by auto
qed

lemma canon_ang_minus_pi1:
  assumes "0 < α" and "α  2*pi"
  shows "α - pi = α - pi"
proof (rule canon_ang_id)
  show "- pi < α - pi  α - pi  pi"
    using assms
    by auto
qed

text ‹Canonical angle of angles from $(-2\pi, 0]$ shifted by $\pi$›

lemma canon_ang_plus_pi2:
  assumes "-2*pi < α" and "α  0"
  shows "α + pi = α + pi"
proof (rule canon_ang_id)
  show "- pi < α + pi  α + pi  pi"
    using assms
    by auto
qed

lemma canon_ang_minus_pi2:
  assumes "-2*pi < α" and "α  0"
  shows "α - pi = α + pi"
proof (rule canon_ang_eqI)
  show " x::int. α + pi - (α - pi) = 2 * x * pi"
    by (rule_tac x="1" in exI) auto
next
  show "- pi < α + pi  α + pi  pi"
    using assms
    by auto
qed

text ‹Canonical angle of angle in $(\pi, 3\pi]$.›
lemma canon_ang_pi_3pi: 
  assumes "pi < α" and "α  3 * pi"
  shows "α = α - 2*pi"
proof-
  have "x. - pi = pi * real_of_int x"
    by (rule_tac x="-1" in exI, simp)
  thus ?thesis
    using assms canon_ang_eqI[of "α - 2*pi" "α"]
    by auto
qed

text ‹Canonical angle of angle in $(-3\pi, -\pi]$.›
lemma canon_ang_minus_3pi_minus_pi: 
  assumes "-3*pi < α" and "α  -pi"
  shows "α = α + 2*pi"
proof-
  have "x. pi = pi * real_of_int x"
    by (rule_tac x="1" in exI, simp)
  thus ?thesis
    using assms canon_ang_eqI[of "α + 2*pi" "α"]
    by auto
qed

text ‹Canonical angles for some special angles›

lemma zero_canonical [simp]:
  shows "0 = 0"
  using canon_ang_eqI[of 0 0]
  by simp

lemma pi_canonical [simp]:
  shows "pi = pi"
  by (simp add: canon_ang_id)

lemma two_pi_canonical [simp]:
  shows "2 * pi = 0"
  using canon_ang_plus_pi1[of "pi"]
  by simp

text ‹Canonization preserves sine and cosine›
lemma canon_ang_sin [simp]:
  shows "sin α = sin α"
proof-
  obtain x::int where "α = α + pi * (x * 2)"
    using canon_ang(3)[of α]
    by (auto simp add: field_simps)
  thus ?thesis
    using sin_periodic_int[of "α" x]
    by (simp add: field_simps)
qed

lemma canon_ang_cos [simp]:
  shows "cos α = cos α"
proof-
  obtain x::int where "α = α + pi * (x * 2)"
    using canon_ang(3)[of α]
    by (auto simp add: field_simps)
  thus ?thesis
    using cos_periodic_int[of "α" x]
    by (simp add: field_simps)
qed

end