author  huffman 
Mon, 23 Feb 2009 07:58:13 0800  
changeset 30073  a4ad0c08b7d9 
parent 29693  708dcf7dec9f 
child 30082  43c5b7bfc791 
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 
30073  10 
imports Main 
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" 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

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" 
25162  23 
by simp 
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

24 

29693
708dcf7dec9f
moved upwards in thy graph, real related theorems moved to Transcendental.thy
chaieb
parents:
28952
diff
changeset

25 
lemma of_nat_fact_not_zero [simp]: "of_nat (fact n) \<noteq> (0::'a::semiring_char_0)" 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

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

27 

29693
708dcf7dec9f
moved upwards in thy graph, real related theorems moved to Transcendental.thy
chaieb
parents:
28952
diff
changeset

28 
class ordered_semiring_1 = ordered_semiring + semiring_1 
708dcf7dec9f
moved upwards in thy graph, real related theorems moved to Transcendental.thy
chaieb
parents:
28952
diff
changeset

29 
class ordered_semiring_1_strict = ordered_semiring_strict + semiring_1 
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset

30 

29693
708dcf7dec9f
moved upwards in thy graph, real related theorems moved to Transcendental.thy
chaieb
parents:
28952
diff
changeset

31 
lemma of_nat_fact_gt_zero [simp]: "(0::'a::{ordered_semidom}) < of_nat(fact n)" by auto 
708dcf7dec9f
moved upwards in thy graph, real related theorems moved to Transcendental.thy
chaieb
parents:
28952
diff
changeset

32 

708dcf7dec9f
moved upwards in thy graph, real related theorems moved to Transcendental.thy
chaieb
parents:
28952
diff
changeset

33 
lemma of_nat_fact_ge_zero [simp]: "(0::'a::ordered_semidom) \<le> of_nat(fact n)" 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

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

35 

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

36 
lemma fact_ge_one [simp]: "1 \<le> fact n" 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

37 
by (induct n) auto 
12196  38 

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

39 
lemma fact_mono: "m \<le> n ==> fact m \<le> fact n" 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

40 
apply (drule le_imp_less_or_eq) 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

41 
apply (auto dest!: less_imp_Suc_add) 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

42 
apply (induct_tac k, auto) 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

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

44 

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

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

46 
lemma fact_less_mono: "[ 0 < m; m < n ] ==> fact m < fact n" 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

47 
apply (drule_tac m = m in less_imp_Suc_add, auto) 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

48 
apply (induct_tac k, auto) 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

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

50 

29693
708dcf7dec9f
moved upwards in thy graph, real related theorems moved to Transcendental.thy
chaieb
parents:
28952
diff
changeset

51 
lemma inv_of_nat_fact_gt_zero [simp]: "(0::'a::ordered_field) < inverse (of_nat (fact n))" 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

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

53 

29693
708dcf7dec9f
moved upwards in thy graph, real related theorems moved to Transcendental.thy
chaieb
parents:
28952
diff
changeset

54 
lemma inv_of_nat_fact_ge_zero [simp]: "(0::'a::ordered_field) \<le> inverse (of_nat (fact n))" 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

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

56 

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

57 
lemma fact_diff_Suc [rule_format]: 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

58 
"n < Suc m ==> fact (Suc m  n) = (Suc m  n) * fact (m  n)" 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

59 
apply (induct n arbitrary: m) 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

60 
apply auto 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

61 
apply (drule_tac x = "m  1" in meta_spec, auto) 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

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

63 

29693
708dcf7dec9f
moved upwards in thy graph, real related theorems moved to Transcendental.thy
chaieb
parents:
28952
diff
changeset

64 
lemma fact_num0: "fact 0 = 1" 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

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

66 

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

67 
lemma fact_num_eq_if: "fact m = (if m=0 then 1 else m * fact (m  1))" 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

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

69 

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

70 
lemma fact_add_num_eq_if: 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

71 
"fact (m + n) = (if m + n = 0 then 1 else (m + n) * fact (m + n  1))" 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

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

73 

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

74 
lemma fact_add_num_eq_if2: 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

75 
"fact (m + n) = (if m = 0 then fact n else (m + n) * fact ((m  1) + n))" 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

76 
by (cases m) auto 
12196  77 

15131  78 
end 