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.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 +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.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