src/HOL/Number_Theory/Primes.thy
author haftmann
Wed Feb 17 21:51:57 2016 +0100 (2016-02-17)
changeset 62349 7c23469b5118
parent 62348 9a5f43dac883
child 62410 2fc7a8d9c529
permissions -rw-r--r--
cleansed junk-producing interpretations for gcd/lcm on nat altogether
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
wenzelm@58623
    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
wenzelm@60526
    28
section \<open>Primes\<close>
wenzelm@21256
    29
haftmann@32479
    30
theory Primes
lp15@59669
    31
imports "~~/src/HOL/GCD" "~~/src/HOL/Binomial"
huffman@31706
    32
begin
huffman@31706
    33
lp15@55242
    34
declare [[coercion int]]
lp15@55242
    35
declare [[coercion_enabled]]
huffman@31706
    36
lp15@55242
    37
definition prime :: "nat \<Rightarrow> bool"
haftmann@60804
    38
  where "prime p = (1 < p \<and> (\<forall>m. m dvd p \<longrightarrow> m = 1 \<or> m = p))"
huffman@31706
    39
wenzelm@60526
    40
subsection \<open>Primes\<close>
huffman@31706
    41
lp15@55242
    42
lemma prime_odd_nat: "prime p \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
lp15@61762
    43
  apply (auto simp add: prime_def even_iff_mod_2_eq_zero dvd_eq_mod_eq_0)
haftmann@60688
    44
  apply (metis dvd_eq_mod_eq_0 even_Suc mod_by_1 nat_dvd_not_less not_mod_2_eq_0_eq_1 zero_less_numeral)
haftmann@54228
    45
  done
huffman@31706
    46
lp15@61762
    47
lemma prime_gt_0_nat: "prime p \<Longrightarrow> p > 0"
lp15@61762
    48
  unfolding prime_def by auto
chaieb@22027
    49
lp15@61762
    50
lemma prime_ge_1_nat: "prime p \<Longrightarrow> p >= 1"
lp15@61762
    51
  unfolding prime_def by auto
chaieb@22027
    52
lp15@61762
    53
lemma prime_gt_1_nat: "prime p \<Longrightarrow> p > 1"
lp15@61762
    54
  unfolding prime_def by auto
wenzelm@22367
    55
lp15@61762
    56
lemma prime_ge_Suc_0_nat: "prime p \<Longrightarrow> p >= Suc 0"
lp15@61762
    57
  unfolding prime_def by auto
huffman@31706
    58
lp15@61762
    59
lemma prime_gt_Suc_0_nat: "prime p \<Longrightarrow> p > Suc 0"
lp15@61762
    60
  unfolding prime_def by auto
huffman@31706
    61
lp15@61762
    62
lemma prime_ge_2_nat: "prime p \<Longrightarrow> p >= 2"
lp15@61762
    63
  unfolding prime_def by auto
huffman@31706
    64
lp15@55242
    65
lemma prime_imp_coprime_nat: "prime p \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
lp15@61762
    66
  apply (unfold prime_def)
haftmann@62348
    67
  apply (metis gcd_dvd1 gcd_dvd2)
huffman@31706
    68
  done
huffman@31706
    69
lp15@59669
    70
lemma prime_int_altdef:
lp15@55242
    71
  "prime p = (1 < p \<and> (\<forall>m::int. m \<ge> 0 \<longrightarrow> m dvd p \<longrightarrow>
lp15@55242
    72
    m = 1 \<or> m = p))"
lp15@55242
    73
  apply (simp add: prime_def)
lp15@55242
    74
  apply (auto simp add: )
haftmann@62348
    75
  apply (metis One_nat_def of_nat_1 nat_0_le nat_dvd_iff)
lp15@55242
    76
  apply (metis zdvd_int One_nat_def le0 of_nat_0 of_nat_1 of_nat_eq_iff of_nat_le_iff)
lp15@55242
    77
  done
lp15@55242
    78
lp15@55242
    79
lemma prime_imp_coprime_int:
lp15@55242
    80
  fixes n::int shows "prime p \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
huffman@31706
    81
  apply (unfold prime_int_altdef)
haftmann@62348
    82
  apply (metis gcd_dvd1 gcd_dvd2 gcd_ge_0_int)
chaieb@27568
    83
  done
chaieb@27568
    84
lp15@55242
    85
lemma prime_dvd_mult_nat: "prime p \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
haftmann@62348
    86
  by (blast intro: coprime_dvd_mult prime_imp_coprime_nat)
huffman@31706
    87
lp15@59669
    88
lemma prime_dvd_mult_int:
lp15@55242
    89
  fixes n::int shows "prime p \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
haftmann@62348
    90
  by (blast intro: coprime_dvd_mult prime_imp_coprime_int)
huffman@31706
    91
lp15@55242
    92
lemma prime_dvd_mult_eq_nat [simp]: "prime p \<Longrightarrow>
huffman@31706
    93
    p dvd m * n = (p dvd m \<or> p dvd n)"
nipkow@31952
    94
  by (rule iffI, rule prime_dvd_mult_nat, auto)
chaieb@27568
    95
lp15@55242
    96
lemma prime_dvd_mult_eq_int [simp]:
lp15@59669
    97
  fixes n::int
lp15@55242
    98
  shows "prime p \<Longrightarrow> p dvd m * n = (p dvd m \<or> p dvd n)"
nipkow@31952
    99
  by (rule iffI, rule prime_dvd_mult_int, auto)
chaieb@27568
   100
nipkow@31952
   101
lemma not_prime_eq_prod_nat: "(n::nat) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
huffman@31706
   102
    EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
lp15@61762
   103
  unfolding prime_def dvd_def apply auto
haftmann@57512
   104
  by (metis mult.commute linorder_neq_iff linorder_not_le mult_1
wenzelm@44872
   105
      n_less_n_mult_m one_le_mult_iff less_imp_le_nat)
chaieb@27568
   106
lp15@55242
   107
lemma prime_dvd_power_nat: "prime p \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x"
huffman@53598
   108
  by (induct n) auto
chaieb@27568
   109
lp15@55242
   110
lemma prime_dvd_power_int:
lp15@55242
   111
  fixes x::int shows "prime p \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x"
lp15@55242
   112
  by (induct n) auto
huffman@31706
   113
lp15@55242
   114
lemma prime_dvd_power_nat_iff: "prime p \<Longrightarrow> n > 0 \<Longrightarrow>
huffman@53598
   115
    p dvd x^n \<longleftrightarrow> p dvd x"
huffman@53598
   116
  by (cases n) (auto elim: prime_dvd_power_nat)
huffman@53598
   117
lp15@55242
   118
lemma prime_dvd_power_int_iff:
lp15@59669
   119
  fixes x::int
lp15@55242
   120
  shows "prime p \<Longrightarrow> n > 0 \<Longrightarrow> p dvd x^n \<longleftrightarrow> p dvd x"
huffman@53598
   121
  by (cases n) (auto elim: prime_dvd_power_int)
huffman@53598
   122
huffman@53598
   123
wenzelm@60526
   124
subsubsection \<open>Make prime naively executable\<close>
nipkow@32007
   125
nipkow@32007
   126
lemma zero_not_prime_nat [simp]: "~prime (0::nat)"
lp15@61762
   127
  by (simp add: prime_def)
nipkow@32007
   128
nipkow@32007
   129
lemma one_not_prime_nat [simp]: "~prime (1::nat)"
lp15@61762
   130
  by (simp add: prime_def)
nipkow@32007
   131
nipkow@32007
   132
lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)"
lp15@61762
   133
  by (simp add: prime_def)
nipkow@32007
   134
haftmann@37607
   135
lemma prime_nat_code [code]:
lp15@55242
   136
    "prime p \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)"
wenzelm@44872
   137
  apply (simp add: Ball_def)
lp15@61762
   138
  apply (metis One_nat_def less_not_refl prime_def dvd_triv_right not_prime_eq_prod_nat)
wenzelm@44872
   139
  done
nipkow@32007
   140
nipkow@32007
   141
lemma prime_nat_simp:
lp15@55242
   142
    "prime p \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..<p]. \<not> n dvd p)"
wenzelm@44872
   143
  by (auto simp add: prime_nat_code)
nipkow@32007
   144
huffman@47108
   145
lemmas prime_nat_simp_numeral [simp] = prime_nat_simp [of "numeral m"] for m
nipkow@32007
   146
nipkow@32007
   147
lemma two_is_prime_nat [simp]: "prime (2::nat)"
wenzelm@44872
   148
  by simp
nipkow@32007
   149
wenzelm@60526
   150
text\<open>A bit of regression testing:\<close>
nipkow@32111
   151
haftmann@58954
   152
lemma "prime(97::nat)" by simp
wenzelm@44872
   153
lemma "prime(997::nat)" by eval
nipkow@32111
   154
nipkow@32007
   155
lp15@55242
   156
lemma prime_imp_power_coprime_nat: "prime p \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
haftmann@60688
   157
  by (metis coprime_exp_nat gcd.commute prime_imp_coprime_nat)
chaieb@27568
   158
lp15@55242
   159
lemma prime_imp_power_coprime_int:
lp15@55242
   160
  fixes a::int shows "prime p \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
haftmann@60688
   161
  by (metis coprime_exp_int gcd.commute prime_imp_coprime_int)
chaieb@27568
   162
lp15@55242
   163
lemma primes_coprime_nat: "prime p \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
lp15@55130
   164
  by (metis gcd_nat.absorb1 gcd_nat.absorb2 prime_imp_coprime_nat)
chaieb@27568
   165
wenzelm@44872
   166
lemma primes_imp_powers_coprime_nat:
lp15@55242
   167
    "prime p \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
nipkow@31952
   168
  by (rule coprime_exp2_nat, rule primes_coprime_nat)
chaieb@27568
   169
haftmann@62349
   170
lemma prime_factor_nat:
haftmann@62349
   171
  "n \<noteq> (1::nat) \<Longrightarrow> \<exists>p. prime p \<and> p dvd n"
haftmann@62349
   172
proof (induct n rule: nat_less_induct)
haftmann@62349
   173
  case (1 n) show ?case
haftmann@62349
   174
  proof (cases "n = 0")
haftmann@62349
   175
    case True then show ?thesis
haftmann@62349
   176
    by (auto intro: two_is_prime_nat)
haftmann@62349
   177
  next
haftmann@62349
   178
    case False with "1.prems" have "n > 1" by simp
haftmann@62349
   179
    with "1.hyps" show ?thesis
haftmann@62349
   180
    by (metis One_nat_def dvd_mult dvd_refl not_prime_eq_prod_nat order_less_irrefl)
haftmann@62349
   181
  qed
haftmann@62349
   182
qed
chaieb@23244
   183
wenzelm@60526
   184
text \<open>One property of coprimality is easier to prove via prime factors.\<close>
huffman@31706
   185
nipkow@31952
   186
lemma prime_divprod_pow_nat:
lp15@55242
   187
  assumes p: "prime p" and ab: "coprime a b" and pab: "p^n dvd a * b"
huffman@31706
   188
  shows "p^n dvd a \<or> p^n dvd b"
huffman@31706
   189
proof-
wenzelm@44872
   190
  { assume "n = 0 \<or> a = 1 \<or> b = 1" with pab have ?thesis
huffman@31706
   191
      apply (cases "n=0", simp_all)
wenzelm@44872
   192
      apply (cases "a=1", simp_all)
wenzelm@44872
   193
      done }
huffman@31706
   194
  moreover
wenzelm@44872
   195
  { assume n: "n \<noteq> 0" and a: "a\<noteq>1" and b: "b\<noteq>1"
wenzelm@44872
   196
    then obtain m where m: "n = Suc m" by (cases n) auto
wenzelm@44872
   197
    from n have "p dvd p^n" apply (intro dvd_power) apply auto done
huffman@31706
   198
    also note pab
huffman@31706
   199
    finally have pab': "p dvd a * b".
nipkow@31952
   200
    from prime_dvd_mult_nat[OF p pab']
huffman@31706
   201
    have "p dvd a \<or> p dvd b" .
huffman@31706
   202
    moreover
nipkow@33946
   203
    { assume pa: "p dvd a"
nipkow@31952
   204
      from coprime_common_divisor_nat [OF ab, OF pa] p have "\<not> p dvd b" by auto
huffman@31706
   205
      with p have "coprime b p"
haftmann@62348
   206
        by (subst gcd.commute, intro prime_imp_coprime_nat)
wenzelm@44872
   207
      then have pnb: "coprime (p^n) b"
haftmann@62348
   208
        by (subst gcd.commute, rule coprime_exp_nat)
haftmann@62348
   209
      from coprime_dvd_mult[OF pnb pab] have ?thesis by blast }
huffman@31706
   210
    moreover
nipkow@33946
   211
    { assume pb: "p dvd b"
haftmann@57512
   212
      have pnba: "p^n dvd b*a" using pab by (simp add: mult.commute)
nipkow@31952
   213
      from coprime_common_divisor_nat [OF ab, of p] pb p have "\<not> p dvd a"
huffman@31706
   214
        by auto
huffman@31706
   215
      with p have "coprime a p"
haftmann@62348
   216
        by (subst gcd.commute, intro prime_imp_coprime_nat)
wenzelm@44872
   217
      then have pna: "coprime (p^n) a"
haftmann@62348
   218
        by (subst gcd.commute, rule coprime_exp_nat)
haftmann@62348
   219
      from coprime_dvd_mult[OF pna pnba] have ?thesis by blast }
wenzelm@44872
   220
    ultimately have ?thesis by blast }
huffman@31706
   221
  ultimately show ?thesis by blast
nipkow@23983
   222
qed
nipkow@23983
   223
wenzelm@44872
   224
wenzelm@60526
   225
subsection \<open>Infinitely many primes\<close>
avigad@32036
   226
lp15@55242
   227
lemma next_prime_bound: "\<exists>p. prime p \<and> n < p \<and> p <= fact n + 1"
avigad@32036
   228
proof-
lp15@59730
   229
  have f1: "fact n + 1 \<noteq> (1::nat)" using fact_ge_1 [of n, where 'a=nat] by arith
avigad@32036
   230
  from prime_factor_nat [OF f1]
wenzelm@44872
   231
  obtain p where "prime p" and "p dvd fact n + 1" by auto
wenzelm@44872
   232
  then have "p \<le> fact n + 1" apply (intro dvd_imp_le) apply auto done
wenzelm@44872
   233
  { assume "p \<le> n"
wenzelm@60526
   234
    from \<open>prime p\<close> have "p \<ge> 1"
avigad@32036
   235
      by (cases p, simp_all)
wenzelm@60526
   236
    with \<open>p <= n\<close> have "p dvd fact n"
lp15@59730
   237
      by (intro dvd_fact)
wenzelm@60526
   238
    with \<open>p dvd fact n + 1\<close> have "p dvd fact n + 1 - fact n"
avigad@32036
   239
      by (rule dvd_diff_nat)
wenzelm@44872
   240
    then have "p dvd 1" by simp
wenzelm@44872
   241
    then have "p <= 1" by auto
lp15@61762
   242
    moreover from \<open>prime p\<close> have "p > 1"
lp15@61762
   243
      using prime_def by blast
avigad@32036
   244
    ultimately have False by auto}
wenzelm@44872
   245
  then have "n < p" by presburger
wenzelm@60526
   246
  with \<open>prime p\<close> and \<open>p <= fact n + 1\<close> show ?thesis by auto
avigad@32036
   247
qed
avigad@32036
   248
lp15@59669
   249
lemma bigger_prime: "\<exists>p. prime p \<and> p > (n::nat)"
wenzelm@44872
   250
  using next_prime_bound by auto
avigad@32036
   251
avigad@32036
   252
lemma primes_infinite: "\<not> (finite {(p::nat). prime p})"
avigad@32036
   253
proof
avigad@32036
   254
  assume "finite {(p::nat). prime p}"
avigad@32036
   255
  with Max_ge have "(EX b. (ALL x : {(p::nat). prime p}. x <= b))"
avigad@32036
   256
    by auto
avigad@32036
   257
  then obtain b where "ALL (x::nat). prime x \<longrightarrow> x <= b"
avigad@32036
   258
    by auto
wenzelm@44872
   259
  with bigger_prime [of b] show False
wenzelm@44872
   260
    by auto
avigad@32036
   261
qed
avigad@32036
   262
wenzelm@60526
   263
subsection\<open>Powers of Primes\<close>
lp15@55215
   264
wenzelm@60526
   265
text\<open>Versions for type nat only\<close>
lp15@55215
   266
lp15@59669
   267
lemma prime_product:
lp15@55215
   268
  fixes p::nat
lp15@55215
   269
  assumes "prime (p * q)"
lp15@55215
   270
  shows "p = 1 \<or> q = 1"
lp15@55215
   271
proof -
lp15@59669
   272
  from assms have
lp15@55215
   273
    "1 < p * q" and P: "\<And>m. m dvd p * q \<Longrightarrow> m = 1 \<or> m = p * q"
lp15@61762
   274
    unfolding prime_def by auto
wenzelm@60526
   275
  from \<open>1 < p * q\<close> have "p \<noteq> 0" by (cases p) auto
lp15@55215
   276
  then have Q: "p = p * q \<longleftrightarrow> q = 1" by auto
lp15@55215
   277
  have "p dvd p * q" by simp
lp15@55215
   278
  then have "p = 1 \<or> p = p * q" by (rule P)
lp15@55215
   279
  then show ?thesis by (simp add: Q)
lp15@55215
   280
qed
lp15@55215
   281
lp15@59669
   282
lemma prime_exp:
lp15@55215
   283
  fixes p::nat
lp15@55215
   284
  shows "prime (p^n) \<longleftrightarrow> prime p \<and> n = 1"
lp15@55215
   285
proof(induct n)
lp15@55215
   286
  case 0 thus ?case by simp
lp15@55215
   287
next
lp15@55215
   288
  case (Suc n)
lp15@55215
   289
  {assume "p = 0" hence ?case by simp}
lp15@55215
   290
  moreover
lp15@55215
   291
  {assume "p=1" hence ?case by simp}
lp15@55215
   292
  moreover
lp15@55215
   293
  {assume p: "p \<noteq> 0" "p\<noteq>1"
lp15@55215
   294
    {assume pp: "prime (p^Suc n)"
lp15@55215
   295
      hence "p = 1 \<or> p^n = 1" using prime_product[of p "p^n"] by simp
lp15@55215
   296
      with p have n: "n = 0"
lp15@55215
   297
        by (metis One_nat_def nat_power_eq_Suc_0_iff)
lp15@55215
   298
      with pp have "prime p \<and> Suc n = 1" by simp}
lp15@55215
   299
    moreover
lp15@55215
   300
    {assume n: "prime p \<and> Suc n = 1" hence "prime (p^Suc n)" by simp}
lp15@55215
   301
    ultimately have ?case by blast}
lp15@55215
   302
  ultimately show ?case by blast
lp15@55215
   303
qed
lp15@55215
   304
lp15@59669
   305
lemma prime_power_mult:
lp15@55215
   306
  fixes p::nat
lp15@55215
   307
  assumes p: "prime p" and xy: "x * y = p ^ k"
lp15@55215
   308
  shows "\<exists>i j. x = p ^i \<and> y = p^ j"
lp15@55215
   309
using xy
lp15@55215
   310
proof(induct k arbitrary: x y)
lp15@55215
   311
  case 0 thus ?case apply simp by (rule exI[where x="0"], simp)
lp15@55215
   312
next
lp15@55215
   313
  case (Suc k x y)
lp15@55215
   314
  from Suc.prems have pxy: "p dvd x*y" by auto
lp15@55215
   315
  from Primes.prime_dvd_mult_nat [OF p pxy] have pxyc: "p dvd x \<or> p dvd y" .
lp15@59669
   316
  from p have p0: "p \<noteq> 0" by - (rule ccontr, simp)
lp15@55215
   317
  {assume px: "p dvd x"
lp15@55215
   318
    then obtain d where d: "x = p*d" unfolding dvd_def by blast
lp15@55215
   319
    from Suc.prems d  have "p*d*y = p^Suc k" by simp
lp15@55215
   320
    hence th: "d*y = p^k" using p0 by simp
lp15@55215
   321
    from Suc.hyps[OF th] obtain i j where ij: "d = p^i" "y = p^j" by blast
lp15@59669
   322
    with d have "x = p^Suc i" by simp
lp15@55215
   323
    with ij(2) have ?case by blast}
lp15@59669
   324
  moreover
lp15@55215
   325
  {assume px: "p dvd y"
lp15@55215
   326
    then obtain d where d: "y = p*d" unfolding dvd_def by blast
haftmann@57512
   327
    from Suc.prems d  have "p*d*x = p^Suc k" by (simp add: mult.commute)
lp15@55215
   328
    hence th: "d*x = p^k" using p0 by simp
lp15@55215
   329
    from Suc.hyps[OF th] obtain i j where ij: "d = p^i" "x = p^j" by blast
lp15@59669
   330
    with d have "y = p^Suc i" by simp
lp15@55215
   331
    with ij(2) have ?case by blast}
lp15@55215
   332
  ultimately show ?case  using pxyc by blast
lp15@55215
   333
qed
lp15@55215
   334
lp15@59669
   335
lemma prime_power_exp:
lp15@55215
   336
  fixes p::nat
lp15@59669
   337
  assumes p: "prime p" and n: "n \<noteq> 0"
lp15@55215
   338
    and xn: "x^n = p^k" shows "\<exists>i. x = p^i"
lp15@55215
   339
  using n xn
lp15@55215
   340
proof(induct n arbitrary: k)
lp15@55215
   341
  case 0 thus ?case by simp
lp15@55215
   342
next
lp15@55215
   343
  case (Suc n k) hence th: "x*x^n = p^k" by simp
lp15@55215
   344
  {assume "n = 0" with Suc have ?case by simp (rule exI[where x="k"], simp)}
lp15@55215
   345
  moreover
lp15@55215
   346
  {assume n: "n \<noteq> 0"
lp15@59669
   347
    from prime_power_mult[OF p th]
lp15@55215
   348
    obtain i j where ij: "x = p^i" "x^n = p^j"by blast
lp15@55215
   349
    from Suc.hyps[OF n ij(2)] have ?case .}
lp15@55215
   350
  ultimately show ?case by blast
lp15@55215
   351
qed
lp15@55215
   352
lp15@55215
   353
lemma divides_primepow:
lp15@55215
   354
  fixes p::nat
lp15@59669
   355
  assumes p: "prime p"
lp15@55215
   356
  shows "d dvd p^k \<longleftrightarrow> (\<exists> i. i \<le> k \<and> d = p ^i)"
lp15@55215
   357
proof
lp15@59669
   358
  assume H: "d dvd p^k" then obtain e where e: "d*e = p^k"
haftmann@57512
   359
    unfolding dvd_def  apply (auto simp add: mult.commute) by blast
lp15@55215
   360
  from prime_power_mult[OF p e] obtain i j where ij: "d = p^i" "e=p^j" by blast
lp15@55215
   361
  from e ij have "p^(i + j) = p^k" by (simp add: power_add)
lp15@59669
   362
  hence "i + j = k" using p prime_gt_1_nat power_inject_exp[of p "i+j" k] by simp
lp15@55215
   363
  hence "i \<le> k" by arith
lp15@55215
   364
  with ij(1) show "\<exists>i\<le>k. d = p ^ i" by blast
lp15@55215
   365
next
lp15@55215
   366
  {fix i assume H: "i \<le> k" "d = p^i"
lp15@55215
   367
    then obtain j where j: "k = i + j"
lp15@55215
   368
      by (metis le_add_diff_inverse)
lp15@55215
   369
    hence "p^k = p^j*d" using H(2) by (simp add: power_add)
lp15@55215
   370
    hence "d dvd p^k" unfolding dvd_def by auto}
lp15@55215
   371
  thus "\<exists>i\<le>k. d = p ^ i \<Longrightarrow> d dvd p ^ k" by blast
lp15@55215
   372
qed
lp15@55215
   373
wenzelm@60526
   374
subsection \<open>Chinese Remainder Theorem Variants\<close>
lp15@55238
   375
lp15@55238
   376
lemma bezout_gcd_nat:
lp15@55238
   377
  fixes a::nat shows "\<exists>x y. a * x - b * y = gcd a b \<or> b * x - a * y = gcd a b"
lp15@55238
   378
  using bezout_nat[of a b]
haftmann@60688
   379
by (metis bezout_nat diff_add_inverse gcd_add_mult_nat gcd.commute
lp15@59669
   380
  gcd_nat.right_neutral mult_0)
lp15@55238
   381
lp15@55238
   382
lemma gcd_bezout_sum_nat:
lp15@59669
   383
  fixes a::nat
lp15@59669
   384
  assumes "a * x + b * y = d"
lp15@55238
   385
  shows "gcd a b dvd d"
lp15@55238
   386
proof-
lp15@55238
   387
  let ?g = "gcd a b"
lp15@59669
   388
    have dv: "?g dvd a*x" "?g dvd b * y"
lp15@55238
   389
      by simp_all
lp15@55238
   390
    from dvd_add[OF dv] assms
lp15@55238
   391
    show ?thesis by auto
lp15@55238
   392
qed
lp15@55238
   393
lp15@55238
   394
wenzelm@60526
   395
text \<open>A binary form of the Chinese Remainder Theorem.\<close>
lp15@55238
   396
lp15@59669
   397
lemma chinese_remainder:
lp15@55238
   398
  fixes a::nat  assumes ab: "coprime a b" and a: "a \<noteq> 0" and b: "b \<noteq> 0"
lp15@55238
   399
  shows "\<exists>x q1 q2. x = u + q1 * a \<and> x = v + q2 * b"
lp15@55238
   400
proof-
lp15@55238
   401
  from bezout_add_strong_nat[OF a, of b] bezout_add_strong_nat[OF b, of a]
lp15@59669
   402
  obtain d1 x1 y1 d2 x2 y2 where dxy1: "d1 dvd a" "d1 dvd b" "a * x1 = b * y1 + d1"
lp15@55238
   403
    and dxy2: "d2 dvd b" "d2 dvd a" "b * x2 = a * y2 + d2" by blast
lp15@55238
   404
  then have d12: "d1 = 1" "d2 =1"
lp15@55238
   405
    by (metis ab coprime_nat)+
lp15@55238
   406
  let ?x = "v * a * x1 + u * b * x2"
lp15@55238
   407
  let ?q1 = "v * x1 + u * y2"
lp15@55238
   408
  let ?q2 = "v * y1 + u * x2"
lp15@59669
   409
  from dxy2(3)[simplified d12] dxy1(3)[simplified d12]
lp15@55238
   410
  have "?x = u + ?q1 * a" "?x = v + ?q2 * b"
lp15@55337
   411
    by algebra+
lp15@55238
   412
  thus ?thesis by blast
lp15@55238
   413
qed
lp15@55238
   414
wenzelm@60526
   415
text \<open>Primality\<close>
lp15@55238
   416
lp15@55238
   417
lemma coprime_bezout_strong:
lp15@55238
   418
  fixes a::nat assumes "coprime a b"  "b \<noteq> 1"
lp15@55238
   419
  shows "\<exists>x y. a * x = b * y + 1"
lp15@55238
   420
by (metis assms bezout_nat gcd_nat.left_neutral)
lp15@55238
   421
lp15@59669
   422
lemma bezout_prime:
lp15@55238
   423
  assumes p: "prime p" and pa: "\<not> p dvd a"
lp15@55238
   424
  shows "\<exists>x y. a*x = Suc (p*y)"
haftmann@62349
   425
proof -
lp15@55238
   426
  have ap: "coprime a p"
haftmann@60688
   427
    by (metis gcd.commute p pa prime_imp_coprime_nat)
haftmann@62349
   428
  moreover from p have "p \<noteq> 1" by auto
haftmann@62349
   429
  ultimately have "\<exists>x y. a * x = p * y + 1"
haftmann@62349
   430
    by (rule coprime_bezout_strong)
haftmann@62349
   431
  then show ?thesis by simp    
lp15@55238
   432
qed
lp15@55238
   433
wenzelm@21256
   434
end