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.45    by (induct n) (auto simp add: real_of_nat_Suc distrib_left exp_add mult.commute)
    1.46 -  
    1.47 +
    1.48  text {* Strict monotonicity of exponential. *}
    1.49  
    1.50 -lemma exp_ge_add_one_self_aux: 
    1.51 +lemma exp_ge_add_one_self_aux:
    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.65      by (simp add: exp_def)
    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.71      by (simp add: exp_def)
    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.223        by (metis div_add power_add le_add_diff_inverse odd_add)
   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.315 -theorem cos_add: 
   1.316 +theorem cos_add:
   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.359 -lemma sin_cos_squared_add [simp]: 
   1.360 +
   1.361 +lemma sin_cos_squared_add [simp]:
   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.367 -lemma sin_cos_squared_add2 [simp]:  
   1.368 +lemma sin_cos_squared_add2 [simp]:
   1.369    fixes x :: "'a::{real_normed_field,banach}"
   1.370    shows "(cos x)\<^sup>2 + (sin x)\<^sup>2 = 1"
   1.371    by (subst add.commute, rule sin_cos_squared_add)
   1.372  
   1.373 -lemma sin_cos_squared_add3 [simp]:  
   1.374 +lemma sin_cos_squared_add3 [simp]:
   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.493 -lemma sin_add: 
   1.494 +lemma sin_add:
   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.508    by (simp add: cos_of_real)
   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.513    by (simp add: sin_of_real)
   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.526      apply (simp add: cos_zero_iff)
   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.544      apply (simp add: sin_zero_iff)
   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.554    apply (simp_all add: field_simps)
   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.568  lemma tan_add:
   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.574        by (simp add: add_tan_eq lemma_tan_add1 field_simps) (simp add: tan_def)
   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.582    using tan_add [of x x] by (simp add: power2_eq_square)
   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