author  wenzelm 
Fri, 02 Jun 2006 23:22:29 +0200  
changeset 19765  dfe940911617 
parent 15241  a3949068537e 
child 20503  503ac4c5ef91 
permissions  rwrr 
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

1 
(* Title : Fact.thy 
12196  2 
Author : Jacques D. Fleuriot 
3 
Copyright : 1998 University of Cambridge 

15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

4 
Conversion to Isar and new proofs by Lawrence C Paulson, 2004 
12196  5 
*) 
6 

15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

7 
header{*Factorial Function*} 
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

8 

15131  9 
theory Fact 
15241  10 
imports "../Real/Real" 
15131  11 
begin 
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

12 

a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

13 
consts fact :: "nat => nat" 
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

14 
primrec 
19765  15 
fact_0: "fact 0 = 1" 
16 
fact_Suc: "fact (Suc n) = (Suc n) * fact n" 

15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

17 

a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

18 

a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

19 
lemma fact_gt_zero [simp]: "0 < fact n" 
19765  20 
by (induct n) auto 
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

21 

a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

22 
lemma fact_not_eq_zero [simp]: "fact n \<noteq> 0" 
19765  23 
by simp 
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

24 

a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

25 
lemma real_of_nat_fact_not_zero [simp]: "real (fact n) \<noteq> 0" 
19765  26 
by auto 
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

27 

a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

28 
lemma real_of_nat_fact_gt_zero [simp]: "0 < real(fact n)" 
19765  29 
by auto 
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

30 

a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

31 
lemma real_of_nat_fact_ge_zero [simp]: "0 \<le> real(fact n)" 
19765  32 
by simp 
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

33 

a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

34 
lemma fact_ge_one [simp]: "1 \<le> fact n" 
19765  35 
by (induct n) auto 
12196  36 

15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

37 
lemma fact_mono: "m \<le> n ==> fact m \<le> fact n" 
19765  38 
apply (drule le_imp_less_or_eq) 
39 
apply (auto dest!: less_imp_Suc_add) 

40 
apply (induct_tac k, auto) 

41 
done 

15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

42 

a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

43 
text{*Note that @{term "fact 0 = fact 1"}*} 
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

44 
lemma fact_less_mono: "[ 0 < m; m < n ] ==> fact m < fact n" 
19765  45 
apply (drule_tac m = m in less_imp_Suc_add, auto) 
46 
apply (induct_tac k, auto) 

47 
done 

15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

48 

a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

49 
lemma inv_real_of_nat_fact_gt_zero [simp]: "0 < inverse (real (fact n))" 
19765  50 
by (auto simp add: positive_imp_inverse_positive) 
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

51 

a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

52 
lemma inv_real_of_nat_fact_ge_zero [simp]: "0 \<le> inverse (real (fact n))" 
19765  53 
by (auto intro: order_less_imp_le) 
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

54 

a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

55 
lemma fact_diff_Suc [rule_format]: 
19765  56 
"n < Suc m ==> fact (Suc m  n) = (Suc m  n) * fact (m  n)" 
57 
apply (induct n fixing: m) 

58 
apply auto 

59 
apply (drule_tac x = "m  1" in meta_spec, auto) 

60 
done 

15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

61 

a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

62 
lemma fact_num0 [simp]: "fact 0 = 1" 
19765  63 
by auto 
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

64 

a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

65 
lemma fact_num_eq_if: "fact m = (if m=0 then 1 else m * fact (m  1))" 
19765  66 
by (cases m) auto 
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

67 

a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

68 
lemma fact_add_num_eq_if: 
19765  69 
"fact (m + n) = (if m + n = 0 then 1 else (m + n) * fact (m + n  1))" 
70 
by (cases "m + n") auto 

15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

71 

a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

72 
lemma fact_add_num_eq_if2: 
19765  73 
"fact (m + n) = (if m = 0 then fact n else (m + n) * fact ((m  1) + n))" 
74 
by (cases m) auto 

12196  75 

15131  76 
end 