Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
authoravigad
Fri Jul 10 10:45:30 2009 -0400 (2009-07-10)
changeset 320368a9228872fbd
parent 31970 ccaadfcf6941
child 32037 bed71e0d83e6
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
src/HOL/Fact.thy
src/HOL/GCD.thy
src/HOL/NewNumberTheory/Binomial.thy
src/HOL/Transcendental.thy
     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
     2.1 --- a/src/HOL/GCD.thy	Thu Jul 09 17:34:59 2009 +0200
     2.2 +++ b/src/HOL/GCD.thy	Fri Jul 10 10:45:30 2009 -0400
     2.3 @@ -20,6 +20,9 @@
     2.4  the congruence relations on the integers. The notion was extended to
     2.5  the natural numbers by Chiaeb.
     2.6  
     2.7 +Jeremy Avigad combined all of these, made everything uniform for the
     2.8 +natural numbers and the integers, and added a number of new theorems.
     2.9 +
    2.10  Tobias Nipkow cleaned up a lot.
    2.11  *)
    2.12  
    2.13 @@ -27,7 +30,7 @@
    2.14  header {* GCD *}
    2.15  
    2.16  theory GCD
    2.17 -imports NatTransfer
    2.18 +imports Fact
    2.19  begin
    2.20  
    2.21  declare One_nat_def [simp del]
    2.22 @@ -1730,4 +1733,42 @@
    2.23    ultimately show ?thesis by blast
    2.24  qed
    2.25  
    2.26 +subsection {* Infinitely many primes *}
    2.27 +
    2.28 +lemma next_prime_bound: "\<exists>(p::nat). prime p \<and> n < p \<and> p <= fact n + 1"
    2.29 +proof-
    2.30 +  have f1: "fact n + 1 \<noteq> 1" using fact_ge_one_nat [of n] by arith 
    2.31 +  from prime_factor_nat [OF f1]
    2.32 +      obtain p where "prime p" and "p dvd fact n + 1" by auto
    2.33 +  hence "p \<le> fact n + 1" 
    2.34 +    by (intro dvd_imp_le, auto)
    2.35 +  {assume "p \<le> n"
    2.36 +    from `prime p` have "p \<ge> 1" 
    2.37 +      by (cases p, simp_all)
    2.38 +    with `p <= n` have "p dvd fact n" 
    2.39 +      by (intro dvd_fact_nat)
    2.40 +    with `p dvd fact n + 1` have "p dvd fact n + 1 - fact n"
    2.41 +      by (rule dvd_diff_nat)
    2.42 +    hence "p dvd 1" by simp
    2.43 +    hence "p <= 1" by auto
    2.44 +    moreover from `prime p` have "p > 1" by auto
    2.45 +    ultimately have False by auto}
    2.46 +  hence "n < p" by arith
    2.47 +  with `prime p` and `p <= fact n + 1` show ?thesis by auto
    2.48 +qed
    2.49 +
    2.50 +lemma bigger_prime: "\<exists>p. prime p \<and> p > (n::nat)" 
    2.51 +using next_prime_bound by auto
    2.52 +
    2.53 +lemma primes_infinite: "\<not> (finite {(p::nat). prime p})"
    2.54 +proof
    2.55 +  assume "finite {(p::nat). prime p}"
    2.56 +  with Max_ge have "(EX b. (ALL x : {(p::nat). prime p}. x <= b))"
    2.57 +    by auto
    2.58 +  then obtain b where "ALL (x::nat). prime x \<longrightarrow> x <= b"
    2.59 +    by auto
    2.60 +  with bigger_prime [of b] show False by auto
    2.61 +qed
    2.62 +
    2.63 +
    2.64  end
     3.1 --- a/src/HOL/NewNumberTheory/Binomial.thy	Thu Jul 09 17:34:59 2009 +0200
     3.2 +++ b/src/HOL/NewNumberTheory/Binomial.thy	Fri Jul 10 10:45:30 2009 -0400
     3.3 @@ -2,7 +2,7 @@
     3.4      Authors:    Lawrence C. Paulson, Jeremy Avigad, Tobias Nipkow
     3.5  
     3.6  
     3.7 -Defines factorial and the "choose" function, and establishes basic properties.
     3.8 +Defines the "choose" function, and establishes basic properties.
     3.9  
    3.10  The original theory "Binomial" was by Lawrence C. Paulson, based on
    3.11  the work of Andy Gordon and Florian Kammueller. The approach here,
    3.12 @@ -16,7 +16,7 @@
    3.13  header {* Binomial *}
    3.14  
    3.15  theory Binomial
    3.16 -imports Cong
    3.17 +imports Cong Fact
    3.18  begin
    3.19  
    3.20  
    3.21 @@ -25,7 +25,6 @@
    3.22  class binomial =
    3.23  
    3.24  fixes 
    3.25 -  fact :: "'a \<Rightarrow> 'a" and
    3.26    binomial :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "choose" 65)
    3.27  
    3.28  (* definitions for the natural numbers *)
    3.29 @@ -35,13 +34,6 @@
    3.30  begin 
    3.31  
    3.32  fun
    3.33 -  fact_nat :: "nat \<Rightarrow> nat"
    3.34 -where
    3.35 -  "fact_nat x = 
    3.36 -   (if x = 0 then 1 else
    3.37 -                  x * fact(x - 1))"
    3.38 -
    3.39 -fun
    3.40    binomial_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
    3.41  where
    3.42    "binomial_nat n k =
    3.43 @@ -60,11 +52,6 @@
    3.44  begin 
    3.45  
    3.46  definition
    3.47 -  fact_int :: "int \<Rightarrow> int"
    3.48 -where  
    3.49 -  "fact_int x = (if x >= 0 then int (fact (nat x)) else 0)"
    3.50 -
    3.51 -definition
    3.52    binomial_int :: "int => int \<Rightarrow> int"
    3.53  where
    3.54    "binomial_int n k = (if n \<ge> 0 \<and> k \<ge> 0 then int (binomial (nat n) (nat k))
    3.55 @@ -76,182 +63,29 @@
    3.56  
    3.57  subsection {* Set up Transfer *}
    3.58  
    3.59 -
    3.60  lemma transfer_nat_int_binomial:
    3.61 -  "(x::int) >= 0 \<Longrightarrow> fact (nat x) = nat (fact x)"
    3.62    "(n::int) >= 0 \<Longrightarrow> k >= 0 \<Longrightarrow> binomial (nat n) (nat k) = 
    3.63        nat (binomial n k)"
    3.64 -  unfolding fact_int_def binomial_int_def 
    3.65 +  unfolding binomial_int_def 
    3.66    by auto
    3.67  
    3.68 -
    3.69 -lemma transfer_nat_int_binomial_closures:
    3.70 -  "x >= (0::int) \<Longrightarrow> fact x >= 0"
    3.71 +lemma transfer_nat_int_binomial_closure:
    3.72    "n >= (0::int) \<Longrightarrow> k >= 0 \<Longrightarrow> binomial n k >= 0"
    3.73 -  by (auto simp add: fact_int_def binomial_int_def)
    3.74 +  by (auto simp add: binomial_int_def)
    3.75  
    3.76  declare TransferMorphism_nat_int[transfer add return: 
    3.77 -    transfer_nat_int_binomial transfer_nat_int_binomial_closures]
    3.78 +    transfer_nat_int_binomial transfer_nat_int_binomial_closure]
    3.79  
    3.80  lemma transfer_int_nat_binomial:
    3.81 -  "fact (int x) = int (fact x)"
    3.82    "binomial (int n) (int k) = int (binomial n k)"
    3.83    unfolding fact_int_def binomial_int_def by auto
    3.84  
    3.85 -lemma transfer_int_nat_binomial_closures:
    3.86 -  "is_nat x \<Longrightarrow> fact x >= 0"
    3.87 +lemma transfer_int_nat_binomial_closure:
    3.88    "is_nat n \<Longrightarrow> is_nat k \<Longrightarrow> binomial n k >= 0"
    3.89 -  by (auto simp add: fact_int_def binomial_int_def)
    3.90 +  by (auto simp add: binomial_int_def)
    3.91  
    3.92  declare TransferMorphism_int_nat[transfer add return: 
    3.93 -    transfer_int_nat_binomial transfer_int_nat_binomial_closures]
    3.94 -
    3.95 -
    3.96 -subsection {* Factorial *}
    3.97 -
    3.98 -lemma fact_zero_nat [simp]: "fact (0::nat) = 1"
    3.99 -  by simp
   3.100 -
   3.101 -lemma fact_zero_int [simp]: "fact (0::int) = 1"
   3.102 -  by (simp add: fact_int_def)
   3.103 -
   3.104 -lemma fact_one_nat [simp]: "fact (1::nat) = 1"
   3.105 -  by simp
   3.106 -
   3.107 -lemma fact_Suc_0_nat [simp]: "fact (Suc 0) = Suc 0"
   3.108 -  by (simp add: One_nat_def)
   3.109 -
   3.110 -lemma fact_one_int [simp]: "fact (1::int) = 1"
   3.111 -  by (simp add: fact_int_def)
   3.112 -
   3.113 -lemma fact_plus_one_nat: "fact ((n::nat) + 1) = (n + 1) * fact n"
   3.114 -  by simp
   3.115 -
   3.116 -lemma fact_Suc_nat: "fact (Suc n) = (Suc n) * fact n"
   3.117 -  by (simp add: One_nat_def)
   3.118 -
   3.119 -lemma fact_plus_one_int: 
   3.120 -  assumes "n >= 0"
   3.121 -  shows "fact ((n::int) + 1) = (n + 1) * fact n"
   3.122 -
   3.123 -  using prems by (rule fact_plus_one_nat [transferred])
   3.124 -
   3.125 -lemma fact_reduce_nat: "(n::nat) > 0 \<Longrightarrow> fact n = n * fact (n - 1)"
   3.126 -  by simp
   3.127 -
   3.128 -lemma fact_reduce_int: 
   3.129 -  assumes "(n::int) > 0"
   3.130 -  shows "fact n = n * fact (n - 1)"
   3.131 -
   3.132 -  using prems apply (subst tsub_eq [symmetric], auto)
   3.133 -  apply (rule fact_reduce_nat [transferred])
   3.134 -  using prems apply auto
   3.135 -done
   3.136 -
   3.137 -declare fact_nat.simps [simp del]
   3.138 -
   3.139 -lemma fact_nonzero_nat [simp]: "fact (n::nat) \<noteq> 0"
   3.140 -  apply (induct n rule: induct'_nat)
   3.141 -  apply (auto simp add: fact_plus_one_nat)
   3.142 -done
   3.143 -
   3.144 -lemma fact_nonzero_int [simp]: "n >= 0 \<Longrightarrow> fact (n::int) ~= 0"
   3.145 -  by (simp add: fact_int_def)
   3.146 -
   3.147 -lemma fact_gt_zero_nat [simp]: "fact (n :: nat) > 0"
   3.148 -  by (insert fact_nonzero_nat [of n], arith)
   3.149 -
   3.150 -lemma fact_gt_zero_int [simp]: "n >= 0 \<Longrightarrow> fact (n :: int) > 0"
   3.151 -  by (auto simp add: fact_int_def)
   3.152 -
   3.153 -lemma fact_ge_one_nat [simp]: "fact (n :: nat) >= 1"
   3.154 -  by (insert fact_nonzero_nat [of n], arith)
   3.155 -
   3.156 -lemma fact_ge_Suc_0_nat [simp]: "fact (n :: nat) >= Suc 0"
   3.157 -  by (insert fact_nonzero_nat [of n], arith)
   3.158 -
   3.159 -lemma fact_ge_one_int [simp]: "n >= 0 \<Longrightarrow> fact (n :: int) >= 1"
   3.160 -  apply (auto simp add: fact_int_def)
   3.161 -  apply (subgoal_tac "1 = int 1")
   3.162 -  apply (erule ssubst)
   3.163 -  apply (subst zle_int)
   3.164 -  apply auto
   3.165 -done
   3.166 -
   3.167 -lemma dvd_fact_nat [rule_format]: "1 <= m \<longrightarrow> m <= n \<longrightarrow> m dvd fact (n::nat)"
   3.168 -  apply (induct n rule: induct'_nat)
   3.169 -  apply (auto simp add: fact_plus_one_nat)
   3.170 -  apply (subgoal_tac "m = n + 1")
   3.171 -  apply auto
   3.172 -done
   3.173 -
   3.174 -lemma dvd_fact_int [rule_format]: "1 <= m \<longrightarrow> m <= n \<longrightarrow> m dvd fact (n::int)"
   3.175 -  apply (case_tac "1 <= n")
   3.176 -  apply (induct n rule: int_ge_induct)
   3.177 -  apply (auto simp add: fact_plus_one_int)
   3.178 -  apply (subgoal_tac "m = i + 1")
   3.179 -  apply auto
   3.180 -done
   3.181 -
   3.182 -lemma interval_plus_one_nat: "(i::nat) <= j + 1 \<Longrightarrow> 
   3.183 -  {i..j+1} = {i..j} Un {j+1}"
   3.184 -  by auto
   3.185 -
   3.186 -lemma interval_plus_one_int: "(i::int) <= j + 1 \<Longrightarrow> {i..j+1} = {i..j} Un {j+1}"
   3.187 -  by auto
   3.188 -
   3.189 -lemma fact_altdef_nat: "fact (n::nat) = (PROD i:{1..n}. i)"
   3.190 -  apply (induct n rule: induct'_nat)
   3.191 -  apply force
   3.192 -  apply (subst fact_plus_one_nat)
   3.193 -  apply (subst interval_plus_one_nat)
   3.194 -  apply auto
   3.195 -done
   3.196 -
   3.197 -lemma fact_altdef_int: "n >= 0 \<Longrightarrow> fact (n::int) = (PROD i:{1..n}. i)"
   3.198 -  apply (induct n rule: int_ge_induct)
   3.199 -  apply force
   3.200 -  apply (subst fact_plus_one_int, assumption)
   3.201 -  apply (subst interval_plus_one_int)
   3.202 -  apply auto
   3.203 -done
   3.204 -
   3.205 -subsection {* Infinitely many primes *}
   3.206 -
   3.207 -lemma next_prime_bound: "\<exists>(p::nat). prime p \<and> n < p \<and> p <= fact n + 1"
   3.208 -proof-
   3.209 -  have f1: "fact n + 1 \<noteq> 1" using fact_ge_one_nat [of n] by arith 
   3.210 -  from prime_factor_nat [OF f1]
   3.211 -      obtain p where "prime p" and "p dvd fact n + 1" by auto
   3.212 -  hence "p \<le> fact n + 1" 
   3.213 -    by (intro dvd_imp_le, auto)
   3.214 -  {assume "p \<le> n"
   3.215 -    from `prime p` have "p \<ge> 1" 
   3.216 -      by (cases p, simp_all)
   3.217 -    with `p <= n` have "p dvd fact n" 
   3.218 -      by (intro dvd_fact_nat)
   3.219 -    with `p dvd fact n + 1` have "p dvd fact n + 1 - fact n"
   3.220 -      by (rule dvd_diff_nat)
   3.221 -    hence "p dvd 1" by simp
   3.222 -    hence "p <= 1" by auto
   3.223 -    moreover from `prime p` have "p > 1" by auto
   3.224 -    ultimately have False by auto}
   3.225 -  hence "n < p" by arith
   3.226 -  with `prime p` and `p <= fact n + 1` show ?thesis by auto
   3.227 -qed
   3.228 -
   3.229 -lemma bigger_prime: "\<exists>p. prime p \<and> p > (n::nat)" 
   3.230 -using next_prime_bound by auto
   3.231 -
   3.232 -lemma primes_infinite: "\<not> (finite {(p::nat). prime p})"
   3.233 -proof
   3.234 -  assume "finite {(p::nat). prime p}"
   3.235 -  with Max_ge have "(EX b. (ALL x : {(p::nat). prime p}. x <= b))"
   3.236 -    by auto
   3.237 -  then obtain b where "ALL (x::nat). prime x \<longrightarrow> x <= b"
   3.238 -    by auto
   3.239 -  with bigger_prime [of b] show False by auto
   3.240 -qed
   3.241 +    transfer_int_nat_binomial transfer_int_nat_binomial_closure]
   3.242  
   3.243  
   3.244  subsection {* Binomial coefficients *}
     4.1 --- a/src/HOL/Transcendental.thy	Thu Jul 09 17:34:59 2009 +0200
     4.2 +++ b/src/HOL/Transcendental.thy	Fri Jul 10 10:45:30 2009 -0400
     4.3 @@ -621,19 +621,19 @@
     4.4  
     4.5  subsection{* Some properties of factorials *}
     4.6  
     4.7 -lemma real_of_nat_fact_not_zero [simp]: "real (fact n) \<noteq> 0"
     4.8 +lemma real_of_nat_fact_not_zero [simp]: "real (fact (n::nat)) \<noteq> 0"
     4.9  by auto
    4.10  
    4.11 -lemma real_of_nat_fact_gt_zero [simp]: "0 < real(fact n)"
    4.12 +lemma real_of_nat_fact_gt_zero [simp]: "0 < real(fact (n::nat))"
    4.13  by auto
    4.14  
    4.15 -lemma real_of_nat_fact_ge_zero [simp]: "0 \<le> real(fact n)"
    4.16 +lemma real_of_nat_fact_ge_zero [simp]: "0 \<le> real(fact (n::nat))"
    4.17  by simp
    4.18  
    4.19 -lemma inv_real_of_nat_fact_gt_zero [simp]: "0 < inverse (real (fact n))"
    4.20 +lemma inv_real_of_nat_fact_gt_zero [simp]: "0 < inverse (real (fact (n::nat)))"
    4.21  by (auto simp add: positive_imp_inverse_positive)
    4.22  
    4.23 -lemma inv_real_of_nat_fact_ge_zero [simp]: "0 \<le> inverse (real (fact n))"
    4.24 +lemma inv_real_of_nat_fact_ge_zero [simp]: "0 \<le> inverse (real (fact (n::nat)))"
    4.25  by (auto intro: order_less_imp_le)
    4.26  
    4.27  subsection {* Derivability of power series *}
    4.28 @@ -1604,11 +1604,11 @@
    4.29  apply (rotate_tac 2)
    4.30  apply (drule sin_paired [THEN sums_unique, THEN ssubst])
    4.31  unfolding One_nat_def
    4.32 -apply (auto simp del: fact_Suc)
    4.33 +apply (auto simp del: fact_Suc_nat)
    4.34  apply (frule sums_unique)
    4.35 -apply (auto simp del: fact_Suc)
    4.36 +apply (auto simp del: fact_Suc_nat)
    4.37  apply (rule_tac n1 = 0 in series_pos_less [THEN [2] order_le_less_trans])
    4.38 -apply (auto simp del: fact_Suc)
    4.39 +apply (auto simp del: fact_Suc_nat)
    4.40  apply (erule sums_summable)
    4.41  apply (case_tac "m=0")
    4.42  apply (simp (no_asm_simp))
    4.43 @@ -1617,24 +1617,24 @@
    4.44  apply (simp (no_asm_simp) add: numeral_2_eq_2 [symmetric] mult_assoc [symmetric])
    4.45  apply (subgoal_tac "x*x < 2*3", simp) 
    4.46  apply (rule mult_strict_mono)
    4.47 -apply (auto simp add: real_0_less_add_iff real_of_nat_Suc simp del: fact_Suc)
    4.48 -apply (subst fact_Suc)
    4.49 -apply (subst fact_Suc)
    4.50 -apply (subst fact_Suc)
    4.51 -apply (subst fact_Suc)
    4.52 +apply (auto simp add: real_0_less_add_iff real_of_nat_Suc simp del: fact_Suc_nat)
    4.53 +apply (subst fact_Suc_nat)
    4.54 +apply (subst fact_Suc_nat)
    4.55 +apply (subst fact_Suc_nat)
    4.56 +apply (subst fact_Suc_nat)
    4.57  apply (subst real_of_nat_mult)
    4.58  apply (subst real_of_nat_mult)
    4.59  apply (subst real_of_nat_mult)
    4.60  apply (subst real_of_nat_mult)
    4.61 -apply (simp (no_asm) add: divide_inverse del: fact_Suc)
    4.62 -apply (auto simp add: mult_assoc [symmetric] simp del: fact_Suc)
    4.63 +apply (simp (no_asm) add: divide_inverse del: fact_Suc_nat)
    4.64 +apply (auto simp add: mult_assoc [symmetric] simp del: fact_Suc_nat)
    4.65  apply (rule_tac c="real (Suc (Suc (4*m)))" in mult_less_imp_less_right) 
    4.66 -apply (auto simp add: mult_assoc simp del: fact_Suc)
    4.67 +apply (auto simp add: mult_assoc simp del: fact_Suc_nat)
    4.68  apply (rule_tac c="real (Suc (Suc (Suc (4*m))))" in mult_less_imp_less_right) 
    4.69 -apply (auto simp add: mult_assoc mult_less_cancel_left simp del: fact_Suc)
    4.70 +apply (auto simp add: mult_assoc mult_less_cancel_left simp del: fact_Suc_nat)
    4.71  apply (subgoal_tac "x * (x * x ^ (4*m)) = (x ^ (4*m)) * (x * x)") 
    4.72  apply (erule ssubst)+
    4.73 -apply (auto simp del: fact_Suc)
    4.74 +apply (auto simp del: fact_Suc_nat)
    4.75  apply (subgoal_tac "0 < x ^ (4 * m) ")
    4.76   prefer 2 apply (simp only: zero_less_power) 
    4.77  apply (simp (no_asm_simp) add: mult_less_cancel_left)
    4.78 @@ -1670,24 +1670,24 @@
    4.79  apply (rule_tac y =
    4.80   "\<Sum>n=0..< Suc(Suc(Suc 0)). - (-1 ^ n / (real(fact (2*n))) * 2 ^ (2*n))"
    4.81         in order_less_trans)
    4.82 -apply (simp (no_asm) add: fact_num_eq_if realpow_num_eq_if del: fact_Suc)
    4.83 +apply (simp (no_asm) add: fact_num_eq_if_nat realpow_num_eq_if del: fact_Suc_nat)
    4.84  apply (simp (no_asm) add: mult_assoc del: setsum_op_ivl_Suc)
    4.85  apply (rule sumr_pos_lt_pair)
    4.86  apply (erule sums_summable, safe)
    4.87  unfolding One_nat_def
    4.88  apply (simp (no_asm) add: divide_inverse real_0_less_add_iff mult_assoc [symmetric] 
    4.89 -            del: fact_Suc)
    4.90 +            del: fact_Suc_nat)
    4.91  apply (rule real_mult_inverse_cancel2)
    4.92  apply (rule real_of_nat_fact_gt_zero)+
    4.93 -apply (simp (no_asm) add: mult_assoc [symmetric] del: fact_Suc)
    4.94 +apply (simp (no_asm) add: mult_assoc [symmetric] del: fact_Suc_nat)
    4.95  apply (subst fact_lemma) 
    4.96 -apply (subst fact_Suc [of "Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))"])
    4.97 +apply (subst fact_Suc_nat [of "Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))"])
    4.98  apply (simp only: real_of_nat_mult)
    4.99  apply (rule mult_strict_mono, force)
   4.100    apply (rule_tac [3] real_of_nat_ge_zero)
   4.101   prefer 2 apply force
   4.102  apply (rule real_of_nat_less_iff [THEN iffD2])
   4.103 -apply (rule fact_less_mono, auto)
   4.104 +apply (rule fact_less_mono_nat, auto)
   4.105  done
   4.106  
   4.107  lemmas cos_two_neq_zero [simp] = cos_two_less_zero [THEN less_imp_neq]