Repaired uses of factorial.

--- a/src/HOL/Ln.thy	Fri Jul 10 10:45:49 2009 -0400
+++ b/src/HOL/Ln.thy	Fri Jul 10 12:55:06 2009 -0400
@@ -31,13 +31,13 @@
 qed
 
 lemma aux1: assumes a: "0 <= x" and b: "x <= 1"
-    shows "inverse (real (fact (n + 2))) * x ^ (n + 2) <= (x^2/2) * ((1/2)^n)"
+    shows "inverse (real (fact ((n::nat) + 2))) * x ^ (n + 2) <= (x^2/2) * ((1/2)^n)"
 proof (induct n)
-  show "inverse (real (fact (0 + 2))) * x ^ (0 + 2) <= 
+  show "inverse (real (fact ((0::nat) + 2))) * x ^ (0 + 2) <= 
       x ^ 2 / 2 * (1 / 2) ^ 0"
     by (simp add: real_of_nat_Suc power2_eq_square)
 next
-  fix n
+  fix n :: nat
   assume c: "inverse (real (fact (n + 2))) * x ^ (n + 2)
        <= x ^ 2 / 2 * (1 / 2) ^ n"
   show "inverse (real (fact (Suc n + 2))) * x ^ (Suc n + 2)

--- a/src/HOL/MacLaurin.thy	Fri Jul 10 10:45:49 2009 -0400
+++ b/src/HOL/MacLaurin.thy	Fri Jul 10 12:55:06 2009 -0400
@@ -27,6 +27,10 @@
 lemma eq_diff_eq': "(x = y - z) = (y = x + (z::real))"
 by arith
 
+lemma fact_diff_Suc [rule_format]:
+  "n < Suc m ==> fact (Suc m - n) = (Suc m - n) * fact (m - n)"
+  by (subst fact_reduce_nat, auto)
+
 lemma Maclaurin_lemma2:
   assumes diff: "\<forall>m t. m < n \<and> 0\<le>t \<and> t\<le>h \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
   assumes n: "n = Suc k"
@@ -47,22 +51,24 @@
    apply (rule_tac [2] DERIV_quotient)
      apply (rule_tac [3] DERIV_const)
     apply (rule_tac [2] DERIV_pow)
-   prefer 3 apply (simp add: fact_diff_Suc)
+   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 "Suc 0"])
- apply (simp del: setsum_op_ivl_Suc fact_Suc power_Suc)
+ apply (simp del: setsum_op_ivl_Suc fact_Suc_nat power_Suc)
  apply (rule lemma_DERIV_subst)
   apply (rule DERIV_add)
    apply (rule_tac [2] DERIV_const)
   apply (rule DERIV_sumr, clarify)
   prefer 2 apply simp
- apply (simp (no_asm) add: divide_inverse mult_assoc del: fact_Suc power_Suc)
+ apply (simp (no_asm) add: divide_inverse mult_assoc del: fact_Suc_nat power_Suc)
  apply (rule DERIV_cmult)
  apply (rule lemma_DERIV_subst)
   apply (best intro!: DERIV_intros)
- apply (subst fact_Suc)
+ apply (subst fact_Suc_nat)
  apply (subst real_of_nat_mult)
  apply (simp add: mult_ac)
 done
@@ -114,7 +120,7 @@
     apply (frule less_iff_Suc_add [THEN iffD1], clarify)
     apply (simp del: setsum_op_ivl_Suc)
     apply (insert sumr_offset4 [of "Suc 0"])
-    apply (simp del: setsum_op_ivl_Suc fact_Suc)
+    apply (simp del: setsum_op_ivl_Suc fact_Suc_nat)
     done
 
   have isCont_difg: "\<And>m x. \<lbrakk>m < n; 0 \<le> x; x \<le> h\<rbrakk> \<Longrightarrow> isCont (difg m) x"
@@ -174,7 +180,7 @@
       (\<Sum>m = 0..<n. diff m 0 / real (fact m) * h ^ m) +
       diff n t / real (fact n) * h ^ n"
       using `difg (Suc m) t = 0`
-      by (simp add: m f_h difg_def del: fact_Suc)
+      by (simp add: m f_h difg_def del: fact_Suc_nat)
   qed
 
 qed