src/HOL/MacLaurin.thy
changeset 58410 6d46ad54a2ab
parent 57514 bdc2c6b40bf2
child 58709 efdc6c533bd3
     1.1 --- a/src/HOL/MacLaurin.thy	Sun Sep 21 16:56:06 2014 +0200
     1.2 +++ b/src/HOL/MacLaurin.thy	Sun Sep 21 16:56:11 2014 +0200
     1.3 @@ -221,10 +221,10 @@
     1.4      by (intro Maclaurin) (auto intro!: derivative_eq_intros DERIV')
     1.5    then guess t ..
     1.6    moreover
     1.7 -  have "-1 ^ n * diff n (- t) * (- h) ^ n / real (fact n) = diff n (- t) * h ^ n / real (fact n)"
     1.8 +  have "(- 1) ^ n * diff n (- t) * (- h) ^ n / real (fact n) = diff n (- t) * h ^ n / real (fact n)"
     1.9      by (auto simp add: power_mult_distrib[symmetric])
    1.10    moreover
    1.11 -  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.12 +  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.13      by (auto intro: setsum.cong simp add: power_mult_distrib[symmetric])
    1.14    ultimately have " h < - t \<and>
    1.15      - t < 0 \<and>
    1.16 @@ -561,7 +561,7 @@
    1.17        ?diff n t / real (fact n) * x ^ n" by fast
    1.18    have diff_m_0:
    1.19      "\<And>m. ?diff m 0 = (if even m then 0
    1.20 -         else -1 ^ ((m - Suc 0) div 2))"
    1.21 +         else (- 1) ^ ((m - Suc 0) div 2))"
    1.22      apply (subst even_even_mod_4_iff)
    1.23      apply (cut_tac m=m in mod_exhaust_less_4)
    1.24      apply (elim disjE, simp_all)