# HG changeset patch
# User avigad
# Date 1247237130 14400
# Node ID 8a9228872fbd4a44a5049556bb1493b79cc5e946
# Parent  ccaadfcf6941479b71b97e935ea95c9a4747a2e4
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.

diff -r ccaadfcf6941 -r 8a9228872fbd src/HOL/Fact.thy
--- a/src/HOL/Fact.thy	Thu Jul 09 17:34:59 2009 +0200
+++ b/src/HOL/Fact.thy	Fri Jul 10 10:45:30 2009 -0400
@@ -2,25 +2,266 @@
     Author      : Jacques D. Fleuriot
     Copyright   : 1998  University of Cambridge
     Conversion to Isar and new proofs by Lawrence C Paulson, 2004
+    The integer version of factorial and other additions by Jeremy Avigad.
 *)
 
 header{*Factorial Function*}
 
 theory Fact
-imports Main
+imports NatTransfer
 begin
 
-consts fact :: "nat => nat"
-primrec
-  fact_0:     "fact 0 = 1"
-  fact_Suc:   "fact (Suc n) = (Suc n) * fact n"
+class fact =
+
+fixes 
+  fact :: "'a \<Rightarrow> 'a"
+
+instantiation nat :: fact
+
+begin 
+
+fun
+  fact_nat :: "nat \<Rightarrow> nat"
+where
+  fact_0_nat: "fact_nat 0 = Suc 0"
+| fact_Suc_nat: "fact_nat (Suc x) = Suc x * fact x"
+
+instance proof qed
+
+end
+
+(* definitions for the integers *)
+
+instantiation int :: fact
+
+begin 
+
+definition
+  fact_int :: "int \<Rightarrow> int"
+where  
+  "fact_int x = (if x >= 0 then int (fact (nat x)) else 0)"
+
+instance proof qed
+
+end
+
+
+subsection {* Set up Transfer *}
+
+lemma transfer_nat_int_factorial:
+  "(x::int) >= 0 \<Longrightarrow> fact (nat x) = nat (fact x)"
+  unfolding fact_int_def
+  by auto
+
+
+lemma transfer_nat_int_factorial_closure:
+  "x >= (0::int) \<Longrightarrow> fact x >= 0"
+  by (auto simp add: fact_int_def)
+
+declare TransferMorphism_nat_int[transfer add return: 
+    transfer_nat_int_factorial transfer_nat_int_factorial_closure]
+
+lemma transfer_int_nat_factorial:
+  "fact (int x) = int (fact x)"
+  unfolding fact_int_def by auto
+
+lemma transfer_int_nat_factorial_closure:
+  "is_nat x \<Longrightarrow> fact x >= 0"
+  by (auto simp add: fact_int_def)
+
+declare TransferMorphism_int_nat[transfer add return: 
+    transfer_int_nat_factorial transfer_int_nat_factorial_closure]
 
 
-lemma fact_gt_zero [simp]: "0 < fact n"
-by (induct n) auto
+subsection {* Factorial *}
+
+lemma fact_0_int [simp]: "fact (0::int) = 1"
+  by (simp add: fact_int_def)
+
+lemma fact_1_nat [simp]: "fact (1::nat) = 1"
+  by simp
+
+lemma fact_Suc_0_nat [simp]: "fact (Suc 0) = Suc 0"
+  by simp
+
+lemma fact_1_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_plus_one_int: 
+  assumes "n >= 0"
+  shows "fact ((n::int) + 1) = (n + 1) * fact n"
+
+  using prems unfolding fact_int_def 
+  by (simp add: nat_add_distrib algebra_simps int_mult)
+
+lemma fact_reduce_nat: "(n::nat) > 0 \<Longrightarrow> fact n = n * fact (n - 1)"
+  apply (subgoal_tac "n = Suc (n - 1)")
+  apply (erule ssubst)
+  apply (subst fact_Suc_nat)
+  apply simp_all
+done
+
+lemma fact_reduce_int: "(n::int) > 0 \<Longrightarrow> fact n = n * fact (n - 1)"
+  apply (subgoal_tac "n = (n - 1) + 1")
+  apply (erule ssubst)
+  apply (subst fact_plus_one_int)
+  apply simp_all
+done
+
+lemma fact_nonzero_nat [simp]: "fact (n::nat) \<noteq> 0"
+  apply (induct n)
+  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)
+  apply force
+  apply (auto simp only: fact_Suc_nat)
+  apply (subgoal_tac "m = Suc n")
+  apply (erule ssubst)
+  apply (rule dvd_triv_left)
+  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_Suc: "i <= Suc j \<Longrightarrow> {i..Suc j} = {i..j} Un {Suc j}"
+  by auto
+
+lemma interval_plus_one_int: "(i::int) <= j + 1 \<Longrightarrow> {i..j+1} = {i..j} Un {j+1}"
+  by auto
 
-lemma fact_not_eq_zero [simp]: "fact n \<noteq> 0"
-by simp
+lemma fact_altdef_nat: "fact (n::nat) = (PROD i:{1..n}. i)"
+  apply (induct n)
+  apply force
+  apply (subst fact_Suc_nat)
+  apply (subst interval_Suc)
+  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
+
+lemma fact_mono_nat: "(m::nat) \<le> n \<Longrightarrow> fact m \<le> fact n"
+apply (drule le_imp_less_or_eq)
+apply (auto dest!: less_imp_Suc_add)
+apply (induct_tac k, auto)
+done
+
+lemma fact_neg_int [simp]: "m < (0::int) \<Longrightarrow> fact m = 0"
+  unfolding fact_int_def by auto
+
+lemma fact_ge_zero_int [simp]: "fact m >= (0::int)"
+  apply (case_tac "m >= 0")
+  apply auto
+  apply (frule fact_gt_zero_int)
+  apply arith
+done
+
+lemma fact_mono_int_aux [rule_format]: "k >= (0::int) \<Longrightarrow> 
+    fact (m + k) >= fact m"
+  apply (case_tac "m < 0")
+  apply auto
+  apply (induct k rule: int_ge_induct)
+  apply auto
+  apply (subst add_assoc [symmetric])
+  apply (subst fact_plus_one_int)
+  apply auto
+  apply (erule order_trans)
+  apply (subst mult_le_cancel_right1)
+  apply (subgoal_tac "fact (m + i) >= 0")
+  apply arith
+  apply auto
+done
+
+lemma fact_mono_int: "(m::int) <= n \<Longrightarrow> fact m <= fact n"
+  apply (insert fact_mono_int_aux [of "n - m" "m"])
+  apply auto
+done
+
+text{*Note that @{term "fact 0 = fact 1"}*}
+lemma fact_less_mono_nat: "[| (0::nat) < m; m < n |] ==> fact m < fact n"
+apply (drule_tac m = m in less_imp_Suc_add, auto)
+apply (induct_tac k, auto)
+done
+
+lemma fact_less_mono_int_aux: "k >= 0 \<Longrightarrow> (0::int) < m \<Longrightarrow>
+    fact m < fact ((m + 1) + k)"
+  apply (induct k rule: int_ge_induct)
+  apply (simp add: fact_plus_one_int)
+  apply (subst mult_less_cancel_right1)
+  apply (insert fact_gt_zero_int [of m], arith)
+  apply (subst (2) fact_reduce_int)
+  apply (auto simp add: add_ac)
+  apply (erule order_less_le_trans)
+  apply (subst mult_le_cancel_right1)
+  apply auto
+  apply (subgoal_tac "fact (i + (1 + m)) >= 0")
+  apply force
+  apply (rule fact_ge_zero_int)
+done
+
+lemma fact_less_mono_int: "(0::int) < m \<Longrightarrow> m < n \<Longrightarrow> fact m < fact n"
+  apply (insert fact_less_mono_int_aux [of "n - (m + 1)" "m"])
+  apply auto
+done
+
+lemma fact_num_eq_if_nat: "fact (m::nat) = 
+  (if m=0 then 1 else m * fact (m - 1))"
+by (cases m) auto
+
+lemma fact_add_num_eq_if_nat:
+  "fact ((m::nat) + n) = (if m + n = 0 then 1 else (m + n) * fact (m + n - 1))"
+by (cases "m + n") auto
+
+lemma fact_add_num_eq_if2_nat:
+  "fact ((m::nat) + n) = 
+    (if m = 0 then fact n else (m + n) * fact ((m - 1) + n))"
+by (cases m) auto
+
+
+subsection {* fact and of_nat *}
 
 lemma of_nat_fact_not_zero [simp]: "of_nat (fact n) \<noteq> (0::'a::semiring_char_0)"
 by auto
@@ -33,46 +274,10 @@
 lemma of_nat_fact_ge_zero [simp]: "(0::'a::ordered_semidom) \<le> of_nat(fact n)"
 by simp
 
-lemma fact_ge_one [simp]: "1 \<le> fact n"
-by (induct n) auto
-
-lemma fact_mono: "m \<le> n ==> fact m \<le> fact n"
-apply (drule le_imp_less_or_eq)
-apply (auto dest!: less_imp_Suc_add)
-apply (induct_tac k, auto)
-done
-
-text{*Note that @{term "fact 0 = fact 1"}*}
-lemma fact_less_mono: "[| 0 < m; m < n |] ==> fact m < fact n"
-apply (drule_tac m = m in less_imp_Suc_add, auto)
-apply (induct_tac k, auto)
-done
-
 lemma inv_of_nat_fact_gt_zero [simp]: "(0::'a::ordered_field) < inverse (of_nat (fact n))"
 by (auto simp add: positive_imp_inverse_positive)
 
 lemma inv_of_nat_fact_ge_zero [simp]: "(0::'a::ordered_field) \<le> inverse (of_nat (fact n))"
 by (auto intro: order_less_imp_le)
 
-lemma fact_diff_Suc [rule_format]:
-  "n < Suc m ==> fact (Suc m - n) = (Suc m - n) * fact (m - n)"
-apply (induct n arbitrary: m)
-apply auto
-apply (drule_tac x = "m - Suc 0" in meta_spec, auto)
-done
-
-lemma fact_num0: "fact 0 = 1"
-by auto
-
-lemma fact_num_eq_if: "fact m = (if m=0 then 1 else m * fact (m - 1))"
-by (cases m) auto
-
-lemma fact_add_num_eq_if:
-  "fact (m + n) = (if m + n = 0 then 1 else (m + n) * fact (m + n - 1))"
-by (cases "m + n") auto
-
-lemma fact_add_num_eq_if2:
-  "fact (m + n) = (if m = 0 then fact n else (m + n) * fact ((m - 1) + n))"
-by (cases m) auto
-
 end
diff -r ccaadfcf6941 -r 8a9228872fbd src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Thu Jul 09 17:34:59 2009 +0200
+++ b/src/HOL/GCD.thy	Fri Jul 10 10:45:30 2009 -0400
@@ -20,6 +20,9 @@
 the congruence relations on the integers. The notion was extended to
 the natural numbers by Chiaeb.
 
+Jeremy Avigad combined all of these, made everything uniform for the
+natural numbers and the integers, and added a number of new theorems.
+
 Tobias Nipkow cleaned up a lot.
 *)
 
@@ -27,7 +30,7 @@
 header {* GCD *}
 
 theory GCD
-imports NatTransfer
+imports Fact
 begin
 
 declare One_nat_def [simp del]
@@ -1730,4 +1733,42 @@
   ultimately show ?thesis by blast
 qed
 
+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
+
+
 end
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 *}
diff -r ccaadfcf6941 -r 8a9228872fbd src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Thu Jul 09 17:34:59 2009 +0200
+++ b/src/HOL/Transcendental.thy	Fri Jul 10 10:45:30 2009 -0400
@@ -621,19 +621,19 @@
 
 subsection{* Some properties of factorials *}
 
-lemma real_of_nat_fact_not_zero [simp]: "real (fact n) \<noteq> 0"
+lemma real_of_nat_fact_not_zero [simp]: "real (fact (n::nat)) \<noteq> 0"
 by auto
 
-lemma real_of_nat_fact_gt_zero [simp]: "0 < real(fact n)"
+lemma real_of_nat_fact_gt_zero [simp]: "0 < real(fact (n::nat))"
 by auto
 
-lemma real_of_nat_fact_ge_zero [simp]: "0 \<le> real(fact n)"
+lemma real_of_nat_fact_ge_zero [simp]: "0 \<le> real(fact (n::nat))"
 by simp
 
-lemma inv_real_of_nat_fact_gt_zero [simp]: "0 < inverse (real (fact n))"
+lemma inv_real_of_nat_fact_gt_zero [simp]: "0 < inverse (real (fact (n::nat)))"
 by (auto simp add: positive_imp_inverse_positive)
 
-lemma inv_real_of_nat_fact_ge_zero [simp]: "0 \<le> inverse (real (fact n))"
+lemma inv_real_of_nat_fact_ge_zero [simp]: "0 \<le> inverse (real (fact (n::nat)))"
 by (auto intro: order_less_imp_le)
 
 subsection {* Derivability of power series *}
@@ -1604,11 +1604,11 @@
 apply (rotate_tac 2)
 apply (drule sin_paired [THEN sums_unique, THEN ssubst])
 unfolding One_nat_def
-apply (auto simp del: fact_Suc)
+apply (auto simp del: fact_Suc_nat)
 apply (frule sums_unique)
-apply (auto simp del: fact_Suc)
+apply (auto simp del: fact_Suc_nat)
 apply (rule_tac n1 = 0 in series_pos_less [THEN [2] order_le_less_trans])
-apply (auto simp del: fact_Suc)
+apply (auto simp del: fact_Suc_nat)
 apply (erule sums_summable)
 apply (case_tac "m=0")
 apply (simp (no_asm_simp))
@@ -1617,24 +1617,24 @@
 apply (simp (no_asm_simp) add: numeral_2_eq_2 [symmetric] mult_assoc [symmetric])
 apply (subgoal_tac "x*x < 2*3", simp) 
 apply (rule mult_strict_mono)
-apply (auto simp add: real_0_less_add_iff real_of_nat_Suc simp del: fact_Suc)
-apply (subst fact_Suc)
-apply (subst fact_Suc)
-apply (subst fact_Suc)
-apply (subst fact_Suc)
+apply (auto simp add: real_0_less_add_iff real_of_nat_Suc simp del: fact_Suc_nat)
+apply (subst fact_Suc_nat)
+apply (subst fact_Suc_nat)
+apply (subst fact_Suc_nat)
+apply (subst fact_Suc_nat)
 apply (subst real_of_nat_mult)
 apply (subst real_of_nat_mult)
 apply (subst real_of_nat_mult)
 apply (subst real_of_nat_mult)
-apply (simp (no_asm) add: divide_inverse del: fact_Suc)
-apply (auto simp add: mult_assoc [symmetric] simp del: fact_Suc)
+apply (simp (no_asm) add: divide_inverse del: fact_Suc_nat)
+apply (auto simp add: mult_assoc [symmetric] simp del: fact_Suc_nat)
 apply (rule_tac c="real (Suc (Suc (4*m)))" in mult_less_imp_less_right) 
-apply (auto simp add: mult_assoc simp del: fact_Suc)
+apply (auto simp add: mult_assoc simp del: fact_Suc_nat)
 apply (rule_tac c="real (Suc (Suc (Suc (4*m))))" in mult_less_imp_less_right) 
-apply (auto simp add: mult_assoc mult_less_cancel_left simp del: fact_Suc)
+apply (auto simp add: mult_assoc mult_less_cancel_left simp del: fact_Suc_nat)
 apply (subgoal_tac "x * (x * x ^ (4*m)) = (x ^ (4*m)) * (x * x)") 
 apply (erule ssubst)+
-apply (auto simp del: fact_Suc)
+apply (auto simp del: fact_Suc_nat)
 apply (subgoal_tac "0 < x ^ (4 * m) ")
  prefer 2 apply (simp only: zero_less_power) 
 apply (simp (no_asm_simp) add: mult_less_cancel_left)
@@ -1670,24 +1670,24 @@
 apply (rule_tac y =
  "\<Sum>n=0..< Suc(Suc(Suc 0)). - (-1 ^ n / (real(fact (2*n))) * 2 ^ (2*n))"
        in order_less_trans)
-apply (simp (no_asm) add: fact_num_eq_if realpow_num_eq_if del: fact_Suc)
+apply (simp (no_asm) add: fact_num_eq_if_nat realpow_num_eq_if del: fact_Suc_nat)
 apply (simp (no_asm) add: mult_assoc del: setsum_op_ivl_Suc)
 apply (rule sumr_pos_lt_pair)
 apply (erule sums_summable, safe)
 unfolding One_nat_def
 apply (simp (no_asm) add: divide_inverse real_0_less_add_iff mult_assoc [symmetric] 
-            del: fact_Suc)
+            del: fact_Suc_nat)
 apply (rule real_mult_inverse_cancel2)
 apply (rule real_of_nat_fact_gt_zero)+
-apply (simp (no_asm) add: mult_assoc [symmetric] del: fact_Suc)
+apply (simp (no_asm) add: mult_assoc [symmetric] del: fact_Suc_nat)
 apply (subst fact_lemma) 
-apply (subst fact_Suc [of "Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))"])
+apply (subst fact_Suc_nat [of "Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))"])
 apply (simp only: real_of_nat_mult)
 apply (rule mult_strict_mono, force)
   apply (rule_tac [3] real_of_nat_ge_zero)
  prefer 2 apply force
 apply (rule real_of_nat_less_iff [THEN iffD2])
-apply (rule fact_less_mono, auto)
+apply (rule fact_less_mono_nat, auto)
 done
 
 lemmas cos_two_neq_zero [simp] = cos_two_less_zero [THEN less_imp_neq]