src/HOL/Transcendental.thy
changeset 59751 916c0f6c83e3
parent 59746 ddae5727c5a9
child 59862 44b3f4fa33ca
     1.1 --- a/src/HOL/Transcendental.thy	Thu Mar 19 11:54:20 2015 +0100
     1.2 +++ b/src/HOL/Transcendental.thy	Thu Mar 19 14:24:51 2015 +0000
     1.3 @@ -3391,7 +3391,7 @@
     1.4    thus ?thesis by auto
     1.5  qed
     1.6  
     1.7 -lemma cos_monotone_0_pi':
     1.8 +lemma cos_monotone_0_pi_le:
     1.9    assumes "0 \<le> y" and "y \<le> x" and "x \<le> pi"
    1.10    shows "cos x \<le> cos y"
    1.11  proof (cases "y < x")
    1.12 @@ -3427,16 +3427,19 @@
    1.13    thus ?thesis by auto
    1.14  qed
    1.15  
    1.16 -lemma sin_monotone_2pi':
    1.17 +lemma sin_monotone_2pi:
    1.18 +  assumes "- (pi/2) \<le> y" and "y < x" and "x \<le> pi/2"
    1.19 +  shows "sin y < sin x"
    1.20 +    apply (simp add: sin_cos_eq)
    1.21 +    apply (rule cos_monotone_0_pi)
    1.22 +    using assms
    1.23 +    apply auto
    1.24 +    done
    1.25 +
    1.26 +lemma sin_monotone_2pi_le:
    1.27    assumes "- (pi / 2) \<le> y" and "y \<le> x" and "x \<le> pi / 2"
    1.28    shows "sin y \<le> sin x"
    1.29 -proof -
    1.30 -  have "0 \<le> y + pi / 2" and "y + pi / 2 \<le> x + pi / 2" and "x + pi /2 \<le> pi"
    1.31 -    using pi_ge_two and assms by auto
    1.32 -  from cos_monotone_0_pi'[OF this] show ?thesis
    1.33 -    unfolding minus_sin_cos_eq[symmetric]
    1.34 -    by (metis minus_sin_cos_eq mult.right_neutral neg_le_iff_le of_real_def real_scaleR_def)
    1.35 -qed
    1.36 +  by (metis assms le_less sin_monotone_2pi)
    1.37  
    1.38  lemma sin_x_le_x:
    1.39    fixes x::real assumes x: "x \<ge> 0" shows "sin x \<le> x"
    1.40 @@ -3468,6 +3471,191 @@
    1.41    by (auto simp: abs_real_def)
    1.42  
    1.43  
    1.44 +subsection {* More Corollaries about Sine and Cosine *}
    1.45 +
    1.46 +lemma sin_cos_npi [simp]: "sin (real (Suc (2 * n)) * pi / 2) = (-1) ^ n"
    1.47 +proof -
    1.48 +  have "sin ((real n + 1/2) * pi) = cos (real n * pi)"
    1.49 +    by (auto simp: algebra_simps sin_add)
    1.50 +  thus ?thesis
    1.51 +    by (simp add: real_of_nat_Suc distrib_right add_divide_distrib
    1.52 +                  mult.commute [of pi])
    1.53 +qed
    1.54 +
    1.55 +lemma cos_2npi [simp]: "cos (2 * real (n::nat) * pi) = 1"
    1.56 +  by (cases "even n") (simp_all add: cos_double mult.assoc)
    1.57 +
    1.58 +lemma cos_3over2_pi [simp]: "cos (3/2*pi) = 0"
    1.59 +  apply (subgoal_tac "cos (pi + pi/2) = 0", simp)
    1.60 +  apply (subst cos_add, simp)
    1.61 +  done
    1.62 +
    1.63 +lemma sin_2npi [simp]: "sin (2 * real (n::nat) * pi) = 0"
    1.64 +  by (auto simp: mult.assoc sin_double)
    1.65 +
    1.66 +lemma sin_3over2_pi [simp]: "sin (3/2*pi) = - 1"
    1.67 +  apply (subgoal_tac "sin (pi + pi/2) = - 1", simp)
    1.68 +  apply (subst sin_add, simp)
    1.69 +  done
    1.70 +
    1.71 +lemma cos_pi_eq_zero [simp]: "cos (pi * real (Suc (2 * m)) / 2) = 0"
    1.72 +by (simp only: cos_add sin_add real_of_nat_Suc distrib_right distrib_left add_divide_distrib, auto)
    1.73 +
    1.74 +lemma DERIV_cos_add [simp]: "DERIV (\<lambda>x. cos (x + k)) xa :> - sin (xa + k)"
    1.75 +  by (auto intro!: derivative_eq_intros)
    1.76 +
    1.77 +lemma sin_zero_norm_cos_one:
    1.78 +  fixes x :: "'a::{real_normed_field,banach}"
    1.79 +  assumes "sin x = 0" shows "norm (cos x) = 1"
    1.80 +  using sin_cos_squared_add [of x, unfolded assms]
    1.81 +  by (simp add: square_norm_one)
    1.82 +
    1.83 +lemma sin_zero_abs_cos_one: "sin x = 0 \<Longrightarrow> \<bar>cos x\<bar> = (1::real)"
    1.84 +  using sin_zero_norm_cos_one by fastforce
    1.85 +
    1.86 +lemma cos_one_sin_zero:
    1.87 +  fixes x :: "'a::{real_normed_field,banach}"
    1.88 +  assumes "cos x = 1" shows "sin x = 0"
    1.89 +  using sin_cos_squared_add [of x, unfolded assms]
    1.90 +  by simp
    1.91 +
    1.92 +lemma sin_times_pi_eq_0: "sin(x * pi) = 0 \<longleftrightarrow> x \<in> Ints"
    1.93 +  by (simp add: sin_zero_iff_int2) (metis Ints_cases Ints_real_of_int real_of_int_def)
    1.94 +
    1.95 +lemma cos_one_2pi: 
    1.96 +    "cos(x) = 1 \<longleftrightarrow> (\<exists>n::nat. x = n * 2*pi) | (\<exists>n::nat. x = -(n * 2*pi))"
    1.97 +    (is "?lhs = ?rhs")
    1.98 +proof
    1.99 +  assume "cos(x) = 1"
   1.100 +  then have "sin x = 0"
   1.101 +    by (simp add: cos_one_sin_zero)
   1.102 +  then show ?rhs
   1.103 +  proof (simp only: sin_zero_iff, elim exE disjE conjE)
   1.104 +    fix n::nat
   1.105 +    assume n: "even n" "x = real n * (pi/2)"
   1.106 +    then obtain m where m: "n = 2 * m"
   1.107 +      using dvdE by blast
   1.108 +    then have me: "even m" using `?lhs` n
   1.109 +      by (auto simp: field_simps) (metis one_neq_neg_one  power_minus_odd power_one)
   1.110 +    show ?rhs
   1.111 +      using m me n
   1.112 +      by (auto simp: field_simps elim!: evenE)
   1.113 +  next    
   1.114 +    fix n::nat
   1.115 +    assume n: "even n" "x = - (real n * (pi/2))"
   1.116 +    then obtain m where m: "n = 2 * m"
   1.117 +      using dvdE by blast
   1.118 +    then have me: "even m" using `?lhs` n
   1.119 +      by (auto simp: field_simps) (metis one_neq_neg_one  power_minus_odd power_one)
   1.120 +    show ?rhs
   1.121 +      using m me n
   1.122 +      by (auto simp: field_simps elim!: evenE)
   1.123 +  qed
   1.124 +next
   1.125 +  assume "?rhs"
   1.126 +  then show "cos x = 1"
   1.127 +    by (metis cos_2npi cos_minus mult.assoc mult.left_commute)
   1.128 +qed
   1.129 +
   1.130 +lemma cos_one_2pi_int: "cos(x) = 1 \<longleftrightarrow> (\<exists>n::int. x = n * 2*pi)"
   1.131 +  apply auto  --{*FIXME simproc bug*}
   1.132 +  apply (auto simp: cos_one_2pi)
   1.133 +  apply (metis real_of_int_of_nat_eq)
   1.134 +  apply (metis mult_minus_right real_of_int_minus real_of_int_of_nat_eq)
   1.135 +  by (metis mult_minus_right of_int_of_nat real_of_int_def real_of_nat_def)
   1.136 +
   1.137 +lemma sin_cos_sqrt: "0 \<le> sin(x) \<Longrightarrow> (sin(x) = sqrt(1 - (cos(x) ^ 2)))"
   1.138 +  using sin_squared_eq real_sqrt_unique by fastforce
   1.139 +
   1.140 +lemma sin_eq_0_pi: "-pi < x \<Longrightarrow> x < pi \<Longrightarrow> sin(x) = 0 \<Longrightarrow> x = 0"
   1.141 +  by (metis sin_gt_zero sin_minus minus_less_iff neg_0_less_iff_less not_less_iff_gr_or_eq)
   1.142 +
   1.143 +lemma cos_treble_cos: 
   1.144 +  fixes x :: "'a::{real_normed_field,banach}"
   1.145 +  shows "cos(3 * x) = 4 * cos(x) ^ 3 - 3 * cos x"
   1.146 +proof -
   1.147 +  have *: "(sin x * (sin x * 3)) = 3 - (cos x * (cos x * 3))"
   1.148 +    by (simp add: mult.assoc [symmetric] sin_squared_eq [unfolded power2_eq_square])
   1.149 +  have "cos(3 * x) = cos(2*x + x)"
   1.150 +    by simp
   1.151 +  also have "... = 4 * cos(x) ^ 3 - 3 * cos x"
   1.152 +    apply (simp only: cos_add cos_double sin_double)
   1.153 +    apply (simp add: * field_simps power2_eq_square power3_eq_cube)
   1.154 +    done
   1.155 +  finally show ?thesis .
   1.156 +qed
   1.157 +
   1.158 +lemma cos_45: "cos (pi / 4) = sqrt 2 / 2"
   1.159 +proof -
   1.160 +  let ?c = "cos (pi / 4)" and ?s = "sin (pi / 4)"
   1.161 +  have nonneg: "0 \<le> ?c"
   1.162 +    by (simp add: cos_ge_zero)
   1.163 +  have "0 = cos (pi / 4 + pi / 4)"
   1.164 +    by simp
   1.165 +  also have "cos (pi / 4 + pi / 4) = ?c\<^sup>2 - ?s\<^sup>2"
   1.166 +    by (simp only: cos_add power2_eq_square)
   1.167 +  also have "\<dots> = 2 * ?c\<^sup>2 - 1"
   1.168 +    by (simp add: sin_squared_eq)
   1.169 +  finally have "?c\<^sup>2 = (sqrt 2 / 2)\<^sup>2"
   1.170 +    by (simp add: power_divide)
   1.171 +  thus ?thesis
   1.172 +    using nonneg by (rule power2_eq_imp_eq) simp
   1.173 +qed
   1.174 +
   1.175 +lemma cos_30: "cos (pi / 6) = sqrt 3/2"
   1.176 +proof -
   1.177 +  let ?c = "cos (pi / 6)" and ?s = "sin (pi / 6)"
   1.178 +  have pos_c: "0 < ?c"
   1.179 +    by (rule cos_gt_zero, simp, simp)
   1.180 +  have "0 = cos (pi / 6 + pi / 6 + pi / 6)"
   1.181 +    by simp
   1.182 +  also have "\<dots> = (?c * ?c - ?s * ?s) * ?c - (?s * ?c + ?c * ?s) * ?s"
   1.183 +    by (simp only: cos_add sin_add)
   1.184 +  also have "\<dots> = ?c * (?c\<^sup>2 - 3 * ?s\<^sup>2)"
   1.185 +    by (simp add: algebra_simps power2_eq_square)
   1.186 +  finally have "?c\<^sup>2 = (sqrt 3/2)\<^sup>2"
   1.187 +    using pos_c by (simp add: sin_squared_eq power_divide)
   1.188 +  thus ?thesis
   1.189 +    using pos_c [THEN order_less_imp_le]
   1.190 +    by (rule power2_eq_imp_eq) simp
   1.191 +qed
   1.192 +
   1.193 +lemma sin_45: "sin (pi / 4) = sqrt 2 / 2"
   1.194 +  by (simp add: sin_cos_eq cos_45)
   1.195 +
   1.196 +lemma sin_60: "sin (pi / 3) = sqrt 3/2"
   1.197 +  by (simp add: sin_cos_eq cos_30)
   1.198 +
   1.199 +lemma cos_60: "cos (pi / 3) = 1 / 2"
   1.200 +  apply (rule power2_eq_imp_eq)
   1.201 +  apply (simp add: cos_squared_eq sin_60 power_divide)
   1.202 +  apply (rule cos_ge_zero, rule order_trans [where y=0], simp_all)
   1.203 +  done
   1.204 +
   1.205 +lemma sin_30: "sin (pi / 6) = 1 / 2"
   1.206 +  by (simp add: sin_cos_eq cos_60)
   1.207 +
   1.208 +lemma cos_integer_2pi: "n \<in> Ints \<Longrightarrow> cos(2*pi * n) = 1"
   1.209 +  by (metis Ints_cases cos_one_2pi_int mult.assoc mult.commute real_of_int_def)
   1.210 +
   1.211 +lemma sin_integer_2pi: "n \<in> Ints \<Longrightarrow> sin(2*pi * n) = 0"
   1.212 +  by (metis sin_two_pi Ints_mult mult.assoc mult.commute sin_times_pi_eq_0)
   1.213 +
   1.214 +lemma cos_int_2npi [simp]: "cos (2 * real (n::int) * pi) = 1"
   1.215 +  by (simp add: cos_one_2pi_int)
   1.216 +
   1.217 +lemma sin_int_2npi [simp]: "sin (2 * real (n::int) * pi) = 0"
   1.218 +  by (metis Ints_real_of_int mult.assoc mult.commute sin_integer_2pi)
   1.219 +
   1.220 +lemma sincos_principal_value: "\<exists>y. (-pi < y \<and> y \<le> pi) \<and> (sin(y) = sin(x) \<and> cos(y) = cos(x))"
   1.221 +  apply (rule exI [where x="pi - (2*pi) * frac((pi - x) / (2*pi))"])
   1.222 +  apply (auto simp: field_simps frac_lt_1)
   1.223 +  apply (simp_all add: frac_def divide_simps)
   1.224 +  apply (simp_all add: add_divide_distrib diff_divide_distrib)
   1.225 +  apply (simp_all add: sin_diff cos_diff mult.assoc [symmetric] cos_integer_2pi sin_integer_2pi)
   1.226 +  done
   1.227 +
   1.228 +
   1.229  subsection {* Tangent *}
   1.230  
   1.231  definition tan :: "'a \<Rightarrow> 'a::{real_normed_field,banach}"
   1.232 @@ -3528,6 +3716,15 @@
   1.233    unfolding tan_def sin_double cos_double sin_squared_eq
   1.234    by (simp add: power2_eq_square)
   1.235  
   1.236 +lemma tan_30: "tan (pi / 6) = 1 / sqrt 3"
   1.237 +  unfolding tan_def by (simp add: sin_30 cos_30)
   1.238 +
   1.239 +lemma tan_45: "tan (pi / 4) = 1"
   1.240 +  unfolding tan_def by (simp add: sin_45 cos_45)
   1.241 +
   1.242 +lemma tan_60: "tan (pi / 3) = sqrt 3"
   1.243 +  unfolding tan_def by (simp add: sin_60 cos_60)
   1.244 +
   1.245  lemma DERIV_tan [simp]:
   1.246    fixes x :: "'a::{real_normed_field,banach}"
   1.247    shows "cos x \<noteq> 0 \<Longrightarrow> DERIV tan x :> inverse ((cos x)\<^sup>2)"
   1.248 @@ -3705,9 +3902,48 @@
   1.249  lemma tan_periodic_n[simp]: "tan (x + numeral n * pi) = tan x"
   1.250    using tan_periodic_int[of _ "numeral n" ] unfolding real_numeral .
   1.251  
   1.252 +lemma tan_minus_45: "tan (-(pi/4)) = -1"
   1.253 +  unfolding tan_def by (simp add: sin_45 cos_45)
   1.254 +
   1.255 +lemma tan_diff:
   1.256 +  fixes x :: "'a::{real_normed_field,banach}"
   1.257 +  shows
   1.258 +     "\<lbrakk>cos x \<noteq> 0; cos y \<noteq> 0; cos (x - y) \<noteq> 0\<rbrakk>
   1.259 +      \<Longrightarrow> tan(x - y) = (tan(x) - tan(y))/(1 + tan(x) * tan(y))"
   1.260 +  using tan_add [of x "-y"]
   1.261 +  by simp
   1.262 +
   1.263 +
   1.264 +lemma tan_pos_pi2_le: "0 \<le> x ==> x < pi/2 \<Longrightarrow> 0 \<le> tan x"
   1.265 +  using less_eq_real_def tan_gt_zero by auto
   1.266 +
   1.267 +lemma cos_tan: "abs(x) < pi/2 \<Longrightarrow> cos(x) = 1 / sqrt(1 + tan(x) ^ 2)"
   1.268 +  using cos_gt_zero_pi [of x]
   1.269 +  by (simp add: divide_simps tan_def real_sqrt_divide abs_if split: split_if_asm)
   1.270 +
   1.271 +lemma sin_tan: "abs(x) < pi/2 \<Longrightarrow> sin(x) = tan(x) / sqrt(1 + tan(x) ^ 2)"
   1.272 +  using cos_gt_zero [of "x"] cos_gt_zero [of "-x"]
   1.273 +  by (force simp add: divide_simps tan_def real_sqrt_divide abs_if split: split_if_asm)
   1.274 +
   1.275 +lemma tan_mono_le: "-(pi/2) < x ==> x \<le> y ==> y < pi/2 \<Longrightarrow> tan(x) \<le> tan(y)"
   1.276 +  using less_eq_real_def tan_monotone by auto
   1.277 +
   1.278 +lemma tan_mono_lt_eq: "-(pi/2) < x ==> x < pi/2 ==> -(pi/2) < y ==> y < pi/2
   1.279 +         \<Longrightarrow> (tan(x) < tan(y) \<longleftrightarrow> x < y)"
   1.280 +  using tan_monotone' by blast
   1.281 +
   1.282 +lemma tan_mono_le_eq: "-(pi/2) < x ==> x < pi/2 ==> -(pi/2) < y ==> y < pi/2
   1.283 +         \<Longrightarrow> (tan(x) \<le> tan(y) \<longleftrightarrow> x \<le> y)"
   1.284 +  by (meson tan_mono_le not_le tan_monotone)
   1.285 +
   1.286 +lemma tan_bound_pi2: "abs(x) < pi/4 \<Longrightarrow> abs(tan x) < 1"
   1.287 +  using tan_45 tan_monotone [of x "pi/4"] tan_monotone [of "-x" "pi/4"]
   1.288 +  by (auto simp: abs_if split: split_if_asm)
   1.289 +
   1.290 +lemma tan_cot: "tan(pi/2 - x) = inverse(tan x)"
   1.291 +  by (simp add: tan_def sin_diff cos_diff)
   1.292  
   1.293  subsection {* Inverse Trigonometric Functions *}
   1.294 -text{*STILL DEFINED FOR THE REALS ONLY*}
   1.295  
   1.296  definition arcsin :: "real => real"
   1.297    where "arcsin y = (THE x. -(pi/2) \<le> x & x \<le> pi/2 & sin x = y)"
   1.298 @@ -3820,6 +4056,12 @@
   1.299    apply (rule power_mono, simp, simp)
   1.300    done
   1.301  
   1.302 +lemma arccos_0 [simp]: "arccos 0 = pi/2"
   1.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)
   1.304 +
   1.305 +lemma arccos_1 [simp]: "arccos 1 = 0"
   1.306 +  using arccos_cos by force
   1.307 +
   1.308  lemma arctan [simp]: "- (pi/2) < arctan y  & arctan y < pi/2 & tan (arctan y) = y"
   1.309    unfolding arctan_def by (rule theI' [OF tan_total])
   1.310  
   1.311 @@ -4049,124 +4291,34 @@
   1.312    by (intro tendsto_minus tendsto_arctan_at_top)
   1.313  
   1.314  
   1.315 -subsection {* More Theorems about Sin and Cos *}
   1.316 -
   1.317 -lemma cos_45: "cos (pi / 4) = sqrt 2 / 2"
   1.318 -proof -
   1.319 -  let ?c = "cos (pi / 4)" and ?s = "sin (pi / 4)"
   1.320 -  have nonneg: "0 \<le> ?c"
   1.321 -    by (simp add: cos_ge_zero)
   1.322 -  have "0 = cos (pi / 4 + pi / 4)"
   1.323 -    by simp
   1.324 -  also have "cos (pi / 4 + pi / 4) = ?c\<^sup>2 - ?s\<^sup>2"
   1.325 -    by (simp only: cos_add power2_eq_square)
   1.326 -  also have "\<dots> = 2 * ?c\<^sup>2 - 1"
   1.327 -    by (simp add: sin_squared_eq)
   1.328 -  finally have "?c\<^sup>2 = (sqrt 2 / 2)\<^sup>2"
   1.329 -    by (simp add: power_divide)
   1.330 -  thus ?thesis
   1.331 -    using nonneg by (rule power2_eq_imp_eq) simp
   1.332 -qed
   1.333 -
   1.334 -lemma cos_30: "cos (pi / 6) = sqrt 3/2"
   1.335 -proof -
   1.336 -  let ?c = "cos (pi / 6)" and ?s = "sin (pi / 6)"
   1.337 -  have pos_c: "0 < ?c"
   1.338 -    by (rule cos_gt_zero, simp, simp)
   1.339 -  have "0 = cos (pi / 6 + pi / 6 + pi / 6)"
   1.340 -    by simp
   1.341 -  also have "\<dots> = (?c * ?c - ?s * ?s) * ?c - (?s * ?c + ?c * ?s) * ?s"
   1.342 -    by (simp only: cos_add sin_add)
   1.343 -  also have "\<dots> = ?c * (?c\<^sup>2 - 3 * ?s\<^sup>2)"
   1.344 -    by (simp add: algebra_simps power2_eq_square)
   1.345 -  finally have "?c\<^sup>2 = (sqrt 3/2)\<^sup>2"
   1.346 -    using pos_c by (simp add: sin_squared_eq power_divide)
   1.347 -  thus ?thesis
   1.348 -    using pos_c [THEN order_less_imp_le]
   1.349 -    by (rule power2_eq_imp_eq) simp
   1.350 -qed
   1.351 -
   1.352 -lemma sin_45: "sin (pi / 4) = sqrt 2 / 2"
   1.353 -  by (simp add: sin_cos_eq cos_45)
   1.354 -
   1.355 -lemma sin_60: "sin (pi / 3) = sqrt 3/2"
   1.356 -  by (simp add: sin_cos_eq cos_30)
   1.357 -
   1.358 -lemma cos_60: "cos (pi / 3) = 1 / 2"
   1.359 -  apply (rule power2_eq_imp_eq)
   1.360 -  apply (simp add: cos_squared_eq sin_60 power_divide)
   1.361 -  apply (rule cos_ge_zero, rule order_trans [where y=0], simp_all)
   1.362 -  done
   1.363 -
   1.364 -lemma sin_30: "sin (pi / 6) = 1 / 2"
   1.365 -  by (simp add: sin_cos_eq cos_60)
   1.366 -
   1.367 -lemma tan_30: "tan (pi / 6) = 1 / sqrt 3"
   1.368 -  unfolding tan_def by (simp add: sin_30 cos_30)
   1.369 -
   1.370 -lemma tan_45: "tan (pi / 4) = 1"
   1.371 -  unfolding tan_def by (simp add: sin_45 cos_45)
   1.372 -
   1.373 -lemma tan_60: "tan (pi / 3) = sqrt 3"
   1.374 -  unfolding tan_def by (simp add: sin_60 cos_60)
   1.375 -
   1.376 -lemma sin_cos_npi [simp]: "sin (real (Suc (2 * n)) * pi / 2) = (-1) ^ n"
   1.377 -proof -
   1.378 -  have "sin ((real n + 1/2) * pi) = cos (real n * pi)"
   1.379 -    by (auto simp: algebra_simps sin_add)
   1.380 -  thus ?thesis
   1.381 -    by (simp add: real_of_nat_Suc distrib_right add_divide_distrib
   1.382 -                  mult.commute [of pi])
   1.383 -qed
   1.384 -
   1.385 -lemma cos_2npi [simp]: "cos (2 * real (n::nat) * pi) = 1"
   1.386 -  by (cases "even n") (simp_all add: cos_double mult.assoc)
   1.387 -
   1.388 -lemma cos_3over2_pi [simp]: "cos (3/2*pi) = 0"
   1.389 -  apply (subgoal_tac "cos (pi + pi/2) = 0", simp)
   1.390 -  apply (subst cos_add, simp)
   1.391 -  done
   1.392 -
   1.393 -lemma sin_2npi [simp]: "sin (2 * real (n::nat) * pi) = 0"
   1.394 -  by (auto simp: mult.assoc sin_double)
   1.395 -
   1.396 -lemma sin_3over2_pi [simp]: "sin (3/2*pi) = - 1"
   1.397 -  apply (subgoal_tac "sin (pi + pi/2) = - 1", simp)
   1.398 -  apply (subst sin_add, simp)
   1.399 -  done
   1.400 -
   1.401 -lemma cos_pi_eq_zero [simp]: "cos (pi * real (Suc (2 * m)) / 2) = 0"
   1.402 -by (simp only: cos_add sin_add real_of_nat_Suc distrib_right distrib_left add_divide_distrib, auto)
   1.403 -
   1.404 -lemma DERIV_cos_add [simp]: "DERIV (\<lambda>x. cos (x + k)) xa :> - sin (xa + k)"
   1.405 -  by (auto intro!: derivative_eq_intros)
   1.406 -
   1.407 -lemma sin_zero_norm_cos_one:
   1.408 -  fixes x :: "'a::{real_normed_field,banach}"
   1.409 -  assumes "sin x = 0" shows "norm (cos x) = 1"
   1.410 -  using sin_cos_squared_add [of x, unfolded assms]
   1.411 -  by (simp add: square_norm_one)
   1.412 -
   1.413 -lemma sin_zero_abs_cos_one: "sin x = 0 \<Longrightarrow> \<bar>cos x\<bar> = (1::real)"
   1.414 -  using sin_zero_norm_cos_one by fastforce
   1.415 -
   1.416 -lemma cos_one_sin_zero:
   1.417 -  fixes x :: "'a::{real_normed_field,banach}"
   1.418 -  assumes "cos x = 1" shows "sin x = 0"
   1.419 -  using sin_cos_squared_add [of x, unfolded assms]
   1.420 -  by simp
   1.421 -
   1.422 -
   1.423  subsection{* Prove Totality of the Trigonometric Functions *}
   1.424  
   1.425 -lemma arccos_0 [simp]: "arccos 0 = pi/2"
   1.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)
   1.427 -
   1.428 -lemma arccos_1 [simp]: "arccos 1 = 0"
   1.429 -  using arccos_cos by force
   1.430 +lemma sin_mono_less_eq: "\<lbrakk>-(pi/2) \<le> x; x \<le> pi/2; -(pi/2) \<le> y; y \<le> pi/2\<rbrakk>
   1.431 +         \<Longrightarrow> (sin(x) < sin(y) \<longleftrightarrow> x < y)"
   1.432 +by (metis not_less_iff_gr_or_eq sin_monotone_2pi)
   1.433 +
   1.434 +lemma sin_mono_le_eq: "\<lbrakk>-(pi/2) \<le> x; x \<le> pi/2; -(pi/2) \<le> y; y \<le> pi/2\<rbrakk>
   1.435 +         \<Longrightarrow> (sin(x) \<le> sin(y) \<longleftrightarrow> x \<le> y)"
   1.436 +by (meson leD le_less_linear sin_monotone_2pi sin_monotone_2pi_le)
   1.437 +
   1.438 +lemma sin_inj_pi: "-(pi/2) \<le> x ==> x \<le> pi/2 ==>
   1.439 +         -(pi/2) \<le> y ==> y \<le> pi/2 ==> sin(x) = sin(y) \<Longrightarrow> x = y"
   1.440 +by (metis arcsin_sin)
   1.441 +
   1.442 +lemma cos_mono_lt_eq: "0 \<le> x ==> x \<le> pi ==> 0 \<le> y ==> y \<le> pi
   1.443 +         \<Longrightarrow> (cos(x) < cos(y) \<longleftrightarrow> y < x)"
   1.444 +by (meson cos_monotone_0_pi cos_monotone_0_pi_le leD le_less_linear)
   1.445 +
   1.446 +lemma cos_mono_le_eq: "0 \<le> x ==> x \<le> pi ==> 0 \<le> y ==> y \<le> pi
   1.447 +         \<Longrightarrow> (cos(x) \<le> cos(y) \<longleftrightarrow> y \<le> x)"
   1.448 +  by (metis arccos_cos cos_monotone_0_pi_le eq_iff linear)
   1.449 +
   1.450 +lemma cos_inj_pi: "0 \<le> x ==> x \<le> pi ==> 0 \<le> y ==> y \<le> pi ==> cos(x) = cos(y)
   1.451 +         \<Longrightarrow> x = y"
   1.452 +by (metis arccos_cos)
   1.453  
   1.454  lemma arccos_le_pi2: "\<lbrakk>0 \<le> y; y \<le> 1\<rbrakk> \<Longrightarrow> arccos y \<le> pi/2"
   1.455 -  by (metis (mono_tags) arccos_0 arccos cos_le_one cos_monotone_0_pi'
   1.456 +  by (metis (mono_tags) arccos_0 arccos cos_le_one cos_monotone_0_pi_le
   1.457        cos_pi cos_pi_half pi_half_ge_zero antisym_conv less_eq_neg_nonpos linear minus_minus order.trans order_refl)
   1.458  
   1.459  lemma sincos_total_pi_half: