--- a/NEWS Thu Mar 19 11:54:20 2015 +0100
+++ b/NEWS Thu Mar 19 14:24:51 2015 +0000
@@ -83,14 +83,14 @@
type, so in particular on "real" and "complex" uniformly.
Minor INCOMPATIBILITY: type constraints may be needed.
-* New library of properties of the complex transcendental functions sin, cos, exp,
+* New library of properties of the complex transcendental functions sin, cos, tan, exp,
ported from HOL Light.
* The factorial function, "fact", now has type "nat => 'a" (of a sort that admits
numeric types including nat, int, real and complex. INCOMPATIBILITY:
an expression such as "fact 3 = 6" may require a type constraint, and the combination
"real (fact k)" is likely to be unsatisfactory. If a type conversion is still necessary,
- then use "of_nat (fact k)".
+ then use "of_nat (fact k)" or "real_of_nat (fact k)".
* removed functions "natfloor" and "natceiling",
use "nat o floor" and "nat o ceiling" instead.
--- a/src/HOL/Decision_Procs/Approximation.thy Thu Mar 19 11:54:20 2015 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy Thu Mar 19 14:24:51 2015 +0000
@@ -959,7 +959,7 @@
unfolding cos_coeff_def atLeast0LessThan by auto
have "cos t * (- 1) ^ n = cos t * cos (n * pi) + sin t * sin (n * pi)" by auto
- also have "\<dots> = cos (t + n * pi)" by (simp add: cos_add)
+ also have "\<dots> = cos (t + n * pi)" by (simp add: cos_add)
also have "\<dots> = ?rest" by auto
finally have "cos t * (- 1) ^ n = ?rest" .
moreover
@@ -1029,7 +1029,7 @@
{ fix n
have F: "\<And>m. ((\<lambda>i. i + 2) ^^ n) m = m + 2 * n" by (induct n) auto
have "?f (Suc n) = ?f n * ((\<lambda>i. i + 2) ^^ n) 2 * (((\<lambda>i. i + 2) ^^ n) 2 + 1)"
- unfolding F by auto }
+ unfolding F by auto }
note f_eq = this
from horner_bounds[where lb="lb_sin_cos_aux prec" and ub="ub_sin_cos_aux prec" and j'=0,
OF `0 \<le> real (x * x)` f_eq lb_sin_cos_aux.simps ub_sin_cos_aux.simps]
@@ -1046,7 +1046,7 @@
hence "0 < x" and "0 < real x" using `0 \<le> real x` by auto
have "0 < x * x" using `0 < x` by simp
- { fix x::real and n
+ { fix x::real and n
have "(\<Sum>j = 0 ..< n. (- 1) ^ (((2 * j + 1) - Suc 0) div 2) / ((fact (2 * j + 1))) * x ^(2 * j + 1))
= (\<Sum> i = 0 ..< 2 * n. (if even(i) then 0 else ((- 1) ^ ((i - Suc 0) div 2))/((fact i))) * x ^ i)" (is "?SUM = _")
proof -
@@ -1354,7 +1354,7 @@
by auto
have "cos (x + (-k) * (2 * pi)) \<le> cos ?lx"
- using cos_monotone_0_pi'[OF lx_0 lx pi_x]
+ using cos_monotone_0_pi_le[OF lx_0 lx pi_x]
by (simp only: real_of_int_minus
cos_minus mult_minus_left) simp
also have "\<dots> \<le> (ub_cos prec ?lx)"
@@ -1386,7 +1386,7 @@
have "(lb_cos prec ?ux) \<le> cos ?ux"
using lb_cos[OF ux_0 pi_ux] by simp
also have "\<dots> \<le> cos (x + (-k) * (2 * pi))"
- using cos_monotone_0_pi'[OF x_ge_0 ux pi_ux]
+ using cos_monotone_0_pi_le[OF x_ge_0 ux pi_ux]
by (simp only: real_of_int_minus
cos_minus mult_minus_left) simp
finally have "(lb_cos prec ?ux) \<le> cos x"
@@ -1505,7 +1505,7 @@
have "cos x = cos (x + (-k) * (2 * pi) + (1 :: int) * (2 * pi))"
unfolding cos_periodic_int ..
also have "\<dots> \<le> cos ((?lx + 2 * ?lpi))"
- using cos_monotone_0_pi'[OF lx_0 lx_le_x pi_x]
+ using cos_monotone_0_pi_le[OF lx_0 lx_le_x pi_x]
by (simp only: minus_float.rep_eq real_of_int_minus real_of_one
mult_minus_left mult_1_left) simp
also have "\<dots> \<le> (ub_cos prec (?lx + 2 * ?lpi))"
@@ -1535,7 +1535,7 @@
proof -
{ fix n
have F: "\<And> m. ((\<lambda>i. i + 1) ^^ n) m = n + m" by (induct n, auto)
- have "fact (Suc n) = fact n * ((\<lambda>i::nat. i + 1) ^^ n) 1" unfolding F by auto
+ have "fact (Suc n) = fact n * ((\<lambda>i::nat. i + 1) ^^ n) 1" unfolding F by auto
} note f_eq = this
note bounds = horner_bounds_nonpos[where f="fact" and lb="lb_exp_horner prec" and ub="ub_exp_horner prec" and j'=0 and s=1,
@@ -2022,7 +2022,7 @@
hence "0 \<le> bl" by (simp add: bitlen_def bl_def)
show ?thesis
proof (cases "0 \<le> e")
- case True
+ case True
thus ?thesis
unfolding bl_def[symmetric] using `0 < real m` `0 \<le> bl`
apply (simp add: ln_mult)
@@ -3234,7 +3234,7 @@
qed
lemma setprod_fact: "real (\<Prod> {1..<1 + k}) = fact (k :: nat)"
- using fact_altdef_nat Suc_eq_plus1_left atLeastLessThanSuc_atLeastAtMost real_fact_nat
+ using fact_altdef_nat Suc_eq_plus1_left atLeastLessThanSuc_atLeastAtMost real_fact_nat
by presburger
lemma approx_tse:
--- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Thu Mar 19 11:54:20 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Thu Mar 19 14:24:51 2015 +0000
@@ -156,104 +156,12 @@
lemma Im_cos: "Im(cos z) = sin(Re z) * (exp(-(Im z)) - exp(Im z)) / 2"
by (simp add: cos_exp_eq field_simps Im_divide Im_exp)
-
-
-subsection {* More Corollaries about Sine and Cosine *}
-
-lemma sin_times_pi_eq_0: "sin(x * pi) = 0 \<longleftrightarrow> x \<in> Ints"
- by (simp add: sin_zero_iff_int2) (metis Ints_cases Ints_real_of_int real_of_int_def)
-
-lemma cos_one_2pi:
- "cos(x) = 1 \<longleftrightarrow> (\<exists>n::nat. x = n * 2*pi) | (\<exists>n::nat. x = -(n * 2*pi))"
- (is "?lhs = ?rhs")
-proof
- assume "cos(x) = 1"
- then have "sin x = 0"
- by (simp add: cos_one_sin_zero)
- then show ?rhs
- proof (simp only: sin_zero_iff, elim exE disjE conjE)
- fix n::nat
- assume n: "even n" "x = real n * (pi/2)"
- then obtain m where m: "n = 2 * m"
- using dvdE by blast
- then have me: "even m" using `?lhs` n
- by (auto simp: field_simps) (metis one_neq_neg_one power_minus_odd power_one)
- show ?rhs
- using m me n
- by (auto simp: field_simps elim!: evenE)
- next
- fix n::nat
- assume n: "even n" "x = - (real n * (pi/2))"
- then obtain m where m: "n = 2 * m"
- using dvdE by blast
- then have me: "even m" using `?lhs` n
- by (auto simp: field_simps) (metis one_neq_neg_one power_minus_odd power_one)
- show ?rhs
- using m me n
- by (auto simp: field_simps elim!: evenE)
- qed
-next
- assume "?rhs"
- then show "cos x = 1"
- by (metis cos_2npi cos_minus mult.assoc mult.left_commute)
-qed
-
-lemma cos_one_2pi_int: "cos(x) = 1 \<longleftrightarrow> (\<exists>n::int. x = n * 2*pi)"
- apply auto --{*FIXME simproc bug*}
- apply (auto simp: cos_one_2pi)
- apply (metis real_of_int_of_nat_eq)
- apply (metis mult_minus_right real_of_int_minus real_of_int_of_nat_eq)
- by (metis mult_minus_right of_int_of_nat real_of_int_def real_of_nat_def)
-
-lemma sin_cos_sqrt: "0 \<le> sin(x) \<Longrightarrow> (sin(x) = sqrt(1 - (cos(x) ^ 2)))"
- using sin_squared_eq real_sqrt_unique by fastforce
-
-lemma sin_eq_0_pi: "-pi < x \<Longrightarrow> x < pi \<Longrightarrow> sin(x) = 0 \<Longrightarrow> x = 0"
- by (metis sin_gt_zero sin_minus minus_less_iff neg_0_less_iff_less not_less_iff_gr_or_eq)
-
-lemma cos_treble_cos:
- fixes x :: "'a::{real_normed_field,banach}"
- shows "cos(3 * x) = 4 * cos(x) ^ 3 - 3 * cos x"
-proof -
- have *: "(sin x * (sin x * 3)) = 3 - (cos x * (cos x * 3))"
- by (simp add: mult.assoc [symmetric] sin_squared_eq [unfolded power2_eq_square])
- have "cos(3 * x) = cos(2*x + x)"
- by simp
- also have "... = 4 * cos(x) ^ 3 - 3 * cos x"
- apply (simp only: cos_add cos_double sin_double)
- apply (simp add: * field_simps power2_eq_square power3_eq_cube)
- done
- finally show ?thesis .
-qed
-
subsection{*More on the Polar Representation of Complex Numbers*}
-lemma cos_integer_2pi: "n \<in> Ints \<Longrightarrow> cos(2*pi * n) = 1"
- by (metis Ints_cases cos_one_2pi_int mult.assoc mult.commute real_of_int_def)
-
-lemma sin_integer_2pi: "n \<in> Ints \<Longrightarrow> sin(2*pi * n) = 0"
- by (metis sin_two_pi Ints_mult mult.assoc mult.commute sin_times_pi_eq_0)
-
-lemma cos_int_2npi [simp]: "cos (2 * real (n::int) * pi) = 1"
- by (simp add: cos_one_2pi_int)
-
-lemma sin_int_2npi [simp]: "sin (2 * real (n::int) * pi) = 0"
- by (metis Ints_real_of_int mult.assoc mult.commute sin_integer_2pi)
-
-lemma sincos_principal_value: "\<exists>y. (-pi < y \<and> y \<le> pi) \<and> (sin(y) = sin(x) \<and> cos(y) = cos(x))"
- apply (rule exI [where x="pi - (2*pi) * frac((pi - x) / (2*pi))"])
- apply (auto simp: field_simps frac_lt_1)
- apply (simp_all add: frac_def divide_simps)
- apply (simp_all add: add_divide_distrib diff_divide_distrib)
- apply (simp_all add: sin_diff cos_diff mult.assoc [symmetric] cos_integer_2pi sin_integer_2pi)
- done
-
lemma exp_Complex: "exp(Complex r t) = of_real(exp r) * Complex (cos t) (sin t)"
by (simp add: exp_add exp_Euler exp_of_real)
-
-
lemma exp_eq_1: "exp z = 1 \<longleftrightarrow> Re(z) = 0 \<and> (\<exists>n::int. Im(z) = of_int (2 * n) * pi)"
apply auto
apply (metis exp_eq_one_iff norm_exp_eq_Re norm_one)
@@ -667,6 +575,13 @@
end (* of context *)
+text{*32-bit Approximation to e*}
+lemma e_approx_32: "abs(exp(1) - 5837465777 / 2147483648) \<le> (inverse(2 ^ 32)::real)"
+ using Taylor_exp [of 1 14] exp_le
+ apply (simp add: setsum_left_distrib in_Reals_norm Re_exp atMost_nat_numeral fact_numeral)
+ apply (simp only: pos_le_divide_eq [symmetric], linarith)
+ done
+
subsection{*The argument of a complex number*}
definition Arg :: "complex \<Rightarrow> real" where
@@ -888,7 +803,6 @@
apply auto
by (metis Arg_eq_0 less_irrefl minus_diff_eq right_minus_eq)
-
lemma Arg_add:
assumes "w \<noteq> 0" "z \<noteq> 0"
shows "Arg w + Arg z = (if Arg w + Arg z < 2*pi then Arg(w * z) else Arg(w * z) + 2*pi)"
@@ -921,4 +835,470 @@
lemma Arg_exp: "0 \<le> Im z \<Longrightarrow> Im z < 2*pi \<Longrightarrow> Arg(exp z) = Im z"
by (rule Arg_unique [of "exp(Re z)"]) (auto simp: Exp_eq_polar)
+
+subsection{*Analytic properties of tangent function*}
+
+lemma cnj_tan: "cnj(tan z) = tan(cnj z)"
+ by (simp add: cnj_cos cnj_sin tan_def)
+
+lemma complex_differentiable_at_tan: "~(cos z = 0) \<Longrightarrow> tan complex_differentiable at z"
+ unfolding complex_differentiable_def
+ using DERIV_tan by blast
+
+lemma complex_differentiable_within_tan: "~(cos z = 0)
+ \<Longrightarrow> tan complex_differentiable (at z within s)"
+ using complex_differentiable_at_tan complex_differentiable_at_within by blast
+
+lemma continuous_within_tan: "~(cos z = 0) \<Longrightarrow> continuous (at z within s) tan"
+ using continuous_at_imp_continuous_within isCont_tan by blast
+
+lemma continuous_on_tan [continuous_intros]: "(\<And>z. z \<in> s \<Longrightarrow> ~(cos z = 0)) \<Longrightarrow> continuous_on s tan"
+ by (simp add: continuous_at_imp_continuous_on)
+
+lemma holomorphic_on_tan: "(\<And>z. z \<in> s \<Longrightarrow> ~(cos z = 0)) \<Longrightarrow> tan holomorphic_on s"
+ by (simp add: complex_differentiable_within_tan holomorphic_on_def)
+
+
+subsection{*Complex logarithms (the conventional principal value)*}
+
+definition Ln where
+ "Ln \<equiv> \<lambda>z. THE w. exp w = z & -pi < Im(w) & Im(w) \<le> pi"
+
+lemma
+ assumes "z \<noteq> 0"
+ shows exp_Ln [simp]: "exp(Ln z) = z"
+ and mpi_less_Im_Ln: "-pi < Im(Ln z)"
+ and Im_Ln_le_pi: "Im(Ln z) \<le> pi"
+proof -
+ obtain \<psi> where z: "z / (cmod z) = Complex (cos \<psi>) (sin \<psi>)"
+ using complex_unimodular_polar [of "z / (norm z)"] assms
+ by (auto simp: norm_divide divide_simps)
+ obtain \<phi> where \<phi>: "- pi < \<phi>" "\<phi> \<le> pi" "sin \<phi> = sin \<psi>" "cos \<phi> = cos \<psi>"
+ using sincos_principal_value [of "\<psi>"] assms
+ by (auto simp: norm_divide divide_simps)
+ have "exp(Ln z) = z & -pi < Im(Ln z) & Im(Ln z) \<le> pi" unfolding Ln_def
+ apply (rule theI [where a = "Complex (ln(norm z)) \<phi>"])
+ using z assms \<phi>
+ apply (auto simp: field_simps exp_complex_eqI Exp_eq_polar cis.code)
+ done
+ then show "exp(Ln z) = z" "-pi < Im(Ln z)" "Im(Ln z) \<le> pi"
+ by auto
+qed
+
+lemma Ln_exp [simp]:
+ assumes "-pi < Im(z)" "Im(z) \<le> pi"
+ shows "Ln(exp z) = z"
+ apply (rule exp_complex_eqI)
+ using assms mpi_less_Im_Ln [of "exp z"] Im_Ln_le_pi [of "exp z"]
+ apply auto
+ done
+
+lemma Ln_eq_iff: "w \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> (Ln w = Ln z \<longleftrightarrow> w = z)"
+ by (metis exp_Ln)
+
+lemma Ln_unique: "exp(z) = w \<Longrightarrow> -pi < Im(z) \<Longrightarrow> Im(z) \<le> pi \<Longrightarrow> Ln w = z"
+ using Ln_exp by blast
+
+lemma Re_Ln [simp]: "z \<noteq> 0 \<Longrightarrow> Re(Ln z) = ln(norm z)"
+by (metis exp_Ln assms ln_exp norm_exp_eq_Re)
+
+lemma exists_complex_root:
+ fixes a :: complex
+ shows "n \<noteq> 0 \<Longrightarrow> \<exists>z. z ^ n = a"
+ apply (cases "a=0", simp)
+ apply (rule_tac x= "exp(Ln(a) / n)" in exI)
+ apply (auto simp: exp_of_nat_mult [symmetric])
+ done
+
+subsection{*Derivative of Ln away from the branch cut*}
+
+lemma
+ assumes "Im(z) = 0 \<Longrightarrow> 0 < Re(z)"
+ shows has_field_derivative_Ln: "(Ln has_field_derivative inverse(z)) (at z)"
+ and Im_Ln_less_pi: "Im (Ln z) < pi"
+proof -
+ have znz: "z \<noteq> 0"
+ using assms by auto
+ then show *: "Im (Ln z) < pi" using assms
+ by (metis exp_Ln Im_Ln_le_pi Im_exp Re_exp abs_of_nonneg cmod_eq_Re cos_pi mult.right_neutral mult_minus_right mult_zero_right neg_less_0_iff_less norm_exp_eq_Re not_less not_less_iff_gr_or_eq sin_pi)
+ show "(Ln has_field_derivative inverse(z)) (at z)"
+ apply (rule has_complex_derivative_inverse_strong_x
+ [where f = exp and s = "{w. -pi < Im(w) & Im(w) < pi}"])
+ using znz *
+ apply (auto simp: continuous_on_exp open_Collect_conj open_halfspace_Im_gt open_halfspace_Im_lt)
+ apply (metis DERIV_exp exp_Ln)
+ apply (metis mpi_less_Im_Ln)
+ done
+qed
+
+declare has_field_derivative_Ln [derivative_intros]
+declare has_field_derivative_Ln [THEN DERIV_chain2, derivative_intros]
+
+lemma complex_differentiable_at_Ln: "(Im(z) = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> Ln complex_differentiable at z"
+ using complex_differentiable_def has_field_derivative_Ln by blast
+
+lemma complex_differentiable_within_Ln: "(Im(z) = 0 \<Longrightarrow> 0 < Re(z))
+ \<Longrightarrow> Ln complex_differentiable (at z within s)"
+ using complex_differentiable_at_Ln complex_differentiable_within_subset by blast
+
+lemma continuous_at_Ln: "(Im(z) = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous (at z) Ln"
+ by (simp add: complex_differentiable_imp_continuous_at complex_differentiable_within_Ln)
+
+lemma continuous_within_Ln: "(Im(z) = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous (at z within s) Ln"
+ using continuous_at_Ln continuous_at_imp_continuous_within by blast
+
+lemma continuous_on_Ln [continuous_intros]: "(\<And>z. z \<in> s \<Longrightarrow> Im(z) = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous_on s Ln"
+ by (simp add: continuous_at_imp_continuous_on continuous_within_Ln)
+
+lemma holomorphic_on_Ln: "(\<And>z. z \<in> s \<Longrightarrow> Im(z) = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> Ln holomorphic_on s"
+ by (simp add: complex_differentiable_within_Ln holomorphic_on_def)
+
+
+subsection{*Relation to Real Logarithm*}
+
+lemma ln_of_real:
+ assumes "0 < z"
+ shows "Ln(of_real z) = of_real(ln z)"
+proof -
+ have "Ln(of_real (exp (ln z))) = Ln (exp (of_real (ln z)))"
+ by (simp add: exp_of_real)
+ also have "... = of_real(ln z)"
+ using assms
+ by (subst Ln_exp) auto
+ finally show ?thesis
+ using assms by simp
+qed
+
+
+subsection{*Quadrant-type results for Ln*}
+
+lemma cos_lt_zero_pi: "pi/2 < x \<Longrightarrow> x < 3*pi/2 \<Longrightarrow> cos x < 0"
+ using cos_minus_pi cos_gt_zero_pi [of "x-pi"]
+ by simp
+
+lemma Re_Ln_pos_lt:
+ assumes "z \<noteq> 0"
+ shows "abs(Im(Ln z)) < pi/2 \<longleftrightarrow> 0 < Re(z)"
+proof -
+ { fix w
+ assume "w = Ln z"
+ then have w: "Im w \<le> pi" "- pi < Im w"
+ using Im_Ln_le_pi [of z] mpi_less_Im_Ln [of z] assms
+ by auto
+ then have "abs(Im w) < pi/2 \<longleftrightarrow> 0 < Re(exp w)"
+ apply (auto simp: Re_exp zero_less_mult_iff cos_gt_zero_pi)
+ using cos_lt_zero_pi [of "-(Im w)"] cos_lt_zero_pi [of "(Im w)"]
+ apply (simp add: abs_if split: split_if_asm)
+ apply (metis (no_types) cos_minus cos_pi_half eq_divide_eq_numeral1(1) eq_numeral_simps(4)
+ less_numeral_extra(3) linorder_neqE_linordered_idom minus_mult_minus minus_mult_right
+ mult_numeral_1_right)
+ done
+ }
+ then show ?thesis using assms
+ by auto
+qed
+
+lemma Re_Ln_pos_le:
+ assumes "z \<noteq> 0"
+ shows "abs(Im(Ln z)) \<le> pi/2 \<longleftrightarrow> 0 \<le> Re(z)"
+proof -
+ { fix w
+ assume "w = Ln z"
+ then have w: "Im w \<le> pi" "- pi < Im w"
+ using Im_Ln_le_pi [of z] mpi_less_Im_Ln [of z] assms
+ by auto
+ then have "abs(Im w) \<le> pi/2 \<longleftrightarrow> 0 \<le> Re(exp w)"
+ apply (auto simp: Re_exp zero_le_mult_iff cos_ge_zero)
+ using cos_lt_zero_pi [of "- (Im w)"] cos_lt_zero_pi [of "(Im w)"] not_le
+ apply (auto simp: abs_if split: split_if_asm)
+ done
+ }
+ then show ?thesis using assms
+ by auto
+qed
+
+lemma Im_Ln_pos_lt:
+ assumes "z \<noteq> 0"
+ shows "0 < Im(Ln z) \<and> Im(Ln z) < pi \<longleftrightarrow> 0 < Im(z)"
+proof -
+ { fix w
+ assume "w = Ln z"
+ then have w: "Im w \<le> pi" "- pi < Im w"
+ using Im_Ln_le_pi [of z] mpi_less_Im_Ln [of z] assms
+ by auto
+ then have "0 < Im w \<and> Im w < pi \<longleftrightarrow> 0 < Im(exp w)"
+ using sin_gt_zero [of "- (Im w)"] sin_gt_zero [of "(Im w)"]
+ apply (auto simp: Im_exp zero_less_mult_iff)
+ using less_linear apply fastforce
+ using less_linear apply fastforce
+ done
+ }
+ then show ?thesis using assms
+ by auto
+qed
+
+lemma Im_Ln_pos_le:
+ assumes "z \<noteq> 0"
+ shows "0 \<le> Im(Ln z) \<and> Im(Ln z) \<le> pi \<longleftrightarrow> 0 \<le> Im(z)"
+proof -
+ { fix w
+ assume "w = Ln z"
+ then have w: "Im w \<le> pi" "- pi < Im w"
+ using Im_Ln_le_pi [of z] mpi_less_Im_Ln [of z] assms
+ by auto
+ then have "0 \<le> Im w \<and> Im w \<le> pi \<longleftrightarrow> 0 \<le> Im(exp w)"
+ using sin_ge_zero [of "- (Im w)"] sin_ge_zero [of "(Im w)"]
+ apply (auto simp: Im_exp zero_le_mult_iff sin_ge_zero)
+ apply (metis not_le not_less_iff_gr_or_eq pi_not_less_zero sin_eq_0_pi)
+ done }
+ then show ?thesis using assms
+ by auto
+qed
+
+lemma Re_Ln_pos_lt_imp: "0 < Re(z) \<Longrightarrow> abs(Im(Ln z)) < pi/2"
+ by (metis Re_Ln_pos_lt less_irrefl zero_complex.simps(1))
+
+lemma Im_Ln_pos_lt_imp: "0 < Im(z) \<Longrightarrow> 0 < Im(Ln z) \<and> Im(Ln z) < pi"
+ by (metis Im_Ln_pos_lt not_le order_refl zero_complex.simps(2))
+
+lemma Im_Ln_eq_0: "z \<noteq> 0 \<Longrightarrow> (Im(Ln z) = 0 \<longleftrightarrow> 0 < Re(z) \<and> Im(z) = 0)"
+ by (metis exp_Ln Im_Ln_less_pi Im_Ln_pos_le Im_Ln_pos_lt Re_complex_of_real add.commute add.left_neutral
+ complex_eq exp_of_real le_less mult_zero_right norm_exp_eq_Re norm_le_zero_iff not_le of_real_0)
+
+lemma Im_Ln_eq_pi: "z \<noteq> 0 \<Longrightarrow> (Im(Ln z) = pi \<longleftrightarrow> Re(z) < 0 \<and> Im(z) = 0)"
+ by (metis Im_Ln_eq_0 Im_Ln_less_pi Im_Ln_pos_le Im_Ln_pos_lt add.right_neutral complex_eq mult_zero_right not_less not_less_iff_gr_or_eq of_real_0)
+
+
+subsection{*More Properties of Ln*}
+
+lemma cnj_Ln: "(Im z = 0 \<Longrightarrow> 0 < Re z) \<Longrightarrow> cnj(Ln z) = Ln(cnj z)"
+ apply (cases "z=0", auto)
+ apply (rule exp_complex_eqI)
+ apply (auto simp: abs_if split: split_if_asm)
+ apply (metis Im_Ln_less_pi add_mono_thms_linordered_field(5) cnj.simps(1) cnj.simps(2) mult_2 neg_equal_0_iff_equal)
+ apply (metis add_mono_thms_linordered_field(5) complex_cnj_zero_iff diff_0_right diff_minus_eq_add minus_diff_eq mpi_less_Im_Ln mult.commute mult_2_right neg_less_iff_less)
+ by (metis exp_Ln exp_cnj)
+
+lemma Ln_inverse: "(Im(z) = 0 \<Longrightarrow> 0 < Re z) \<Longrightarrow> Ln(inverse z) = -(Ln z)"
+ apply (cases "z=0", auto)
+ apply (rule exp_complex_eqI)
+ using mpi_less_Im_Ln [of z] mpi_less_Im_Ln [of "inverse z"]
+ apply (auto simp: abs_if exp_minus split: split_if_asm)
+ apply (metis Im_Ln_less_pi Im_Ln_pos_le add_less_cancel_left add_strict_mono
+ inverse_inverse_eq inverse_zero le_less mult.commute mult_2_right)
+ done
+
+lemma Ln_1 [simp]: "Ln(1) = 0"
+proof -
+ have "Ln (exp 0) = 0"
+ by (metis exp_zero ln_exp ln_of_real of_real_0 of_real_1 zero_less_one)
+ then show ?thesis
+ by simp
+qed
+
+lemma Ln_minus1 [simp]: "Ln(-1) = ii * pi"
+ apply (rule exp_complex_eqI)
+ using Im_Ln_le_pi [of "-1"] mpi_less_Im_Ln [of "-1"] cis_conv_exp cis_pi
+ apply (auto simp: abs_if)
+ done
+
+lemma Ln_ii [simp]: "Ln ii = ii * of_real pi/2"
+ using Ln_exp [of "ii * (of_real pi/2)"]
+ unfolding exp_Euler
+ by simp
+
+lemma Ln_minus_ii [simp]: "Ln(-ii) = - (ii * pi/2)"
+proof -
+ have "Ln(-ii) = Ln(1/ii)"
+ by simp
+ also have "... = - (Ln ii)"
+ by (metis Ln_inverse ii.sel(2) inverse_eq_divide zero_neq_one)
+ also have "... = - (ii * pi/2)"
+ by (simp add: Ln_ii)
+ finally show ?thesis .
+qed
+
+lemma Ln_times:
+ assumes "w \<noteq> 0" "z \<noteq> 0"
+ shows "Ln(w * z) =
+ (if Im(Ln w + Ln z) \<le> -pi then
+ (Ln(w) + Ln(z)) + ii * of_real(2*pi)
+ else if Im(Ln w + Ln z) > pi then
+ (Ln(w) + Ln(z)) - ii * of_real(2*pi)
+ else Ln(w) + Ln(z))"
+ using pi_ge_zero Im_Ln_le_pi [of w] Im_Ln_le_pi [of z]
+ using assms mpi_less_Im_Ln [of w] mpi_less_Im_Ln [of z]
+ by (auto simp: of_real_numeral exp_add exp_diff sin_double cos_double exp_Euler intro!: Ln_unique)
+
+lemma Ln_times_simple:
+ "\<lbrakk>w \<noteq> 0; z \<noteq> 0; -pi < Im(Ln w) + Im(Ln z); Im(Ln w) + Im(Ln z) \<le> pi\<rbrakk>
+ \<Longrightarrow> Ln(w * z) = Ln(w) + Ln(z)"
+ by (simp add: Ln_times)
+
+lemma Ln_minus:
+ assumes "z \<noteq> 0"
+ shows "Ln(-z) = (if Im(z) \<le> 0 \<and> ~(Re(z) < 0 \<and> Im(z) = 0)
+ then Ln(z) + ii * pi
+ else Ln(z) - ii * pi)" (is "_ = ?rhs")
+ using Im_Ln_le_pi [of z] mpi_less_Im_Ln [of z] assms
+ Im_Ln_eq_pi [of z] Im_Ln_pos_lt [of z]
+ by (auto simp: of_real_numeral exp_add exp_diff exp_Euler intro!: Ln_unique)
+
+lemma Ln_inverse_if:
+ assumes "z \<noteq> 0"
+ shows "Ln (inverse z) =
+ (if (Im(z) = 0 \<longrightarrow> 0 < Re z)
+ then -(Ln z)
+ else -(Ln z) + \<i> * 2 * complex_of_real pi)"
+proof (cases "(Im(z) = 0 \<longrightarrow> 0 < Re z)")
+ case True then show ?thesis
+ by (simp add: Ln_inverse)
+next
+ case False
+ then have z: "Im z = 0" "Re z < 0"
+ using assms
+ apply auto
+ by (metis cnj.code complex_cnj_cnj not_less_iff_gr_or_eq zero_complex.simps(1) zero_complex.simps(2))
+ have "Ln(inverse z) = Ln(- (inverse (-z)))"
+ by simp
+ also have "... = Ln (inverse (-z)) + \<i> * complex_of_real pi"
+ using assms z
+ apply (simp add: Ln_minus)
+ apply (simp add: field_simps)
+ done
+ also have "... = - Ln (- z) + \<i> * complex_of_real pi"
+ apply (subst Ln_inverse)
+ using z assms by auto
+ also have "... = - (Ln z) + \<i> * 2 * complex_of_real pi"
+ apply (subst Ln_minus [OF assms])
+ using assms z
+ apply simp
+ done
+ finally show ?thesis
+ using assms z
+ by simp
+qed
+
+lemma Ln_times_ii:
+ assumes "z \<noteq> 0"
+ shows "Ln(ii * z) = (if 0 \<le> Re(z) | Im(z) < 0
+ then Ln(z) + ii * of_real pi/2
+ else Ln(z) - ii * of_real(3 * pi/2))"
+ using Im_Ln_le_pi [of z] mpi_less_Im_Ln [of z] assms
+ Im_Ln_eq_pi [of z] Im_Ln_pos_lt [of z] Re_Ln_pos_le [of z]
+ by (auto simp: of_real_numeral Ln_times)
+
+
+subsection{*Relation between Square Root and exp/ln, hence its derivative*}
+
+lemma csqrt_exp_Ln:
+ assumes "z \<noteq> 0"
+ shows "csqrt z = exp(Ln(z) / 2)"
+proof -
+ have "(exp (Ln z / 2))\<^sup>2 = (exp (Ln z))"
+ by (metis exp_double nonzero_mult_divide_cancel_left times_divide_eq_right zero_neq_numeral)
+ also have "... = z"
+ using assms exp_Ln by blast
+ finally have "csqrt z = csqrt ((exp (Ln z / 2))\<^sup>2)"
+ by simp
+ also have "... = exp (Ln z / 2)"
+ apply (subst csqrt_square)
+ using cos_gt_zero_pi [of "(Im (Ln z) / 2)"] Im_Ln_le_pi mpi_less_Im_Ln assms
+ apply (auto simp: Re_exp Im_exp zero_less_mult_iff zero_le_mult_iff, fastforce+)
+ done
+ finally show ?thesis using assms csqrt_square
+ by simp
+qed
+
+lemma csqrt_inverse:
+ assumes "Im(z) = 0 \<Longrightarrow> 0 < Re z"
+ shows "csqrt (inverse z) = inverse (csqrt z)"
+proof (cases "z=0", simp)
+ assume "z \<noteq> 0 "
+ then show ?thesis
+ using assms
+ by (simp add: csqrt_exp_Ln Ln_inverse exp_minus)
+qed
+
+lemma cnj_csqrt:
+ assumes "Im z = 0 \<Longrightarrow> 0 \<le> Re(z)"
+ shows "cnj(csqrt z) = csqrt(cnj z)"
+proof (cases "z=0", simp)
+ assume z: "z \<noteq> 0"
+ then have "Im z = 0 \<Longrightarrow> 0 < Re(z)"
+ using assms cnj.code complex_cnj_zero_iff by fastforce
+ then show ?thesis
+ using z by (simp add: csqrt_exp_Ln cnj_Ln exp_cnj)
+qed
+
+lemma has_field_derivative_csqrt:
+ assumes "Im z = 0 \<Longrightarrow> 0 < Re(z)"
+ shows "(csqrt has_field_derivative inverse(2 * csqrt z)) (at z)"
+proof -
+ have z: "z \<noteq> 0"
+ using assms by auto
+ then have *: "inverse z = inverse (2*z) * 2"
+ by (simp add: divide_simps)
+ show ?thesis
+ apply (rule DERIV_transform_at [where f = "\<lambda>z. exp(Ln(z) / 2)" and d = "norm z"])
+ apply (intro derivative_eq_intros | simp add: assms)+
+ apply (rule *)
+ using z
+ apply (auto simp: field_simps csqrt_exp_Ln [symmetric])
+ apply (metis power2_csqrt power2_eq_square)
+ apply (metis csqrt_exp_Ln dist_0_norm less_irrefl)
+ done
+qed
+
+lemma complex_differentiable_at_csqrt:
+ "(Im z = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> csqrt complex_differentiable at z"
+ using complex_differentiable_def has_field_derivative_csqrt by blast
+
+lemma complex_differentiable_within_csqrt:
+ "(Im z = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> csqrt complex_differentiable (at z within s)"
+ using complex_differentiable_at_csqrt complex_differentiable_within_subset by blast
+
+lemma continuous_at_csqrt:
+ "(Im z = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous (at z) csqrt"
+ by (simp add: complex_differentiable_within_csqrt complex_differentiable_imp_continuous_at)
+
+lemma continuous_within_csqrt:
+ "(Im z = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous (at z within s) csqrt"
+ by (simp add: complex_differentiable_imp_continuous_at complex_differentiable_within_csqrt)
+
+lemma continuous_on_csqrt [continuous_intros]:
+ "(\<And>z. z \<in> s \<and> Im z = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous_on s csqrt"
+ by (simp add: continuous_at_imp_continuous_on continuous_within_csqrt)
+
+lemma holomorphic_on_csqrt:
+ "(\<And>z. z \<in> s \<and> Im z = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> csqrt holomorphic_on s"
+ by (simp add: complex_differentiable_within_csqrt holomorphic_on_def)
+
+lemma continuous_within_closed_nontrivial:
+ "closed s \<Longrightarrow> a \<notin> s ==> continuous (at a within s) f"
+ using open_Compl
+ by (force simp add: continuous_def eventually_at_topological filterlim_iff open_Collect_neg)
+
+lemma closed_Real_halfspace_Re_ge: "closed (\<real> \<inter> {w. x \<le> Re(w)})"
+ using closed_halfspace_Re_ge
+ by (simp add: closed_Int closed_complex_Reals)
+
+lemma continuous_within_csqrt_posreal:
+ "continuous (at z within (\<real> \<inter> {w. 0 \<le> Re(w)})) csqrt"
+proof (cases "Im z = 0 --> 0 < Re(z)")
+ case True then show ?thesis
+ by (blast intro: continuous_within_csqrt)
+next
+ case False
+ then have "Im z = 0" "Re z < 0 \<or> z = 0"
+ using False cnj.code complex_cnj_zero_iff by auto force
+ then show ?thesis
+ apply (auto simp: continuous_within_closed_nontrivial [OF closed_Real_halfspace_Re_ge])
+ apply (auto simp: continuous_within_eps_delta norm_conv_dist [symmetric])
+ apply (rule_tac x="e^2" in exI)
+ apply (auto simp: Reals_def)
+by (metis linear not_less real_sqrt_less_iff real_sqrt_pow2_iff real_sqrt_power)
+qed
+
+
end
--- a/src/HOL/Transcendental.thy Thu Mar 19 11:54:20 2015 +0100
+++ b/src/HOL/Transcendental.thy Thu Mar 19 14:24:51 2015 +0000
@@ -3391,7 +3391,7 @@
thus ?thesis by auto
qed
-lemma cos_monotone_0_pi':
+lemma cos_monotone_0_pi_le:
assumes "0 \<le> y" and "y \<le> x" and "x \<le> pi"
shows "cos x \<le> cos y"
proof (cases "y < x")
@@ -3427,16 +3427,19 @@
thus ?thesis by auto
qed
-lemma sin_monotone_2pi':
+lemma sin_monotone_2pi:
+ assumes "- (pi/2) \<le> y" and "y < x" and "x \<le> pi/2"
+ shows "sin y < sin x"
+ apply (simp add: sin_cos_eq)
+ apply (rule cos_monotone_0_pi)
+ using assms
+ apply auto
+ done
+
+lemma sin_monotone_2pi_le:
assumes "- (pi / 2) \<le> y" and "y \<le> x" and "x \<le> pi / 2"
shows "sin y \<le> sin x"
-proof -
- have "0 \<le> y + pi / 2" and "y + pi / 2 \<le> x + pi / 2" and "x + pi /2 \<le> pi"
- using pi_ge_two and assms by auto
- from cos_monotone_0_pi'[OF this] show ?thesis
- unfolding minus_sin_cos_eq[symmetric]
- by (metis minus_sin_cos_eq mult.right_neutral neg_le_iff_le of_real_def real_scaleR_def)
-qed
+ by (metis assms le_less sin_monotone_2pi)
lemma sin_x_le_x:
fixes x::real assumes x: "x \<ge> 0" shows "sin x \<le> x"
@@ -3468,6 +3471,191 @@
by (auto simp: abs_real_def)
+subsection {* More Corollaries about Sine and Cosine *}
+
+lemma sin_cos_npi [simp]: "sin (real (Suc (2 * n)) * pi / 2) = (-1) ^ n"
+proof -
+ have "sin ((real n + 1/2) * pi) = cos (real n * pi)"
+ by (auto simp: algebra_simps sin_add)
+ thus ?thesis
+ by (simp add: real_of_nat_Suc distrib_right add_divide_distrib
+ mult.commute [of pi])
+qed
+
+lemma cos_2npi [simp]: "cos (2 * real (n::nat) * pi) = 1"
+ by (cases "even n") (simp_all add: cos_double mult.assoc)
+
+lemma cos_3over2_pi [simp]: "cos (3/2*pi) = 0"
+ apply (subgoal_tac "cos (pi + pi/2) = 0", simp)
+ apply (subst cos_add, simp)
+ done
+
+lemma sin_2npi [simp]: "sin (2 * real (n::nat) * pi) = 0"
+ by (auto simp: mult.assoc sin_double)
+
+lemma sin_3over2_pi [simp]: "sin (3/2*pi) = - 1"
+ apply (subgoal_tac "sin (pi + pi/2) = - 1", simp)
+ apply (subst sin_add, simp)
+ done
+
+lemma cos_pi_eq_zero [simp]: "cos (pi * real (Suc (2 * m)) / 2) = 0"
+by (simp only: cos_add sin_add real_of_nat_Suc distrib_right distrib_left add_divide_distrib, auto)
+
+lemma DERIV_cos_add [simp]: "DERIV (\<lambda>x. cos (x + k)) xa :> - sin (xa + k)"
+ by (auto intro!: derivative_eq_intros)
+
+lemma sin_zero_norm_cos_one:
+ fixes x :: "'a::{real_normed_field,banach}"
+ assumes "sin x = 0" shows "norm (cos x) = 1"
+ using sin_cos_squared_add [of x, unfolded assms]
+ by (simp add: square_norm_one)
+
+lemma sin_zero_abs_cos_one: "sin x = 0 \<Longrightarrow> \<bar>cos x\<bar> = (1::real)"
+ using sin_zero_norm_cos_one by fastforce
+
+lemma cos_one_sin_zero:
+ fixes x :: "'a::{real_normed_field,banach}"
+ assumes "cos x = 1" shows "sin x = 0"
+ using sin_cos_squared_add [of x, unfolded assms]
+ by simp
+
+lemma sin_times_pi_eq_0: "sin(x * pi) = 0 \<longleftrightarrow> x \<in> Ints"
+ by (simp add: sin_zero_iff_int2) (metis Ints_cases Ints_real_of_int real_of_int_def)
+
+lemma cos_one_2pi:
+ "cos(x) = 1 \<longleftrightarrow> (\<exists>n::nat. x = n * 2*pi) | (\<exists>n::nat. x = -(n * 2*pi))"
+ (is "?lhs = ?rhs")
+proof
+ assume "cos(x) = 1"
+ then have "sin x = 0"
+ by (simp add: cos_one_sin_zero)
+ then show ?rhs
+ proof (simp only: sin_zero_iff, elim exE disjE conjE)
+ fix n::nat
+ assume n: "even n" "x = real n * (pi/2)"
+ then obtain m where m: "n = 2 * m"
+ using dvdE by blast
+ then have me: "even m" using `?lhs` n
+ by (auto simp: field_simps) (metis one_neq_neg_one power_minus_odd power_one)
+ show ?rhs
+ using m me n
+ by (auto simp: field_simps elim!: evenE)
+ next
+ fix n::nat
+ assume n: "even n" "x = - (real n * (pi/2))"
+ then obtain m where m: "n = 2 * m"
+ using dvdE by blast
+ then have me: "even m" using `?lhs` n
+ by (auto simp: field_simps) (metis one_neq_neg_one power_minus_odd power_one)
+ show ?rhs
+ using m me n
+ by (auto simp: field_simps elim!: evenE)
+ qed
+next
+ assume "?rhs"
+ then show "cos x = 1"
+ by (metis cos_2npi cos_minus mult.assoc mult.left_commute)
+qed
+
+lemma cos_one_2pi_int: "cos(x) = 1 \<longleftrightarrow> (\<exists>n::int. x = n * 2*pi)"
+ apply auto --{*FIXME simproc bug*}
+ apply (auto simp: cos_one_2pi)
+ apply (metis real_of_int_of_nat_eq)
+ apply (metis mult_minus_right real_of_int_minus real_of_int_of_nat_eq)
+ by (metis mult_minus_right of_int_of_nat real_of_int_def real_of_nat_def)
+
+lemma sin_cos_sqrt: "0 \<le> sin(x) \<Longrightarrow> (sin(x) = sqrt(1 - (cos(x) ^ 2)))"
+ using sin_squared_eq real_sqrt_unique by fastforce
+
+lemma sin_eq_0_pi: "-pi < x \<Longrightarrow> x < pi \<Longrightarrow> sin(x) = 0 \<Longrightarrow> x = 0"
+ by (metis sin_gt_zero sin_minus minus_less_iff neg_0_less_iff_less not_less_iff_gr_or_eq)
+
+lemma cos_treble_cos:
+ fixes x :: "'a::{real_normed_field,banach}"
+ shows "cos(3 * x) = 4 * cos(x) ^ 3 - 3 * cos x"
+proof -
+ have *: "(sin x * (sin x * 3)) = 3 - (cos x * (cos x * 3))"
+ by (simp add: mult.assoc [symmetric] sin_squared_eq [unfolded power2_eq_square])
+ have "cos(3 * x) = cos(2*x + x)"
+ by simp
+ also have "... = 4 * cos(x) ^ 3 - 3 * cos x"
+ apply (simp only: cos_add cos_double sin_double)
+ apply (simp add: * field_simps power2_eq_square power3_eq_cube)
+ done
+ finally show ?thesis .
+qed
+
+lemma cos_45: "cos (pi / 4) = sqrt 2 / 2"
+proof -
+ let ?c = "cos (pi / 4)" and ?s = "sin (pi / 4)"
+ have nonneg: "0 \<le> ?c"
+ by (simp add: cos_ge_zero)
+ have "0 = cos (pi / 4 + pi / 4)"
+ by simp
+ also have "cos (pi / 4 + pi / 4) = ?c\<^sup>2 - ?s\<^sup>2"
+ by (simp only: cos_add power2_eq_square)
+ also have "\<dots> = 2 * ?c\<^sup>2 - 1"
+ by (simp add: sin_squared_eq)
+ finally have "?c\<^sup>2 = (sqrt 2 / 2)\<^sup>2"
+ by (simp add: power_divide)
+ thus ?thesis
+ using nonneg by (rule power2_eq_imp_eq) simp
+qed
+
+lemma cos_30: "cos (pi / 6) = sqrt 3/2"
+proof -
+ let ?c = "cos (pi / 6)" and ?s = "sin (pi / 6)"
+ have pos_c: "0 < ?c"
+ by (rule cos_gt_zero, simp, simp)
+ have "0 = cos (pi / 6 + pi / 6 + pi / 6)"
+ by simp
+ also have "\<dots> = (?c * ?c - ?s * ?s) * ?c - (?s * ?c + ?c * ?s) * ?s"
+ by (simp only: cos_add sin_add)
+ also have "\<dots> = ?c * (?c\<^sup>2 - 3 * ?s\<^sup>2)"
+ by (simp add: algebra_simps power2_eq_square)
+ finally have "?c\<^sup>2 = (sqrt 3/2)\<^sup>2"
+ using pos_c by (simp add: sin_squared_eq power_divide)
+ thus ?thesis
+ using pos_c [THEN order_less_imp_le]
+ by (rule power2_eq_imp_eq) simp
+qed
+
+lemma sin_45: "sin (pi / 4) = sqrt 2 / 2"
+ by (simp add: sin_cos_eq cos_45)
+
+lemma sin_60: "sin (pi / 3) = sqrt 3/2"
+ by (simp add: sin_cos_eq cos_30)
+
+lemma cos_60: "cos (pi / 3) = 1 / 2"
+ apply (rule power2_eq_imp_eq)
+ apply (simp add: cos_squared_eq sin_60 power_divide)
+ apply (rule cos_ge_zero, rule order_trans [where y=0], simp_all)
+ done
+
+lemma sin_30: "sin (pi / 6) = 1 / 2"
+ by (simp add: sin_cos_eq cos_60)
+
+lemma cos_integer_2pi: "n \<in> Ints \<Longrightarrow> cos(2*pi * n) = 1"
+ by (metis Ints_cases cos_one_2pi_int mult.assoc mult.commute real_of_int_def)
+
+lemma sin_integer_2pi: "n \<in> Ints \<Longrightarrow> sin(2*pi * n) = 0"
+ by (metis sin_two_pi Ints_mult mult.assoc mult.commute sin_times_pi_eq_0)
+
+lemma cos_int_2npi [simp]: "cos (2 * real (n::int) * pi) = 1"
+ by (simp add: cos_one_2pi_int)
+
+lemma sin_int_2npi [simp]: "sin (2 * real (n::int) * pi) = 0"
+ by (metis Ints_real_of_int mult.assoc mult.commute sin_integer_2pi)
+
+lemma sincos_principal_value: "\<exists>y. (-pi < y \<and> y \<le> pi) \<and> (sin(y) = sin(x) \<and> cos(y) = cos(x))"
+ apply (rule exI [where x="pi - (2*pi) * frac((pi - x) / (2*pi))"])
+ apply (auto simp: field_simps frac_lt_1)
+ apply (simp_all add: frac_def divide_simps)
+ apply (simp_all add: add_divide_distrib diff_divide_distrib)
+ apply (simp_all add: sin_diff cos_diff mult.assoc [symmetric] cos_integer_2pi sin_integer_2pi)
+ done
+
+
subsection {* Tangent *}
definition tan :: "'a \<Rightarrow> 'a::{real_normed_field,banach}"
@@ -3528,6 +3716,15 @@
unfolding tan_def sin_double cos_double sin_squared_eq
by (simp add: power2_eq_square)
+lemma tan_30: "tan (pi / 6) = 1 / sqrt 3"
+ unfolding tan_def by (simp add: sin_30 cos_30)
+
+lemma tan_45: "tan (pi / 4) = 1"
+ unfolding tan_def by (simp add: sin_45 cos_45)
+
+lemma tan_60: "tan (pi / 3) = sqrt 3"
+ unfolding tan_def by (simp add: sin_60 cos_60)
+
lemma DERIV_tan [simp]:
fixes x :: "'a::{real_normed_field,banach}"
shows "cos x \<noteq> 0 \<Longrightarrow> DERIV tan x :> inverse ((cos x)\<^sup>2)"
@@ -3705,9 +3902,48 @@
lemma tan_periodic_n[simp]: "tan (x + numeral n * pi) = tan x"
using tan_periodic_int[of _ "numeral n" ] unfolding real_numeral .
+lemma tan_minus_45: "tan (-(pi/4)) = -1"
+ unfolding tan_def by (simp add: sin_45 cos_45)
+
+lemma tan_diff:
+ fixes x :: "'a::{real_normed_field,banach}"
+ shows
+ "\<lbrakk>cos x \<noteq> 0; cos y \<noteq> 0; cos (x - y) \<noteq> 0\<rbrakk>
+ \<Longrightarrow> tan(x - y) = (tan(x) - tan(y))/(1 + tan(x) * tan(y))"
+ using tan_add [of x "-y"]
+ by simp
+
+
+lemma tan_pos_pi2_le: "0 \<le> x ==> x < pi/2 \<Longrightarrow> 0 \<le> tan x"
+ using less_eq_real_def tan_gt_zero by auto
+
+lemma cos_tan: "abs(x) < pi/2 \<Longrightarrow> cos(x) = 1 / sqrt(1 + tan(x) ^ 2)"
+ using cos_gt_zero_pi [of x]
+ by (simp add: divide_simps tan_def real_sqrt_divide abs_if split: split_if_asm)
+
+lemma sin_tan: "abs(x) < pi/2 \<Longrightarrow> sin(x) = tan(x) / sqrt(1 + tan(x) ^ 2)"
+ using cos_gt_zero [of "x"] cos_gt_zero [of "-x"]
+ by (force simp add: divide_simps tan_def real_sqrt_divide abs_if split: split_if_asm)
+
+lemma tan_mono_le: "-(pi/2) < x ==> x \<le> y ==> y < pi/2 \<Longrightarrow> tan(x) \<le> tan(y)"
+ using less_eq_real_def tan_monotone by auto
+
+lemma tan_mono_lt_eq: "-(pi/2) < x ==> x < pi/2 ==> -(pi/2) < y ==> y < pi/2
+ \<Longrightarrow> (tan(x) < tan(y) \<longleftrightarrow> x < y)"
+ using tan_monotone' by blast
+
+lemma tan_mono_le_eq: "-(pi/2) < x ==> x < pi/2 ==> -(pi/2) < y ==> y < pi/2
+ \<Longrightarrow> (tan(x) \<le> tan(y) \<longleftrightarrow> x \<le> y)"
+ by (meson tan_mono_le not_le tan_monotone)
+
+lemma tan_bound_pi2: "abs(x) < pi/4 \<Longrightarrow> abs(tan x) < 1"
+ using tan_45 tan_monotone [of x "pi/4"] tan_monotone [of "-x" "pi/4"]
+ by (auto simp: abs_if split: split_if_asm)
+
+lemma tan_cot: "tan(pi/2 - x) = inverse(tan x)"
+ by (simp add: tan_def sin_diff cos_diff)
subsection {* Inverse Trigonometric Functions *}
-text{*STILL DEFINED FOR THE REALS ONLY*}
definition arcsin :: "real => real"
where "arcsin y = (THE x. -(pi/2) \<le> x & x \<le> pi/2 & sin x = y)"
@@ -3820,6 +4056,12 @@
apply (rule power_mono, simp, simp)
done
+lemma arccos_0 [simp]: "arccos 0 = pi/2"
+by (metis arccos_cos cos_gt_zero cos_pi cos_pi_half pi_gt_zero pi_half_ge_zero not_le not_zero_less_neg_numeral numeral_One)
+
+lemma arccos_1 [simp]: "arccos 1 = 0"
+ using arccos_cos by force
+
lemma arctan [simp]: "- (pi/2) < arctan y & arctan y < pi/2 & tan (arctan y) = y"
unfolding arctan_def by (rule theI' [OF tan_total])
@@ -4049,124 +4291,34 @@
by (intro tendsto_minus tendsto_arctan_at_top)
-subsection {* More Theorems about Sin and Cos *}
-
-lemma cos_45: "cos (pi / 4) = sqrt 2 / 2"
-proof -
- let ?c = "cos (pi / 4)" and ?s = "sin (pi / 4)"
- have nonneg: "0 \<le> ?c"
- by (simp add: cos_ge_zero)
- have "0 = cos (pi / 4 + pi / 4)"
- by simp
- also have "cos (pi / 4 + pi / 4) = ?c\<^sup>2 - ?s\<^sup>2"
- by (simp only: cos_add power2_eq_square)
- also have "\<dots> = 2 * ?c\<^sup>2 - 1"
- by (simp add: sin_squared_eq)
- finally have "?c\<^sup>2 = (sqrt 2 / 2)\<^sup>2"
- by (simp add: power_divide)
- thus ?thesis
- using nonneg by (rule power2_eq_imp_eq) simp
-qed
-
-lemma cos_30: "cos (pi / 6) = sqrt 3/2"
-proof -
- let ?c = "cos (pi / 6)" and ?s = "sin (pi / 6)"
- have pos_c: "0 < ?c"
- by (rule cos_gt_zero, simp, simp)
- have "0 = cos (pi / 6 + pi / 6 + pi / 6)"
- by simp
- also have "\<dots> = (?c * ?c - ?s * ?s) * ?c - (?s * ?c + ?c * ?s) * ?s"
- by (simp only: cos_add sin_add)
- also have "\<dots> = ?c * (?c\<^sup>2 - 3 * ?s\<^sup>2)"
- by (simp add: algebra_simps power2_eq_square)
- finally have "?c\<^sup>2 = (sqrt 3/2)\<^sup>2"
- using pos_c by (simp add: sin_squared_eq power_divide)
- thus ?thesis
- using pos_c [THEN order_less_imp_le]
- by (rule power2_eq_imp_eq) simp
-qed
-
-lemma sin_45: "sin (pi / 4) = sqrt 2 / 2"
- by (simp add: sin_cos_eq cos_45)
-
-lemma sin_60: "sin (pi / 3) = sqrt 3/2"
- by (simp add: sin_cos_eq cos_30)
-
-lemma cos_60: "cos (pi / 3) = 1 / 2"
- apply (rule power2_eq_imp_eq)
- apply (simp add: cos_squared_eq sin_60 power_divide)
- apply (rule cos_ge_zero, rule order_trans [where y=0], simp_all)
- done
-
-lemma sin_30: "sin (pi / 6) = 1 / 2"
- by (simp add: sin_cos_eq cos_60)
-
-lemma tan_30: "tan (pi / 6) = 1 / sqrt 3"
- unfolding tan_def by (simp add: sin_30 cos_30)
-
-lemma tan_45: "tan (pi / 4) = 1"
- unfolding tan_def by (simp add: sin_45 cos_45)
-
-lemma tan_60: "tan (pi / 3) = sqrt 3"
- unfolding tan_def by (simp add: sin_60 cos_60)
-
-lemma sin_cos_npi [simp]: "sin (real (Suc (2 * n)) * pi / 2) = (-1) ^ n"
-proof -
- have "sin ((real n + 1/2) * pi) = cos (real n * pi)"
- by (auto simp: algebra_simps sin_add)
- thus ?thesis
- by (simp add: real_of_nat_Suc distrib_right add_divide_distrib
- mult.commute [of pi])
-qed
-
-lemma cos_2npi [simp]: "cos (2 * real (n::nat) * pi) = 1"
- by (cases "even n") (simp_all add: cos_double mult.assoc)
-
-lemma cos_3over2_pi [simp]: "cos (3/2*pi) = 0"
- apply (subgoal_tac "cos (pi + pi/2) = 0", simp)
- apply (subst cos_add, simp)
- done
-
-lemma sin_2npi [simp]: "sin (2 * real (n::nat) * pi) = 0"
- by (auto simp: mult.assoc sin_double)
-
-lemma sin_3over2_pi [simp]: "sin (3/2*pi) = - 1"
- apply (subgoal_tac "sin (pi + pi/2) = - 1", simp)
- apply (subst sin_add, simp)
- done
-
-lemma cos_pi_eq_zero [simp]: "cos (pi * real (Suc (2 * m)) / 2) = 0"
-by (simp only: cos_add sin_add real_of_nat_Suc distrib_right distrib_left add_divide_distrib, auto)
-
-lemma DERIV_cos_add [simp]: "DERIV (\<lambda>x. cos (x + k)) xa :> - sin (xa + k)"
- by (auto intro!: derivative_eq_intros)
-
-lemma sin_zero_norm_cos_one:
- fixes x :: "'a::{real_normed_field,banach}"
- assumes "sin x = 0" shows "norm (cos x) = 1"
- using sin_cos_squared_add [of x, unfolded assms]
- by (simp add: square_norm_one)
-
-lemma sin_zero_abs_cos_one: "sin x = 0 \<Longrightarrow> \<bar>cos x\<bar> = (1::real)"
- using sin_zero_norm_cos_one by fastforce
-
-lemma cos_one_sin_zero:
- fixes x :: "'a::{real_normed_field,banach}"
- assumes "cos x = 1" shows "sin x = 0"
- using sin_cos_squared_add [of x, unfolded assms]
- by simp
-
-
subsection{* Prove Totality of the Trigonometric Functions *}
-lemma arccos_0 [simp]: "arccos 0 = pi/2"
-by (metis arccos_cos cos_gt_zero cos_pi cos_pi_half pi_gt_zero pi_half_ge_zero not_le not_zero_less_neg_numeral numeral_One)
-
-lemma arccos_1 [simp]: "arccos 1 = 0"
- using arccos_cos by force
+lemma sin_mono_less_eq: "\<lbrakk>-(pi/2) \<le> x; x \<le> pi/2; -(pi/2) \<le> y; y \<le> pi/2\<rbrakk>
+ \<Longrightarrow> (sin(x) < sin(y) \<longleftrightarrow> x < y)"
+by (metis not_less_iff_gr_or_eq sin_monotone_2pi)
+
+lemma sin_mono_le_eq: "\<lbrakk>-(pi/2) \<le> x; x \<le> pi/2; -(pi/2) \<le> y; y \<le> pi/2\<rbrakk>
+ \<Longrightarrow> (sin(x) \<le> sin(y) \<longleftrightarrow> x \<le> y)"
+by (meson leD le_less_linear sin_monotone_2pi sin_monotone_2pi_le)
+
+lemma sin_inj_pi: "-(pi/2) \<le> x ==> x \<le> pi/2 ==>
+ -(pi/2) \<le> y ==> y \<le> pi/2 ==> sin(x) = sin(y) \<Longrightarrow> x = y"
+by (metis arcsin_sin)
+
+lemma cos_mono_lt_eq: "0 \<le> x ==> x \<le> pi ==> 0 \<le> y ==> y \<le> pi
+ \<Longrightarrow> (cos(x) < cos(y) \<longleftrightarrow> y < x)"
+by (meson cos_monotone_0_pi cos_monotone_0_pi_le leD le_less_linear)
+
+lemma cos_mono_le_eq: "0 \<le> x ==> x \<le> pi ==> 0 \<le> y ==> y \<le> pi
+ \<Longrightarrow> (cos(x) \<le> cos(y) \<longleftrightarrow> y \<le> x)"
+ by (metis arccos_cos cos_monotone_0_pi_le eq_iff linear)
+
+lemma cos_inj_pi: "0 \<le> x ==> x \<le> pi ==> 0 \<le> y ==> y \<le> pi ==> cos(x) = cos(y)
+ \<Longrightarrow> x = y"
+by (metis arccos_cos)
lemma arccos_le_pi2: "\<lbrakk>0 \<le> y; y \<le> 1\<rbrakk> \<Longrightarrow> arccos y \<le> pi/2"
- by (metis (mono_tags) arccos_0 arccos cos_le_one cos_monotone_0_pi'
+ by (metis (mono_tags) arccos_0 arccos cos_le_one cos_monotone_0_pi_le
cos_pi cos_pi_half pi_half_ge_zero antisym_conv less_eq_neg_nonpos linear minus_minus order.trans order_refl)
lemma sincos_total_pi_half: