src/HOL/GCD.thy
 changeset 32045 efc5f4806cd5 parent 32007 a2a3685f61c3 parent 32040 830141c9e528 child 32111 7c39fcfffd61
```     1.1 --- a/src/HOL/GCD.thy	Thu Jul 16 23:12:12 2009 +0200
1.2 +++ b/src/HOL/GCD.thy	Fri Jul 17 10:07:15 2009 +0200
1.3 @@ -20,6 +20,9 @@
1.4  the congruence relations on the integers. The notion was extended to
1.5  the natural numbers by Chiaeb.
1.6
1.7 +Jeremy Avigad combined all of these, made everything uniform for the
1.8 +natural numbers and the integers, and added a number of new theorems.
1.9 +
1.10  Tobias Nipkow cleaned up a lot.
1.11  *)
1.12
1.13 @@ -27,7 +30,7 @@
1.15
1.16  theory GCD
1.17 -imports NatTransfer
1.18 +imports Fact
1.19  begin
1.20
1.21  declare One_nat_def [simp del]
1.22 @@ -1777,4 +1780,42 @@
1.23    ultimately show ?thesis by blast
1.24  qed
1.25
1.26 +subsection {* Infinitely many primes *}
1.27 +
1.28 +lemma next_prime_bound: "\<exists>(p::nat). prime p \<and> n < p \<and> p <= fact n + 1"
1.29 +proof-
1.30 +  have f1: "fact n + 1 \<noteq> 1" using fact_ge_one_nat [of n] by arith
1.31 +  from prime_factor_nat [OF f1]
1.32 +      obtain p where "prime p" and "p dvd fact n + 1" by auto
1.33 +  hence "p \<le> fact n + 1"
1.34 +    by (intro dvd_imp_le, auto)
1.35 +  {assume "p \<le> n"
1.36 +    from `prime p` have "p \<ge> 1"
1.37 +      by (cases p, simp_all)
1.38 +    with `p <= n` have "p dvd fact n"
1.39 +      by (intro dvd_fact_nat)
1.40 +    with `p dvd fact n + 1` have "p dvd fact n + 1 - fact n"
1.41 +      by (rule dvd_diff_nat)
1.42 +    hence "p dvd 1" by simp
1.43 +    hence "p <= 1" by auto
1.44 +    moreover from `prime p` have "p > 1" by auto
1.45 +    ultimately have False by auto}
1.46 +  hence "n < p" by arith
1.47 +  with `prime p` and `p <= fact n + 1` show ?thesis by auto
1.48 +qed
1.49 +
1.50 +lemma bigger_prime: "\<exists>p. prime p \<and> p > (n::nat)"
1.51 +using next_prime_bound by auto
1.52 +
1.53 +lemma primes_infinite: "\<not> (finite {(p::nat). prime p})"
1.54 +proof
1.55 +  assume "finite {(p::nat). prime p}"
1.56 +  with Max_ge have "(EX b. (ALL x : {(p::nat). prime p}. x <= b))"
1.57 +    by auto
1.58 +  then obtain b where "ALL (x::nat). prime x \<longrightarrow> x <= b"
1.59 +    by auto
1.60 +  with bigger_prime [of b] show False by auto
1.61 +qed
1.62 +
1.63 +
1.64  end
```