src/HOL/Fact.thy
changeset 28952 15a4b2cf8c34
parent 28944 e27abf0db984
child 29693 708dcf7dec9f
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Fact.thy	Wed Dec 03 15:58:44 2008 +0100
     1.3 @@ -0,0 +1,76 @@
     1.4 +(*  Title       : Fact.thy
     1.5 +    Author      : Jacques D. Fleuriot
     1.6 +    Copyright   : 1998  University of Cambridge
     1.7 +    Conversion to Isar and new proofs by Lawrence C Paulson, 2004
     1.8 +*)
     1.9 +
    1.10 +header{*Factorial Function*}
    1.11 +
    1.12 +theory Fact
    1.13 +imports RealDef
    1.14 +begin
    1.15 +
    1.16 +consts fact :: "nat => nat"
    1.17 +primrec
    1.18 +  fact_0:     "fact 0 = 1"
    1.19 +  fact_Suc:   "fact (Suc n) = (Suc n) * fact n"
    1.20 +
    1.21 +
    1.22 +lemma fact_gt_zero [simp]: "0 < fact n"
    1.23 +by (induct n) auto
    1.24 +
    1.25 +lemma fact_not_eq_zero [simp]: "fact n \<noteq> 0"
    1.26 +by simp
    1.27 +
    1.28 +lemma real_of_nat_fact_not_zero [simp]: "real (fact n) \<noteq> 0"
    1.29 +by auto
    1.30 +
    1.31 +lemma real_of_nat_fact_gt_zero [simp]: "0 < real(fact n)"
    1.32 +by auto
    1.33 +
    1.34 +lemma real_of_nat_fact_ge_zero [simp]: "0 \<le> real(fact n)"
    1.35 +by simp
    1.36 +
    1.37 +lemma fact_ge_one [simp]: "1 \<le> fact n"
    1.38 +by (induct n) auto
    1.39 +
    1.40 +lemma fact_mono: "m \<le> n ==> fact m \<le> fact n"
    1.41 +apply (drule le_imp_less_or_eq)
    1.42 +apply (auto dest!: less_imp_Suc_add)
    1.43 +apply (induct_tac k, auto)
    1.44 +done
    1.45 +
    1.46 +text{*Note that @{term "fact 0 = fact 1"}*}
    1.47 +lemma fact_less_mono: "[| 0 < m; m < n |] ==> fact m < fact n"
    1.48 +apply (drule_tac m = m in less_imp_Suc_add, auto)
    1.49 +apply (induct_tac k, auto)
    1.50 +done
    1.51 +
    1.52 +lemma inv_real_of_nat_fact_gt_zero [simp]: "0 < inverse (real (fact n))"
    1.53 +by (auto simp add: positive_imp_inverse_positive)
    1.54 +
    1.55 +lemma inv_real_of_nat_fact_ge_zero [simp]: "0 \<le> inverse (real (fact n))"
    1.56 +by (auto intro: order_less_imp_le)
    1.57 +
    1.58 +lemma fact_diff_Suc [rule_format]:
    1.59 +  "n < Suc m ==> fact (Suc m - n) = (Suc m - n) * fact (m - n)"
    1.60 +apply (induct n arbitrary: m)
    1.61 +apply auto
    1.62 +apply (drule_tac x = "m - 1" in meta_spec, auto)
    1.63 +done
    1.64 +
    1.65 +lemma fact_num0 [simp]: "fact 0 = 1"
    1.66 +by auto
    1.67 +
    1.68 +lemma fact_num_eq_if: "fact m = (if m=0 then 1 else m * fact (m - 1))"
    1.69 +by (cases m) auto
    1.70 +
    1.71 +lemma fact_add_num_eq_if:
    1.72 +  "fact (m + n) = (if m + n = 0 then 1 else (m + n) * fact (m + n - 1))"
    1.73 +by (cases "m + n") auto
    1.74 +
    1.75 +lemma fact_add_num_eq_if2:
    1.76 +  "fact (m + n) = (if m = 0 then fact n else (m + n) * fact ((m - 1) + n))"
    1.77 +by (cases m) auto
    1.78 +
    1.79 +end