src/HOL/Transcendental.thy
 changeset 59669 de7792ea4090 parent 59658 0cc388370041 child 59688 6c896dfef33b child 59730 b7c394c7a619
```     1.1 --- a/src/HOL/Transcendental.thy	Tue Mar 10 15:21:26 2015 +0000
1.2 +++ b/src/HOL/Transcendental.thy	Tue Mar 10 16:12:35 2015 +0000
1.3 @@ -7,7 +7,7 @@
1.4  section{*Power Series, Transcendental Functions etc.*}
1.5
1.6  theory Transcendental
1.7 -imports Fact Series Deriv NthRoot
1.8 +imports Binomial Series Deriv NthRoot
1.9  begin
1.10
1.11  lemma root_test_convergence:
1.12 @@ -81,13 +81,13 @@
1.13  lemma power_diff_1_eq:
1.14    fixes x :: "'a::{comm_ring,monoid_mult}"
1.15    shows "n \<noteq> 0 \<Longrightarrow> x^n - 1 = (x - 1) * (\<Sum>i<n. (x^i))"
1.16 -using lemma_realpow_diff_sumr2 [of x _ 1]
1.17 +using lemma_realpow_diff_sumr2 [of x _ 1]
1.18    by (cases n) auto
1.19
1.20  lemma one_diff_power_eq':
1.21    fixes x :: "'a::{comm_ring,monoid_mult}"
1.22    shows "n \<noteq> 0 \<Longrightarrow> 1 - x^n = (1 - x) * (\<Sum>i<n. x^(n - Suc i))"
1.23 -using lemma_realpow_diff_sumr2 [of 1 _ x]
1.24 +using lemma_realpow_diff_sumr2 [of 1 _ x]
1.25    by (cases n) auto
1.26
1.27  lemma one_diff_power_eq:
1.28 @@ -419,7 +419,7 @@
1.29        by auto
1.30      ultimately show ?thesis by auto
1.31    qed
1.32 -  then show ?summable and ?pos and ?neg and ?f and ?g
1.33 +  then show ?summable and ?pos and ?neg and ?f and ?g
1.34      by safe
1.35  qed
1.36
1.37 @@ -1171,16 +1171,16 @@
1.38  lemma abs_exp_cancel [simp]: "\<bar>exp x::real\<bar> = exp x"
1.39    by simp
1.40
1.41 -(*FIXME: superseded by exp_of_nat_mult*)
1.42 -lemma exp_real_of_nat_mult: "exp(real n * x) = exp(x) ^ n"
1.43 +(*FIXME: superseded by exp_of_nat_mult*)
1.44 +lemma exp_real_of_nat_mult: "exp(real n * x) = exp(x) ^ n"
1.46 -
1.47 +
1.48  text {* Strict monotonicity of exponential. *}
1.49
1.52    assumes "0 \<le> (x::real)" shows "1+x \<le> exp(x)"
1.53  using order_le_imp_less_or_eq [OF assms]
1.54 -proof
1.55 +proof
1.56    assume "0 < x"
1.57    have "1+x \<le> (\<Sum>n<2. inverse (real (fact n)) * x ^ n)"
1.58      by (auto simp add: numeral_2_eq_2)
1.59 @@ -1189,7 +1189,7 @@
1.60      using `0 < x`
1.61      apply (auto  simp add:  zero_le_mult_iff)
1.62      done
1.63 -  finally show "1+x \<le> exp x"
1.64 +  finally show "1+x \<le> exp x"
1.66  next
1.67    assume "0 = x"
1.68 @@ -1443,7 +1443,7 @@
1.69  proof -
1.70    have "exp x = suminf (\<lambda>n. inverse(fact n) * (x ^ n))"
1.72 -  also from summable_exp have "... = (\<Sum> n. inverse(fact(n+2)) * (x ^ (n+2))) +
1.73 +  also from summable_exp have "... = (\<Sum> n. inverse(fact(n+2)) * (x ^ (n+2))) +
1.74      (\<Sum> n::nat<2. inverse(fact n) * (x ^ n))" (is "_ = _ + ?a")
1.75      by (rule suminf_split_initial_segment)
1.76    also have "?a = 1 + x"
1.77 @@ -1536,7 +1536,7 @@
1.78    ultimately have "1 - x <= 1 / (1 + x + x\<^sup>2)"
1.79      by (elim mult_imp_le_div_pos)
1.80    also have "... <= 1 / exp x"
1.81 -    by (metis a abs_one b exp_bound exp_gt_zero frac_le less_eq_real_def real_sqrt_abs
1.82 +    by (metis a abs_one b exp_bound exp_gt_zero frac_le less_eq_real_def real_sqrt_abs
1.83                real_sqrt_pow2_iff real_sqrt_power)
1.84    also have "... = exp (-x)"
1.85      by (auto simp add: exp_minus divide_inverse)
1.86 @@ -1584,7 +1584,7 @@
1.87    qed
1.88    finally have "exp (x - x\<^sup>2) <= exp (ln (1 + x))" .
1.89    thus ?thesis
1.90 -    by (metis exp_le_cancel_iff)
1.91 +    by (metis exp_le_cancel_iff)
1.92  qed
1.93
1.94  lemma ln_one_minus_pos_lower_bound:
1.95 @@ -1690,7 +1690,7 @@
1.96    also have "... = 1 + (y - x) / x"
1.97      using x a by (simp add: field_simps)
1.98    also have "x * ln(1 + (y - x) / x) <= x * ((y - x) / x)"
1.99 -    using x a
1.100 +    using x a
1.101      by (intro mult_left_mono ln_add_one_self_le_self) simp_all
1.102    also have "... = y - x" using a by simp
1.103    also have "... = (y - x) * ln (exp 1)" by simp
1.104 @@ -2204,7 +2204,7 @@
1.105    unfolding powr_def exp_inj_iff by simp
1.106
1.107  lemma ln_powr_bound: "1 <= x ==> 0 < a ==> ln x <= (x powr a) / a"
1.108 -  by (metis less_eq_real_def ln_less_self mult_imp_le_div_pos ln_powr mult.commute
1.109 +  by (metis less_eq_real_def ln_less_self mult_imp_le_div_pos ln_powr mult.commute
1.110              order.strict_trans2 powr_gt_zero zero_less_one)
1.111
1.112  lemma ln_powr_bound2:
1.113 @@ -2302,7 +2302,7 @@
1.114    have "((\<lambda>y. ln (1 + x * y)::real) has_real_derivative 1 * x) (at 0)"
1.115      by (auto intro!: derivative_eq_intros)
1.116    then have "((\<lambda>y. ln (1 + x * y) / y) ---> x) (at 0)"
1.117 -    by (auto simp add: has_field_derivative_def field_has_derivative_at)
1.118 +    by (auto simp add: has_field_derivative_def field_has_derivative_at)
1.119    then have *: "((\<lambda>y. exp (ln (1 + x * y) / y)) ---> exp x) (at 0)"
1.120      by (rule tendsto_intros)
1.121    then show ?thesis
1.122 @@ -2367,15 +2367,15 @@
1.123    unfolding cos_coeff_def sin_coeff_def
1.124    by (simp del: mult_Suc) (auto elim: oddE)
1.125
1.126 -lemma summable_norm_sin:
1.127 +lemma summable_norm_sin:
1.128    fixes x :: "'a::{real_normed_algebra_1,banach}"
1.129    shows "summable (\<lambda>n. norm (sin_coeff n *\<^sub>R x^n))"
1.130 -  unfolding sin_coeff_def
1.131 +  unfolding sin_coeff_def
1.132    apply (rule summable_comparison_test [OF _ summable_norm_exp [where x=x]])
1.133    apply (auto simp: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
1.134    done
1.135
1.136 -lemma summable_norm_cos:
1.137 +lemma summable_norm_cos:
1.138    fixes x :: "'a::{real_normed_algebra_1,banach}"
1.139    shows "summable (\<lambda>n. norm (cos_coeff n *\<^sub>R x ^ n))"
1.140    unfolding cos_coeff_def
1.141 @@ -2405,7 +2405,7 @@
1.142      by (rule sin_converges)
1.143    finally have "(\<lambda>n. of_real (sin_coeff n *\<^sub>R x^n)) sums (sin (of_real x))" .
1.144    then show ?thesis
1.145 -    using sums_unique2 sums_of_real [OF sin_converges]
1.146 +    using sums_unique2 sums_of_real [OF sin_converges]
1.147      by blast
1.148  qed
1.149
1.150 @@ -2423,7 +2423,7 @@
1.151      by (rule cos_converges)
1.152    finally have "(\<lambda>n. of_real (cos_coeff n *\<^sub>R x^n)) sums (cos (of_real x))" .
1.153    then show ?thesis
1.154 -    using sums_unique2 sums_of_real [OF cos_converges]
1.155 +    using sums_unique2 sums_of_real [OF cos_converges]
1.156      by blast
1.157  qed
1.158
1.159 @@ -2441,22 +2441,22 @@
1.160    unfolding sin_def cos_def scaleR_conv_of_real
1.161    apply (rule DERIV_cong)
1.162    apply (rule termdiffs [where K="of_real (norm x) + 1 :: 'a"])
1.163 -  apply (simp_all add: norm_less_p1 diffs_of_real diffs_sin_coeff diffs_cos_coeff
1.164 +  apply (simp_all add: norm_less_p1 diffs_of_real diffs_sin_coeff diffs_cos_coeff
1.165                summable_minus_iff scaleR_conv_of_real [symmetric]
1.166                summable_norm_sin [THEN summable_norm_cancel]
1.167                summable_norm_cos [THEN summable_norm_cancel])
1.168    done
1.169 -
1.170 +
1.171  declare DERIV_sin[THEN DERIV_chain2, derivative_intros]
1.172
1.173 -lemma DERIV_cos [simp]:
1.174 +lemma DERIV_cos [simp]:
1.175    fixes x :: "'a::{real_normed_field,banach}"
1.176    shows "DERIV cos x :> -sin(x)"
1.177    unfolding sin_def cos_def scaleR_conv_of_real
1.178    apply (rule DERIV_cong)
1.179    apply (rule termdiffs [where K="of_real (norm x) + 1 :: 'a"])
1.180 -  apply (simp_all add: norm_less_p1 diffs_of_real diffs_minus suminf_minus
1.181 -              diffs_sin_coeff diffs_cos_coeff
1.182 +  apply (simp_all add: norm_less_p1 diffs_of_real diffs_minus suminf_minus
1.183 +              diffs_sin_coeff diffs_cos_coeff
1.184                summable_minus_iff scaleR_conv_of_real [symmetric]
1.185                summable_norm_sin [THEN summable_norm_cancel]
1.186                summable_norm_cos [THEN summable_norm_cancel])
1.187 @@ -2469,7 +2469,7 @@
1.188    shows "isCont sin x"
1.189    by (rule DERIV_sin [THEN DERIV_isCont])
1.190
1.191 -lemma isCont_cos:
1.192 +lemma isCont_cos:
1.193    fixes x :: "'a::{real_normed_field,banach}"
1.194    shows "isCont cos x"
1.195    by (rule DERIV_cos [THEN DERIV_isCont])
1.196 @@ -2481,7 +2481,7 @@
1.197
1.198  (*FIXME A CONTEXT FOR F WOULD BE BETTER*)
1.199
1.200 -lemma isCont_cos' [simp]:
1.201 +lemma isCont_cos' [simp]:
1.202    fixes f:: "_ \<Rightarrow> 'a::{real_normed_field,banach}"
1.203    shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. cos (f x)) a"
1.204    by (rule isCont_o2 [OF _ isCont_cos])
1.205 @@ -2545,23 +2545,23 @@
1.206  subsection {*Deriving the Addition Formulas*}
1.207
1.208  text{*The the product of two cosine series*}
1.209 -lemma cos_x_cos_y:
1.210 +lemma cos_x_cos_y:
1.211    fixes x :: "'a::{real_normed_field,banach}"
1.212 -  shows "(\<lambda>p. \<Sum>n\<le>p.
1.213 -          if even p \<and> even n
1.214 -          then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)
1.215 +  shows "(\<lambda>p. \<Sum>n\<le>p.
1.216 +          if even p \<and> even n
1.217 +          then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)
1.218           sums (cos x * cos y)"
1.219  proof -
1.220    { fix n p::nat
1.221      assume "n\<le>p"
1.222      then have *: "even n \<Longrightarrow> even p \<Longrightarrow> (-1) ^ (n div 2) * (-1) ^ ((p - n) div 2) = (-1 :: real) ^ (p div 2)"
1.224 -    have "(cos_coeff n * cos_coeff (p - n)) *\<^sub>R (x^n * y^(p-n)) =
1.225 +    have "(cos_coeff n * cos_coeff (p - n)) *\<^sub>R (x^n * y^(p-n)) =
1.226            (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.227      using `n\<le>p`
1.228        by (auto simp: * algebra_simps cos_coeff_def binomial_fact real_of_nat_def)
1.229 -  }
1.230 -  then have "(\<lambda>p. \<Sum>n\<le>p. if even p \<and> even n
1.231 +  }
1.232 +  then have "(\<lambda>p. \<Sum>n\<le>p. if even p \<and> even n
1.233                    then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0) =
1.234               (\<lambda>p. \<Sum>n\<le>p. (cos_coeff n * cos_coeff (p - n)) *\<^sub>R (x^n * y^(p-n)))"
1.235      by simp
1.236 @@ -2574,11 +2574,11 @@
1.237  qed
1.238
1.239  text{*The product of two sine series*}
1.240 -lemma sin_x_sin_y:
1.241 +lemma sin_x_sin_y:
1.242    fixes x :: "'a::{real_normed_field,banach}"
1.243 -  shows "(\<lambda>p. \<Sum>n\<le>p.
1.244 -          if even p \<and> odd n
1.245 -               then - ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)
1.246 +  shows "(\<lambda>p. \<Sum>n\<le>p.
1.247 +          if even p \<and> odd n
1.248 +               then - ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)
1.249           sums (sin x * sin y)"
1.250  proof -
1.251    { fix n p::nat
1.252 @@ -2594,13 +2594,13 @@
1.253          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.254          done
1.255      } then
1.256 -    have "(sin_coeff n * sin_coeff (p - n)) *\<^sub>R (x^n * y^(p-n)) =
1.257 -          (if even p \<and> odd n
1.258 +    have "(sin_coeff n * sin_coeff (p - n)) *\<^sub>R (x^n * y^(p-n)) =
1.259 +          (if even p \<and> odd n
1.260            then -((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)"
1.261      using `n\<le>p`
1.262        by (auto simp:  algebra_simps sin_coeff_def binomial_fact real_of_nat_def)
1.263 -  }
1.264 -  then have "(\<lambda>p. \<Sum>n\<le>p. if even p \<and> odd n
1.265 +  }
1.266 +  then have "(\<lambda>p. \<Sum>n\<le>p. if even p \<and> odd n
1.267                 then - ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0) =
1.268               (\<lambda>p. \<Sum>n\<le>p. (sin_coeff n * sin_coeff (p - n)) *\<^sub>R (x^n * y^(p-n)))"
1.269      by simp
1.270 @@ -2612,18 +2612,18 @@
1.271    finally show ?thesis .
1.272  qed
1.273
1.274 -lemma sums_cos_x_plus_y:
1.275 +lemma sums_cos_x_plus_y:
1.276    fixes x :: "'a::{real_normed_field,banach}"
1.277    shows
1.278 -  "(\<lambda>p. \<Sum>n\<le>p. if even p
1.279 -               then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n)
1.280 -               else 0)
1.281 +  "(\<lambda>p. \<Sum>n\<le>p. if even p
1.282 +               then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n)
1.283 +               else 0)
1.284          sums cos (x + y)"
1.285  proof -
1.286    { fix p::nat
1.287      have "(\<Sum>n\<le>p. if even p
1.288                    then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n)
1.289 -                  else 0) =
1.290 +                  else 0) =
1.291            (if even p
1.292                    then \<Sum>n\<le>p. ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n)
1.293                    else 0)"
1.294 @@ -2637,11 +2637,11 @@
1.295      finally have "(\<Sum>n\<le>p. if even p
1.296                    then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n)
1.297                    else 0) = cos_coeff p *\<^sub>R ((x + y) ^ p)" .
1.298 -  }
1.299 -  then have "(\<lambda>p. \<Sum>n\<le>p.
1.300 -               if even p
1.301 -               then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n)
1.302 -               else 0)
1.303 +  }
1.304 +  then have "(\<lambda>p. \<Sum>n\<le>p.
1.305 +               if even p
1.306 +               then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n)
1.307 +               else 0)
1.308          = (\<lambda>p. cos_coeff p *\<^sub>R ((x+y)^p))"
1.309          by simp
1.310     also have "... sums cos (x + y)"
1.311 @@ -2649,22 +2649,22 @@
1.312     finally show ?thesis .
1.313  qed
1.314
1.317    fixes x :: "'a::{real_normed_field,banach}"
1.318    shows "cos (x + y) = cos x * cos y - sin x * sin y"
1.319  proof -
1.320    { fix n p::nat
1.321      assume "n\<le>p"
1.322 -    then have "(if even p \<and> even n
1.323 +    then have "(if even p \<and> even n
1.324                 then ((- 1) ^ (p div 2) * int (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0) -
1.325 -          (if even p \<and> odd n
1.326 +          (if even p \<and> odd n
1.327                 then - ((- 1) ^ (p div 2) * int (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)
1.328 -          = (if even p
1.329 +          = (if even p
1.330                 then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)"
1.331        by simp
1.332 -  }
1.333 -  then have "(\<lambda>p. \<Sum>n\<le>p. (if even p
1.334 -               then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0))
1.335 +  }
1.336 +  then have "(\<lambda>p. \<Sum>n\<le>p. (if even p
1.337 +               then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0))
1.338          sums (cos x * cos y - sin x * sin y)"
1.339      using sums_diff [OF cos_x_cos_y [of x y] sin_x_sin_y [of x y]]
1.340      by (simp add: setsum_subtractf [symmetric])
1.341 @@ -2683,7 +2683,7 @@
1.342  lemma sin_minus [simp]:
1.343    fixes x :: "'a::{real_normed_algebra_1,banach}"
1.344    shows "sin (-x) = -sin(x)"
1.345 -using sin_minus_converges [of x]
1.346 +using sin_minus_converges [of x]
1.347  by (auto simp: sin_def summable_norm_sin [THEN summable_norm_cancel] suminf_minus sums_iff equation_minus_iff)
1.348
1.349  lemma cos_minus_converges: "(\<lambda>n. (cos_coeff n *\<^sub>R (-x)^n)) sums cos(x)"
1.350 @@ -2698,72 +2698,72 @@
1.351    fixes x :: "'a::{real_normed_algebra_1,banach}"
1.352    shows "cos (-x) = cos(x)"
1.353  using cos_minus_converges [of x]
1.354 -by (simp add: cos_def summable_norm_cos [THEN summable_norm_cancel]
1.355 +by (simp add: cos_def summable_norm_cos [THEN summable_norm_cancel]
1.356                suminf_minus sums_iff equation_minus_iff)
1.357
1.358 -
1.360 +
1.362    fixes x :: "'a::{real_normed_field,banach}"
1.363    shows "(sin x)\<^sup>2 + (cos x)\<^sup>2 = 1"
1.364  using cos_add [of x "-x"]
1.365  by (simp add: power2_eq_square algebra_simps)
1.366
1.369    fixes x :: "'a::{real_normed_field,banach}"
1.370    shows "(cos x)\<^sup>2 + (sin x)\<^sup>2 = 1"
1.372
1.375    fixes x :: "'a::{real_normed_field,banach}"
1.376    shows "cos x * cos x + sin x * sin x = 1"
1.377    using sin_cos_squared_add2 [unfolded power2_eq_square] .
1.378
1.379 -lemma sin_squared_eq:
1.380 +lemma sin_squared_eq:
1.381    fixes x :: "'a::{real_normed_field,banach}"
1.382    shows "(sin x)\<^sup>2 = 1 - (cos x)\<^sup>2"
1.383    unfolding eq_diff_eq by (rule sin_cos_squared_add)
1.384
1.385 -lemma cos_squared_eq:
1.386 +lemma cos_squared_eq:
1.387    fixes x :: "'a::{real_normed_field,banach}"
1.388    shows "(cos x)\<^sup>2 = 1 - (sin x)\<^sup>2"
1.389    unfolding eq_diff_eq by (rule sin_cos_squared_add2)
1.390
1.391 -lemma abs_sin_le_one [simp]:
1.392 +lemma abs_sin_le_one [simp]:
1.393    fixes x :: real
1.394    shows "\<bar>sin x\<bar> \<le> 1"
1.395    by (rule power2_le_imp_le, simp_all add: sin_squared_eq)
1.396
1.397 -lemma sin_ge_minus_one [simp]:
1.398 +lemma sin_ge_minus_one [simp]:
1.399    fixes x :: real
1.400    shows "-1 \<le> sin x"
1.401    using abs_sin_le_one [of x] unfolding abs_le_iff by simp
1.402
1.403 -lemma sin_le_one [simp]:
1.404 +lemma sin_le_one [simp]:
1.405    fixes x :: real
1.406    shows "sin x \<le> 1"
1.407    using abs_sin_le_one [of x] unfolding abs_le_iff by simp
1.408
1.409 -lemma abs_cos_le_one [simp]:
1.410 +lemma abs_cos_le_one [simp]:
1.411    fixes x :: real
1.412    shows "\<bar>cos x\<bar> \<le> 1"
1.413    by (rule power2_le_imp_le, simp_all add: cos_squared_eq)
1.414
1.415 -lemma cos_ge_minus_one [simp]:
1.416 +lemma cos_ge_minus_one [simp]:
1.417    fixes x :: real
1.418    shows "-1 \<le> cos x"
1.419    using abs_cos_le_one [of x] unfolding abs_le_iff by simp
1.420
1.421 -lemma cos_le_one [simp]:
1.422 +lemma cos_le_one [simp]:
1.423    fixes x :: real
1.424    shows "cos x \<le> 1"
1.425    using abs_cos_le_one [of x] unfolding abs_le_iff by simp
1.426
1.427 -lemma cos_diff:
1.428 +lemma cos_diff:
1.429    fixes x :: "'a::{real_normed_field,banach}"
1.430    shows "cos (x - y) = cos x * cos y + sin x * sin y"
1.431    using cos_add [of x "- y"] by simp
1.432
1.433 -lemma cos_double:
1.434 +lemma cos_double:
1.435    fixes x :: "'a::{real_normed_field,banach}"
1.436    shows "cos(2*x) = (cos x)\<^sup>2 - (sin x)\<^sup>2"
1.437    using cos_add [where x=x and y=x]
1.438 @@ -2786,7 +2786,7 @@
1.439     hence define pi.*}
1.440
1.441  lemma sin_paired:
1.442 -  fixes x :: real
1.443 +  fixes x :: real
1.444    shows "(\<lambda>n. (- 1) ^ n /(real (fact (2 * n + 1))) * x ^ (2 * n + 1)) sums  sin x"
1.445  proof -
1.446    have "(\<lambda>n. \<Sum>k = n*2..<n * 2 + 2. sin_coeff k * x ^ k) sums sin x"
1.447 @@ -2797,7 +2797,7 @@
1.448  qed
1.449
1.450  lemma sin_gt_zero_02:
1.451 -  fixes x :: real
1.452 +  fixes x :: real
1.453    assumes "0 < x" and "x < 2"
1.454    shows "0 < sin x"
1.455  proof -
1.456 @@ -2824,12 +2824,12 @@
1.457  qed
1.458
1.459  lemma cos_double_less_one:
1.460 -  fixes x :: real
1.461 +  fixes x :: real
1.462    shows "0 < x \<Longrightarrow> x < 2 \<Longrightarrow> cos (2 * x) < 1"
1.463    using sin_gt_zero_02 [where x = x] by (auto simp: cos_squared_eq cos_double)
1.464
1.465  lemma cos_paired:
1.466 -  fixes x :: real
1.467 +  fixes x :: real
1.468    shows "(\<lambda>n. (- 1) ^ n /(real (fact (2 * n))) * x ^ (2 * n)) sums cos x"
1.469  proof -
1.470    have "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2. cos_coeff k * x ^ k) sums cos x"
1.471 @@ -2927,7 +2927,7 @@
1.472  lemma cos_pi_half [simp]: "cos (pi / 2) = 0"
1.473    by (simp add: pi_half cos_is_zero [THEN theI'])
1.474
1.475 -lemma cos_of_real_pi_half [simp]:
1.476 +lemma cos_of_real_pi_half [simp]:
1.477    fixes x :: "'a :: {real_field,banach,real_normed_algebra_1}"
1.478    shows "cos ((of_real pi / 2) :: 'a) = 0"
1.479  by (metis cos_pi_half cos_of_real eq_numeral_simps(4) nonzero_of_real_divide of_real_0 of_real_numeral)
1.480 @@ -2976,7 +2976,7 @@
1.481  lemma sin_of_real_pi_half [simp]:
1.482    fixes x :: "'a :: {real_field,banach,real_normed_algebra_1}"
1.483    shows "sin ((of_real pi / 2) :: 'a) = 1"
1.484 -  using sin_pi_half
1.485 +  using sin_pi_half
1.486  by (metis sin_pi_half eq_numeral_simps(4) nonzero_of_real_divide of_real_1 of_real_numeral sin_of_real)
1.487
1.488  lemma sin_cos_eq:
1.489 @@ -2995,7 +2995,7 @@
1.490    using sin_cos_eq [of "of_real pi / 2 - x"]
1.491    by simp
1.492
1.495    fixes x :: "'a::{real_normed_field,banach}"
1.496    shows "sin (x + y) = sin x * cos y + cos x * sin y"
1.497    using cos_add [of "of_real pi / 2 - x" "-y"]
1.498 @@ -3006,7 +3006,7 @@
1.499    shows "sin (x - y) = sin x * cos y - cos x * sin y"
1.500    using sin_add [of x "- y"] by simp
1.501
1.502 -lemma sin_double:
1.503 +lemma sin_double:
1.504    fixes x :: "'a::{real_normed_field,banach}"
1.505    shows "sin(2 * x) = 2 * sin x * cos x"
1.506    using sin_add [where x=x and y=x] by simp
1.507 @@ -3017,9 +3017,9 @@
1.509
1.510  lemma sin_of_real_pi [simp]: "sin (of_real pi) = 0"
1.511 -  using sin_add [where x = "pi/2" and y = "pi/2"]
1.512 +  using sin_add [where x = "pi/2" and y = "pi/2"]
1.514 -
1.515 +
1.516  lemma cos_pi [simp]: "cos pi = -1"
1.517    using cos_add [where x = "pi/2" and y = "pi/2"] by simp
1.518
1.519 @@ -3241,7 +3241,7 @@
1.520      done
1.521  next
1.522    fix n::int
1.523 -  assume "odd n"
1.524 +  assume "odd n"
1.525    then show "cos (real n * (pi / 2)) = 0"
1.527      apply (case_tac n rule: int_cases2, simp)
1.528 @@ -3250,7 +3250,7 @@
1.529      done
1.530  qed
1.531
1.532 -lemma sin_zero_iff_int:
1.533 +lemma sin_zero_iff_int:
1.534       "sin x = 0 \<longleftrightarrow> (\<exists>n::int. even n & (x = real n * (pi/2)))"
1.535  proof safe
1.536    assume "sin x = 0"
1.537 @@ -3261,7 +3261,7 @@
1.538      done
1.539  next
1.540    fix n::int
1.541 -  assume "even n"
1.542 +  assume "even n"
1.543    then show "sin (real n * (pi / 2)) = 0"
1.545      apply (case_tac n rule: int_cases2, simp)
1.546 @@ -3271,8 +3271,8 @@
1.547  qed
1.548
1.549  lemma sin_zero_iff_int2: "sin x = 0 \<longleftrightarrow> (\<exists>n::int. x = real n * pi)"
1.550 -  apply (simp only: sin_zero_iff_int)
1.551 -  apply (safe elim!: evenE)
1.552 +  apply (simp only: sin_zero_iff_int)
1.553 +  apply (safe elim!: evenE)
1.555    using dvd_triv_left by fastforce
1.556
1.557 @@ -3337,7 +3337,7 @@
1.558      using pi_ge_two and assms by auto
1.559    from cos_monotone_0_pi'[OF this] show ?thesis
1.560      unfolding minus_sin_cos_eq[symmetric]
1.561 -    by (metis minus_sin_cos_eq mult.right_neutral neg_le_iff_le of_real_def real_scaleR_def)
1.562 +    by (metis minus_sin_cos_eq mult.right_neutral neg_le_iff_le of_real_def real_scaleR_def)
1.563  qed
1.564
1.565  lemma sin_x_le_x:
1.566 @@ -3401,14 +3401,14 @@
1.567
1.569    fixes x :: "'a::{real_normed_field,banach}"
1.570 -  shows
1.571 +  shows
1.572       "\<lbrakk>cos x \<noteq> 0; cos y \<noteq> 0; cos (x + y) \<noteq> 0\<rbrakk>
1.573        \<Longrightarrow> tan(x + y) = (tan(x) + tan(y))/(1 - tan(x) * tan(y))"
1.575
1.576  lemma tan_double:
1.577    fixes x :: "'a::{real_normed_field,banach}"
1.578 -  shows
1.579 +  shows
1.580       "\<lbrakk>cos x \<noteq> 0; cos (2 * x) \<noteq> 0\<rbrakk>
1.581        \<Longrightarrow> tan (2 * x) = (2 * tan x) / (1 - (tan x)\<^sup>2)"
1.583 @@ -3463,7 +3463,7 @@
1.584
1.585  lemma continuous_within_tan [continuous_intros]:
1.586    fixes f :: "'a \<Rightarrow> 'a::{real_normed_field,banach}"
1.587 -  shows
1.588 +  shows
1.589    "continuous (at x within s) f \<Longrightarrow> cos (f x) \<noteq> 0 \<Longrightarrow> continuous (at x within s) (\<lambda>x. tan (f x))"
1.590    unfolding continuous_within by (rule tendsto_tan)
1.591
1.592 @@ -4200,7 +4200,7 @@
1.593    shows "x\<^sup>2 < 1"
1.594  proof -
1.595    have "\<bar>x\<^sup>2\<bar> < 1"
1.596 -    by (metis abs_power2 assms pos2 power2_abs power_0 power_strict_decreasing zero_eq_power2 zero_less_abs_iff)
1.597 +    by (metis abs_power2 assms pos2 power2_abs power_0 power_strict_decreasing zero_eq_power2 zero_less_abs_iff)
1.598    thus ?thesis using zero_le_power2 by auto
1.599  qed
1.600
1.601 @@ -4594,7 +4594,7 @@
1.602      done
1.603    show ?thesis
1.604    proof (cases "0::real" y rule: linorder_cases)
1.605 -    case less
1.606 +    case less
1.607        then show ?thesis by (rule polar_ex1)
1.608    next
1.609      case equal
1.610 @@ -4602,7 +4602,7 @@
1.611          by (force simp add: intro!: cos_zero sin_zero)
1.612    next
1.613      case greater
1.614 -      then show ?thesis
1.615 +      then show ?thesis
1.616       using polar_ex1 [where y="-y"]
1.617      by auto (metis cos_minus minus_minus minus_mult_right sin_minus)
1.618    qed
```