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.56 -    by (metis fact_gt_zero_nat not_add_less1 real_of_nat_add real_of_nat_mult real_of_nat_zero_iff)
    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.61 +    by (metis add_pos_pos fact_gt_zero less_add_same_cancel1 less_add_same_cancel2 less_numeral_extra(3) mult_less_0_iff not_real_of_nat_less_zero)
    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.408  by (simp only: cos_add sin_add real_of_nat_Suc distrib_right add_divide_distrib, auto)
   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))"