author | wenzelm |
Sat, 13 Mar 2010 14:44:47 +0100 | |
changeset 35743 | c506c029a082 |
parent 35644 | d20cf282342e |
child 40033 | 84200d970bf0 |
permissions | -rw-r--r-- |
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 |
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
5 |
The integer version of factorial and other additions by Jeremy Avigad. |
12196 | 6 |
*) |
7 |
||
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset
|
8 |
header{*Factorial Function*} |
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset
|
9 |
|
15131 | 10 |
theory Fact |
33319 | 11 |
imports Main |
15131 | 12 |
begin |
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset
|
13 |
|
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
14 |
class fact = |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
15 |
|
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
16 |
fixes |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
17 |
fact :: "'a \<Rightarrow> 'a" |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
18 |
|
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
19 |
instantiation nat :: fact |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
20 |
|
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
21 |
begin |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
22 |
|
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
23 |
fun |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
24 |
fact_nat :: "nat \<Rightarrow> nat" |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
25 |
where |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
26 |
fact_0_nat: "fact_nat 0 = Suc 0" |
32047 | 27 |
| fact_Suc: "fact_nat (Suc x) = Suc x * fact x" |
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
28 |
|
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
29 |
instance proof qed |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
30 |
|
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
31 |
end |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
32 |
|
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
33 |
(* definitions for the integers *) |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
34 |
|
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
35 |
instantiation int :: fact |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
36 |
|
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
37 |
begin |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
38 |
|
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
39 |
definition |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
40 |
fact_int :: "int \<Rightarrow> int" |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
41 |
where |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
42 |
"fact_int x = (if x >= 0 then int (fact (nat x)) else 0)" |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
43 |
|
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
44 |
instance proof qed |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
45 |
|
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
46 |
end |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
47 |
|
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
48 |
|
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
49 |
subsection {* Set up Transfer *} |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
50 |
|
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
51 |
lemma transfer_nat_int_factorial: |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
52 |
"(x::int) >= 0 \<Longrightarrow> fact (nat x) = nat (fact x)" |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
53 |
unfolding fact_int_def |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
54 |
by auto |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
55 |
|
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
56 |
|
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
57 |
lemma transfer_nat_int_factorial_closure: |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
58 |
"x >= (0::int) \<Longrightarrow> fact x >= 0" |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
59 |
by (auto simp add: fact_int_def) |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
60 |
|
35644 | 61 |
declare transfer_morphism_nat_int[transfer add return: |
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
62 |
transfer_nat_int_factorial transfer_nat_int_factorial_closure] |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
63 |
|
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
64 |
lemma transfer_int_nat_factorial: |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
65 |
"fact (int x) = int (fact x)" |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
66 |
unfolding fact_int_def by auto |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
67 |
|
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
68 |
lemma transfer_int_nat_factorial_closure: |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
69 |
"is_nat x \<Longrightarrow> fact x >= 0" |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
70 |
by (auto simp add: fact_int_def) |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
71 |
|
35644 | 72 |
declare transfer_morphism_int_nat[transfer add return: |
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
73 |
transfer_int_nat_factorial transfer_int_nat_factorial_closure] |
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset
|
74 |
|
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset
|
75 |
|
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
76 |
subsection {* Factorial *} |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
77 |
|
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
78 |
lemma fact_0_int [simp]: "fact (0::int) = 1" |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
79 |
by (simp add: fact_int_def) |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
80 |
|
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
81 |
lemma fact_1_nat [simp]: "fact (1::nat) = 1" |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
82 |
by simp |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
83 |
|
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
84 |
lemma fact_Suc_0_nat [simp]: "fact (Suc 0) = Suc 0" |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
85 |
by simp |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
86 |
|
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
87 |
lemma fact_1_int [simp]: "fact (1::int) = 1" |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
88 |
by (simp add: fact_int_def) |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
89 |
|
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
90 |
lemma fact_plus_one_nat: "fact ((n::nat) + 1) = (n + 1) * fact n" |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
91 |
by simp |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
92 |
|
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
93 |
lemma fact_plus_one_int: |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
94 |
assumes "n >= 0" |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
95 |
shows "fact ((n::int) + 1) = (n + 1) * fact n" |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
96 |
|
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
97 |
using prems unfolding fact_int_def |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
98 |
by (simp add: nat_add_distrib algebra_simps int_mult) |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
99 |
|
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
100 |
lemma fact_reduce_nat: "(n::nat) > 0 \<Longrightarrow> fact n = n * fact (n - 1)" |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
101 |
apply (subgoal_tac "n = Suc (n - 1)") |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
102 |
apply (erule ssubst) |
32047 | 103 |
apply (subst fact_Suc) |
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
104 |
apply simp_all |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
105 |
done |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
106 |
|
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
107 |
lemma fact_reduce_int: "(n::int) > 0 \<Longrightarrow> fact n = n * fact (n - 1)" |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
108 |
apply (subgoal_tac "n = (n - 1) + 1") |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
109 |
apply (erule ssubst) |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
110 |
apply (subst fact_plus_one_int) |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
111 |
apply simp_all |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
112 |
done |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
113 |
|
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
114 |
lemma fact_nonzero_nat [simp]: "fact (n::nat) \<noteq> 0" |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
115 |
apply (induct n) |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
116 |
apply (auto simp add: fact_plus_one_nat) |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
117 |
done |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
118 |
|
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
119 |
lemma fact_nonzero_int [simp]: "n >= 0 \<Longrightarrow> fact (n::int) ~= 0" |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
120 |
by (simp add: fact_int_def) |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
121 |
|
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
122 |
lemma fact_gt_zero_nat [simp]: "fact (n :: nat) > 0" |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
123 |
by (insert fact_nonzero_nat [of n], arith) |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
124 |
|
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
125 |
lemma fact_gt_zero_int [simp]: "n >= 0 \<Longrightarrow> fact (n :: int) > 0" |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
126 |
by (auto simp add: fact_int_def) |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
127 |
|
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
128 |
lemma fact_ge_one_nat [simp]: "fact (n :: nat) >= 1" |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
129 |
by (insert fact_nonzero_nat [of n], arith) |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
130 |
|
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
131 |
lemma fact_ge_Suc_0_nat [simp]: "fact (n :: nat) >= Suc 0" |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
132 |
by (insert fact_nonzero_nat [of n], arith) |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
133 |
|
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
134 |
lemma fact_ge_one_int [simp]: "n >= 0 \<Longrightarrow> fact (n :: int) >= 1" |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
135 |
apply (auto simp add: fact_int_def) |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
136 |
apply (subgoal_tac "1 = int 1") |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
137 |
apply (erule ssubst) |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
138 |
apply (subst zle_int) |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
139 |
apply auto |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
140 |
done |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
141 |
|
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
142 |
lemma dvd_fact_nat [rule_format]: "1 <= m \<longrightarrow> m <= n \<longrightarrow> m dvd fact (n::nat)" |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
143 |
apply (induct n) |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
144 |
apply force |
32047 | 145 |
apply (auto simp only: fact_Suc) |
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
146 |
apply (subgoal_tac "m = Suc n") |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
147 |
apply (erule ssubst) |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
148 |
apply (rule dvd_triv_left) |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
149 |
apply auto |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
150 |
done |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
151 |
|
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
152 |
lemma dvd_fact_int [rule_format]: "1 <= m \<longrightarrow> m <= n \<longrightarrow> m dvd fact (n::int)" |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
153 |
apply (case_tac "1 <= n") |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
154 |
apply (induct n rule: int_ge_induct) |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
155 |
apply (auto simp add: fact_plus_one_int) |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
156 |
apply (subgoal_tac "m = i + 1") |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
157 |
apply auto |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
158 |
done |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
159 |
|
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
160 |
lemma interval_plus_one_nat: "(i::nat) <= j + 1 \<Longrightarrow> |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
161 |
{i..j+1} = {i..j} Un {j+1}" |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
162 |
by auto |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
163 |
|
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
164 |
lemma interval_Suc: "i <= Suc j \<Longrightarrow> {i..Suc j} = {i..j} Un {Suc j}" |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
165 |
by auto |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
166 |
|
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
167 |
lemma interval_plus_one_int: "(i::int) <= j + 1 \<Longrightarrow> {i..j+1} = {i..j} Un {j+1}" |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
168 |
by auto |
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset
|
169 |
|
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
170 |
lemma fact_altdef_nat: "fact (n::nat) = (PROD i:{1..n}. i)" |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
171 |
apply (induct n) |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
172 |
apply force |
32047 | 173 |
apply (subst fact_Suc) |
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
174 |
apply (subst interval_Suc) |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
175 |
apply auto |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
176 |
done |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
177 |
|
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
178 |
lemma fact_altdef_int: "n >= 0 \<Longrightarrow> fact (n::int) = (PROD i:{1..n}. i)" |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
179 |
apply (induct n rule: int_ge_induct) |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
180 |
apply force |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
181 |
apply (subst fact_plus_one_int, assumption) |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
182 |
apply (subst interval_plus_one_int) |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
183 |
apply auto |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
184 |
done |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
185 |
|
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
186 |
lemma fact_mono_nat: "(m::nat) \<le> n \<Longrightarrow> fact m \<le> fact n" |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
187 |
apply (drule le_imp_less_or_eq) |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
188 |
apply (auto dest!: less_imp_Suc_add) |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
189 |
apply (induct_tac k, auto) |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
190 |
done |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
191 |
|
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
192 |
lemma fact_neg_int [simp]: "m < (0::int) \<Longrightarrow> fact m = 0" |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
193 |
unfolding fact_int_def by auto |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
194 |
|
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
195 |
lemma fact_ge_zero_int [simp]: "fact m >= (0::int)" |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
196 |
apply (case_tac "m >= 0") |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
197 |
apply auto |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
198 |
apply (frule fact_gt_zero_int) |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
199 |
apply arith |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
200 |
done |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
201 |
|
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
202 |
lemma fact_mono_int_aux [rule_format]: "k >= (0::int) \<Longrightarrow> |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
203 |
fact (m + k) >= fact m" |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
204 |
apply (case_tac "m < 0") |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
205 |
apply auto |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
206 |
apply (induct k rule: int_ge_induct) |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
207 |
apply auto |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
208 |
apply (subst add_assoc [symmetric]) |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
209 |
apply (subst fact_plus_one_int) |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
210 |
apply auto |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
211 |
apply (erule order_trans) |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
212 |
apply (subst mult_le_cancel_right1) |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
213 |
apply (subgoal_tac "fact (m + i) >= 0") |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
214 |
apply arith |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
215 |
apply auto |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
216 |
done |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
217 |
|
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
218 |
lemma fact_mono_int: "(m::int) <= n \<Longrightarrow> fact m <= fact n" |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
219 |
apply (insert fact_mono_int_aux [of "n - m" "m"]) |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
220 |
apply auto |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
221 |
done |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
222 |
|
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
223 |
text{*Note that @{term "fact 0 = fact 1"}*} |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
224 |
lemma fact_less_mono_nat: "[| (0::nat) < m; m < n |] ==> fact m < fact n" |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
225 |
apply (drule_tac m = m in less_imp_Suc_add, auto) |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
226 |
apply (induct_tac k, auto) |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
227 |
done |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
228 |
|
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
229 |
lemma fact_less_mono_int_aux: "k >= 0 \<Longrightarrow> (0::int) < m \<Longrightarrow> |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
230 |
fact m < fact ((m + 1) + k)" |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
231 |
apply (induct k rule: int_ge_induct) |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
232 |
apply (simp add: fact_plus_one_int) |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
233 |
apply (subst mult_less_cancel_right1) |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
234 |
apply (insert fact_gt_zero_int [of m], arith) |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
235 |
apply (subst (2) fact_reduce_int) |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
236 |
apply (auto simp add: add_ac) |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
237 |
apply (erule order_less_le_trans) |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
238 |
apply (subst mult_le_cancel_right1) |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
239 |
apply auto |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
240 |
apply (subgoal_tac "fact (i + (1 + m)) >= 0") |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
241 |
apply force |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
242 |
apply (rule fact_ge_zero_int) |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
243 |
done |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
244 |
|
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
245 |
lemma fact_less_mono_int: "(0::int) < m \<Longrightarrow> m < n \<Longrightarrow> fact m < fact n" |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
246 |
apply (insert fact_less_mono_int_aux [of "n - (m + 1)" "m"]) |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
247 |
apply auto |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
248 |
done |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
249 |
|
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
250 |
lemma fact_num_eq_if_nat: "fact (m::nat) = |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
251 |
(if m=0 then 1 else m * fact (m - 1))" |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
252 |
by (cases m) auto |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
253 |
|
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
254 |
lemma fact_add_num_eq_if_nat: |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
255 |
"fact ((m::nat) + n) = (if m + n = 0 then 1 else (m + n) * fact (m + n - 1))" |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
256 |
by (cases "m + n") auto |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
257 |
|
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
258 |
lemma fact_add_num_eq_if2_nat: |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
259 |
"fact ((m::nat) + n) = |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
260 |
(if m = 0 then fact n else (m + n) * fact ((m - 1) + n))" |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
261 |
by (cases m) auto |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
262 |
|
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
30242
diff
changeset
|
263 |
|
32039
400a519bc888
Use term antiquotation to refer to constant names in subsection title.
berghofe
parents:
32036
diff
changeset
|
264 |
subsection {* @{term fact} and @{term of_nat} *} |
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset
|
265 |
|
29693
708dcf7dec9f
moved upwards in thy graph, real related theorems moved to Transcendental.thy
chaieb
parents:
28952
diff
changeset
|
266 |
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
|
267 |
by auto |
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset
|
268 |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
33319
diff
changeset
|
269 |
lemma of_nat_fact_gt_zero [simp]: "(0::'a::{linordered_semidom}) < of_nat(fact n)" by auto |
29693
708dcf7dec9f
moved upwards in thy graph, real related theorems moved to Transcendental.thy
chaieb
parents:
28952
diff
changeset
|
270 |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
33319
diff
changeset
|
271 |
lemma of_nat_fact_ge_zero [simp]: "(0::'a::linordered_semidom) \<le> of_nat(fact n)" |
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset
|
272 |
by simp |
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset
|
273 |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
33319
diff
changeset
|
274 |
lemma inv_of_nat_fact_gt_zero [simp]: "(0::'a::linordered_field) < inverse (of_nat (fact n))" |
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset
|
275 |
by (auto simp add: positive_imp_inverse_positive) |
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset
|
276 |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
33319
diff
changeset
|
277 |
lemma inv_of_nat_fact_ge_zero [simp]: "(0::'a::linordered_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
|
278 |
by (auto intro: order_less_imp_le) |
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
12196
diff
changeset
|
279 |
|
15131 | 280 |
end |