Theory Complex_Geometry.More_Transcendental

(* ---------------------------------------------------------------------------- *)
section ‹Introduction›
(* ---------------------------------------------------------------------------- *)

text ‹The complex plane or some of its parts (e.g., the unit disc or the upper half plane) are often
taken as the domain in which models of various geometries (both Euclidean and non-Euclidean ones)
are formalized. The complex plane gives simpler and more compact formulas than the Cartesian plane.
Within complex plane is easier to describe geometric objects and perform the calculations (usually
shedding some new light on the subject). We give a formalization of the extended complex
plane (given both as a complex projective space and as the Riemann sphere), its objects (points,
circles and lines), and its transformations (Möbius transformations).›

(* ---------------------------------------------------------------------------- *)
section ‹Related work›
(* ---------------------------------------------------------------------------- *)

text‹During the last decade, there have been many results in formalizing
geometry in proof-assistants. Parts of Hilbert's seminal book
,,Foundations of Geometry'' cite"hilbert" have been formalized both
in Coq and Isabelle/Isar.  Formalization of first two groups of axioms
in Coq, in an intuitionistic setting was done by Dehlinger et
al. cite"hilbert-coq". First formalization in Isabelle/HOL was done
by Fleuriot and Meikele cite"hilbert-isabelle", and some further
developments were made in master thesis of Scott cite"hilbert-scott".
Large fragments of Tarski's geometry cite"tarski" have been
formalized in Coq by Narboux et al. cite"narboux-tarski". Within Coq,
there are also formalizations of von Plato's constructive geometry by
Kahn cite"vonPlato" and "von-plato-formalization", French high school
geometry by Guilhot cite"guilhot" and ruler and compass geometry by
Duprat cite"duprat2008", etc.

In our previous work cite"petrovic2012formalizing", we have already
formally investigated a Cartesian model of Euclidean geometry. 

(* ---------------------------------------------------------------------------- *)
section ‹Background theories› 
(* ---------------------------------------------------------------------------- *)

text ‹In this section we introduce some basic mathematical notions and prove some lemmas needed in the rest of our
formalization. We describe:

     trigonometric functions,

     complex numbers, 

     systems of two and three linear equations with two unknowns (over arbitrary fields), 

     quadratic equations (over real and complex numbers), systems of quadratic and real
      equations, and systems of two quadratic equations,

     two-dimensional vectors and matrices over complex numbers.

(* -------------------------------------------------------------------------- *)
subsection ‹Library Additions for Trigonometric Functions›
(* -------------------------------------------------------------------------- *)

theory More_Transcendental
  imports Complex_Main "HOL-Library.Periodic_Fun"

text ‹Additional properties of @{term sin} and @{term cos} functions that are later used in proving
conjectures for argument of complex number.›

text ‹Sign of trigonometric functions on some characteristic intervals.›

lemma cos_lt_zero_on_pi2_pi [simp]:
  assumes "x > pi/2" and "x  pi"
  shows "cos x < 0"
  using cos_gt_zero_pi[of "pi - x"] assms
  by simp

text ‹Value of trigonometric functions in points $k\pi$ and $\frac{\pi}{2} + k\pi$.›

lemma sin_kpi [simp]:
  fixes k::int
  shows "sin (k * pi) = 0"
  by (simp add: sin_zero_iff_int2)

lemma cos_odd_kpi [simp]:
  fixes k::int
  assumes "odd k"
  shows "cos (k * pi) = -1"
  by (simp add: assms mult.commute)

lemma cos_even_kpi [simp]:
  fixes k::int
  assumes "even k"
  shows "cos (k * pi) = 1"
  by (simp add: assms mult.commute)

lemma sin_pi2_plus_odd_kpi [simp]:
  fixes k::int
  assumes "odd k"
  shows "sin (pi / 2 + k * pi) = -1"
  using assms
  by (simp add: sin_add)

lemma sin_pi2_plus_even_kpi [simp]:
  fixes k::int
  assumes "even k"
  shows "sin (pi / 2 + k * pi) = 1"
  using assms
  by (simp add: sin_add)

text ‹Solving trigonometric equations and systems with special values (0, 1, or -1) of sine and cosine functions›

lemma cos_0_iff_canon:
  assumes "cos φ = 0" and "-pi < φ" and "φ  pi"
  shows "φ = pi/2  φ = -pi/2"
  by (smt (verit, best) arccos_0 arccos_cos assms cos_minus divide_minus_left)

lemma sin_0_iff_canon:
  assumes "sin φ = 0" and "-pi < φ" and "φ  pi"
  shows "φ = 0  φ = pi"
  using assms sin_eq_0_pi by force

lemma cos0_sin1:
  assumes "sin φ = 1"
  shows " k::int. φ = pi/2 + 2*k*pi"
  by (smt (verit, ccfv_threshold) assms cos_diff cos_one_2pi_int cos_pi_half mult_cancel_right1 sin_pi_half sin_plus_pi)

(* TODO: add lemmas for cos = -1, sin = 0 and cos = 0, sin = -1 *)

text ‹Sine is injective on $[-\frac{\pi}{2}, \frac{\pi}{2}]$›

lemma sin_inj:
  assumes "-pi/2  α  α  pi/2" and "-pi/2  α'  α'  pi/2"
  assumes "α  α'"
  shows "sin α  sin α'"
  by (metis assms divide_minus_left sin_inj_pi)

text ‹Periodicity of trigonometric functions›

text ‹The following are available in HOL-Decision\_Procs.Approximation\_Bounds, but we want to avoid
that dependency›

lemma sin_periodic_nat [simp]: 
  fixes n :: nat
  shows "sin (x + n * (2 * pi)) = sin x"
  by (metis (no_types, opaque_lifting) add.commute add.left_neutral cos_2npi cos_one_2pi_int mult.assoc mult.commute mult.left_neutral mult_zero_left sin_add sin_int_2pin)

lemma sin_periodic_int [simp]:
  fixes i :: int
  shows "sin (x + i * (2 * pi)) = sin x"
  by (metis add.right_neutral cos_int_2pin mult.commute mult.right_neutral mult_zero_right sin_add sin_int_2pin)

lemma cos_periodic_nat [simp]: 
  fixes n :: nat
  shows "cos (x + n * (2 * pi)) = cos x"
  by (metis add.left_neutral cos_2npi cos_add cos_periodic mult.assoc mult_2 mult_2_right of_nat_numeral sin_periodic sin_periodic_nat)

lemma cos_periodic_int [simp]:
  fixes i :: int
  shows "cos (x + i * (2 * pi)) = cos x"
  by (metis cos_add cos_int_2pin diff_zero mult.commute mult.right_neutral mult_zero_right sin_int_2pin)

text ‹Values of both sine and cosine are repeated only after multiples of $2\cdot \pi$›

lemma sin_cos_eq:
  fixes a b :: real
  assumes "cos a = cos b" and "sin a = sin b"
  shows " k::int. a - b = 2*k*pi"
  by (metis assms cos_diff cos_one_2pi_int mult.commute sin_cos_squared_add3)

text ‹The following two lemmas are consequences of surjectivity of cosine for the range $[-1, 1]$.›

lemma ex_cos_eq:
  assumes "-pi/2  α  α  pi/2"
  assumes "a  0" and "a < 1"
  shows " α'. -pi/2  α'  α'  pi/2  α'  α  cos (α - α') = a"
  have "arccos a > 0" "arccos a  pi/2"
    using a  0 a < 1
    using arccos_lt_bounded arccos_le_pi2
    by auto

  show ?thesis
  proof (cases "α - arccos a  - pi/2")
    case True
    thus ?thesis
      using assms arccos a > 0 arccos a  pi/2
      by (rule_tac x = "α - arccos a" in exI) auto
    case False
    thus ?thesis
      using assms arccos a > 0 arccos a  pi/2
      by (rule_tac x = "α + arccos a" in exI) auto

lemma ex_cos_gt:
  assumes "-pi/2  α  α  pi/2"
  assumes "a < 1"
  shows " α'. -pi/2  α'  α'  pi/2  α'  α  cos (α - α') > a"
  obtain a' where "a'  0" "a' > a" "a' < 1"
    by (metis assms(2) dense_le_bounded linear not_one_le_zero)
  thus ?thesis
    using ex_cos_eq[of α a'] assms
    by auto

text ‹The function @{term atan2} is a generalization of @{term arctan} that takes a pair of coordinates
of non-zero points returns its angle in the range $[-\pi, \pi)$.›

definition atan2 where
  "atan2 y x =
    (if x > 0 then arctan (y/x)
     else if x < 0 then
          if y > 0 then arctan (y/x) + pi else arctan (y/x) - pi
          if y > 0 then pi/2 else if y < 0 then -pi/2 else 0)"

lemma atan2_bounded: 
  shows "-pi  atan2 y x  atan2 y x < pi"
  using arctan_bounded[of "y/x"] zero_le_arctan_iff[of "y/x"] arctan_le_zero_iff[of "y/x"] zero_less_arctan_iff[of "y/x"] arctan_less_zero_iff[of "y/x"]
  using divide_neg_neg[of y x] divide_neg_pos[of y x] divide_pos_pos[of y x]  divide_pos_neg[of y x]
  unfolding atan2_def
  by (simp (no_asm_simp)) auto