1.1 --- a/src/HOL/Fact.thy Thu Jul 09 17:34:59 2009 +0200
1.2 +++ b/src/HOL/Fact.thy Fri Jul 10 10:45:30 2009 -0400
1.3 @@ -2,25 +2,266 @@
1.4 Author : Jacques D. Fleuriot
1.5 Copyright : 1998 University of Cambridge
1.6 Conversion to Isar and new proofs by Lawrence C Paulson, 2004
1.7 + The integer version of factorial and other additions by Jeremy Avigad.
1.8 *)
1.9
1.10 header{*Factorial Function*}
1.11
1.12 theory Fact
1.13 -imports Main
1.14 +imports NatTransfer
1.15 begin
1.16
1.17 -consts fact :: "nat => nat"
1.18 -primrec
1.19 - fact_0: "fact 0 = 1"
1.20 - fact_Suc: "fact (Suc n) = (Suc n) * fact n"
1.21 +class fact =
1.22
1.23 +fixes
1.24 + fact :: "'a \<Rightarrow> 'a"
1.25
1.26 -lemma fact_gt_zero [simp]: "0 < fact n"
1.27 -by (induct n) auto
1.28 +instantiation nat :: fact
1.29
1.30 -lemma fact_not_eq_zero [simp]: "fact n \<noteq> 0"
1.31 -by simp
1.32 +begin
1.33 +
1.34 +fun
1.35 + fact_nat :: "nat \<Rightarrow> nat"
1.36 +where
1.37 + fact_0_nat: "fact_nat 0 = Suc 0"
1.38 +| fact_Suc_nat: "fact_nat (Suc x) = Suc x * fact x"
1.39 +
1.40 +instance proof qed
1.41 +
1.42 +end
1.43 +
1.44 +(* definitions for the integers *)
1.45 +
1.46 +instantiation int :: fact
1.47 +
1.48 +begin
1.49 +
1.50 +definition
1.51 + fact_int :: "int \<Rightarrow> int"
1.52 +where
1.53 + "fact_int x = (if x >= 0 then int (fact (nat x)) else 0)"
1.54 +
1.55 +instance proof qed
1.56 +
1.57 +end
1.58 +
1.59 +
1.60 +subsection {* Set up Transfer *}
1.61 +
1.62 +lemma transfer_nat_int_factorial:
1.63 + "(x::int) >= 0 \<Longrightarrow> fact (nat x) = nat (fact x)"
1.64 + unfolding fact_int_def
1.65 + by auto
1.66 +
1.67 +
1.68 +lemma transfer_nat_int_factorial_closure:
1.69 + "x >= (0::int) \<Longrightarrow> fact x >= 0"
1.70 + by (auto simp add: fact_int_def)
1.71 +
1.72 +declare TransferMorphism_nat_int[transfer add return:
1.73 + transfer_nat_int_factorial transfer_nat_int_factorial_closure]
1.74 +
1.75 +lemma transfer_int_nat_factorial:
1.76 + "fact (int x) = int (fact x)"
1.77 + unfolding fact_int_def by auto
1.78 +
1.79 +lemma transfer_int_nat_factorial_closure:
1.80 + "is_nat x \<Longrightarrow> fact x >= 0"
1.81 + by (auto simp add: fact_int_def)
1.82 +
1.83 +declare TransferMorphism_int_nat[transfer add return:
1.84 + transfer_int_nat_factorial transfer_int_nat_factorial_closure]
1.85 +
1.86 +
1.87 +subsection {* Factorial *}
1.88 +
1.89 +lemma fact_0_int [simp]: "fact (0::int) = 1"
1.90 + by (simp add: fact_int_def)
1.91 +
1.92 +lemma fact_1_nat [simp]: "fact (1::nat) = 1"
1.93 + by simp
1.94 +
1.95 +lemma fact_Suc_0_nat [simp]: "fact (Suc 0) = Suc 0"
1.96 + by simp
1.97 +
1.98 +lemma fact_1_int [simp]: "fact (1::int) = 1"
1.99 + by (simp add: fact_int_def)
1.100 +
1.101 +lemma fact_plus_one_nat: "fact ((n::nat) + 1) = (n + 1) * fact n"
1.102 + by simp
1.103 +
1.104 +lemma fact_plus_one_int:
1.105 + assumes "n >= 0"
1.106 + shows "fact ((n::int) + 1) = (n + 1) * fact n"
1.107 +
1.108 + using prems unfolding fact_int_def
1.109 + by (simp add: nat_add_distrib algebra_simps int_mult)
1.110 +
1.111 +lemma fact_reduce_nat: "(n::nat) > 0 \<Longrightarrow> fact n = n * fact (n - 1)"
1.112 + apply (subgoal_tac "n = Suc (n - 1)")
1.113 + apply (erule ssubst)
1.114 + apply (subst fact_Suc_nat)
1.115 + apply simp_all
1.116 +done
1.117 +
1.118 +lemma fact_reduce_int: "(n::int) > 0 \<Longrightarrow> fact n = n * fact (n - 1)"
1.119 + apply (subgoal_tac "n = (n - 1) + 1")
1.120 + apply (erule ssubst)
1.121 + apply (subst fact_plus_one_int)
1.122 + apply simp_all
1.123 +done
1.124 +
1.125 +lemma fact_nonzero_nat [simp]: "fact (n::nat) \<noteq> 0"
1.126 + apply (induct n)
1.127 + apply (auto simp add: fact_plus_one_nat)
1.128 +done
1.129 +
1.130 +lemma fact_nonzero_int [simp]: "n >= 0 \<Longrightarrow> fact (n::int) ~= 0"
1.131 + by (simp add: fact_int_def)
1.132 +
1.133 +lemma fact_gt_zero_nat [simp]: "fact (n :: nat) > 0"
1.134 + by (insert fact_nonzero_nat [of n], arith)
1.135 +
1.136 +lemma fact_gt_zero_int [simp]: "n >= 0 \<Longrightarrow> fact (n :: int) > 0"
1.137 + by (auto simp add: fact_int_def)
1.138 +
1.139 +lemma fact_ge_one_nat [simp]: "fact (n :: nat) >= 1"
1.140 + by (insert fact_nonzero_nat [of n], arith)
1.141 +
1.142 +lemma fact_ge_Suc_0_nat [simp]: "fact (n :: nat) >= Suc 0"
1.143 + by (insert fact_nonzero_nat [of n], arith)
1.144 +
1.145 +lemma fact_ge_one_int [simp]: "n >= 0 \<Longrightarrow> fact (n :: int) >= 1"
1.146 + apply (auto simp add: fact_int_def)
1.147 + apply (subgoal_tac "1 = int 1")
1.148 + apply (erule ssubst)
1.149 + apply (subst zle_int)
1.150 + apply auto
1.151 +done
1.152 +
1.153 +lemma dvd_fact_nat [rule_format]: "1 <= m \<longrightarrow> m <= n \<longrightarrow> m dvd fact (n::nat)"
1.154 + apply (induct n)
1.155 + apply force
1.156 + apply (auto simp only: fact_Suc_nat)
1.157 + apply (subgoal_tac "m = Suc n")
1.158 + apply (erule ssubst)
1.159 + apply (rule dvd_triv_left)
1.160 + apply auto
1.161 +done
1.162 +
1.163 +lemma dvd_fact_int [rule_format]: "1 <= m \<longrightarrow> m <= n \<longrightarrow> m dvd fact (n::int)"
1.164 + apply (case_tac "1 <= n")
1.165 + apply (induct n rule: int_ge_induct)
1.166 + apply (auto simp add: fact_plus_one_int)
1.167 + apply (subgoal_tac "m = i + 1")
1.168 + apply auto
1.169 +done
1.170 +
1.171 +lemma interval_plus_one_nat: "(i::nat) <= j + 1 \<Longrightarrow>
1.172 + {i..j+1} = {i..j} Un {j+1}"
1.173 + by auto
1.174 +
1.175 +lemma interval_Suc: "i <= Suc j \<Longrightarrow> {i..Suc j} = {i..j} Un {Suc j}"
1.176 + by auto
1.177 +
1.178 +lemma interval_plus_one_int: "(i::int) <= j + 1 \<Longrightarrow> {i..j+1} = {i..j} Un {j+1}"
1.179 + by auto
1.180 +
1.181 +lemma fact_altdef_nat: "fact (n::nat) = (PROD i:{1..n}. i)"
1.182 + apply (induct n)
1.183 + apply force
1.184 + apply (subst fact_Suc_nat)
1.185 + apply (subst interval_Suc)
1.186 + apply auto
1.187 +done
1.188 +
1.189 +lemma fact_altdef_int: "n >= 0 \<Longrightarrow> fact (n::int) = (PROD i:{1..n}. i)"
1.190 + apply (induct n rule: int_ge_induct)
1.191 + apply force
1.192 + apply (subst fact_plus_one_int, assumption)
1.193 + apply (subst interval_plus_one_int)
1.194 + apply auto
1.195 +done
1.196 +
1.197 +lemma fact_mono_nat: "(m::nat) \<le> n \<Longrightarrow> fact m \<le> fact n"
1.198 +apply (drule le_imp_less_or_eq)
1.199 +apply (auto dest!: less_imp_Suc_add)
1.200 +apply (induct_tac k, auto)
1.201 +done
1.202 +
1.203 +lemma fact_neg_int [simp]: "m < (0::int) \<Longrightarrow> fact m = 0"
1.204 + unfolding fact_int_def by auto
1.205 +
1.206 +lemma fact_ge_zero_int [simp]: "fact m >= (0::int)"
1.207 + apply (case_tac "m >= 0")
1.208 + apply auto
1.209 + apply (frule fact_gt_zero_int)
1.210 + apply arith
1.211 +done
1.212 +
1.213 +lemma fact_mono_int_aux [rule_format]: "k >= (0::int) \<Longrightarrow>
1.214 + fact (m + k) >= fact m"
1.215 + apply (case_tac "m < 0")
1.216 + apply auto
1.217 + apply (induct k rule: int_ge_induct)
1.218 + apply auto
1.219 + apply (subst add_assoc [symmetric])
1.220 + apply (subst fact_plus_one_int)
1.221 + apply auto
1.222 + apply (erule order_trans)
1.223 + apply (subst mult_le_cancel_right1)
1.224 + apply (subgoal_tac "fact (m + i) >= 0")
1.225 + apply arith
1.226 + apply auto
1.227 +done
1.228 +
1.229 +lemma fact_mono_int: "(m::int) <= n \<Longrightarrow> fact m <= fact n"
1.230 + apply (insert fact_mono_int_aux [of "n - m" "m"])
1.231 + apply auto
1.232 +done
1.233 +
1.234 +text{*Note that @{term "fact 0 = fact 1"}*}
1.235 +lemma fact_less_mono_nat: "[| (0::nat) < m; m < n |] ==> fact m < fact n"
1.236 +apply (drule_tac m = m in less_imp_Suc_add, auto)
1.237 +apply (induct_tac k, auto)
1.238 +done
1.239 +
1.240 +lemma fact_less_mono_int_aux: "k >= 0 \<Longrightarrow> (0::int) < m \<Longrightarrow>
1.241 + fact m < fact ((m + 1) + k)"
1.242 + apply (induct k rule: int_ge_induct)
1.243 + apply (simp add: fact_plus_one_int)
1.244 + apply (subst mult_less_cancel_right1)
1.245 + apply (insert fact_gt_zero_int [of m], arith)
1.246 + apply (subst (2) fact_reduce_int)
1.247 + apply (auto simp add: add_ac)
1.248 + apply (erule order_less_le_trans)
1.249 + apply (subst mult_le_cancel_right1)
1.250 + apply auto
1.251 + apply (subgoal_tac "fact (i + (1 + m)) >= 0")
1.252 + apply force
1.253 + apply (rule fact_ge_zero_int)
1.254 +done
1.255 +
1.256 +lemma fact_less_mono_int: "(0::int) < m \<Longrightarrow> m < n \<Longrightarrow> fact m < fact n"
1.257 + apply (insert fact_less_mono_int_aux [of "n - (m + 1)" "m"])
1.258 + apply auto
1.259 +done
1.260 +
1.261 +lemma fact_num_eq_if_nat: "fact (m::nat) =
1.262 + (if m=0 then 1 else m * fact (m - 1))"
1.263 +by (cases m) auto
1.264 +
1.265 +lemma fact_add_num_eq_if_nat:
1.266 + "fact ((m::nat) + n) = (if m + n = 0 then 1 else (m + n) * fact (m + n - 1))"
1.267 +by (cases "m + n") auto
1.268 +
1.269 +lemma fact_add_num_eq_if2_nat:
1.270 + "fact ((m::nat) + n) =
1.271 + (if m = 0 then fact n else (m + n) * fact ((m - 1) + n))"
1.272 +by (cases m) auto
1.273 +
1.274 +
1.275 +subsection {* fact and of_nat *}
1.276
1.277 lemma of_nat_fact_not_zero [simp]: "of_nat (fact n) \<noteq> (0::'a::semiring_char_0)"
1.278 by auto
1.279 @@ -33,46 +274,10 @@
1.280 lemma of_nat_fact_ge_zero [simp]: "(0::'a::ordered_semidom) \<le> of_nat(fact n)"
1.281 by simp
1.282
1.283 -lemma fact_ge_one [simp]: "1 \<le> fact n"
1.284 -by (induct n) auto
1.285 -
1.286 -lemma fact_mono: "m \<le> n ==> fact m \<le> fact n"
1.287 -apply (drule le_imp_less_or_eq)
1.288 -apply (auto dest!: less_imp_Suc_add)
1.289 -apply (induct_tac k, auto)
1.290 -done
1.291 -
1.292 -text{*Note that @{term "fact 0 = fact 1"}*}
1.293 -lemma fact_less_mono: "[| 0 < m; m < n |] ==> fact m < fact n"
1.294 -apply (drule_tac m = m in less_imp_Suc_add, auto)
1.295 -apply (induct_tac k, auto)
1.296 -done
1.297 -
1.298 lemma inv_of_nat_fact_gt_zero [simp]: "(0::'a::ordered_field) < inverse (of_nat (fact n))"
1.299 by (auto simp add: positive_imp_inverse_positive)
1.300
1.301 lemma inv_of_nat_fact_ge_zero [simp]: "(0::'a::ordered_field) \<le> inverse (of_nat (fact n))"
1.302 by (auto intro: order_less_imp_le)
1.303
1.304 -lemma fact_diff_Suc [rule_format]:
1.305 - "n < Suc m ==> fact (Suc m - n) = (Suc m - n) * fact (m - n)"
1.306 -apply (induct n arbitrary: m)
1.307 -apply auto
1.308 -apply (drule_tac x = "m - Suc 0" in meta_spec, auto)
1.309 -done
1.310 -
1.311 -lemma fact_num0: "fact 0 = 1"
1.312 -by auto
1.313 -
1.314 -lemma fact_num_eq_if: "fact m = (if m=0 then 1 else m * fact (m - 1))"
1.315 -by (cases m) auto
1.316 -
1.317 -lemma fact_add_num_eq_if:
1.318 - "fact (m + n) = (if m + n = 0 then 1 else (m + n) * fact (m + n - 1))"
1.319 -by (cases "m + n") auto
1.320 -
1.321 -lemma fact_add_num_eq_if2:
1.322 - "fact (m + n) = (if m = 0 then fact n else (m + n) * fact ((m - 1) + n))"
1.323 -by (cases m) auto
1.324 -
1.325 end