src/HOL/Transcendental.thy
changeset 59730 b7c394c7a619
parent 59669 de7792ea4090
child 59731 7fccaeec22f0
     1.1 --- a/src/HOL/Transcendental.thy	Tue Mar 10 16:12:35 2015 +0000
     1.2 +++ b/src/HOL/Transcendental.thy	Mon Mar 16 15:30:00 2015 +0000
     1.3 @@ -10,6 +10,12 @@
     1.4  imports Binomial Series Deriv NthRoot
     1.5  begin
     1.6  
     1.7 +lemma of_real_fact [simp]: "of_real (fact n) = fact n"
     1.8 +  by (metis of_nat_fact of_real_of_nat_eq)
     1.9 +
    1.10 +lemma real_fact_nat [simp]: "real (fact n :: nat) = fact n"
    1.11 +  by (simp add: real_of_nat_def)
    1.12 +
    1.13  lemma root_test_convergence:
    1.14    fixes f :: "nat \<Rightarrow> 'a::banach"
    1.15    assumes f: "(\<lambda>n. root n (norm (f n))) ----> x" -- "could be weakened to lim sup"
    1.16 @@ -54,13 +60,13 @@
    1.17        (x - y) * (\<Sum>p<Suc n. (x ^ p) * y ^ (n - p))"
    1.18  proof (induct n)
    1.19    case (Suc n)
    1.20 -  have "x ^ Suc (Suc n) - y ^ Suc (Suc n) = x * (x * x ^ n) - y * (y * y ^ n)"
    1.21 +  have "x ^ Suc (Suc n) - y ^ Suc (Suc n) = x * (x * x^n) - y * (y * y ^ n)"
    1.22      by simp
    1.23 -  also have "... = y * (x ^ (Suc n) - y ^ (Suc n)) + (x - y) * (x * x ^ n)"
    1.24 +  also have "... = y * (x ^ (Suc n) - y ^ (Suc n)) + (x - y) * (x * x^n)"
    1.25      by (simp add: algebra_simps)
    1.26 -  also have "... = y * ((x - y) * (\<Sum>p<Suc n. (x ^ p) * y ^ (n - p))) + (x - y) * (x * x ^ n)"
    1.27 +  also have "... = y * ((x - y) * (\<Sum>p<Suc n. (x ^ p) * y ^ (n - p))) + (x - y) * (x * x^n)"
    1.28      by (simp only: Suc)
    1.29 -  also have "... = (x - y) * (y * (\<Sum>p<Suc n. (x ^ p) * y ^ (n - p))) + (x - y) * (x * x ^ n)"
    1.30 +  also have "... = (x - y) * (y * (\<Sum>p<Suc n. (x ^ p) * y ^ (n - p))) + (x - y) * (x * x^n)"
    1.31      by (simp only: mult.left_commute)
    1.32    also have "... = (x - y) * (\<Sum>p<Suc (Suc n). x ^ p * y ^ (Suc n - p))"
    1.33      by (simp add: field_simps Suc_diff_le setsum_left_distrib setsum_right_distrib)
    1.34 @@ -100,40 +106,40 @@
    1.35  
    1.36  lemma powser_insidea:
    1.37    fixes x z :: "'a::real_normed_div_algebra"
    1.38 -  assumes 1: "summable (\<lambda>n. f n * x ^ n)"
    1.39 +  assumes 1: "summable (\<lambda>n. f n * x^n)"
    1.40      and 2: "norm z < norm x"
    1.41    shows "summable (\<lambda>n. norm (f n * z ^ n))"
    1.42  proof -
    1.43    from 2 have x_neq_0: "x \<noteq> 0" by clarsimp
    1.44 -  from 1 have "(\<lambda>n. f n * x ^ n) ----> 0"
    1.45 +  from 1 have "(\<lambda>n. f n * x^n) ----> 0"
    1.46      by (rule summable_LIMSEQ_zero)
    1.47 -  hence "convergent (\<lambda>n. f n * x ^ n)"
    1.48 +  hence "convergent (\<lambda>n. f n * x^n)"
    1.49      by (rule convergentI)
    1.50 -  hence "Cauchy (\<lambda>n. f n * x ^ n)"
    1.51 +  hence "Cauchy (\<lambda>n. f n * x^n)"
    1.52      by (rule convergent_Cauchy)
    1.53 -  hence "Bseq (\<lambda>n. f n * x ^ n)"
    1.54 +  hence "Bseq (\<lambda>n. f n * x^n)"
    1.55      by (rule Cauchy_Bseq)
    1.56 -  then obtain K where 3: "0 < K" and 4: "\<forall>n. norm (f n * x ^ n) \<le> K"
    1.57 +  then obtain K where 3: "0 < K" and 4: "\<forall>n. norm (f n * x^n) \<le> K"
    1.58      by (simp add: Bseq_def, safe)
    1.59    have "\<exists>N. \<forall>n\<ge>N. norm (norm (f n * z ^ n)) \<le>
    1.60 -                   K * norm (z ^ n) * inverse (norm (x ^ n))"
    1.61 +                   K * norm (z ^ n) * inverse (norm (x^n))"
    1.62    proof (intro exI allI impI)
    1.63      fix n::nat
    1.64      assume "0 \<le> n"
    1.65 -    have "norm (norm (f n * z ^ n)) * norm (x ^ n) =
    1.66 -          norm (f n * x ^ n) * norm (z ^ n)"
    1.67 +    have "norm (norm (f n * z ^ n)) * norm (x^n) =
    1.68 +          norm (f n * x^n) * norm (z ^ n)"
    1.69        by (simp add: norm_mult abs_mult)
    1.70      also have "\<dots> \<le> K * norm (z ^ n)"
    1.71        by (simp only: mult_right_mono 4 norm_ge_zero)
    1.72 -    also have "\<dots> = K * norm (z ^ n) * (inverse (norm (x ^ n)) * norm (x ^ n))"
    1.73 +    also have "\<dots> = K * norm (z ^ n) * (inverse (norm (x^n)) * norm (x^n))"
    1.74        by (simp add: x_neq_0)
    1.75 -    also have "\<dots> = K * norm (z ^ n) * inverse (norm (x ^ n)) * norm (x ^ n)"
    1.76 +    also have "\<dots> = K * norm (z ^ n) * inverse (norm (x^n)) * norm (x^n)"
    1.77        by (simp only: mult.assoc)
    1.78      finally show "norm (norm (f n * z ^ n)) \<le>
    1.79 -                  K * norm (z ^ n) * inverse (norm (x ^ n))"
    1.80 +                  K * norm (z ^ n) * inverse (norm (x^n))"
    1.81        by (simp add: mult_le_cancel_right x_neq_0)
    1.82    qed
    1.83 -  moreover have "summable (\<lambda>n. K * norm (z ^ n) * inverse (norm (x ^ n)))"
    1.84 +  moreover have "summable (\<lambda>n. K * norm (z ^ n) * inverse (norm (x^n)))"
    1.85    proof -
    1.86      from 2 have "norm (norm (z * inverse x)) < 1"
    1.87        using x_neq_0
    1.88 @@ -142,7 +148,7 @@
    1.89        by (rule summable_geometric)
    1.90      hence "summable (\<lambda>n. K * norm (z * inverse x) ^ n)"
    1.91        by (rule summable_mult)
    1.92 -    thus "summable (\<lambda>n. K * norm (z ^ n) * inverse (norm (x ^ n)))"
    1.93 +    thus "summable (\<lambda>n. K * norm (z ^ n) * inverse (norm (x^n)))"
    1.94        using x_neq_0
    1.95        by (simp add: norm_mult nonzero_norm_inverse power_mult_distrib
    1.96                      power_inverse norm_power mult.assoc)
    1.97 @@ -154,7 +160,7 @@
    1.98  lemma powser_inside:
    1.99    fixes f :: "nat \<Rightarrow> 'a::{real_normed_div_algebra,banach}"
   1.100    shows
   1.101 -    "summable (\<lambda>n. f n * (x ^ n)) \<Longrightarrow> norm z < norm x \<Longrightarrow>
   1.102 +    "summable (\<lambda>n. f n * (x^n)) \<Longrightarrow> norm z < norm x \<Longrightarrow>
   1.103        summable (\<lambda>n. f n * (z ^ n))"
   1.104    by (rule powser_insidea [THEN summable_norm_cancel])
   1.105  
   1.106 @@ -581,7 +587,7 @@
   1.107    fixes x :: "'a::{real_normed_field,banach}"
   1.108    assumes 1: "summable (\<lambda>n. diffs (diffs c) n * K ^ n)"
   1.109      and 2: "norm x < norm K"
   1.110 -  shows "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n - x ^ n) / h
   1.111 +  shows "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n - x^n) / h
   1.112               - of_nat n * x ^ (n - Suc 0))) -- 0 --> 0"
   1.113  proof -
   1.114    from dense [OF 2]
   1.115 @@ -629,7 +635,7 @@
   1.116      hence "norm x + norm h < r" by simp
   1.117      with norm_triangle_ineq have xh: "norm (x + h) < r"
   1.118        by (rule order_le_less_trans)
   1.119 -    show "norm (c n * (((x + h) ^ n - x ^ n) / h - of_nat n * x ^ (n - Suc 0)))
   1.120 +    show "norm (c n * (((x + h) ^ n - x^n) / h - of_nat n * x ^ (n - Suc 0)))
   1.121            \<le> norm (c n) * of_nat n * of_nat (n - Suc 0) * r ^ (n - 2) * norm h"
   1.122        apply (simp only: norm_mult mult.assoc)
   1.123        apply (rule mult_left_mono [OF _ norm_ge_zero])
   1.124 @@ -645,11 +651,11 @@
   1.125        and 2: "summable (\<lambda>n. (diffs c) n * K ^ n)"
   1.126        and 3: "summable (\<lambda>n. (diffs (diffs c)) n * K ^ n)"
   1.127        and 4: "norm x < norm K"
   1.128 -  shows "DERIV (\<lambda>x. \<Sum>n. c n * x ^ n) x :> (\<Sum>n. (diffs c) n * x ^ n)"
   1.129 +  shows "DERIV (\<lambda>x. \<Sum>n. c n * x^n) x :> (\<Sum>n. (diffs c) n * x^n)"
   1.130    unfolding DERIV_def
   1.131  proof (rule LIM_zero_cancel)
   1.132 -  show "(\<lambda>h. (suminf (\<lambda>n. c n * (x + h) ^ n) - suminf (\<lambda>n. c n * x ^ n)) / h
   1.133 -            - suminf (\<lambda>n. diffs c n * x ^ n)) -- 0 --> 0"
   1.134 +  show "(\<lambda>h. (suminf (\<lambda>n. c n * (x + h) ^ n) - suminf (\<lambda>n. c n * x^n)) / h
   1.135 +            - suminf (\<lambda>n. diffs c n * x^n)) -- 0 --> 0"
   1.136    proof (rule LIM_equal2)
   1.137      show "0 < norm K - norm x" using 4 by (simp add: less_diff_eq)
   1.138    next
   1.139 @@ -658,18 +664,18 @@
   1.140      hence "norm x + norm h < norm K" by simp
   1.141      hence 5: "norm (x + h) < norm K"
   1.142        by (rule norm_triangle_ineq [THEN order_le_less_trans])
   1.143 -    have "summable (\<lambda>n. c n * x ^ n)"
   1.144 +    have "summable (\<lambda>n. c n * x^n)"
   1.145        and "summable (\<lambda>n. c n * (x + h) ^ n)"
   1.146 -      and "summable (\<lambda>n. diffs c n * x ^ n)"
   1.147 +      and "summable (\<lambda>n. diffs c n * x^n)"
   1.148        using 1 2 4 5 by (auto elim: powser_inside)
   1.149 -    then have "((\<Sum>n. c n * (x + h) ^ n) - (\<Sum>n. c n * x ^ n)) / h - (\<Sum>n. diffs c n * x ^ n) =
   1.150 -          (\<Sum>n. (c n * (x + h) ^ n - c n * x ^ n) / h - of_nat n * c n * x ^ (n - Suc 0))"
   1.151 +    then have "((\<Sum>n. c n * (x + h) ^ n) - (\<Sum>n. c n * x^n)) / h - (\<Sum>n. diffs c n * x^n) =
   1.152 +          (\<Sum>n. (c n * (x + h) ^ n - c n * x^n) / h - of_nat n * c n * x ^ (n - Suc 0))"
   1.153        by (intro sums_unique sums_diff sums_divide diffs_equiv summable_sums)
   1.154 -    then show "((\<Sum>n. c n * (x + h) ^ n) - (\<Sum>n. c n * x ^ n)) / h - (\<Sum>n. diffs c n * x ^ n) =
   1.155 -          (\<Sum>n. c n * (((x + h) ^ n - x ^ n) / h - of_nat n * x ^ (n - Suc 0)))"
   1.156 +    then show "((\<Sum>n. c n * (x + h) ^ n) - (\<Sum>n. c n * x^n)) / h - (\<Sum>n. diffs c n * x^n) =
   1.157 +          (\<Sum>n. c n * (((x + h) ^ n - x^n) / h - of_nat n * x ^ (n - Suc 0)))"
   1.158        by (simp add: algebra_simps)
   1.159    next
   1.160 -    show "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n - x ^ n) / h - of_nat n * x ^ (n - Suc 0))) -- 0 --> 0"
   1.161 +    show "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n - x^n) / h - of_nat n * x ^ (n - Suc 0))) -- 0 --> 0"
   1.162        by (rule termdiffs_aux [OF 3 4])
   1.163    qed
   1.164  qed
   1.165 @@ -889,7 +895,7 @@
   1.166            fix n
   1.167            have le: "\<bar>f n\<bar> * 1 \<le> \<bar>f n\<bar> * real (Suc n)"
   1.168              by (rule mult_left_mono) auto
   1.169 -          show "norm (f n * x ^ n) \<le> norm (f n * real (Suc n) * x ^ n)"
   1.170 +          show "norm (f n * x^n) \<le> norm (f n * real (Suc n) * x^n)"
   1.171              unfolding real_norm_def abs_mult
   1.172              by (rule mult_right_mono) (auto simp add: le[unfolded mult_1_right])
   1.173          qed (rule powser_insidea[OF converges[OF `R' \<in> {-R <..< R}`] `norm x < norm R'`])
   1.174 @@ -925,14 +931,14 @@
   1.175  subsection {* Exponential Function *}
   1.176  
   1.177  definition exp :: "'a \<Rightarrow> 'a::{real_normed_algebra_1,banach}"
   1.178 -  where "exp = (\<lambda>x. \<Sum>n. x ^ n /\<^sub>R real (fact n))"
   1.179 +  where "exp = (\<lambda>x. \<Sum>n. x^n /\<^sub>R fact n)"
   1.180  
   1.181  lemma summable_exp_generic:
   1.182    fixes x :: "'a::{real_normed_algebra_1,banach}"
   1.183 -  defines S_def: "S \<equiv> \<lambda>n. x ^ n /\<^sub>R real (fact n)"
   1.184 +  defines S_def: "S \<equiv> \<lambda>n. x^n /\<^sub>R fact n"
   1.185    shows "summable S"
   1.186  proof -
   1.187 -  have S_Suc: "\<And>n. S (Suc n) = (x * S n) /\<^sub>R real (Suc n)"
   1.188 +  have S_Suc: "\<And>n. S (Suc n) = (x * S n) /\<^sub>R (Suc n)"
   1.189      unfolding S_def by (simp del: mult_Suc)
   1.190    obtain r :: real where r0: "0 < r" and r1: "r < 1"
   1.191      using dense [OF zero_less_one] by fast
   1.192 @@ -959,26 +965,29 @@
   1.193  
   1.194  lemma summable_norm_exp:
   1.195    fixes x :: "'a::{real_normed_algebra_1,banach}"
   1.196 -  shows "summable (\<lambda>n. norm (x ^ n /\<^sub>R real (fact n)))"
   1.197 +  shows "summable (\<lambda>n. norm (x^n /\<^sub>R fact n))"
   1.198  proof (rule summable_norm_comparison_test [OF exI, rule_format])
   1.199 -  show "summable (\<lambda>n. norm x ^ n /\<^sub>R real (fact n))"
   1.200 +  show "summable (\<lambda>n. norm x^n /\<^sub>R fact n)"
   1.201      by (rule summable_exp_generic)
   1.202    fix n
   1.203 -  show "norm (x ^ n /\<^sub>R real (fact n)) \<le> norm x ^ n /\<^sub>R real (fact n)"
   1.204 +  show "norm (x^n /\<^sub>R fact n) \<le> norm x^n /\<^sub>R fact n"
   1.205      by (simp add: norm_power_ineq)
   1.206  qed
   1.207  
   1.208 -lemma summable_exp: "summable (\<lambda>n. inverse (real (fact n)) * x ^ n)"
   1.209 -  using summable_exp_generic [where x=x] by simp
   1.210 -
   1.211 -lemma exp_converges: "(\<lambda>n. x ^ n /\<^sub>R real (fact n)) sums exp x"
   1.212 +lemma summable_exp: 
   1.213 +  fixes x :: "'a::{real_normed_field,banach}"
   1.214 +  shows "summable (\<lambda>n. inverse (fact n) * x^n)"
   1.215 +  using summable_exp_generic [where x=x]
   1.216 +  by (simp add: scaleR_conv_of_real nonzero_of_real_inverse)
   1.217 +
   1.218 +lemma exp_converges: "(\<lambda>n. x^n /\<^sub>R fact n) sums exp x"
   1.219    unfolding exp_def by (rule summable_exp_generic [THEN summable_sums])
   1.220  
   1.221 -
   1.222  lemma exp_fdiffs:
   1.223 -      "diffs (\<lambda>n. inverse(real (fact n))) = (\<lambda>n. inverse(real (fact n)))"
   1.224 -  by (simp add: diffs_def mult.assoc [symmetric] real_of_nat_def of_nat_mult
   1.225 -        del: mult_Suc of_nat_Suc)
   1.226 +  fixes XXX :: "'a::{real_normed_field,banach}"
   1.227 +  shows "diffs (\<lambda>n. inverse (fact n)) = (\<lambda>n. inverse (fact n :: 'a))"
   1.228 +  by (simp add: diffs_def mult_ac nonzero_inverse_mult_distrib nonzero_of_real_inverse
   1.229 +           del: mult_Suc of_nat_Suc)
   1.230  
   1.231  lemma diffs_of_real: "diffs (\<lambda>n. of_real (f n)) = (\<lambda>n. of_real (diffs f n))"
   1.232    by (simp add: diffs_def)
   1.233 @@ -997,7 +1006,7 @@
   1.234  lemma norm_exp: "norm (exp x) \<le> exp (norm x)"
   1.235  proof -
   1.236    from summable_norm[OF summable_norm_exp, of x]
   1.237 -  have "norm (exp x) \<le> (\<Sum>n. inverse (real (fact n)) * norm (x ^ n))"
   1.238 +  have "norm (exp x) \<le> (\<Sum>n. inverse (fact n) * norm (x^n))"
   1.239      by (simp add: exp_def)
   1.240    also have "\<dots> \<le> exp (norm x)"
   1.241      using summable_exp_generic[of "norm x"] summable_norm_exp[of x]
   1.242 @@ -1047,7 +1056,7 @@
   1.243  
   1.244  lemma exp_series_add_commuting:
   1.245    fixes x y :: "'a::{real_normed_algebra_1, banach}"
   1.246 -  defines S_def: "S \<equiv> \<lambda>x n. x ^ n /\<^sub>R real (fact n)"
   1.247 +  defines S_def: "S \<equiv> \<lambda>x n. x^n /\<^sub>R fact n"
   1.248    assumes comm: "x * y = y * x"
   1.249    shows "S (x + y) n = (\<Sum>i\<le>n. S x i * S y (n - i))"
   1.250  proof (induct n)
   1.251 @@ -1182,9 +1191,9 @@
   1.252  using order_le_imp_less_or_eq [OF assms]
   1.253  proof
   1.254    assume "0 < x"
   1.255 -  have "1+x \<le> (\<Sum>n<2. inverse (real (fact n)) * x ^ n)"
   1.256 +  have "1+x \<le> (\<Sum>n<2. inverse (fact n) * x^n)"
   1.257      by (auto simp add: numeral_2_eq_2)
   1.258 -  also have "... \<le> (\<Sum>n. inverse (real (fact n)) * x ^ n)"
   1.259 +  also have "... \<le> (\<Sum>n. inverse (fact n) * x^n)"
   1.260      apply (rule setsum_le_suminf [OF summable_exp])
   1.261      using `0 < x`
   1.262      apply (auto  simp add:  zero_le_mult_iff)
   1.263 @@ -1297,7 +1306,7 @@
   1.264  lemma ln_div: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln (x / y) = ln x - ln y"
   1.265    by (rule ln_unique) (simp add: exp_diff)
   1.266  
   1.267 -lemma ln_realpow: "0 < x \<Longrightarrow> ln (x ^ n) = real n * ln x"
   1.268 +lemma ln_realpow: "0 < x \<Longrightarrow> ln (x^n) = real n * ln x"
   1.269    by (rule ln_unique) (simp add: exp_real_of_nat_mult)
   1.270  
   1.271  lemma ln_less_cancel_iff [simp]: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln x < ln y \<longleftrightarrow> x < y"
   1.272 @@ -1424,7 +1433,7 @@
   1.273        fix x :: real
   1.274        assume "x \<in> {- 1<..<1}"
   1.275        hence "norm (-x) < 1" by auto
   1.276 -      show "summable (\<lambda>n. (- 1) ^ n * (1 / real (n + 1)) * real (Suc n) * x ^ n)"
   1.277 +      show "summable (\<lambda>n. (- 1) ^ n * (1 / real (n + 1)) * real (Suc n) * x^n)"
   1.278          unfolding One_nat_def
   1.279          by (auto simp add: power_mult_distrib[symmetric] summable_geometric[OF `norm (-x) < 1`])
   1.280      qed
   1.281 @@ -1439,12 +1448,14 @@
   1.282    thus ?thesis by auto
   1.283  qed
   1.284  
   1.285 -lemma exp_first_two_terms: "exp x = 1 + x + (\<Sum> n. inverse(fact (n+2)) * (x ^ (n+2)))"
   1.286 +lemma exp_first_two_terms:
   1.287 +  fixes x :: "'a::{real_normed_field,banach}"
   1.288 +  shows "exp x = 1 + x + (\<Sum> n. inverse(fact (n+2)) * (x ^ (n+2)))"
   1.289  proof -
   1.290 -  have "exp x = suminf (\<lambda>n. inverse(fact n) * (x ^ n))"
   1.291 -    by (simp add: exp_def)
   1.292 +  have "exp x = suminf (\<lambda>n. inverse(fact n) * (x^n))"
   1.293 +    by (simp add: exp_def scaleR_conv_of_real nonzero_of_real_inverse)
   1.294    also from summable_exp have "... = (\<Sum> n. inverse(fact(n+2)) * (x ^ (n+2))) +
   1.295 -    (\<Sum> n::nat<2. inverse(fact n) * (x ^ n))" (is "_ = _ + ?a")
   1.296 +    (\<Sum> n::nat<2. inverse(fact n) * (x^n))" (is "_ = _ + ?a")
   1.297      by (rule suminf_split_initial_segment)
   1.298    also have "?a = 1 + x"
   1.299      by (simp add: numeral_2_eq_2)
   1.300 @@ -1458,21 +1469,22 @@
   1.301    assume b: "x <= 1"
   1.302    {
   1.303      fix n :: nat
   1.304 -    have "2 * 2 ^ n \<le> fact (n + 2)"
   1.305 +    have "(2::nat) * 2 ^ n \<le> fact (n + 2)"
   1.306        by (induct n) simp_all
   1.307 -    hence "real ((2::nat) * 2 ^ n) \<le> real (fact (n + 2))"
   1.308 +    hence "real ((2::nat) * 2 ^ n) \<le> real_of_nat (fact (n + 2))"
   1.309        by (simp only: real_of_nat_le_iff)
   1.310 -    hence "2 * 2 ^ n \<le> real (fact (n + 2))"
   1.311 -      by simp
   1.312 -    hence "inverse (fact (n + 2)) \<le> inverse (2 * 2 ^ n)"
   1.313 +    hence "((2::real) * 2 ^ n) \<le> fact (n + 2)"
   1.314 +      unfolding of_nat_fact real_of_nat_def
   1.315 +      by (simp add: of_nat_mult of_nat_power)
   1.316 +    hence "inverse (fact (n + 2)) \<le> inverse ((2::real) * 2 ^ n)"
   1.317        by (rule le_imp_inverse_le) simp
   1.318 -    hence "inverse (fact (n + 2)) \<le> 1/2 * (1/2)^n"
   1.319 +    hence "inverse (fact (n + 2)) \<le> 1/(2::real) * (1/2)^n"
   1.320        by (simp add: power_inverse)
   1.321      hence "inverse (fact (n + 2)) * (x^n * x\<^sup>2) \<le> 1/2 * (1/2)^n * (1 * x\<^sup>2)"
   1.322        by (rule mult_mono)
   1.323          (rule mult_mono, simp_all add: power_le_one a b)
   1.324      hence "inverse (fact (n + 2)) * x ^ (n + 2) \<le> (x\<^sup>2/2) * ((1/2)^n)"
   1.325 -      unfolding power_add by (simp add: ac_simps del: fact_Suc) }
   1.326 +      unfolding power_add by (simp add: ac_simps del: fact.simps) }
   1.327    note aux1 = this
   1.328    have "(\<lambda>n. x\<^sup>2 / 2 * (1 / 2) ^ n) sums (x\<^sup>2 / 2 * (1 / (1 - 1 / 2)))"
   1.329      by (intro sums_mult geometric_sums, simp)
   1.330 @@ -2140,7 +2152,7 @@
   1.331  lemma log_powr: "log b (x powr y) = y * log b x"
   1.332    by (simp add: log_def ln_powr)
   1.333  
   1.334 -lemma log_nat_power: "0 < x \<Longrightarrow> log b (x ^ n) = real n * log b x"
   1.335 +lemma log_nat_power: "0 < x \<Longrightarrow> log b (x^n) = real n * log b x"
   1.336    by (simp add: log_powr powr_realpow [symmetric])
   1.337  
   1.338  lemma log_base_change: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> log b x = log a x / log a b"
   1.339 @@ -2342,10 +2354,10 @@
   1.340  subsection {* Sine and Cosine *}
   1.341  
   1.342  definition sin_coeff :: "nat \<Rightarrow> real" where
   1.343 -  "sin_coeff = (\<lambda>n. if even n then 0 else (- 1) ^ ((n - Suc 0) div 2) / real (fact n))"
   1.344 +  "sin_coeff = (\<lambda>n. if even n then 0 else (- 1) ^ ((n - Suc 0) div 2) / (fact n))"
   1.345  
   1.346  definition cos_coeff :: "nat \<Rightarrow> real" where
   1.347 -  "cos_coeff = (\<lambda>n. if even n then ((- 1) ^ (n div 2)) / real (fact n) else 0)"
   1.348 +  "cos_coeff = (\<lambda>n. if even n then ((- 1) ^ (n div 2)) / (fact n) else 0)"
   1.349  
   1.350  definition sin :: "'a \<Rightarrow> 'a::{real_normed_algebra_1,banach}"
   1.351    where "sin = (\<lambda>x. \<Sum>n. sin_coeff n *\<^sub>R x^n)"
   1.352 @@ -2377,7 +2389,7 @@
   1.353  
   1.354  lemma summable_norm_cos:
   1.355    fixes x :: "'a::{real_normed_algebra_1,banach}"
   1.356 -  shows "summable (\<lambda>n. norm (cos_coeff n *\<^sub>R x ^ n))"
   1.357 +  shows "summable (\<lambda>n. norm (cos_coeff n *\<^sub>R x^n))"
   1.358    unfolding cos_coeff_def
   1.359    apply (rule summable_comparison_test [OF _ summable_norm_exp [where x=x]])
   1.360    apply (auto simp: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
   1.361 @@ -2398,7 +2410,7 @@
   1.362    have "(\<lambda>n. of_real (sin_coeff n *\<^sub>R  x^n)) = (\<lambda>n. sin_coeff n *\<^sub>R  (of_real x)^n)"
   1.363    proof
   1.364      fix n
   1.365 -    show "of_real (sin_coeff n *\<^sub>R  x ^ n) = sin_coeff n *\<^sub>R of_real x ^ n"
   1.366 +    show "of_real (sin_coeff n *\<^sub>R  x^n) = sin_coeff n *\<^sub>R of_real x^n"
   1.367        by (simp add: scaleR_conv_of_real)
   1.368    qed
   1.369    also have "... sums (sin (of_real x))"
   1.370 @@ -2416,7 +2428,7 @@
   1.371    have "(\<lambda>n. of_real (cos_coeff n *\<^sub>R  x^n)) = (\<lambda>n. cos_coeff n *\<^sub>R  (of_real x)^n)"
   1.372    proof
   1.373      fix n
   1.374 -    show "of_real (cos_coeff n *\<^sub>R  x ^ n) = cos_coeff n *\<^sub>R of_real x ^ n"
   1.375 +    show "of_real (cos_coeff n *\<^sub>R  x^n) = cos_coeff n *\<^sub>R of_real x^n"
   1.376        by (simp add: scaleR_conv_of_real)
   1.377    qed
   1.378    also have "... sums (cos (of_real x))"
   1.379 @@ -2549,7 +2561,7 @@
   1.380    fixes x :: "'a::{real_normed_field,banach}"
   1.381    shows "(\<lambda>p. \<Sum>n\<le>p.
   1.382            if even p \<and> even n
   1.383 -          then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)
   1.384 +          then ((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)
   1.385           sums (cos x * cos y)"
   1.386  proof -
   1.387    { fix n p::nat
   1.388 @@ -2557,12 +2569,12 @@
   1.389      then have *: "even n \<Longrightarrow> even p \<Longrightarrow> (-1) ^ (n div 2) * (-1) ^ ((p - n) div 2) = (-1 :: real) ^ (p div 2)"
   1.390        by (metis div_add power_add le_add_diff_inverse odd_add)
   1.391      have "(cos_coeff n * cos_coeff (p - n)) *\<^sub>R (x^n * y^(p-n)) =
   1.392 -          (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.393 +          (if even p \<and> even n then ((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)"
   1.394      using `n\<le>p`
   1.395        by (auto simp: * algebra_simps cos_coeff_def binomial_fact real_of_nat_def)
   1.396    }
   1.397    then have "(\<lambda>p. \<Sum>n\<le>p. if even p \<and> even n
   1.398 -                  then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0) =
   1.399 +                  then ((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0) =
   1.400               (\<lambda>p. \<Sum>n\<le>p. (cos_coeff n * cos_coeff (p - n)) *\<^sub>R (x^n * y^(p-n)))"
   1.401      by simp
   1.402    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.403 @@ -2578,7 +2590,7 @@
   1.404    fixes x :: "'a::{real_normed_field,banach}"
   1.405    shows "(\<lambda>p. \<Sum>n\<le>p.
   1.406            if even p \<and> odd n
   1.407 -               then - ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)
   1.408 +               then - ((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)
   1.409           sums (sin x * sin y)"
   1.410  proof -
   1.411    { fix n p::nat
   1.412 @@ -2596,12 +2608,12 @@
   1.413      } then
   1.414      have "(sin_coeff n * sin_coeff (p - n)) *\<^sub>R (x^n * y^(p-n)) =
   1.415            (if even p \<and> odd n
   1.416 -          then -((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)"
   1.417 +          then -((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)"
   1.418      using `n\<le>p`
   1.419        by (auto simp:  algebra_simps sin_coeff_def binomial_fact real_of_nat_def)
   1.420    }
   1.421    then have "(\<lambda>p. \<Sum>n\<le>p. if even p \<and> odd n
   1.422 -               then - ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0) =
   1.423 +               then - ((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0) =
   1.424               (\<lambda>p. \<Sum>n\<le>p. (sin_coeff n * sin_coeff (p - n)) *\<^sub>R (x^n * y^(p-n)))"
   1.425      by simp
   1.426    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.427 @@ -2616,31 +2628,31 @@
   1.428    fixes x :: "'a::{real_normed_field,banach}"
   1.429    shows
   1.430    "(\<lambda>p. \<Sum>n\<le>p. if even p
   1.431 -               then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n)
   1.432 +               then ((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n)
   1.433                 else 0)
   1.434          sums cos (x + y)"
   1.435  proof -
   1.436    { fix p::nat
   1.437      have "(\<Sum>n\<le>p. if even p
   1.438 -                  then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n)
   1.439 +                  then ((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n)
   1.440                    else 0) =
   1.441            (if even p
   1.442 -                  then \<Sum>n\<le>p. ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n)
   1.443 +                  then \<Sum>n\<le>p. ((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n)
   1.444                    else 0)"
   1.445        by simp
   1.446      also have "... = (if even p
   1.447 -                  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.448 +                  then of_real ((-1) ^ (p div 2) / (fact p)) * (\<Sum>n\<le>p. (p choose n) *\<^sub>R (x^n) * y^(p-n))
   1.449                    else 0)"
   1.450        by (auto simp: setsum_right_distrib field_simps scaleR_conv_of_real nonzero_of_real_divide)
   1.451      also have "... = cos_coeff p *\<^sub>R ((x + y) ^ p)"
   1.452        by (simp add: cos_coeff_def binomial_ring [of x y]  scaleR_conv_of_real real_of_nat_def atLeast0AtMost)
   1.453      finally have "(\<Sum>n\<le>p. if even p
   1.454 -                  then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n)
   1.455 +                  then ((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n)
   1.456                    else 0) = cos_coeff p *\<^sub>R ((x + y) ^ p)" .
   1.457    }
   1.458    then have "(\<lambda>p. \<Sum>n\<le>p.
   1.459                 if even p
   1.460 -               then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n)
   1.461 +               then ((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n)
   1.462                 else 0)
   1.463          = (\<lambda>p. cos_coeff p *\<^sub>R ((x+y)^p))"
   1.464          by simp
   1.465 @@ -2656,15 +2668,15 @@
   1.466    { fix n p::nat
   1.467      assume "n\<le>p"
   1.468      then have "(if even p \<and> even n
   1.469 -               then ((- 1) ^ (p div 2) * int (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0) -
   1.470 +               then ((- 1) ^ (p div 2) * int (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0) -
   1.471            (if even p \<and> odd n
   1.472 -               then - ((- 1) ^ (p div 2) * int (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)
   1.473 +               then - ((- 1) ^ (p div 2) * int (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)
   1.474            = (if even p
   1.475 -               then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)"
   1.476 +               then ((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)"
   1.477        by simp
   1.478    }
   1.479    then have "(\<lambda>p. \<Sum>n\<le>p. (if even p
   1.480 -               then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0))
   1.481 +               then ((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0))
   1.482          sums (cos x * cos y - sin x * sin y)"
   1.483      using sums_diff [OF cos_x_cos_y [of x y] sin_x_sin_y [of x y]]
   1.484      by (simp add: setsum_subtractf [symmetric])
   1.485 @@ -2701,7 +2713,6 @@
   1.486  by (simp add: cos_def summable_norm_cos [THEN summable_norm_cancel]
   1.487                suminf_minus sums_iff equation_minus_iff)
   1.488  
   1.489 -
   1.490  lemma sin_cos_squared_add [simp]:
   1.491    fixes x :: "'a::{real_normed_field,banach}"
   1.492    shows "(sin x)\<^sup>2 + (cos x)\<^sup>2 = 1"
   1.493 @@ -2787,7 +2798,7 @@
   1.494  
   1.495  lemma sin_paired:
   1.496    fixes x :: real
   1.497 -  shows "(\<lambda>n. (- 1) ^ n /(real (fact (2 * n + 1))) * x ^ (2 * n + 1)) sums  sin x"
   1.498 +  shows "(\<lambda>n. (- 1) ^ n / (fact (2 * n + 1)) * x ^ (2 * n + 1)) sums  sin x"
   1.499  proof -
   1.500    have "(\<lambda>n. \<Sum>k = n*2..<n * 2 + 2. sin_coeff k * x ^ k) sums sin x"
   1.501      apply (rule sums_group)
   1.502 @@ -2801,7 +2812,7 @@
   1.503    assumes "0 < x" and "x < 2"
   1.504    shows "0 < sin x"
   1.505  proof -
   1.506 -  let ?f = "\<lambda>n. \<Sum>k = n*2..<n*2+2. (- 1) ^ k / real (fact (2*k+1)) * x^(2*k+1)"
   1.507 +  let ?f = "\<lambda>n::nat. \<Sum>k = n*2..<n*2+2. (- 1) ^ k / (fact (2*k+1)) * x^(2*k+1)"
   1.508    have pos: "\<forall>n. 0 < ?f n"
   1.509    proof
   1.510      fix n :: nat
   1.511 @@ -2812,9 +2823,8 @@
   1.512      hence "x * x * x * x ^ (n * 4) < ?k2 * ?k3 * x * x ^ (n * 4)"
   1.513        by (intro mult_strict_right_mono zero_less_power `0 < x`)
   1.514      thus "0 < ?f n"
   1.515 -      by (simp del: mult_Suc,
   1.516 -        simp add: less_divide_eq field_simps del: mult_Suc)
   1.517 -  qed
   1.518 +      by (simp add: real_of_nat_def divide_simps mult_ac del: mult_Suc)
   1.519 +qed
   1.520    have sums: "?f sums sin x"
   1.521      by (rule sin_paired [THEN sums_group], simp)
   1.522    show "0 < sin x"
   1.523 @@ -2830,7 +2840,7 @@
   1.524  
   1.525  lemma cos_paired:
   1.526    fixes x :: real
   1.527 -  shows "(\<lambda>n. (- 1) ^ n /(real (fact (2 * n))) * x ^ (2 * n)) sums cos x"
   1.528 +  shows "(\<lambda>n. (- 1) ^ n / (fact (2 * n)) * x ^ (2 * n)) sums cos x"
   1.529  proof -
   1.530    have "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2. cos_coeff k * x ^ k) sums cos x"
   1.531      apply (rule sums_group)
   1.532 @@ -2860,29 +2870,28 @@
   1.533  lemma cos_two_less_zero [simp]:
   1.534    "cos 2 < (0::real)"
   1.535  proof -
   1.536 -  note fact_Suc [simp del]
   1.537 -  from cos_paired
   1.538 -  have "(\<lambda>n. - ((- 1) ^ n / real (fact (2 * n)) * 2 ^ (2 * n))) sums - cos 2"
   1.539 -    by (rule sums_minus)
   1.540 -  then have *: "(\<lambda>n. - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n)))) sums - cos 2"
   1.541 +  note fact.simps(2) [simp del]
   1.542 +  from sums_minus [OF cos_paired]
   1.543 +  have *: "(\<lambda>n. - ((- 1) ^ n * 2 ^ (2 * n) / fact (2 * n))) sums - cos (2::real)"
   1.544      by simp
   1.545 -  then have **: "summable (\<lambda>n. - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
   1.546 +  then have **: "summable (\<lambda>n. - ((- 1::real) ^ n * 2 ^ (2 * n) / (fact (2 * n))))"
   1.547      by (rule sums_summable)
   1.548 -  have "0 < (\<Sum>n<Suc (Suc (Suc 0)). - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
   1.549 -    by (simp add: fact_num_eq_if_nat realpow_num_eq_if)
   1.550 -  moreover have "(\<Sum>n<Suc (Suc (Suc 0)). - ((- 1) ^ n  * 2 ^ (2 * n) / real (fact (2 * n))))
   1.551 -    < (\<Sum>n. - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
   1.552 +  have "0 < (\<Sum>n<Suc (Suc (Suc 0)). - ((- 1::real) ^ n * 2 ^ (2 * n) / (fact (2 * n))))"
   1.553 +    by (simp add: fact_num_eq_if realpow_num_eq_if)
   1.554 +  moreover have "(\<Sum>n<Suc (Suc (Suc 0)). - ((- 1::real) ^ n  * 2 ^ (2 * n) / (fact (2 * n))))
   1.555 +    < (\<Sum>n. - ((- 1) ^ n * 2 ^ (2 * n) / (fact (2 * n))))"
   1.556    proof -
   1.557      { fix d
   1.558 -      have "4 * real (fact (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))
   1.559 -       < real (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))) *
   1.560 -           fact (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))))"
   1.561 -        by (simp only: real_of_nat_mult) (auto intro!: mult_strict_mono fact_less_mono_nat)
   1.562 -      then have "4 * real (fact (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))
   1.563 -        < real (fact (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))))"
   1.564 -        by (simp only: fact_Suc [of "Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))"])
   1.565 -      then have "4 * inverse (real (fact (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))))))
   1.566 -        < inverse (real (fact (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))))"
   1.567 +      have "(4::real) * (fact (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))
   1.568 +            < (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))) *
   1.569 +              fact (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))))"
   1.570 +        unfolding real_of_nat_mult
   1.571 +        by (rule mult_strict_mono) (simp_all add: fact_less_mono)
   1.572 +      then have "(4::real) * (fact (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))
   1.573 +        <  (fact (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))))"
   1.574 +        by (simp only: fact.simps(2) [of "Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))"] real_of_nat_def of_nat_mult of_nat_fact)
   1.575 +      then have "(4::real) * inverse (fact (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))))
   1.576 +        < inverse (fact (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))"
   1.577          by (simp add: inverse_eq_divide less_divide_eq)
   1.578      }
   1.579      note *** = this
   1.580 @@ -2890,9 +2899,9 @@
   1.581      from ** show ?thesis by (rule sumr_pos_lt_pair)
   1.582        (simp add: divide_inverse mult.assoc [symmetric] ***)
   1.583    qed
   1.584 -  ultimately have "0 < (\<Sum>n. - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
   1.585 +  ultimately have "0 < (\<Sum>n. - ((- 1::real) ^ n * 2 ^ (2 * n) / (fact (2 * n))))"
   1.586      by (rule order_less_trans)
   1.587 -  moreover from * have "- cos 2 = (\<Sum>n. - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
   1.588 +  moreover from * have "- cos 2 = (\<Sum>n. - ((- 1::real) ^ n * 2 ^ (2 * n) / (fact (2 * n))))"
   1.589      by (rule sums_unique)
   1.590    ultimately have "(0::real) < - cos 2" by simp
   1.591    then show ?thesis by simp