src/HOL/Transcendental.thy
changeset 59658 0cc388370041
parent 59647 c6f413b660cf
child 59669 de7792ea4090
     1.1 --- a/src/HOL/Transcendental.thy	Mon Mar 09 11:32:32 2015 +0100
     1.2 +++ b/src/HOL/Transcendental.thy	Mon Mar 09 16:28:19 2015 +0000
     1.3 @@ -2347,11 +2347,11 @@
     1.4  definition cos_coeff :: "nat \<Rightarrow> real" where
     1.5    "cos_coeff = (\<lambda>n. if even n then ((- 1) ^ (n div 2)) / real (fact n) else 0)"
     1.6  
     1.7 -definition sin :: "real \<Rightarrow> real"
     1.8 -  where "sin = (\<lambda>x. \<Sum>n. sin_coeff n * x ^ n)"
     1.9 -
    1.10 -definition cos :: "real \<Rightarrow> real"
    1.11 -  where "cos = (\<lambda>x. \<Sum>n. cos_coeff n * x ^ n)"
    1.12 +definition sin :: "'a \<Rightarrow> 'a::{real_normed_algebra_1,banach}"
    1.13 +  where "sin = (\<lambda>x. \<Sum>n. sin_coeff n *\<^sub>R x^n)"
    1.14 +
    1.15 +definition cos :: "'a \<Rightarrow> 'a::{real_normed_algebra_1,banach}"
    1.16 +  where "cos = (\<lambda>x. \<Sum>n. cos_coeff n *\<^sub>R x^n)"
    1.17  
    1.18  lemma sin_coeff_0 [simp]: "sin_coeff 0 = 0"
    1.19    unfolding sin_coeff_def by simp
    1.20 @@ -2367,23 +2367,65 @@
    1.21    unfolding cos_coeff_def sin_coeff_def
    1.22    by (simp del: mult_Suc) (auto elim: oddE)
    1.23  
    1.24 -lemma summable_sin: "summable (\<lambda>n. sin_coeff n * x ^ n)"
    1.25 -  unfolding sin_coeff_def
    1.26 -  apply (rule summable_comparison_test [OF _ summable_exp [where x="\<bar>x\<bar>"]])
    1.27 -  apply (auto simp add: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
    1.28 +lemma summable_norm_sin: 
    1.29 +  fixes x :: "'a::{real_normed_algebra_1,banach}"
    1.30 +  shows "summable (\<lambda>n. norm (sin_coeff n *\<^sub>R x^n))"
    1.31 +  unfolding sin_coeff_def 
    1.32 +  apply (rule summable_comparison_test [OF _ summable_norm_exp [where x=x]])
    1.33 +  apply (auto simp: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
    1.34    done
    1.35  
    1.36 -lemma summable_cos: "summable (\<lambda>n. cos_coeff n * x ^ n)"
    1.37 +lemma summable_norm_cos: 
    1.38 +  fixes x :: "'a::{real_normed_algebra_1,banach}"
    1.39 +  shows "summable (\<lambda>n. norm (cos_coeff n *\<^sub>R x ^ n))"
    1.40    unfolding cos_coeff_def
    1.41 -  apply (rule summable_comparison_test [OF _ summable_exp [where x="\<bar>x\<bar>"]])
    1.42 -  apply (auto simp add: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
    1.43 +  apply (rule summable_comparison_test [OF _ summable_norm_exp [where x=x]])
    1.44 +  apply (auto simp: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
    1.45    done
    1.46  
    1.47 -lemma sin_converges: "(\<lambda>n. sin_coeff n * x ^ n) sums sin(x)"
    1.48 -  unfolding sin_def by (rule summable_sin [THEN summable_sums])
    1.49 -
    1.50 -lemma cos_converges: "(\<lambda>n. cos_coeff n * x ^ n) sums cos(x)"
    1.51 -  unfolding cos_def by (rule summable_cos [THEN summable_sums])
    1.52 +lemma sin_converges: "(\<lambda>n. sin_coeff n *\<^sub>R x^n) sums sin(x)"
    1.53 +unfolding sin_def
    1.54 +  by (metis (full_types) summable_norm_cancel summable_norm_sin summable_sums)
    1.55 +
    1.56 +lemma cos_converges: "(\<lambda>n. cos_coeff n *\<^sub>R x^n) sums cos(x)"
    1.57 +unfolding cos_def
    1.58 +  by (metis (full_types) summable_norm_cancel summable_norm_cos summable_sums)
    1.59 +
    1.60 +lemma sin_of_real:
    1.61 +  fixes x::real
    1.62 +  shows "sin (of_real x) = of_real (sin x)"
    1.63 +proof -
    1.64 +  have "(\<lambda>n. of_real (sin_coeff n *\<^sub>R  x^n)) = (\<lambda>n. sin_coeff n *\<^sub>R  (of_real x)^n)"
    1.65 +  proof
    1.66 +    fix n
    1.67 +    show "of_real (sin_coeff n *\<^sub>R  x ^ n) = sin_coeff n *\<^sub>R of_real x ^ n"
    1.68 +      by (simp add: scaleR_conv_of_real)
    1.69 +  qed
    1.70 +  also have "... sums (sin (of_real x))"
    1.71 +    by (rule sin_converges)
    1.72 +  finally have "(\<lambda>n. of_real (sin_coeff n *\<^sub>R x^n)) sums (sin (of_real x))" .
    1.73 +  then show ?thesis
    1.74 +    using sums_unique2 sums_of_real [OF sin_converges] 
    1.75 +    by blast
    1.76 +qed
    1.77 +
    1.78 +lemma cos_of_real:
    1.79 +  fixes x::real
    1.80 +  shows "cos (of_real x) = of_real (cos x)"
    1.81 +proof -
    1.82 +  have "(\<lambda>n. of_real (cos_coeff n *\<^sub>R  x^n)) = (\<lambda>n. cos_coeff n *\<^sub>R  (of_real x)^n)"
    1.83 +  proof
    1.84 +    fix n
    1.85 +    show "of_real (cos_coeff n *\<^sub>R  x ^ n) = cos_coeff n *\<^sub>R of_real x ^ n"
    1.86 +      by (simp add: scaleR_conv_of_real)
    1.87 +  qed
    1.88 +  also have "... sums (cos (of_real x))"
    1.89 +    by (rule cos_converges)
    1.90 +  finally have "(\<lambda>n. of_real (cos_coeff n *\<^sub>R x^n)) sums (cos (of_real x))" .
    1.91 +  then show ?thesis
    1.92 +    using sums_unique2 sums_of_real [OF cos_converges]  
    1.93 +    by blast
    1.94 +qed
    1.95  
    1.96  lemma diffs_sin_coeff: "diffs sin_coeff = cos_coeff"
    1.97    by (simp add: diffs_def sin_coeff_Suc real_of_nat_def del: of_nat_Suc)
    1.98 @@ -2393,106 +2435,339 @@
    1.99  
   1.100  text{*Now at last we can get the derivatives of exp, sin and cos*}
   1.101  
   1.102 -lemma DERIV_sin [simp]: "DERIV sin x :> cos(x)"
   1.103 -  unfolding sin_def cos_def
   1.104 -  apply (rule DERIV_cong, rule termdiffs [where K="1 + \<bar>x\<bar>"])
   1.105 -  apply (simp_all add: diffs_sin_coeff diffs_cos_coeff
   1.106 -    summable_minus summable_sin summable_cos)
   1.107 +lemma DERIV_sin [simp]:
   1.108 +  fixes x :: "'a::{real_normed_field,banach}"
   1.109 +  shows "DERIV sin x :> cos(x)"
   1.110 +  unfolding sin_def cos_def scaleR_conv_of_real
   1.111 +  apply (rule DERIV_cong)
   1.112 +  apply (rule termdiffs [where K="of_real (norm x) + 1 :: 'a"])
   1.113 +  apply (simp_all add: norm_less_p1 diffs_of_real diffs_sin_coeff diffs_cos_coeff 
   1.114 +              summable_minus_iff scaleR_conv_of_real [symmetric]
   1.115 +              summable_norm_sin [THEN summable_norm_cancel]
   1.116 +              summable_norm_cos [THEN summable_norm_cancel])
   1.117    done
   1.118 -
   1.119 +  
   1.120  declare DERIV_sin[THEN DERIV_chain2, derivative_intros]
   1.121  
   1.122 -lemma DERIV_cos [simp]: "DERIV cos x :> -sin(x)"
   1.123 -  unfolding cos_def sin_def
   1.124 -  apply (rule DERIV_cong, rule termdiffs [where K="1 + \<bar>x\<bar>"])
   1.125 -  apply (simp_all add: diffs_sin_coeff diffs_cos_coeff diffs_minus
   1.126 -    summable_minus summable_sin summable_cos suminf_minus)
   1.127 +lemma DERIV_cos [simp]: 
   1.128 +  fixes x :: "'a::{real_normed_field,banach}"
   1.129 +  shows "DERIV cos x :> -sin(x)"
   1.130 +  unfolding sin_def cos_def scaleR_conv_of_real
   1.131 +  apply (rule DERIV_cong)
   1.132 +  apply (rule termdiffs [where K="of_real (norm x) + 1 :: 'a"])
   1.133 +  apply (simp_all add: norm_less_p1 diffs_of_real diffs_minus suminf_minus 
   1.134 +              diffs_sin_coeff diffs_cos_coeff 
   1.135 +              summable_minus_iff scaleR_conv_of_real [symmetric]
   1.136 +              summable_norm_sin [THEN summable_norm_cancel]
   1.137 +              summable_norm_cos [THEN summable_norm_cancel])
   1.138    done
   1.139  
   1.140  declare DERIV_cos[THEN DERIV_chain2, derivative_intros]
   1.141  
   1.142 -lemma isCont_sin: "isCont sin x"
   1.143 +lemma isCont_sin:
   1.144 +  fixes x :: "'a::{real_normed_field,banach}"
   1.145 +  shows "isCont sin x"
   1.146    by (rule DERIV_sin [THEN DERIV_isCont])
   1.147  
   1.148 -lemma isCont_cos: "isCont cos x"
   1.149 +lemma isCont_cos: 
   1.150 +  fixes x :: "'a::{real_normed_field,banach}"
   1.151 +  shows "isCont cos x"
   1.152    by (rule DERIV_cos [THEN DERIV_isCont])
   1.153  
   1.154 -lemma isCont_sin' [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. sin (f x)) a"
   1.155 +lemma isCont_sin' [simp]:
   1.156 +  fixes f:: "_ \<Rightarrow> 'a::{real_normed_field,banach}"
   1.157 +  shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. sin (f x)) a"
   1.158    by (rule isCont_o2 [OF _ isCont_sin])
   1.159  
   1.160 -lemma isCont_cos' [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. cos (f x)) a"
   1.161 +(*FIXME A CONTEXT FOR F WOULD BE BETTER*)
   1.162 +
   1.163 +lemma isCont_cos' [simp]: 
   1.164 +  fixes f:: "_ \<Rightarrow> 'a::{real_normed_field,banach}"
   1.165 +  shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. cos (f x)) a"
   1.166    by (rule isCont_o2 [OF _ isCont_cos])
   1.167  
   1.168  lemma tendsto_sin [tendsto_intros]:
   1.169 -  "(f ---> a) F \<Longrightarrow> ((\<lambda>x. sin (f x)) ---> sin a) F"
   1.170 +  fixes f:: "_ \<Rightarrow> 'a::{real_normed_field,banach}"
   1.171 +  shows "(f ---> a) F \<Longrightarrow> ((\<lambda>x. sin (f x)) ---> sin a) F"
   1.172    by (rule isCont_tendsto_compose [OF isCont_sin])
   1.173  
   1.174  lemma tendsto_cos [tendsto_intros]:
   1.175 -  "(f ---> a) F \<Longrightarrow> ((\<lambda>x. cos (f x)) ---> cos a) F"
   1.176 +  fixes f:: "_ \<Rightarrow> 'a::{real_normed_field,banach}"
   1.177 +  shows "(f ---> a) F \<Longrightarrow> ((\<lambda>x. cos (f x)) ---> cos a) F"
   1.178    by (rule isCont_tendsto_compose [OF isCont_cos])
   1.179  
   1.180  lemma continuous_sin [continuous_intros]:
   1.181 -  "continuous F f \<Longrightarrow> continuous F (\<lambda>x. sin (f x))"
   1.182 +  fixes f:: "_ \<Rightarrow> 'a::{real_normed_field,banach}"
   1.183 +  shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. sin (f x))"
   1.184    unfolding continuous_def by (rule tendsto_sin)
   1.185  
   1.186  lemma continuous_on_sin [continuous_intros]:
   1.187 -  "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. sin (f x))"
   1.188 +  fixes f:: "_ \<Rightarrow> 'a::{real_normed_field,banach}"
   1.189 +  shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. sin (f x))"
   1.190    unfolding continuous_on_def by (auto intro: tendsto_sin)
   1.191  
   1.192 +lemma continuous_within_sin:
   1.193 +  fixes z :: "'a::{real_normed_field,banach}"
   1.194 +  shows "continuous (at z within s) sin"
   1.195 +  by (simp add: continuous_within tendsto_sin)
   1.196 +
   1.197  lemma continuous_cos [continuous_intros]:
   1.198 -  "continuous F f \<Longrightarrow> continuous F (\<lambda>x. cos (f x))"
   1.199 +  fixes f:: "_ \<Rightarrow> 'a::{real_normed_field,banach}"
   1.200 +  shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. cos (f x))"
   1.201    unfolding continuous_def by (rule tendsto_cos)
   1.202  
   1.203  lemma continuous_on_cos [continuous_intros]:
   1.204 -  "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. cos (f x))"
   1.205 +  fixes f:: "_ \<Rightarrow> 'a::{real_normed_field,banach}"
   1.206 +  shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. cos (f x))"
   1.207    unfolding continuous_on_def by (auto intro: tendsto_cos)
   1.208  
   1.209 +lemma continuous_within_cos:
   1.210 +  fixes z :: "'a::{real_normed_field,banach}"
   1.211 +  shows "continuous (at z within s) cos"
   1.212 +  by (simp add: continuous_within tendsto_cos)
   1.213 +
   1.214  subsection {* Properties of Sine and Cosine *}
   1.215  
   1.216  lemma sin_zero [simp]: "sin 0 = 0"
   1.217 -  unfolding sin_def sin_coeff_def by (simp add: powser_zero)
   1.218 +  unfolding sin_def sin_coeff_def by (simp add: scaleR_conv_of_real powser_zero)
   1.219  
   1.220  lemma cos_zero [simp]: "cos 0 = 1"
   1.221 -  unfolding cos_def cos_coeff_def by (simp add: powser_zero)
   1.222 -
   1.223 -lemma sin_cos_squared_add [simp]: "(sin x)\<^sup>2 + (cos x)\<^sup>2 = 1"
   1.224 +  unfolding cos_def cos_coeff_def by (simp add: scaleR_conv_of_real powser_zero)
   1.225 +
   1.226 +lemma DERIV_fun_sin:
   1.227 +     "DERIV g x :> m \<Longrightarrow> DERIV (\<lambda>x. sin(g x)) x :> cos(g x) * m"
   1.228 +  by (auto intro!: derivative_intros)
   1.229 +
   1.230 +lemma DERIV_fun_cos:
   1.231 +     "DERIV g x :> m \<Longrightarrow> DERIV (\<lambda>x. cos(g x)) x :> -sin(g x) * m"
   1.232 +  by (auto intro!: derivative_eq_intros simp: real_of_nat_def)
   1.233 +
   1.234 +subsection {*Deriving the Addition Formulas*}
   1.235 +
   1.236 +text{*The the product of two cosine series*}
   1.237 +lemma cos_x_cos_y: 
   1.238 +  fixes x :: "'a::{real_normed_field,banach}"
   1.239 +  shows "(\<lambda>p. \<Sum>n\<le>p. 
   1.240 +          if even p \<and> even n 
   1.241 +          then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0) 
   1.242 +         sums (cos x * cos y)"
   1.243 +proof -
   1.244 +  { fix n p::nat
   1.245 +    assume "n\<le>p"
   1.246 +    then have *: "even n \<Longrightarrow> even p \<Longrightarrow> (-1) ^ (n div 2) * (-1) ^ ((p - n) div 2) = (-1 :: real) ^ (p div 2)"
   1.247 +      by (metis div_add power_add le_add_diff_inverse odd_add)
   1.248 +    have "(cos_coeff n * cos_coeff (p - n)) *\<^sub>R (x^n * y^(p-n)) = 
   1.249 +          (if even p \<and> even n then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)"
   1.250 +    using `n\<le>p`
   1.251 +      by (auto simp: * algebra_simps cos_coeff_def binomial_fact real_of_nat_def)
   1.252 +  } 
   1.253 +  then have "(\<lambda>p. \<Sum>n\<le>p. if even p \<and> even n 
   1.254 +                  then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0) =
   1.255 +             (\<lambda>p. \<Sum>n\<le>p. (cos_coeff n * cos_coeff (p - n)) *\<^sub>R (x^n * y^(p-n)))"
   1.256 +    by simp
   1.257 +  also have "... = (\<lambda>p. \<Sum>n\<le>p. (cos_coeff n *\<^sub>R x^n) * (cos_coeff (p - n) *\<^sub>R y^(p-n)))"
   1.258 +    by (simp add: algebra_simps)
   1.259 +  also have "... sums (cos x * cos y)"
   1.260 +    using summable_norm_cos
   1.261 +    by (auto simp: cos_def scaleR_conv_of_real intro!: Cauchy_product_sums)
   1.262 +  finally show ?thesis .
   1.263 +qed
   1.264 +
   1.265 +text{*The product of two sine series*}
   1.266 +lemma sin_x_sin_y: 
   1.267 +  fixes x :: "'a::{real_normed_field,banach}"
   1.268 +  shows "(\<lambda>p. \<Sum>n\<le>p. 
   1.269 +          if even p \<and> odd n 
   1.270 +               then - ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0) 
   1.271 +         sums (sin x * sin y)"
   1.272 +proof -
   1.273 +  { fix n p::nat
   1.274 +    assume "n\<le>p"
   1.275 +    { assume np: "odd n" "even p"
   1.276 +        with `n\<le>p` have "n - Suc 0 + (p - Suc n) = p - Suc (Suc 0)" "Suc (Suc 0) \<le> p"
   1.277 +        by arith+
   1.278 +      moreover have "(p - Suc (Suc 0)) div 2 = p div 2 - Suc 0"
   1.279 +        by simp
   1.280 +      ultimately have *: "(-1) ^ ((n - Suc 0) div 2) * (-1) ^ ((p - Suc n) div 2) = - ((-1 :: real) ^ (p div 2))"
   1.281 +        using np `n\<le>p`
   1.282 +        apply (simp add: power_add [symmetric] div_add [symmetric] del: div_add)
   1.283 +        apply (metis (no_types) One_nat_def Suc_1 le_div_geq minus_minus mult.left_neutral mult_minus_left power.simps(2) zero_less_Suc)
   1.284 +        done
   1.285 +    } then
   1.286 +    have "(sin_coeff n * sin_coeff (p - n)) *\<^sub>R (x^n * y^(p-n)) = 
   1.287 +          (if even p \<and> odd n 
   1.288 +          then -((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)"
   1.289 +    using `n\<le>p`
   1.290 +      by (auto simp:  algebra_simps sin_coeff_def binomial_fact real_of_nat_def)
   1.291 +  } 
   1.292 +  then have "(\<lambda>p. \<Sum>n\<le>p. if even p \<and> odd n 
   1.293 +               then - ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0) =
   1.294 +             (\<lambda>p. \<Sum>n\<le>p. (sin_coeff n * sin_coeff (p - n)) *\<^sub>R (x^n * y^(p-n)))"
   1.295 +    by simp
   1.296 +  also have "... = (\<lambda>p. \<Sum>n\<le>p. (sin_coeff n *\<^sub>R x^n) * (sin_coeff (p - n) *\<^sub>R y^(p-n)))"
   1.297 +    by (simp add: algebra_simps)
   1.298 +  also have "... sums (sin x * sin y)"
   1.299 +    using summable_norm_sin
   1.300 +    by (auto simp: sin_def scaleR_conv_of_real intro!: Cauchy_product_sums)
   1.301 +  finally show ?thesis .
   1.302 +qed
   1.303 +
   1.304 +lemma sums_cos_x_plus_y: 
   1.305 +  fixes x :: "'a::{real_normed_field,banach}"
   1.306 +  shows
   1.307 +  "(\<lambda>p. \<Sum>n\<le>p. if even p 
   1.308 +               then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) 
   1.309 +               else 0) 
   1.310 +        sums cos (x + y)"
   1.311  proof -
   1.312 -  have "\<forall>x. DERIV (\<lambda>x. (sin x)\<^sup>2 + (cos x)\<^sup>2) x :> 0"
   1.313 -    by (auto intro!: derivative_eq_intros)
   1.314 -  hence "(sin x)\<^sup>2 + (cos x)\<^sup>2 = (sin 0)\<^sup>2 + (cos 0)\<^sup>2"
   1.315 -    by (rule DERIV_isconst_all)
   1.316 -  thus "(sin x)\<^sup>2 + (cos x)\<^sup>2 = 1" by simp
   1.317 +  { fix p::nat
   1.318 +    have "(\<Sum>n\<le>p. if even p
   1.319 +                  then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n)
   1.320 +                  else 0) = 
   1.321 +          (if even p
   1.322 +                  then \<Sum>n\<le>p. ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n)
   1.323 +                  else 0)"
   1.324 +      by simp
   1.325 +    also have "... = (if even p
   1.326 +                  then of_real ((-1) ^ (p div 2) / of_nat (fact p)) * (\<Sum>n\<le>p. (p choose n) *\<^sub>R (x^n) * y^(p-n))
   1.327 +                  else 0)"
   1.328 +      by (auto simp: setsum_right_distrib field_simps scaleR_conv_of_real nonzero_of_real_divide)
   1.329 +    also have "... = cos_coeff p *\<^sub>R ((x + y) ^ p)"
   1.330 +      by (simp add: cos_coeff_def binomial_ring [of x y]  scaleR_conv_of_real real_of_nat_def atLeast0AtMost)
   1.331 +    finally have "(\<Sum>n\<le>p. if even p
   1.332 +                  then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n)
   1.333 +                  else 0) = cos_coeff p *\<^sub>R ((x + y) ^ p)" .
   1.334 +  }  
   1.335 +  then have "(\<lambda>p. \<Sum>n\<le>p. 
   1.336 +               if even p 
   1.337 +               then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) 
   1.338 +               else 0) 
   1.339 +        = (\<lambda>p. cos_coeff p *\<^sub>R ((x+y)^p))"
   1.340 +        by simp
   1.341 +   also have "... sums cos (x + y)"
   1.342 +    by (rule cos_converges)
   1.343 +   finally show ?thesis .
   1.344 +qed
   1.345 +
   1.346 +theorem cos_add: 
   1.347 +  fixes x :: "'a::{real_normed_field,banach}"
   1.348 +  shows "cos (x + y) = cos x * cos y - sin x * sin y"
   1.349 +proof -
   1.350 +  { fix n p::nat
   1.351 +    assume "n\<le>p"
   1.352 +    then have "(if even p \<and> even n 
   1.353 +               then ((- 1) ^ (p div 2) * int (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0) -
   1.354 +          (if even p \<and> odd n 
   1.355 +               then - ((- 1) ^ (p div 2) * int (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)
   1.356 +          = (if even p 
   1.357 +               then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)"
   1.358 +      by simp
   1.359 +  }   
   1.360 +  then have "(\<lambda>p. \<Sum>n\<le>p. (if even p 
   1.361 +               then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)) 
   1.362 +        sums (cos x * cos y - sin x * sin y)"
   1.363 +    using sums_diff [OF cos_x_cos_y [of x y] sin_x_sin_y [of x y]]
   1.364 +    by (simp add: setsum_subtractf [symmetric])
   1.365 +  then show ?thesis
   1.366 +    by (blast intro: sums_cos_x_plus_y sums_unique2)
   1.367  qed
   1.368  
   1.369 -lemma sin_cos_squared_add2 [simp]: "(cos x)\<^sup>2 + (sin x)\<^sup>2 = 1"
   1.370 +lemma sin_minus_converges: "(\<lambda>n. - (sin_coeff n *\<^sub>R (-x)^n)) sums sin(x)"
   1.371 +proof -
   1.372 +  have [simp]: "\<And>n. - (sin_coeff n *\<^sub>R (-x)^n) = (sin_coeff n *\<^sub>R x^n)"
   1.373 +    by (auto simp: sin_coeff_def elim!: oddE)
   1.374 +  show ?thesis
   1.375 +    by (simp add: sin_def summable_norm_sin [THEN summable_norm_cancel, THEN summable_sums])
   1.376 +qed
   1.377 +
   1.378 +lemma sin_minus [simp]:
   1.379 +  fixes x :: "'a::{real_normed_algebra_1,banach}"
   1.380 +  shows "sin (-x) = -sin(x)"
   1.381 +using sin_minus_converges [of x] 
   1.382 +by (auto simp: sin_def summable_norm_sin [THEN summable_norm_cancel] suminf_minus sums_iff equation_minus_iff)
   1.383 +
   1.384 +lemma cos_minus_converges: "(\<lambda>n. (cos_coeff n *\<^sub>R (-x)^n)) sums cos(x)"
   1.385 +proof -
   1.386 +  have [simp]: "\<And>n. (cos_coeff n *\<^sub>R (-x)^n) = (cos_coeff n *\<^sub>R x^n)"
   1.387 +    by (auto simp: Transcendental.cos_coeff_def elim!: evenE)
   1.388 +  show ?thesis
   1.389 +    by (simp add: cos_def summable_norm_cos [THEN summable_norm_cancel, THEN summable_sums])
   1.390 +qed
   1.391 +
   1.392 +lemma cos_minus [simp]:
   1.393 +  fixes x :: "'a::{real_normed_algebra_1,banach}"
   1.394 +  shows "cos (-x) = cos(x)"
   1.395 +using cos_minus_converges [of x]
   1.396 +by (simp add: cos_def summable_norm_cos [THEN summable_norm_cancel] 
   1.397 +              suminf_minus sums_iff equation_minus_iff)
   1.398 +
   1.399 +    
   1.400 +lemma sin_cos_squared_add [simp]: 
   1.401 +  fixes x :: "'a::{real_normed_field,banach}"
   1.402 +  shows "(sin x)\<^sup>2 + (cos x)\<^sup>2 = 1"
   1.403 +using cos_add [of x "-x"]
   1.404 +by (simp add: power2_eq_square algebra_simps)
   1.405 +
   1.406 +lemma sin_cos_squared_add2 [simp]:  
   1.407 +  fixes x :: "'a::{real_normed_field,banach}"
   1.408 +  shows "(cos x)\<^sup>2 + (sin x)\<^sup>2 = 1"
   1.409    by (subst add.commute, rule sin_cos_squared_add)
   1.410  
   1.411 -lemma sin_cos_squared_add3 [simp]: "cos x * cos x + sin x * sin x = 1"
   1.412 +lemma sin_cos_squared_add3 [simp]:  
   1.413 +  fixes x :: "'a::{real_normed_field,banach}"
   1.414 +  shows "cos x * cos x + sin x * sin x = 1"
   1.415    using sin_cos_squared_add2 [unfolded power2_eq_square] .
   1.416  
   1.417 -lemma sin_squared_eq: "(sin x)\<^sup>2 = 1 - (cos x)\<^sup>2"
   1.418 +lemma sin_squared_eq:  
   1.419 +  fixes x :: "'a::{real_normed_field,banach}"
   1.420 +  shows "(sin x)\<^sup>2 = 1 - (cos x)\<^sup>2"
   1.421    unfolding eq_diff_eq by (rule sin_cos_squared_add)
   1.422  
   1.423 -lemma cos_squared_eq: "(cos x)\<^sup>2 = 1 - (sin x)\<^sup>2"
   1.424 +lemma cos_squared_eq:  
   1.425 +  fixes x :: "'a::{real_normed_field,banach}"
   1.426 +  shows "(cos x)\<^sup>2 = 1 - (sin x)\<^sup>2"
   1.427    unfolding eq_diff_eq by (rule sin_cos_squared_add2)
   1.428  
   1.429 -lemma abs_sin_le_one [simp]: "\<bar>sin x\<bar> \<le> 1"
   1.430 +lemma abs_sin_le_one [simp]:  
   1.431 +  fixes x :: real
   1.432 +  shows "\<bar>sin x\<bar> \<le> 1"
   1.433    by (rule power2_le_imp_le, simp_all add: sin_squared_eq)
   1.434  
   1.435 -lemma sin_ge_minus_one [simp]: "-1 \<le> sin x"
   1.436 +lemma sin_ge_minus_one [simp]: 
   1.437 +  fixes x :: real
   1.438 +  shows "-1 \<le> sin x"
   1.439 +  using abs_sin_le_one [of x] unfolding abs_le_iff by simp
   1.440 +
   1.441 +lemma sin_le_one [simp]: 
   1.442 +  fixes x :: real
   1.443 +  shows "sin x \<le> 1"
   1.444    using abs_sin_le_one [of x] unfolding abs_le_iff by simp
   1.445  
   1.446 -lemma sin_le_one [simp]: "sin x \<le> 1"
   1.447 -  using abs_sin_le_one [of x] unfolding abs_le_iff by simp
   1.448 -
   1.449 -lemma abs_cos_le_one [simp]: "\<bar>cos x\<bar> \<le> 1"
   1.450 +lemma abs_cos_le_one [simp]: 
   1.451 +  fixes x :: real
   1.452 +  shows "\<bar>cos x\<bar> \<le> 1"
   1.453    by (rule power2_le_imp_le, simp_all add: cos_squared_eq)
   1.454  
   1.455 -lemma cos_ge_minus_one [simp]: "-1 \<le> cos x"
   1.456 +lemma cos_ge_minus_one [simp]: 
   1.457 +  fixes x :: real
   1.458 +  shows "-1 \<le> cos x"
   1.459 +  using abs_cos_le_one [of x] unfolding abs_le_iff by simp
   1.460 +
   1.461 +lemma cos_le_one [simp]: 
   1.462 +  fixes x :: real
   1.463 +  shows "cos x \<le> 1"
   1.464    using abs_cos_le_one [of x] unfolding abs_le_iff by simp
   1.465  
   1.466 -lemma cos_le_one [simp]: "cos x \<le> 1"
   1.467 -  using abs_cos_le_one [of x] unfolding abs_le_iff by simp
   1.468 +lemma cos_diff: 
   1.469 +  fixes x :: "'a::{real_normed_field,banach}"
   1.470 +  shows "cos (x - y) = cos x * cos y + sin x * sin y"
   1.471 +  using cos_add [of x "- y"] by simp
   1.472 +
   1.473 +lemma cos_double: 
   1.474 +  fixes x :: "'a::{real_normed_field,banach}"
   1.475 +  shows "cos(2*x) = (cos x)\<^sup>2 - (sin x)\<^sup>2"
   1.476 +  using cos_add [where x=x and y=x]
   1.477 +  by (simp add: power2_eq_square)
   1.478  
   1.479  lemma DERIV_fun_pow: "DERIV g x :> m ==>
   1.480        DERIV (\<lambda>x. (g x) ^ n) x :> real n * (g x) ^ (n - 1) * m"
   1.481 @@ -2502,93 +2777,6 @@
   1.482       "DERIV g x :> m ==> DERIV (\<lambda>x. exp(g x)) x :> exp(g x) * m"
   1.483    by (auto intro!: derivative_intros)
   1.484  
   1.485 -lemma DERIV_fun_sin:
   1.486 -     "DERIV g x :> m ==> DERIV (\<lambda>x. sin(g x)) x :> cos(g x) * m"
   1.487 -  by (auto intro!: derivative_intros)
   1.488 -
   1.489 -lemma DERIV_fun_cos:
   1.490 -     "DERIV g x :> m ==> DERIV (\<lambda>x. cos(g x)) x :> -sin(g x) * m"
   1.491 -  by (auto intro!: derivative_eq_intros simp: real_of_nat_def)
   1.492 -
   1.493 -lemma sin_cos_add_lemma:
   1.494 -  "(sin (x + y) - (sin x * cos y + cos x * sin y))\<^sup>2 +
   1.495 -    (cos (x + y) - (cos x * cos y - sin x * sin y))\<^sup>2 = 0"
   1.496 -  (is "?f x = 0")
   1.497 -proof -
   1.498 -  have "\<forall>x. DERIV (\<lambda>x. ?f x) x :> 0"
   1.499 -    by (auto intro!: derivative_eq_intros simp add: algebra_simps)
   1.500 -  hence "?f x = ?f 0"
   1.501 -    by (rule DERIV_isconst_all)
   1.502 -  thus ?thesis by simp
   1.503 -qed
   1.504 -
   1.505 -lemma sin_add: "sin (x + y) = sin x * cos y + cos x * sin y"
   1.506 -  using sin_cos_add_lemma unfolding realpow_two_sum_zero_iff by simp
   1.507 -
   1.508 -lemma cos_add: "cos (x + y) = cos x * cos y - sin x * sin y"
   1.509 -  using sin_cos_add_lemma unfolding realpow_two_sum_zero_iff by simp
   1.510 -
   1.511 -lemma sin_cos_minus_lemma:
   1.512 -  "(sin(-x) + sin(x))\<^sup>2 + (cos(-x) - cos(x))\<^sup>2 = 0" (is "?f x = 0")
   1.513 -proof -
   1.514 -  have "\<forall>x. DERIV (\<lambda>x. ?f x) x :> 0"
   1.515 -    by (auto intro!: derivative_eq_intros simp add: algebra_simps)
   1.516 -  hence "?f x = ?f 0"
   1.517 -    by (rule DERIV_isconst_all)
   1.518 -  thus ?thesis by simp
   1.519 -qed
   1.520 -
   1.521 -lemma sin_minus [simp]: "sin (-x) = -sin(x)"
   1.522 -  using sin_cos_minus_lemma [where x=x] by simp
   1.523 -
   1.524 -lemma cos_minus [simp]: "cos (-x) = cos(x)"
   1.525 -  using sin_cos_minus_lemma [where x=x] by simp
   1.526 -
   1.527 -lemma sin_diff: "sin (x - y) = sin x * cos y - cos x * sin y"
   1.528 -  using sin_add [of x "- y"] by simp
   1.529 -
   1.530 -lemma sin_diff2: "sin (x - y) = cos y * sin x - sin y * cos x"
   1.531 -  by (simp add: sin_diff mult.commute)
   1.532 -
   1.533 -lemma cos_diff: "cos (x - y) = cos x * cos y + sin x * sin y"
   1.534 -  using cos_add [of x "- y"] by simp
   1.535 -
   1.536 -lemma cos_diff2: "cos (x - y) = cos y * cos x + sin y * sin x"
   1.537 -  by (simp add: cos_diff mult.commute)
   1.538 -
   1.539 -lemma sin_double [simp]: "sin(2 * x) = 2* sin x * cos x"
   1.540 -  using sin_add [where x=x and y=x] by simp
   1.541 -
   1.542 -lemma cos_double: "cos(2* x) = ((cos x)\<^sup>2) - ((sin x)\<^sup>2)"
   1.543 -  using cos_add [where x=x and y=x]
   1.544 -  by (simp add: power2_eq_square)
   1.545 -
   1.546 -lemma sin_x_le_x: assumes x: "x \<ge> 0" shows "sin x \<le> x"
   1.547 -proof -
   1.548 -  let ?f = "\<lambda>x. x - sin x"
   1.549 -  from x have "?f x \<ge> ?f 0"
   1.550 -    apply (rule DERIV_nonneg_imp_nondecreasing)
   1.551 -    apply (intro allI impI exI[of _ "1 - cos x" for x])
   1.552 -    apply (auto intro!: derivative_eq_intros simp: field_simps)
   1.553 -    done
   1.554 -  thus "sin x \<le> x" by simp
   1.555 -qed
   1.556 -
   1.557 -lemma sin_x_ge_neg_x: assumes x: "x \<ge> 0" shows "sin x \<ge> - x"
   1.558 -proof -
   1.559 -  let ?f = "\<lambda>x. x + sin x"
   1.560 -  from x have "?f x \<ge> ?f 0"
   1.561 -    apply (rule DERIV_nonneg_imp_nondecreasing)
   1.562 -    apply (intro allI impI exI[of _ "1 + cos x" for x])
   1.563 -    apply (auto intro!: derivative_eq_intros simp: field_simps real_0_le_add_iff)
   1.564 -    done
   1.565 -  thus "sin x \<ge> -x" by simp
   1.566 -qed
   1.567 -
   1.568 -lemma abs_sin_x_le_abs_x: "\<bar>sin x\<bar> \<le> \<bar>x\<bar>"
   1.569 -  using sin_x_ge_neg_x [of x] sin_x_le_x [of x] sin_x_ge_neg_x [of "-x"] sin_x_le_x [of "-x"]
   1.570 -  by (auto simp: abs_real_def)
   1.571 -
   1.572  subsection {* The Constant Pi *}
   1.573  
   1.574  definition pi :: real
   1.575 @@ -2598,14 +2786,18 @@
   1.576     hence define pi.*}
   1.577  
   1.578  lemma sin_paired:
   1.579 -  "(\<lambda>n. (- 1) ^ n /(real (fact (2 * n + 1))) * x ^ (2 * n + 1)) sums  sin x"
   1.580 +  fixes x :: real 
   1.581 +  shows "(\<lambda>n. (- 1) ^ n /(real (fact (2 * n + 1))) * x ^ (2 * n + 1)) sums  sin x"
   1.582  proof -
   1.583 -  have "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2. sin_coeff k * x ^ k) sums sin x"
   1.584 -    by (rule sin_converges [THEN sums_group], simp)
   1.585 +  have "(\<lambda>n. \<Sum>k = n*2..<n * 2 + 2. sin_coeff k * x ^ k) sums sin x"
   1.586 +    apply (rule sums_group)
   1.587 +    using sin_converges [of x, unfolded scaleR_conv_of_real]
   1.588 +    by auto
   1.589    thus ?thesis unfolding One_nat_def sin_coeff_def by (simp add: ac_simps)
   1.590  qed
   1.591  
   1.592 -lemma sin_gt_zero:
   1.593 +lemma sin_gt_zero_02:
   1.594 +  fixes x :: real 
   1.595    assumes "0 < x" and "x < 2"
   1.596    shows "0 < sin x"
   1.597  proof -
   1.598 @@ -2631,39 +2823,42 @@
   1.599      by (rule suminf_pos)
   1.600  qed
   1.601  
   1.602 -lemma cos_double_less_one: "0 < x \<Longrightarrow> x < 2 \<Longrightarrow> cos (2 * x) < 1"
   1.603 -  using sin_gt_zero [where x = x] by (auto simp add: cos_squared_eq cos_double)
   1.604 -
   1.605 -lemma cos_paired: "(\<lambda>n. (- 1) ^ n /(real (fact (2 * n))) * x ^ (2 * n)) sums cos x"
   1.606 +lemma cos_double_less_one:
   1.607 +  fixes x :: real 
   1.608 +  shows "0 < x \<Longrightarrow> x < 2 \<Longrightarrow> cos (2 * x) < 1"
   1.609 +  using sin_gt_zero_02 [where x = x] by (auto simp: cos_squared_eq cos_double)
   1.610 +
   1.611 +lemma cos_paired:
   1.612 +  fixes x :: real 
   1.613 +  shows "(\<lambda>n. (- 1) ^ n /(real (fact (2 * n))) * x ^ (2 * n)) sums cos x"
   1.614  proof -
   1.615    have "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2. cos_coeff k * x ^ k) sums cos x"
   1.616 -    by (rule cos_converges [THEN sums_group], simp)
   1.617 +    apply (rule sums_group)
   1.618 +    using cos_converges [of x, unfolded scaleR_conv_of_real]
   1.619 +    by auto
   1.620    thus ?thesis unfolding cos_coeff_def by (simp add: ac_simps)
   1.621  qed
   1.622  
   1.623  lemmas realpow_num_eq_if = power_eq_if
   1.624  
   1.625 -lemma sumr_pos_lt_pair:
   1.626 +lemma sumr_pos_lt_pair:  (*FIXME A MESS, BUT THE REAL MESS IS THE NEXT THEOREM*)
   1.627    fixes f :: "nat \<Rightarrow> real"
   1.628    shows "\<lbrakk>summable f;
   1.629          \<And>d. 0 < f (k + (Suc(Suc 0) * d)) + f (k + ((Suc(Suc 0) * d) + 1))\<rbrakk>
   1.630        \<Longrightarrow> setsum f {..<k} < suminf f"
   1.631  unfolding One_nat_def
   1.632 -apply (subst suminf_split_initial_segment [where k="k"])
   1.633 -apply assumption
   1.634 -apply simp
   1.635 -apply (drule_tac k="k" in summable_ignore_initial_segment)
   1.636 +apply (subst suminf_split_initial_segment [where k=k], assumption, simp)
   1.637 +apply (drule_tac k=k in summable_ignore_initial_segment)
   1.638  apply (drule_tac k="Suc (Suc 0)" in sums_group [OF summable_sums], simp)
   1.639  apply simp
   1.640  apply (frule sums_unique)
   1.641 -apply (drule sums_summable)
   1.642 -apply simp
   1.643 +apply (drule sums_summable, simp)
   1.644  apply (erule suminf_pos)
   1.645  apply (simp add: ac_simps)
   1.646  done
   1.647  
   1.648  lemma cos_two_less_zero [simp]:
   1.649 -  "cos 2 < 0"
   1.650 +  "cos 2 < (0::real)"
   1.651  proof -
   1.652    note fact_Suc [simp del]
   1.653    from cos_paired
   1.654 @@ -2699,30 +2894,30 @@
   1.655      by (rule order_less_trans)
   1.656    moreover from * have "- cos 2 = (\<Sum>n. - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
   1.657      by (rule sums_unique)
   1.658 -  ultimately have "0 < - cos 2" by simp
   1.659 +  ultimately have "(0::real) < - cos 2" by simp
   1.660    then show ?thesis by simp
   1.661  qed
   1.662  
   1.663  lemmas cos_two_neq_zero [simp] = cos_two_less_zero [THEN less_imp_neq]
   1.664  lemmas cos_two_le_zero [simp] = cos_two_less_zero [THEN order_less_imp_le]
   1.665  
   1.666 -lemma cos_is_zero: "EX! x. 0 \<le> x & x \<le> 2 \<and> cos x = 0"
   1.667 +lemma cos_is_zero: "EX! x::real. 0 \<le> x & x \<le> 2 \<and> cos x = 0"
   1.668  proof (rule ex_ex1I)
   1.669 -  show "\<exists>x. 0 \<le> x & x \<le> 2 & cos x = 0"
   1.670 +  show "\<exists>x::real. 0 \<le> x & x \<le> 2 & cos x = 0"
   1.671      by (rule IVT2, simp_all)
   1.672  next
   1.673 -  fix x y
   1.674 +  fix x::real and y::real
   1.675    assume x: "0 \<le> x \<and> x \<le> 2 \<and> cos x = 0"
   1.676    assume y: "0 \<le> y \<and> y \<le> 2 \<and> cos y = 0"
   1.677 -  have [simp]: "\<forall>x. cos differentiable (at x)"
   1.678 +  have [simp]: "\<forall>x::real. cos differentiable (at x)"
   1.679      unfolding real_differentiable_def by (auto intro: DERIV_cos)
   1.680    from x y show "x = y"
   1.681      apply (cut_tac less_linear [of x y], auto)
   1.682      apply (drule_tac f = cos in Rolle)
   1.683      apply (drule_tac [5] f = cos in Rolle)
   1.684      apply (auto dest!: DERIV_cos [THEN DERIV_unique])
   1.685 -    apply (metis order_less_le_trans less_le sin_gt_zero)
   1.686 -    apply (metis order_less_le_trans less_le sin_gt_zero)
   1.687 +    apply (metis order_less_le_trans less_le sin_gt_zero_02)
   1.688 +    apply (metis order_less_le_trans less_le sin_gt_zero_02)
   1.689      done
   1.690  qed
   1.691  
   1.692 @@ -2732,6 +2927,11 @@
   1.693  lemma cos_pi_half [simp]: "cos (pi / 2) = 0"
   1.694    by (simp add: pi_half cos_is_zero [THEN theI'])
   1.695  
   1.696 +lemma cos_of_real_pi_half [simp]: 
   1.697 +  fixes x :: "'a :: {real_field,banach,real_normed_algebra_1}"
   1.698 +  shows "cos ((of_real pi / 2) :: 'a) = 0"
   1.699 +by (metis cos_pi_half cos_of_real eq_numeral_simps(4) nonzero_of_real_divide of_real_0 of_real_numeral)
   1.700 +
   1.701  lemma pi_half_gt_zero [simp]: "0 < pi / 2"
   1.702    apply (rule order_le_neq_trans)
   1.703    apply (simp add: pi_half cos_is_zero [THEN theI'])
   1.704 @@ -2765,29 +2965,67 @@
   1.705  lemma minus_pi_half_less_zero: "-(pi/2) < 0"
   1.706    by simp
   1.707  
   1.708 -lemma m2pi_less_pi: "- (2 * pi) < pi"
   1.709 +lemma m2pi_less_pi: "- (2*pi) < pi"
   1.710    by simp
   1.711  
   1.712  lemma sin_pi_half [simp]: "sin(pi/2) = 1"
   1.713    using sin_cos_squared_add2 [where x = "pi/2"]
   1.714 -  using sin_gt_zero [OF pi_half_gt_zero pi_half_less_two]
   1.715 +  using sin_gt_zero_02 [OF pi_half_gt_zero pi_half_less_two]
   1.716    by (simp add: power2_eq_1_iff)
   1.717  
   1.718 +lemma sin_of_real_pi_half [simp]:
   1.719 +  fixes x :: "'a :: {real_field,banach,real_normed_algebra_1}"
   1.720 +  shows "sin ((of_real pi / 2) :: 'a) = 1"
   1.721 +  using sin_pi_half 
   1.722 +by (metis sin_pi_half eq_numeral_simps(4) nonzero_of_real_divide of_real_1 of_real_numeral sin_of_real)
   1.723 +
   1.724 +lemma sin_cos_eq:
   1.725 +  fixes x :: "'a::{real_normed_field,banach}"
   1.726 +  shows "sin x = cos (of_real pi / 2 - x)"
   1.727 +  by (simp add: cos_diff)
   1.728 +
   1.729 +lemma minus_sin_cos_eq:
   1.730 +  fixes x :: "'a::{real_normed_field,banach}"
   1.731 +  shows "-sin x = cos (x + of_real pi / 2)"
   1.732 +  by (simp add: cos_add nonzero_of_real_divide)
   1.733 +
   1.734 +lemma cos_sin_eq:
   1.735 +  fixes x :: "'a::{real_normed_field,banach}"
   1.736 +  shows "cos x = sin (of_real pi / 2 - x)"
   1.737 +  using sin_cos_eq [of "of_real pi / 2 - x"]
   1.738 +  by simp
   1.739 +
   1.740 +lemma sin_add: 
   1.741 +  fixes x :: "'a::{real_normed_field,banach}"
   1.742 +  shows "sin (x + y) = sin x * cos y + cos x * sin y"
   1.743 +  using cos_add [of "of_real pi / 2 - x" "-y"]
   1.744 +  by (simp add: cos_sin_eq) (simp add: sin_cos_eq)
   1.745 +
   1.746 +lemma sin_diff:
   1.747 +  fixes x :: "'a::{real_normed_field,banach}"
   1.748 +  shows "sin (x - y) = sin x * cos y - cos x * sin y"
   1.749 +  using sin_add [of x "- y"] by simp
   1.750 +
   1.751 +lemma sin_double: 
   1.752 +  fixes x :: "'a::{real_normed_field,banach}"
   1.753 +  shows "sin(2 * x) = 2 * sin x * cos x"
   1.754 +  using sin_add [where x=x and y=x] by simp
   1.755 +
   1.756 +
   1.757 +lemma cos_of_real_pi [simp]: "cos (of_real pi) = -1"
   1.758 +  using cos_add [where x = "pi/2" and y = "pi/2"]
   1.759 +  by (simp add: cos_of_real)
   1.760 +
   1.761 +lemma sin_of_real_pi [simp]: "sin (of_real pi) = 0"
   1.762 +  using sin_add [where x = "pi/2" and y = "pi/2"] 
   1.763 +  by (simp add: sin_of_real)
   1.764 +  
   1.765  lemma cos_pi [simp]: "cos pi = -1"
   1.766    using cos_add [where x = "pi/2" and y = "pi/2"] by simp
   1.767  
   1.768  lemma sin_pi [simp]: "sin pi = 0"
   1.769    using sin_add [where x = "pi/2" and y = "pi/2"] by simp
   1.770  
   1.771 -lemma sin_cos_eq: "sin x = cos (pi/2 - x)"
   1.772 -  by (simp add: cos_diff)
   1.773 -
   1.774 -lemma minus_sin_cos_eq: "-sin x = cos (x + pi/2)"
   1.775 -  by (simp add: cos_add)
   1.776 -
   1.777 -lemma cos_sin_eq: "cos x = sin (pi/2 - x)"
   1.778 -  by (simp add: sin_diff)
   1.779 -
   1.780  lemma sin_periodic_pi [simp]: "sin (x + pi) = - sin x"
   1.781    by (simp add: sin_add)
   1.782  
   1.783 @@ -2798,31 +3036,31 @@
   1.784    by (simp add: cos_add)
   1.785  
   1.786  lemma sin_periodic [simp]: "sin (x + 2*pi) = sin x"
   1.787 -  by (simp add: sin_add cos_double)
   1.788 +  by (simp add: sin_add sin_double cos_double)
   1.789  
   1.790  lemma cos_periodic [simp]: "cos (x + 2*pi) = cos x"
   1.791 -  by (simp add: cos_add cos_double)
   1.792 +  by (simp add: cos_add sin_double cos_double)
   1.793  
   1.794  lemma cos_npi [simp]: "cos (real n * pi) = (- 1) ^ n"
   1.795 -  by (induct n) (auto simp add: real_of_nat_Suc distrib_right)
   1.796 +  by (induct n) (auto simp: real_of_nat_Suc distrib_right)
   1.797  
   1.798  lemma cos_npi2 [simp]: "cos (pi * real n) = (- 1) ^ n"
   1.799    by (metis cos_npi mult.commute)
   1.800  
   1.801  lemma sin_npi [simp]: "sin (real (n::nat) * pi) = 0"
   1.802 -  by (induct n) (auto simp add: real_of_nat_Suc distrib_right)
   1.803 +  by (induct n) (auto simp: real_of_nat_Suc distrib_right)
   1.804  
   1.805  lemma sin_npi2 [simp]: "sin (pi * real (n::nat)) = 0"
   1.806    by (simp add: mult.commute [of pi])
   1.807  
   1.808 -lemma cos_two_pi [simp]: "cos (2 * pi) = 1"
   1.809 +lemma cos_two_pi [simp]: "cos (2*pi) = 1"
   1.810    by (simp add: cos_double)
   1.811  
   1.812 -lemma sin_two_pi [simp]: "sin (2 * pi) = 0"
   1.813 -  by simp
   1.814 -
   1.815 -lemma sin_gt_zero2: "[| 0 < x; x < pi/2 |] ==> 0 < sin x"
   1.816 -  by (metis sin_gt_zero order_less_trans pi_half_less_two)
   1.817 +lemma sin_two_pi [simp]: "sin (2*pi) = 0"
   1.818 +  by (simp add: sin_double)
   1.819 +
   1.820 +lemma sin_gt_zero2: "\<lbrakk>0 < x; x < pi/2\<rbrakk> \<Longrightarrow> 0 < sin x"
   1.821 +  by (metis sin_gt_zero_02 order_less_trans pi_half_less_two)
   1.822  
   1.823  lemma sin_less_zero:
   1.824    assumes "- pi/2 < x" and "x < 0"
   1.825 @@ -2835,53 +3073,52 @@
   1.826  lemma pi_less_4: "pi < 4"
   1.827    using pi_half_less_two by auto
   1.828  
   1.829 -lemma cos_gt_zero: "[| 0 < x; x < pi/2 |] ==> 0 < cos x"
   1.830 -  apply (cut_tac pi_less_4)
   1.831 -  apply (cut_tac f = cos and a = 0 and b = x and y = 0 in IVT2_objl, safe, simp_all)
   1.832 -  apply (cut_tac cos_is_zero, safe)
   1.833 -  apply (rename_tac y z)
   1.834 -  apply (drule_tac x = y in spec)
   1.835 -  apply (drule_tac x = "pi/2" in spec, simp)
   1.836 -  done
   1.837 -
   1.838 -lemma cos_gt_zero_pi: "[| -(pi/2) < x; x < pi/2 |] ==> 0 < cos x"
   1.839 -  apply (rule_tac x = x and y = 0 in linorder_cases)
   1.840 -  apply (metis cos_gt_zero cos_minus minus_less_iff neg_0_less_iff_less)
   1.841 -  apply (auto intro: cos_gt_zero)
   1.842 -  done
   1.843 -
   1.844 -lemma cos_ge_zero: "[| -(pi/2) \<le> x; x \<le> pi/2 |] ==> 0 \<le> cos x"
   1.845 -  apply (auto simp add: order_le_less cos_gt_zero_pi)
   1.846 -  apply (subgoal_tac "x = pi/2", auto)
   1.847 -  done
   1.848 -
   1.849 -lemma sin_gt_zero_pi: "[| 0 < x; x < pi  |] ==> 0 < sin x"
   1.850 +lemma cos_gt_zero: "\<lbrakk>0 < x; x < pi/2\<rbrakk> \<Longrightarrow> 0 < cos x"
   1.851 +  by (simp add: cos_sin_eq sin_gt_zero2)
   1.852 +
   1.853 +lemma cos_gt_zero_pi: "\<lbrakk>-(pi/2) < x; x < pi/2\<rbrakk> \<Longrightarrow> 0 < cos x"
   1.854 +  using cos_gt_zero [of x] cos_gt_zero [of "-x"]
   1.855 +  by (cases rule: linorder_cases [of x 0]) auto
   1.856 +
   1.857 +lemma cos_ge_zero: "\<lbrakk>-(pi/2) \<le> x; x \<le> pi/2\<rbrakk> \<Longrightarrow> 0 \<le> cos x"
   1.858 +  apply (auto simp: order_le_less cos_gt_zero_pi)
   1.859 +  by (metis cos_pi_half eq_divide_eq eq_numeral_simps(4))
   1.860 +
   1.861 +lemma sin_gt_zero: "\<lbrakk>0 < x; x < pi \<rbrakk> \<Longrightarrow> 0 < sin x"
   1.862    by (simp add: sin_cos_eq cos_gt_zero_pi)
   1.863  
   1.864 +lemma sin_lt_zero: "pi < x \<Longrightarrow> x < 2*pi \<Longrightarrow> sin x < 0"
   1.865 +  using sin_gt_zero [of "x-pi"]
   1.866 +  by (simp add: sin_diff)
   1.867 +
   1.868  lemma pi_ge_two: "2 \<le> pi"
   1.869  proof (rule ccontr)
   1.870    assume "\<not> 2 \<le> pi" hence "pi < 2" by auto
   1.871 -  have "\<exists>y > pi. y < 2 \<and> y < 2 * pi"
   1.872 -  proof (cases "2 < 2 * pi")
   1.873 +  have "\<exists>y > pi. y < 2 \<and> y < 2*pi"
   1.874 +  proof (cases "2 < 2*pi")
   1.875      case True with dense[OF `pi < 2`] show ?thesis by auto
   1.876    next
   1.877 -    case False have "pi < 2 * pi" by auto
   1.878 +    case False have "pi < 2*pi" by auto
   1.879      from dense[OF this] and False show ?thesis by auto
   1.880    qed
   1.881 -  then obtain y where "pi < y" and "y < 2" and "y < 2 * pi" by blast
   1.882 -  hence "0 < sin y" using sin_gt_zero by auto
   1.883 +  then obtain y where "pi < y" and "y < 2" and "y < 2*pi" by blast
   1.884 +  hence "0 < sin y" using sin_gt_zero_02 by auto
   1.885    moreover
   1.886 -  have "sin y < 0" using sin_gt_zero_pi[of "y - pi"] `pi < y` and `y < 2 * pi` sin_periodic_pi[of "y - pi"] by auto
   1.887 +  have "sin y < 0" using sin_gt_zero[of "y - pi"] `pi < y` and `y < 2*pi` sin_periodic_pi[of "y - pi"] by auto
   1.888    ultimately show False by auto
   1.889  qed
   1.890  
   1.891 -lemma sin_ge_zero: "[| 0 \<le> x; x \<le> pi |] ==> 0 \<le> sin x"
   1.892 -  by (auto simp add: order_le_less sin_gt_zero_pi)
   1.893 +lemma sin_ge_zero: "\<lbrakk>0 \<le> x; x \<le> pi\<rbrakk> \<Longrightarrow> 0 \<le> sin x"
   1.894 +  by (auto simp: order_le_less sin_gt_zero)
   1.895 +
   1.896 +lemma sin_le_zero: "pi \<le> x \<Longrightarrow> x < 2*pi \<Longrightarrow> sin x \<le> 0"
   1.897 +  using sin_ge_zero [of "x-pi"]
   1.898 +  by (simp add: sin_diff)
   1.899  
   1.900  text {* FIXME: This proof is almost identical to lemma @{text cos_is_zero}.
   1.901    It should be possible to factor out some of the common parts. *}
   1.902  
   1.903 -lemma cos_total: "[| -1 \<le> y; y \<le> 1 |] ==> EX! x. 0 \<le> x & x \<le> pi & (cos x = y)"
   1.904 +lemma cos_total: "\<lbrakk>-1 \<le> y; y \<le> 1\<rbrakk> \<Longrightarrow> EX! x. 0 \<le> x & x \<le> pi & (cos x = y)"
   1.905  proof (rule ex_ex1I)
   1.906    assume y: "-1 \<le> y" "y \<le> 1"
   1.907    show "\<exists>x. 0 \<le> x & x \<le> pi & cos x = y"
   1.908 @@ -2890,34 +3127,37 @@
   1.909    fix a b
   1.910    assume a: "0 \<le> a \<and> a \<le> pi \<and> cos a = y"
   1.911    assume b: "0 \<le> b \<and> b \<le> pi \<and> cos b = y"
   1.912 -  have [simp]: "\<forall>x. cos differentiable (at x)"
   1.913 +  have [simp]: "\<forall>x::real. cos differentiable (at x)"
   1.914      unfolding real_differentiable_def by (auto intro: DERIV_cos)
   1.915    from a b show "a = b"
   1.916      apply (cut_tac less_linear [of a b], auto)
   1.917      apply (drule_tac f = cos in Rolle)
   1.918      apply (drule_tac [5] f = cos in Rolle)
   1.919      apply (auto dest!: DERIV_cos [THEN DERIV_unique])
   1.920 -    apply (metis order_less_le_trans less_le sin_gt_zero_pi)
   1.921 -    apply (metis order_less_le_trans less_le sin_gt_zero_pi)
   1.922 +    apply (metis order_less_le_trans less_le sin_gt_zero)
   1.923 +    apply (metis order_less_le_trans less_le sin_gt_zero)
   1.924      done
   1.925  qed
   1.926  
   1.927  lemma sin_total:
   1.928 -     "[| -1 \<le> y; y \<le> 1 |] ==> EX! x. -(pi/2) \<le> x & x \<le> pi/2 & (sin x = y)"
   1.929 -apply (rule ccontr)
   1.930 -apply (subgoal_tac "\<forall>x. (- (pi/2) \<le> x & x \<le> pi/2 & (sin x = y)) = (0 \<le> (x + pi/2) & (x + pi/2) \<le> pi & (cos (x + pi/2) = -y))")
   1.931 -apply (erule contrapos_np)
   1.932 -apply simp
   1.933 -apply (cut_tac y="-y" in cos_total, simp) apply simp
   1.934 -apply (erule ex1E)
   1.935 -apply (rule_tac a = "x - (pi/2)" in ex1I)
   1.936 -apply (simp (no_asm) add: add.assoc)
   1.937 -apply (rotate_tac 3)
   1.938 -apply (drule_tac x = "xa + pi/2" in spec, safe, simp_all add: cos_add)
   1.939 -done
   1.940 +  assumes y: "-1 \<le> y" "y \<le> 1"
   1.941 +    shows "\<exists>! x. -(pi/2) \<le> x & x \<le> pi/2 & (sin x = y)"
   1.942 +proof -
   1.943 +  from cos_total [OF y]
   1.944 +  obtain x where x: "0 \<le> x" "x \<le> pi" "cos x = y"
   1.945 +           and uniq: "\<And>x'. 0 \<le> x' \<Longrightarrow> x' \<le> pi \<Longrightarrow> cos x' = y \<Longrightarrow> x' = x "
   1.946 +    by blast
   1.947 +  show ?thesis
   1.948 +    apply (simp add: sin_cos_eq)
   1.949 +    apply (rule ex1I [where a="pi/2 - x"])
   1.950 +    apply (cut_tac [2] x'="pi/2 - xa" in uniq)
   1.951 +    using x
   1.952 +    apply auto
   1.953 +    done
   1.954 +qed
   1.955  
   1.956  lemma reals_Archimedean4:
   1.957 -     "[| 0 < y; 0 \<le> x |] ==> \<exists>n. real n * y \<le> x & x < real (Suc n) * y"
   1.958 +     "\<lbrakk>0 < y; 0 \<le> x\<rbrakk> \<Longrightarrow> \<exists>n. real n * y \<le> x & x < real (Suc n) * y"
   1.959  apply (auto dest!: reals_Archimedean3)
   1.960  apply (drule_tac x = x in spec, clarify)
   1.961  apply (subgoal_tac "x < real(LEAST m::nat. x < real m * y) * y")
   1.962 @@ -2928,15 +3168,13 @@
   1.963   prefer 2 apply (rule not_less_Least, simp, force)
   1.964  done
   1.965  
   1.966 -(* Pre Isabelle99-2 proof was simpler- numerals arithmetic
   1.967 -   now causes some unwanted re-arrangements of literals!   *)
   1.968  lemma cos_zero_lemma:
   1.969 -     "[| 0 \<le> x; cos x = 0 |] ==>
   1.970 -      \<exists>n::nat. ~even n & x = real n * (pi/2)"
   1.971 +     "\<lbrakk>0 \<le> x; cos x = 0\<rbrakk> \<Longrightarrow>
   1.972 +      \<exists>n::nat. odd n & x = real n * (pi/2)"
   1.973  apply (drule pi_gt_zero [THEN reals_Archimedean4], safe)
   1.974  apply (subgoal_tac "0 \<le> x - real n * pi &
   1.975                      (x - real n * pi) \<le> pi & (cos (x - real n * pi) = 0) ")
   1.976 -apply (auto simp add: algebra_simps real_of_nat_Suc)
   1.977 +apply (auto simp: algebra_simps real_of_nat_Suc)
   1.978   prefer 2 apply (simp add: cos_diff)
   1.979  apply (simp add: cos_diff)
   1.980  apply (subgoal_tac "EX! x. 0 \<le> x & x \<le> pi & cos x = 0")
   1.981 @@ -2949,19 +3187,19 @@
   1.982  done
   1.983  
   1.984  lemma sin_zero_lemma:
   1.985 -     "[| 0 \<le> x; sin x = 0 |] ==>
   1.986 +     "\<lbrakk>0 \<le> x; sin x = 0\<rbrakk> \<Longrightarrow>
   1.987        \<exists>n::nat. even n & x = real n * (pi/2)"
   1.988  apply (subgoal_tac "\<exists>n::nat. ~ even n & x + pi/2 = real n * (pi/2) ")
   1.989   apply (clarify, rule_tac x = "n - 1" in exI)
   1.990   apply (auto elim!: oddE simp add: real_of_nat_Suc field_simps)[1]
   1.991   apply (rule cos_zero_lemma)
   1.992 - apply (auto simp add: cos_add)
   1.993 + apply (auto simp: cos_add)
   1.994  done
   1.995  
   1.996  lemma cos_zero_iff:
   1.997       "(cos x = 0) =
   1.998 -      ((\<exists>n::nat. ~even n & (x = real n * (pi/2))) |
   1.999 -       (\<exists>n::nat. ~even n & (x = -(real n * (pi/2)))))"
  1.1000 +      ((\<exists>n::nat. odd n & (x = real n * (pi/2))) |
  1.1001 +       (\<exists>n::nat. odd n & (x = -(real n * (pi/2)))))"
  1.1002  proof -
  1.1003    { fix n :: nat
  1.1004      assume "odd n"
  1.1005 @@ -2991,6 +3229,53 @@
  1.1006  apply (auto elim: evenE)
  1.1007  done
  1.1008  
  1.1009 +
  1.1010 +lemma cos_zero_iff_int:
  1.1011 +     "cos x = 0 \<longleftrightarrow> (\<exists>n::int. odd n & x = real n * (pi/2))"
  1.1012 +proof safe
  1.1013 +  assume "cos x = 0"
  1.1014 +  then show "\<exists>n::int. odd n & x = real n * (pi/2)"
  1.1015 +    apply (simp add: cos_zero_iff, safe)
  1.1016 +    apply (metis even_int_iff real_of_int_of_nat_eq)
  1.1017 +    apply (rule_tac x="- (int n)" in exI, simp)
  1.1018 +    done
  1.1019 +next
  1.1020 +  fix n::int
  1.1021 +  assume "odd n" 
  1.1022 +  then show "cos (real n * (pi / 2)) = 0"
  1.1023 +    apply (simp add: cos_zero_iff)
  1.1024 +    apply (case_tac n rule: int_cases2, simp)
  1.1025 +    apply (rule disjI2)
  1.1026 +    apply (rule_tac x="nat (-n)" in exI, simp)
  1.1027 +    done
  1.1028 +qed
  1.1029 +
  1.1030 +lemma sin_zero_iff_int:  
  1.1031 +     "sin x = 0 \<longleftrightarrow> (\<exists>n::int. even n & (x = real n * (pi/2)))"
  1.1032 +proof safe
  1.1033 +  assume "sin x = 0"
  1.1034 +  then show "\<exists>n::int. even n \<and> x = real n * (pi / 2)"
  1.1035 +    apply (simp add: sin_zero_iff, safe)
  1.1036 +    apply (metis even_int_iff real_of_int_of_nat_eq)
  1.1037 +    apply (rule_tac x="- (int n)" in exI, simp)
  1.1038 +    done
  1.1039 +next
  1.1040 +  fix n::int
  1.1041 +  assume "even n" 
  1.1042 +  then show "sin (real n * (pi / 2)) = 0"
  1.1043 +    apply (simp add: sin_zero_iff)
  1.1044 +    apply (case_tac n rule: int_cases2, simp)
  1.1045 +    apply (rule disjI2)
  1.1046 +    apply (rule_tac x="nat (-n)" in exI, simp)
  1.1047 +    done
  1.1048 +qed
  1.1049 +
  1.1050 +lemma sin_zero_iff_int2: "sin x = 0 \<longleftrightarrow> (\<exists>n::int. x = real n * pi)"
  1.1051 +  apply (simp only: sin_zero_iff_int)     
  1.1052 +  apply (safe elim!: evenE)     
  1.1053 +  apply (simp_all add: field_simps)
  1.1054 +  using dvd_triv_left by fastforce
  1.1055 +
  1.1056  lemma cos_monotone_0_pi:
  1.1057    assumes "0 \<le> y" and "y < x" and "x \<le> pi"
  1.1058    shows "cos x < cos y"
  1.1059 @@ -3001,7 +3286,7 @@
  1.1060    obtain z where "y < z" and "z < x" and cos_diff: "cos x - cos y = (x - y) * - sin z"
  1.1061      by auto
  1.1062    hence "0 < z" and "z < pi" using assms by auto
  1.1063 -  hence "0 < sin z" using sin_gt_zero_pi by auto
  1.1064 +  hence "0 < sin z" using sin_gt_zero by auto
  1.1065    hence "cos x - cos y < 0"
  1.1066      unfolding cos_diff minus_mult_commute[symmetric]
  1.1067      using `- (x - y) < 0` by (rule mult_pos_neg2)
  1.1068 @@ -3051,13 +3336,43 @@
  1.1069    have "0 \<le> y + pi / 2" and "y + pi / 2 \<le> x + pi / 2" and "x + pi /2 \<le> pi"
  1.1070      using pi_ge_two and assms by auto
  1.1071    from cos_monotone_0_pi'[OF this] show ?thesis
  1.1072 -    unfolding minus_sin_cos_eq[symmetric] by auto
  1.1073 +    unfolding minus_sin_cos_eq[symmetric]
  1.1074 +    by (metis minus_sin_cos_eq mult.right_neutral neg_le_iff_le of_real_def real_scaleR_def) 
  1.1075 +qed
  1.1076 +
  1.1077 +lemma sin_x_le_x:
  1.1078 +  fixes x::real assumes x: "x \<ge> 0" shows "sin x \<le> x"
  1.1079 +proof -
  1.1080 +  let ?f = "\<lambda>x. x - sin x"
  1.1081 +  from x have "?f x \<ge> ?f 0"
  1.1082 +    apply (rule DERIV_nonneg_imp_nondecreasing)
  1.1083 +    apply (intro allI impI exI[of _ "1 - cos x" for x])
  1.1084 +    apply (auto intro!: derivative_eq_intros simp: field_simps)
  1.1085 +    done
  1.1086 +  thus "sin x \<le> x" by simp
  1.1087  qed
  1.1088  
  1.1089 +lemma sin_x_ge_neg_x:
  1.1090 +  fixes x::real assumes x: "x \<ge> 0" shows "sin x \<ge> - x"
  1.1091 +proof -
  1.1092 +  let ?f = "\<lambda>x. x + sin x"
  1.1093 +  from x have "?f x \<ge> ?f 0"
  1.1094 +    apply (rule DERIV_nonneg_imp_nondecreasing)
  1.1095 +    apply (intro allI impI exI[of _ "1 + cos x" for x])
  1.1096 +    apply (auto intro!: derivative_eq_intros simp: field_simps real_0_le_add_iff)
  1.1097 +    done
  1.1098 +  thus "sin x \<ge> -x" by simp
  1.1099 +qed
  1.1100 +
  1.1101 +lemma abs_sin_x_le_abs_x:
  1.1102 +  fixes x::real shows "\<bar>sin x\<bar> \<le> \<bar>x\<bar>"
  1.1103 +  using sin_x_ge_neg_x [of x] sin_x_le_x [of x] sin_x_ge_neg_x [of "-x"] sin_x_le_x [of "-x"]
  1.1104 +  by (auto simp: abs_real_def)
  1.1105 +
  1.1106  
  1.1107  subsection {* Tangent *}
  1.1108  
  1.1109 -definition tan :: "real \<Rightarrow> real"
  1.1110 +definition tan :: "'a \<Rightarrow> 'a::{real_normed_field,banach}"
  1.1111    where "tan = (\<lambda>x. sin x / cos x)"
  1.1112  
  1.1113  lemma tan_zero [simp]: "tan 0 = 0"
  1.1114 @@ -3080,20 +3395,25 @@
  1.1115    by (simp add: tan_def cos_add field_simps)
  1.1116  
  1.1117  lemma add_tan_eq:
  1.1118 -  "\<lbrakk>cos x \<noteq> 0; cos y \<noteq> 0\<rbrakk> \<Longrightarrow> tan x + tan y = sin(x + y)/(cos x * cos y)"
  1.1119 +  fixes x :: "'a::{real_normed_field,banach}"
  1.1120 +  shows "\<lbrakk>cos x \<noteq> 0; cos y \<noteq> 0\<rbrakk> \<Longrightarrow> tan x + tan y = sin(x + y)/(cos x * cos y)"
  1.1121    by (simp add: tan_def sin_add field_simps)
  1.1122  
  1.1123  lemma tan_add:
  1.1124 -     "[| cos x \<noteq> 0; cos y \<noteq> 0; cos (x + y) \<noteq> 0 |]
  1.1125 -      ==> tan(x + y) = (tan(x) + tan(y))/(1 - tan(x) * tan(y))"
  1.1126 -  by (simp add: add_tan_eq lemma_tan_add1, simp add: tan_def)
  1.1127 +  fixes x :: "'a::{real_normed_field,banach}"
  1.1128 +  shows 
  1.1129 +     "\<lbrakk>cos x \<noteq> 0; cos y \<noteq> 0; cos (x + y) \<noteq> 0\<rbrakk>
  1.1130 +      \<Longrightarrow> tan(x + y) = (tan(x) + tan(y))/(1 - tan(x) * tan(y))"
  1.1131 +      by (simp add: add_tan_eq lemma_tan_add1 field_simps) (simp add: tan_def)
  1.1132  
  1.1133  lemma tan_double:
  1.1134 -     "[| cos x \<noteq> 0; cos (2 * x) \<noteq> 0 |]
  1.1135 -      ==> tan (2 * x) = (2 * tan x) / (1 - (tan x)\<^sup>2)"
  1.1136 +  fixes x :: "'a::{real_normed_field,banach}"
  1.1137 +  shows 
  1.1138 +     "\<lbrakk>cos x \<noteq> 0; cos (2 * x) \<noteq> 0\<rbrakk>
  1.1139 +      \<Longrightarrow> tan (2 * x) = (2 * tan x) / (1 - (tan x)\<^sup>2)"
  1.1140    using tan_add [of x x] by (simp add: power2_eq_square)
  1.1141  
  1.1142 -lemma tan_gt_zero: "[| 0 < x; x < pi/2 |] ==> 0 < tan x"
  1.1143 +lemma tan_gt_zero: "\<lbrakk>0 < x; x < pi/2\<rbrakk> \<Longrightarrow> 0 < tan x"
  1.1144    by (simp add: tan_def zero_less_divide_iff sin_gt_zero2 cos_gt_zero_pi)
  1.1145  
  1.1146  lemma tan_less_zero:
  1.1147 @@ -3104,41 +3424,49 @@
  1.1148    thus ?thesis by simp
  1.1149  qed
  1.1150  
  1.1151 -lemma tan_half: "tan x = sin (2 * x) / (cos (2 * x) + 1)"
  1.1152 +lemma tan_half:
  1.1153 +  fixes x :: "'a::{real_normed_field,banach,field_inverse_zero}"
  1.1154 +  shows  "tan x = sin (2 * x) / (cos (2 * x) + 1)"
  1.1155    unfolding tan_def sin_double cos_double sin_squared_eq
  1.1156    by (simp add: power2_eq_square)
  1.1157  
  1.1158 -lemma DERIV_tan [simp]: "cos x \<noteq> 0 \<Longrightarrow> DERIV tan x :> inverse ((cos x)\<^sup>2)"
  1.1159 +lemma DERIV_tan [simp]:
  1.1160 +  fixes x :: "'a::{real_normed_field,banach}"
  1.1161 +  shows "cos x \<noteq> 0 \<Longrightarrow> DERIV tan x :> inverse ((cos x)\<^sup>2)"
  1.1162    unfolding tan_def
  1.1163    by (auto intro!: derivative_eq_intros, simp add: divide_inverse power2_eq_square)
  1.1164  
  1.1165 -lemma isCont_tan: "cos x \<noteq> 0 \<Longrightarrow> isCont tan x"
  1.1166 +lemma isCont_tan:
  1.1167 +  fixes x :: "'a::{real_normed_field,banach}"
  1.1168 +  shows "cos x \<noteq> 0 \<Longrightarrow> isCont tan x"
  1.1169    by (rule DERIV_tan [THEN DERIV_isCont])
  1.1170  
  1.1171 -lemma isCont_tan' [simp]:
  1.1172 -  "\<lbrakk>isCont f a; cos (f a) \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. tan (f x)) a"
  1.1173 +lemma isCont_tan' [simp,continuous_intros]:
  1.1174 +  fixes a :: "'a::{real_normed_field,banach}" and f :: "'a \<Rightarrow> 'a"
  1.1175 +  shows "\<lbrakk>isCont f a; cos (f a) \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. tan (f x)) a"
  1.1176    by (rule isCont_o2 [OF _ isCont_tan])
  1.1177  
  1.1178  lemma tendsto_tan [tendsto_intros]:
  1.1179 -  "\<lbrakk>(f ---> a) F; cos a \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. tan (f x)) ---> tan a) F"
  1.1180 +  fixes f :: "'a \<Rightarrow> 'a::{real_normed_field,banach}"
  1.1181 +  shows "\<lbrakk>(f ---> a) F; cos a \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. tan (f x)) ---> tan a) F"
  1.1182    by (rule isCont_tendsto_compose [OF isCont_tan])
  1.1183  
  1.1184  lemma continuous_tan:
  1.1185 -  "continuous F f \<Longrightarrow> cos (f (Lim F (\<lambda>x. x))) \<noteq> 0 \<Longrightarrow> continuous F (\<lambda>x. tan (f x))"
  1.1186 +  fixes f :: "'a \<Rightarrow> 'a::{real_normed_field,banach}"
  1.1187 +  shows "continuous F f \<Longrightarrow> cos (f (Lim F (\<lambda>x. x))) \<noteq> 0 \<Longrightarrow> continuous F (\<lambda>x. tan (f x))"
  1.1188    unfolding continuous_def by (rule tendsto_tan)
  1.1189  
  1.1190 -lemma isCont_tan'' [continuous_intros]:
  1.1191 -  "continuous (at x) f \<Longrightarrow> cos (f x) \<noteq> 0 \<Longrightarrow> continuous (at x) (\<lambda>x. tan (f x))"
  1.1192 -  unfolding continuous_at by (rule tendsto_tan)
  1.1193 +lemma continuous_on_tan [continuous_intros]:
  1.1194 +  fixes f :: "'a \<Rightarrow> 'a::{real_normed_field,banach}"
  1.1195 +  shows "continuous_on s f \<Longrightarrow> (\<forall>x\<in>s. cos (f x) \<noteq> 0) \<Longrightarrow> continuous_on s (\<lambda>x. tan (f x))"
  1.1196 +  unfolding continuous_on_def by (auto intro: tendsto_tan)
  1.1197  
  1.1198  lemma continuous_within_tan [continuous_intros]:
  1.1199 +  fixes f :: "'a \<Rightarrow> 'a::{real_normed_field,banach}"
  1.1200 +  shows 
  1.1201    "continuous (at x within s) f \<Longrightarrow> cos (f x) \<noteq> 0 \<Longrightarrow> continuous (at x within s) (\<lambda>x. tan (f x))"
  1.1202    unfolding continuous_within by (rule tendsto_tan)
  1.1203  
  1.1204 -lemma continuous_on_tan [continuous_intros]:
  1.1205 -  "continuous_on s f \<Longrightarrow> (\<forall>x\<in>s. cos (f x) \<noteq> 0) \<Longrightarrow> continuous_on s (\<lambda>x. tan (f x))"
  1.1206 -  unfolding continuous_on_def by (auto intro: tendsto_tan)
  1.1207 -
  1.1208  lemma LIM_cos_div_sin: "(\<lambda>x. cos(x)/sin(x)) -- pi/2 --> 0"
  1.1209    by (rule LIM_cong_limit, (rule tendsto_intros)+, simp_all)
  1.1210  
  1.1211 @@ -3279,7 +3607,9 @@
  1.1212  lemma tan_periodic_n[simp]: "tan (x + numeral n * pi) = tan x"
  1.1213    using tan_periodic_int[of _ "numeral n" ] unfolding real_numeral .
  1.1214  
  1.1215 +
  1.1216  subsection {* Inverse Trigonometric Functions *}
  1.1217 +text{*STILL DEFINED FOR THE REALS ONLY*}
  1.1218  
  1.1219  definition arcsin :: "real => real"
  1.1220    where "arcsin y = (THE x. -(pi/2) \<le> x & x \<le> pi/2 & sin x = y)"
  1.1221 @@ -3314,7 +3644,7 @@
  1.1222    by (blast dest: arcsin)
  1.1223  
  1.1224  lemma arcsin_lt_bounded:
  1.1225 -     "[| -1 < y; y < 1 |] ==> -(pi/2) < arcsin y & arcsin y < pi/2"
  1.1226 +     "\<lbrakk>-1 < y; y < 1\<rbrakk> \<Longrightarrow> -(pi/2) < arcsin y & arcsin y < pi/2"
  1.1227    apply (frule order_less_imp_le)
  1.1228    apply (frule_tac y = y in order_less_imp_le)
  1.1229    apply (frule arcsin_bounded)
  1.1230 @@ -3324,32 +3654,32 @@
  1.1231    apply (drule_tac [!] f = sin in arg_cong, auto)
  1.1232    done
  1.1233  
  1.1234 -lemma arcsin_sin: "[|-(pi/2) \<le> x; x \<le> pi/2 |] ==> arcsin(sin x) = x"
  1.1235 +lemma arcsin_sin: "\<lbrakk>-(pi/2) \<le> x; x \<le> pi/2\<rbrakk> \<Longrightarrow> arcsin(sin x) = x"
  1.1236    apply (unfold arcsin_def)
  1.1237    apply (rule the1_equality)
  1.1238    apply (rule sin_total, auto)
  1.1239    done
  1.1240  
  1.1241  lemma arccos:
  1.1242 -     "[| -1 \<le> y; y \<le> 1 |]
  1.1243 -      ==> 0 \<le> arccos y & arccos y \<le> pi & cos(arccos y) = y"
  1.1244 +     "\<lbrakk>-1 \<le> y; y \<le> 1\<rbrakk>
  1.1245 +      \<Longrightarrow> 0 \<le> arccos y & arccos y \<le> pi & cos(arccos y) = y"
  1.1246    unfolding arccos_def by (rule theI' [OF cos_total])
  1.1247  
  1.1248 -lemma cos_arccos [simp]: "[| -1 \<le> y; y \<le> 1 |] ==> cos(arccos y) = y"
  1.1249 +lemma cos_arccos [simp]: "\<lbrakk>-1 \<le> y; y \<le> 1\<rbrakk> \<Longrightarrow> cos(arccos y) = y"
  1.1250    by (blast dest: arccos)
  1.1251  
  1.1252 -lemma arccos_bounded: "[| -1 \<le> y; y \<le> 1 |] ==> 0 \<le> arccos y & arccos y \<le> pi"
  1.1253 +lemma arccos_bounded: "\<lbrakk>-1 \<le> y; y \<le> 1\<rbrakk> \<Longrightarrow> 0 \<le> arccos y & arccos y \<le> pi"
  1.1254    by (blast dest: arccos)
  1.1255  
  1.1256 -lemma arccos_lbound: "[| -1 \<le> y; y \<le> 1 |] ==> 0 \<le> arccos y"
  1.1257 +lemma arccos_lbound: "\<lbrakk>-1 \<le> y; y \<le> 1\<rbrakk> \<Longrightarrow> 0 \<le> arccos y"
  1.1258    by (blast dest: arccos)
  1.1259  
  1.1260 -lemma arccos_ubound: "[| -1 \<le> y; y \<le> 1 |] ==> arccos y \<le> pi"
  1.1261 +lemma arccos_ubound: "\<lbrakk>-1 \<le> y; y \<le> 1\<rbrakk> \<Longrightarrow> arccos y \<le> pi"
  1.1262    by (blast dest: arccos)
  1.1263  
  1.1264  lemma arccos_lt_bounded:
  1.1265 -     "[| -1 < y; y < 1 |]
  1.1266 -      ==> 0 < arccos y & arccos y < pi"
  1.1267 +     "\<lbrakk>-1 < y; y < 1\<rbrakk>
  1.1268 +      \<Longrightarrow> 0 < arccos y & arccos y < pi"
  1.1269    apply (frule order_less_imp_le)
  1.1270    apply (frule_tac y = y in order_less_imp_le)
  1.1271    apply (frule arccos_bounded, auto)
  1.1272 @@ -3358,12 +3688,12 @@
  1.1273    apply (drule_tac [!] f = cos in arg_cong, auto)
  1.1274    done
  1.1275  
  1.1276 -lemma arccos_cos: "[|0 \<le> x; x \<le> pi |] ==> arccos(cos x) = x"
  1.1277 +lemma arccos_cos: "\<lbrakk>0 \<le> x; x \<le> pi\<rbrakk> \<Longrightarrow> arccos(cos x) = x"
  1.1278    apply (simp add: arccos_def)
  1.1279    apply (auto intro!: the1_equality cos_total)
  1.1280    done
  1.1281  
  1.1282 -lemma arccos_cos2: "[|x \<le> 0; -pi \<le> x |] ==> arccos(cos x) = -x"
  1.1283 +lemma arccos_cos2: "\<lbrakk>x \<le> 0; -pi \<le> x\<rbrakk> \<Longrightarrow> arccos(cos x) = -x"
  1.1284    apply (simp add: arccos_def)
  1.1285    apply (auto intro!: the1_equality cos_total)
  1.1286    done
  1.1287 @@ -3423,8 +3753,7 @@
  1.1288  lemma arctan_minus: "arctan (- x) = - arctan x"
  1.1289    apply (rule arctan_unique)
  1.1290    apply (simp only: neg_less_iff_less arctan_ubound)
  1.1291 -  apply (metis minus_less_iff arctan_lbound)
  1.1292 -  apply simp
  1.1293 +  apply (metis minus_less_iff arctan_lbound, simp)
  1.1294    done
  1.1295  
  1.1296  lemma cos_arctan_not_zero [simp]: "cos (arctan x) \<noteq> 0"
  1.1297 @@ -3448,7 +3777,9 @@
  1.1298    using tan_arctan [of x] unfolding tan_def cos_arctan
  1.1299    by (simp add: eq_divide_eq)
  1.1300  
  1.1301 -lemma tan_sec: "cos x \<noteq> 0 ==> 1 + (tan x)\<^sup>2 = (inverse (cos x))\<^sup>2"
  1.1302 +lemma tan_sec:
  1.1303 +  fixes x :: "'a::{real_normed_field,banach,field_inverse_zero}"
  1.1304 +  shows "cos x \<noteq> 0 \<Longrightarrow> 1 + (tan x)\<^sup>2 = (inverse (cos x))\<^sup>2"
  1.1305    apply (rule power_inverse [THEN subst])
  1.1306    apply (rule_tac c1 = "(cos x)\<^sup>2" in mult_right_cancel [THEN iffD1])
  1.1307    apply (auto dest: field_power_not_zero
  1.1308 @@ -3548,26 +3879,22 @@
  1.1309  
  1.1310  lemma DERIV_arcsin:
  1.1311    "\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> DERIV arcsin x :> inverse (sqrt (1 - x\<^sup>2))"
  1.1312 -  apply (rule DERIV_inverse_function [where f=sin and a="-1" and b="1"])
  1.1313 +  apply (rule DERIV_inverse_function [where f=sin and a="-1" and b=1])
  1.1314    apply (rule DERIV_cong [OF DERIV_sin])
  1.1315    apply (simp add: cos_arcsin)
  1.1316    apply (subgoal_tac "\<bar>x\<bar>\<^sup>2 < 1\<^sup>2", simp)
  1.1317 -  apply (rule power_strict_mono, simp, simp, simp)
  1.1318 -  apply assumption
  1.1319 -  apply assumption
  1.1320 +  apply (rule power_strict_mono, simp, simp, simp, assumption, assumption)
  1.1321    apply simp
  1.1322    apply (erule (1) isCont_arcsin)
  1.1323    done
  1.1324  
  1.1325  lemma DERIV_arccos:
  1.1326    "\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> DERIV arccos x :> inverse (- sqrt (1 - x\<^sup>2))"
  1.1327 -  apply (rule DERIV_inverse_function [where f=cos and a="-1" and b="1"])
  1.1328 +  apply (rule DERIV_inverse_function [where f=cos and a="-1" and b=1])
  1.1329    apply (rule DERIV_cong [OF DERIV_cos])
  1.1330    apply (simp add: sin_arccos)
  1.1331    apply (subgoal_tac "\<bar>x\<bar>\<^sup>2 < 1\<^sup>2", simp)
  1.1332 -  apply (rule power_strict_mono, simp, simp, simp)
  1.1333 -  apply assumption
  1.1334 -  apply assumption
  1.1335 +  apply (rule power_strict_mono, simp, simp, simp, assumption, assumption)
  1.1336    apply simp
  1.1337    apply (erule (1) isCont_arccos)
  1.1338    done
  1.1339 @@ -3643,7 +3970,7 @@
  1.1340      using nonneg by (rule power2_eq_imp_eq) simp
  1.1341  qed
  1.1342  
  1.1343 -lemma cos_30: "cos (pi / 6) = sqrt 3 / 2"
  1.1344 +lemma cos_30: "cos (pi / 6) = sqrt 3/2"
  1.1345  proof -
  1.1346    let ?c = "cos (pi / 6)" and ?s = "sin (pi / 6)"
  1.1347    have pos_c: "0 < ?c"
  1.1348 @@ -3654,7 +3981,7 @@
  1.1349      by (simp only: cos_add sin_add)
  1.1350    also have "\<dots> = ?c * (?c\<^sup>2 - 3 * ?s\<^sup>2)"
  1.1351      by (simp add: algebra_simps power2_eq_square)
  1.1352 -  finally have "?c\<^sup>2 = (sqrt 3 / 2)\<^sup>2"
  1.1353 +  finally have "?c\<^sup>2 = (sqrt 3/2)\<^sup>2"
  1.1354      using pos_c by (simp add: sin_squared_eq power_divide)
  1.1355    thus ?thesis
  1.1356      using pos_c [THEN order_less_imp_le]
  1.1357 @@ -3664,7 +3991,7 @@
  1.1358  lemma sin_45: "sin (pi / 4) = sqrt 2 / 2"
  1.1359    by (simp add: sin_cos_eq cos_45)
  1.1360  
  1.1361 -lemma sin_60: "sin (pi / 3) = sqrt 3 / 2"
  1.1362 +lemma sin_60: "sin (pi / 3) = sqrt 3/2"
  1.1363    by (simp add: sin_cos_eq cos_30)
  1.1364  
  1.1365  lemma cos_60: "cos (pi / 3) = 1 / 2"
  1.1366 @@ -3688,7 +4015,7 @@
  1.1367  lemma sin_cos_npi [simp]: "sin (real (Suc (2 * n)) * pi / 2) = (-1) ^ n"
  1.1368  proof -
  1.1369    have "sin ((real n + 1/2) * pi) = cos (real n * pi)"
  1.1370 -    by (auto simp add: algebra_simps sin_add)
  1.1371 +    by (auto simp: algebra_simps sin_add)
  1.1372    thus ?thesis
  1.1373      by (simp add: real_of_nat_Suc distrib_right add_divide_distrib
  1.1374                    mult.commute [of pi])
  1.1375 @@ -3697,32 +4024,39 @@
  1.1376  lemma cos_2npi [simp]: "cos (2 * real (n::nat) * pi) = 1"
  1.1377    by (cases "even n") (simp_all add: cos_double mult.assoc)
  1.1378  
  1.1379 -lemma cos_3over2_pi [simp]: "cos (3 / 2 * pi) = 0"
  1.1380 +lemma cos_3over2_pi [simp]: "cos (3/2*pi) = 0"
  1.1381    apply (subgoal_tac "cos (pi + pi/2) = 0", simp)
  1.1382    apply (subst cos_add, simp)
  1.1383    done
  1.1384  
  1.1385  lemma sin_2npi [simp]: "sin (2 * real (n::nat) * pi) = 0"
  1.1386 -  by (auto simp add: mult.assoc)
  1.1387 -
  1.1388 -lemma sin_3over2_pi [simp]: "sin (3 / 2 * pi) = - 1"
  1.1389 +  by (auto simp: mult.assoc sin_double)
  1.1390 +
  1.1391 +lemma sin_3over2_pi [simp]: "sin (3/2*pi) = - 1"
  1.1392    apply (subgoal_tac "sin (pi + pi/2) = - 1", simp)
  1.1393    apply (subst sin_add, simp)
  1.1394    done
  1.1395  
  1.1396  lemma cos_pi_eq_zero [simp]: "cos (pi * real (Suc (2 * m)) / 2) = 0"
  1.1397 -  apply (simp only: cos_add sin_add real_of_nat_Suc distrib_right distrib_left add_divide_distrib)
  1.1398 -  apply auto
  1.1399 -  done
  1.1400 +by (simp only: cos_add sin_add real_of_nat_Suc distrib_right distrib_left add_divide_distrib, auto)
  1.1401  
  1.1402  lemma DERIV_cos_add [simp]: "DERIV (\<lambda>x. cos (x + k)) xa :> - sin (xa + k)"
  1.1403    by (auto intro!: derivative_eq_intros)
  1.1404  
  1.1405 -lemma sin_zero_abs_cos_one: "sin x = 0 ==> \<bar>cos x\<bar> = 1"
  1.1406 -  by (auto simp add: sin_zero_iff elim: evenE)
  1.1407 -
  1.1408 -lemma cos_one_sin_zero: "cos x = 1 ==> sin x = 0"
  1.1409 -  using sin_cos_squared_add3 [where x = x] by auto
  1.1410 +lemma sin_zero_norm_cos_one:
  1.1411 +  fixes x :: "'a::{real_normed_field,banach}"
  1.1412 +  assumes "sin x = 0" shows "norm (cos x) = 1"
  1.1413 +  using sin_cos_squared_add [of x, unfolded assms]
  1.1414 +  by (simp add: square_norm_one)
  1.1415 +
  1.1416 +lemma sin_zero_abs_cos_one: "sin x = 0 \<Longrightarrow> \<bar>cos x\<bar> = (1::real)"
  1.1417 +  using sin_zero_norm_cos_one by fastforce
  1.1418 +
  1.1419 +lemma cos_one_sin_zero:
  1.1420 +  fixes x :: "'a::{real_normed_field,banach}"
  1.1421 +  assumes "cos x = 1" shows "sin x = 0"
  1.1422 +  using sin_cos_squared_add [of x, unfolded assms]
  1.1423 +  by simp
  1.1424  
  1.1425  
  1.1426  subsection {* Machins formula *}
  1.1427 @@ -3775,7 +4109,7 @@
  1.1428  qed
  1.1429  
  1.1430  
  1.1431 -subsection {* Introducing the arcus tangens power series *}
  1.1432 +subsection {* Introducing the inverse tangent power series *}
  1.1433  
  1.1434  lemma monoseq_arctan_series:
  1.1435    fixes x :: real
  1.1436 @@ -3852,6 +4186,7 @@
  1.1437    qed
  1.1438  qed
  1.1439  
  1.1440 +text{*FIXME: generalise from the reals via type classes?*}
  1.1441  lemma summable_arctan_series:
  1.1442    fixes x :: real and n :: nat
  1.1443    assumes "\<bar>x\<bar> \<le> 1"
  1.1444 @@ -4249,7 +4584,7 @@
  1.1445  
  1.1446  lemmas sin_arccos_lemma1 = sin_arccos_abs [OF cos_x_y_le_one]
  1.1447  
  1.1448 -lemma polar_Ex: "\<exists>r a. x = r * cos a & y = r * sin a"
  1.1449 +lemma polar_Ex: "\<exists>r::real. \<exists>a. x = r * cos a & y = r * sin a"
  1.1450  proof -
  1.1451    have polar_ex1: "\<And>y. 0 < y \<Longrightarrow> \<exists>r a. x = r * cos a & y = r * sin a"
  1.1452      apply (rule_tac x = "sqrt (x\<^sup>2 + y\<^sup>2)" in exI)