src/HOL/Fact.thy
 changeset 32036 8a9228872fbd parent 30242 aea5d7fa7ef5 child 32039 400a519bc888
```     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.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 +instantiation nat :: fact
1.27 +
1.28 +begin
1.29 +
1.30 +fun
1.31 +  fact_nat :: "nat \<Rightarrow> nat"
1.32 +where
1.33 +  fact_0_nat: "fact_nat 0 = Suc 0"
1.34 +| fact_Suc_nat: "fact_nat (Suc x) = Suc x * fact x"
1.35 +
1.36 +instance proof qed
1.37 +
1.38 +end
1.39 +
1.40 +(* definitions for the integers *)
1.41 +
1.42 +instantiation int :: fact
1.43 +
1.44 +begin
1.45 +
1.46 +definition
1.47 +  fact_int :: "int \<Rightarrow> int"
1.48 +where
1.49 +  "fact_int x = (if x >= 0 then int (fact (nat x)) else 0)"
1.50 +
1.51 +instance proof qed
1.52 +
1.53 +end
1.54 +
1.55 +
1.56 +subsection {* Set up Transfer *}
1.57 +
1.58 +lemma transfer_nat_int_factorial:
1.59 +  "(x::int) >= 0 \<Longrightarrow> fact (nat x) = nat (fact x)"
1.60 +  unfolding fact_int_def
1.61 +  by auto
1.62 +
1.63 +
1.64 +lemma transfer_nat_int_factorial_closure:
1.65 +  "x >= (0::int) \<Longrightarrow> fact x >= 0"
1.66 +  by (auto simp add: fact_int_def)
1.67 +
1.68 +declare TransferMorphism_nat_int[transfer add return:
1.69 +    transfer_nat_int_factorial transfer_nat_int_factorial_closure]
1.70 +
1.71 +lemma transfer_int_nat_factorial:
1.72 +  "fact (int x) = int (fact x)"
1.73 +  unfolding fact_int_def by auto
1.74 +
1.75 +lemma transfer_int_nat_factorial_closure:
1.76 +  "is_nat x \<Longrightarrow> fact x >= 0"
1.77 +  by (auto simp add: fact_int_def)
1.78 +
1.79 +declare TransferMorphism_int_nat[transfer add return:
1.80 +    transfer_int_nat_factorial transfer_int_nat_factorial_closure]
1.81
1.82
1.83 -lemma fact_gt_zero [simp]: "0 < fact n"
1.84 -by (induct n) auto
1.85 +subsection {* Factorial *}
1.86 +
1.87 +lemma fact_0_int [simp]: "fact (0::int) = 1"
1.88 +  by (simp add: fact_int_def)
1.89 +
1.90 +lemma fact_1_nat [simp]: "fact (1::nat) = 1"
1.91 +  by simp
1.92 +
1.93 +lemma fact_Suc_0_nat [simp]: "fact (Suc 0) = Suc 0"
1.94 +  by simp
1.95 +
1.96 +lemma fact_1_int [simp]: "fact (1::int) = 1"
1.97 +  by (simp add: fact_int_def)
1.98 +
1.99 +lemma fact_plus_one_nat: "fact ((n::nat) + 1) = (n + 1) * fact n"
1.100 +  by simp
1.101 +
1.102 +lemma fact_plus_one_int:
1.103 +  assumes "n >= 0"
1.104 +  shows "fact ((n::int) + 1) = (n + 1) * fact n"
1.105 +
1.106 +  using prems unfolding fact_int_def
1.107 +  by (simp add: nat_add_distrib algebra_simps int_mult)
1.108 +
1.109 +lemma fact_reduce_nat: "(n::nat) > 0 \<Longrightarrow> fact n = n * fact (n - 1)"
1.110 +  apply (subgoal_tac "n = Suc (n - 1)")
1.111 +  apply (erule ssubst)
1.112 +  apply (subst fact_Suc_nat)
1.113 +  apply simp_all
1.114 +done
1.115 +
1.116 +lemma fact_reduce_int: "(n::int) > 0 \<Longrightarrow> fact n = n * fact (n - 1)"
1.117 +  apply (subgoal_tac "n = (n - 1) + 1")
1.118 +  apply (erule ssubst)
1.119 +  apply (subst fact_plus_one_int)
1.120 +  apply simp_all
1.121 +done
1.122 +
1.123 +lemma fact_nonzero_nat [simp]: "fact (n::nat) \<noteq> 0"
1.124 +  apply (induct n)
1.125 +  apply (auto simp add: fact_plus_one_nat)
1.126 +done
1.127 +
1.128 +lemma fact_nonzero_int [simp]: "n >= 0 \<Longrightarrow> fact (n::int) ~= 0"
1.129 +  by (simp add: fact_int_def)
1.130 +
1.131 +lemma fact_gt_zero_nat [simp]: "fact (n :: nat) > 0"
1.132 +  by (insert fact_nonzero_nat [of n], arith)
1.133 +
1.134 +lemma fact_gt_zero_int [simp]: "n >= 0 \<Longrightarrow> fact (n :: int) > 0"
1.135 +  by (auto simp add: fact_int_def)
1.136 +
1.137 +lemma fact_ge_one_nat [simp]: "fact (n :: nat) >= 1"
1.138 +  by (insert fact_nonzero_nat [of n], arith)
1.139 +
1.140 +lemma fact_ge_Suc_0_nat [simp]: "fact (n :: nat) >= Suc 0"
1.141 +  by (insert fact_nonzero_nat [of n], arith)
1.142 +
1.143 +lemma fact_ge_one_int [simp]: "n >= 0 \<Longrightarrow> fact (n :: int) >= 1"
1.144 +  apply (auto simp add: fact_int_def)
1.145 +  apply (subgoal_tac "1 = int 1")
1.146 +  apply (erule ssubst)
1.147 +  apply (subst zle_int)
1.148 +  apply auto
1.149 +done
1.150 +
1.151 +lemma dvd_fact_nat [rule_format]: "1 <= m \<longrightarrow> m <= n \<longrightarrow> m dvd fact (n::nat)"
1.152 +  apply (induct n)
1.153 +  apply force
1.154 +  apply (auto simp only: fact_Suc_nat)
1.155 +  apply (subgoal_tac "m = Suc n")
1.156 +  apply (erule ssubst)
1.157 +  apply (rule dvd_triv_left)
1.158 +  apply auto
1.159 +done
1.160 +
1.161 +lemma dvd_fact_int [rule_format]: "1 <= m \<longrightarrow> m <= n \<longrightarrow> m dvd fact (n::int)"
1.162 +  apply (case_tac "1 <= n")
1.163 +  apply (induct n rule: int_ge_induct)
1.164 +  apply (auto simp add: fact_plus_one_int)
1.165 +  apply (subgoal_tac "m = i + 1")
1.166 +  apply auto
1.167 +done
1.168 +
1.169 +lemma interval_plus_one_nat: "(i::nat) <= j + 1 \<Longrightarrow>
1.170 +  {i..j+1} = {i..j} Un {j+1}"
1.171 +  by auto
1.172 +
1.173 +lemma interval_Suc: "i <= Suc j \<Longrightarrow> {i..Suc j} = {i..j} Un {Suc j}"
1.174 +  by auto
1.175 +
1.176 +lemma interval_plus_one_int: "(i::int) <= j + 1 \<Longrightarrow> {i..j+1} = {i..j} Un {j+1}"
1.177 +  by auto
1.178
1.179 -lemma fact_not_eq_zero [simp]: "fact n \<noteq> 0"
1.180 -by simp
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.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.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 -