author nipkow Wed, 06 May 2009 19:15:40 +0200 changeset 31044 6896c2498ac0 parent 31043 df5ade763445 child 31057 0954ed96e2d5
new lemmas
 src/HOL/Library/Primes.thy file | annotate | diff | comparison | revisions src/HOL/SetInterval.thy file | annotate | diff | comparison | revisions
```--- 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})"
-  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 (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  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)"