New material for complex sin, cos, tan, Ln, also some reorganisation
authorpaulson <lp15@cam.ac.uk>
Thu Mar 19 14:24:51 2015 +0000 (2015-03-19)
changeset 59751916c0f6c83e3
parent 59749 118f4995df8c
child 59752 11b22fe9a6f0
New material for complex sin, cos, tan, Ln, also some reorganisation
NEWS
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Multivariate_Analysis/Complex_Transcendental.thy
src/HOL/Transcendental.thy
     1.1 --- a/NEWS	Thu Mar 19 11:54:20 2015 +0100
     1.2 +++ b/NEWS	Thu Mar 19 14:24:51 2015 +0000
     1.3 @@ -83,14 +83,14 @@
     1.4    type, so in particular on "real" and "complex" uniformly.
     1.5    Minor INCOMPATIBILITY: type constraints may be needed.
     1.6  
     1.7 -* New library of properties of the complex transcendental functions sin, cos, exp,
     1.8 +* New library of properties of the complex transcendental functions sin, cos, tan, exp,
     1.9    ported from HOL Light.
    1.10  
    1.11  * The factorial function, "fact", now has type "nat => 'a" (of a sort that admits
    1.12    numeric types including nat, int, real and complex. INCOMPATIBILITY:
    1.13    an expression such as "fact 3 = 6" may require a type constraint, and the combination
    1.14    "real (fact k)" is likely to be unsatisfactory. If a type conversion is still necessary,
    1.15 -  then use "of_nat (fact k)".
    1.16 +  then use "of_nat (fact k)" or "real_of_nat (fact k)".
    1.17  
    1.18  * removed functions "natfloor" and "natceiling",
    1.19    use "nat o floor" and "nat o ceiling" instead.
     2.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Thu Mar 19 11:54:20 2015 +0100
     2.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Thu Mar 19 14:24:51 2015 +0000
     2.3 @@ -959,7 +959,7 @@
     2.4        unfolding cos_coeff_def atLeast0LessThan by auto
     2.5  
     2.6      have "cos t * (- 1) ^ n = cos t * cos (n * pi) + sin t * sin (n * pi)" by auto
     2.7 -    also have "\<dots> = cos (t + n * pi)" by (simp add: cos_add)  
     2.8 +    also have "\<dots> = cos (t + n * pi)" by (simp add: cos_add)
     2.9      also have "\<dots> = ?rest" by auto
    2.10      finally have "cos t * (- 1) ^ n = ?rest" .
    2.11      moreover
    2.12 @@ -1029,7 +1029,7 @@
    2.13    { fix n
    2.14      have F: "\<And>m. ((\<lambda>i. i + 2) ^^ n) m = m + 2 * n" by (induct n) auto
    2.15      have "?f (Suc n) = ?f n * ((\<lambda>i. i + 2) ^^ n) 2 * (((\<lambda>i. i + 2) ^^ n) 2 + 1)"
    2.16 -      unfolding F by auto } 
    2.17 +      unfolding F by auto }
    2.18    note f_eq = this
    2.19    from horner_bounds[where lb="lb_sin_cos_aux prec" and ub="ub_sin_cos_aux prec" and j'=0,
    2.20      OF `0 \<le> real (x * x)` f_eq lb_sin_cos_aux.simps ub_sin_cos_aux.simps]
    2.21 @@ -1046,7 +1046,7 @@
    2.22    hence "0 < x" and "0 < real x" using `0 \<le> real x` by auto
    2.23    have "0 < x * x" using `0 < x` by simp
    2.24  
    2.25 -  { fix x::real and n 
    2.26 +  { fix x::real and n
    2.27      have "(\<Sum>j = 0 ..< n. (- 1) ^ (((2 * j + 1) - Suc 0) div 2) / ((fact (2 * j + 1))) * x ^(2 * j + 1))
    2.28      = (\<Sum> i = 0 ..< 2 * n. (if even(i) then 0 else ((- 1) ^ ((i - Suc 0) div 2))/((fact i))) * x ^ i)" (is "?SUM = _")
    2.29      proof -
    2.30 @@ -1354,7 +1354,7 @@
    2.31        by auto
    2.32  
    2.33      have "cos (x + (-k) * (2 * pi)) \<le> cos ?lx"
    2.34 -      using cos_monotone_0_pi'[OF lx_0 lx pi_x]
    2.35 +      using cos_monotone_0_pi_le[OF lx_0 lx pi_x]
    2.36        by (simp only: real_of_int_minus
    2.37          cos_minus mult_minus_left) simp
    2.38      also have "\<dots> \<le> (ub_cos prec ?lx)"
    2.39 @@ -1386,7 +1386,7 @@
    2.40      have "(lb_cos prec ?ux) \<le> cos ?ux"
    2.41        using lb_cos[OF ux_0 pi_ux] by simp
    2.42      also have "\<dots> \<le> cos (x + (-k) * (2 * pi))"
    2.43 -      using cos_monotone_0_pi'[OF x_ge_0 ux pi_ux]
    2.44 +      using cos_monotone_0_pi_le[OF x_ge_0 ux pi_ux]
    2.45        by (simp only: real_of_int_minus
    2.46          cos_minus mult_minus_left) simp
    2.47      finally have "(lb_cos prec ?ux) \<le> cos x"
    2.48 @@ -1505,7 +1505,7 @@
    2.49        have "cos x = cos (x + (-k) * (2 * pi) + (1 :: int) * (2 * pi))"
    2.50          unfolding cos_periodic_int ..
    2.51        also have "\<dots> \<le> cos ((?lx + 2 * ?lpi))"
    2.52 -        using cos_monotone_0_pi'[OF lx_0 lx_le_x pi_x]
    2.53 +        using cos_monotone_0_pi_le[OF lx_0 lx_le_x pi_x]
    2.54          by (simp only: minus_float.rep_eq real_of_int_minus real_of_one
    2.55            mult_minus_left mult_1_left) simp
    2.56        also have "\<dots> \<le> (ub_cos prec (?lx + 2 * ?lpi))"
    2.57 @@ -1535,7 +1535,7 @@
    2.58  proof -
    2.59    { fix n
    2.60      have F: "\<And> m. ((\<lambda>i. i + 1) ^^ n) m = n + m" by (induct n, auto)
    2.61 -    have "fact (Suc n) = fact n * ((\<lambda>i::nat. i + 1) ^^ n) 1" unfolding F by auto 
    2.62 +    have "fact (Suc n) = fact n * ((\<lambda>i::nat. i + 1) ^^ n) 1" unfolding F by auto
    2.63    } note f_eq = this
    2.64  
    2.65    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,
    2.66 @@ -2022,7 +2022,7 @@
    2.67    hence "0 \<le> bl" by (simp add: bitlen_def bl_def)
    2.68    show ?thesis
    2.69    proof (cases "0 \<le> e")
    2.70 -    case True 
    2.71 +    case True
    2.72      thus ?thesis
    2.73        unfolding bl_def[symmetric] using `0 < real m` `0 \<le> bl`
    2.74        apply (simp add: ln_mult)
    2.75 @@ -3234,7 +3234,7 @@
    2.76  qed
    2.77  
    2.78  lemma setprod_fact: "real (\<Prod> {1..<1 + k}) = fact (k :: nat)"
    2.79 -  using fact_altdef_nat Suc_eq_plus1_left atLeastLessThanSuc_atLeastAtMost real_fact_nat 
    2.80 +  using fact_altdef_nat Suc_eq_plus1_left atLeastLessThanSuc_atLeastAtMost real_fact_nat
    2.81    by presburger
    2.82  
    2.83  lemma approx_tse:
     3.1 --- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Thu Mar 19 11:54:20 2015 +0100
     3.2 +++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Thu Mar 19 14:24:51 2015 +0000
     3.3 @@ -156,104 +156,12 @@
     3.4  
     3.5  lemma Im_cos: "Im(cos z) = sin(Re z) * (exp(-(Im z)) - exp(Im z)) / 2"
     3.6    by (simp add: cos_exp_eq field_simps Im_divide Im_exp)
     3.7 -
     3.8 -
     3.9 -subsection {* More Corollaries about Sine and Cosine *}
    3.10 -
    3.11 -lemma sin_times_pi_eq_0: "sin(x * pi) = 0 \<longleftrightarrow> x \<in> Ints"
    3.12 -  by (simp add: sin_zero_iff_int2) (metis Ints_cases Ints_real_of_int real_of_int_def)
    3.13 -
    3.14 -lemma cos_one_2pi: 
    3.15 -    "cos(x) = 1 \<longleftrightarrow> (\<exists>n::nat. x = n * 2*pi) | (\<exists>n::nat. x = -(n * 2*pi))"
    3.16 -    (is "?lhs = ?rhs")
    3.17 -proof
    3.18 -  assume "cos(x) = 1"
    3.19 -  then have "sin x = 0"
    3.20 -    by (simp add: cos_one_sin_zero)
    3.21 -  then show ?rhs
    3.22 -  proof (simp only: sin_zero_iff, elim exE disjE conjE)
    3.23 -    fix n::nat
    3.24 -    assume n: "even n" "x = real n * (pi/2)"
    3.25 -    then obtain m where m: "n = 2 * m"
    3.26 -      using dvdE by blast
    3.27 -    then have me: "even m" using `?lhs` n
    3.28 -      by (auto simp: field_simps) (metis one_neq_neg_one  power_minus_odd power_one)
    3.29 -    show ?rhs
    3.30 -      using m me n
    3.31 -      by (auto simp: field_simps elim!: evenE)
    3.32 -  next    
    3.33 -    fix n::nat
    3.34 -    assume n: "even n" "x = - (real n * (pi/2))"
    3.35 -    then obtain m where m: "n = 2 * m"
    3.36 -      using dvdE by blast
    3.37 -    then have me: "even m" using `?lhs` n
    3.38 -      by (auto simp: field_simps) (metis one_neq_neg_one  power_minus_odd power_one)
    3.39 -    show ?rhs
    3.40 -      using m me n
    3.41 -      by (auto simp: field_simps elim!: evenE)
    3.42 -  qed
    3.43 -next
    3.44 -  assume "?rhs"
    3.45 -  then show "cos x = 1"
    3.46 -    by (metis cos_2npi cos_minus mult.assoc mult.left_commute)
    3.47 -qed
    3.48 -
    3.49 -lemma cos_one_2pi_int: "cos(x) = 1 \<longleftrightarrow> (\<exists>n::int. x = n * 2*pi)"
    3.50 -  apply auto  --{*FIXME simproc bug*}
    3.51 -  apply (auto simp: cos_one_2pi)
    3.52 -  apply (metis real_of_int_of_nat_eq)
    3.53 -  apply (metis mult_minus_right real_of_int_minus real_of_int_of_nat_eq)
    3.54 -  by (metis mult_minus_right of_int_of_nat real_of_int_def real_of_nat_def)
    3.55 -
    3.56 -lemma sin_cos_sqrt: "0 \<le> sin(x) \<Longrightarrow> (sin(x) = sqrt(1 - (cos(x) ^ 2)))"
    3.57 -  using sin_squared_eq real_sqrt_unique by fastforce
    3.58 -
    3.59 -lemma sin_eq_0_pi: "-pi < x \<Longrightarrow> x < pi \<Longrightarrow> sin(x) = 0 \<Longrightarrow> x = 0"
    3.60 -  by (metis sin_gt_zero sin_minus minus_less_iff neg_0_less_iff_less not_less_iff_gr_or_eq)
    3.61 -
    3.62 -lemma cos_treble_cos: 
    3.63 -  fixes x :: "'a::{real_normed_field,banach}"
    3.64 -  shows "cos(3 * x) = 4 * cos(x) ^ 3 - 3 * cos x"
    3.65 -proof -
    3.66 -  have *: "(sin x * (sin x * 3)) = 3 - (cos x * (cos x * 3))"
    3.67 -    by (simp add: mult.assoc [symmetric] sin_squared_eq [unfolded power2_eq_square])
    3.68 -  have "cos(3 * x) = cos(2*x + x)"
    3.69 -    by simp
    3.70 -  also have "... = 4 * cos(x) ^ 3 - 3 * cos x"
    3.71 -    apply (simp only: cos_add cos_double sin_double)
    3.72 -    apply (simp add: * field_simps power2_eq_square power3_eq_cube)
    3.73 -    done
    3.74 -  finally show ?thesis .
    3.75 -qed
    3.76 -
    3.77    
    3.78  subsection{*More on the Polar Representation of Complex Numbers*}
    3.79  
    3.80 -lemma cos_integer_2pi: "n \<in> Ints \<Longrightarrow> cos(2*pi * n) = 1"
    3.81 -  by (metis Ints_cases cos_one_2pi_int mult.assoc mult.commute real_of_int_def)
    3.82 -
    3.83 -lemma sin_integer_2pi: "n \<in> Ints \<Longrightarrow> sin(2*pi * n) = 0"
    3.84 -  by (metis sin_two_pi Ints_mult mult.assoc mult.commute sin_times_pi_eq_0)
    3.85 -
    3.86 -lemma cos_int_2npi [simp]: "cos (2 * real (n::int) * pi) = 1"
    3.87 -  by (simp add: cos_one_2pi_int)
    3.88 -
    3.89 -lemma sin_int_2npi [simp]: "sin (2 * real (n::int) * pi) = 0"
    3.90 -  by (metis Ints_real_of_int mult.assoc mult.commute sin_integer_2pi)
    3.91 -
    3.92 -lemma sincos_principal_value: "\<exists>y. (-pi < y \<and> y \<le> pi) \<and> (sin(y) = sin(x) \<and> cos(y) = cos(x))"
    3.93 -  apply (rule exI [where x="pi - (2*pi) * frac((pi - x) / (2*pi))"])
    3.94 -  apply (auto simp: field_simps frac_lt_1)
    3.95 -  apply (simp_all add: frac_def divide_simps)
    3.96 -  apply (simp_all add: add_divide_distrib diff_divide_distrib)
    3.97 -  apply (simp_all add: sin_diff cos_diff mult.assoc [symmetric] cos_integer_2pi sin_integer_2pi)
    3.98 -  done
    3.99 -
   3.100  lemma exp_Complex: "exp(Complex r t) = of_real(exp r) * Complex (cos t) (sin t)"
   3.101    by (simp add: exp_add exp_Euler exp_of_real)
   3.102  
   3.103 -
   3.104 -
   3.105  lemma exp_eq_1: "exp z = 1 \<longleftrightarrow> Re(z) = 0 \<and> (\<exists>n::int. Im(z) = of_int (2 * n) * pi)"
   3.106  apply auto
   3.107  apply (metis exp_eq_one_iff norm_exp_eq_Re norm_one)
   3.108 @@ -667,6 +575,13 @@
   3.109  
   3.110  end (* of context *)
   3.111  
   3.112 +text{*32-bit Approximation to e*}
   3.113 +lemma e_approx_32: "abs(exp(1) - 5837465777 / 2147483648) \<le> (inverse(2 ^ 32)::real)"
   3.114 +  using Taylor_exp [of 1 14] exp_le
   3.115 +  apply (simp add: setsum_left_distrib in_Reals_norm Re_exp atMost_nat_numeral fact_numeral)
   3.116 +  apply (simp only: pos_le_divide_eq [symmetric], linarith)
   3.117 +  done
   3.118 +
   3.119  subsection{*The argument of a complex number*}
   3.120  
   3.121  definition Arg :: "complex \<Rightarrow> real" where
   3.122 @@ -888,7 +803,6 @@
   3.123    apply auto
   3.124    by (metis Arg_eq_0 less_irrefl minus_diff_eq right_minus_eq)
   3.125  
   3.126 -
   3.127  lemma Arg_add:
   3.128    assumes "w \<noteq> 0" "z \<noteq> 0"
   3.129      shows "Arg w + Arg z = (if Arg w + Arg z < 2*pi then Arg(w * z) else Arg(w * z) + 2*pi)"
   3.130 @@ -921,4 +835,470 @@
   3.131  lemma Arg_exp: "0 \<le> Im z \<Longrightarrow> Im z < 2*pi \<Longrightarrow> Arg(exp z) = Im z"
   3.132    by (rule Arg_unique [of  "exp(Re z)"]) (auto simp: Exp_eq_polar)
   3.133  
   3.134 +
   3.135 +subsection{*Analytic properties of tangent function*}
   3.136 +
   3.137 +lemma cnj_tan: "cnj(tan z) = tan(cnj z)"
   3.138 +  by (simp add: cnj_cos cnj_sin tan_def)
   3.139 +
   3.140 +lemma complex_differentiable_at_tan: "~(cos z = 0) \<Longrightarrow> tan complex_differentiable at z"
   3.141 +  unfolding complex_differentiable_def
   3.142 +  using DERIV_tan by blast
   3.143 +
   3.144 +lemma complex_differentiable_within_tan: "~(cos z = 0)
   3.145 +         \<Longrightarrow> tan complex_differentiable (at z within s)"
   3.146 +  using complex_differentiable_at_tan complex_differentiable_at_within by blast
   3.147 +
   3.148 +lemma continuous_within_tan: "~(cos z = 0) \<Longrightarrow> continuous (at z within s) tan"
   3.149 +  using continuous_at_imp_continuous_within isCont_tan by blast
   3.150 +
   3.151 +lemma continuous_on_tan [continuous_intros]: "(\<And>z. z \<in> s \<Longrightarrow> ~(cos z = 0)) \<Longrightarrow> continuous_on s tan"
   3.152 +  by (simp add: continuous_at_imp_continuous_on)
   3.153 +
   3.154 +lemma holomorphic_on_tan: "(\<And>z. z \<in> s \<Longrightarrow> ~(cos z = 0)) \<Longrightarrow> tan holomorphic_on s"
   3.155 +  by (simp add: complex_differentiable_within_tan holomorphic_on_def)
   3.156 +
   3.157 +
   3.158 +subsection{*Complex logarithms (the conventional principal value)*}
   3.159 +
   3.160 +definition Ln where
   3.161 +   "Ln \<equiv> \<lambda>z. THE w. exp w = z & -pi < Im(w) & Im(w) \<le> pi"
   3.162 +
   3.163 +lemma
   3.164 +  assumes "z \<noteq> 0"
   3.165 +    shows exp_Ln [simp]: "exp(Ln z) = z"
   3.166 +      and mpi_less_Im_Ln: "-pi < Im(Ln z)"
   3.167 +      and Im_Ln_le_pi:    "Im(Ln z) \<le> pi"
   3.168 +proof -
   3.169 +  obtain \<psi> where z: "z / (cmod z) = Complex (cos \<psi>) (sin \<psi>)"
   3.170 +    using complex_unimodular_polar [of "z / (norm z)"] assms
   3.171 +    by (auto simp: norm_divide divide_simps)
   3.172 +  obtain \<phi> where \<phi>: "- pi < \<phi>" "\<phi> \<le> pi" "sin \<phi> = sin \<psi>" "cos \<phi> = cos \<psi>"
   3.173 +    using sincos_principal_value [of "\<psi>"] assms
   3.174 +    by (auto simp: norm_divide divide_simps)
   3.175 +  have "exp(Ln z) = z & -pi < Im(Ln z) & Im(Ln z) \<le> pi" unfolding Ln_def
   3.176 +    apply (rule theI [where a = "Complex (ln(norm z)) \<phi>"])
   3.177 +    using z assms \<phi>
   3.178 +    apply (auto simp: field_simps exp_complex_eqI Exp_eq_polar cis.code)
   3.179 +    done
   3.180 +  then show "exp(Ln z) = z" "-pi < Im(Ln z)" "Im(Ln z) \<le> pi"
   3.181 +    by auto
   3.182 +qed
   3.183 +
   3.184 +lemma Ln_exp [simp]:
   3.185 +  assumes "-pi < Im(z)" "Im(z) \<le> pi"
   3.186 +    shows "Ln(exp z) = z"
   3.187 +  apply (rule exp_complex_eqI)
   3.188 +  using assms mpi_less_Im_Ln  [of "exp z"] Im_Ln_le_pi [of "exp z"]
   3.189 +  apply auto
   3.190 +  done
   3.191 +
   3.192 +lemma Ln_eq_iff: "w \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> (Ln w = Ln z \<longleftrightarrow> w = z)"
   3.193 +  by (metis exp_Ln)
   3.194 +
   3.195 +lemma Ln_unique: "exp(z) = w \<Longrightarrow> -pi < Im(z) \<Longrightarrow> Im(z) \<le> pi \<Longrightarrow> Ln w = z"
   3.196 +  using Ln_exp by blast
   3.197 +
   3.198 +lemma Re_Ln [simp]: "z \<noteq> 0 \<Longrightarrow> Re(Ln z) = ln(norm z)"
   3.199 +by (metis exp_Ln assms ln_exp norm_exp_eq_Re)
   3.200 +
   3.201 +lemma exists_complex_root:
   3.202 +  fixes a :: complex
   3.203 +  shows "n \<noteq> 0 \<Longrightarrow> \<exists>z. z ^ n = a"
   3.204 +  apply (cases "a=0", simp)
   3.205 +  apply (rule_tac x= "exp(Ln(a) / n)" in exI)
   3.206 +  apply (auto simp: exp_of_nat_mult [symmetric])
   3.207 +  done
   3.208 +
   3.209 +subsection{*Derivative of Ln away from the branch cut*}
   3.210 +
   3.211 +lemma
   3.212 +  assumes "Im(z) = 0 \<Longrightarrow> 0 < Re(z)"
   3.213 +    shows has_field_derivative_Ln: "(Ln has_field_derivative inverse(z)) (at z)"
   3.214 +      and Im_Ln_less_pi:           "Im (Ln z) < pi"
   3.215 +proof -
   3.216 +  have znz: "z \<noteq> 0"
   3.217 +    using assms by auto
   3.218 +  then show *: "Im (Ln z) < pi" using assms
   3.219 +    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)
   3.220 +  show "(Ln has_field_derivative inverse(z)) (at z)"
   3.221 +    apply (rule has_complex_derivative_inverse_strong_x
   3.222 +              [where f = exp and s = "{w. -pi < Im(w) & Im(w) < pi}"])
   3.223 +    using znz *
   3.224 +    apply (auto simp: continuous_on_exp open_Collect_conj open_halfspace_Im_gt open_halfspace_Im_lt)
   3.225 +    apply (metis DERIV_exp exp_Ln)
   3.226 +    apply (metis mpi_less_Im_Ln)
   3.227 +    done
   3.228 +qed
   3.229 +
   3.230 +declare has_field_derivative_Ln [derivative_intros]
   3.231 +declare has_field_derivative_Ln [THEN DERIV_chain2, derivative_intros]
   3.232 +
   3.233 +lemma complex_differentiable_at_Ln: "(Im(z) = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> Ln complex_differentiable at z"
   3.234 +  using complex_differentiable_def has_field_derivative_Ln by blast
   3.235 +
   3.236 +lemma complex_differentiable_within_Ln: "(Im(z) = 0 \<Longrightarrow> 0 < Re(z))
   3.237 +         \<Longrightarrow> Ln complex_differentiable (at z within s)"
   3.238 +  using complex_differentiable_at_Ln complex_differentiable_within_subset by blast
   3.239 +
   3.240 +lemma continuous_at_Ln: "(Im(z) = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous (at z) Ln"
   3.241 +  by (simp add: complex_differentiable_imp_continuous_at complex_differentiable_within_Ln)
   3.242 +
   3.243 +lemma continuous_within_Ln: "(Im(z) = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous (at z within s) Ln"
   3.244 +  using continuous_at_Ln continuous_at_imp_continuous_within by blast
   3.245 +
   3.246 +lemma continuous_on_Ln [continuous_intros]: "(\<And>z. z \<in> s \<Longrightarrow> Im(z) = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous_on s Ln"
   3.247 +  by (simp add: continuous_at_imp_continuous_on continuous_within_Ln)
   3.248 +
   3.249 +lemma holomorphic_on_Ln: "(\<And>z. z \<in> s \<Longrightarrow> Im(z) = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> Ln holomorphic_on s"
   3.250 +  by (simp add: complex_differentiable_within_Ln holomorphic_on_def)
   3.251 +
   3.252 +
   3.253 +subsection{*Relation to Real Logarithm*}
   3.254 +
   3.255 +lemma ln_of_real:
   3.256 +  assumes "0 < z"
   3.257 +    shows "Ln(of_real z) = of_real(ln z)"
   3.258 +proof -
   3.259 +  have "Ln(of_real (exp (ln z))) = Ln (exp (of_real (ln z)))"
   3.260 +    by (simp add: exp_of_real)
   3.261 +  also have "... = of_real(ln z)"
   3.262 +    using assms
   3.263 +    by (subst Ln_exp) auto
   3.264 +  finally show ?thesis
   3.265 +    using assms by simp
   3.266 +qed
   3.267 +
   3.268 +
   3.269 +subsection{*Quadrant-type results for Ln*}
   3.270 +
   3.271 +lemma cos_lt_zero_pi: "pi/2 < x \<Longrightarrow> x < 3*pi/2 \<Longrightarrow> cos x < 0"
   3.272 +  using cos_minus_pi cos_gt_zero_pi [of "x-pi"]
   3.273 +  by simp
   3.274 +
   3.275 +lemma Re_Ln_pos_lt:
   3.276 +  assumes "z \<noteq> 0"
   3.277 +    shows "abs(Im(Ln z)) < pi/2 \<longleftrightarrow> 0 < Re(z)"
   3.278 +proof -
   3.279 +  { fix w
   3.280 +    assume "w = Ln z"
   3.281 +    then have w: "Im w \<le> pi" "- pi < Im w"
   3.282 +      using Im_Ln_le_pi [of z]  mpi_less_Im_Ln [of z]  assms
   3.283 +      by auto
   3.284 +    then have "abs(Im w) < pi/2 \<longleftrightarrow> 0 < Re(exp w)"
   3.285 +      apply (auto simp: Re_exp zero_less_mult_iff cos_gt_zero_pi)
   3.286 +      using cos_lt_zero_pi [of "-(Im w)"] cos_lt_zero_pi [of "(Im w)"]
   3.287 +      apply (simp add: abs_if split: split_if_asm)
   3.288 +      apply (metis (no_types) cos_minus cos_pi_half eq_divide_eq_numeral1(1) eq_numeral_simps(4)
   3.289 +               less_numeral_extra(3) linorder_neqE_linordered_idom minus_mult_minus minus_mult_right
   3.290 +               mult_numeral_1_right)
   3.291 +      done
   3.292 +  }
   3.293 +  then show ?thesis using assms
   3.294 +    by auto
   3.295 +qed
   3.296 +
   3.297 +lemma Re_Ln_pos_le:
   3.298 +  assumes "z \<noteq> 0"
   3.299 +    shows "abs(Im(Ln z)) \<le> pi/2 \<longleftrightarrow> 0 \<le> Re(z)"
   3.300 +proof -
   3.301 +  { fix w
   3.302 +    assume "w = Ln z"
   3.303 +    then have w: "Im w \<le> pi" "- pi < Im w"
   3.304 +      using Im_Ln_le_pi [of z]  mpi_less_Im_Ln [of z]  assms
   3.305 +      by auto
   3.306 +    then have "abs(Im w) \<le> pi/2 \<longleftrightarrow> 0 \<le> Re(exp w)"
   3.307 +      apply (auto simp: Re_exp zero_le_mult_iff cos_ge_zero)
   3.308 +      using cos_lt_zero_pi [of "- (Im w)"] cos_lt_zero_pi [of "(Im w)"] not_le
   3.309 +      apply (auto simp: abs_if split: split_if_asm)
   3.310 +      done
   3.311 +  }
   3.312 +  then show ?thesis using assms
   3.313 +    by auto
   3.314 +qed
   3.315 +
   3.316 +lemma Im_Ln_pos_lt:
   3.317 +  assumes "z \<noteq> 0"
   3.318 +    shows "0 < Im(Ln z) \<and> Im(Ln z) < pi \<longleftrightarrow> 0 < Im(z)"
   3.319 +proof -
   3.320 +  { fix w
   3.321 +    assume "w = Ln z"
   3.322 +    then have w: "Im w \<le> pi" "- pi < Im w"
   3.323 +      using Im_Ln_le_pi [of z]  mpi_less_Im_Ln [of z]  assms
   3.324 +      by auto
   3.325 +    then have "0 < Im w \<and> Im w < pi \<longleftrightarrow> 0 < Im(exp w)"
   3.326 +      using sin_gt_zero [of "- (Im w)"] sin_gt_zero [of "(Im w)"]
   3.327 +      apply (auto simp: Im_exp zero_less_mult_iff)
   3.328 +      using less_linear apply fastforce
   3.329 +      using less_linear apply fastforce
   3.330 +      done
   3.331 +  }
   3.332 +  then show ?thesis using assms
   3.333 +    by auto
   3.334 +qed
   3.335 +
   3.336 +lemma Im_Ln_pos_le:
   3.337 +  assumes "z \<noteq> 0"
   3.338 +    shows "0 \<le> Im(Ln z) \<and> Im(Ln z) \<le> pi \<longleftrightarrow> 0 \<le> Im(z)"
   3.339 +proof -
   3.340 +  { fix w
   3.341 +    assume "w = Ln z"
   3.342 +    then have w: "Im w \<le> pi" "- pi < Im w"
   3.343 +      using Im_Ln_le_pi [of z]  mpi_less_Im_Ln [of z]  assms
   3.344 +      by auto
   3.345 +    then have "0 \<le> Im w \<and> Im w \<le> pi \<longleftrightarrow> 0 \<le> Im(exp w)"
   3.346 +      using sin_ge_zero [of "- (Im w)"] sin_ge_zero [of "(Im w)"]
   3.347 +      apply (auto simp: Im_exp zero_le_mult_iff sin_ge_zero)
   3.348 +      apply (metis not_le not_less_iff_gr_or_eq pi_not_less_zero sin_eq_0_pi)
   3.349 +      done }
   3.350 +  then show ?thesis using assms
   3.351 +    by auto
   3.352 +qed
   3.353 +
   3.354 +lemma Re_Ln_pos_lt_imp: "0 < Re(z) \<Longrightarrow> abs(Im(Ln z)) < pi/2"
   3.355 +  by (metis Re_Ln_pos_lt less_irrefl zero_complex.simps(1))
   3.356 +
   3.357 +lemma Im_Ln_pos_lt_imp: "0 < Im(z) \<Longrightarrow> 0 < Im(Ln z) \<and> Im(Ln z) < pi"
   3.358 +  by (metis Im_Ln_pos_lt not_le order_refl zero_complex.simps(2))
   3.359 +
   3.360 +lemma Im_Ln_eq_0: "z \<noteq> 0 \<Longrightarrow> (Im(Ln z) = 0 \<longleftrightarrow> 0 < Re(z) \<and> Im(z) = 0)"
   3.361 +  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
   3.362 +       complex_eq exp_of_real le_less mult_zero_right norm_exp_eq_Re norm_le_zero_iff not_le of_real_0)
   3.363 +
   3.364 +lemma Im_Ln_eq_pi: "z \<noteq> 0 \<Longrightarrow> (Im(Ln z) = pi \<longleftrightarrow> Re(z) < 0 \<and> Im(z) = 0)"
   3.365 +  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)
   3.366 +
   3.367 +
   3.368 +subsection{*More Properties of Ln*}
   3.369 +
   3.370 +lemma cnj_Ln: "(Im z = 0 \<Longrightarrow> 0 < Re z) \<Longrightarrow> cnj(Ln z) = Ln(cnj z)"
   3.371 +  apply (cases "z=0", auto)
   3.372 +  apply (rule exp_complex_eqI)
   3.373 +  apply (auto simp: abs_if split: split_if_asm)
   3.374 +  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)
   3.375 +  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)
   3.376 +  by (metis exp_Ln exp_cnj)
   3.377 +
   3.378 +lemma Ln_inverse: "(Im(z) = 0 \<Longrightarrow> 0 < Re z) \<Longrightarrow> Ln(inverse z) = -(Ln z)"
   3.379 +  apply (cases "z=0", auto)
   3.380 +  apply (rule exp_complex_eqI)
   3.381 +  using mpi_less_Im_Ln [of z] mpi_less_Im_Ln [of "inverse z"]
   3.382 +  apply (auto simp: abs_if exp_minus split: split_if_asm)
   3.383 +  apply (metis Im_Ln_less_pi Im_Ln_pos_le add_less_cancel_left add_strict_mono
   3.384 +               inverse_inverse_eq inverse_zero le_less mult.commute mult_2_right)
   3.385 +  done
   3.386 +
   3.387 +lemma Ln_1 [simp]: "Ln(1) = 0"
   3.388 +proof -
   3.389 +  have "Ln (exp 0) = 0"
   3.390 +    by (metis exp_zero ln_exp ln_of_real of_real_0 of_real_1 zero_less_one)
   3.391 +  then show ?thesis
   3.392 +    by simp
   3.393 +qed
   3.394 +
   3.395 +lemma Ln_minus1 [simp]: "Ln(-1) = ii * pi"
   3.396 +  apply (rule exp_complex_eqI)
   3.397 +  using Im_Ln_le_pi [of "-1"] mpi_less_Im_Ln [of "-1"] cis_conv_exp cis_pi
   3.398 +  apply (auto simp: abs_if)
   3.399 +  done
   3.400 +
   3.401 +lemma Ln_ii [simp]: "Ln ii = ii * of_real pi/2"
   3.402 +  using Ln_exp [of "ii * (of_real pi/2)"]
   3.403 +  unfolding exp_Euler
   3.404 +  by simp
   3.405 +
   3.406 +lemma Ln_minus_ii [simp]: "Ln(-ii) = - (ii * pi/2)"
   3.407 +proof -
   3.408 +  have  "Ln(-ii) = Ln(1/ii)"
   3.409 +    by simp
   3.410 +  also have "... = - (Ln ii)"
   3.411 +    by (metis Ln_inverse ii.sel(2) inverse_eq_divide zero_neq_one)
   3.412 +  also have "... = - (ii * pi/2)"
   3.413 +    by (simp add: Ln_ii)
   3.414 +  finally show ?thesis .
   3.415 +qed
   3.416 +
   3.417 +lemma Ln_times:
   3.418 +  assumes "w \<noteq> 0" "z \<noteq> 0"
   3.419 +    shows "Ln(w * z) =
   3.420 +                (if Im(Ln w + Ln z) \<le> -pi then
   3.421 +                  (Ln(w) + Ln(z)) + ii * of_real(2*pi)
   3.422 +                else if Im(Ln w + Ln z) > pi then
   3.423 +                  (Ln(w) + Ln(z)) - ii * of_real(2*pi)
   3.424 +                else Ln(w) + Ln(z))"
   3.425 +  using pi_ge_zero Im_Ln_le_pi [of w] Im_Ln_le_pi [of z]
   3.426 +  using assms mpi_less_Im_Ln [of w] mpi_less_Im_Ln [of z]
   3.427 +  by (auto simp: of_real_numeral exp_add exp_diff sin_double cos_double exp_Euler intro!: Ln_unique)
   3.428 +
   3.429 +lemma Ln_times_simple:
   3.430 +    "\<lbrakk>w \<noteq> 0; z \<noteq> 0; -pi < Im(Ln w) + Im(Ln z); Im(Ln w) + Im(Ln z) \<le> pi\<rbrakk>
   3.431 +         \<Longrightarrow> Ln(w * z) = Ln(w) + Ln(z)"
   3.432 +  by (simp add: Ln_times)
   3.433 +
   3.434 +lemma Ln_minus:
   3.435 +  assumes "z \<noteq> 0"
   3.436 +    shows "Ln(-z) = (if Im(z) \<le> 0 \<and> ~(Re(z) < 0 \<and> Im(z) = 0)
   3.437 +                     then Ln(z) + ii * pi
   3.438 +                     else Ln(z) - ii * pi)" (is "_ = ?rhs")
   3.439 +  using Im_Ln_le_pi [of z] mpi_less_Im_Ln [of z] assms
   3.440 +        Im_Ln_eq_pi [of z] Im_Ln_pos_lt [of z]
   3.441 +    by (auto simp: of_real_numeral exp_add exp_diff exp_Euler intro!: Ln_unique)
   3.442 +
   3.443 +lemma Ln_inverse_if:
   3.444 +  assumes "z \<noteq> 0"
   3.445 +    shows "Ln (inverse z) =
   3.446 +            (if (Im(z) = 0 \<longrightarrow> 0 < Re z)
   3.447 +             then -(Ln z)
   3.448 +             else -(Ln z) + \<i> * 2 * complex_of_real pi)"
   3.449 +proof (cases "(Im(z) = 0 \<longrightarrow> 0 < Re z)")
   3.450 +  case True then show ?thesis
   3.451 +    by (simp add: Ln_inverse)
   3.452 +next
   3.453 +  case False
   3.454 +  then have z: "Im z = 0" "Re z < 0"
   3.455 +    using assms
   3.456 +    apply auto
   3.457 +    by (metis cnj.code complex_cnj_cnj not_less_iff_gr_or_eq zero_complex.simps(1) zero_complex.simps(2))
   3.458 +  have "Ln(inverse z) = Ln(- (inverse (-z)))"
   3.459 +    by simp
   3.460 +  also have "... = Ln (inverse (-z)) + \<i> * complex_of_real pi"
   3.461 +    using assms z
   3.462 +    apply (simp add: Ln_minus)
   3.463 +    apply (simp add: field_simps)
   3.464 +    done
   3.465 +  also have "... = - Ln (- z) + \<i> * complex_of_real pi"
   3.466 +    apply (subst Ln_inverse)
   3.467 +    using z assms by auto
   3.468 +  also have "... = - (Ln z) + \<i> * 2 * complex_of_real pi"
   3.469 +    apply (subst Ln_minus [OF assms])
   3.470 +    using assms z
   3.471 +    apply simp
   3.472 +    done
   3.473 +  finally show ?thesis
   3.474 +    using assms z
   3.475 +    by simp
   3.476 +qed
   3.477 +
   3.478 +lemma Ln_times_ii:
   3.479 +  assumes "z \<noteq> 0"
   3.480 +    shows  "Ln(ii * z) = (if 0 \<le> Re(z) | Im(z) < 0
   3.481 +                          then Ln(z) + ii * of_real pi/2
   3.482 +                          else Ln(z) - ii * of_real(3 * pi/2))"
   3.483 +  using Im_Ln_le_pi [of z] mpi_less_Im_Ln [of z] assms
   3.484 +        Im_Ln_eq_pi [of z] Im_Ln_pos_lt [of z] Re_Ln_pos_le [of z]
   3.485 +  by (auto simp: of_real_numeral Ln_times)
   3.486 +
   3.487 +
   3.488 +subsection{*Relation between Square Root and exp/ln, hence its derivative*}
   3.489 +
   3.490 +lemma csqrt_exp_Ln:
   3.491 +  assumes "z \<noteq> 0"
   3.492 +    shows "csqrt z = exp(Ln(z) / 2)"
   3.493 +proof -
   3.494 +  have "(exp (Ln z / 2))\<^sup>2 = (exp (Ln z))"
   3.495 +    by (metis exp_double nonzero_mult_divide_cancel_left times_divide_eq_right zero_neq_numeral)
   3.496 +  also have "... = z"
   3.497 +    using assms exp_Ln by blast
   3.498 +  finally have "csqrt z = csqrt ((exp (Ln z / 2))\<^sup>2)"
   3.499 +    by simp
   3.500 +  also have "... = exp (Ln z / 2)"
   3.501 +    apply (subst csqrt_square)
   3.502 +    using cos_gt_zero_pi [of "(Im (Ln z) / 2)"] Im_Ln_le_pi mpi_less_Im_Ln assms
   3.503 +    apply (auto simp: Re_exp Im_exp zero_less_mult_iff zero_le_mult_iff, fastforce+)
   3.504 +    done
   3.505 +  finally show ?thesis using assms csqrt_square
   3.506 +    by simp
   3.507 +qed
   3.508 +
   3.509 +lemma csqrt_inverse:
   3.510 +  assumes "Im(z) = 0 \<Longrightarrow> 0 < Re z"
   3.511 +    shows "csqrt (inverse z) = inverse (csqrt z)"
   3.512 +proof (cases "z=0", simp)
   3.513 +  assume "z \<noteq> 0 "
   3.514 +  then show ?thesis
   3.515 +    using assms
   3.516 +    by (simp add: csqrt_exp_Ln Ln_inverse exp_minus)
   3.517 +qed
   3.518 +
   3.519 +lemma cnj_csqrt:
   3.520 +  assumes "Im z = 0 \<Longrightarrow> 0 \<le> Re(z)"
   3.521 +    shows "cnj(csqrt z) = csqrt(cnj z)"
   3.522 +proof (cases "z=0", simp)
   3.523 +  assume z: "z \<noteq> 0"
   3.524 +  then have "Im z = 0 \<Longrightarrow> 0 < Re(z)"
   3.525 +    using assms cnj.code complex_cnj_zero_iff by fastforce
   3.526 +  then show ?thesis
   3.527 +   using z by (simp add: csqrt_exp_Ln cnj_Ln exp_cnj)
   3.528 +qed
   3.529 +
   3.530 +lemma has_field_derivative_csqrt:
   3.531 +  assumes "Im z = 0 \<Longrightarrow> 0 < Re(z)"
   3.532 +    shows "(csqrt has_field_derivative inverse(2 * csqrt z)) (at z)"
   3.533 +proof -
   3.534 +  have z: "z \<noteq> 0"
   3.535 +    using assms by auto
   3.536 +  then have *: "inverse z = inverse (2*z) * 2"
   3.537 +    by (simp add: divide_simps)
   3.538 +  show ?thesis
   3.539 +    apply (rule DERIV_transform_at [where f = "\<lambda>z. exp(Ln(z) / 2)" and d = "norm z"])
   3.540 +    apply (intro derivative_eq_intros | simp add: assms)+
   3.541 +    apply (rule *)
   3.542 +    using z
   3.543 +    apply (auto simp: field_simps csqrt_exp_Ln [symmetric])
   3.544 +    apply (metis power2_csqrt power2_eq_square)
   3.545 +    apply (metis csqrt_exp_Ln dist_0_norm less_irrefl)
   3.546 +    done
   3.547 +qed
   3.548 +
   3.549 +lemma complex_differentiable_at_csqrt:
   3.550 +    "(Im z = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> csqrt complex_differentiable at z"
   3.551 +  using complex_differentiable_def has_field_derivative_csqrt by blast
   3.552 +
   3.553 +lemma complex_differentiable_within_csqrt:
   3.554 +    "(Im z = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> csqrt complex_differentiable (at z within s)"
   3.555 +  using complex_differentiable_at_csqrt complex_differentiable_within_subset by blast
   3.556 +
   3.557 +lemma continuous_at_csqrt:
   3.558 +    "(Im z = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous (at z) csqrt"
   3.559 +  by (simp add: complex_differentiable_within_csqrt complex_differentiable_imp_continuous_at)
   3.560 +
   3.561 +lemma continuous_within_csqrt:
   3.562 +    "(Im z = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous (at z within s) csqrt"
   3.563 +  by (simp add: complex_differentiable_imp_continuous_at complex_differentiable_within_csqrt)
   3.564 +
   3.565 +lemma continuous_on_csqrt [continuous_intros]:
   3.566 +    "(\<And>z. z \<in> s \<and> Im z = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous_on s csqrt"
   3.567 +  by (simp add: continuous_at_imp_continuous_on continuous_within_csqrt)
   3.568 +
   3.569 +lemma holomorphic_on_csqrt:
   3.570 +    "(\<And>z. z \<in> s \<and> Im z = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> csqrt holomorphic_on s"
   3.571 +  by (simp add: complex_differentiable_within_csqrt holomorphic_on_def)
   3.572 +
   3.573 +lemma continuous_within_closed_nontrivial:
   3.574 +    "closed s \<Longrightarrow> a \<notin> s ==> continuous (at a within s) f"
   3.575 +  using open_Compl
   3.576 +  by (force simp add: continuous_def eventually_at_topological filterlim_iff open_Collect_neg)
   3.577 +
   3.578 +lemma closed_Real_halfspace_Re_ge: "closed (\<real> \<inter> {w. x \<le> Re(w)})"
   3.579 +  using closed_halfspace_Re_ge
   3.580 +  by (simp add: closed_Int closed_complex_Reals)
   3.581 +
   3.582 +lemma continuous_within_csqrt_posreal:
   3.583 +    "continuous (at z within (\<real> \<inter> {w. 0 \<le> Re(w)})) csqrt"
   3.584 +proof (cases "Im z = 0 --> 0 < Re(z)")
   3.585 +  case True then show ?thesis
   3.586 +    by (blast intro: continuous_within_csqrt)
   3.587 +next
   3.588 +  case False
   3.589 +  then have "Im z = 0" "Re z < 0 \<or> z = 0"
   3.590 +    using False cnj.code complex_cnj_zero_iff by auto force
   3.591 +  then show ?thesis
   3.592 +    apply (auto simp: continuous_within_closed_nontrivial [OF closed_Real_halfspace_Re_ge])
   3.593 +    apply (auto simp: continuous_within_eps_delta norm_conv_dist [symmetric])
   3.594 +    apply (rule_tac x="e^2" in exI)
   3.595 +    apply (auto simp: Reals_def)
   3.596 +by (metis linear not_less real_sqrt_less_iff real_sqrt_pow2_iff real_sqrt_power)
   3.597 +qed
   3.598 +
   3.599 +
   3.600  end
     4.1 --- a/src/HOL/Transcendental.thy	Thu Mar 19 11:54:20 2015 +0100
     4.2 +++ b/src/HOL/Transcendental.thy	Thu Mar 19 14:24:51 2015 +0000
     4.3 @@ -3391,7 +3391,7 @@
     4.4    thus ?thesis by auto
     4.5  qed
     4.6  
     4.7 -lemma cos_monotone_0_pi':
     4.8 +lemma cos_monotone_0_pi_le:
     4.9    assumes "0 \<le> y" and "y \<le> x" and "x \<le> pi"
    4.10    shows "cos x \<le> cos y"
    4.11  proof (cases "y < x")
    4.12 @@ -3427,16 +3427,19 @@
    4.13    thus ?thesis by auto
    4.14  qed
    4.15  
    4.16 -lemma sin_monotone_2pi':
    4.17 +lemma sin_monotone_2pi:
    4.18 +  assumes "- (pi/2) \<le> y" and "y < x" and "x \<le> pi/2"
    4.19 +  shows "sin y < sin x"
    4.20 +    apply (simp add: sin_cos_eq)
    4.21 +    apply (rule cos_monotone_0_pi)
    4.22 +    using assms
    4.23 +    apply auto
    4.24 +    done
    4.25 +
    4.26 +lemma sin_monotone_2pi_le:
    4.27    assumes "- (pi / 2) \<le> y" and "y \<le> x" and "x \<le> pi / 2"
    4.28    shows "sin y \<le> sin x"
    4.29 -proof -
    4.30 -  have "0 \<le> y + pi / 2" and "y + pi / 2 \<le> x + pi / 2" and "x + pi /2 \<le> pi"
    4.31 -    using pi_ge_two and assms by auto
    4.32 -  from cos_monotone_0_pi'[OF this] show ?thesis
    4.33 -    unfolding minus_sin_cos_eq[symmetric]
    4.34 -    by (metis minus_sin_cos_eq mult.right_neutral neg_le_iff_le of_real_def real_scaleR_def)
    4.35 -qed
    4.36 +  by (metis assms le_less sin_monotone_2pi)
    4.37  
    4.38  lemma sin_x_le_x:
    4.39    fixes x::real assumes x: "x \<ge> 0" shows "sin x \<le> x"
    4.40 @@ -3468,6 +3471,191 @@
    4.41    by (auto simp: abs_real_def)
    4.42  
    4.43  
    4.44 +subsection {* More Corollaries about Sine and Cosine *}
    4.45 +
    4.46 +lemma sin_cos_npi [simp]: "sin (real (Suc (2 * n)) * pi / 2) = (-1) ^ n"
    4.47 +proof -
    4.48 +  have "sin ((real n + 1/2) * pi) = cos (real n * pi)"
    4.49 +    by (auto simp: algebra_simps sin_add)
    4.50 +  thus ?thesis
    4.51 +    by (simp add: real_of_nat_Suc distrib_right add_divide_distrib
    4.52 +                  mult.commute [of pi])
    4.53 +qed
    4.54 +
    4.55 +lemma cos_2npi [simp]: "cos (2 * real (n::nat) * pi) = 1"
    4.56 +  by (cases "even n") (simp_all add: cos_double mult.assoc)
    4.57 +
    4.58 +lemma cos_3over2_pi [simp]: "cos (3/2*pi) = 0"
    4.59 +  apply (subgoal_tac "cos (pi + pi/2) = 0", simp)
    4.60 +  apply (subst cos_add, simp)
    4.61 +  done
    4.62 +
    4.63 +lemma sin_2npi [simp]: "sin (2 * real (n::nat) * pi) = 0"
    4.64 +  by (auto simp: mult.assoc sin_double)
    4.65 +
    4.66 +lemma sin_3over2_pi [simp]: "sin (3/2*pi) = - 1"
    4.67 +  apply (subgoal_tac "sin (pi + pi/2) = - 1", simp)
    4.68 +  apply (subst sin_add, simp)
    4.69 +  done
    4.70 +
    4.71 +lemma cos_pi_eq_zero [simp]: "cos (pi * real (Suc (2 * m)) / 2) = 0"
    4.72 +by (simp only: cos_add sin_add real_of_nat_Suc distrib_right distrib_left add_divide_distrib, auto)
    4.73 +
    4.74 +lemma DERIV_cos_add [simp]: "DERIV (\<lambda>x. cos (x + k)) xa :> - sin (xa + k)"
    4.75 +  by (auto intro!: derivative_eq_intros)
    4.76 +
    4.77 +lemma sin_zero_norm_cos_one:
    4.78 +  fixes x :: "'a::{real_normed_field,banach}"
    4.79 +  assumes "sin x = 0" shows "norm (cos x) = 1"
    4.80 +  using sin_cos_squared_add [of x, unfolded assms]
    4.81 +  by (simp add: square_norm_one)
    4.82 +
    4.83 +lemma sin_zero_abs_cos_one: "sin x = 0 \<Longrightarrow> \<bar>cos x\<bar> = (1::real)"
    4.84 +  using sin_zero_norm_cos_one by fastforce
    4.85 +
    4.86 +lemma cos_one_sin_zero:
    4.87 +  fixes x :: "'a::{real_normed_field,banach}"
    4.88 +  assumes "cos x = 1" shows "sin x = 0"
    4.89 +  using sin_cos_squared_add [of x, unfolded assms]
    4.90 +  by simp
    4.91 +
    4.92 +lemma sin_times_pi_eq_0: "sin(x * pi) = 0 \<longleftrightarrow> x \<in> Ints"
    4.93 +  by (simp add: sin_zero_iff_int2) (metis Ints_cases Ints_real_of_int real_of_int_def)
    4.94 +
    4.95 +lemma cos_one_2pi: 
    4.96 +    "cos(x) = 1 \<longleftrightarrow> (\<exists>n::nat. x = n * 2*pi) | (\<exists>n::nat. x = -(n * 2*pi))"
    4.97 +    (is "?lhs = ?rhs")
    4.98 +proof
    4.99 +  assume "cos(x) = 1"
   4.100 +  then have "sin x = 0"
   4.101 +    by (simp add: cos_one_sin_zero)
   4.102 +  then show ?rhs
   4.103 +  proof (simp only: sin_zero_iff, elim exE disjE conjE)
   4.104 +    fix n::nat
   4.105 +    assume n: "even n" "x = real n * (pi/2)"
   4.106 +    then obtain m where m: "n = 2 * m"
   4.107 +      using dvdE by blast
   4.108 +    then have me: "even m" using `?lhs` n
   4.109 +      by (auto simp: field_simps) (metis one_neq_neg_one  power_minus_odd power_one)
   4.110 +    show ?rhs
   4.111 +      using m me n
   4.112 +      by (auto simp: field_simps elim!: evenE)
   4.113 +  next    
   4.114 +    fix n::nat
   4.115 +    assume n: "even n" "x = - (real n * (pi/2))"
   4.116 +    then obtain m where m: "n = 2 * m"
   4.117 +      using dvdE by blast
   4.118 +    then have me: "even m" using `?lhs` n
   4.119 +      by (auto simp: field_simps) (metis one_neq_neg_one  power_minus_odd power_one)
   4.120 +    show ?rhs
   4.121 +      using m me n
   4.122 +      by (auto simp: field_simps elim!: evenE)
   4.123 +  qed
   4.124 +next
   4.125 +  assume "?rhs"
   4.126 +  then show "cos x = 1"
   4.127 +    by (metis cos_2npi cos_minus mult.assoc mult.left_commute)
   4.128 +qed
   4.129 +
   4.130 +lemma cos_one_2pi_int: "cos(x) = 1 \<longleftrightarrow> (\<exists>n::int. x = n * 2*pi)"
   4.131 +  apply auto  --{*FIXME simproc bug*}
   4.132 +  apply (auto simp: cos_one_2pi)
   4.133 +  apply (metis real_of_int_of_nat_eq)
   4.134 +  apply (metis mult_minus_right real_of_int_minus real_of_int_of_nat_eq)
   4.135 +  by (metis mult_minus_right of_int_of_nat real_of_int_def real_of_nat_def)
   4.136 +
   4.137 +lemma sin_cos_sqrt: "0 \<le> sin(x) \<Longrightarrow> (sin(x) = sqrt(1 - (cos(x) ^ 2)))"
   4.138 +  using sin_squared_eq real_sqrt_unique by fastforce
   4.139 +
   4.140 +lemma sin_eq_0_pi: "-pi < x \<Longrightarrow> x < pi \<Longrightarrow> sin(x) = 0 \<Longrightarrow> x = 0"
   4.141 +  by (metis sin_gt_zero sin_minus minus_less_iff neg_0_less_iff_less not_less_iff_gr_or_eq)
   4.142 +
   4.143 +lemma cos_treble_cos: 
   4.144 +  fixes x :: "'a::{real_normed_field,banach}"
   4.145 +  shows "cos(3 * x) = 4 * cos(x) ^ 3 - 3 * cos x"
   4.146 +proof -
   4.147 +  have *: "(sin x * (sin x * 3)) = 3 - (cos x * (cos x * 3))"
   4.148 +    by (simp add: mult.assoc [symmetric] sin_squared_eq [unfolded power2_eq_square])
   4.149 +  have "cos(3 * x) = cos(2*x + x)"
   4.150 +    by simp
   4.151 +  also have "... = 4 * cos(x) ^ 3 - 3 * cos x"
   4.152 +    apply (simp only: cos_add cos_double sin_double)
   4.153 +    apply (simp add: * field_simps power2_eq_square power3_eq_cube)
   4.154 +    done
   4.155 +  finally show ?thesis .
   4.156 +qed
   4.157 +
   4.158 +lemma cos_45: "cos (pi / 4) = sqrt 2 / 2"
   4.159 +proof -
   4.160 +  let ?c = "cos (pi / 4)" and ?s = "sin (pi / 4)"
   4.161 +  have nonneg: "0 \<le> ?c"
   4.162 +    by (simp add: cos_ge_zero)
   4.163 +  have "0 = cos (pi / 4 + pi / 4)"
   4.164 +    by simp
   4.165 +  also have "cos (pi / 4 + pi / 4) = ?c\<^sup>2 - ?s\<^sup>2"
   4.166 +    by (simp only: cos_add power2_eq_square)
   4.167 +  also have "\<dots> = 2 * ?c\<^sup>2 - 1"
   4.168 +    by (simp add: sin_squared_eq)
   4.169 +  finally have "?c\<^sup>2 = (sqrt 2 / 2)\<^sup>2"
   4.170 +    by (simp add: power_divide)
   4.171 +  thus ?thesis
   4.172 +    using nonneg by (rule power2_eq_imp_eq) simp
   4.173 +qed
   4.174 +
   4.175 +lemma cos_30: "cos (pi / 6) = sqrt 3/2"
   4.176 +proof -
   4.177 +  let ?c = "cos (pi / 6)" and ?s = "sin (pi / 6)"
   4.178 +  have pos_c: "0 < ?c"
   4.179 +    by (rule cos_gt_zero, simp, simp)
   4.180 +  have "0 = cos (pi / 6 + pi / 6 + pi / 6)"
   4.181 +    by simp
   4.182 +  also have "\<dots> = (?c * ?c - ?s * ?s) * ?c - (?s * ?c + ?c * ?s) * ?s"
   4.183 +    by (simp only: cos_add sin_add)
   4.184 +  also have "\<dots> = ?c * (?c\<^sup>2 - 3 * ?s\<^sup>2)"
   4.185 +    by (simp add: algebra_simps power2_eq_square)
   4.186 +  finally have "?c\<^sup>2 = (sqrt 3/2)\<^sup>2"
   4.187 +    using pos_c by (simp add: sin_squared_eq power_divide)
   4.188 +  thus ?thesis
   4.189 +    using pos_c [THEN order_less_imp_le]
   4.190 +    by (rule power2_eq_imp_eq) simp
   4.191 +qed
   4.192 +
   4.193 +lemma sin_45: "sin (pi / 4) = sqrt 2 / 2"
   4.194 +  by (simp add: sin_cos_eq cos_45)
   4.195 +
   4.196 +lemma sin_60: "sin (pi / 3) = sqrt 3/2"
   4.197 +  by (simp add: sin_cos_eq cos_30)
   4.198 +
   4.199 +lemma cos_60: "cos (pi / 3) = 1 / 2"
   4.200 +  apply (rule power2_eq_imp_eq)
   4.201 +  apply (simp add: cos_squared_eq sin_60 power_divide)
   4.202 +  apply (rule cos_ge_zero, rule order_trans [where y=0], simp_all)
   4.203 +  done
   4.204 +
   4.205 +lemma sin_30: "sin (pi / 6) = 1 / 2"
   4.206 +  by (simp add: sin_cos_eq cos_60)
   4.207 +
   4.208 +lemma cos_integer_2pi: "n \<in> Ints \<Longrightarrow> cos(2*pi * n) = 1"
   4.209 +  by (metis Ints_cases cos_one_2pi_int mult.assoc mult.commute real_of_int_def)
   4.210 +
   4.211 +lemma sin_integer_2pi: "n \<in> Ints \<Longrightarrow> sin(2*pi * n) = 0"
   4.212 +  by (metis sin_two_pi Ints_mult mult.assoc mult.commute sin_times_pi_eq_0)
   4.213 +
   4.214 +lemma cos_int_2npi [simp]: "cos (2 * real (n::int) * pi) = 1"
   4.215 +  by (simp add: cos_one_2pi_int)
   4.216 +
   4.217 +lemma sin_int_2npi [simp]: "sin (2 * real (n::int) * pi) = 0"
   4.218 +  by (metis Ints_real_of_int mult.assoc mult.commute sin_integer_2pi)
   4.219 +
   4.220 +lemma sincos_principal_value: "\<exists>y. (-pi < y \<and> y \<le> pi) \<and> (sin(y) = sin(x) \<and> cos(y) = cos(x))"
   4.221 +  apply (rule exI [where x="pi - (2*pi) * frac((pi - x) / (2*pi))"])
   4.222 +  apply (auto simp: field_simps frac_lt_1)
   4.223 +  apply (simp_all add: frac_def divide_simps)
   4.224 +  apply (simp_all add: add_divide_distrib diff_divide_distrib)
   4.225 +  apply (simp_all add: sin_diff cos_diff mult.assoc [symmetric] cos_integer_2pi sin_integer_2pi)
   4.226 +  done
   4.227 +
   4.228 +
   4.229  subsection {* Tangent *}
   4.230  
   4.231  definition tan :: "'a \<Rightarrow> 'a::{real_normed_field,banach}"
   4.232 @@ -3528,6 +3716,15 @@
   4.233    unfolding tan_def sin_double cos_double sin_squared_eq
   4.234    by (simp add: power2_eq_square)
   4.235  
   4.236 +lemma tan_30: "tan (pi / 6) = 1 / sqrt 3"
   4.237 +  unfolding tan_def by (simp add: sin_30 cos_30)
   4.238 +
   4.239 +lemma tan_45: "tan (pi / 4) = 1"
   4.240 +  unfolding tan_def by (simp add: sin_45 cos_45)
   4.241 +
   4.242 +lemma tan_60: "tan (pi / 3) = sqrt 3"
   4.243 +  unfolding tan_def by (simp add: sin_60 cos_60)
   4.244 +
   4.245  lemma DERIV_tan [simp]:
   4.246    fixes x :: "'a::{real_normed_field,banach}"
   4.247    shows "cos x \<noteq> 0 \<Longrightarrow> DERIV tan x :> inverse ((cos x)\<^sup>2)"
   4.248 @@ -3705,9 +3902,48 @@
   4.249  lemma tan_periodic_n[simp]: "tan (x + numeral n * pi) = tan x"
   4.250    using tan_periodic_int[of _ "numeral n" ] unfolding real_numeral .
   4.251  
   4.252 +lemma tan_minus_45: "tan (-(pi/4)) = -1"
   4.253 +  unfolding tan_def by (simp add: sin_45 cos_45)
   4.254 +
   4.255 +lemma tan_diff:
   4.256 +  fixes x :: "'a::{real_normed_field,banach}"
   4.257 +  shows
   4.258 +     "\<lbrakk>cos x \<noteq> 0; cos y \<noteq> 0; cos (x - y) \<noteq> 0\<rbrakk>
   4.259 +      \<Longrightarrow> tan(x - y) = (tan(x) - tan(y))/(1 + tan(x) * tan(y))"
   4.260 +  using tan_add [of x "-y"]
   4.261 +  by simp
   4.262 +
   4.263 +
   4.264 +lemma tan_pos_pi2_le: "0 \<le> x ==> x < pi/2 \<Longrightarrow> 0 \<le> tan x"
   4.265 +  using less_eq_real_def tan_gt_zero by auto
   4.266 +
   4.267 +lemma cos_tan: "abs(x) < pi/2 \<Longrightarrow> cos(x) = 1 / sqrt(1 + tan(x) ^ 2)"
   4.268 +  using cos_gt_zero_pi [of x]
   4.269 +  by (simp add: divide_simps tan_def real_sqrt_divide abs_if split: split_if_asm)
   4.270 +
   4.271 +lemma sin_tan: "abs(x) < pi/2 \<Longrightarrow> sin(x) = tan(x) / sqrt(1 + tan(x) ^ 2)"
   4.272 +  using cos_gt_zero [of "x"] cos_gt_zero [of "-x"]
   4.273 +  by (force simp add: divide_simps tan_def real_sqrt_divide abs_if split: split_if_asm)
   4.274 +
   4.275 +lemma tan_mono_le: "-(pi/2) < x ==> x \<le> y ==> y < pi/2 \<Longrightarrow> tan(x) \<le> tan(y)"
   4.276 +  using less_eq_real_def tan_monotone by auto
   4.277 +
   4.278 +lemma tan_mono_lt_eq: "-(pi/2) < x ==> x < pi/2 ==> -(pi/2) < y ==> y < pi/2
   4.279 +         \<Longrightarrow> (tan(x) < tan(y) \<longleftrightarrow> x < y)"
   4.280 +  using tan_monotone' by blast
   4.281 +
   4.282 +lemma tan_mono_le_eq: "-(pi/2) < x ==> x < pi/2 ==> -(pi/2) < y ==> y < pi/2
   4.283 +         \<Longrightarrow> (tan(x) \<le> tan(y) \<longleftrightarrow> x \<le> y)"
   4.284 +  by (meson tan_mono_le not_le tan_monotone)
   4.285 +
   4.286 +lemma tan_bound_pi2: "abs(x) < pi/4 \<Longrightarrow> abs(tan x) < 1"
   4.287 +  using tan_45 tan_monotone [of x "pi/4"] tan_monotone [of "-x" "pi/4"]
   4.288 +  by (auto simp: abs_if split: split_if_asm)
   4.289 +
   4.290 +lemma tan_cot: "tan(pi/2 - x) = inverse(tan x)"
   4.291 +  by (simp add: tan_def sin_diff cos_diff)
   4.292  
   4.293  subsection {* Inverse Trigonometric Functions *}
   4.294 -text{*STILL DEFINED FOR THE REALS ONLY*}
   4.295  
   4.296  definition arcsin :: "real => real"
   4.297    where "arcsin y = (THE x. -(pi/2) \<le> x & x \<le> pi/2 & sin x = y)"
   4.298 @@ -3820,6 +4056,12 @@
   4.299    apply (rule power_mono, simp, simp)
   4.300    done
   4.301  
   4.302 +lemma arccos_0 [simp]: "arccos 0 = pi/2"
   4.303 +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)
   4.304 +
   4.305 +lemma arccos_1 [simp]: "arccos 1 = 0"
   4.306 +  using arccos_cos by force
   4.307 +
   4.308  lemma arctan [simp]: "- (pi/2) < arctan y  & arctan y < pi/2 & tan (arctan y) = y"
   4.309    unfolding arctan_def by (rule theI' [OF tan_total])
   4.310  
   4.311 @@ -4049,124 +4291,34 @@
   4.312    by (intro tendsto_minus tendsto_arctan_at_top)
   4.313  
   4.314  
   4.315 -subsection {* More Theorems about Sin and Cos *}
   4.316 -
   4.317 -lemma cos_45: "cos (pi / 4) = sqrt 2 / 2"
   4.318 -proof -
   4.319 -  let ?c = "cos (pi / 4)" and ?s = "sin (pi / 4)"
   4.320 -  have nonneg: "0 \<le> ?c"
   4.321 -    by (simp add: cos_ge_zero)
   4.322 -  have "0 = cos (pi / 4 + pi / 4)"
   4.323 -    by simp
   4.324 -  also have "cos (pi / 4 + pi / 4) = ?c\<^sup>2 - ?s\<^sup>2"
   4.325 -    by (simp only: cos_add power2_eq_square)
   4.326 -  also have "\<dots> = 2 * ?c\<^sup>2 - 1"
   4.327 -    by (simp add: sin_squared_eq)
   4.328 -  finally have "?c\<^sup>2 = (sqrt 2 / 2)\<^sup>2"
   4.329 -    by (simp add: power_divide)
   4.330 -  thus ?thesis
   4.331 -    using nonneg by (rule power2_eq_imp_eq) simp
   4.332 -qed
   4.333 -
   4.334 -lemma cos_30: "cos (pi / 6) = sqrt 3/2"
   4.335 -proof -
   4.336 -  let ?c = "cos (pi / 6)" and ?s = "sin (pi / 6)"
   4.337 -  have pos_c: "0 < ?c"
   4.338 -    by (rule cos_gt_zero, simp, simp)
   4.339 -  have "0 = cos (pi / 6 + pi / 6 + pi / 6)"
   4.340 -    by simp
   4.341 -  also have "\<dots> = (?c * ?c - ?s * ?s) * ?c - (?s * ?c + ?c * ?s) * ?s"
   4.342 -    by (simp only: cos_add sin_add)
   4.343 -  also have "\<dots> = ?c * (?c\<^sup>2 - 3 * ?s\<^sup>2)"
   4.344 -    by (simp add: algebra_simps power2_eq_square)
   4.345 -  finally have "?c\<^sup>2 = (sqrt 3/2)\<^sup>2"
   4.346 -    using pos_c by (simp add: sin_squared_eq power_divide)
   4.347 -  thus ?thesis
   4.348 -    using pos_c [THEN order_less_imp_le]
   4.349 -    by (rule power2_eq_imp_eq) simp
   4.350 -qed
   4.351 -
   4.352 -lemma sin_45: "sin (pi / 4) = sqrt 2 / 2"
   4.353 -  by (simp add: sin_cos_eq cos_45)
   4.354 -
   4.355 -lemma sin_60: "sin (pi / 3) = sqrt 3/2"
   4.356 -  by (simp add: sin_cos_eq cos_30)
   4.357 -
   4.358 -lemma cos_60: "cos (pi / 3) = 1 / 2"
   4.359 -  apply (rule power2_eq_imp_eq)
   4.360 -  apply (simp add: cos_squared_eq sin_60 power_divide)
   4.361 -  apply (rule cos_ge_zero, rule order_trans [where y=0], simp_all)
   4.362 -  done
   4.363 -
   4.364 -lemma sin_30: "sin (pi / 6) = 1 / 2"
   4.365 -  by (simp add: sin_cos_eq cos_60)
   4.366 -
   4.367 -lemma tan_30: "tan (pi / 6) = 1 / sqrt 3"
   4.368 -  unfolding tan_def by (simp add: sin_30 cos_30)
   4.369 -
   4.370 -lemma tan_45: "tan (pi / 4) = 1"
   4.371 -  unfolding tan_def by (simp add: sin_45 cos_45)
   4.372 -
   4.373 -lemma tan_60: "tan (pi / 3) = sqrt 3"
   4.374 -  unfolding tan_def by (simp add: sin_60 cos_60)
   4.375 -
   4.376 -lemma sin_cos_npi [simp]: "sin (real (Suc (2 * n)) * pi / 2) = (-1) ^ n"
   4.377 -proof -
   4.378 -  have "sin ((real n + 1/2) * pi) = cos (real n * pi)"
   4.379 -    by (auto simp: algebra_simps sin_add)
   4.380 -  thus ?thesis
   4.381 -    by (simp add: real_of_nat_Suc distrib_right add_divide_distrib
   4.382 -                  mult.commute [of pi])
   4.383 -qed
   4.384 -
   4.385 -lemma cos_2npi [simp]: "cos (2 * real (n::nat) * pi) = 1"
   4.386 -  by (cases "even n") (simp_all add: cos_double mult.assoc)
   4.387 -
   4.388 -lemma cos_3over2_pi [simp]: "cos (3/2*pi) = 0"
   4.389 -  apply (subgoal_tac "cos (pi + pi/2) = 0", simp)
   4.390 -  apply (subst cos_add, simp)
   4.391 -  done
   4.392 -
   4.393 -lemma sin_2npi [simp]: "sin (2 * real (n::nat) * pi) = 0"
   4.394 -  by (auto simp: mult.assoc sin_double)
   4.395 -
   4.396 -lemma sin_3over2_pi [simp]: "sin (3/2*pi) = - 1"
   4.397 -  apply (subgoal_tac "sin (pi + pi/2) = - 1", simp)
   4.398 -  apply (subst sin_add, simp)
   4.399 -  done
   4.400 -
   4.401 -lemma cos_pi_eq_zero [simp]: "cos (pi * real (Suc (2 * m)) / 2) = 0"
   4.402 -by (simp only: cos_add sin_add real_of_nat_Suc distrib_right distrib_left add_divide_distrib, auto)
   4.403 -
   4.404 -lemma DERIV_cos_add [simp]: "DERIV (\<lambda>x. cos (x + k)) xa :> - sin (xa + k)"
   4.405 -  by (auto intro!: derivative_eq_intros)
   4.406 -
   4.407 -lemma sin_zero_norm_cos_one:
   4.408 -  fixes x :: "'a::{real_normed_field,banach}"
   4.409 -  assumes "sin x = 0" shows "norm (cos x) = 1"
   4.410 -  using sin_cos_squared_add [of x, unfolded assms]
   4.411 -  by (simp add: square_norm_one)
   4.412 -
   4.413 -lemma sin_zero_abs_cos_one: "sin x = 0 \<Longrightarrow> \<bar>cos x\<bar> = (1::real)"
   4.414 -  using sin_zero_norm_cos_one by fastforce
   4.415 -
   4.416 -lemma cos_one_sin_zero:
   4.417 -  fixes x :: "'a::{real_normed_field,banach}"
   4.418 -  assumes "cos x = 1" shows "sin x = 0"
   4.419 -  using sin_cos_squared_add [of x, unfolded assms]
   4.420 -  by simp
   4.421 -
   4.422 -
   4.423  subsection{* Prove Totality of the Trigonometric Functions *}
   4.424  
   4.425 -lemma arccos_0 [simp]: "arccos 0 = pi/2"
   4.426 -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)
   4.427 -
   4.428 -lemma arccos_1 [simp]: "arccos 1 = 0"
   4.429 -  using arccos_cos by force
   4.430 +lemma sin_mono_less_eq: "\<lbrakk>-(pi/2) \<le> x; x \<le> pi/2; -(pi/2) \<le> y; y \<le> pi/2\<rbrakk>
   4.431 +         \<Longrightarrow> (sin(x) < sin(y) \<longleftrightarrow> x < y)"
   4.432 +by (metis not_less_iff_gr_or_eq sin_monotone_2pi)
   4.433 +
   4.434 +lemma sin_mono_le_eq: "\<lbrakk>-(pi/2) \<le> x; x \<le> pi/2; -(pi/2) \<le> y; y \<le> pi/2\<rbrakk>
   4.435 +         \<Longrightarrow> (sin(x) \<le> sin(y) \<longleftrightarrow> x \<le> y)"
   4.436 +by (meson leD le_less_linear sin_monotone_2pi sin_monotone_2pi_le)
   4.437 +
   4.438 +lemma sin_inj_pi: "-(pi/2) \<le> x ==> x \<le> pi/2 ==>
   4.439 +         -(pi/2) \<le> y ==> y \<le> pi/2 ==> sin(x) = sin(y) \<Longrightarrow> x = y"
   4.440 +by (metis arcsin_sin)
   4.441 +
   4.442 +lemma cos_mono_lt_eq: "0 \<le> x ==> x \<le> pi ==> 0 \<le> y ==> y \<le> pi
   4.443 +         \<Longrightarrow> (cos(x) < cos(y) \<longleftrightarrow> y < x)"
   4.444 +by (meson cos_monotone_0_pi cos_monotone_0_pi_le leD le_less_linear)
   4.445 +
   4.446 +lemma cos_mono_le_eq: "0 \<le> x ==> x \<le> pi ==> 0 \<le> y ==> y \<le> pi
   4.447 +         \<Longrightarrow> (cos(x) \<le> cos(y) \<longleftrightarrow> y \<le> x)"
   4.448 +  by (metis arccos_cos cos_monotone_0_pi_le eq_iff linear)
   4.449 +
   4.450 +lemma cos_inj_pi: "0 \<le> x ==> x \<le> pi ==> 0 \<le> y ==> y \<le> pi ==> cos(x) = cos(y)
   4.451 +         \<Longrightarrow> x = y"
   4.452 +by (metis arccos_cos)
   4.453  
   4.454  lemma arccos_le_pi2: "\<lbrakk>0 \<le> y; y \<le> 1\<rbrakk> \<Longrightarrow> arccos y \<le> pi/2"
   4.455 -  by (metis (mono_tags) arccos_0 arccos cos_le_one cos_monotone_0_pi'
   4.456 +  by (metis (mono_tags) arccos_0 arccos cos_le_one cos_monotone_0_pi_le
   4.457        cos_pi cos_pi_half pi_half_ge_zero antisym_conv less_eq_neg_nonpos linear minus_minus order.trans order_refl)
   4.458  
   4.459  lemma sincos_total_pi_half: