author | haftmann |
Sun, 22 Jul 2012 09:56:34 +0200 | |
changeset 49442 | 571cb1df0768 |
parent 47111 | 933f35c4e126 |
child 51239 | aacd6da09825 |
permissions | -rw-r--r-- |
paulson@15094 | 1 |
(* Title : Fact.thy |
paulson@12196 | 2 |
Author : Jacques D. Fleuriot |
paulson@12196 | 3 |
Copyright : 1998 University of Cambridge |
paulson@15094 | 4 |
Conversion to Isar and new proofs by Lawrence C Paulson, 2004 |
avigad@32029 | 5 |
The integer version of factorial and other additions by Jeremy Avigad. |
paulson@12196 | 6 |
*) |
paulson@12196 | 7 |
|
paulson@15094 | 8 |
header{*Factorial Function*} |
paulson@12196 | 9 |
|
nipkow@15131 | 10 |
theory Fact |
haftmann@33302 | 11 |
imports Main |
nipkow@15131 | 12 |
begin |
paulson@15094 | 13 |
|
avigad@32029 | 14 |
class fact = |
wenzelm@41798 | 15 |
fixes fact :: "'a \<Rightarrow> 'a" |
paulson@15094 | 16 |
|
avigad@32029 | 17 |
instantiation nat :: fact |
avigad@32029 | 18 |
begin |
avigad@32029 | 19 |
|
avigad@32029 | 20 |
fun |
avigad@32029 | 21 |
fact_nat :: "nat \<Rightarrow> nat" |
avigad@32029 | 22 |
where |
avigad@32029 | 23 |
fact_0_nat: "fact_nat 0 = Suc 0" |
avigad@32039 | 24 |
| fact_Suc: "fact_nat (Suc x) = Suc x * fact x" |
avigad@32029 | 25 |
|
wenzelm@41798 | 26 |
instance .. |
avigad@32029 | 27 |
|
avigad@32029 | 28 |
end |
avigad@32029 | 29 |
|
avigad@32029 | 30 |
(* definitions for the integers *) |
avigad@32029 | 31 |
|
avigad@32029 | 32 |
instantiation int :: fact |
avigad@32029 | 33 |
|
avigad@32029 | 34 |
begin |
avigad@32029 | 35 |
|
avigad@32029 | 36 |
definition |
avigad@32029 | 37 |
fact_int :: "int \<Rightarrow> int" |
avigad@32029 | 38 |
where |
avigad@32029 | 39 |
"fact_int x = (if x >= 0 then int (fact (nat x)) else 0)" |
avigad@32029 | 40 |
|
avigad@32029 | 41 |
instance proof qed |
avigad@32029 | 42 |
|
avigad@32029 | 43 |
end |
avigad@32029 | 44 |
|
avigad@32029 | 45 |
|
avigad@32029 | 46 |
subsection {* Set up Transfer *} |
avigad@32029 | 47 |
|
avigad@32029 | 48 |
lemma transfer_nat_int_factorial: |
avigad@32029 | 49 |
"(x::int) >= 0 \<Longrightarrow> fact (nat x) = nat (fact x)" |
avigad@32029 | 50 |
unfolding fact_int_def |
avigad@32029 | 51 |
by auto |
avigad@32029 | 52 |
|
avigad@32029 | 53 |
|
avigad@32029 | 54 |
lemma transfer_nat_int_factorial_closure: |
avigad@32029 | 55 |
"x >= (0::int) \<Longrightarrow> fact x >= 0" |
avigad@32029 | 56 |
by (auto simp add: fact_int_def) |
avigad@32029 | 57 |
|
haftmann@35644 | 58 |
declare transfer_morphism_nat_int[transfer add return: |
avigad@32029 | 59 |
transfer_nat_int_factorial transfer_nat_int_factorial_closure] |
avigad@32029 | 60 |
|
avigad@32029 | 61 |
lemma transfer_int_nat_factorial: |
avigad@32029 | 62 |
"fact (int x) = int (fact x)" |
avigad@32029 | 63 |
unfolding fact_int_def by auto |
avigad@32029 | 64 |
|
avigad@32029 | 65 |
lemma transfer_int_nat_factorial_closure: |
avigad@32029 | 66 |
"is_nat x \<Longrightarrow> fact x >= 0" |
avigad@32029 | 67 |
by (auto simp add: fact_int_def) |
avigad@32029 | 68 |
|
haftmann@35644 | 69 |
declare transfer_morphism_int_nat[transfer add return: |
avigad@32029 | 70 |
transfer_int_nat_factorial transfer_int_nat_factorial_closure] |
avigad@32029 | 71 |
|
avigad@32029 | 72 |
|
avigad@32029 | 73 |
subsection {* Factorial *} |
avigad@32029 | 74 |
|
avigad@32029 | 75 |
lemma fact_0_int [simp]: "fact (0::int) = 1" |
avigad@32029 | 76 |
by (simp add: fact_int_def) |
avigad@32029 | 77 |
|
avigad@32029 | 78 |
lemma fact_1_nat [simp]: "fact (1::nat) = 1" |
avigad@32029 | 79 |
by simp |
avigad@32029 | 80 |
|
avigad@32029 | 81 |
lemma fact_Suc_0_nat [simp]: "fact (Suc 0) = Suc 0" |
avigad@32029 | 82 |
by simp |
avigad@32029 | 83 |
|
avigad@32029 | 84 |
lemma fact_1_int [simp]: "fact (1::int) = 1" |
avigad@32029 | 85 |
by (simp add: fact_int_def) |
avigad@32029 | 86 |
|
avigad@32029 | 87 |
lemma fact_plus_one_nat: "fact ((n::nat) + 1) = (n + 1) * fact n" |
avigad@32029 | 88 |
by simp |
avigad@32029 | 89 |
|
avigad@32029 | 90 |
lemma fact_plus_one_int: |
avigad@32029 | 91 |
assumes "n >= 0" |
avigad@32029 | 92 |
shows "fact ((n::int) + 1) = (n + 1) * fact n" |
wenzelm@41798 | 93 |
using assms unfolding fact_int_def |
avigad@32029 | 94 |
by (simp add: nat_add_distrib algebra_simps int_mult) |
avigad@32029 | 95 |
|
avigad@32029 | 96 |
lemma fact_reduce_nat: "(n::nat) > 0 \<Longrightarrow> fact n = n * fact (n - 1)" |
avigad@32029 | 97 |
apply (subgoal_tac "n = Suc (n - 1)") |
avigad@32029 | 98 |
apply (erule ssubst) |
avigad@32039 | 99 |
apply (subst fact_Suc) |
avigad@32029 | 100 |
apply simp_all |
wenzelm@41798 | 101 |
done |
avigad@32029 | 102 |
|
avigad@32029 | 103 |
lemma fact_reduce_int: "(n::int) > 0 \<Longrightarrow> fact n = n * fact (n - 1)" |
avigad@32029 | 104 |
apply (subgoal_tac "n = (n - 1) + 1") |
avigad@32029 | 105 |
apply (erule ssubst) |
avigad@32029 | 106 |
apply (subst fact_plus_one_int) |
avigad@32029 | 107 |
apply simp_all |
wenzelm@41798 | 108 |
done |
avigad@32029 | 109 |
|
avigad@32029 | 110 |
lemma fact_nonzero_nat [simp]: "fact (n::nat) \<noteq> 0" |
avigad@32029 | 111 |
apply (induct n) |
avigad@32029 | 112 |
apply (auto simp add: fact_plus_one_nat) |
wenzelm@41798 | 113 |
done |
avigad@32029 | 114 |
|
avigad@32029 | 115 |
lemma fact_nonzero_int [simp]: "n >= 0 \<Longrightarrow> fact (n::int) ~= 0" |
avigad@32029 | 116 |
by (simp add: fact_int_def) |
avigad@32029 | 117 |
|
avigad@32029 | 118 |
lemma fact_gt_zero_nat [simp]: "fact (n :: nat) > 0" |
avigad@32029 | 119 |
by (insert fact_nonzero_nat [of n], arith) |
avigad@32029 | 120 |
|
avigad@32029 | 121 |
lemma fact_gt_zero_int [simp]: "n >= 0 \<Longrightarrow> fact (n :: int) > 0" |
avigad@32029 | 122 |
by (auto simp add: fact_int_def) |
avigad@32029 | 123 |
|
avigad@32029 | 124 |
lemma fact_ge_one_nat [simp]: "fact (n :: nat) >= 1" |
avigad@32029 | 125 |
by (insert fact_nonzero_nat [of n], arith) |
avigad@32029 | 126 |
|
avigad@32029 | 127 |
lemma fact_ge_Suc_0_nat [simp]: "fact (n :: nat) >= Suc 0" |
avigad@32029 | 128 |
by (insert fact_nonzero_nat [of n], arith) |
avigad@32029 | 129 |
|
avigad@32029 | 130 |
lemma fact_ge_one_int [simp]: "n >= 0 \<Longrightarrow> fact (n :: int) >= 1" |
avigad@32029 | 131 |
apply (auto simp add: fact_int_def) |
avigad@32029 | 132 |
apply (subgoal_tac "1 = int 1") |
avigad@32029 | 133 |
apply (erule ssubst) |
avigad@32029 | 134 |
apply (subst zle_int) |
avigad@32029 | 135 |
apply auto |
wenzelm@41798 | 136 |
done |
avigad@32029 | 137 |
|
avigad@32029 | 138 |
lemma dvd_fact_nat [rule_format]: "1 <= m \<longrightarrow> m <= n \<longrightarrow> m dvd fact (n::nat)" |
avigad@32029 | 139 |
apply (induct n) |
avigad@32029 | 140 |
apply force |
avigad@32039 | 141 |
apply (auto simp only: fact_Suc) |
avigad@32029 | 142 |
apply (subgoal_tac "m = Suc n") |
avigad@32029 | 143 |
apply (erule ssubst) |
avigad@32029 | 144 |
apply (rule dvd_triv_left) |
avigad@32029 | 145 |
apply auto |
wenzelm@41798 | 146 |
done |
avigad@32029 | 147 |
|
avigad@32029 | 148 |
lemma dvd_fact_int [rule_format]: "1 <= m \<longrightarrow> m <= n \<longrightarrow> m dvd fact (n::int)" |
avigad@32029 | 149 |
apply (case_tac "1 <= n") |
avigad@32029 | 150 |
apply (induct n rule: int_ge_induct) |
avigad@32029 | 151 |
apply (auto simp add: fact_plus_one_int) |
avigad@32029 | 152 |
apply (subgoal_tac "m = i + 1") |
avigad@32029 | 153 |
apply auto |
wenzelm@41798 | 154 |
done |
avigad@32029 | 155 |
|
avigad@32029 | 156 |
lemma interval_plus_one_nat: "(i::nat) <= j + 1 \<Longrightarrow> |
avigad@32029 | 157 |
{i..j+1} = {i..j} Un {j+1}" |
avigad@32029 | 158 |
by auto |
avigad@32029 | 159 |
|
avigad@32029 | 160 |
lemma interval_Suc: "i <= Suc j \<Longrightarrow> {i..Suc j} = {i..j} Un {Suc j}" |
avigad@32029 | 161 |
by auto |
avigad@32029 | 162 |
|
avigad@32029 | 163 |
lemma interval_plus_one_int: "(i::int) <= j + 1 \<Longrightarrow> {i..j+1} = {i..j} Un {j+1}" |
avigad@32029 | 164 |
by auto |
avigad@32029 | 165 |
|
avigad@32029 | 166 |
lemma fact_altdef_nat: "fact (n::nat) = (PROD i:{1..n}. i)" |
avigad@32029 | 167 |
apply (induct n) |
avigad@32029 | 168 |
apply force |
avigad@32039 | 169 |
apply (subst fact_Suc) |
avigad@32029 | 170 |
apply (subst interval_Suc) |
avigad@32029 | 171 |
apply auto |
avigad@32029 | 172 |
done |
avigad@32029 | 173 |
|
avigad@32029 | 174 |
lemma fact_altdef_int: "n >= 0 \<Longrightarrow> fact (n::int) = (PROD i:{1..n}. i)" |
avigad@32029 | 175 |
apply (induct n rule: int_ge_induct) |
avigad@32029 | 176 |
apply force |
avigad@32029 | 177 |
apply (subst fact_plus_one_int, assumption) |
avigad@32029 | 178 |
apply (subst interval_plus_one_int) |
avigad@32029 | 179 |
apply auto |
avigad@32029 | 180 |
done |
avigad@32029 | 181 |
|
bulwahn@40214 | 182 |
lemma fact_dvd: "n \<le> m \<Longrightarrow> fact n dvd fact (m::nat)" |
bulwahn@40214 | 183 |
by (auto simp add: fact_altdef_nat intro!: setprod_dvd_setprod_subset) |
bulwahn@40214 | 184 |
|
bulwahn@40214 | 185 |
lemma fact_mod: "m \<le> (n::nat) \<Longrightarrow> fact n mod fact m = 0" |
bulwahn@40214 | 186 |
by (auto simp add: dvd_imp_mod_0 fact_dvd) |
bulwahn@40214 | 187 |
|
bulwahn@40214 | 188 |
lemma fact_div_fact: |
bulwahn@40214 | 189 |
assumes "m \<ge> (n :: nat)" |
bulwahn@40214 | 190 |
shows "(fact m) div (fact n) = \<Prod>{n + 1..m}" |
bulwahn@40214 | 191 |
proof - |
bulwahn@40214 | 192 |
obtain d where "d = m - n" by auto |
bulwahn@40214 | 193 |
from assms this have "m = n + d" by auto |
bulwahn@40214 | 194 |
have "fact (n + d) div (fact n) = \<Prod>{n + 1..n + d}" |
bulwahn@40214 | 195 |
proof (induct d) |
bulwahn@40214 | 196 |
case 0 |
bulwahn@40214 | 197 |
show ?case by simp |
bulwahn@40214 | 198 |
next |
bulwahn@40214 | 199 |
case (Suc d') |
bulwahn@40214 | 200 |
have "fact (n + Suc d') div fact n = Suc (n + d') * fact (n + d') div fact n" |
bulwahn@40214 | 201 |
by simp |
bulwahn@40214 | 202 |
also from Suc.hyps have "... = Suc (n + d') * \<Prod>{n + 1..n + d'}" |
bulwahn@40214 | 203 |
unfolding div_mult1_eq[of _ "fact (n + d')"] by (simp add: fact_mod) |
bulwahn@40214 | 204 |
also have "... = \<Prod>{n + 1..n + Suc d'}" |
bulwahn@40214 | 205 |
by (simp add: atLeastAtMostSuc_conv setprod_insert) |
bulwahn@40214 | 206 |
finally show ?case . |
bulwahn@40214 | 207 |
qed |
bulwahn@40214 | 208 |
from this `m = n + d` show ?thesis by simp |
bulwahn@40214 | 209 |
qed |
bulwahn@40214 | 210 |
|
avigad@32029 | 211 |
lemma fact_mono_nat: "(m::nat) \<le> n \<Longrightarrow> fact m \<le> fact n" |
avigad@32029 | 212 |
apply (drule le_imp_less_or_eq) |
avigad@32029 | 213 |
apply (auto dest!: less_imp_Suc_add) |
avigad@32029 | 214 |
apply (induct_tac k, auto) |
avigad@32029 | 215 |
done |
avigad@32029 | 216 |
|
avigad@32029 | 217 |
lemma fact_neg_int [simp]: "m < (0::int) \<Longrightarrow> fact m = 0" |
avigad@32029 | 218 |
unfolding fact_int_def by auto |
avigad@32029 | 219 |
|
avigad@32029 | 220 |
lemma fact_ge_zero_int [simp]: "fact m >= (0::int)" |
avigad@32029 | 221 |
apply (case_tac "m >= 0") |
avigad@32029 | 222 |
apply auto |
avigad@32029 | 223 |
apply (frule fact_gt_zero_int) |
avigad@32029 | 224 |
apply arith |
avigad@32029 | 225 |
done |
avigad@32029 | 226 |
|
avigad@32029 | 227 |
lemma fact_mono_int_aux [rule_format]: "k >= (0::int) \<Longrightarrow> |
avigad@32029 | 228 |
fact (m + k) >= fact m" |
avigad@32029 | 229 |
apply (case_tac "m < 0") |
avigad@32029 | 230 |
apply auto |
avigad@32029 | 231 |
apply (induct k rule: int_ge_induct) |
avigad@32029 | 232 |
apply auto |
avigad@32029 | 233 |
apply (subst add_assoc [symmetric]) |
avigad@32029 | 234 |
apply (subst fact_plus_one_int) |
avigad@32029 | 235 |
apply auto |
avigad@32029 | 236 |
apply (erule order_trans) |
avigad@32029 | 237 |
apply (subst mult_le_cancel_right1) |
avigad@32029 | 238 |
apply (subgoal_tac "fact (m + i) >= 0") |
avigad@32029 | 239 |
apply arith |
avigad@32029 | 240 |
apply auto |
avigad@32029 | 241 |
done |
avigad@32029 | 242 |
|
avigad@32029 | 243 |
lemma fact_mono_int: "(m::int) <= n \<Longrightarrow> fact m <= fact n" |
avigad@32029 | 244 |
apply (insert fact_mono_int_aux [of "n - m" "m"]) |
avigad@32029 | 245 |
apply auto |
avigad@32029 | 246 |
done |
avigad@32029 | 247 |
|
avigad@32029 | 248 |
text{*Note that @{term "fact 0 = fact 1"}*} |
avigad@32029 | 249 |
lemma fact_less_mono_nat: "[| (0::nat) < m; m < n |] ==> fact m < fact n" |
avigad@32029 | 250 |
apply (drule_tac m = m in less_imp_Suc_add, auto) |
avigad@32029 | 251 |
apply (induct_tac k, auto) |
avigad@32029 | 252 |
done |
avigad@32029 | 253 |
|
avigad@32029 | 254 |
lemma fact_less_mono_int_aux: "k >= 0 \<Longrightarrow> (0::int) < m \<Longrightarrow> |
avigad@32029 | 255 |
fact m < fact ((m + 1) + k)" |
avigad@32029 | 256 |
apply (induct k rule: int_ge_induct) |
avigad@32029 | 257 |
apply (simp add: fact_plus_one_int) |
avigad@32029 | 258 |
apply (subst (2) fact_reduce_int) |
avigad@32029 | 259 |
apply (auto simp add: add_ac) |
avigad@32029 | 260 |
apply (erule order_less_le_trans) |
avigad@32029 | 261 |
apply (subst mult_le_cancel_right1) |
avigad@32029 | 262 |
apply auto |
avigad@32029 | 263 |
apply (subgoal_tac "fact (i + (1 + m)) >= 0") |
avigad@32029 | 264 |
apply force |
avigad@32029 | 265 |
apply (rule fact_ge_zero_int) |
avigad@32029 | 266 |
done |
avigad@32029 | 267 |
|
avigad@32029 | 268 |
lemma fact_less_mono_int: "(0::int) < m \<Longrightarrow> m < n \<Longrightarrow> fact m < fact n" |
avigad@32029 | 269 |
apply (insert fact_less_mono_int_aux [of "n - (m + 1)" "m"]) |
avigad@32029 | 270 |
apply auto |
avigad@32029 | 271 |
done |
avigad@32029 | 272 |
|
avigad@32029 | 273 |
lemma fact_num_eq_if_nat: "fact (m::nat) = |
avigad@32029 | 274 |
(if m=0 then 1 else m * fact (m - 1))" |
avigad@32029 | 275 |
by (cases m) auto |
avigad@32029 | 276 |
|
avigad@32029 | 277 |
lemma fact_add_num_eq_if_nat: |
avigad@32029 | 278 |
"fact ((m::nat) + n) = (if m + n = 0 then 1 else (m + n) * fact (m + n - 1))" |
avigad@32029 | 279 |
by (cases "m + n") auto |
avigad@32029 | 280 |
|
avigad@32029 | 281 |
lemma fact_add_num_eq_if2_nat: |
avigad@32029 | 282 |
"fact ((m::nat) + n) = |
avigad@32029 | 283 |
(if m = 0 then fact n else (m + n) * fact ((m - 1) + n))" |
avigad@32029 | 284 |
by (cases m) auto |
avigad@32029 | 285 |
|
noschinl@46801 | 286 |
lemma fact_le_power: "fact n \<le> n^n" |
noschinl@46801 | 287 |
proof (induct n) |
noschinl@46801 | 288 |
case (Suc n) |
noschinl@46801 | 289 |
then have "fact n \<le> Suc n ^ n" by (rule le_trans) (simp add: power_mono) |
noschinl@46801 | 290 |
then show ?case by (simp add: add_le_mono) |
noschinl@46801 | 291 |
qed simp |
avigad@32029 | 292 |
|
berghofe@32032 | 293 |
subsection {* @{term fact} and @{term of_nat} *} |
paulson@15094 | 294 |
|
chaieb@29693 | 295 |
lemma of_nat_fact_not_zero [simp]: "of_nat (fact n) \<noteq> (0::'a::semiring_char_0)" |
nipkow@25134 | 296 |
by auto |
paulson@15094 | 297 |
|
haftmann@35028 | 298 |
lemma of_nat_fact_gt_zero [simp]: "(0::'a::{linordered_semidom}) < of_nat(fact n)" by auto |
chaieb@29693 | 299 |
|
haftmann@35028 | 300 |
lemma of_nat_fact_ge_zero [simp]: "(0::'a::linordered_semidom) \<le> of_nat(fact n)" |
nipkow@25134 | 301 |
by simp |
paulson@15094 | 302 |
|
haftmann@35028 | 303 |
lemma inv_of_nat_fact_gt_zero [simp]: "(0::'a::linordered_field) < inverse (of_nat (fact n))" |
nipkow@25134 | 304 |
by (auto simp add: positive_imp_inverse_positive) |
paulson@15094 | 305 |
|
haftmann@35028 | 306 |
lemma inv_of_nat_fact_ge_zero [simp]: "(0::'a::linordered_field) \<le> inverse (of_nat (fact n))" |
nipkow@25134 | 307 |
by (auto intro: order_less_imp_le) |
paulson@15094 | 308 |
|
nipkow@15131 | 309 |
end |