--- 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)"
--- 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)