src/HOL/MacLaurin.thy
 changeset 59730 b7c394c7a619 parent 58889 5b7a9633cfa8 child 60017 b785d6d06430
```     1.1 --- a/src/HOL/MacLaurin.thy	Tue Mar 10 16:12:35 2015 +0000
1.2 +++ b/src/HOL/MacLaurin.thy	Mon Mar 16 15:30:00 2015 +0000
1.3 @@ -17,47 +17,52 @@
1.4
1.5  lemma Maclaurin_lemma:
1.6      "0 < h ==>
1.7 -     \<exists>B. f h = (\<Sum>m<n. (j m / real (fact m)) * (h^m)) +
1.8 -               (B * ((h^n) / real(fact n)))"
1.9 -by (rule exI[where x = "(f h - (\<Sum>m<n. (j m / real (fact m)) * h^m)) * real(fact n) / (h^n)"]) simp
1.10 +     \<exists>B::real. f h = (\<Sum>m<n. (j m / (fact m)) * (h^m)) +
1.11 +               (B * ((h^n) /(fact n)))"
1.12 +by (rule exI[where x = "(f h - (\<Sum>m<n. (j m / (fact m)) * h^m)) * (fact n) / (h^n)"]) simp
1.13
1.14  lemma eq_diff_eq': "(x = y - z) = (y = x + (z::real))"
1.15  by arith
1.16
1.17  lemma fact_diff_Suc [rule_format]:
1.18    "n < Suc m ==> fact (Suc m - n) = (Suc m - n) * fact (m - n)"
1.19 -  by (subst fact_reduce_nat, auto)
1.20 +  by (subst fact_reduce, auto)
1.21
1.22  lemma Maclaurin_lemma2:
1.23    fixes B
1.24    assumes DERIV : "\<forall>m t. m < n \<and> 0\<le>t \<and> t\<le>h \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
1.25 -    and INIT : "n = Suc k"
1.26 -  defines "difg \<equiv> (\<lambda>m t. diff m t - ((\<Sum>p<n - m. diff (m + p) 0 / real (fact p) * t ^ p) +
1.27 -    B * (t ^ (n - m) / real (fact (n - m)))))" (is "difg \<equiv> (\<lambda>m t. diff m t - ?difg m t)")
1.28 +      and INIT : "n = Suc k"
1.29 +  defines "difg \<equiv>
1.30 +      (\<lambda>m t::real. diff m t -
1.31 +         ((\<Sum>p<n - m. diff (m + p) 0 / (fact p) * t ^ p) + B * (t ^ (n - m) / (fact (n - m)))))"
1.32 +        (is "difg \<equiv> (\<lambda>m t. diff m t - ?difg m t)")
1.33    shows "\<forall>m t. m < n & 0 \<le> t & t \<le> h --> DERIV (difg m) t :> difg (Suc m) t"
1.34  proof (rule allI impI)+
1.35 -  fix m t assume INIT2: "m < n & 0 \<le> t & t \<le> h"
1.36 +  fix m and t::real
1.37 +  assume INIT2: "m < n & 0 \<le> t & t \<le> h"
1.38    have "DERIV (difg m) t :> diff (Suc m) t -
1.39 -    ((\<Sum>x<n - m. real x * t ^ (x - Suc 0) * diff (m + x) 0 / real (fact x)) +
1.40 -     real (n - m) * t ^ (n - Suc m) * B / real (fact (n - m)))" unfolding difg_def
1.41 +    ((\<Sum>x<n - m. real x * t ^ (x - Suc 0) * diff (m + x) 0 / (fact x)) +
1.42 +     real (n - m) * t ^ (n - Suc m) * B / (fact (n - m)))"
1.43 +    unfolding difg_def
1.44      by (auto intro!: derivative_eq_intros DERIV[rule_format, OF INIT2]
1.45               simp: real_of_nat_def[symmetric])
1.46    moreover
1.47    from INIT2 have intvl: "{..<n - m} = insert 0 (Suc ` {..<n - Suc m})" and "0 < n - m"
1.48      unfolding atLeast0LessThan[symmetric] by auto
1.49 -  have "(\<Sum>x<n - m. real x * t ^ (x - Suc 0) * diff (m + x) 0 / real (fact x)) =
1.50 -      (\<Sum>x<n - Suc m. real (Suc x) * t ^ x * diff (Suc m + x) 0 / real (fact (Suc x)))"
1.51 +  have "(\<Sum>x<n - m. real x * t ^ (x - Suc 0) * diff (m + x) 0 / (fact x)) =
1.52 +      (\<Sum>x<n - Suc m. real (Suc x) * t ^ x * diff (Suc m + x) 0 / (fact (Suc x)))"
1.53      unfolding intvl atLeast0LessThan by (subst setsum.insert) (auto simp: setsum.reindex)
1.54    moreover
1.55 -  have fact_neq_0: "\<And>x::nat. real (fact x) + real x * real (fact x) \<noteq> 0"
1.57 -  have "\<And>x. real (Suc x) * t ^ x * diff (Suc m + x) 0 / real (fact (Suc x)) =
1.58 -      diff (Suc m + x) 0 * t^x / real (fact x)"
1.59 -    by (auto simp: field_simps real_of_nat_Suc fact_neq_0 intro!: nonzero_divide_eq_eq[THEN iffD2])
1.60 +  have fact_neq_0: "\<And>x. (fact x) + real x * (fact x) \<noteq> 0"
1.62 +  have "\<And>x. (Suc x) * t ^ x * diff (Suc m + x) 0 / (fact (Suc x)) =
1.63 +            diff (Suc m + x) 0 * t^x / (fact x)"
1.64 +    by (rule nonzero_divide_eq_eq[THEN iffD2]) auto
1.65    moreover
1.66 -  have "real (n - m) * t ^ (n - Suc m) * B / real (fact (n - m)) =
1.67 -      B * (t ^ (n - Suc m) / real (fact (n - Suc m)))"
1.68 -    using `0 < n - m` by (simp add: fact_reduce_nat)
1.69 +  have "(n - m) * t ^ (n - Suc m) * B / (fact (n - m)) =
1.70 +        B * (t ^ (n - Suc m) / (fact (n - Suc m)))"
1.71 +    using `0 < n - m`
1.72 +    by (simp add: divide_simps fact_reduce)
1.73    ultimately show "DERIV (difg m) t :> difg (Suc m) t"
1.74      unfolding difg_def by simp
1.75  qed
1.76 @@ -69,29 +74,27 @@
1.77    assumes diff_Suc:
1.78      "\<forall>m t. m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t"
1.79    shows
1.80 -    "\<exists>t. 0 < t & t < h &
1.81 +    "\<exists>t::real. 0 < t & t < h &
1.82                f h =
1.83 -              setsum (%m. (diff m 0 / real (fact m)) * h ^ m) {..<n} +
1.84 -              (diff n t / real (fact n)) * h ^ n"
1.85 +              setsum (%m. (diff m 0 / (fact m)) * h ^ m) {..<n} +
1.86 +              (diff n t / (fact n)) * h ^ n"
1.87  proof -
1.88    from n obtain m where m: "n = Suc m"
1.89      by (cases n) (simp add: n)
1.90
1.91    obtain B where f_h: "f h =
1.92 -        (\<Sum>m<n. diff m (0\<Colon>real) / real (fact m) * h ^ m) +
1.93 -        B * (h ^ n / real (fact n))"
1.94 +        (\<Sum>m<n. diff m (0\<Colon>real) / (fact m) * h ^ m) + B * (h ^ n / (fact n))"
1.95      using Maclaurin_lemma [OF h] ..
1.96
1.97    def g \<equiv> "(\<lambda>t. f t -
1.98 -    (setsum (\<lambda>m. (diff m 0 / real(fact m)) * t^m) {..<n}
1.99 -      + (B * (t^n / real(fact n)))))"
1.100 +    (setsum (\<lambda>m. (diff m 0 / (fact m)) * t^m) {..<n} + (B * (t^n / (fact n)))))"
1.101
1.102    have g2: "g 0 = 0 & g h = 0"
1.103      by (simp add: m f_h g_def lessThan_Suc_eq_insert_0 image_iff diff_0 setsum.reindex)
1.104
1.105    def difg \<equiv> "(%m t. diff m t -
1.106 -    (setsum (%p. (diff (m + p) 0 / real (fact p)) * (t ^ p)) {..<n-m}
1.107 -      + (B * ((t ^ (n - m)) / real (fact (n - m))))))"
1.108 +    (setsum (%p. (diff (m + p) 0 / (fact p)) * (t ^ p)) {..<n-m}
1.109 +      + (B * ((t ^ (n - m)) / (fact (n - m))))))"
1.110
1.111    have difg_0: "difg 0 = g"
1.112      unfolding difg_def g_def by (simp add: diff_0)
1.113 @@ -146,7 +149,6 @@
1.114      thus ?case
1.115        using `t < h` by auto
1.116    qed
1.117 -
1.118    then obtain t where "0 < t" "t < h" "DERIV (difg m) t :> 0" by fast
1.119
1.120    hence "difg (Suc m) t = 0"
1.121 @@ -156,30 +158,28 @@
1.122    proof (intro exI conjI)
1.123      show "0 < t" by fact
1.124      show "t < h" by fact
1.125 -    show "f h =
1.126 -      (\<Sum>m<n. diff m 0 / real (fact m) * h ^ m) +
1.127 -      diff n t / real (fact n) * h ^ n"
1.128 +    show "f h = (\<Sum>m<n. diff m 0 / (fact m) * h ^ m) + diff n t / (fact n) * h ^ n"
1.129        using `difg (Suc m) t = 0`
1.130 -      by (simp add: m f_h difg_def del: fact_Suc)
1.131 +      by (simp add: m f_h difg_def)
1.132    qed
1.133  qed
1.134
1.135  lemma Maclaurin_objl:
1.136    "0 < h & n>0 & diff 0 = f &
1.137    (\<forall>m t. m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t)
1.138 -   --> (\<exists>t. 0 < t & t < h &
1.139 -            f h = (\<Sum>m<n. diff m 0 / real (fact m) * h ^ m) +
1.140 -                  diff n t / real (fact n) * h ^ n)"
1.141 +   --> (\<exists>t::real. 0 < t & t < h &
1.142 +            f h = (\<Sum>m<n. diff m 0 / (fact m) * h ^ m) +
1.143 +                  diff n t / (fact n) * h ^ n)"
1.144  by (blast intro: Maclaurin)
1.145
1.146
1.147  lemma Maclaurin2:
1.148    assumes INIT1: "0 < h " and INIT2: "diff 0 = f"
1.149 -  and DERIV: "\<forall>m t.
1.150 +  and DERIV: "\<forall>m t::real.
1.151    m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t"
1.152    shows "\<exists>t. 0 < t \<and> t \<le> h \<and> f h =
1.153 -  (\<Sum>m<n. diff m 0 / real (fact m) * h ^ m) +
1.154 -  diff n t / real (fact n) * h ^ n"
1.155 +  (\<Sum>m<n. diff m 0 / (fact m) * h ^ m) +
1.156 +  diff n t / (fact n) * h ^ n"
1.157  proof (cases "n")
1.158    case 0 with INIT1 INIT2 show ?thesis by fastforce
1.159  next
1.160 @@ -187,28 +187,28 @@
1.161    hence "n > 0" by simp
1.162    from INIT1 this INIT2 DERIV have "\<exists>t>0. t < h \<and>
1.163      f h =
1.164 -    (\<Sum>m<n. diff m 0 / real (fact m) * h ^ m) + diff n t / real (fact n) * h ^ n"
1.165 +    (\<Sum>m<n. diff m 0 / (fact m) * h ^ m) + diff n t / (fact n) * h ^ n"
1.166      by (rule Maclaurin)
1.167    thus ?thesis by fastforce
1.168  qed
1.169
1.170  lemma Maclaurin2_objl:
1.171       "0 < h & diff 0 = f &
1.172 -       (\<forall>m t.
1.173 -          m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t)
1.174 -    --> (\<exists>t. 0 < t &
1.175 +       (\<forall>m t. m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t)
1.176 +    --> (\<exists>t::real. 0 < t &
1.177                t \<le> h &
1.178                f h =
1.179 -              (\<Sum>m<n. diff m 0 / real (fact m) * h ^ m) +
1.180 -              diff n t / real (fact n) * h ^ n)"
1.181 +              (\<Sum>m<n. diff m 0 / (fact m) * h ^ m) +
1.182 +              diff n t / (fact n) * h ^ n)"
1.183  by (blast intro: Maclaurin2)
1.184
1.185  lemma Maclaurin_minus:
1.186 +  fixes h::real
1.187    assumes "h < 0" "0 < n" "diff 0 = f"
1.188    and DERIV: "\<forall>m t. m < n & h \<le> t & t \<le> 0 --> DERIV (diff m) t :> diff (Suc m) t"
1.189    shows "\<exists>t. h < t & t < 0 &
1.190 -         f h = (\<Sum>m<n. diff m 0 / real (fact m) * h ^ m) +
1.191 -         diff n t / real (fact n) * h ^ n"
1.192 +         f h = (\<Sum>m<n. diff m 0 / (fact m) * h ^ m) +
1.193 +         diff n t / (fact n) * h ^ n"
1.194  proof -
1.195    txt "Transform @{text ABL'} into @{text derivative_intros} format."
1.196    note DERIV' = DERIV_chain'[OF _ DERIV[rule_format], THEN DERIV_cong]
1.197 @@ -216,33 +216,35 @@
1.198    have "\<exists>t>0. t < - h \<and>
1.199      f (- (- h)) =
1.200      (\<Sum>m<n.
1.201 -    (- 1) ^ m * diff m (- 0) / real (fact m) * (- h) ^ m) +
1.202 -    (- 1) ^ n * diff n (- t) / real (fact n) * (- h) ^ n"
1.203 +    (- 1) ^ m * diff m (- 0) / (fact m) * (- h) ^ m) +
1.204 +    (- 1) ^ n * diff n (- t) / (fact n) * (- h) ^ n"
1.205      by (intro Maclaurin) (auto intro!: derivative_eq_intros DERIV')
1.206    then guess t ..
1.207    moreover
1.208 -  have "(- 1) ^ n * diff n (- t) * (- h) ^ n / real (fact n) = diff n (- t) * h ^ n / real (fact n)"
1.209 +  have "(- 1) ^ n * diff n (- t) * (- h) ^ n / (fact n) = diff n (- t) * h ^ n / (fact n)"
1.210      by (auto simp add: power_mult_distrib[symmetric])
1.211    moreover
1.212 -  have "(SUM m<n. (- 1) ^ m * diff m 0 * (- h) ^ m / real (fact m)) = (SUM m<n. diff m 0 * h ^ m / real (fact m))"
1.213 +  have "(SUM m<n. (- 1) ^ m * diff m 0 * (- h) ^ m / (fact m)) = (SUM m<n. diff m 0 * h ^ m / (fact m))"
1.214      by (auto intro: setsum.cong simp add: power_mult_distrib[symmetric])
1.215    ultimately have " h < - t \<and>
1.216      - t < 0 \<and>
1.217      f h =
1.218 -    (\<Sum>m<n. diff m 0 / real (fact m) * h ^ m) + diff n (- t) / real (fact n) * h ^ n"
1.219 +    (\<Sum>m<n. diff m 0 / (fact m) * h ^ m) + diff n (- t) / (fact n) * h ^ n"
1.220      by auto
1.221    thus ?thesis ..
1.222  qed
1.223
1.224  lemma Maclaurin_minus_objl:
1.225 +  fixes h::real
1.226 +  shows
1.227       "(h < 0 & n > 0 & diff 0 = f &
1.228         (\<forall>m t.
1.229            m < n & h \<le> t & t \<le> 0 --> DERIV (diff m) t :> diff (Suc m) t))
1.230      --> (\<exists>t. h < t &
1.231                t < 0 &
1.232                f h =
1.233 -              (\<Sum>m<n. diff m 0 / real (fact m) * h ^ m) +
1.234 -              diff n t / real (fact n) * h ^ n)"
1.235 +              (\<Sum>m<n. diff m 0 / (fact m) * h ^ m) +
1.236 +              diff n t / (fact n) * h ^ n)"
1.237  by (blast intro: Maclaurin_minus)
1.238
1.239
1.240 @@ -250,20 +252,19 @@
1.241
1.242  (* not good for PVS sin_approx, cos_approx *)
1.243
1.244 -lemma Maclaurin_bi_le_lemma [rule_format]:
1.245 -  "n>0 \<longrightarrow>
1.246 +lemma Maclaurin_bi_le_lemma:
1.247 +  "n>0 \<Longrightarrow>
1.248     diff 0 0 =
1.249 -   (\<Sum>m<n. diff m 0 * 0 ^ m / real (fact m)) +
1.250 -   diff n 0 * 0 ^ n / real (fact n)"
1.251 +   (\<Sum>m<n. diff m 0 * 0 ^ m / (fact m)) + diff n 0 * 0 ^ n / (fact n :: real)"
1.252  by (induct "n") auto
1.253
1.254  lemma Maclaurin_bi_le:
1.255     assumes "diff 0 = f"
1.256 -   and DERIV : "\<forall>m t. m < n & abs t \<le> abs x --> DERIV (diff m) t :> diff (Suc m) t"
1.257 +   and DERIV : "\<forall>m t::real. m < n & abs t \<le> abs x --> DERIV (diff m) t :> diff (Suc m) t"
1.258     shows "\<exists>t. abs t \<le> abs x &
1.259                f x =
1.260 -              (\<Sum>m<n. diff m 0 / real (fact m) * x ^ m) +
1.261 -     diff n t / real (fact n) * x ^ n" (is "\<exists>t. _ \<and> f x = ?f x t")
1.262 +              (\<Sum>m<n. diff m 0 / (fact m) * x ^ m) +
1.263 +     diff n t / (fact n) * x ^ n" (is "\<exists>t. _ \<and> f x = ?f x t")
1.264  proof cases
1.265    assume "n = 0" with `diff 0 = f` show ?thesis by force
1.266  next
1.267 @@ -291,11 +292,12 @@
1.268  qed
1.269
1.270  lemma Maclaurin_all_lt:
1.271 +  fixes x::real
1.272    assumes INIT1: "diff 0 = f" and INIT2: "0 < n" and INIT3: "x \<noteq> 0"
1.273    and DERIV: "\<forall>m x. DERIV (diff m) x :> diff(Suc m) x"
1.274    shows "\<exists>t. 0 < abs t & abs t < abs x & f x =
1.275 -    (\<Sum>m<n. (diff m 0 / real (fact m)) * x ^ m) +
1.276 -                (diff n t / real (fact n)) * x ^ n" (is "\<exists>t. _ \<and> _ \<and> f x = ?f x t")
1.277 +    (\<Sum>m<n. (diff m 0 / (fact m)) * x ^ m) +
1.278 +                (diff n t / (fact n)) * x ^ n" (is "\<exists>t. _ \<and> _ \<and> f x = ?f x t")
1.279  proof (cases rule: linorder_cases)
1.280    assume "x = 0" with INIT3 show "?thesis"..
1.281  next
1.282 @@ -314,28 +316,30 @@
1.283
1.284
1.285  lemma Maclaurin_all_lt_objl:
1.286 +  fixes x::real
1.287 +  shows
1.288       "diff 0 = f &
1.289        (\<forall>m x. DERIV (diff m) x :> diff(Suc m) x) &
1.290        x ~= 0 & n > 0
1.291        --> (\<exists>t. 0 < abs t & abs t < abs x &
1.292 -               f x = (\<Sum>m<n. (diff m 0 / real (fact m)) * x ^ m) +
1.293 -                     (diff n t / real (fact n)) * x ^ n)"
1.294 +               f x = (\<Sum>m<n. (diff m 0 / (fact m)) * x ^ m) +
1.295 +                     (diff n t / (fact n)) * x ^ n)"
1.296  by (blast intro: Maclaurin_all_lt)
1.297
1.298  lemma Maclaurin_zero [rule_format]:
1.299       "x = (0::real)
1.300        ==> n \<noteq> 0 -->
1.301 -          (\<Sum>m<n. (diff m (0::real) / real (fact m)) * x ^ m) =
1.302 +          (\<Sum>m<n. (diff m (0::real) / (fact m)) * x ^ m) =
1.303            diff 0 0"
1.304  by (induct n, auto)
1.305
1.306
1.307  lemma Maclaurin_all_le:
1.308    assumes INIT: "diff 0 = f"
1.309 -  and DERIV: "\<forall>m x. DERIV (diff m) x :> diff (Suc m) x"
1.310 +  and DERIV: "\<forall>m x::real. DERIV (diff m) x :> diff (Suc m) x"
1.311    shows "\<exists>t. abs t \<le> abs x & f x =
1.312 -    (\<Sum>m<n. (diff m 0 / real (fact m)) * x ^ m) +
1.313 -    (diff n t / real (fact n)) * x ^ n" (is "\<exists>t. _ \<and> f x = ?f x t")
1.314 +    (\<Sum>m<n. (diff m 0 / (fact m)) * x ^ m) +
1.315 +    (diff n t / (fact n)) * x ^ n" (is "\<exists>t. _ \<and> f x = ?f x t")
1.316  proof cases
1.317    assume "n = 0" with INIT show ?thesis by force
1.318    next
1.319 @@ -343,7 +347,7 @@
1.320    show ?thesis
1.321    proof cases
1.322      assume "x = 0"
1.323 -    with `n \<noteq> 0` have "(\<Sum>m<n. diff m 0 / real (fact m) * x ^ m) = diff 0 0"
1.324 +    with `n \<noteq> 0` have "(\<Sum>m<n. diff m 0 / (fact m) * x ^ m) = diff 0 0"
1.325        by (intro Maclaurin_zero) auto
1.326      with INIT `x = 0` `n \<noteq> 0` have " \<bar>0\<bar> \<le> \<bar>x\<bar> \<and> f x = ?f x 0" by force
1.327      thus ?thesis ..
1.328 @@ -357,28 +361,32 @@
1.329    qed
1.330  qed
1.331
1.332 -lemma Maclaurin_all_le_objl: "diff 0 = f &
1.333 +lemma Maclaurin_all_le_objl:
1.334 +  "diff 0 = f &
1.335        (\<forall>m x. DERIV (diff m) x :> diff (Suc m) x)
1.336 -      --> (\<exists>t. abs t \<le> abs x &
1.337 -              f x = (\<Sum>m<n. (diff m 0 / real (fact m)) * x ^ m) +
1.338 -                    (diff n t / real (fact n)) * x ^ n)"
1.339 +      --> (\<exists>t::real. abs t \<le> abs x &
1.340 +              f x = (\<Sum>m<n. (diff m 0 / (fact m)) * x ^ m) +
1.341 +                    (diff n t / (fact n)) * x ^ n)"
1.342  by (blast intro: Maclaurin_all_le)
1.343
1.344
1.345  subsection{*Version for Exponential Function*}
1.346
1.347 -lemma Maclaurin_exp_lt: "[| x ~= 0; n > 0 |]
1.348 +lemma Maclaurin_exp_lt:
1.349 +  fixes x::real
1.350 +  shows
1.351 +  "[| x ~= 0; n > 0 |]
1.352        ==> (\<exists>t. 0 < abs t &
1.353                  abs t < abs x &
1.354 -                exp x = (\<Sum>m<n. (x ^ m) / real (fact m)) +
1.355 -                        (exp t / real (fact n)) * x ^ n)"
1.356 +                exp x = (\<Sum>m<n. (x ^ m) / (fact m)) +
1.357 +                        (exp t / (fact n)) * x ^ n)"
1.358  by (cut_tac diff = "%n. exp" and f = exp and x = x and n = n in Maclaurin_all_lt_objl, auto)
1.359
1.360
1.361  lemma Maclaurin_exp_le:
1.362 -     "\<exists>t. abs t \<le> abs x &
1.363 -            exp x = (\<Sum>m<n. (x ^ m) / real (fact m)) +
1.364 -                       (exp t / real (fact n)) * x ^ n"
1.365 +     "\<exists>t::real. abs t \<le> abs x &
1.366 +            exp x = (\<Sum>m<n. (x ^ m) / (fact m)) +
1.367 +                       (exp t / (fact n)) * x ^ n"
1.368  by (cut_tac diff = "%n. exp" and f = exp and x = x and n = n in Maclaurin_all_le_objl, auto)
1.369
1.370
1.371 @@ -412,7 +420,7 @@
1.372       "\<exists>t. abs t \<le> abs x &
1.373         sin x =
1.374         (\<Sum>m<n. sin_coeff m * x ^ m)
1.375 -      + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
1.376 +      + ((sin(t + 1/2 * real (n) *pi) / (fact n)) * x ^ n)"
1.377  apply (cut_tac f = sin and n = n and x = x
1.378          and diff = "%n x. sin (x + 1/2*real n * pi)" in Maclaurin_all_lt_objl)
1.379  apply safe
1.380 @@ -431,7 +439,7 @@
1.381  lemma Maclaurin_sin_expansion:
1.382       "\<exists>t. sin x =
1.383         (\<Sum>m<n. sin_coeff m * x ^ m)
1.384 -      + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
1.385 +      + ((sin(t + 1/2 * real (n) *pi) / (fact n)) * x ^ n)"
1.386  apply (insert Maclaurin_sin_expansion2 [of x n])
1.387  apply (blast intro: elim:)
1.388  done
1.389 @@ -441,7 +449,7 @@
1.390         \<exists>t. 0 < t & t < x &
1.391         sin x =
1.392         (\<Sum>m<n. sin_coeff m * x ^ m)
1.393 -      + ((sin(t + 1/2 * real(n) *pi) / real (fact n)) * x ^ n)"
1.394 +      + ((sin(t + 1/2 * real(n) *pi) / (fact n)) * x ^ n)"
1.395  apply (cut_tac f = sin and n = n and h = x and diff = "%n x. sin (x + 1/2*real (n) *pi)" in Maclaurin_objl)
1.396  apply safe
1.397  apply simp
1.398 @@ -458,7 +466,7 @@
1.399         \<exists>t. 0 < t & t \<le> x &
1.400         sin x =
1.401         (\<Sum>m<n. sin_coeff m * x ^ m)
1.402 -      + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
1.403 +      + ((sin(t + 1/2 * real (n) *pi) / (fact n)) * x ^ n)"
1.404  apply (cut_tac f = sin and n = n and h = x and diff = "%n x. sin (x + 1/2*real (n) *pi)" in Maclaurin2_objl)
1.405  apply safe
1.406  apply simp
1.407 @@ -482,10 +490,10 @@
1.409
1.410  lemma Maclaurin_cos_expansion:
1.411 -     "\<exists>t. abs t \<le> abs x &
1.412 +     "\<exists>t::real. abs t \<le> abs x &
1.413         cos x =
1.414         (\<Sum>m<n. cos_coeff m * x ^ m)
1.415 -      + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
1.416 +      + ((cos(t + 1/2 * real (n) *pi) / (fact n)) * x ^ n)"
1.417  apply (cut_tac f = cos and n = n and x = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_all_lt_objl)
1.418  apply safe
1.419  apply (simp (no_asm))
1.420 @@ -505,7 +513,7 @@
1.421         \<exists>t. 0 < t & t < x &
1.422         cos x =
1.423         (\<Sum>m<n. cos_coeff m * x ^ m)
1.424 -      + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
1.425 +      + ((cos(t + 1/2 * real (n) *pi) / (fact n)) * x ^ n)"
1.426  apply (cut_tac f = cos and n = n and h = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_objl)
1.427  apply safe
1.428  apply simp
1.429 @@ -521,7 +529,7 @@
1.430         \<exists>t. x < t & t < 0 &
1.431         cos x =
1.432         (\<Sum>m<n. cos_coeff m * x ^ m)
1.433 -      + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
1.434 +      + ((cos(t + 1/2 * real (n) *pi) / (fact n)) * x ^ n)"
1.435  apply (cut_tac f = cos and n = n and h = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_minus_objl)
1.436  apply safe
1.437  apply simp
1.438 @@ -542,7 +550,7 @@
1.439
1.440  lemma Maclaurin_sin_bound:
1.441    "abs(sin x - (\<Sum>m<n. sin_coeff m * x ^ m))
1.442 -  \<le> inverse(real (fact n)) * \<bar>x\<bar> ^ n"
1.443 +  \<le> inverse((fact n)) * \<bar>x\<bar> ^ n"
1.444  proof -
1.445    have "!! x (y::real). x \<le> 1 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x * y \<le> 1 * y"
1.446      by (rule_tac mult_right_mono,simp_all)
1.447 @@ -557,8 +565,8 @@
1.448      done
1.449    from Maclaurin_all_le [OF diff_0 DERIV_diff]
1.450    obtain t where t1: "\<bar>t\<bar> \<le> \<bar>x\<bar>" and
1.451 -    t2: "sin x = (\<Sum>m<n. ?diff m 0 / real (fact m) * x ^ m) +
1.452 -      ?diff n t / real (fact n) * x ^ n" by fast
1.453 +    t2: "sin x = (\<Sum>m<n. ?diff m 0 / (fact m) * x ^ m) +
1.454 +      ?diff n t / (fact n) * x ^ n" by fast
1.455    have diff_m_0:
1.456      "\<And>m. ?diff m 0 = (if even m then 0
1.457           else (- 1) ^ ((m - Suc 0) div 2))"
```