diff -r ccaadfcf6941 -r 8a9228872fbd src/HOL/NewNumberTheory/Binomial.thy
--- a/src/HOL/NewNumberTheory/Binomial.thy	Thu Jul 09 17:34:59 2009 +0200
+++ b/src/HOL/NewNumberTheory/Binomial.thy	Fri Jul 10 10:45:30 2009 -0400
@@ -2,7 +2,7 @@
     Authors:    Lawrence C. Paulson, Jeremy Avigad, Tobias Nipkow
 
 
-Defines factorial and the "choose" function, and establishes basic properties.
+Defines the "choose" function, and establishes basic properties.
 
 The original theory "Binomial" was by Lawrence C. Paulson, based on
 the work of Andy Gordon and Florian Kammueller. The approach here,
@@ -16,7 +16,7 @@
 header {* Binomial *}
 
 theory Binomial
-imports Cong
+imports Cong Fact
 begin
 
 
@@ -25,7 +25,6 @@
 class binomial =
 
 fixes 
-  fact :: "'a \<Rightarrow> 'a" and
   binomial :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "choose" 65)
 
 (* definitions for the natural numbers *)
@@ -35,13 +34,6 @@
 begin 
 
 fun
-  fact_nat :: "nat \<Rightarrow> nat"
-where
-  "fact_nat x = 
-   (if x = 0 then 1 else
-                  x * fact(x - 1))"
-
-fun
   binomial_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
 where
   "binomial_nat n k =
@@ -60,11 +52,6 @@
 begin 
 
 definition
-  fact_int :: "int \<Rightarrow> int"
-where  
-  "fact_int x = (if x >= 0 then int (fact (nat x)) else 0)"
-
-definition
   binomial_int :: "int => int \<Rightarrow> int"
 where
   "binomial_int n k = (if n \<ge> 0 \<and> k \<ge> 0 then int (binomial (nat n) (nat k))
@@ -76,182 +63,29 @@
 
 subsection {* Set up Transfer *}
 
-
 lemma transfer_nat_int_binomial:
-  "(x::int) >= 0 \<Longrightarrow> fact (nat x) = nat (fact x)"
   "(n::int) >= 0 \<Longrightarrow> k >= 0 \<Longrightarrow> binomial (nat n) (nat k) = 
       nat (binomial n k)"
-  unfolding fact_int_def binomial_int_def 
+  unfolding binomial_int_def 
   by auto
 
-
-lemma transfer_nat_int_binomial_closures:
-  "x >= (0::int) \<Longrightarrow> fact x >= 0"
+lemma transfer_nat_int_binomial_closure:
   "n >= (0::int) \<Longrightarrow> k >= 0 \<Longrightarrow> binomial n k >= 0"
-  by (auto simp add: fact_int_def binomial_int_def)
+  by (auto simp add: binomial_int_def)
 
 declare TransferMorphism_nat_int[transfer add return: 
-    transfer_nat_int_binomial transfer_nat_int_binomial_closures]
+    transfer_nat_int_binomial transfer_nat_int_binomial_closure]
 
 lemma transfer_int_nat_binomial:
-  "fact (int x) = int (fact x)"
   "binomial (int n) (int k) = int (binomial n k)"
   unfolding fact_int_def binomial_int_def by auto
 
-lemma transfer_int_nat_binomial_closures:
-  "is_nat x \<Longrightarrow> fact x >= 0"
+lemma transfer_int_nat_binomial_closure:
   "is_nat n \<Longrightarrow> is_nat k \<Longrightarrow> binomial n k >= 0"
-  by (auto simp add: fact_int_def binomial_int_def)
+  by (auto simp add: binomial_int_def)
 
 declare TransferMorphism_int_nat[transfer add return: 
-    transfer_int_nat_binomial transfer_int_nat_binomial_closures]
-
-
-subsection {* Factorial *}
-
-lemma fact_zero_nat [simp]: "fact (0::nat) = 1"
-  by simp
-
-lemma fact_zero_int [simp]: "fact (0::int) = 1"
-  by (simp add: fact_int_def)
-
-lemma fact_one_nat [simp]: "fact (1::nat) = 1"
-  by simp
-
-lemma fact_Suc_0_nat [simp]: "fact (Suc 0) = Suc 0"
-  by (simp add: One_nat_def)
-
-lemma fact_one_int [simp]: "fact (1::int) = 1"
-  by (simp add: fact_int_def)
-
-lemma fact_plus_one_nat: "fact ((n::nat) + 1) = (n + 1) * fact n"
-  by simp
-
-lemma fact_Suc_nat: "fact (Suc n) = (Suc n) * fact n"
-  by (simp add: One_nat_def)
-
-lemma fact_plus_one_int: 
-  assumes "n >= 0"
-  shows "fact ((n::int) + 1) = (n + 1) * fact n"
-
-  using prems by (rule fact_plus_one_nat [transferred])
-
-lemma fact_reduce_nat: "(n::nat) > 0 \<Longrightarrow> fact n = n * fact (n - 1)"
-  by simp
-
-lemma fact_reduce_int: 
-  assumes "(n::int) > 0"
-  shows "fact n = n * fact (n - 1)"
-
-  using prems apply (subst tsub_eq [symmetric], auto)
-  apply (rule fact_reduce_nat [transferred])
-  using prems apply auto
-done
-
-declare fact_nat.simps [simp del]
-
-lemma fact_nonzero_nat [simp]: "fact (n::nat) \<noteq> 0"
-  apply (induct n rule: induct'_nat)
-  apply (auto simp add: fact_plus_one_nat)
-done
-
-lemma fact_nonzero_int [simp]: "n >= 0 \<Longrightarrow> fact (n::int) ~= 0"
-  by (simp add: fact_int_def)
-
-lemma fact_gt_zero_nat [simp]: "fact (n :: nat) > 0"
-  by (insert fact_nonzero_nat [of n], arith)
-
-lemma fact_gt_zero_int [simp]: "n >= 0 \<Longrightarrow> fact (n :: int) > 0"
-  by (auto simp add: fact_int_def)
-
-lemma fact_ge_one_nat [simp]: "fact (n :: nat) >= 1"
-  by (insert fact_nonzero_nat [of n], arith)
-
-lemma fact_ge_Suc_0_nat [simp]: "fact (n :: nat) >= Suc 0"
-  by (insert fact_nonzero_nat [of n], arith)
-
-lemma fact_ge_one_int [simp]: "n >= 0 \<Longrightarrow> fact (n :: int) >= 1"
-  apply (auto simp add: fact_int_def)
-  apply (subgoal_tac "1 = int 1")
-  apply (erule ssubst)
-  apply (subst zle_int)
-  apply auto
-done
-
-lemma dvd_fact_nat [rule_format]: "1 <= m \<longrightarrow> m <= n \<longrightarrow> m dvd fact (n::nat)"
-  apply (induct n rule: induct'_nat)
-  apply (auto simp add: fact_plus_one_nat)
-  apply (subgoal_tac "m = n + 1")
-  apply auto
-done
-
-lemma dvd_fact_int [rule_format]: "1 <= m \<longrightarrow> m <= n \<longrightarrow> m dvd fact (n::int)"
-  apply (case_tac "1 <= n")
-  apply (induct n rule: int_ge_induct)
-  apply (auto simp add: fact_plus_one_int)
-  apply (subgoal_tac "m = i + 1")
-  apply auto
-done
-
-lemma interval_plus_one_nat: "(i::nat) <= j + 1 \<Longrightarrow> 
-  {i..j+1} = {i..j} Un {j+1}"
-  by auto
-
-lemma interval_plus_one_int: "(i::int) <= j + 1 \<Longrightarrow> {i..j+1} = {i..j} Un {j+1}"
-  by auto
-
-lemma fact_altdef_nat: "fact (n::nat) = (PROD i:{1..n}. i)"
-  apply (induct n rule: induct'_nat)
-  apply force
-  apply (subst fact_plus_one_nat)
-  apply (subst interval_plus_one_nat)
-  apply auto
-done
-
-lemma fact_altdef_int: "n >= 0 \<Longrightarrow> fact (n::int) = (PROD i:{1..n}. i)"
-  apply (induct n rule: int_ge_induct)
-  apply force
-  apply (subst fact_plus_one_int, assumption)
-  apply (subst interval_plus_one_int)
-  apply auto
-done
-
-subsection {* Infinitely many primes *}
-
-lemma next_prime_bound: "\<exists>(p::nat). prime p \<and> n < p \<and> p <= fact n + 1"
-proof-
-  have f1: "fact n + 1 \<noteq> 1" using fact_ge_one_nat [of n] by arith 
-  from prime_factor_nat [OF f1]
-      obtain p where "prime p" and "p dvd fact n + 1" by auto
-  hence "p \<le> fact n + 1" 
-    by (intro dvd_imp_le, auto)
-  {assume "p \<le> n"
-    from `prime p` have "p \<ge> 1" 
-      by (cases p, simp_all)
-    with `p <= n` have "p dvd fact n" 
-      by (intro dvd_fact_nat)
-    with `p dvd fact n + 1` have "p dvd fact n + 1 - fact n"
-      by (rule dvd_diff_nat)
-    hence "p dvd 1" by simp
-    hence "p <= 1" by auto
-    moreover from `prime p` have "p > 1" by auto
-    ultimately have False by auto}
-  hence "n < p" by arith
-  with `prime p` and `p <= fact n + 1` show ?thesis by auto
-qed
-
-lemma bigger_prime: "\<exists>p. prime p \<and> p > (n::nat)" 
-using next_prime_bound by auto
-
-lemma primes_infinite: "\<not> (finite {(p::nat). prime p})"
-proof
-  assume "finite {(p::nat). prime p}"
-  with Max_ge have "(EX b. (ALL x : {(p::nat). prime p}. x <= b))"
-    by auto
-  then obtain b where "ALL (x::nat). prime x \<longrightarrow> x <= b"
-    by auto
-  with bigger_prime [of b] show False by auto
-qed
+    transfer_int_nat_binomial transfer_int_nat_binomial_closure]
 
 
 subsection {* Binomial coefficients *}