src/HOL/Number_Theory/Primes.thy
author haftmann
Thu Oct 31 11:44:20 2013 +0100 (2013-10-31)
changeset 54228 229282d53781
parent 53598 2bd8d459ebae
child 55130 70db8d380d62
permissions -rw-r--r--
purely algebraic foundation for even/odd
haftmann@32479
     1
(*  Authors:    Christophe Tabacznyj, Lawrence C. Paulson, Amine Chaieb,
nipkow@31798
     2
                Thomas M. Rasmussen, Jeremy Avigad, Tobias Nipkow
huffman@31706
     3
huffman@31706
     4
haftmann@32479
     5
This file deals with properties of primes. Definitions and lemmas are
haftmann@32479
     6
proved uniformly for the natural numbers and integers.
huffman@31706
     7
huffman@31706
     8
This file combines and revises a number of prior developments.
huffman@31706
     9
huffman@31706
    10
The original theories "GCD" and "Primes" were by Christophe Tabacznyj
huffman@31706
    11
and Lawrence C. Paulson, based on \cite{davenport92}. They introduced
huffman@31706
    12
gcd, lcm, and prime for the natural numbers.
huffman@31706
    13
huffman@31706
    14
The original theory "IntPrimes" was by Thomas M. Rasmussen, and
huffman@31706
    15
extended gcd, lcm, primes to the integers. Amine Chaieb provided
huffman@31706
    16
another extension of the notions to the integers, and added a number
huffman@31706
    17
of results to "Primes" and "GCD". IntPrimes also defined and developed
huffman@31706
    18
the congruence relations on the integers. The notion was extended to
webertj@33718
    19
the natural numbers by Chaieb.
huffman@31706
    20
avigad@32036
    21
Jeremy Avigad combined all of these, made everything uniform for the
avigad@32036
    22
natural numbers and the integers, and added a number of new theorems.
avigad@32036
    23
nipkow@31798
    24
Tobias Nipkow cleaned up a lot.
wenzelm@21256
    25
*)
wenzelm@21256
    26
huffman@31706
    27
haftmann@32479
    28
header {* Primes *}
wenzelm@21256
    29
haftmann@32479
    30
theory Primes
haftmann@37294
    31
imports "~~/src/HOL/GCD"
huffman@31706
    32
begin
huffman@31706
    33
huffman@31706
    34
class prime = one +
wenzelm@44872
    35
  fixes prime :: "'a \<Rightarrow> bool"
huffman@31706
    36
huffman@31706
    37
instantiation nat :: prime
huffman@31706
    38
begin
wenzelm@21256
    39
wenzelm@44872
    40
definition prime_nat :: "nat \<Rightarrow> bool"
wenzelm@44872
    41
  where "prime_nat p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
huffman@31706
    42
wenzelm@44872
    43
instance ..
haftmann@23687
    44
huffman@31706
    45
end
huffman@31706
    46
huffman@31706
    47
instantiation int :: prime
huffman@31706
    48
begin
huffman@31706
    49
wenzelm@44872
    50
definition prime_int :: "int \<Rightarrow> bool"
wenzelm@44872
    51
  where "prime_int p = prime (nat p)"
huffman@31706
    52
wenzelm@44872
    53
instance ..
huffman@31706
    54
huffman@31706
    55
end
huffman@31706
    56
huffman@31706
    57
huffman@31706
    58
subsection {* Set up Transfer *}
huffman@31706
    59
haftmann@32479
    60
lemma transfer_nat_int_prime:
huffman@31706
    61
  "(x::int) >= 0 \<Longrightarrow> prime (nat x) = prime x"
wenzelm@44872
    62
  unfolding gcd_int_def lcm_int_def prime_int_def by auto
haftmann@23687
    63
haftmann@35644
    64
declare transfer_morphism_nat_int[transfer add return:
haftmann@32479
    65
    transfer_nat_int_prime]
huffman@31706
    66
wenzelm@44872
    67
lemma transfer_int_nat_prime: "prime (int x) = prime x"
wenzelm@44872
    68
  unfolding gcd_int_def lcm_int_def prime_int_def by auto
huffman@31706
    69
haftmann@35644
    70
declare transfer_morphism_int_nat[transfer add return:
haftmann@32479
    71
    transfer_int_nat_prime]
nipkow@31798
    72
wenzelm@21256
    73
haftmann@32479
    74
subsection {* Primes *}
huffman@31706
    75
nipkow@31952
    76
lemma prime_odd_nat: "prime (p::nat) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
haftmann@54228
    77
  apply (auto simp add: prime_nat_def even_def dvd_eq_mod_eq_0)
haftmann@54228
    78
  apply (metis dvd_eq_mod_eq_0 even_Suc even_def mod_by_1 nat_dvd_not_less not_mod_2_eq_0_eq_1 zero_less_numeral)
haftmann@54228
    79
  done
huffman@31706
    80
nipkow@31952
    81
lemma prime_odd_int: "prime (p::int) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
huffman@31706
    82
  unfolding prime_int_def
nipkow@31952
    83
  apply (frule prime_odd_nat)
huffman@31706
    84
  apply (auto simp add: even_nat_def)
wenzelm@44872
    85
  done
huffman@31706
    86
nipkow@31992
    87
(* FIXME Is there a better way to handle these, rather than making them elim rules? *)
chaieb@22027
    88
nipkow@31952
    89
lemma prime_ge_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 0"
wenzelm@44872
    90
  unfolding prime_nat_def by auto
chaieb@22027
    91
nipkow@31952
    92
lemma prime_gt_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p > 0"
wenzelm@44872
    93
  unfolding prime_nat_def by auto
wenzelm@22367
    94
nipkow@31952
    95
lemma prime_ge_1_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 1"
wenzelm@44872
    96
  unfolding prime_nat_def by auto
chaieb@22027
    97
nipkow@31952
    98
lemma prime_gt_1_nat [elim]: "prime (p::nat) \<Longrightarrow> p > 1"
wenzelm@44872
    99
  unfolding prime_nat_def by auto
wenzelm@22367
   100
nipkow@31952
   101
lemma prime_ge_Suc_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= Suc 0"
wenzelm@44872
   102
  unfolding prime_nat_def by auto
wenzelm@22367
   103
nipkow@31952
   104
lemma prime_gt_Suc_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p > Suc 0"
wenzelm@44872
   105
  unfolding prime_nat_def by auto
huffman@31706
   106
nipkow@31952
   107
lemma prime_ge_2_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 2"
wenzelm@44872
   108
  unfolding prime_nat_def by auto
huffman@31706
   109
nipkow@31952
   110
lemma prime_ge_0_int [elim]: "prime (p::int) \<Longrightarrow> p >= 0"
wenzelm@44872
   111
  unfolding prime_int_def prime_nat_def by auto
wenzelm@22367
   112
nipkow@31952
   113
lemma prime_gt_0_int [elim]: "prime (p::int) \<Longrightarrow> p > 0"
wenzelm@44872
   114
  unfolding prime_int_def prime_nat_def by auto
huffman@31706
   115
nipkow@31952
   116
lemma prime_ge_1_int [elim]: "prime (p::int) \<Longrightarrow> p >= 1"
wenzelm@44872
   117
  unfolding prime_int_def prime_nat_def by auto
chaieb@22027
   118
nipkow@31952
   119
lemma prime_gt_1_int [elim]: "prime (p::int) \<Longrightarrow> p > 1"
wenzelm@44872
   120
  unfolding prime_int_def prime_nat_def by auto
huffman@31706
   121
nipkow@31952
   122
lemma prime_ge_2_int [elim]: "prime (p::int) \<Longrightarrow> p >= 2"
wenzelm@44872
   123
  unfolding prime_int_def prime_nat_def by auto
wenzelm@22367
   124
huffman@31706
   125
huffman@31706
   126
lemma prime_int_altdef: "prime (p::int) = (1 < p \<and> (\<forall>m \<ge> 0. m dvd p \<longrightarrow>
huffman@31706
   127
    m = 1 \<or> m = p))"
huffman@31706
   128
  using prime_nat_def [transferred]
wenzelm@44872
   129
  apply (cases "p >= 0")
wenzelm@44872
   130
  apply blast
wenzelm@44872
   131
  apply (auto simp add: prime_ge_0_int)
wenzelm@44872
   132
  done
huffman@31706
   133
nipkow@31952
   134
lemma prime_imp_coprime_nat: "prime (p::nat) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
huffman@31706
   135
  apply (unfold prime_nat_def)
nipkow@31952
   136
  apply (metis gcd_dvd1_nat gcd_dvd2_nat)
huffman@31706
   137
  done
huffman@31706
   138
nipkow@31952
   139
lemma prime_imp_coprime_int: "prime (p::int) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
huffman@31706
   140
  apply (unfold prime_int_altdef)
nipkow@31952
   141
  apply (metis gcd_dvd1_int gcd_dvd2_int gcd_ge_0_int)
chaieb@27568
   142
  done
chaieb@27568
   143
nipkow@31952
   144
lemma prime_dvd_mult_nat: "prime (p::nat) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
nipkow@31952
   145
  by (blast intro: coprime_dvd_mult_nat prime_imp_coprime_nat)
huffman@31706
   146
nipkow@31952
   147
lemma prime_dvd_mult_int: "prime (p::int) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
nipkow@31952
   148
  by (blast intro: coprime_dvd_mult_int prime_imp_coprime_int)
huffman@31706
   149
nipkow@31952
   150
lemma prime_dvd_mult_eq_nat [simp]: "prime (p::nat) \<Longrightarrow>
huffman@31706
   151
    p dvd m * n = (p dvd m \<or> p dvd n)"
nipkow@31952
   152
  by (rule iffI, rule prime_dvd_mult_nat, auto)
chaieb@27568
   153
nipkow@31952
   154
lemma prime_dvd_mult_eq_int [simp]: "prime (p::int) \<Longrightarrow>
huffman@31706
   155
    p dvd m * n = (p dvd m \<or> p dvd n)"
nipkow@31952
   156
  by (rule iffI, rule prime_dvd_mult_int, auto)
chaieb@27568
   157
nipkow@31952
   158
lemma not_prime_eq_prod_nat: "(n::nat) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
huffman@31706
   159
    EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
huffman@31706
   160
  unfolding prime_nat_def dvd_def apply auto
wenzelm@44872
   161
  by (metis mult_commute linorder_neq_iff linorder_not_le mult_1
wenzelm@44872
   162
      n_less_n_mult_m one_le_mult_iff less_imp_le_nat)
chaieb@27568
   163
nipkow@31952
   164
lemma not_prime_eq_prod_int: "(n::int) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
huffman@31706
   165
    EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
huffman@31706
   166
  unfolding prime_int_altdef dvd_def
huffman@31706
   167
  apply auto
wenzelm@44872
   168
  by (metis div_mult_self1_is_id div_mult_self2_is_id
wenzelm@44872
   169
      int_div_less_self int_one_le_iff_zero_less zero_less_mult_pos less_le)
chaieb@27568
   170
huffman@53598
   171
lemma prime_dvd_power_nat: "prime (p::nat) \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x"
huffman@53598
   172
  by (induct n) auto
chaieb@27568
   173
huffman@53598
   174
lemma prime_dvd_power_int: "prime (p::int) \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x"
huffman@53598
   175
  apply (induct n)
nipkow@31952
   176
  apply (frule prime_ge_0_int)
huffman@31706
   177
  apply auto
wenzelm@44872
   178
  done
huffman@31706
   179
huffman@53598
   180
lemma prime_dvd_power_nat_iff: "prime (p::nat) \<Longrightarrow> n > 0 \<Longrightarrow>
huffman@53598
   181
    p dvd x^n \<longleftrightarrow> p dvd x"
huffman@53598
   182
  by (cases n) (auto elim: prime_dvd_power_nat)
huffman@53598
   183
huffman@53598
   184
lemma prime_dvd_power_int_iff: "prime (p::int) \<Longrightarrow> n > 0 \<Longrightarrow>
huffman@53598
   185
    p dvd x^n \<longleftrightarrow> p dvd x"
huffman@53598
   186
  by (cases n) (auto elim: prime_dvd_power_int)
huffman@53598
   187
huffman@53598
   188
wenzelm@44872
   189
subsubsection {* Make prime naively executable *}
nipkow@32007
   190
nipkow@32007
   191
lemma zero_not_prime_nat [simp]: "~prime (0::nat)"
nipkow@32007
   192
  by (simp add: prime_nat_def)
nipkow@32007
   193
nipkow@32007
   194
lemma zero_not_prime_int [simp]: "~prime (0::int)"
nipkow@32007
   195
  by (simp add: prime_int_def)
nipkow@32007
   196
nipkow@32007
   197
lemma one_not_prime_nat [simp]: "~prime (1::nat)"
nipkow@32007
   198
  by (simp add: prime_nat_def)
nipkow@32007
   199
nipkow@32007
   200
lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)"
nipkow@32007
   201
  by (simp add: prime_nat_def One_nat_def)
nipkow@32007
   202
nipkow@32007
   203
lemma one_not_prime_int [simp]: "~prime (1::int)"
nipkow@32007
   204
  by (simp add: prime_int_def)
nipkow@32007
   205
haftmann@37607
   206
lemma prime_nat_code [code]:
wenzelm@44872
   207
    "prime (p::nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)"
wenzelm@44872
   208
  apply (simp add: Ball_def)
wenzelm@44872
   209
  apply (metis less_not_refl prime_nat_def dvd_triv_right not_prime_eq_prod_nat)
wenzelm@44872
   210
  done
nipkow@32007
   211
nipkow@32007
   212
lemma prime_nat_simp:
wenzelm@44872
   213
    "prime (p::nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..<p]. \<not> n dvd p)"
wenzelm@44872
   214
  by (auto simp add: prime_nat_code)
nipkow@32007
   215
huffman@47108
   216
lemmas prime_nat_simp_numeral [simp] = prime_nat_simp [of "numeral m"] for m
nipkow@32007
   217
haftmann@37607
   218
lemma prime_int_code [code]:
haftmann@37607
   219
  "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)" (is "?L = ?R")
nipkow@32007
   220
proof
wenzelm@44872
   221
  assume "?L"
wenzelm@44872
   222
  then show "?R"
huffman@44821
   223
    by (clarsimp simp: prime_gt_1_int) (metis int_one_le_iff_zero_less prime_int_altdef less_le)
nipkow@32007
   224
next
wenzelm@44872
   225
  assume "?R"
wenzelm@44872
   226
  then show "?L" by (clarsimp simp: Ball_def) (metis dvdI not_prime_eq_prod_int)
nipkow@32007
   227
qed
nipkow@32007
   228
wenzelm@44872
   229
lemma prime_int_simp: "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..p - 1]. ~ n dvd p)"
wenzelm@44872
   230
  by (auto simp add: prime_int_code)
nipkow@32007
   231
huffman@47108
   232
lemmas prime_int_simp_numeral [simp] = prime_int_simp [of "numeral m"] for m
nipkow@32007
   233
nipkow@32007
   234
lemma two_is_prime_nat [simp]: "prime (2::nat)"
wenzelm@44872
   235
  by simp
nipkow@32007
   236
nipkow@32007
   237
lemma two_is_prime_int [simp]: "prime (2::int)"
wenzelm@44872
   238
  by simp
nipkow@32007
   239
nipkow@32111
   240
text{* A bit of regression testing: *}
nipkow@32111
   241
wenzelm@44872
   242
lemma "prime(97::nat)" by simp
wenzelm@44872
   243
lemma "prime(97::int)" by simp
wenzelm@44872
   244
lemma "prime(997::nat)" by eval
wenzelm@44872
   245
lemma "prime(997::int)" by eval
nipkow@32111
   246
nipkow@32007
   247
nipkow@32007
   248
lemma prime_imp_power_coprime_nat: "prime (p::nat) \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
nipkow@31952
   249
  apply (rule coprime_exp_nat)
nipkow@31952
   250
  apply (subst gcd_commute_nat)
nipkow@31952
   251
  apply (erule (1) prime_imp_coprime_nat)
wenzelm@44872
   252
  done
chaieb@27568
   253
nipkow@32007
   254
lemma prime_imp_power_coprime_int: "prime (p::int) \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
nipkow@31952
   255
  apply (rule coprime_exp_int)
nipkow@31952
   256
  apply (subst gcd_commute_int)
nipkow@31952
   257
  apply (erule (1) prime_imp_coprime_int)
wenzelm@44872
   258
  done
chaieb@27568
   259
nipkow@31952
   260
lemma primes_coprime_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
nipkow@31952
   261
  apply (rule prime_imp_coprime_nat, assumption)
wenzelm@44872
   262
  apply (unfold prime_nat_def)
wenzelm@44872
   263
  apply auto
wenzelm@44872
   264
  done
chaieb@27568
   265
nipkow@31952
   266
lemma primes_coprime_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
nipkow@31952
   267
  apply (rule prime_imp_coprime_int, assumption)
paulson@40461
   268
  apply (unfold prime_int_altdef)
huffman@44821
   269
  apply (metis int_one_le_iff_zero_less less_le)
wenzelm@44872
   270
  done
chaieb@27568
   271
wenzelm@44872
   272
lemma primes_imp_powers_coprime_nat:
wenzelm@44872
   273
    "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
nipkow@31952
   274
  by (rule coprime_exp2_nat, rule primes_coprime_nat)
chaieb@27568
   275
wenzelm@44872
   276
lemma primes_imp_powers_coprime_int:
wenzelm@44872
   277
    "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
nipkow@31952
   278
  by (rule coprime_exp2_int, rule primes_coprime_int)
chaieb@27568
   279
nipkow@31952
   280
lemma prime_factor_nat: "n \<noteq> (1::nat) \<Longrightarrow> \<exists> p. prime p \<and> p dvd n"
huffman@31706
   281
  apply (induct n rule: nat_less_induct)
huffman@31706
   282
  apply (case_tac "n = 0")
wenzelm@44872
   283
  using two_is_prime_nat
wenzelm@44872
   284
  apply blast
wenzelm@44872
   285
  apply (metis One_nat_def dvd.order_trans dvd_refl less_Suc0 linorder_neqE_nat
wenzelm@44872
   286
    nat_dvd_not_less neq0_conv prime_nat_def)
wenzelm@44872
   287
  done
chaieb@23244
   288
huffman@31706
   289
(* An Isar version:
huffman@31706
   290
nipkow@31952
   291
lemma prime_factor_b_nat:
huffman@31706
   292
  fixes n :: nat
huffman@31706
   293
  assumes "n \<noteq> 1"
huffman@31706
   294
  shows "\<exists>p. prime p \<and> p dvd n"
nipkow@23983
   295
huffman@31706
   296
using `n ~= 1`
nipkow@31952
   297
proof (induct n rule: less_induct_nat)
huffman@31706
   298
  fix n :: nat
huffman@31706
   299
  assume "n ~= 1" and
huffman@31706
   300
    ih: "\<forall>m<n. m \<noteq> 1 \<longrightarrow> (\<exists>p. prime p \<and> p dvd m)"
wenzelm@44872
   301
  then show "\<exists>p. prime p \<and> p dvd n"
huffman@31706
   302
  proof -
huffman@31706
   303
  {
huffman@31706
   304
    assume "n = 0"
nipkow@31952
   305
    moreover note two_is_prime_nat
huffman@31706
   306
    ultimately have ?thesis
nipkow@31952
   307
      by (auto simp del: two_is_prime_nat)
huffman@31706
   308
  }
huffman@31706
   309
  moreover
huffman@31706
   310
  {
huffman@31706
   311
    assume "prime n"
wenzelm@44872
   312
    then have ?thesis by auto
huffman@31706
   313
  }
huffman@31706
   314
  moreover
huffman@31706
   315
  {
huffman@31706
   316
    assume "n ~= 0" and "~ prime n"
huffman@31706
   317
    with `n ~= 1` have "n > 1" by auto
nipkow@31952
   318
    with `~ prime n` and not_prime_eq_prod_nat obtain m k where
huffman@31706
   319
      "n = m * k" and "1 < m" and "m < n" by blast
huffman@31706
   320
    with ih obtain p where "prime p" and "p dvd m" by blast
huffman@31706
   321
    with `n = m * k` have ?thesis by auto
huffman@31706
   322
  }
huffman@31706
   323
  ultimately show ?thesis by blast
huffman@31706
   324
  qed
nipkow@23983
   325
qed
nipkow@23983
   326
huffman@31706
   327
*)
huffman@31706
   328
huffman@31706
   329
text {* One property of coprimality is easier to prove via prime factors. *}
huffman@31706
   330
nipkow@31952
   331
lemma prime_divprod_pow_nat:
huffman@31706
   332
  assumes p: "prime (p::nat)" and ab: "coprime a b" and pab: "p^n dvd a * b"
huffman@31706
   333
  shows "p^n dvd a \<or> p^n dvd b"
huffman@31706
   334
proof-
wenzelm@44872
   335
  { assume "n = 0 \<or> a = 1 \<or> b = 1" with pab have ?thesis
huffman@31706
   336
      apply (cases "n=0", simp_all)
wenzelm@44872
   337
      apply (cases "a=1", simp_all)
wenzelm@44872
   338
      done }
huffman@31706
   339
  moreover
wenzelm@44872
   340
  { assume n: "n \<noteq> 0" and a: "a\<noteq>1" and b: "b\<noteq>1"
wenzelm@44872
   341
    then obtain m where m: "n = Suc m" by (cases n) auto
wenzelm@44872
   342
    from n have "p dvd p^n" apply (intro dvd_power) apply auto done
huffman@31706
   343
    also note pab
huffman@31706
   344
    finally have pab': "p dvd a * b".
nipkow@31952
   345
    from prime_dvd_mult_nat[OF p pab']
huffman@31706
   346
    have "p dvd a \<or> p dvd b" .
huffman@31706
   347
    moreover
nipkow@33946
   348
    { assume pa: "p dvd a"
nipkow@31952
   349
      from coprime_common_divisor_nat [OF ab, OF pa] p have "\<not> p dvd b" by auto
huffman@31706
   350
      with p have "coprime b p"
nipkow@31952
   351
        by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
wenzelm@44872
   352
      then have pnb: "coprime (p^n) b"
nipkow@31952
   353
        by (subst gcd_commute_nat, rule coprime_exp_nat)
nipkow@33946
   354
      from coprime_dvd_mult_nat[OF pnb pab] have ?thesis by blast }
huffman@31706
   355
    moreover
nipkow@33946
   356
    { assume pb: "p dvd b"
huffman@31706
   357
      have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute)
nipkow@31952
   358
      from coprime_common_divisor_nat [OF ab, of p] pb p have "\<not> p dvd a"
huffman@31706
   359
        by auto
huffman@31706
   360
      with p have "coprime a p"
nipkow@31952
   361
        by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
wenzelm@44872
   362
      then have pna: "coprime (p^n) a"
nipkow@31952
   363
        by (subst gcd_commute_nat, rule coprime_exp_nat)
nipkow@33946
   364
      from coprime_dvd_mult_nat[OF pna pnba] have ?thesis by blast }
wenzelm@44872
   365
    ultimately have ?thesis by blast }
huffman@31706
   366
  ultimately show ?thesis by blast
nipkow@23983
   367
qed
nipkow@23983
   368
wenzelm@44872
   369
avigad@32036
   370
subsection {* Infinitely many primes *}
avigad@32036
   371
avigad@32036
   372
lemma next_prime_bound: "\<exists>(p::nat). prime p \<and> n < p \<and> p <= fact n + 1"
avigad@32036
   373
proof-
avigad@32036
   374
  have f1: "fact n + 1 \<noteq> 1" using fact_ge_one_nat [of n] by arith 
avigad@32036
   375
  from prime_factor_nat [OF f1]
wenzelm@44872
   376
  obtain p where "prime p" and "p dvd fact n + 1" by auto
wenzelm@44872
   377
  then have "p \<le> fact n + 1" apply (intro dvd_imp_le) apply auto done
wenzelm@44872
   378
  { assume "p \<le> n"
avigad@32036
   379
    from `prime p` have "p \<ge> 1" 
avigad@32036
   380
      by (cases p, simp_all)
avigad@32036
   381
    with `p <= n` have "p dvd fact n" 
avigad@32036
   382
      by (intro dvd_fact_nat)
avigad@32036
   383
    with `p dvd fact n + 1` have "p dvd fact n + 1 - fact n"
avigad@32036
   384
      by (rule dvd_diff_nat)
wenzelm@44872
   385
    then have "p dvd 1" by simp
wenzelm@44872
   386
    then have "p <= 1" by auto
avigad@32036
   387
    moreover from `prime p` have "p > 1" by auto
avigad@32036
   388
    ultimately have False by auto}
wenzelm@44872
   389
  then have "n < p" by presburger
avigad@32036
   390
  with `prime p` and `p <= fact n + 1` show ?thesis by auto
avigad@32036
   391
qed
avigad@32036
   392
avigad@32036
   393
lemma bigger_prime: "\<exists>p. prime p \<and> p > (n::nat)" 
wenzelm@44872
   394
  using next_prime_bound by auto
avigad@32036
   395
avigad@32036
   396
lemma primes_infinite: "\<not> (finite {(p::nat). prime p})"
avigad@32036
   397
proof
avigad@32036
   398
  assume "finite {(p::nat). prime p}"
avigad@32036
   399
  with Max_ge have "(EX b. (ALL x : {(p::nat). prime p}. x <= b))"
avigad@32036
   400
    by auto
avigad@32036
   401
  then obtain b where "ALL (x::nat). prime x \<longrightarrow> x <= b"
avigad@32036
   402
    by auto
wenzelm@44872
   403
  with bigger_prime [of b] show False
wenzelm@44872
   404
    by auto
avigad@32036
   405
qed
avigad@32036
   406
wenzelm@21256
   407
end