author  paulson 
Sat, 31 Jul 2004 20:54:23 +0200  
changeset 15094  a7d1a3fdc30d 
parent 12196  a3be6b3a9c0b 
child 15131  c69542757a4d 
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 

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

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

10 

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

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

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

13 
fact_0: "fact 0 = 1" 
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

14 
fact_Suc: "fact (Suc n) = (Suc n) * fact n" 
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

15 

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

16 

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

17 
lemma fact_gt_zero [simp]: "0 < fact n" 
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

18 
by (induct "n", auto) 
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

19 

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

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

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

22 

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

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

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

25 

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

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

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

28 

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

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

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

31 

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

32 
lemma fact_ge_one [simp]: "1 \<le> fact n" 
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

33 
by (induct "n", auto) 
12196  34 

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

35 
lemma fact_mono: "m \<le> n ==> fact m \<le> fact n" 
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

36 
apply (drule le_imp_less_or_eq) 
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

37 
apply (auto dest!: less_imp_Suc_add) 
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

38 
apply (induct_tac "k", auto) 
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

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

40 

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

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

42 
lemma fact_less_mono: "[ 0 < m; m < n ] ==> fact m < fact n" 
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

43 
apply (drule_tac m = m in less_imp_Suc_add, auto) 
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

44 
apply (induct_tac "k", auto) 
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

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

46 

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

47 
lemma inv_real_of_nat_fact_gt_zero [simp]: "0 < inverse (real (fact n))" 
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

48 
by (auto simp add: positive_imp_inverse_positive) 
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

49 

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

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

51 
by (auto intro: order_less_imp_le) 
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

52 

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

53 
lemma fact_diff_Suc [rule_format]: 
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

54 
"\<forall>m. n < Suc m > fact (Suc m  n) = (Suc m  n) * fact (m  n)" 
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

55 
apply (induct n, auto) 
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

56 
apply (drule_tac x = "m  1" in spec, auto) 
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

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

58 

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

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

60 
by auto 
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_num_eq_if: "fact m = (if m=0 then 1 else m * fact (m  1))" 
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

63 
by (case_tac "m", auto) 
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_add_num_eq_if: 
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

66 
"fact (m+n) = (if (m+n = 0) then 1 else (m+n) * (fact (m + n  1)))" 
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

67 
by (case_tac "m+n", auto) 
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

68 

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

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

70 
"fact (m+n) = (if m=0 then fact n else (m+n) * (fact ((m  1) + n)))" 
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

71 
by (case_tac "m", auto) 
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

72 

12196  73 

74 
end 