src/HOL/MacLaurin.thy
changeset 56193 c726ecfb22b6
parent 56181 2aa0b19e74f3
child 56238 5d147e1e18d1
     1.1 --- a/src/HOL/MacLaurin.thy	Tue Mar 18 14:32:23 2014 +0100
     1.2 +++ b/src/HOL/MacLaurin.thy	Tue Mar 18 15:53:48 2014 +0100
     1.3 @@ -17,10 +17,9 @@
     1.4  
     1.5  lemma Maclaurin_lemma:
     1.6      "0 < h ==>
     1.7 -     \<exists>B. f h = (\<Sum>m=0..<n. (j m / real (fact m)) * (h^m)) +
     1.8 +     \<exists>B. f h = (\<Sum>m<n. (j m / real (fact m)) * (h^m)) +
     1.9                 (B * ((h^n) / real(fact n)))"
    1.10 -by (rule exI[where x = "(f h - (\<Sum>m=0..<n. (j m / real (fact m)) * h^m)) *
    1.11 -                 real(fact n) / (h^n)"]) simp
    1.12 +by (rule exI[where x = "(f h - (\<Sum>m<n. (j m / real (fact m)) * h^m)) * real(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 @@ -33,20 +32,20 @@
    1.17    fixes B
    1.18    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.19      and INIT : "n = Suc k"
    1.20 -  defines "difg \<equiv> (\<lambda>m t. diff m t - ((\<Sum>p = 0..<n - m. diff (m + p) 0 / real (fact p) * t ^ p) +
    1.21 +  defines "difg \<equiv> (\<lambda>m t. diff m t - ((\<Sum>p<n - m. diff (m + p) 0 / real (fact p) * t ^ p) +
    1.22      B * (t ^ (n - m) / real (fact (n - m)))))" (is "difg \<equiv> (\<lambda>m t. diff m t - ?difg m t)")
    1.23    shows "\<forall>m t. m < n & 0 \<le> t & t \<le> h --> DERIV (difg m) t :> difg (Suc m) t"
    1.24  proof (rule allI impI)+
    1.25    fix m t assume INIT2: "m < n & 0 \<le> t & t \<le> h"
    1.26    have "DERIV (difg m) t :> diff (Suc m) t -
    1.27 -    ((\<Sum>x = 0..<n - m. real x * t ^ (x - Suc 0) * diff (m + x) 0 / real (fact x)) +
    1.28 +    ((\<Sum>x<n - m. real x * t ^ (x - Suc 0) * diff (m + x) 0 / real (fact x)) +
    1.29       real (n - m) * t ^ (n - Suc m) * B / real (fact (n - m)))" unfolding difg_def
    1.30      by (auto intro!: DERIV_intros DERIV[rule_format, OF INIT2])
    1.31 -      moreover
    1.32 +  moreover
    1.33    from INIT2 have intvl: "{..<n - m} = insert 0 (Suc ` {..<n - Suc m})" and "0 < n - m"
    1.34      unfolding atLeast0LessThan[symmetric] by auto
    1.35 -  have "(\<Sum>x = 0..<n - m. real x * t ^ (x - Suc 0) * diff (m + x) 0 / real (fact x)) =
    1.36 -      (\<Sum>x = 0..<n - Suc m. real (Suc x) * t ^ x * diff (Suc m + x) 0 / real (fact (Suc x)))"
    1.37 +  have "(\<Sum>x<n - m. real x * t ^ (x - Suc 0) * diff (m + x) 0 / real (fact x)) =
    1.38 +      (\<Sum>x<n - Suc m. real (Suc x) * t ^ x * diff (Suc m + x) 0 / real (fact (Suc x)))"
    1.39      unfolding intvl atLeast0LessThan by (subst setsum.insert) (auto simp: setsum.reindex)
    1.40    moreover
    1.41    have fact_neq_0: "\<And>x::nat. real (fact x) + real x * real (fact x) \<noteq> 0"
    1.42 @@ -71,29 +70,26 @@
    1.43    shows
    1.44      "\<exists>t. 0 < t & t < h &
    1.45                f h =
    1.46 -              setsum (%m. (diff m 0 / real (fact m)) * h ^ m) {0..<n} +
    1.47 +              setsum (%m. (diff m 0 / real (fact m)) * h ^ m) {..<n} +
    1.48                (diff n t / real (fact n)) * h ^ n"
    1.49  proof -
    1.50    from n obtain m where m: "n = Suc m"
    1.51      by (cases n) (simp add: n)
    1.52  
    1.53    obtain B where f_h: "f h =
    1.54 -        (\<Sum>m = 0..<n. diff m (0\<Colon>real) / real (fact m) * h ^ m) +
    1.55 +        (\<Sum>m<n. diff m (0\<Colon>real) / real (fact m) * h ^ m) +
    1.56          B * (h ^ n / real (fact n))"
    1.57      using Maclaurin_lemma [OF h] ..
    1.58  
    1.59    def g \<equiv> "(\<lambda>t. f t -
    1.60 -    (setsum (\<lambda>m. (diff m 0 / real(fact m)) * t^m) {0..<n}
    1.61 +    (setsum (\<lambda>m. (diff m 0 / real(fact m)) * t^m) {..<n}
    1.62        + (B * (t^n / real(fact n)))))"
    1.63  
    1.64    have g2: "g 0 = 0 & g h = 0"
    1.65 -    apply (simp add: m f_h g_def del: setsum_op_ivl_Suc)
    1.66 -    apply (cut_tac n = m and k = "Suc 0" in sumr_offset2)
    1.67 -    apply (simp add: eq_diff_eq' diff_0 del: setsum_op_ivl_Suc)
    1.68 -    done
    1.69 +    by (simp add: m f_h g_def lessThan_Suc_eq_insert_0 image_iff diff_0 setsum_reindex)
    1.70  
    1.71    def difg \<equiv> "(%m t. diff m t -
    1.72 -    (setsum (%p. (diff (m + p) 0 / real (fact p)) * (t ^ p)) {0..<n-m}
    1.73 +    (setsum (%p. (diff (m + p) 0 / real (fact p)) * (t ^ p)) {..<n-m}
    1.74        + (B * ((t ^ (n - m)) / real (fact (n - m))))))"
    1.75  
    1.76    have difg_0: "difg 0 = g"
    1.77 @@ -103,14 +99,8 @@
    1.78          m < n \<and> (0\<Colon>real) \<le> t \<and> t \<le> h \<longrightarrow> DERIV (difg m) t :> difg (Suc m) t"
    1.79      using diff_Suc m unfolding difg_def by (rule Maclaurin_lemma2)
    1.80  
    1.81 -  have difg_eq_0: "\<forall>m. m < n --> difg m 0 = 0"
    1.82 -    apply clarify
    1.83 -    apply (simp add: m difg_def)
    1.84 -    apply (frule less_iff_Suc_add [THEN iffD1], clarify)
    1.85 -    apply (simp del: setsum_op_ivl_Suc)
    1.86 -    apply (insert sumr_offset4 [of "Suc 0"])
    1.87 -    apply (simp del: setsum_op_ivl_Suc fact_Suc)
    1.88 -    done
    1.89 +  have difg_eq_0: "\<forall>m<n. difg m 0 = 0"
    1.90 +    by (auto simp: difg_def m Suc_diff_le lessThan_Suc_eq_insert_0 image_iff setsum_reindex)
    1.91  
    1.92    have isCont_difg: "\<And>m x. \<lbrakk>m < n; 0 \<le> x; x \<le> h\<rbrakk> \<Longrightarrow> isCont (difg m) x"
    1.93      by (rule DERIV_isCont [OF difg_Suc [rule_format]]) simp
    1.94 @@ -166,7 +156,7 @@
    1.95      show "0 < t" by fact
    1.96      show "t < h" by fact
    1.97      show "f h =
    1.98 -      (\<Sum>m = 0..<n. diff m 0 / real (fact m) * h ^ m) +
    1.99 +      (\<Sum>m<n. diff m 0 / real (fact m) * h ^ m) +
   1.100        diff n t / real (fact n) * h ^ n"
   1.101        using `difg (Suc m) t = 0`
   1.102        by (simp add: m f_h difg_def del: fact_Suc)
   1.103 @@ -177,7 +167,7 @@
   1.104    "0 < h & n>0 & diff 0 = f &
   1.105    (\<forall>m t. m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t)
   1.106     --> (\<exists>t. 0 < t & t < h &
   1.107 -            f h = (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
   1.108 +            f h = (\<Sum>m<n. diff m 0 / real (fact m) * h ^ m) +
   1.109                    diff n t / real (fact n) * h ^ n)"
   1.110  by (blast intro: Maclaurin)
   1.111  
   1.112 @@ -187,7 +177,7 @@
   1.113    and DERIV: "\<forall>m t.
   1.114    m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t"
   1.115    shows "\<exists>t. 0 < t \<and> t \<le> h \<and> f h =
   1.116 -  (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
   1.117 +  (\<Sum>m<n. diff m 0 / real (fact m) * h ^ m) +
   1.118    diff n t / real (fact n) * h ^ n"
   1.119  proof (cases "n")
   1.120    case 0 with INIT1 INIT2 show ?thesis by fastforce
   1.121 @@ -196,7 +186,7 @@
   1.122    hence "n > 0" by simp
   1.123    from INIT1 this INIT2 DERIV have "\<exists>t>0. t < h \<and>
   1.124      f h =
   1.125 -    (\<Sum>m = 0..<n. diff m 0 / real (fact m) * h ^ m) + diff n t / real (fact n) * h ^ n"
   1.126 +    (\<Sum>m<n. diff m 0 / real (fact m) * h ^ m) + diff n t / real (fact n) * h ^ n"
   1.127      by (rule Maclaurin)
   1.128    thus ?thesis by fastforce
   1.129  qed
   1.130 @@ -208,7 +198,7 @@
   1.131      --> (\<exists>t. 0 < t &
   1.132                t \<le> h &
   1.133                f h =
   1.134 -              (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
   1.135 +              (\<Sum>m<n. diff m 0 / real (fact m) * h ^ m) +
   1.136                diff n t / real (fact n) * h ^ n)"
   1.137  by (blast intro: Maclaurin2)
   1.138  
   1.139 @@ -216,7 +206,7 @@
   1.140    assumes "h < 0" "0 < n" "diff 0 = f"
   1.141    and DERIV: "\<forall>m t. m < n & h \<le> t & t \<le> 0 --> DERIV (diff m) t :> diff (Suc m) t"
   1.142    shows "\<exists>t. h < t & t < 0 &
   1.143 -         f h = (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
   1.144 +         f h = (\<Sum>m<n. diff m 0 / real (fact m) * h ^ m) +
   1.145           diff n t / real (fact n) * h ^ n"
   1.146  proof -
   1.147    txt "Transform @{text ABL'} into @{text DERIV_intros} format."
   1.148 @@ -224,7 +214,7 @@
   1.149    from assms
   1.150    have "\<exists>t>0. t < - h \<and>
   1.151      f (- (- h)) =
   1.152 -    (\<Sum>m = 0..<n.
   1.153 +    (\<Sum>m<n.
   1.154      (- 1) ^ m * diff m (- 0) / real (fact m) * (- h) ^ m) +
   1.155      (- 1) ^ n * diff n (- t) / real (fact n) * (- h) ^ n"
   1.156      by (intro Maclaurin) (auto intro!: DERIV_intros DERIV')
   1.157 @@ -233,12 +223,12 @@
   1.158    have "-1 ^ n * diff n (- t) * (- h) ^ n / real (fact n) = diff n (- t) * h ^ n / real (fact n)"
   1.159      by (auto simp add: power_mult_distrib[symmetric])
   1.160    moreover
   1.161 -  have "(SUM m = 0..<n. -1 ^ m * diff m 0 * (- h) ^ m / real (fact m)) = (SUM m = 0..<n. diff m 0 * h ^ m / real (fact m))"
   1.162 +  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.163      by (auto intro: setsum_cong simp add: power_mult_distrib[symmetric])
   1.164    ultimately have " h < - t \<and>
   1.165      - t < 0 \<and>
   1.166      f h =
   1.167 -    (\<Sum>m = 0..<n. diff m 0 / real (fact m) * h ^ m) + diff n (- t) / real (fact n) * h ^ n"
   1.168 +    (\<Sum>m<n. diff m 0 / real (fact m) * h ^ m) + diff n (- t) / real (fact n) * h ^ n"
   1.169      by auto
   1.170    thus ?thesis ..
   1.171  qed
   1.172 @@ -250,7 +240,7 @@
   1.173      --> (\<exists>t. h < t &
   1.174                t < 0 &
   1.175                f h =
   1.176 -              (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
   1.177 +              (\<Sum>m<n. diff m 0 / real (fact m) * h ^ m) +
   1.178                diff n t / real (fact n) * h ^ n)"
   1.179  by (blast intro: Maclaurin_minus)
   1.180  
   1.181 @@ -262,7 +252,7 @@
   1.182  lemma Maclaurin_bi_le_lemma [rule_format]:
   1.183    "n>0 \<longrightarrow>
   1.184     diff 0 0 =
   1.185 -   (\<Sum>m = 0..<n. diff m 0 * 0 ^ m / real (fact m)) +
   1.186 +   (\<Sum>m<n. diff m 0 * 0 ^ m / real (fact m)) +
   1.187     diff n 0 * 0 ^ n / real (fact n)"
   1.188  by (induct "n") auto
   1.189  
   1.190 @@ -271,7 +261,7 @@
   1.191     and DERIV : "\<forall>m t. m < n & abs t \<le> abs x --> DERIV (diff m) t :> diff (Suc m) t"
   1.192     shows "\<exists>t. abs t \<le> abs x &
   1.193                f x =
   1.194 -              (\<Sum>m=0..<n. diff m 0 / real (fact m) * x ^ m) +
   1.195 +              (\<Sum>m<n. diff m 0 / real (fact m) * x ^ m) +
   1.196       diff n t / real (fact n) * x ^ n" (is "\<exists>t. _ \<and> f x = ?f x t")
   1.197  proof cases
   1.198    assume "n = 0" with `diff 0 = f` show ?thesis by force
   1.199 @@ -303,7 +293,7 @@
   1.200    assumes INIT1: "diff 0 = f" and INIT2: "0 < n" and INIT3: "x \<noteq> 0"
   1.201    and DERIV: "\<forall>m x. DERIV (diff m) x :> diff(Suc m) x"
   1.202    shows "\<exists>t. 0 < abs t & abs t < abs x & f x =
   1.203 -    (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
   1.204 +    (\<Sum>m<n. (diff m 0 / real (fact m)) * x ^ m) +
   1.205                  (diff n t / real (fact n)) * x ^ n" (is "\<exists>t. _ \<and> _ \<and> f x = ?f x t")
   1.206  proof (cases rule: linorder_cases)
   1.207    assume "x = 0" with INIT3 show "?thesis"..
   1.208 @@ -327,14 +317,14 @@
   1.209        (\<forall>m x. DERIV (diff m) x :> diff(Suc m) x) &
   1.210        x ~= 0 & n > 0
   1.211        --> (\<exists>t. 0 < abs t & abs t < abs x &
   1.212 -               f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
   1.213 +               f x = (\<Sum>m<n. (diff m 0 / real (fact m)) * x ^ m) +
   1.214                       (diff n t / real (fact n)) * x ^ n)"
   1.215  by (blast intro: Maclaurin_all_lt)
   1.216  
   1.217  lemma Maclaurin_zero [rule_format]:
   1.218       "x = (0::real)
   1.219        ==> n \<noteq> 0 -->
   1.220 -          (\<Sum>m=0..<n. (diff m (0::real) / real (fact m)) * x ^ m) =
   1.221 +          (\<Sum>m<n. (diff m (0::real) / real (fact m)) * x ^ m) =
   1.222            diff 0 0"
   1.223  by (induct n, auto)
   1.224  
   1.225 @@ -343,7 +333,7 @@
   1.226    assumes INIT: "diff 0 = f"
   1.227    and DERIV: "\<forall>m x. DERIV (diff m) x :> diff (Suc m) x"
   1.228    shows "\<exists>t. abs t \<le> abs x & f x =
   1.229 -    (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
   1.230 +    (\<Sum>m<n. (diff m 0 / real (fact m)) * x ^ m) +
   1.231      (diff n t / real (fact n)) * x ^ n" (is "\<exists>t. _ \<and> f x = ?f x t")
   1.232  proof cases
   1.233    assume "n = 0" with INIT show ?thesis by force
   1.234 @@ -352,7 +342,7 @@
   1.235    show ?thesis
   1.236    proof cases
   1.237      assume "x = 0"
   1.238 -    with `n \<noteq> 0` have "(\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) = diff 0 0"
   1.239 +    with `n \<noteq> 0` have "(\<Sum>m<n. diff m 0 / real (fact m) * x ^ m) = diff 0 0"
   1.240        by (intro Maclaurin_zero) auto
   1.241      with INIT `x = 0` `n \<noteq> 0` have " \<bar>0\<bar> \<le> \<bar>x\<bar> \<and> f x = ?f x 0" by force
   1.242      thus ?thesis ..
   1.243 @@ -369,7 +359,7 @@
   1.244  lemma Maclaurin_all_le_objl: "diff 0 = f &
   1.245        (\<forall>m x. DERIV (diff m) x :> diff (Suc m) x)
   1.246        --> (\<exists>t. abs t \<le> abs x &
   1.247 -              f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
   1.248 +              f x = (\<Sum>m<n. (diff m 0 / real (fact m)) * x ^ m) +
   1.249                      (diff n t / real (fact n)) * x ^ n)"
   1.250  by (blast intro: Maclaurin_all_le)
   1.251  
   1.252 @@ -379,14 +369,14 @@
   1.253  lemma Maclaurin_exp_lt: "[| x ~= 0; n > 0 |]
   1.254        ==> (\<exists>t. 0 < abs t &
   1.255                  abs t < abs x &
   1.256 -                exp x = (\<Sum>m=0..<n. (x ^ m) / real (fact m)) +
   1.257 +                exp x = (\<Sum>m<n. (x ^ m) / real (fact m)) +
   1.258                          (exp t / real (fact n)) * x ^ n)"
   1.259  by (cut_tac diff = "%n. exp" and f = exp and x = x and n = n in Maclaurin_all_lt_objl, auto)
   1.260  
   1.261  
   1.262  lemma Maclaurin_exp_le:
   1.263       "\<exists>t. abs t \<le> abs x &
   1.264 -            exp x = (\<Sum>m=0..<n. (x ^ m) / real (fact m)) +
   1.265 +            exp x = (\<Sum>m<n. (x ^ m) / real (fact m)) +
   1.266                         (exp t / real (fact n)) * x ^ n"
   1.267  by (cut_tac diff = "%n. exp" and f = exp and x = x and n = n in Maclaurin_all_le_objl, auto)
   1.268  
   1.269 @@ -420,7 +410,7 @@
   1.270  lemma Maclaurin_sin_expansion2:
   1.271       "\<exists>t. abs t \<le> abs x &
   1.272         sin x =
   1.273 -       (\<Sum>m=0..<n. sin_coeff m * x ^ m)
   1.274 +       (\<Sum>m<n. sin_coeff m * x ^ m)
   1.275        + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
   1.276  apply (cut_tac f = sin and n = n and x = x
   1.277          and diff = "%n x. sin (x + 1/2*real n * pi)" in Maclaurin_all_lt_objl)
   1.278 @@ -440,7 +430,7 @@
   1.279  
   1.280  lemma Maclaurin_sin_expansion:
   1.281       "\<exists>t. sin x =
   1.282 -       (\<Sum>m=0..<n. sin_coeff m * x ^ m)
   1.283 +       (\<Sum>m<n. sin_coeff m * x ^ m)
   1.284        + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
   1.285  apply (insert Maclaurin_sin_expansion2 [of x n])
   1.286  apply (blast intro: elim:)
   1.287 @@ -450,7 +440,7 @@
   1.288       "[| n > 0; 0 < x |] ==>
   1.289         \<exists>t. 0 < t & t < x &
   1.290         sin x =
   1.291 -       (\<Sum>m=0..<n. sin_coeff m * x ^ m)
   1.292 +       (\<Sum>m<n. sin_coeff m * x ^ m)
   1.293        + ((sin(t + 1/2 * real(n) *pi) / real (fact n)) * x ^ n)"
   1.294  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.295  apply safe
   1.296 @@ -467,7 +457,7 @@
   1.297       "0 < x ==>
   1.298         \<exists>t. 0 < t & t \<le> x &
   1.299         sin x =
   1.300 -       (\<Sum>m=0..<n. sin_coeff m * x ^ m)
   1.301 +       (\<Sum>m<n. sin_coeff m * x ^ m)
   1.302        + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
   1.303  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.304  apply safe
   1.305 @@ -484,7 +474,7 @@
   1.306  subsection{*Maclaurin Expansion for Cosine Function*}
   1.307  
   1.308  lemma sumr_cos_zero_one [simp]:
   1.309 -  "(\<Sum>m=0..<(Suc n). cos_coeff m * 0 ^ m) = 1"
   1.310 +  "(\<Sum>m<(Suc n). cos_coeff m * 0 ^ m) = 1"
   1.311  by (induct "n", auto)
   1.312  
   1.313  lemma cos_expansion_lemma:
   1.314 @@ -494,14 +484,14 @@
   1.315  lemma Maclaurin_cos_expansion:
   1.316       "\<exists>t. abs t \<le> abs x &
   1.317         cos x =
   1.318 -       (\<Sum>m=0..<n. cos_coeff m * x ^ m)
   1.319 +       (\<Sum>m<n. cos_coeff m * x ^ m)
   1.320        + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
   1.321  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.322  apply safe
   1.323  apply (simp (no_asm))
   1.324  apply (simp (no_asm) add: cos_expansion_lemma)
   1.325  apply (case_tac "n", simp)
   1.326 -apply (simp del: setsum_op_ivl_Suc)
   1.327 +apply (simp del: setsum_lessThan_Suc)
   1.328  apply (rule ccontr, simp)
   1.329  apply (drule_tac x = x in spec, simp)
   1.330  apply (erule ssubst)
   1.331 @@ -514,7 +504,7 @@
   1.332       "[| 0 < x; n > 0 |] ==>
   1.333         \<exists>t. 0 < t & t < x &
   1.334         cos x =
   1.335 -       (\<Sum>m=0..<n. cos_coeff m * x ^ m)
   1.336 +       (\<Sum>m<n. cos_coeff m * x ^ m)
   1.337        + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
   1.338  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.339  apply safe
   1.340 @@ -530,7 +520,7 @@
   1.341       "[| x < 0; n > 0 |] ==>
   1.342         \<exists>t. x < t & t < 0 &
   1.343         cos x =
   1.344 -       (\<Sum>m=0..<n. cos_coeff m * x ^ m)
   1.345 +       (\<Sum>m<n. cos_coeff m * x ^ m)
   1.346        + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
   1.347  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.348  apply safe
   1.349 @@ -551,7 +541,7 @@
   1.350  by auto
   1.351  
   1.352  lemma Maclaurin_sin_bound:
   1.353 -  "abs(sin x - (\<Sum>m=0..<n. sin_coeff m * x ^ m))
   1.354 +  "abs(sin x - (\<Sum>m<n. sin_coeff m * x ^ m))
   1.355    \<le> inverse(real (fact n)) * \<bar>x\<bar> ^ n"
   1.356  proof -
   1.357    have "!! x (y::real). x \<le> 1 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x * y \<le> 1 * y"
   1.358 @@ -567,7 +557,7 @@
   1.359      done
   1.360    from Maclaurin_all_le [OF diff_0 DERIV_diff]
   1.361    obtain t where t1: "\<bar>t\<bar> \<le> \<bar>x\<bar>" and
   1.362 -    t2: "sin x = (\<Sum>m = 0..<n. ?diff m 0 / real (fact m) * x ^ m) +
   1.363 +    t2: "sin x = (\<Sum>m<n. ?diff m 0 / real (fact m) * x ^ m) +
   1.364        ?diff n t / real (fact n) * x ^ n" by fast
   1.365    have diff_m_0:
   1.366      "\<And>m. ?diff m 0 = (if even m then 0