src/HOL/MacLaurin.thy
changeset 56381 0556204bc230
parent 56238 5d147e1e18d1
child 56536 aefb4a8da31f
     1.1 --- a/src/HOL/MacLaurin.thy	Thu Apr 03 17:16:02 2014 +0200
     1.2 +++ b/src/HOL/MacLaurin.thy	Thu Apr 03 17:56:08 2014 +0200
     1.3 @@ -40,7 +40,8 @@
     1.4    have "DERIV (difg m) t :> diff (Suc m) t -
     1.5      ((\<Sum>x<n - m. real x * t ^ (x - Suc 0) * diff (m + x) 0 / real (fact x)) +
     1.6       real (n - m) * t ^ (n - Suc m) * B / real (fact (n - m)))" unfolding difg_def
     1.7 -    by (auto intro!: DERIV_intros DERIV[rule_format, OF INIT2])
     1.8 +    by (auto intro!: derivative_eq_intros DERIV[rule_format, OF INIT2]
     1.9 +             simp: real_of_nat_def[symmetric])
    1.10    moreover
    1.11    from INIT2 have intvl: "{..<n - m} = insert 0 (Suc ` {..<n - Suc m})" and "0 < n - m"
    1.12      unfolding atLeast0LessThan[symmetric] by auto
    1.13 @@ -209,7 +210,7 @@
    1.14           f h = (\<Sum>m<n. diff m 0 / real (fact m) * h ^ m) +
    1.15           diff n t / real (fact n) * h ^ n"
    1.16  proof -
    1.17 -  txt "Transform @{text ABL'} into @{text DERIV_intros} format."
    1.18 +  txt "Transform @{text ABL'} into @{text derivative_intros} format."
    1.19    note DERIV' = DERIV_chain'[OF _ DERIV[rule_format], THEN DERIV_cong]
    1.20    from assms
    1.21    have "\<exists>t>0. t < - h \<and>
    1.22 @@ -217,7 +218,7 @@
    1.23      (\<Sum>m<n.
    1.24      (- 1) ^ m * diff m (- 0) / real (fact m) * (- h) ^ m) +
    1.25      (- 1) ^ n * diff n (- t) / real (fact n) * (- h) ^ n"
    1.26 -    by (intro Maclaurin) (auto intro!: DERIV_intros DERIV')
    1.27 +    by (intro Maclaurin) (auto intro!: derivative_eq_intros DERIV')
    1.28    then guess t ..
    1.29    moreover
    1.30    have "-1 ^ n * diff n (- t) * (- h) ^ n / real (fact n) = diff n (- t) * h ^ n / real (fact n)"
    1.31 @@ -417,7 +418,7 @@
    1.32  apply safe
    1.33  apply (simp (no_asm))
    1.34  apply (simp (no_asm) add: sin_expansion_lemma)
    1.35 -apply (force intro!: DERIV_intros)
    1.36 +apply (force intro!: derivative_eq_intros)
    1.37  apply (subst (asm) setsum_0', clarify, case_tac "x", simp, simp)
    1.38  apply (cases n, simp, simp)
    1.39  apply (rule ccontr, simp)
    1.40 @@ -446,7 +447,7 @@
    1.41  apply safe
    1.42  apply simp
    1.43  apply (simp (no_asm) add: sin_expansion_lemma)
    1.44 -apply (force intro!: DERIV_intros)
    1.45 +apply (force intro!: derivative_eq_intros)
    1.46  apply (erule ssubst)
    1.47  apply (rule_tac x = t in exI, simp)
    1.48  apply (rule setsum_cong[OF refl])
    1.49 @@ -463,7 +464,7 @@
    1.50  apply safe
    1.51  apply simp
    1.52  apply (simp (no_asm) add: sin_expansion_lemma)
    1.53 -apply (force intro!: DERIV_intros)
    1.54 +apply (force intro!: derivative_eq_intros)
    1.55  apply (erule ssubst)
    1.56  apply (rule_tac x = t in exI, simp)
    1.57  apply (rule setsum_cong[OF refl])
    1.58 @@ -553,7 +554,7 @@
    1.59      apply (clarify)
    1.60      apply (subst (1 2 3) mod_Suc_eq_Suc_mod)
    1.61      apply (cut_tac m=m in mod_exhaust_less_4)
    1.62 -    apply (safe, auto intro!: DERIV_intros)
    1.63 +    apply (safe, auto intro!: derivative_eq_intros)
    1.64      done
    1.65    from Maclaurin_all_le [OF diff_0 DERIV_diff]
    1.66    obtain t where t1: "\<bar>t\<bar> \<le> \<bar>x\<bar>" and