# 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
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›
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"

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 α]
thus ?thesis
using sin_periodic_int[of "⇂α⇃" x]
qed

lemma canon_ang_cos [simp]:
shows "cos ⇂α⇃ = cos α"
proof-
obtain x::int where "α = ⇂α⇃ + pi * (x * 2)"
using canon_ang(3)[of α]