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