# HG changeset patch
# User nipkow
# Date 1241630140 -7200
# Node ID 6896c2498ac0e7f0a89bb9d93c37047124ff7609
# Parent  df5ade76344530e8efabf6b900efbdbc788dd588
new lemmas

diff -r df5ade763445 -r 6896c2498ac0 src/HOL/Library/Primes.thy
--- a/src/HOL/Library/Primes.thy	Wed May 06 09:58:24 2009 +0200
+++ b/src/HOL/Library/Primes.thy	Wed May 06 19:15:40 2009 +0200
@@ -454,19 +454,11 @@
 qed
 
 lemma euclid: "\<exists>p. prime p \<and> p > n" using euclid_bound by auto
+
 lemma primes_infinite: "\<not> (finite {p. prime p})"
-proof (auto simp add: finite_conv_nat_seg_image)
-  fix n f 
-  assume H: "Collect prime = f ` {i. i < (n::nat)}"
-  let ?P = "Collect prime"
-  let ?m = "Max ?P"
-  have P0: "?P \<noteq> {}" using two_is_prime by auto
-  from H have fP: "finite ?P" using finite_conv_nat_seg_image by blast 
-  from Max_in [OF fP P0] have "?m \<in> ?P" . 
-  from Max_ge [OF fP] have contr: "\<forall> p. prime p \<longrightarrow> p \<le> ?m" by blast
-  from euclid [of ?m] obtain q where q: "prime q" "q > ?m" by blast
-  with contr show False by auto
-qed
+apply(simp add: finite_nat_set_iff_bounded_le)
+apply (metis euclid linorder_not_le)
+done
 
 lemma coprime_prime: assumes ab: "coprime a b"
   shows "~(prime p \<and> p dvd a \<and> p dvd b)"
diff -r df5ade763445 -r 6896c2498ac0 src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Wed May 06 09:58:24 2009 +0200
+++ b/src/HOL/SetInterval.thy	Wed May 06 19:15:40 2009 +0200
@@ -397,6 +397,22 @@
  apply (rule_tac [2] finite_lessThan, auto)
 done
 
+text {* A set of natural numbers is finite iff it is bounded. *}
+lemma finite_nat_set_iff_bounded:
+  "finite(N::nat set) = (EX m. ALL n:N. n<m)" (is "?F = ?B")
+proof
+  assume f:?F  show ?B
+    using Max_ge[OF `?F`, simplified less_Suc_eq_le[symmetric]] by blast
+next
+  assume ?B show ?F using `?B` by(blast intro:bounded_nat_set_is_finite)
+qed
+
+lemma finite_nat_set_iff_bounded_le:
+  "finite(N::nat set) = (EX m. ALL n:N. n<=m)"
+apply(simp add:finite_nat_set_iff_bounded)
+apply(blast dest:less_imp_le_nat le_imp_less_Suc)
+done
+
 lemma finite_less_ub:
      "!!f::nat=>nat. (!!n. n \<le> f n) ==> finite {n. f n \<le> u}"
 by (rule_tac B="{..u}" in finite_subset, auto intro: order_trans)