summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/GCD.thy

changeset 32036 | 8a9228872fbd |

parent 31952 | 40501bb2d57c |

child 32040 | 830141c9e528 |

1.1 --- a/src/HOL/GCD.thy Thu Jul 09 17:34:59 2009 +0200 1.2 +++ b/src/HOL/GCD.thy Fri Jul 10 10:45:30 2009 -0400 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.14 header {* GCD *} 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 @@ -1730,4 +1733,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