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)