# HG changeset patch # User paulson # Date 1676040711 0 # Node ID 2d26af072990e2c942f5698a8d92f52702c0726a # Parent 268c8184288349b4e755c9d78575051edd57ecc3 Some basis results about trigonometric functions diff -r 268c81842883 -r 2d26af072990 src/HOL/Analysis/Complex_Transcendental.thy --- 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: "(\z. z \ s \ Im z = 0 \ \Re z\ < 1) \ Arccos holomorphic_on s" by (simp add: field_differentiable_within_Arccos holomorphic_on_def) +text \This theorem is about REAL cos/arccos but relies on theorems about @{term Arg}\ +lemma cos_eq_arccos_Ex: + "cos x = y \ -1\y \ y\1 \ (\k::int. x = arccos y + 2*k*pi \ x = - arccos y + 2*k*pi)" (is "?L=?R") +proof + assume R: ?R + then obtain k::int where "x = arccos y + 2*k*pi \ 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 = "(\k::int. x = arccos y + 2*k*pi \ x = - arccos y + 2*k*pi)" + obtain k::int where k: "-pi < x-k*2*pi" "x-k*2*pi \ 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 \
: ?goal when "x-k*2*pi \ 0" + using arccos_cos k that by force + moreover have ?goal when "\ x-k*2*pi \0" + proof - + have "cos (k * 2*pi - x) = y" + by (metis * cos_minus minus_diff_eq) + then show ?goal + using arccos_cos \
k by fastforce + qed + ultimately show "-1\y \ y\1 \ ?goal" + using L by auto +qed subsection\<^marker>\tag unimportant\\Upper and Lower Bounds for Inverse Sine and Cosine\ @@ -4279,8 +4309,8 @@ qed lemma finite_complex_roots_unity_explicit: - "finite {exp(2 * of_real pi * \ * of_nat j / of_nat n) | j::nat. j < n}" -by simp + "finite {exp(2 * of_real pi * \ * of_nat j / of_nat n) | j::nat. j < n}" + by simp lemma card_complex_roots_unity_explicit: "card {exp(2 * of_real pi * \ * of_nat j / of_nat n) | j::nat. j < n} = n" diff -r 268c81842883 -r 2d26af072990 src/HOL/Transcendental.thy --- 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 \ (\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 \ cos x = 0 \ sin x = 0" + by (auto simp: tan_def) + +text \Note: half of these zeros would normally be regarded as undefined cases.\ +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 \ 0 \ cos y \ 0 \ cos (x + y) \ 0 \ 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 \ 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 "\ = 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 \ 0 \ 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) \ 0" by (intro less_imp_neq [symmetric] cos_gt_zero_pi arctan_lbound arctan_ubound) +lemma tan_eq_arctan_Ex: + shows "tan x = y \ (\k::int. x = arctan y + k*pi \ (x = pi/2 + k*pi \ y=0))" +proof + assume lhs: "tan x = y" + obtain k::int where k:"-pi/2 < x-k*pi" "x-k*pi \ pi/2" + proof + define k where "k \ 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 \ 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 \ 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 "\k. x = arctan y + of_int k * pi \ (x = pi/2 + k*pi \ y=0)" + using lhs k by force +qed (auto simp: arctan) + +lemma arctan_tan_eq_abs_pi: + assumes "cos \ \ 0" + obtains k where "arctan (tan \) = \ - 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 \ 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)