src/HOL/MacLaurin.thy

     apply (rule_tac [2] DERIV_pow)
    prefer 3 apply (simp add: fact_diff_Suc)
   prefer 2 apply simp
  apply (frule less_iff_Suc_add [THEN iffD1], clarify)
  apply (simp del: setsum_op_ivl_Suc)
- apply (insert sumr_offset4 [of 1])
+ apply (insert sumr_offset4 [of "Suc 0"])
  apply (simp del: setsum_op_ivl_Suc fact_Suc realpow_Suc)
  apply (rule lemma_DERIV_subst)
   apply (rule DERIV_add)
    apply (rule_tac [2] DERIV_const)
   apply (rule DERIV_sumr, clarify)

     (setsum (%m. (diff m 0 / real(fact m)) * t^m) {0..<n}
       + (B * (t^n / real(fact n)))))" by blast
 
   have g2: "g 0 = 0 & g h = 0"
     apply (simp add: m f_h g_def del: setsum_op_ivl_Suc)
-    apply (cut_tac n = m and k = 1 in sumr_offset2)
+    apply (cut_tac n = m and k = "Suc 0" in sumr_offset2)
     apply (simp add: eq_diff_eq' diff_0 del: setsum_op_ivl_Suc)
     done
 
   obtain difg where difg_def: "difg = (%m t. diff m t -
     (setsum (%p. (diff (m + p) 0 / real (fact p)) * (t ^ p)) {0..<n-m}

   have difg_eq_0: "\<forall>m. m < n --> difg m 0 = 0"
     apply clarify
     apply (simp add: m difg_def)
     apply (frule less_iff_Suc_add [THEN iffD1], clarify)
     apply (simp del: setsum_op_ivl_Suc)
-    apply (insert sumr_offset4 [of 1])
+    apply (insert sumr_offset4 [of "Suc 0"])
     apply (simp del: setsum_op_ivl_Suc fact_Suc realpow_Suc)
     done
 
   have isCont_difg: "\<And>m x. \<lbrakk>m < n; 0 \<le> x; x \<le> h\<rbrakk> \<Longrightarrow> isCont (difg m) x"
     by (rule DERIV_isCont [OF difg_Suc [rule_format]]) simp

 (* ------------------------------------------------------------------------- *)
 
 lemma sin_bound_lemma:
     "[|x = y; abs u \<le> (v::real) |] ==> \<bar>(x + u) - y\<bar> \<le> v"
 by auto
+
+text {* TODO: move to Parity.thy *}
+lemma nat_odd_1 [simp]: "odd (1::nat)"
+  unfolding even_nat_def by simp
 
 lemma Maclaurin_sin_bound:
   "abs(sin x - (\<Sum>m=0..<n. (if even m then 0 else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) *
   x ^ m))  \<le> inverse(real (fact n)) * \<bar>x\<bar> ^ n"
 proof -