src/HOL/MacLaurin.thy
changeset 30082 43c5b7bfc791
parent 29811 026b0f9f579f
child 30273 ecd6f0ca62ea
     1.1 --- a/src/HOL/MacLaurin.thy	Tue Feb 24 11:10:05 2009 -0800
     1.2 +++ b/src/HOL/MacLaurin.thy	Tue Feb 24 11:12:58 2009 -0800
     1.3 @@ -81,7 +81,7 @@
     1.4    prefer 2 apply simp
     1.5   apply (frule less_iff_Suc_add [THEN iffD1], clarify)
     1.6   apply (simp del: setsum_op_ivl_Suc)
     1.7 - apply (insert sumr_offset4 [of 1])
     1.8 + apply (insert sumr_offset4 [of "Suc 0"])
     1.9   apply (simp del: setsum_op_ivl_Suc fact_Suc realpow_Suc)
    1.10   apply (rule lemma_DERIV_subst)
    1.11    apply (rule DERIV_add)
    1.12 @@ -124,7 +124,7 @@
    1.13  
    1.14    have g2: "g 0 = 0 & g h = 0"
    1.15      apply (simp add: m f_h g_def del: setsum_op_ivl_Suc)
    1.16 -    apply (cut_tac n = m and k = 1 in sumr_offset2)
    1.17 +    apply (cut_tac n = m and k = "Suc 0" in sumr_offset2)
    1.18      apply (simp add: eq_diff_eq' diff_0 del: setsum_op_ivl_Suc)
    1.19      done
    1.20  
    1.21 @@ -144,7 +144,7 @@
    1.22      apply (simp add: m difg_def)
    1.23      apply (frule less_iff_Suc_add [THEN iffD1], clarify)
    1.24      apply (simp del: setsum_op_ivl_Suc)
    1.25 -    apply (insert sumr_offset4 [of 1])
    1.26 +    apply (insert sumr_offset4 [of "Suc 0"])
    1.27      apply (simp del: setsum_op_ivl_Suc fact_Suc realpow_Suc)
    1.28      done
    1.29  
    1.30 @@ -552,6 +552,10 @@
    1.31      "[|x = y; abs u \<le> (v::real) |] ==> \<bar>(x + u) - y\<bar> \<le> v"
    1.32  by auto
    1.33  
    1.34 +text {* TODO: move to Parity.thy *}
    1.35 +lemma nat_odd_1 [simp]: "odd (1::nat)"
    1.36 +  unfolding even_nat_def by simp
    1.37 +
    1.38  lemma Maclaurin_sin_bound:
    1.39    "abs(sin x - (\<Sum>m=0..<n. (if even m then 0 else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) *
    1.40    x ^ m))  \<le> inverse(real (fact n)) * \<bar>x\<bar> ^ n"