Some basis results about trigonometric functions

--- a/src/HOL/Analysis/Complex_Transcendental.thy	Thu Feb 09 16:29:53 2023 +0000
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Fri Feb 10 14:51:51 2023 +0000
@@ -4038,6 +4038,36 @@
 lemma holomorphic_on_Arccos: "(\<And>z. z \<in> s \<Longrightarrow> Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> Arccos holomorphic_on s"
   by (simp add: field_differentiable_within_Arccos holomorphic_on_def)
 
+text \<open>This theorem is about REAL cos/arccos but relies on theorems about @{term Arg}\<close>
+lemma cos_eq_arccos_Ex:
+  "cos x = y \<longleftrightarrow> -1\<le>y \<and> y\<le>1 \<and> (\<exists>k::int. x = arccos y + 2*k*pi \<or> x = - arccos y + 2*k*pi)" (is "?L=?R")
+proof
+  assume R: ?R
+  then obtain k::int where "x = arccos y + 2*k*pi \<or> x = - arccos y + 2*k*pi" by auto
+  moreover have "cos x = y" when "x = arccos y + 2*k*pi"
+    by (metis (no_types) R cos_arccos cos_eq_periodic_intro cos_minus minus_add_cancel)
+  moreover have "cos x = y" when "x = -arccos y + 2*k*pi"
+    by (metis add_minus_cancel R cos_arccos cos_eq_periodic_intro uminus_add_conv_diff)
+  ultimately show "cos x = y" by auto
+next
+  assume L: ?L
+  let ?goal = "(\<exists>k::int. x = arccos y + 2*k*pi \<or> x = - arccos y + 2*k*pi)"
+  obtain k::int where k: "-pi < x-k*2*pi" "x-k*2*pi \<le> pi"
+    by (metis Arg_bounded Arg_exp_diff_2pi complex.sel(2) mult.assoc of_int_mult of_int_numeral)
+  have *: "cos (x - k * 2*pi) = y"
+    using cos.periodic_simps(3)[of x "-k"] L by (auto simp add:field_simps)
+  then have \<section>: ?goal when "x-k*2*pi \<ge> 0"
+    using arccos_cos k that by force
+  moreover have ?goal when "\<not> x-k*2*pi \<ge>0"
+  proof -
+    have "cos (k * 2*pi - x) = y"
+      by (metis * cos_minus minus_diff_eq)
+    then show ?goal
+      using arccos_cos \<section> k by fastforce 
+  qed
+  ultimately show "-1\<le>y \<and> y\<le>1 \<and> ?goal"
+    using L by auto
+qed
 
 subsection\<^marker>\<open>tag unimportant\<close>\<open>Upper and Lower Bounds for Inverse Sine and Cosine\<close>
 
@@ -4279,8 +4309,8 @@
 qed
 
 lemma finite_complex_roots_unity_explicit:
-     "finite {exp(2 * of_real pi * \<i> * of_nat j / of_nat n) | j::nat. j < n}"
-by simp
+  "finite {exp(2 * of_real pi * \<i> * of_nat j / of_nat n) | j::nat. j < n}"
+  by simp
 
 lemma card_complex_roots_unity_explicit:
      "card {exp(2 * of_real pi * \<i> * of_nat j / of_nat n) | j::nat. j < n} = n"

--- a/src/HOL/Transcendental.thy	Thu Feb 09 16:29:53 2023 +0000
+++ b/src/HOL/Transcendental.thy	Fri Feb 10 14:51:51 2023 +0000
@@ -4204,6 +4204,12 @@
   finally show ?thesis .
 qed
 
+lemma cos_zero_iff_int2:
+  fixes x::real
+  shows "cos x = 0 \<longleftrightarrow> (\<exists>n::int. x = n * pi +  pi/2)"
+  using sin_zero_iff_int2[of "x-pi/2"] unfolding sin_cos_eq 
+  by (auto simp add: algebra_simps)
+
 lemma sin_npi_int [simp]: "sin (pi * of_int n) = 0"
   by (simp add: sin_zero_iff_int2)
 
@@ -4548,6 +4554,9 @@
   for n :: nat
   by (simp add: tan_def)
 
+lemma tan_pi_half [simp]: "tan (pi / 2) = 0"
+  by (simp add: tan_def)
+
 lemma tan_minus [simp]: "tan (- x) = - tan x"
   by (simp add: tan_def)
 
@@ -4561,6 +4570,16 @@
   for x :: "'a::{real_normed_field,banach}"
   by (simp add: tan_def sin_add field_simps)
 
+lemma tan_eq_0_cos_sin: "tan x = 0 \<longleftrightarrow> cos x = 0 \<or> sin x = 0"
+  by (auto simp: tan_def)
+
+text \<open>Note: half of these zeros would normally be regarded as undefined cases.\<close>
+lemma tan_eq_0_Ex:
+  assumes "tan x = 0"
+  obtains k::int where "x = (k/2) * pi"
+  using assms
+  by (metis cos_zero_iff_int mult.commute sin_zero_iff_int tan_eq_0_cos_sin times_divide_eq_left) 
+
 lemma tan_add:
   "cos x \<noteq> 0 \<Longrightarrow> cos y \<noteq> 0 \<Longrightarrow> cos (x + y) \<noteq> 0 \<Longrightarrow> tan (x + y) = (tan x + tan y)/(1 - tan x * tan y)"
   for x :: "'a::{real_normed_field,banach}"
@@ -4803,7 +4822,6 @@
   by (simp add: tan_def)
 
 lemma tan_periodic_nat[simp]: "tan (x + real n * pi) = tan x"
-  for n :: nat
 proof (induct n arbitrary: x)
   case 0
   then show ?case by simp
@@ -4817,25 +4835,16 @@
 
 lemma tan_periodic_int[simp]: "tan (x + of_int i * pi) = tan x"
 proof (cases "0 \<le> i")
-  case True
-  then have i_nat: "of_int i = of_int (nat i)" by auto
-  show ?thesis unfolding i_nat
-    by (metis of_int_of_nat_eq tan_periodic_nat)
-next
   case False
   then have i_nat: "of_int i = - of_int (nat (- i))" by auto
-  have "tan x = tan (x + of_int i * pi - of_int i * pi)"
-    by auto
-  also have "\<dots> = tan (x + of_int i * pi)"
-    unfolding i_nat mult_minus_left diff_minus_eq_add
-    by (metis of_int_of_nat_eq tan_periodic_nat)
-  finally show ?thesis by auto
-qed
+  then show ?thesis
+    by (smt (verit, best) mult_minus_left of_int_of_nat_eq tan_periodic_nat)
+qed (use zero_le_imp_eq_int in fastforce)
 
 lemma tan_periodic_n[simp]: "tan (x + numeral n * pi) = tan x"
   using tan_periodic_int[of _ "numeral n" ] by simp
 
-lemma tan_minus_45: "tan (-(pi/4)) = -1"
+lemma tan_minus_45 [simp]: "tan (-(pi/4)) = -1"
   unfolding tan_def by (simp add: sin_45 cos_45)
 
 lemma tan_diff:
@@ -4923,11 +4932,7 @@
 lemma cot_less_zero:
   assumes lb: "- pi/2 < x" and "x < 0"
   shows "cot x < 0"
-proof -
-  have "0 < cot (- x)"
-    using assms by (simp only: cot_gt_zero)
-  then show ?thesis by simp
-qed
+  by (smt (verit) assms cot_gt_zero cot_minus divide_minus_left)
 
 lemma DERIV_cot [simp]: "sin x \<noteq> 0 \<Longrightarrow> DERIV cot x :> -inverse ((sin x)\<^sup>2)"
   for x :: "'a::{real_normed_field,banach}"
@@ -5160,6 +5165,48 @@
 lemma cos_arctan_not_zero [simp]: "cos (arctan x) \<noteq> 0"
   by (intro less_imp_neq [symmetric] cos_gt_zero_pi arctan_lbound arctan_ubound)
 
+lemma tan_eq_arctan_Ex:
+  shows "tan x = y \<longleftrightarrow> (\<exists>k::int. x = arctan y + k*pi \<or> (x = pi/2 + k*pi \<and> y=0))"
+proof
+  assume lhs: "tan x = y"
+  obtain k::int where k:"-pi/2 < x-k*pi" "x-k*pi \<le> pi/2"
+  proof 
+    define k where "k \<equiv> ceiling (x/pi - 1/2)"
+    show "- pi / 2 < x - real_of_int k * pi" 
+      using ceiling_divide_lower [of "pi*2" "(x * 2 - pi)"] by (auto simp: k_def field_simps)
+    show  "x-k*pi \<le> pi/2"
+      using ceiling_divide_upper [of "pi*2" "(x * 2 - pi)"] by (auto simp: k_def field_simps)
+  qed
+  have "x = arctan y + of_int k * pi" when "x \<noteq> pi/2 + k*pi"
+  proof -
+    have "tan (x - k * pi) = y" using lhs tan_periodic_int[of _ "-k"] by auto
+    then have "arctan y = x - real_of_int k * pi"
+      by (smt (verit) arctan_tan lhs divide_minus_left k mult_minus_left of_int_minus tan_periodic_int that)
+    then show ?thesis by auto
+  qed
+  then show "\<exists>k. x = arctan y + of_int k * pi \<or> (x = pi/2 + k*pi \<and> y=0)"
+    using lhs k by force
+qed (auto simp: arctan)
+
+lemma arctan_tan_eq_abs_pi:
+  assumes "cos \<theta> \<noteq> 0"
+  obtains k where "arctan (tan \<theta>) = \<theta> - of_int k * pi"
+  by (metis add.commute assms cos_zero_iff_int2 eq_diff_eq tan_eq_arctan_Ex)
+
+lemma tan_eq:
+  assumes "tan x = tan y" "tan x \<noteq> 0"
+  obtains k::int where "x = y + k * pi"
+proof -
+  obtain k0 where k0: "x = arctan (tan y) + real_of_int k0 * pi"
+    using assms tan_eq_arctan_Ex[of x "tan y"] by auto
+  obtain k1 where k1: "arctan (tan y) = y - of_int k1 * pi"
+    using arctan_tan_eq_abs_pi assms tan_eq_0_cos_sin by auto
+  have "x = y + (k0-k1)*pi"
+    using k0 k1 by (auto simp: algebra_simps)
+  with that show ?thesis
+    by blast
+qed
+
 lemma cos_arctan: "cos (arctan x) = 1 / sqrt (1 + x\<^sup>2)"
 proof (rule power2_eq_imp_eq)
   have "0 < 1 + x\<^sup>2" by (simp add: add_pos_nonneg)