1.1 --- a/src/HOL/Hyperreal/MacLaurin.thy Sat Feb 19 18:44:34 2005 +0100
1.2 +++ b/src/HOL/Hyperreal/MacLaurin.thy Mon Feb 21 15:04:10 2005 +0100
1.3 @@ -9,25 +9,32 @@
1.4 imports Log
1.5 begin
1.6
1.7 -lemma sumr_offset: "sumr 0 n (%m. f (m+k)) = sumr 0 (n+k) f - sumr 0 k f"
1.8 +(* FIXME generalize? *)
1.9 +lemma sumr_offset:
1.10 + "(\<Sum>m=0..<n::nat. f(m+k)::real) = setsum f {0..<n+k} - setsum f {0..<k}"
1.11 by (induct "n", auto)
1.12
1.13 -lemma sumr_offset2: "\<forall>f. sumr 0 n (%m. f (m+k)) = sumr 0 (n+k) f - sumr 0 k f"
1.14 +lemma sumr_offset2:
1.15 + "\<forall>f. (\<Sum>m=0..<n::nat. f(m+k)::real) = setsum f {0..<n+k} - setsum f {0..<k}"
1.16 by (induct "n", auto)
1.17
1.18 -lemma sumr_offset3: "sumr 0 (n+k) f = sumr 0 n (%m. f (m+k)) + sumr 0 k f"
1.19 +lemma sumr_offset3:
1.20 + "setsum f {0::nat..<n+k} = (\<Sum>m=0..<n. f (m+k)::real) + setsum f {0..<k}"
1.21 by (simp add: sumr_offset)
1.22
1.23 -lemma sumr_offset4: "\<forall>n f. sumr 0 (n+k) f = sumr 0 n (%m. f (m+k)) + sumr 0 k f"
1.24 +lemma sumr_offset4:
1.25 + "\<forall>n f. setsum f {0::nat..<n+k} =
1.26 + (\<Sum>m=0..<n. f (m+k)::real) + setsum f {0..<k}"
1.27 by (simp add: sumr_offset)
1.28
1.29 +(*
1.30 lemma sumr_from_1_from_0: "0 < n ==>
1.31 - sumr (Suc 0) (Suc n) (%n. (if even(n) then 0 else
1.32 - ((- 1) ^ ((n - (Suc 0)) div 2))/(real (fact n))) * a ^ n) =
1.33 - sumr 0 (Suc n) (%n. (if even(n) then 0 else
1.34 - ((- 1) ^ ((n - (Suc 0)) div 2))/(real (fact n))) * a ^ n)"
1.35 + (\<Sum>n=Suc 0 ..< Suc n. if even(n) then 0 else
1.36 + ((- 1) ^ ((n - (Suc 0)) div 2))/(real (fact n))) * a ^ n =
1.37 + (\<Sum>n=0..<Suc n. if even(n) then 0 else
1.38 + ((- 1) ^ ((n - (Suc 0)) div 2))/(real (fact n))) * a ^ n"
1.39 by (rule_tac n1 = 1 in sumr_split_add [THEN subst], auto)
1.40 -
1.41 +*)
1.42
1.43 subsection{*Maclaurin's Theorem with Lagrange Form of Remainder*}
1.44
1.45 @@ -36,12 +43,12 @@
1.46
1.47 lemma Maclaurin_lemma:
1.48 "0 < h ==>
1.49 - \<exists>B. f h = sumr 0 n (%m. (j m / real (fact m)) * (h^m)) +
1.50 + \<exists>B. f h = (\<Sum>m=0..<n. (j m / real (fact m)) * (h^m)) +
1.51 (B * ((h^n) / real(fact n)))"
1.52 -apply (rule_tac x = "(f h - sumr 0 n (%m. (j m / real (fact m)) * h^m)) *
1.53 +apply (rule_tac x = "(f h - (\<Sum>m=0..<n. (j m / real (fact m)) * h^m)) *
1.54 real(fact n) / (h^n)"
1.55 in exI)
1.56 -apply (simp add: times_divide_eq)
1.57 +apply (simp)
1.58 done
1.59
1.60 lemma eq_diff_eq': "(x = y - z) = (y = x + (z::real))"
1.61 @@ -92,9 +99,9 @@
1.62 prefer 3 apply (simp add: fact_diff_Suc)
1.63 prefer 2 apply simp
1.64 apply (frule_tac m = m in less_add_one, clarify)
1.65 -apply (simp del: sumr_Suc)
1.66 +apply (simp del: setsum_Suc)
1.67 apply (insert sumr_offset4 [of 1])
1.68 -apply (simp del: sumr_Suc fact_Suc realpow_Suc)
1.69 +apply (simp del: setsum_Suc fact_Suc realpow_Suc)
1.70 apply (rule lemma_DERIV_subst)
1.71 apply (rule DERIV_add)
1.72 apply (rule_tac [2] DERIV_const)
1.73 @@ -106,7 +113,7 @@
1.74 apply (best intro: DERIV_chain2 intro!: DERIV_intros)
1.75 apply (subst fact_Suc)
1.76 apply (subst real_of_nat_mult)
1.77 -apply (simp add: inverse_mult_distrib mult_ac)
1.78 +apply (simp add: mult_ac)
1.79 done
1.80
1.81
1.82 @@ -137,7 +144,7 @@
1.83 ==> \<exists>t. 0 < t &
1.84 t < h &
1.85 f h =
1.86 - sumr 0 n (%m. (diff m 0 / real (fact m)) * h ^ m) +
1.87 + setsum (%m. (diff m 0 / real (fact m)) * h ^ m) {0..<n} +
1.88 (diff n t / real (fact n)) * h ^ n"
1.89 apply (case_tac "n = 0", force)
1.90 apply (drule not0_implies_Suc)
1.91 @@ -145,15 +152,15 @@
1.92 apply (frule_tac f=f and n=n and j="%m. diff m 0" in Maclaurin_lemma)
1.93 apply (erule exE)
1.94 apply (subgoal_tac "\<exists>g.
1.95 - g = (%t. f t - (sumr 0 n (%m. (diff m 0 / real(fact m)) * t^m) + (B * (t^n / real(fact n)))))")
1.96 + g = (%t. f t - (setsum (%m. (diff m 0 / real(fact m)) * t^m) {0..<n} + (B * (t^n / real(fact n)))))")
1.97 prefer 2 apply blast
1.98 apply (erule exE)
1.99 apply (subgoal_tac "g 0 = 0 & g h =0")
1.100 prefer 2
1.101 - apply (simp del: sumr_Suc)
1.102 + apply (simp del: setsum_Suc)
1.103 apply (cut_tac n = m and k = 1 in sumr_offset2)
1.104 - apply (simp add: eq_diff_eq' del: sumr_Suc)
1.105 -apply (subgoal_tac "\<exists>difg. difg = (%m t. diff m t - (sumr 0 (n - m) (%p. (diff (m + p) 0 / real (fact p)) * (t ^ p)) + (B * ((t ^ (n - m)) / real (fact (n - m))))))")
1.106 + apply (simp add: eq_diff_eq' del: setsum_Suc)
1.107 +apply (subgoal_tac "\<exists>difg. difg = (%m t. diff m t - (setsum (%p. (diff (m + p) 0 / real (fact p)) * (t ^ p)) {0..<n-m} + (B * ((t ^ (n - m)) / real (fact (n - m))))))")
1.108 prefer 2 apply blast
1.109 apply (erule exE)
1.110 apply (subgoal_tac "difg 0 = g")
1.111 @@ -165,15 +172,15 @@
1.112 apply (simp (no_asm_simp))
1.113 apply (erule exE)
1.114 apply (rule_tac x = t in exI)
1.115 - apply (simp add: times_divide_eq del: realpow_Suc fact_Suc)
1.116 + apply (simp del: realpow_Suc fact_Suc)
1.117 apply (subgoal_tac "\<forall>m. m < n --> difg m 0 = 0")
1.118 prefer 2
1.119 apply clarify
1.120 apply simp
1.121 apply (frule_tac m = ma in less_add_one, clarify)
1.122 - apply (simp del: sumr_Suc)
1.123 + apply (simp del: setsum_Suc)
1.124 apply (insert sumr_offset4 [of 1])
1.125 -apply (simp del: sumr_Suc fact_Suc realpow_Suc)
1.126 +apply (simp del: setsum_Suc fact_Suc realpow_Suc)
1.127 apply (subgoal_tac "\<forall>m. m < n --> (\<exists>t. 0 < t & t < h & DERIV (difg m) t :> 0) ")
1.128 apply (rule allI, rule impI)
1.129 apply (drule_tac x = ma and P="%m. m<n --> (\<exists>t. ?QQ m t)" in spec)
1.130 @@ -181,11 +188,11 @@
1.131 apply (erule exE)
1.132 apply (rule_tac x = t in exI)
1.133 (* do some tidying up *)
1.134 -apply (erule_tac [!] V= "difg = (%m t. diff m t - (sumr 0 (n - m) (%p. diff (m + p) 0 / real (fact p) * t ^ p) + B * (t ^ (n - m) / real (fact (n - m)))))"
1.135 +apply (erule_tac [!] V= "difg = (%m t. diff m t - (setsum (%p. diff (m + p) 0 / real (fact p) * t ^ p) {0..<n-m} + B * (t ^ (n - m) / real (fact (n - m)))))"
1.136 in thin_rl)
1.137 -apply (erule_tac [!] V="g = (%t. f t - (sumr 0 n (%m. diff m 0 / real (fact m) * t ^ m) + B * (t ^ n / real (fact n))))"
1.138 +apply (erule_tac [!] V="g = (%t. f t - (setsum (%m. diff m 0 / real (fact m) * t ^ m) {0..<n} + B * (t ^ n / real (fact n))))"
1.139 in thin_rl)
1.140 -apply (erule_tac [!] V="f h = sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) + B * (h ^ n / real (fact n))"
1.141 +apply (erule_tac [!] V="f h = setsum (%m. diff m 0 / real (fact m) * h ^ m) {0..<n} + B * (h ^ n / real (fact n))"
1.142 in thin_rl)
1.143 (* back to business *)
1.144 apply (simp (no_asm_simp))
1.145 @@ -215,7 +222,7 @@
1.146 --> (\<exists>t. 0 < t &
1.147 t < h &
1.148 f h =
1.149 - sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) +
1.150 + (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
1.151 diff n t / real (fact n) * h ^ n)"
1.152 by (blast intro: Maclaurin)
1.153
1.154 @@ -227,7 +234,7 @@
1.155 ==> \<exists>t. 0 < t &
1.156 t \<le> h &
1.157 f h =
1.158 - sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) +
1.159 + (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
1.160 diff n t / real (fact n) * h ^ n"
1.161 apply (case_tac "n", auto)
1.162 apply (drule Maclaurin, auto)
1.163 @@ -240,7 +247,7 @@
1.164 --> (\<exists>t. 0 < t &
1.165 t \<le> h &
1.166 f h =
1.167 - sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) +
1.168 + (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
1.169 diff n t / real (fact n) * h ^ n)"
1.170 by (blast intro: Maclaurin2)
1.171
1.172 @@ -250,12 +257,12 @@
1.173 ==> \<exists>t. h < t &
1.174 t < 0 &
1.175 f h =
1.176 - sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) +
1.177 + (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
1.178 diff n t / real (fact n) * h ^ n"
1.179 apply (cut_tac f = "%x. f (-x)"
1.180 and diff = "%n x. ((- 1) ^ n) * diff n (-x)"
1.181 and h = "-h" and n = n in Maclaurin_objl)
1.182 -apply (simp add: times_divide_eq)
1.183 +apply (simp)
1.184 apply safe
1.185 apply (subst minus_mult_right)
1.186 apply (rule DERIV_cmult)
1.187 @@ -278,7 +285,7 @@
1.188 --> (\<exists>t. h < t &
1.189 t < 0 &
1.190 f h =
1.191 - sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) +
1.192 + (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
1.193 diff n t / real (fact n) * h ^ n)"
1.194 by (blast intro: Maclaurin_minus)
1.195
1.196 @@ -299,12 +306,12 @@
1.197 \<forall>m t. m < n & abs t \<le> abs x --> DERIV (diff m) t :> diff (Suc m) t |]
1.198 ==> \<exists>t. abs t \<le> abs x &
1.199 f x =
1.200 - sumr 0 n (%m. diff m 0 / real (fact m) * x ^ m) +
1.201 + (\<Sum>m=0..<n. diff m 0 / real (fact m) * x ^ m) +
1.202 diff n t / real (fact n) * x ^ n"
1.203 apply (case_tac "n = 0", force)
1.204 apply (case_tac "x = 0")
1.205 apply (rule_tac x = 0 in exI)
1.206 -apply (force simp add: Maclaurin_bi_le_lemma times_divide_eq)
1.207 +apply (force simp add: Maclaurin_bi_le_lemma)
1.208 apply (cut_tac x = x and y = 0 in linorder_less_linear, auto)
1.209 txt{*Case 1, where @{term "x < 0"}*}
1.210 apply (cut_tac f = "diff 0" and diff = diff and h = x and n = n in Maclaurin_minus_objl, safe)
1.211 @@ -323,7 +330,7 @@
1.212 \<forall>m x. DERIV (diff m) x :> diff(Suc m) x;
1.213 x ~= 0; 0 < n
1.214 |] ==> \<exists>t. 0 < abs t & abs t < abs x &
1.215 - f x = sumr 0 n (%m. (diff m 0 / real (fact m)) * x ^ m) +
1.216 + f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
1.217 (diff n t / real (fact n)) * x ^ n"
1.218 apply (rule_tac x = x and y = 0 in linorder_cases)
1.219 prefer 2 apply blast
1.220 @@ -337,21 +344,21 @@
1.221 (\<forall>m x. DERIV (diff m) x :> diff(Suc m) x) &
1.222 x ~= 0 & 0 < n
1.223 --> (\<exists>t. 0 < abs t & abs t < abs x &
1.224 - f x = sumr 0 n (%m. (diff m 0 / real (fact m)) * x ^ m) +
1.225 + f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
1.226 (diff n t / real (fact n)) * x ^ n)"
1.227 by (blast intro: Maclaurin_all_lt)
1.228
1.229 lemma Maclaurin_zero [rule_format]:
1.230 "x = (0::real)
1.231 ==> 0 < n -->
1.232 - sumr 0 n (%m. (diff m (0::real) / real (fact m)) * x ^ m) =
1.233 + (\<Sum>m=0..<n. (diff m (0::real) / real (fact m)) * x ^ m) =
1.234 diff 0 0"
1.235 by (induct n, auto)
1.236
1.237 lemma Maclaurin_all_le: "[| diff 0 = f;
1.238 \<forall>m x. DERIV (diff m) x :> diff (Suc m) x
1.239 |] ==> \<exists>t. abs t \<le> abs x &
1.240 - f x = sumr 0 n (%m. (diff m 0 / real (fact m)) * x ^ m) +
1.241 + f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
1.242 (diff n t / real (fact n)) * x ^ n"
1.243 apply (insert linorder_le_less_linear [of n 0])
1.244 apply (erule disjE, force)
1.245 @@ -366,7 +373,7 @@
1.246 lemma Maclaurin_all_le_objl: "diff 0 = f &
1.247 (\<forall>m x. DERIV (diff m) x :> diff (Suc m) x)
1.248 --> (\<exists>t. abs t \<le> abs x &
1.249 - f x = sumr 0 n (%m. (diff m 0 / real (fact m)) * x ^ m) +
1.250 + f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
1.251 (diff n t / real (fact n)) * x ^ n)"
1.252 by (blast intro: Maclaurin_all_le)
1.253
1.254 @@ -376,14 +383,14 @@
1.255 lemma Maclaurin_exp_lt: "[| x ~= 0; 0 < n |]
1.256 ==> (\<exists>t. 0 < abs t &
1.257 abs t < abs x &
1.258 - exp x = sumr 0 n (%m. (x ^ m) / real (fact m)) +
1.259 + exp x = (\<Sum>m=0..<n. (x ^ m) / real (fact m)) +
1.260 (exp t / real (fact n)) * x ^ n)"
1.261 by (cut_tac diff = "%n. exp" and f = exp and x = x and n = n in Maclaurin_all_lt_objl, auto)
1.262
1.263
1.264 lemma Maclaurin_exp_le:
1.265 "\<exists>t. abs t \<le> abs x &
1.266 - exp x = sumr 0 n (%m. (x ^ m) / real (fact m)) +
1.267 + exp x = (\<Sum>m=0..<n. (x ^ m) / real (fact m)) +
1.268 (exp t / real (fact n)) * x ^ n"
1.269 by (cut_tac diff = "%n. exp" and f = exp and x = x and n = n in Maclaurin_all_le_objl, auto)
1.270
1.271 @@ -421,29 +428,29 @@
1.272 lemma Maclaurin_sin_expansion2:
1.273 "\<exists>t. abs t \<le> abs x &
1.274 sin x =
1.275 - (sumr 0 n (%m. (if even m then 0
1.276 + (\<Sum>m=0..<n. (if even m then 0
1.277 else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) *
1.278 - x ^ m))
1.279 + x ^ m)
1.280 + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
1.281 apply (cut_tac f = sin and n = n and x = x
1.282 and diff = "%n x. sin (x + 1/2*real n * pi)" in Maclaurin_all_lt_objl)
1.283 apply safe
1.284 apply (simp (no_asm))
1.285 -apply (simp (no_asm) add: times_divide_eq)
1.286 +apply (simp (no_asm))
1.287 apply (case_tac "n", clarify, simp, simp)
1.288 apply (rule ccontr, simp)
1.289 apply (drule_tac x = x in spec, simp)
1.290 apply (erule ssubst)
1.291 apply (rule_tac x = t in exI, simp)
1.292 apply (rule setsum_cong[OF refl])
1.293 -apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex times_divide_eq)
1.294 +apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex)
1.295 done
1.296
1.297 lemma Maclaurin_sin_expansion:
1.298 "\<exists>t. sin x =
1.299 - (sumr 0 n (%m. (if even m then 0
1.300 + (\<Sum>m=0..<n. (if even m then 0
1.301 else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) *
1.302 - x ^ m))
1.303 + x ^ m)
1.304 + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
1.305 apply (insert Maclaurin_sin_expansion2 [of x n])
1.306 apply (blast intro: elim:);
1.307 @@ -455,63 +462,60 @@
1.308 "[| 0 < n; 0 < x |] ==>
1.309 \<exists>t. 0 < t & t < x &
1.310 sin x =
1.311 - (sumr 0 n (%m. (if even m then 0
1.312 + (\<Sum>m=0..<n. (if even m then 0
1.313 else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) *
1.314 - x ^ m))
1.315 + x ^ m)
1.316 + ((sin(t + 1/2 * real(n) *pi) / real (fact n)) * x ^ n)"
1.317 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.318 apply safe
1.319 apply simp
1.320 -apply (simp (no_asm) add: times_divide_eq)
1.321 +apply (simp (no_asm))
1.322 apply (erule ssubst)
1.323 apply (rule_tac x = t in exI, simp)
1.324 apply (rule setsum_cong[OF refl])
1.325 -apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex times_divide_eq)
1.326 +apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex)
1.327 done
1.328
1.329 lemma Maclaurin_sin_expansion4:
1.330 "0 < x ==>
1.331 \<exists>t. 0 < t & t \<le> x &
1.332 sin x =
1.333 - (sumr 0 n (%m. (if even m then 0
1.334 + (\<Sum>m=0..<n. (if even m then 0
1.335 else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) *
1.336 - x ^ m))
1.337 + x ^ m)
1.338 + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
1.339 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.340 apply safe
1.341 apply simp
1.342 -apply (simp (no_asm) add: times_divide_eq)
1.343 +apply (simp (no_asm))
1.344 apply (erule ssubst)
1.345 apply (rule_tac x = t in exI, simp)
1.346 apply (rule setsum_cong[OF refl])
1.347 -apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex times_divide_eq)
1.348 +apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex)
1.349 done
1.350
1.351
1.352 subsection{*Maclaurin Expansion for Cosine Function*}
1.353
1.354 lemma sumr_cos_zero_one [simp]:
1.355 - "sumr 0 (Suc n)
1.356 - (%m. (if even m
1.357 - then (- 1) ^ (m div 2)/(real (fact m))
1.358 - else 0) *
1.359 - 0 ^ m) = 1"
1.360 + "(\<Sum>m=0..<(Suc n).
1.361 + (if even m then (- 1) ^ (m div 2)/(real (fact m)) else 0) * 0 ^ m) = 1"
1.362 by (induct "n", auto)
1.363
1.364 lemma Maclaurin_cos_expansion:
1.365 "\<exists>t. abs t \<le> abs x &
1.366 cos x =
1.367 - (sumr 0 n (%m. (if even m
1.368 + (\<Sum>m=0..<n. (if even m
1.369 then (- 1) ^ (m div 2)/(real (fact m))
1.370 else 0) *
1.371 - x ^ m))
1.372 + x ^ m)
1.373 + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
1.374 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.375 apply safe
1.376 apply (simp (no_asm))
1.377 -apply (simp (no_asm) add: times_divide_eq)
1.378 +apply (simp (no_asm))
1.379 apply (case_tac "n", simp)
1.380 -apply (simp del: sumr_Suc)
1.381 +apply (simp del: setsum_Suc)
1.382 apply (rule ccontr, simp)
1.383 apply (drule_tac x = x in spec, simp)
1.384 apply (erule ssubst)
1.385 @@ -524,15 +528,15 @@
1.386 "[| 0 < x; 0 < n |] ==>
1.387 \<exists>t. 0 < t & t < x &
1.388 cos x =
1.389 - (sumr 0 n (%m. (if even m
1.390 + (\<Sum>m=0..<n. (if even m
1.391 then (- 1) ^ (m div 2)/(real (fact m))
1.392 else 0) *
1.393 - x ^ m))
1.394 + x ^ m)
1.395 + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
1.396 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.397 apply safe
1.398 apply simp
1.399 -apply (simp (no_asm) add: times_divide_eq)
1.400 +apply (simp (no_asm))
1.401 apply (erule ssubst)
1.402 apply (rule_tac x = t in exI, simp)
1.403 apply (rule setsum_cong[OF refl])
1.404 @@ -543,15 +547,15 @@
1.405 "[| x < 0; 0 < n |] ==>
1.406 \<exists>t. x < t & t < 0 &
1.407 cos x =
1.408 - (sumr 0 n (%m. (if even m
1.409 + (\<Sum>m=0..<n. (if even m
1.410 then (- 1) ^ (m div 2)/(real (fact m))
1.411 else 0) *
1.412 - x ^ m))
1.413 + x ^ m)
1.414 + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
1.415 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.416 apply safe
1.417 apply simp
1.418 -apply (simp (no_asm) add: times_divide_eq)
1.419 +apply (simp (no_asm))
1.420 apply (erule ssubst)
1.421 apply (rule_tac x = t in exI, simp)
1.422 apply (rule setsum_cong[OF refl])
1.423 @@ -567,7 +571,7 @@
1.424 by auto
1.425
1.426 lemma Maclaurin_sin_bound:
1.427 - "abs(sin x - sumr 0 n (%m. (if even m then 0 else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) *
1.428 + "abs(sin x - (\<Sum>m=0..<n. (if even m then 0 else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) *
1.429 x ^ m)) \<le> inverse(real (fact n)) * \<bar>x\<bar> ^ n"
1.430 proof -
1.431 have "!! x (y::real). x \<le> 1 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x * y \<le> 1 * y"