# 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: "\p. prime p \ p > n" using euclid_bound by auto + lemma primes_infinite: "\ (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 \ {}" 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 \ ?P" . - from Max_ge [OF fP] have contr: "\ p. prime p \ p \ ?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 \ p dvd a \ 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. nnat. (!!n. n \ f n) ==> finite {n. f n \ u}" by (rule_tac B="{..u}" in finite_subset, auto intro: order_trans)