src/HOL/Number_Theory/Primes.thy
author paulson <lp15@cam.ac.uk>
Sat Feb 01 20:38:29 2014 +0000 (2014-02-01)
changeset 55238 7ddb889e23bd
parent 55215 b6c926e67350
child 55242 413ec965f95d
permissions -rw-r--r--
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
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
lp15@55130
    34
declare One_nat_def [simp]
lp15@55130
    35
huffman@31706
    36
class prime = one +
wenzelm@44872
    37
  fixes prime :: "'a \<Rightarrow> bool"
huffman@31706
    38
huffman@31706
    39
instantiation nat :: prime
huffman@31706
    40
begin
wenzelm@21256
    41
wenzelm@44872
    42
definition prime_nat :: "nat \<Rightarrow> bool"
wenzelm@44872
    43
  where "prime_nat p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
huffman@31706
    44
wenzelm@44872
    45
instance ..
haftmann@23687
    46
huffman@31706
    47
end
huffman@31706
    48
huffman@31706
    49
instantiation int :: prime
huffman@31706
    50
begin
huffman@31706
    51
wenzelm@44872
    52
definition prime_int :: "int \<Rightarrow> bool"
wenzelm@44872
    53
  where "prime_int p = prime (nat p)"
huffman@31706
    54
wenzelm@44872
    55
instance ..
huffman@31706
    56
huffman@31706
    57
end
huffman@31706
    58
huffman@31706
    59
huffman@31706
    60
subsection {* Set up Transfer *}
huffman@31706
    61
haftmann@32479
    62
lemma transfer_nat_int_prime:
huffman@31706
    63
  "(x::int) >= 0 \<Longrightarrow> prime (nat x) = prime x"
wenzelm@44872
    64
  unfolding gcd_int_def lcm_int_def prime_int_def by auto
haftmann@23687
    65
haftmann@35644
    66
declare transfer_morphism_nat_int[transfer add return:
haftmann@32479
    67
    transfer_nat_int_prime]
huffman@31706
    68
wenzelm@44872
    69
lemma transfer_int_nat_prime: "prime (int x) = prime x"
wenzelm@44872
    70
  unfolding gcd_int_def lcm_int_def prime_int_def by auto
huffman@31706
    71
haftmann@35644
    72
declare transfer_morphism_int_nat[transfer add return:
haftmann@32479
    73
    transfer_int_nat_prime]
nipkow@31798
    74
wenzelm@21256
    75
haftmann@32479
    76
subsection {* Primes *}
huffman@31706
    77
nipkow@31952
    78
lemma prime_odd_nat: "prime (p::nat) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
haftmann@54228
    79
  apply (auto simp add: prime_nat_def even_def dvd_eq_mod_eq_0)
haftmann@54228
    80
  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
    81
  done
huffman@31706
    82
nipkow@31952
    83
lemma prime_odd_int: "prime (p::int) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
huffman@31706
    84
  unfolding prime_int_def
nipkow@31952
    85
  apply (frule prime_odd_nat)
huffman@31706
    86
  apply (auto simp add: even_nat_def)
wenzelm@44872
    87
  done
huffman@31706
    88
nipkow@31992
    89
(* FIXME Is there a better way to handle these, rather than making them elim rules? *)
chaieb@22027
    90
nipkow@31952
    91
lemma prime_ge_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 0"
wenzelm@44872
    92
  unfolding prime_nat_def by auto
chaieb@22027
    93
nipkow@31952
    94
lemma prime_gt_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p > 0"
wenzelm@44872
    95
  unfolding prime_nat_def by auto
wenzelm@22367
    96
nipkow@31952
    97
lemma prime_ge_1_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 1"
wenzelm@44872
    98
  unfolding prime_nat_def by auto
chaieb@22027
    99
nipkow@31952
   100
lemma prime_gt_1_nat [elim]: "prime (p::nat) \<Longrightarrow> p > 1"
wenzelm@44872
   101
  unfolding prime_nat_def by auto
wenzelm@22367
   102
nipkow@31952
   103
lemma prime_ge_Suc_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= Suc 0"
wenzelm@44872
   104
  unfolding prime_nat_def by auto
wenzelm@22367
   105
nipkow@31952
   106
lemma prime_gt_Suc_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p > Suc 0"
wenzelm@44872
   107
  unfolding prime_nat_def by auto
huffman@31706
   108
nipkow@31952
   109
lemma prime_ge_2_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 2"
wenzelm@44872
   110
  unfolding prime_nat_def by auto
huffman@31706
   111
nipkow@31952
   112
lemma prime_ge_0_int [elim]: "prime (p::int) \<Longrightarrow> p >= 0"
wenzelm@44872
   113
  unfolding prime_int_def prime_nat_def by auto
wenzelm@22367
   114
nipkow@31952
   115
lemma prime_gt_0_int [elim]: "prime (p::int) \<Longrightarrow> p > 0"
wenzelm@44872
   116
  unfolding prime_int_def prime_nat_def by auto
huffman@31706
   117
nipkow@31952
   118
lemma prime_ge_1_int [elim]: "prime (p::int) \<Longrightarrow> p >= 1"
wenzelm@44872
   119
  unfolding prime_int_def prime_nat_def by auto
chaieb@22027
   120
nipkow@31952
   121
lemma prime_gt_1_int [elim]: "prime (p::int) \<Longrightarrow> p > 1"
wenzelm@44872
   122
  unfolding prime_int_def prime_nat_def by auto
huffman@31706
   123
nipkow@31952
   124
lemma prime_ge_2_int [elim]: "prime (p::int) \<Longrightarrow> p >= 2"
wenzelm@44872
   125
  unfolding prime_int_def prime_nat_def by auto
wenzelm@22367
   126
huffman@31706
   127
huffman@31706
   128
lemma prime_int_altdef: "prime (p::int) = (1 < p \<and> (\<forall>m \<ge> 0. m dvd p \<longrightarrow>
huffman@31706
   129
    m = 1 \<or> m = p))"
huffman@31706
   130
  using prime_nat_def [transferred]
wenzelm@44872
   131
  apply (cases "p >= 0")
wenzelm@44872
   132
  apply blast
wenzelm@44872
   133
  apply (auto simp add: prime_ge_0_int)
wenzelm@44872
   134
  done
huffman@31706
   135
nipkow@31952
   136
lemma prime_imp_coprime_nat: "prime (p::nat) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
huffman@31706
   137
  apply (unfold prime_nat_def)
nipkow@31952
   138
  apply (metis gcd_dvd1_nat gcd_dvd2_nat)
huffman@31706
   139
  done
huffman@31706
   140
nipkow@31952
   141
lemma prime_imp_coprime_int: "prime (p::int) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
huffman@31706
   142
  apply (unfold prime_int_altdef)
nipkow@31952
   143
  apply (metis gcd_dvd1_int gcd_dvd2_int gcd_ge_0_int)
chaieb@27568
   144
  done
chaieb@27568
   145
nipkow@31952
   146
lemma prime_dvd_mult_nat: "prime (p::nat) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
nipkow@31952
   147
  by (blast intro: coprime_dvd_mult_nat prime_imp_coprime_nat)
huffman@31706
   148
nipkow@31952
   149
lemma prime_dvd_mult_int: "prime (p::int) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
nipkow@31952
   150
  by (blast intro: coprime_dvd_mult_int prime_imp_coprime_int)
huffman@31706
   151
nipkow@31952
   152
lemma prime_dvd_mult_eq_nat [simp]: "prime (p::nat) \<Longrightarrow>
huffman@31706
   153
    p dvd m * n = (p dvd m \<or> p dvd n)"
nipkow@31952
   154
  by (rule iffI, rule prime_dvd_mult_nat, auto)
chaieb@27568
   155
nipkow@31952
   156
lemma prime_dvd_mult_eq_int [simp]: "prime (p::int) \<Longrightarrow>
huffman@31706
   157
    p dvd m * n = (p dvd m \<or> p dvd n)"
nipkow@31952
   158
  by (rule iffI, rule prime_dvd_mult_int, auto)
chaieb@27568
   159
nipkow@31952
   160
lemma not_prime_eq_prod_nat: "(n::nat) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
huffman@31706
   161
    EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
huffman@31706
   162
  unfolding prime_nat_def dvd_def apply auto
wenzelm@44872
   163
  by (metis mult_commute linorder_neq_iff linorder_not_le mult_1
wenzelm@44872
   164
      n_less_n_mult_m one_le_mult_iff less_imp_le_nat)
chaieb@27568
   165
nipkow@31952
   166
lemma not_prime_eq_prod_int: "(n::int) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
huffman@31706
   167
    EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
huffman@31706
   168
  unfolding prime_int_altdef dvd_def
huffman@31706
   169
  apply auto
wenzelm@44872
   170
  by (metis div_mult_self1_is_id div_mult_self2_is_id
wenzelm@44872
   171
      int_div_less_self int_one_le_iff_zero_less zero_less_mult_pos less_le)
chaieb@27568
   172
huffman@53598
   173
lemma prime_dvd_power_nat: "prime (p::nat) \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x"
huffman@53598
   174
  by (induct n) auto
chaieb@27568
   175
huffman@53598
   176
lemma prime_dvd_power_int: "prime (p::int) \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x"
lp15@55130
   177
  by (induct n) (auto simp: prime_ge_0_int)
huffman@31706
   178
huffman@53598
   179
lemma prime_dvd_power_nat_iff: "prime (p::nat) \<Longrightarrow> n > 0 \<Longrightarrow>
huffman@53598
   180
    p dvd x^n \<longleftrightarrow> p dvd x"
huffman@53598
   181
  by (cases n) (auto elim: prime_dvd_power_nat)
huffman@53598
   182
huffman@53598
   183
lemma prime_dvd_power_int_iff: "prime (p::int) \<Longrightarrow> n > 0 \<Longrightarrow>
huffman@53598
   184
    p dvd x^n \<longleftrightarrow> p dvd x"
huffman@53598
   185
  by (cases n) (auto elim: prime_dvd_power_int)
huffman@53598
   186
huffman@53598
   187
wenzelm@44872
   188
subsubsection {* Make prime naively executable *}
nipkow@32007
   189
nipkow@32007
   190
lemma zero_not_prime_nat [simp]: "~prime (0::nat)"
nipkow@32007
   191
  by (simp add: prime_nat_def)
nipkow@32007
   192
nipkow@32007
   193
lemma zero_not_prime_int [simp]: "~prime (0::int)"
nipkow@32007
   194
  by (simp add: prime_int_def)
nipkow@32007
   195
nipkow@32007
   196
lemma one_not_prime_nat [simp]: "~prime (1::nat)"
nipkow@32007
   197
  by (simp add: prime_nat_def)
nipkow@32007
   198
nipkow@32007
   199
lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)"
lp15@55130
   200
  by (simp add: prime_nat_def)
nipkow@32007
   201
nipkow@32007
   202
lemma one_not_prime_int [simp]: "~prime (1::int)"
nipkow@32007
   203
  by (simp add: prime_int_def)
nipkow@32007
   204
haftmann@37607
   205
lemma prime_nat_code [code]:
wenzelm@44872
   206
    "prime (p::nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)"
wenzelm@44872
   207
  apply (simp add: Ball_def)
lp15@55130
   208
  apply (metis One_nat_def less_not_refl prime_nat_def dvd_triv_right not_prime_eq_prod_nat)
wenzelm@44872
   209
  done
nipkow@32007
   210
nipkow@32007
   211
lemma prime_nat_simp:
wenzelm@44872
   212
    "prime (p::nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..<p]. \<not> n dvd p)"
wenzelm@44872
   213
  by (auto simp add: prime_nat_code)
nipkow@32007
   214
huffman@47108
   215
lemmas prime_nat_simp_numeral [simp] = prime_nat_simp [of "numeral m"] for m
nipkow@32007
   216
haftmann@37607
   217
lemma prime_int_code [code]:
haftmann@37607
   218
  "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)" (is "?L = ?R")
nipkow@32007
   219
proof
wenzelm@44872
   220
  assume "?L"
wenzelm@44872
   221
  then show "?R"
huffman@44821
   222
    by (clarsimp simp: prime_gt_1_int) (metis int_one_le_iff_zero_less prime_int_altdef less_le)
nipkow@32007
   223
next
wenzelm@44872
   224
  assume "?R"
wenzelm@44872
   225
  then show "?L" by (clarsimp simp: Ball_def) (metis dvdI not_prime_eq_prod_int)
nipkow@32007
   226
qed
nipkow@32007
   227
wenzelm@44872
   228
lemma prime_int_simp: "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..p - 1]. ~ n dvd p)"
wenzelm@44872
   229
  by (auto simp add: prime_int_code)
nipkow@32007
   230
huffman@47108
   231
lemmas prime_int_simp_numeral [simp] = prime_int_simp [of "numeral m"] for m
nipkow@32007
   232
nipkow@32007
   233
lemma two_is_prime_nat [simp]: "prime (2::nat)"
wenzelm@44872
   234
  by simp
nipkow@32007
   235
nipkow@32007
   236
lemma two_is_prime_int [simp]: "prime (2::int)"
wenzelm@44872
   237
  by simp
nipkow@32007
   238
nipkow@32111
   239
text{* A bit of regression testing: *}
nipkow@32111
   240
wenzelm@44872
   241
lemma "prime(97::nat)" by simp
wenzelm@44872
   242
lemma "prime(97::int)" by simp
wenzelm@44872
   243
lemma "prime(997::nat)" by eval
wenzelm@44872
   244
lemma "prime(997::int)" by eval
nipkow@32111
   245
nipkow@32007
   246
nipkow@32007
   247
lemma prime_imp_power_coprime_nat: "prime (p::nat) \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
lp15@55130
   248
  by (metis coprime_exp_nat gcd_nat.commute prime_imp_coprime_nat)
chaieb@27568
   249
nipkow@32007
   250
lemma prime_imp_power_coprime_int: "prime (p::int) \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
lp15@55130
   251
  by (metis coprime_exp_int gcd_int.commute prime_imp_coprime_int)
chaieb@27568
   252
nipkow@31952
   253
lemma primes_coprime_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
lp15@55130
   254
  by (metis gcd_nat.absorb1 gcd_nat.absorb2 prime_imp_coprime_nat)
chaieb@27568
   255
nipkow@31952
   256
lemma primes_coprime_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
lp15@55130
   257
  by (metis leD linear prime_gt_0_int prime_imp_coprime_int prime_int_altdef)
chaieb@27568
   258
wenzelm@44872
   259
lemma primes_imp_powers_coprime_nat:
wenzelm@44872
   260
    "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
nipkow@31952
   261
  by (rule coprime_exp2_nat, rule primes_coprime_nat)
chaieb@27568
   262
wenzelm@44872
   263
lemma primes_imp_powers_coprime_int:
wenzelm@44872
   264
    "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
nipkow@31952
   265
  by (rule coprime_exp2_int, rule primes_coprime_int)
chaieb@27568
   266
nipkow@31952
   267
lemma prime_factor_nat: "n \<noteq> (1::nat) \<Longrightarrow> \<exists> p. prime p \<and> p dvd n"
huffman@31706
   268
  apply (induct n rule: nat_less_induct)
huffman@31706
   269
  apply (case_tac "n = 0")
wenzelm@44872
   270
  using two_is_prime_nat
wenzelm@44872
   271
  apply blast
wenzelm@44872
   272
  apply (metis One_nat_def dvd.order_trans dvd_refl less_Suc0 linorder_neqE_nat
wenzelm@44872
   273
    nat_dvd_not_less neq0_conv prime_nat_def)
wenzelm@44872
   274
  done
chaieb@23244
   275
huffman@31706
   276
text {* One property of coprimality is easier to prove via prime factors. *}
huffman@31706
   277
nipkow@31952
   278
lemma prime_divprod_pow_nat:
huffman@31706
   279
  assumes p: "prime (p::nat)" and ab: "coprime a b" and pab: "p^n dvd a * b"
huffman@31706
   280
  shows "p^n dvd a \<or> p^n dvd b"
huffman@31706
   281
proof-
wenzelm@44872
   282
  { assume "n = 0 \<or> a = 1 \<or> b = 1" with pab have ?thesis
huffman@31706
   283
      apply (cases "n=0", simp_all)
wenzelm@44872
   284
      apply (cases "a=1", simp_all)
wenzelm@44872
   285
      done }
huffman@31706
   286
  moreover
wenzelm@44872
   287
  { assume n: "n \<noteq> 0" and a: "a\<noteq>1" and b: "b\<noteq>1"
wenzelm@44872
   288
    then obtain m where m: "n = Suc m" by (cases n) auto
wenzelm@44872
   289
    from n have "p dvd p^n" apply (intro dvd_power) apply auto done
huffman@31706
   290
    also note pab
huffman@31706
   291
    finally have pab': "p dvd a * b".
nipkow@31952
   292
    from prime_dvd_mult_nat[OF p pab']
huffman@31706
   293
    have "p dvd a \<or> p dvd b" .
huffman@31706
   294
    moreover
nipkow@33946
   295
    { assume pa: "p dvd a"
nipkow@31952
   296
      from coprime_common_divisor_nat [OF ab, OF pa] p have "\<not> p dvd b" by auto
huffman@31706
   297
      with p have "coprime b p"
nipkow@31952
   298
        by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
wenzelm@44872
   299
      then have pnb: "coprime (p^n) b"
nipkow@31952
   300
        by (subst gcd_commute_nat, rule coprime_exp_nat)
nipkow@33946
   301
      from coprime_dvd_mult_nat[OF pnb pab] have ?thesis by blast }
huffman@31706
   302
    moreover
nipkow@33946
   303
    { assume pb: "p dvd b"
huffman@31706
   304
      have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute)
nipkow@31952
   305
      from coprime_common_divisor_nat [OF ab, of p] pb p have "\<not> p dvd a"
huffman@31706
   306
        by auto
huffman@31706
   307
      with p have "coprime a p"
nipkow@31952
   308
        by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
wenzelm@44872
   309
      then have pna: "coprime (p^n) a"
nipkow@31952
   310
        by (subst gcd_commute_nat, rule coprime_exp_nat)
nipkow@33946
   311
      from coprime_dvd_mult_nat[OF pna pnba] have ?thesis by blast }
wenzelm@44872
   312
    ultimately have ?thesis by blast }
huffman@31706
   313
  ultimately show ?thesis by blast
nipkow@23983
   314
qed
nipkow@23983
   315
wenzelm@44872
   316
avigad@32036
   317
subsection {* Infinitely many primes *}
avigad@32036
   318
avigad@32036
   319
lemma next_prime_bound: "\<exists>(p::nat). prime p \<and> n < p \<and> p <= fact n + 1"
avigad@32036
   320
proof-
avigad@32036
   321
  have f1: "fact n + 1 \<noteq> 1" using fact_ge_one_nat [of n] by arith 
avigad@32036
   322
  from prime_factor_nat [OF f1]
wenzelm@44872
   323
  obtain p where "prime p" and "p dvd fact n + 1" by auto
wenzelm@44872
   324
  then have "p \<le> fact n + 1" apply (intro dvd_imp_le) apply auto done
wenzelm@44872
   325
  { assume "p \<le> n"
avigad@32036
   326
    from `prime p` have "p \<ge> 1" 
avigad@32036
   327
      by (cases p, simp_all)
avigad@32036
   328
    with `p <= n` have "p dvd fact n" 
avigad@32036
   329
      by (intro dvd_fact_nat)
avigad@32036
   330
    with `p dvd fact n + 1` have "p dvd fact n + 1 - fact n"
avigad@32036
   331
      by (rule dvd_diff_nat)
wenzelm@44872
   332
    then have "p dvd 1" by simp
wenzelm@44872
   333
    then have "p <= 1" by auto
avigad@32036
   334
    moreover from `prime p` have "p > 1" by auto
avigad@32036
   335
    ultimately have False by auto}
wenzelm@44872
   336
  then have "n < p" by presburger
avigad@32036
   337
  with `prime p` and `p <= fact n + 1` show ?thesis by auto
avigad@32036
   338
qed
avigad@32036
   339
avigad@32036
   340
lemma bigger_prime: "\<exists>p. prime p \<and> p > (n::nat)" 
wenzelm@44872
   341
  using next_prime_bound by auto
avigad@32036
   342
avigad@32036
   343
lemma primes_infinite: "\<not> (finite {(p::nat). prime p})"
avigad@32036
   344
proof
avigad@32036
   345
  assume "finite {(p::nat). prime p}"
avigad@32036
   346
  with Max_ge have "(EX b. (ALL x : {(p::nat). prime p}. x <= b))"
avigad@32036
   347
    by auto
avigad@32036
   348
  then obtain b where "ALL (x::nat). prime x \<longrightarrow> x <= b"
avigad@32036
   349
    by auto
wenzelm@44872
   350
  with bigger_prime [of b] show False
wenzelm@44872
   351
    by auto
avigad@32036
   352
qed
avigad@32036
   353
lp15@55215
   354
subsection{*Powers of Primes*}
lp15@55215
   355
lp15@55215
   356
text{*Versions for type nat only*}
lp15@55215
   357
lp15@55215
   358
lemma prime_product: 
lp15@55215
   359
  fixes p::nat
lp15@55215
   360
  assumes "prime (p * q)"
lp15@55215
   361
  shows "p = 1 \<or> q = 1"
lp15@55215
   362
proof -
lp15@55215
   363
  from assms have 
lp15@55215
   364
    "1 < p * q" and P: "\<And>m. m dvd p * q \<Longrightarrow> m = 1 \<or> m = p * q"
lp15@55215
   365
    unfolding prime_nat_def by auto
lp15@55215
   366
  from `1 < p * q` have "p \<noteq> 0" by (cases p) auto
lp15@55215
   367
  then have Q: "p = p * q \<longleftrightarrow> q = 1" by auto
lp15@55215
   368
  have "p dvd p * q" by simp
lp15@55215
   369
  then have "p = 1 \<or> p = p * q" by (rule P)
lp15@55215
   370
  then show ?thesis by (simp add: Q)
lp15@55215
   371
qed
lp15@55215
   372
lp15@55215
   373
lemma prime_exp: 
lp15@55215
   374
  fixes p::nat
lp15@55215
   375
  shows "prime (p^n) \<longleftrightarrow> prime p \<and> n = 1"
lp15@55215
   376
proof(induct n)
lp15@55215
   377
  case 0 thus ?case by simp
lp15@55215
   378
next
lp15@55215
   379
  case (Suc n)
lp15@55215
   380
  {assume "p = 0" hence ?case by simp}
lp15@55215
   381
  moreover
lp15@55215
   382
  {assume "p=1" hence ?case by simp}
lp15@55215
   383
  moreover
lp15@55215
   384
  {assume p: "p \<noteq> 0" "p\<noteq>1"
lp15@55215
   385
    {assume pp: "prime (p^Suc n)"
lp15@55215
   386
      hence "p = 1 \<or> p^n = 1" using prime_product[of p "p^n"] by simp
lp15@55215
   387
      with p have n: "n = 0"
lp15@55215
   388
        by (metis One_nat_def nat_power_eq_Suc_0_iff)
lp15@55215
   389
      with pp have "prime p \<and> Suc n = 1" by simp}
lp15@55215
   390
    moreover
lp15@55215
   391
    {assume n: "prime p \<and> Suc n = 1" hence "prime (p^Suc n)" by simp}
lp15@55215
   392
    ultimately have ?case by blast}
lp15@55215
   393
  ultimately show ?case by blast
lp15@55215
   394
qed
lp15@55215
   395
lp15@55215
   396
lemma prime_power_mult: 
lp15@55215
   397
  fixes p::nat
lp15@55215
   398
  assumes p: "prime p" and xy: "x * y = p ^ k"
lp15@55215
   399
  shows "\<exists>i j. x = p ^i \<and> y = p^ j"
lp15@55215
   400
using xy
lp15@55215
   401
proof(induct k arbitrary: x y)
lp15@55215
   402
  case 0 thus ?case apply simp by (rule exI[where x="0"], simp)
lp15@55215
   403
next
lp15@55215
   404
  case (Suc k x y)
lp15@55215
   405
  from Suc.prems have pxy: "p dvd x*y" by auto
lp15@55215
   406
  from Primes.prime_dvd_mult_nat [OF p pxy] have pxyc: "p dvd x \<or> p dvd y" .
lp15@55215
   407
  from p have p0: "p \<noteq> 0" by - (rule ccontr, simp) 
lp15@55215
   408
  {assume px: "p dvd x"
lp15@55215
   409
    then obtain d where d: "x = p*d" unfolding dvd_def by blast
lp15@55215
   410
    from Suc.prems d  have "p*d*y = p^Suc k" by simp
lp15@55215
   411
    hence th: "d*y = p^k" using p0 by simp
lp15@55215
   412
    from Suc.hyps[OF th] obtain i j where ij: "d = p^i" "y = p^j" by blast
lp15@55215
   413
    with d have "x = p^Suc i" by simp 
lp15@55215
   414
    with ij(2) have ?case by blast}
lp15@55215
   415
  moreover 
lp15@55215
   416
  {assume px: "p dvd y"
lp15@55215
   417
    then obtain d where d: "y = p*d" unfolding dvd_def by blast
lp15@55215
   418
    from Suc.prems d  have "p*d*x = p^Suc k" by (simp add: mult_commute)
lp15@55215
   419
    hence th: "d*x = p^k" using p0 by simp
lp15@55215
   420
    from Suc.hyps[OF th] obtain i j where ij: "d = p^i" "x = p^j" by blast
lp15@55215
   421
    with d have "y = p^Suc i" by simp 
lp15@55215
   422
    with ij(2) have ?case by blast}
lp15@55215
   423
  ultimately show ?case  using pxyc by blast
lp15@55215
   424
qed
lp15@55215
   425
lp15@55215
   426
lemma prime_power_exp: 
lp15@55215
   427
  fixes p::nat
lp15@55215
   428
  assumes p: "prime p" and n: "n \<noteq> 0" 
lp15@55215
   429
    and xn: "x^n = p^k" shows "\<exists>i. x = p^i"
lp15@55215
   430
  using n xn
lp15@55215
   431
proof(induct n arbitrary: k)
lp15@55215
   432
  case 0 thus ?case by simp
lp15@55215
   433
next
lp15@55215
   434
  case (Suc n k) hence th: "x*x^n = p^k" by simp
lp15@55215
   435
  {assume "n = 0" with Suc have ?case by simp (rule exI[where x="k"], simp)}
lp15@55215
   436
  moreover
lp15@55215
   437
  {assume n: "n \<noteq> 0"
lp15@55215
   438
    from prime_power_mult[OF p th] 
lp15@55215
   439
    obtain i j where ij: "x = p^i" "x^n = p^j"by blast
lp15@55215
   440
    from Suc.hyps[OF n ij(2)] have ?case .}
lp15@55215
   441
  ultimately show ?case by blast
lp15@55215
   442
qed
lp15@55215
   443
lp15@55215
   444
lemma divides_primepow:
lp15@55215
   445
  fixes p::nat
lp15@55215
   446
  assumes p: "prime p" 
lp15@55215
   447
  shows "d dvd p^k \<longleftrightarrow> (\<exists> i. i \<le> k \<and> d = p ^i)"
lp15@55215
   448
proof
lp15@55215
   449
  assume H: "d dvd p^k" then obtain e where e: "d*e = p^k" 
lp15@55215
   450
    unfolding dvd_def  apply (auto simp add: mult_commute) by blast
lp15@55215
   451
  from prime_power_mult[OF p e] obtain i j where ij: "d = p^i" "e=p^j" by blast
lp15@55215
   452
  from e ij have "p^(i + j) = p^k" by (simp add: power_add)
lp15@55215
   453
  hence "i + j = k" using p prime_gt_1_nat power_inject_exp[of p "i+j" k] by simp 
lp15@55215
   454
  hence "i \<le> k" by arith
lp15@55215
   455
  with ij(1) show "\<exists>i\<le>k. d = p ^ i" by blast
lp15@55215
   456
next
lp15@55215
   457
  {fix i assume H: "i \<le> k" "d = p^i"
lp15@55215
   458
    then obtain j where j: "k = i + j"
lp15@55215
   459
      by (metis le_add_diff_inverse)
lp15@55215
   460
    hence "p^k = p^j*d" using H(2) by (simp add: power_add)
lp15@55215
   461
    hence "d dvd p^k" unfolding dvd_def by auto}
lp15@55215
   462
  thus "\<exists>i\<le>k. d = p ^ i \<Longrightarrow> d dvd p ^ k" by blast
lp15@55215
   463
qed
lp15@55215
   464
lp15@55238
   465
subsection {*Chinese Remainder Theorem Variants*}
lp15@55238
   466
lp15@55238
   467
lemma bezout_gcd_nat:
lp15@55238
   468
  fixes a::nat shows "\<exists>x y. a * x - b * y = gcd a b \<or> b * x - a * y = gcd a b"
lp15@55238
   469
  using bezout_nat[of a b]
lp15@55238
   470
by (metis bezout_nat diff_add_inverse gcd_add_mult_nat gcd_nat.commute 
lp15@55238
   471
  gcd_nat.right_neutral mult_0) 
lp15@55238
   472
lp15@55238
   473
lemma gcd_bezout_sum_nat:
lp15@55238
   474
  fixes a::nat 
lp15@55238
   475
  assumes "a * x + b * y = d" 
lp15@55238
   476
  shows "gcd a b dvd d"
lp15@55238
   477
proof-
lp15@55238
   478
  let ?g = "gcd a b"
lp15@55238
   479
    have dv: "?g dvd a*x" "?g dvd b * y" 
lp15@55238
   480
      by simp_all
lp15@55238
   481
    from dvd_add[OF dv] assms
lp15@55238
   482
    show ?thesis by auto
lp15@55238
   483
qed
lp15@55238
   484
lp15@55238
   485
lp15@55238
   486
text {* A binary form of the Chinese Remainder Theorem. *}
lp15@55238
   487
lp15@55238
   488
lemma chinese_remainder: 
lp15@55238
   489
  fixes a::nat  assumes ab: "coprime a b" and a: "a \<noteq> 0" and b: "b \<noteq> 0"
lp15@55238
   490
  shows "\<exists>x q1 q2. x = u + q1 * a \<and> x = v + q2 * b"
lp15@55238
   491
proof-
lp15@55238
   492
  from bezout_add_strong_nat[OF a, of b] bezout_add_strong_nat[OF b, of a]
lp15@55238
   493
  obtain d1 x1 y1 d2 x2 y2 where dxy1: "d1 dvd a" "d1 dvd b" "a * x1 = b * y1 + d1" 
lp15@55238
   494
    and dxy2: "d2 dvd b" "d2 dvd a" "b * x2 = a * y2 + d2" by blast
lp15@55238
   495
  then have d12: "d1 = 1" "d2 =1"
lp15@55238
   496
    by (metis ab coprime_nat)+
lp15@55238
   497
  let ?x = "v * a * x1 + u * b * x2"
lp15@55238
   498
  let ?q1 = "v * x1 + u * y2"
lp15@55238
   499
  let ?q2 = "v * y1 + u * x2"
lp15@55238
   500
  from dxy2(3)[simplified d12] dxy1(3)[simplified d12] 
lp15@55238
   501
  have "?x = u + ?q1 * a" "?x = v + ?q2 * b"
lp15@55238
   502
    apply (auto simp add: algebra_simps) 
lp15@55238
   503
    apply (metis mult_Suc_right nat_mult_assoc nat_mult_commute)+
lp15@55238
   504
    done
lp15@55238
   505
  thus ?thesis by blast
lp15@55238
   506
qed
lp15@55238
   507
lp15@55238
   508
text {* Primality *}
lp15@55238
   509
lp15@55238
   510
lemma coprime_bezout_strong:
lp15@55238
   511
  fixes a::nat assumes "coprime a b"  "b \<noteq> 1"
lp15@55238
   512
  shows "\<exists>x y. a * x = b * y + 1"
lp15@55238
   513
by (metis assms bezout_nat gcd_nat.left_neutral)
lp15@55238
   514
lp15@55238
   515
lemma bezout_prime: 
lp15@55238
   516
  assumes p: "prime p" and pa: "\<not> p dvd a"
lp15@55238
   517
  shows "\<exists>x y. a*x = Suc (p*y)"
lp15@55238
   518
proof-
lp15@55238
   519
  have ap: "coprime a p"
lp15@55238
   520
    by (metis gcd_nat.commute p pa prime_imp_coprime_nat) 
lp15@55238
   521
  from coprime_bezout_strong[OF ap] show ?thesis
lp15@55238
   522
    by (metis Suc_eq_plus1 gcd_lcm_complete_lattice_nat.bot.extremum pa) 
lp15@55238
   523
qed
lp15@55238
   524
wenzelm@21256
   525
end