Theory 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"
begin
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)
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"
proof-
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
next
case False
thus ?thesis
using assms ‹arccos a > 0› ‹arccos a ≤ pi/2›
by (rule_tac x = "α + arccos a" in exI) auto
qed
qed
lemma ex_cos_gt:
assumes "-pi/2 ≤ α ∧ α ≤ pi/2"
assumes "a < 1"
shows "∃ α'. -pi/2 ≤ α' ∧ α' ≤ pi/2 ∧ α' ≠ α ∧ cos (α - α') > a"
proof-
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
qed
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
else
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
end