src/HOL/MacLaurin.thy
 changeset 63040 eb4ddd18d635 parent 61954 1d43f86f48be child 63365 5340fb6633d0
```     1.1 --- a/src/HOL/MacLaurin.thy	Sun Apr 24 21:31:14 2016 +0200
1.2 +++ b/src/HOL/MacLaurin.thy	Mon Apr 25 16:09:26 2016 +0200
1.3 @@ -85,22 +85,22 @@
1.4          (\<Sum>m<n. diff m (0::real) / (fact m) * h ^ m) + B * (h ^ n / (fact n))"
1.5      using Maclaurin_lemma [OF h] ..
1.6
1.7 -  def g \<equiv> "(\<lambda>t. f t -
1.8 -    (setsum (\<lambda>m. (diff m 0 / (fact m)) * t^m) {..<n} + (B * (t^n / (fact n)))))"
1.9 +  define g where [abs_def]: "g t =
1.10 +    f t - (setsum (\<lambda>m. (diff m 0 / (fact m)) * t^m) {..<n} + (B * (t^n / (fact n))))" for t
1.11
1.12    have g2: "g 0 = 0 & g h = 0"
1.13      by (simp add: m f_h g_def lessThan_Suc_eq_insert_0 image_iff diff_0 setsum.reindex)
1.14
1.15 -  def difg \<equiv> "(%m t. diff m t -
1.16 -    (setsum (%p. (diff (m + p) 0 / (fact p)) * (t ^ p)) {..<n-m}
1.17 -      + (B * ((t ^ (n - m)) / (fact (n - m))))))"
1.18 +  define difg where [abs_def]: "difg m t =
1.19 +    diff m t - (setsum (%p. (diff (m + p) 0 / (fact p)) * (t ^ p)) {..<n-m}
1.20 +      + (B * ((t ^ (n - m)) / (fact (n - m)))))" for m t
1.21
1.22    have difg_0: "difg 0 = g"
1.23      unfolding difg_def g_def by (simp add: diff_0)
1.24
1.25    have difg_Suc: "\<forall>(m::nat) t::real.
1.26          m < n \<and> (0::real) \<le> t \<and> t \<le> h \<longrightarrow> DERIV (difg m) t :> difg (Suc m) t"
1.27 -    using diff_Suc m unfolding difg_def by (rule Maclaurin_lemma2)
1.28 +    using diff_Suc m unfolding difg_def [abs_def] by (rule Maclaurin_lemma2)
1.29
1.30    have difg_eq_0: "\<forall>m<n. difg m 0 = 0"
1.31      by (auto simp: difg_def m Suc_diff_le lessThan_Suc_eq_insert_0 image_iff setsum.reindex)
```