Repaired uses of factorial.
authoravigad
Fri Jul 10 12:55:06 2009 -0400 (2009-07-10)
changeset 320384127b89f48ab
parent 32037 bed71e0d83e6
child 32039 400a519bc888
child 32042 df28ead1cf19
Repaired uses of factorial.
src/HOL/Ln.thy
src/HOL/MacLaurin.thy
     1.1 --- a/src/HOL/Ln.thy	Fri Jul 10 10:45:49 2009 -0400
     1.2 +++ b/src/HOL/Ln.thy	Fri Jul 10 12:55:06 2009 -0400
     1.3 @@ -31,13 +31,13 @@
     1.4  qed
     1.5  
     1.6  lemma aux1: assumes a: "0 <= x" and b: "x <= 1"
     1.7 -    shows "inverse (real (fact (n + 2))) * x ^ (n + 2) <= (x^2/2) * ((1/2)^n)"
     1.8 +    shows "inverse (real (fact ((n::nat) + 2))) * x ^ (n + 2) <= (x^2/2) * ((1/2)^n)"
     1.9  proof (induct n)
    1.10 -  show "inverse (real (fact (0 + 2))) * x ^ (0 + 2) <= 
    1.11 +  show "inverse (real (fact ((0::nat) + 2))) * x ^ (0 + 2) <= 
    1.12        x ^ 2 / 2 * (1 / 2) ^ 0"
    1.13      by (simp add: real_of_nat_Suc power2_eq_square)
    1.14  next
    1.15 -  fix n
    1.16 +  fix n :: nat
    1.17    assume c: "inverse (real (fact (n + 2))) * x ^ (n + 2)
    1.18         <= x ^ 2 / 2 * (1 / 2) ^ n"
    1.19    show "inverse (real (fact (Suc n + 2))) * x ^ (Suc n + 2)
     2.1 --- a/src/HOL/MacLaurin.thy	Fri Jul 10 10:45:49 2009 -0400
     2.2 +++ b/src/HOL/MacLaurin.thy	Fri Jul 10 12:55:06 2009 -0400
     2.3 @@ -27,6 +27,10 @@
     2.4  lemma eq_diff_eq': "(x = y - z) = (y = x + (z::real))"
     2.5  by arith
     2.6  
     2.7 +lemma fact_diff_Suc [rule_format]:
     2.8 +  "n < Suc m ==> fact (Suc m - n) = (Suc m - n) * fact (m - n)"
     2.9 +  by (subst fact_reduce_nat, auto)
    2.10 +
    2.11  lemma Maclaurin_lemma2:
    2.12    assumes diff: "\<forall>m t. m < n \<and> 0\<le>t \<and> t\<le>h \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
    2.13    assumes n: "n = Suc k"
    2.14 @@ -47,22 +51,24 @@
    2.15     apply (rule_tac [2] DERIV_quotient)
    2.16       apply (rule_tac [3] DERIV_const)
    2.17      apply (rule_tac [2] DERIV_pow)
    2.18 -   prefer 3 apply (simp add: fact_diff_Suc)
    2.19 +   prefer 3 
    2.20 +
    2.21 +apply (simp add: fact_diff_Suc)
    2.22    prefer 2 apply simp
    2.23   apply (frule less_iff_Suc_add [THEN iffD1], clarify)
    2.24   apply (simp del: setsum_op_ivl_Suc)
    2.25   apply (insert sumr_offset4 [of "Suc 0"])
    2.26 - apply (simp del: setsum_op_ivl_Suc fact_Suc power_Suc)
    2.27 + apply (simp del: setsum_op_ivl_Suc fact_Suc_nat power_Suc)
    2.28   apply (rule lemma_DERIV_subst)
    2.29    apply (rule DERIV_add)
    2.30     apply (rule_tac [2] DERIV_const)
    2.31    apply (rule DERIV_sumr, clarify)
    2.32    prefer 2 apply simp
    2.33 - apply (simp (no_asm) add: divide_inverse mult_assoc del: fact_Suc power_Suc)
    2.34 + apply (simp (no_asm) add: divide_inverse mult_assoc del: fact_Suc_nat power_Suc)
    2.35   apply (rule DERIV_cmult)
    2.36   apply (rule lemma_DERIV_subst)
    2.37    apply (best intro!: DERIV_intros)
    2.38 - apply (subst fact_Suc)
    2.39 + apply (subst fact_Suc_nat)
    2.40   apply (subst real_of_nat_mult)
    2.41   apply (simp add: mult_ac)
    2.42  done
    2.43 @@ -114,7 +120,7 @@
    2.44      apply (frule less_iff_Suc_add [THEN iffD1], clarify)
    2.45      apply (simp del: setsum_op_ivl_Suc)
    2.46      apply (insert sumr_offset4 [of "Suc 0"])
    2.47 -    apply (simp del: setsum_op_ivl_Suc fact_Suc)
    2.48 +    apply (simp del: setsum_op_ivl_Suc fact_Suc_nat)
    2.49      done
    2.50  
    2.51    have isCont_difg: "\<And>m x. \<lbrakk>m < n; 0 \<le> x; x \<le> h\<rbrakk> \<Longrightarrow> isCont (difg m) x"
    2.52 @@ -174,7 +180,7 @@
    2.53        (\<Sum>m = 0..<n. diff m 0 / real (fact m) * h ^ m) +
    2.54        diff n t / real (fact n) * h ^ n"
    2.55        using `difg (Suc m) t = 0`
    2.56 -      by (simp add: m f_h difg_def del: fact_Suc)
    2.57 +      by (simp add: m f_h difg_def del: fact_Suc_nat)
    2.58    qed
    2.59  
    2.60  qed