src/HOL/Hyperreal/Fact.thy
 changeset 15094 a7d1a3fdc30d parent 12196 a3be6b3a9c0b child 15131 c69542757a4d
```     1.1 --- a/src/HOL/Hyperreal/Fact.thy	Fri Jul 30 18:37:58 2004 +0200
1.2 +++ b/src/HOL/Hyperreal/Fact.thy	Sat Jul 31 20:54:23 2004 +0200
1.3 @@ -1,14 +1,74 @@
1.4 -(*  Title       : Fact.thy
1.5 +(*  Title       : Fact.thy
1.6      Author      : Jacques D. Fleuriot
1.7      Copyright   : 1998  University of Cambridge
1.8 -    Description : Factorial function
1.9 +    Conversion to Isar and new proofs by Lawrence C Paulson, 2004
1.10  *)
1.11
1.12 -Fact = NatStar +
1.13 +header{*Factorial Function*}
1.14 +
1.15 +theory Fact = Real:
1.16 +
1.17 +consts fact :: "nat => nat"
1.18 +primrec
1.19 +   fact_0:     "fact 0 = 1"
1.20 +   fact_Suc:   "fact (Suc n) = (Suc n) * fact n"
1.21 +
1.22 +
1.23 +lemma fact_gt_zero [simp]: "0 < fact n"
1.24 +by (induct "n", auto)
1.25 +
1.26 +lemma fact_not_eq_zero [simp]: "fact n \<noteq> 0"
1.27 +by simp
1.28 +
1.29 +lemma real_of_nat_fact_not_zero [simp]: "real (fact n) \<noteq> 0"
1.30 +by auto
1.31 +
1.32 +lemma real_of_nat_fact_gt_zero [simp]: "0 < real(fact n)"
1.33 +by auto
1.34 +
1.35 +lemma real_of_nat_fact_ge_zero [simp]: "0 \<le> real(fact n)"
1.36 +by simp
1.37 +
1.38 +lemma fact_ge_one [simp]: "1 \<le> fact n"
1.39 +by (induct "n", auto)
1.40
1.41 -consts fact :: nat => nat
1.42 -primrec
1.43 -   fact_0     "fact 0 = 1"
1.44 -   fact_Suc   "fact (Suc n) = (Suc n) * fact n"
1.45 +lemma fact_mono: "m \<le> n ==> fact m \<le> fact n"
1.46 +apply (drule le_imp_less_or_eq)
1.47 +apply (auto dest!: less_imp_Suc_add)
1.48 +apply (induct_tac "k", auto)
1.49 +done
1.50 +
1.51 +text{*Note that @{term "fact 0 = fact 1"}*}
1.52 +lemma fact_less_mono: "[| 0 < m; m < n |] ==> fact m < fact n"
1.53 +apply (drule_tac m = m in less_imp_Suc_add, auto)
1.54 +apply (induct_tac "k", auto)
1.55 +done
1.56 +
1.57 +lemma inv_real_of_nat_fact_gt_zero [simp]: "0 < inverse (real (fact n))"
1.58 +by (auto simp add: positive_imp_inverse_positive)
1.59 +
1.60 +lemma inv_real_of_nat_fact_ge_zero [simp]: "0 \<le> inverse (real (fact n))"
1.61 +by (auto intro: order_less_imp_le)
1.62 +
1.63 +lemma fact_diff_Suc [rule_format]:
1.64 +     "\<forall>m. n < Suc m --> fact (Suc m - n) = (Suc m - n) * fact (m - n)"
1.65 +apply (induct n, auto)
1.66 +apply (drule_tac x = "m - 1" in spec, auto)
1.67 +done
1.68 +
1.69 +lemma fact_num0 [simp]: "fact 0 = 1"
1.70 +by auto
1.71 +
1.72 +lemma fact_num_eq_if: "fact m = (if m=0 then 1 else m * fact (m - 1))"
1.73 +by (case_tac "m", auto)
1.74 +
1.75 +lemma fact_add_num_eq_if:
1.76 +     "fact (m+n) = (if (m+n = 0) then 1 else (m+n) * (fact (m + n - 1)))"
1.77 +by (case_tac "m+n", auto)
1.78 +
1.79 +lemma fact_add_num_eq_if2:
1.80 +     "fact (m+n) = (if m=0 then fact n else (m+n) * (fact ((m - 1) + n)))"
1.81 +by (case_tac "m", auto)
1.82 +
1.83
1.84  end
1.85 \ No newline at end of file
```