src/HOL/Number_Theory/Primes.thy
author Manuel Eberl <eberlm@in.tum.de>
Thu Sep 01 11:53:07 2016 +0200 (2016-09-01)
changeset 63766 695d60817cb1
parent 63635 858a225ebb62
child 63830 2ea3725a34bd
permissions -rw-r--r--
Some facts about factorial and binomial coefficients
haftmann@32479
     1
(*  Authors:    Christophe Tabacznyj, Lawrence C. Paulson, Amine Chaieb,
eberlm@63534
     2
                Thomas M. Rasmussen, Jeremy Avigad, Tobias Nipkow, 
eberlm@63534
     3
                Manuel Eberl
huffman@31706
     4
huffman@31706
     5
haftmann@32479
     6
This file deals with properties of primes. Definitions and lemmas are
haftmann@32479
     7
proved uniformly for the natural numbers and integers.
huffman@31706
     8
huffman@31706
     9
This file combines and revises a number of prior developments.
huffman@31706
    10
huffman@31706
    11
The original theories "GCD" and "Primes" were by Christophe Tabacznyj
wenzelm@58623
    12
and Lawrence C. Paulson, based on @{cite davenport92}. They introduced
huffman@31706
    13
gcd, lcm, and prime for the natural numbers.
huffman@31706
    14
huffman@31706
    15
The original theory "IntPrimes" was by Thomas M. Rasmussen, and
huffman@31706
    16
extended gcd, lcm, primes to the integers. Amine Chaieb provided
huffman@31706
    17
another extension of the notions to the integers, and added a number
huffman@31706
    18
of results to "Primes" and "GCD". IntPrimes also defined and developed
huffman@31706
    19
the congruence relations on the integers. The notion was extended to
webertj@33718
    20
the natural numbers by Chaieb.
huffman@31706
    21
avigad@32036
    22
Jeremy Avigad combined all of these, made everything uniform for the
avigad@32036
    23
natural numbers and the integers, and added a number of new theorems.
avigad@32036
    24
nipkow@31798
    25
Tobias Nipkow cleaned up a lot.
eberlm@63534
    26
eberlm@63534
    27
Florian Haftmann and Manuel Eberl put primality and prime factorisation
eberlm@63534
    28
onto an algebraic foundation and thus generalised these concepts to 
eberlm@63534
    29
other rings, such as polynomials. (see also the Factorial_Ring theory).
eberlm@63534
    30
eberlm@63534
    31
There were also previous formalisations of unique factorisation by 
eberlm@63534
    32
Thomas Marthedal Rasmussen, Jeremy Avigad, and David Gray.
wenzelm@21256
    33
*)
wenzelm@21256
    34
huffman@31706
    35
wenzelm@60526
    36
section \<open>Primes\<close>
wenzelm@21256
    37
haftmann@32479
    38
theory Primes
eberlm@63534
    39
imports "~~/src/HOL/Binomial" Euclidean_Algorithm
huffman@31706
    40
begin
huffman@31706
    41
eberlm@63534
    42
(* As a simp or intro rule,
eberlm@63534
    43
eberlm@63534
    44
     prime p \<Longrightarrow> p > 0
eberlm@63534
    45
eberlm@63534
    46
   wreaks havoc here. When the premise includes \<forall>x \<in># M. prime x, it
eberlm@63534
    47
   leads to the backchaining
eberlm@63534
    48
eberlm@63534
    49
     x > 0
eberlm@63534
    50
     prime x
eberlm@63534
    51
     x \<in># M   which is, unfortunately,
eberlm@63534
    52
     count M x > 0
eberlm@63534
    53
*)
eberlm@63534
    54
lp15@55242
    55
declare [[coercion int]]
lp15@55242
    56
declare [[coercion_enabled]]
huffman@31706
    57
eberlm@63633
    58
lemma prime_elem_nat_iff:
eberlm@63633
    59
  "prime_elem (n :: nat) \<longleftrightarrow> (1 < n \<and> (\<forall>m. m dvd n \<longrightarrow> m = 1 \<or> m = n))"
eberlm@63534
    60
proof safe
eberlm@63633
    61
  assume *: "prime_elem n"
eberlm@63534
    62
  from * have "n \<noteq> 0" "n \<noteq> 1" by (intro notI, simp del: One_nat_def)+
eberlm@63534
    63
  thus "n > 1" by (cases n) simp_all
eberlm@63534
    64
  fix m assume m: "m dvd n" "m \<noteq> n"
eberlm@63534
    65
  from * \<open>m dvd n\<close> have "n dvd m \<or> is_unit m"
eberlm@63633
    66
    by (intro irreducibleD' prime_elem_imp_irreducible)
eberlm@63534
    67
  with m show "m = 1" by (auto dest: dvd_antisym)
eberlm@63534
    68
next
eberlm@63534
    69
  assume "n > 1" "\<forall>m. m dvd n \<longrightarrow> m = 1 \<or> m = n"
eberlm@63633
    70
  thus "prime_elem n"
eberlm@63633
    71
    by (auto simp: prime_elem_iff_irreducible irreducible_altdef)
eberlm@63534
    72
qed
eberlm@63534
    73
eberlm@63633
    74
lemma prime_nat_iff_prime_elem: "prime (n :: nat) \<longleftrightarrow> prime_elem n"
eberlm@63633
    75
  by (simp add: prime_def)
huffman@31706
    76
eberlm@63633
    77
lemma prime_nat_iff:
eberlm@63633
    78
  "prime (n :: nat) \<longleftrightarrow> (1 < n \<and> (\<forall>m. m dvd n \<longrightarrow> m = 1 \<or> m = n))"
eberlm@63633
    79
  by (simp add: prime_nat_iff_prime_elem prime_elem_nat_iff)
huffman@31706
    80
eberlm@63633
    81
lemma prime_elem_int_nat_transfer: "prime_elem (n::int) \<longleftrightarrow> prime_elem (nat (abs n))"
eberlm@63534
    82
proof
eberlm@63633
    83
  assume "prime_elem n"
eberlm@63633
    84
  thus "prime_elem (nat (abs n))" by (auto simp: prime_elem_def nat_dvd_iff)
eberlm@63534
    85
next
eberlm@63633
    86
  assume "prime_elem (nat (abs n))"
eberlm@63633
    87
  thus "prime_elem n"
eberlm@63633
    88
    by (auto simp: dvd_int_unfold_dvd_nat prime_elem_def abs_mult nat_mult_distrib)
eberlm@63534
    89
qed
eberlm@63534
    90
eberlm@63633
    91
lemma prime_elem_nat_int_transfer [simp]: "prime_elem (int n) \<longleftrightarrow> prime_elem n"
eberlm@63633
    92
  by (auto simp: prime_elem_int_nat_transfer)
eberlm@63534
    93
eberlm@63633
    94
lemma prime_nat_int_transfer [simp]: "prime (int n) \<longleftrightarrow> prime n"
eberlm@63633
    95
  by (auto simp: prime_elem_int_nat_transfer prime_def)
eberlm@63534
    96
eberlm@63633
    97
lemma prime_int_nat_transfer: "prime (n::int) \<longleftrightarrow> n \<ge> 0 \<and> prime (nat n)"
eberlm@63633
    98
  by (auto simp: prime_elem_int_nat_transfer prime_def)
huffman@31706
    99
eberlm@63633
   100
lemma prime_int_iff:
eberlm@63633
   101
  "prime (n::int) \<longleftrightarrow> (1 < n \<and> (\<forall>m. m \<ge> 0 \<and> m dvd n \<longrightarrow> m = 1 \<or> m = n))"
eberlm@63534
   102
proof (intro iffI conjI allI impI; (elim conjE)?)
eberlm@63633
   103
  assume *: "prime n"
eberlm@63633
   104
  hence irred: "irreducible n" by (simp add: prime_elem_imp_irreducible)
eberlm@63534
   105
  from * have "n \<ge> 0" "n \<noteq> 0" "n \<noteq> 1" 
eberlm@63633
   106
    by (auto simp: prime_def zabs_def not_less split: if_splits)
eberlm@63534
   107
  thus "n > 1" by presburger
eberlm@63534
   108
  fix m assume "m dvd n" \<open>m \<ge> 0\<close>
eberlm@63534
   109
  with irred have "m dvd 1 \<or> n dvd m" by (auto simp: irreducible_altdef)
eberlm@63534
   110
  with \<open>m dvd n\<close> \<open>m \<ge> 0\<close> \<open>n > 1\<close> show "m = 1 \<or> m = n"
eberlm@63534
   111
    using associated_iff_dvd[of m n] by auto
eberlm@63534
   112
next
eberlm@63534
   113
  assume n: "1 < n" "\<forall>m. m \<ge> 0 \<and> m dvd n \<longrightarrow> m = 1 \<or> m = n"
eberlm@63534
   114
  hence "nat n > 1" by simp
eberlm@63534
   115
  moreover have "\<forall>m. m dvd nat n \<longrightarrow> m = 1 \<or> m = nat n"
eberlm@63534
   116
  proof (intro allI impI)
eberlm@63534
   117
    fix m assume "m dvd nat n"
eberlm@63534
   118
    with \<open>n > 1\<close> have "int m dvd n" by (auto simp: int_dvd_iff)
eberlm@63534
   119
    with n(2) have "int m = 1 \<or> int m = n" by auto
eberlm@63534
   120
    thus "m = 1 \<or> m = nat n" by auto
eberlm@63534
   121
  qed
eberlm@63633
   122
  ultimately show "prime n" 
eberlm@63633
   123
    unfolding prime_int_nat_transfer prime_nat_iff by auto
eberlm@63534
   124
qed
chaieb@22027
   125
eberlm@63534
   126
eberlm@63534
   127
lemma prime_nat_not_dvd:
eberlm@63534
   128
  assumes "prime p" "p > n" "n \<noteq> (1::nat)"
eberlm@63534
   129
  shows   "\<not>n dvd p"
eberlm@63534
   130
proof
eberlm@63534
   131
  assume "n dvd p"
eberlm@63633
   132
  from assms(1) have "irreducible p" by (simp add: prime_elem_imp_irreducible)
eberlm@63534
   133
  from irreducibleD'[OF this \<open>n dvd p\<close>] \<open>n dvd p\<close> \<open>p > n\<close> assms show False
eberlm@63534
   134
    by (cases "n = 0") (auto dest!: dvd_imp_le)
eberlm@63534
   135
qed
chaieb@22027
   136
eberlm@63534
   137
lemma prime_int_not_dvd:
eberlm@63534
   138
  assumes "prime p" "p > n" "n > (1::int)"
eberlm@63534
   139
  shows   "\<not>n dvd p"
eberlm@63534
   140
proof
eberlm@63534
   141
  assume "n dvd p"
eberlm@63633
   142
  from assms(1) have "irreducible p" by (simp add: prime_elem_imp_irreducible)
eberlm@63534
   143
  from irreducibleD'[OF this \<open>n dvd p\<close>] \<open>n dvd p\<close> \<open>p > n\<close> assms show False
eberlm@63534
   144
    by (auto dest!: zdvd_imp_le)
eberlm@63534
   145
qed
eberlm@63534
   146
eberlm@63534
   147
lemma prime_odd_nat: "prime p \<Longrightarrow> p > (2::nat) \<Longrightarrow> odd p"
eberlm@63534
   148
  by (intro prime_nat_not_dvd) auto
eberlm@63534
   149
eberlm@63534
   150
lemma prime_odd_int: "prime p \<Longrightarrow> p > (2::int) \<Longrightarrow> odd p"
eberlm@63534
   151
  by (intro prime_int_not_dvd) auto
wenzelm@22367
   152
eberlm@63534
   153
lemma prime_ge_0_int: "prime p \<Longrightarrow> p \<ge> (0::int)"
eberlm@63633
   154
  unfolding prime_int_iff by auto
eberlm@63534
   155
eberlm@63534
   156
lemma prime_gt_0_nat: "prime p \<Longrightarrow> p > (0::nat)"
eberlm@63633
   157
  unfolding prime_nat_iff by auto
eberlm@63534
   158
eberlm@63534
   159
lemma prime_gt_0_int: "prime p \<Longrightarrow> p > (0::int)"
eberlm@63633
   160
  unfolding prime_int_iff by auto
eberlm@63534
   161
eberlm@63534
   162
lemma prime_ge_1_nat: "prime p \<Longrightarrow> p \<ge> (1::nat)"
eberlm@63633
   163
  unfolding prime_nat_iff by auto
eberlm@63534
   164
eberlm@63534
   165
lemma prime_ge_Suc_0_nat: "prime p \<Longrightarrow> p \<ge> Suc 0"
eberlm@63633
   166
  unfolding prime_nat_iff by auto
eberlm@63534
   167
eberlm@63534
   168
lemma prime_ge_1_int: "prime p \<Longrightarrow> p \<ge> (1::int)"
eberlm@63633
   169
  unfolding prime_int_iff by auto
eberlm@63534
   170
eberlm@63534
   171
lemma prime_gt_1_nat: "prime p \<Longrightarrow> p > (1::nat)"
eberlm@63633
   172
  unfolding prime_nat_iff by auto
huffman@31706
   173
lp15@61762
   174
lemma prime_gt_Suc_0_nat: "prime p \<Longrightarrow> p > Suc 0"
eberlm@63633
   175
  unfolding prime_nat_iff by auto
huffman@31706
   176
eberlm@63534
   177
lemma prime_gt_1_int: "prime p \<Longrightarrow> p > (1::int)"
eberlm@63633
   178
  unfolding prime_int_iff by auto
huffman@31706
   179
eberlm@63534
   180
lemma prime_ge_2_nat: "prime p \<Longrightarrow> p \<ge> (2::nat)"
eberlm@63633
   181
  unfolding prime_nat_iff by auto
eberlm@63534
   182
eberlm@63534
   183
lemma prime_ge_2_int: "prime p \<Longrightarrow> p \<ge> (2::int)"
eberlm@63633
   184
  unfolding prime_int_iff by auto
huffman@31706
   185
lp15@59669
   186
lemma prime_int_altdef:
lp15@55242
   187
  "prime p = (1 < p \<and> (\<forall>m::int. m \<ge> 0 \<longrightarrow> m dvd p \<longrightarrow>
lp15@55242
   188
    m = 1 \<or> m = p))"
eberlm@63633
   189
  unfolding prime_int_iff by blast
chaieb@27568
   190
haftmann@62481
   191
lemma not_prime_eq_prod_nat:
eberlm@63534
   192
  assumes "m > 1" "\<not>prime (m::nat)"
eberlm@63534
   193
  shows   "\<exists>n k. n = m * k \<and> 1 < m \<and> m < n \<and> 1 < k \<and> k < n"
eberlm@63534
   194
  using assms irreducible_altdef[of m]
eberlm@63633
   195
  by (auto simp: prime_elem_iff_irreducible prime_def irreducible_altdef)
huffman@53598
   196
huffman@53598
   197
wenzelm@60526
   198
subsubsection \<open>Make prime naively executable\<close>
nipkow@32007
   199
eberlm@63534
   200
lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)"
eberlm@63633
   201
  unfolding One_nat_def [symmetric] by (rule not_prime_1)
nipkow@32007
   202
eberlm@63633
   203
lemma prime_nat_iff':
eberlm@63535
   204
  "prime (p :: nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)"
eberlm@63534
   205
proof safe
eberlm@63534
   206
  assume "p > 1" and *: "\<forall>n\<in>{1<..<p}. \<not>n dvd p"
eberlm@63633
   207
  show "prime p" unfolding prime_nat_iff
eberlm@63534
   208
  proof (intro conjI allI impI)
eberlm@63534
   209
    fix m assume "m dvd p"
eberlm@63534
   210
    with \<open>p > 1\<close> have "m \<noteq> 0" by (intro notI) auto
eberlm@63534
   211
    hence "m \<ge> 1" by simp
eberlm@63534
   212
    moreover from \<open>m dvd p\<close> and * have "m \<notin> {1<..<p}" by blast
eberlm@63534
   213
    with \<open>m dvd p\<close> and \<open>p > 1\<close> have "m \<le> 1 \<or> m = p" by (auto dest: dvd_imp_le)
eberlm@63534
   214
    ultimately show "m = 1 \<or> m = p" by simp
eberlm@63534
   215
  qed fact+
eberlm@63633
   216
qed (auto simp: prime_nat_iff)
nipkow@32007
   217
eberlm@63535
   218
lemma prime_nat_code [code_unfold]:
eberlm@63535
   219
  "(prime :: nat \<Rightarrow> bool) = (\<lambda>p. p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p))"
eberlm@63633
   220
  by (rule ext, rule prime_nat_iff')
eberlm@63535
   221
eberlm@63633
   222
lemma prime_int_iff':
eberlm@63535
   223
  "prime (p :: int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)" (is "?lhs = ?rhs")
eberlm@63534
   224
proof
eberlm@63534
   225
  assume "?lhs"
eberlm@63633
   226
  thus "?rhs" by (auto simp: prime_int_nat_transfer dvd_int_unfold_dvd_nat prime_nat_code)
eberlm@63534
   227
next
eberlm@63534
   228
  assume "?rhs"
eberlm@63633
   229
  thus "?lhs" by (auto simp: prime_int_nat_transfer zdvd_int prime_nat_code)
eberlm@63534
   230
qed
nipkow@32007
   231
eberlm@63535
   232
lemma prime_int_code [code_unfold]:
eberlm@63535
   233
  "(prime :: int \<Rightarrow> bool) = (\<lambda>p. p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p))" 
eberlm@63633
   234
  by (rule ext, rule prime_int_iff')
eberlm@63535
   235
nipkow@32007
   236
lemma prime_nat_simp:
lp15@55242
   237
    "prime p \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..<p]. \<not> n dvd p)"
wenzelm@44872
   238
  by (auto simp add: prime_nat_code)
nipkow@32007
   239
eberlm@63534
   240
lemma prime_int_simp:
eberlm@63534
   241
    "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {2..<p}. \<not> n dvd p)"
eberlm@63534
   242
  by (auto simp add: prime_int_code)
eberlm@63534
   243
huffman@47108
   244
lemmas prime_nat_simp_numeral [simp] = prime_nat_simp [of "numeral m"] for m
nipkow@32007
   245
eberlm@63635
   246
lemma two_is_prime_nat [simp]: "prime (2::nat)"
wenzelm@44872
   247
  by simp
nipkow@32007
   248
eberlm@63633
   249
declare prime_int_nat_transfer[of "numeral m" for m, simp]
eberlm@63534
   250
eberlm@63534
   251
wenzelm@60526
   252
text\<open>A bit of regression testing:\<close>
nipkow@32111
   253
haftmann@58954
   254
lemma "prime(97::nat)" by simp
wenzelm@44872
   255
lemma "prime(997::nat)" by eval
eberlm@63534
   256
lemma "prime(97::int)" by simp
eberlm@63534
   257
lemma "prime(997::int)" by eval
huffman@31706
   258
eberlm@63534
   259
lemma prime_factor_nat: 
eberlm@63534
   260
  "n \<noteq> (1::nat) \<Longrightarrow> \<exists>p. prime p \<and> p dvd n"
eberlm@63534
   261
  using prime_divisor_exists[of n]
eberlm@63534
   262
  by (cases "n = 0") (auto intro: exI[of _ "2::nat"])
nipkow@23983
   263
wenzelm@44872
   264
wenzelm@60526
   265
subsection \<open>Infinitely many primes\<close>
avigad@32036
   266
eberlm@63534
   267
lemma next_prime_bound: "\<exists>p::nat. prime p \<and> n < p \<and> p \<le> fact n + 1"
avigad@32036
   268
proof-
lp15@59730
   269
  have f1: "fact n + 1 \<noteq> (1::nat)" using fact_ge_1 [of n, where 'a=nat] by arith
avigad@32036
   270
  from prime_factor_nat [OF f1]
eberlm@63534
   271
  obtain p :: nat where "prime p" and "p dvd fact n + 1" by auto
wenzelm@44872
   272
  then have "p \<le> fact n + 1" apply (intro dvd_imp_le) apply auto done
wenzelm@44872
   273
  { assume "p \<le> n"
wenzelm@60526
   274
    from \<open>prime p\<close> have "p \<ge> 1"
avigad@32036
   275
      by (cases p, simp_all)
wenzelm@60526
   276
    with \<open>p <= n\<close> have "p dvd fact n"
lp15@59730
   277
      by (intro dvd_fact)
wenzelm@60526
   278
    with \<open>p dvd fact n + 1\<close> have "p dvd fact n + 1 - fact n"
avigad@32036
   279
      by (rule dvd_diff_nat)
wenzelm@44872
   280
    then have "p dvd 1" by simp
wenzelm@44872
   281
    then have "p <= 1" by auto
lp15@61762
   282
    moreover from \<open>prime p\<close> have "p > 1"
eberlm@63633
   283
      using prime_nat_iff by blast
avigad@32036
   284
    ultimately have False by auto}
wenzelm@44872
   285
  then have "n < p" by presburger
wenzelm@60526
   286
  with \<open>prime p\<close> and \<open>p <= fact n + 1\<close> show ?thesis by auto
avigad@32036
   287
qed
avigad@32036
   288
lp15@59669
   289
lemma bigger_prime: "\<exists>p. prime p \<and> p > (n::nat)"
wenzelm@44872
   290
  using next_prime_bound by auto
avigad@32036
   291
avigad@32036
   292
lemma primes_infinite: "\<not> (finite {(p::nat). prime p})"
avigad@32036
   293
proof
avigad@32036
   294
  assume "finite {(p::nat). prime p}"
avigad@32036
   295
  with Max_ge have "(EX b. (ALL x : {(p::nat). prime p}. x <= b))"
avigad@32036
   296
    by auto
avigad@32036
   297
  then obtain b where "ALL (x::nat). prime x \<longrightarrow> x <= b"
avigad@32036
   298
    by auto
wenzelm@44872
   299
  with bigger_prime [of b] show False
wenzelm@44872
   300
    by auto
avigad@32036
   301
qed
avigad@32036
   302
wenzelm@60526
   303
subsection\<open>Powers of Primes\<close>
lp15@55215
   304
wenzelm@60526
   305
text\<open>Versions for type nat only\<close>
lp15@55215
   306
lp15@59669
   307
lemma prime_product:
lp15@55215
   308
  fixes p::nat
lp15@55215
   309
  assumes "prime (p * q)"
lp15@55215
   310
  shows "p = 1 \<or> q = 1"
lp15@55215
   311
proof -
lp15@59669
   312
  from assms have
lp15@55215
   313
    "1 < p * q" and P: "\<And>m. m dvd p * q \<Longrightarrow> m = 1 \<or> m = p * q"
eberlm@63633
   314
    unfolding prime_nat_iff by auto
wenzelm@60526
   315
  from \<open>1 < p * q\<close> have "p \<noteq> 0" by (cases p) auto
lp15@55215
   316
  then have Q: "p = p * q \<longleftrightarrow> q = 1" by auto
lp15@55215
   317
  have "p dvd p * q" by simp
lp15@55215
   318
  then have "p = 1 \<or> p = p * q" by (rule P)
lp15@55215
   319
  then show ?thesis by (simp add: Q)
lp15@55215
   320
qed
lp15@55215
   321
eberlm@63534
   322
(* TODO: Generalise? *)
eberlm@63534
   323
lemma prime_power_mult_nat:
lp15@55215
   324
  fixes p::nat
lp15@55215
   325
  assumes p: "prime p" and xy: "x * y = p ^ k"
lp15@55215
   326
  shows "\<exists>i j. x = p ^i \<and> y = p^ j"
lp15@55215
   327
using xy
lp15@55215
   328
proof(induct k arbitrary: x y)
lp15@55215
   329
  case 0 thus ?case apply simp by (rule exI[where x="0"], simp)
lp15@55215
   330
next
lp15@55215
   331
  case (Suc k x y)
lp15@55215
   332
  from Suc.prems have pxy: "p dvd x*y" by auto
eberlm@63633
   333
  from prime_dvd_multD [OF p pxy] have pxyc: "p dvd x \<or> p dvd y" .
lp15@59669
   334
  from p have p0: "p \<noteq> 0" by - (rule ccontr, simp)
lp15@55215
   335
  {assume px: "p dvd x"
lp15@55215
   336
    then obtain d where d: "x = p*d" unfolding dvd_def by blast
lp15@55215
   337
    from Suc.prems d  have "p*d*y = p^Suc k" by simp
lp15@55215
   338
    hence th: "d*y = p^k" using p0 by simp
lp15@55215
   339
    from Suc.hyps[OF th] obtain i j where ij: "d = p^i" "y = p^j" by blast
lp15@59669
   340
    with d have "x = p^Suc i" by simp
lp15@55215
   341
    with ij(2) have ?case by blast}
lp15@59669
   342
  moreover
lp15@55215
   343
  {assume px: "p dvd y"
lp15@55215
   344
    then obtain d where d: "y = p*d" unfolding dvd_def by blast
haftmann@57512
   345
    from Suc.prems d  have "p*d*x = p^Suc k" by (simp add: mult.commute)
lp15@55215
   346
    hence th: "d*x = p^k" using p0 by simp
lp15@55215
   347
    from Suc.hyps[OF th] obtain i j where ij: "d = p^i" "x = p^j" by blast
lp15@59669
   348
    with d have "y = p^Suc i" by simp
lp15@55215
   349
    with ij(2) have ?case by blast}
lp15@55215
   350
  ultimately show ?case  using pxyc by blast
lp15@55215
   351
qed
lp15@55215
   352
eberlm@63534
   353
lemma prime_power_exp_nat:
lp15@55215
   354
  fixes p::nat
lp15@59669
   355
  assumes p: "prime p" and n: "n \<noteq> 0"
lp15@55215
   356
    and xn: "x^n = p^k" shows "\<exists>i. x = p^i"
lp15@55215
   357
  using n xn
lp15@55215
   358
proof(induct n arbitrary: k)
lp15@55215
   359
  case 0 thus ?case by simp
lp15@55215
   360
next
lp15@55215
   361
  case (Suc n k) hence th: "x*x^n = p^k" by simp
lp15@55215
   362
  {assume "n = 0" with Suc have ?case by simp (rule exI[where x="k"], simp)}
lp15@55215
   363
  moreover
lp15@55215
   364
  {assume n: "n \<noteq> 0"
eberlm@63534
   365
    from prime_power_mult_nat[OF p th]
lp15@55215
   366
    obtain i j where ij: "x = p^i" "x^n = p^j"by blast
lp15@55215
   367
    from Suc.hyps[OF n ij(2)] have ?case .}
lp15@55215
   368
  ultimately show ?case by blast
lp15@55215
   369
qed
lp15@55215
   370
eberlm@63534
   371
lemma divides_primepow_nat:
lp15@55215
   372
  fixes p::nat
lp15@59669
   373
  assumes p: "prime p"
lp15@55215
   374
  shows "d dvd p^k \<longleftrightarrow> (\<exists> i. i \<le> k \<and> d = p ^i)"
lp15@55215
   375
proof
lp15@59669
   376
  assume H: "d dvd p^k" then obtain e where e: "d*e = p^k"
haftmann@57512
   377
    unfolding dvd_def  apply (auto simp add: mult.commute) by blast
eberlm@63534
   378
  from prime_power_mult_nat[OF p e] obtain i j where ij: "d = p^i" "e=p^j" by blast
lp15@55215
   379
  from e ij have "p^(i + j) = p^k" by (simp add: power_add)
lp15@59669
   380
  hence "i + j = k" using p prime_gt_1_nat power_inject_exp[of p "i+j" k] by simp
lp15@55215
   381
  hence "i \<le> k" by arith
lp15@55215
   382
  with ij(1) show "\<exists>i\<le>k. d = p ^ i" by blast
lp15@55215
   383
next
lp15@55215
   384
  {fix i assume H: "i \<le> k" "d = p^i"
lp15@55215
   385
    then obtain j where j: "k = i + j"
lp15@55215
   386
      by (metis le_add_diff_inverse)
lp15@55215
   387
    hence "p^k = p^j*d" using H(2) by (simp add: power_add)
lp15@55215
   388
    hence "d dvd p^k" unfolding dvd_def by auto}
lp15@55215
   389
  thus "\<exists>i\<le>k. d = p ^ i \<Longrightarrow> d dvd p ^ k" by blast
lp15@55215
   390
qed
lp15@55215
   391
eberlm@63534
   392
wenzelm@60526
   393
subsection \<open>Chinese Remainder Theorem Variants\<close>
lp15@55238
   394
lp15@55238
   395
lemma bezout_gcd_nat:
lp15@55238
   396
  fixes a::nat shows "\<exists>x y. a * x - b * y = gcd a b \<or> b * x - a * y = gcd a b"
lp15@55238
   397
  using bezout_nat[of a b]
eberlm@62429
   398
by (metis bezout_nat diff_add_inverse gcd_add_mult gcd.commute
lp15@59669
   399
  gcd_nat.right_neutral mult_0)
lp15@55238
   400
lp15@55238
   401
lemma gcd_bezout_sum_nat:
lp15@59669
   402
  fixes a::nat
lp15@59669
   403
  assumes "a * x + b * y = d"
lp15@55238
   404
  shows "gcd a b dvd d"
lp15@55238
   405
proof-
lp15@55238
   406
  let ?g = "gcd a b"
lp15@59669
   407
    have dv: "?g dvd a*x" "?g dvd b * y"
lp15@55238
   408
      by simp_all
lp15@55238
   409
    from dvd_add[OF dv] assms
lp15@55238
   410
    show ?thesis by auto
lp15@55238
   411
qed
lp15@55238
   412
lp15@55238
   413
wenzelm@60526
   414
text \<open>A binary form of the Chinese Remainder Theorem.\<close>
lp15@55238
   415
eberlm@63534
   416
(* TODO: Generalise? *)
lp15@59669
   417
lemma chinese_remainder:
lp15@55238
   418
  fixes a::nat  assumes ab: "coprime a b" and a: "a \<noteq> 0" and b: "b \<noteq> 0"
lp15@55238
   419
  shows "\<exists>x q1 q2. x = u + q1 * a \<and> x = v + q2 * b"
lp15@55238
   420
proof-
lp15@55238
   421
  from bezout_add_strong_nat[OF a, of b] bezout_add_strong_nat[OF b, of a]
lp15@59669
   422
  obtain d1 x1 y1 d2 x2 y2 where dxy1: "d1 dvd a" "d1 dvd b" "a * x1 = b * y1 + d1"
lp15@55238
   423
    and dxy2: "d2 dvd b" "d2 dvd a" "b * x2 = a * y2 + d2" by blast
lp15@55238
   424
  then have d12: "d1 = 1" "d2 =1"
lp15@55238
   425
    by (metis ab coprime_nat)+
lp15@55238
   426
  let ?x = "v * a * x1 + u * b * x2"
lp15@55238
   427
  let ?q1 = "v * x1 + u * y2"
lp15@55238
   428
  let ?q2 = "v * y1 + u * x2"
lp15@59669
   429
  from dxy2(3)[simplified d12] dxy1(3)[simplified d12]
lp15@55238
   430
  have "?x = u + ?q1 * a" "?x = v + ?q2 * b"
lp15@55337
   431
    by algebra+
lp15@55238
   432
  thus ?thesis by blast
lp15@55238
   433
qed
lp15@55238
   434
wenzelm@60526
   435
text \<open>Primality\<close>
lp15@55238
   436
lp15@55238
   437
lemma coprime_bezout_strong:
lp15@55238
   438
  fixes a::nat assumes "coprime a b"  "b \<noteq> 1"
lp15@55238
   439
  shows "\<exists>x y. a * x = b * y + 1"
lp15@55238
   440
by (metis assms bezout_nat gcd_nat.left_neutral)
lp15@55238
   441
lp15@59669
   442
lemma bezout_prime:
lp15@55238
   443
  assumes p: "prime p" and pa: "\<not> p dvd a"
lp15@55238
   444
  shows "\<exists>x y. a*x = Suc (p*y)"
haftmann@62349
   445
proof -
lp15@55238
   446
  have ap: "coprime a p"
eberlm@63633
   447
    by (metis gcd.commute p pa prime_imp_coprime)
haftmann@62349
   448
  moreover from p have "p \<noteq> 1" by auto
haftmann@62349
   449
  ultimately have "\<exists>x y. a * x = p * y + 1"
haftmann@62349
   450
    by (rule coprime_bezout_strong)
haftmann@62349
   451
  then show ?thesis by simp    
lp15@55238
   452
qed
eberlm@63534
   453
(* END TODO *)
lp15@55238
   454
eberlm@63534
   455
eberlm@63534
   456
eberlm@63534
   457
subsection \<open>Multiplicity and primality for natural numbers and integers\<close>
eberlm@63534
   458
eberlm@63534
   459
lemma prime_factors_gt_0_nat:
eberlm@63534
   460
  "p \<in> prime_factors x \<Longrightarrow> p > (0::nat)"
eberlm@63534
   461
  by (simp add: prime_factors_prime prime_gt_0_nat)
eberlm@63534
   462
eberlm@63534
   463
lemma prime_factors_gt_0_int:
eberlm@63534
   464
  "p \<in> prime_factors x \<Longrightarrow> p > (0::int)"
eberlm@63534
   465
  by (simp add: prime_factors_prime prime_gt_0_int)
eberlm@63534
   466
eberlm@63534
   467
lemma prime_factors_ge_0_int [elim]:
eberlm@63534
   468
  fixes n :: int
eberlm@63534
   469
  shows "p \<in> prime_factors n \<Longrightarrow> p \<ge> 0"
eberlm@63534
   470
  unfolding prime_factors_def 
eberlm@63633
   471
  by (auto split: if_splits simp: prime_def dest!: in_prime_factorization_imp_prime)
eberlm@63534
   472
eberlm@63534
   473
lemma msetprod_prime_factorization_int:
eberlm@63534
   474
  fixes n :: int
eberlm@63534
   475
  assumes "n > 0"
eberlm@63534
   476
  shows   "msetprod (prime_factorization n) = n"
eberlm@63534
   477
  using assms by (simp add: msetprod_prime_factorization)
eberlm@63534
   478
eberlm@63534
   479
lemma prime_factorization_exists_nat:
eberlm@63534
   480
  "n > 0 \<Longrightarrow> (\<exists>M. (\<forall>p::nat \<in> set_mset M. prime p) \<and> n = (\<Prod>i \<in># M. i))"
eberlm@63633
   481
  using prime_factorization_exists[of n] by (auto simp: prime_def)
eberlm@63534
   482
eberlm@63534
   483
lemma msetprod_prime_factorization_nat [simp]: 
eberlm@63534
   484
  "(n::nat) > 0 \<Longrightarrow> msetprod (prime_factorization n) = n"
eberlm@63534
   485
  by (subst msetprod_prime_factorization) simp_all
eberlm@63534
   486
eberlm@63534
   487
lemma prime_factorization_nat:
eberlm@63534
   488
    "n > (0::nat) \<Longrightarrow> n = (\<Prod>p \<in> prime_factors n. p ^ multiplicity p n)"
eberlm@63534
   489
  by (simp add: setprod_prime_factors)
eberlm@63534
   490
eberlm@63534
   491
lemma prime_factorization_int:
eberlm@63534
   492
    "n > (0::int) \<Longrightarrow> n = (\<Prod>p \<in> prime_factors n. p ^ multiplicity p n)"
eberlm@63534
   493
  by (simp add: setprod_prime_factors)
eberlm@63534
   494
eberlm@63534
   495
lemma prime_factorization_unique_nat:
eberlm@63534
   496
  fixes f :: "nat \<Rightarrow> _"
eberlm@63534
   497
  assumes S_eq: "S = {p. 0 < f p}"
eberlm@63534
   498
    and "finite S"
eberlm@63534
   499
    and S: "\<forall>p\<in>S. prime p" "n = (\<Prod>p\<in>S. p ^ f p)"
eberlm@63633
   500
  shows "S = prime_factors n \<and> (\<forall>p. prime p \<longrightarrow> f p = multiplicity p n)"
eberlm@63534
   501
  using assms by (intro prime_factorization_unique'') auto
eberlm@63534
   502
eberlm@63534
   503
lemma prime_factorization_unique_int:
eberlm@63534
   504
  fixes f :: "int \<Rightarrow> _"
eberlm@63534
   505
  assumes S_eq: "S = {p. 0 < f p}"
eberlm@63534
   506
    and "finite S"
eberlm@63534
   507
    and S: "\<forall>p\<in>S. prime p" "abs n = (\<Prod>p\<in>S. p ^ f p)"
eberlm@63633
   508
  shows "S = prime_factors n \<and> (\<forall>p. prime p \<longrightarrow> f p = multiplicity p n)"
eberlm@63534
   509
  using assms by (intro prime_factorization_unique'') auto
eberlm@63534
   510
eberlm@63534
   511
lemma prime_factors_characterization_nat:
eberlm@63534
   512
  "S = {p. 0 < f (p::nat)} \<Longrightarrow>
eberlm@63534
   513
    finite S \<Longrightarrow> \<forall>p\<in>S. prime p \<Longrightarrow> n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> prime_factors n = S"
eberlm@63534
   514
  by (rule prime_factorization_unique_nat [THEN conjunct1, symmetric])
eberlm@63534
   515
eberlm@63534
   516
lemma prime_factors_characterization'_nat:
eberlm@63534
   517
  "finite {p. 0 < f (p::nat)} \<Longrightarrow>
eberlm@63534
   518
    (\<forall>p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow>
eberlm@63534
   519
      prime_factors (\<Prod>p | 0 < f p. p ^ f p) = {p. 0 < f p}"
eberlm@63534
   520
  by (rule prime_factors_characterization_nat) auto
eberlm@63534
   521
eberlm@63534
   522
lemma prime_factors_characterization_int:
eberlm@63534
   523
  "S = {p. 0 < f (p::int)} \<Longrightarrow> finite S \<Longrightarrow>
eberlm@63534
   524
    \<forall>p\<in>S. prime p \<Longrightarrow> abs n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> prime_factors n = S"
eberlm@63534
   525
  by (rule prime_factorization_unique_int [THEN conjunct1, symmetric])
eberlm@63534
   526
eberlm@63534
   527
(* TODO Move *)
eberlm@63534
   528
lemma abs_setprod: "abs (setprod f A :: 'a :: linordered_idom) = setprod (\<lambda>x. abs (f x)) A"
eberlm@63534
   529
  by (cases "finite A", induction A rule: finite_induct) (simp_all add: abs_mult)
eberlm@63534
   530
eberlm@63534
   531
lemma primes_characterization'_int [rule_format]:
eberlm@63534
   532
  "finite {p. p \<ge> 0 \<and> 0 < f (p::int)} \<Longrightarrow> \<forall>p. 0 < f p \<longrightarrow> prime p \<Longrightarrow>
eberlm@63534
   533
      prime_factors (\<Prod>p | p \<ge> 0 \<and> 0 < f p. p ^ f p) = {p. p \<ge> 0 \<and> 0 < f p}"
eberlm@63534
   534
  by (rule prime_factors_characterization_int) (auto simp: abs_setprod prime_ge_0_int)
eberlm@63534
   535
eberlm@63534
   536
lemma multiplicity_characterization_nat:
eberlm@63633
   537
  "S = {p. 0 < f (p::nat)} \<Longrightarrow> finite S \<Longrightarrow> \<forall>p\<in>S. prime p \<Longrightarrow> prime p \<Longrightarrow>
eberlm@63534
   538
    n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> multiplicity p n = f p"
eberlm@63534
   539
  by (frule prime_factorization_unique_nat [of S f n, THEN conjunct2, rule_format, symmetric]) auto
eberlm@63534
   540
eberlm@63534
   541
lemma multiplicity_characterization'_nat: "finite {p. 0 < f (p::nat)} \<longrightarrow>
eberlm@63633
   542
    (\<forall>p. 0 < f p \<longrightarrow> prime p) \<longrightarrow> prime p \<longrightarrow>
eberlm@63534
   543
      multiplicity p (\<Prod>p | 0 < f p. p ^ f p) = f p"
eberlm@63534
   544
  by (intro impI, rule multiplicity_characterization_nat) auto
eberlm@63534
   545
eberlm@63534
   546
lemma multiplicity_characterization_int: "S = {p. 0 < f (p::int)} \<Longrightarrow>
eberlm@63633
   547
    finite S \<Longrightarrow> \<forall>p\<in>S. prime p \<Longrightarrow> prime p \<Longrightarrow> n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> multiplicity p n = f p"
eberlm@63534
   548
  by (frule prime_factorization_unique_int [of S f n, THEN conjunct2, rule_format, symmetric]) 
eberlm@63534
   549
     (auto simp: abs_setprod power_abs prime_ge_0_int intro!: setprod.cong)
eberlm@63534
   550
eberlm@63534
   551
lemma multiplicity_characterization'_int [rule_format]:
eberlm@63534
   552
  "finite {p. p \<ge> 0 \<and> 0 < f (p::int)} \<Longrightarrow>
eberlm@63633
   553
    (\<forall>p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow> prime p \<Longrightarrow>
eberlm@63534
   554
      multiplicity p (\<Prod>p | p \<ge> 0 \<and> 0 < f p. p ^ f p) = f p"
eberlm@63534
   555
  by (rule multiplicity_characterization_int) (auto simp: prime_ge_0_int)
eberlm@63534
   556
eberlm@63534
   557
lemma multiplicity_one_nat [simp]: "multiplicity p (Suc 0) = 0"
eberlm@63534
   558
  unfolding One_nat_def [symmetric] by (rule multiplicity_one)
eberlm@63534
   559
eberlm@63534
   560
lemma multiplicity_eq_nat:
eberlm@63534
   561
  fixes x and y::nat
eberlm@63633
   562
  assumes "x > 0" "y > 0" "\<And>p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
eberlm@63534
   563
  shows "x = y"
eberlm@63534
   564
  using multiplicity_eq_imp_eq[of x y] assms by simp
eberlm@63534
   565
eberlm@63534
   566
lemma multiplicity_eq_int:
eberlm@63534
   567
  fixes x y :: int
eberlm@63633
   568
  assumes "x > 0" "y > 0" "\<And>p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
eberlm@63534
   569
  shows "x = y"
eberlm@63534
   570
  using multiplicity_eq_imp_eq[of x y] assms by simp
eberlm@63534
   571
eberlm@63534
   572
lemma multiplicity_prod_prime_powers:
eberlm@63633
   573
  assumes "finite S" "\<And>x. x \<in> S \<Longrightarrow> prime x" "prime p"
eberlm@63534
   574
  shows   "multiplicity p (\<Prod>p \<in> S. p ^ f p) = (if p \<in> S then f p else 0)"
eberlm@63534
   575
proof -
eberlm@63534
   576
  define g where "g = (\<lambda>x. if x \<in> S then f x else 0)"
eberlm@63534
   577
  define A where "A = Abs_multiset g"
eberlm@63534
   578
  have "{x. g x > 0} \<subseteq> S" by (auto simp: g_def)
eberlm@63534
   579
  from finite_subset[OF this assms(1)] have [simp]: "g :  multiset"
eberlm@63534
   580
    by (simp add: multiset_def)
eberlm@63534
   581
  from assms have count_A: "count A x = g x" for x unfolding A_def
eberlm@63534
   582
    by simp
eberlm@63534
   583
  have set_mset_A: "set_mset A = {x\<in>S. f x > 0}"
eberlm@63534
   584
    unfolding set_mset_def count_A by (auto simp: g_def)
eberlm@63534
   585
  with assms have prime: "prime x" if "x \<in># A" for x using that by auto
eberlm@63534
   586
  from set_mset_A assms have "(\<Prod>p \<in> S. p ^ f p) = (\<Prod>p \<in> S. p ^ g p) "
eberlm@63534
   587
    by (intro setprod.cong) (auto simp: g_def)
eberlm@63534
   588
  also from set_mset_A assms have "\<dots> = (\<Prod>p \<in> set_mset A. p ^ g p)"
eberlm@63534
   589
    by (intro setprod.mono_neutral_right) (auto simp: g_def set_mset_A)
eberlm@63534
   590
  also have "\<dots> = msetprod A"
eberlm@63534
   591
    by (auto simp: msetprod_multiplicity count_A set_mset_A intro!: setprod.cong)
eberlm@63534
   592
  also from assms have "multiplicity p \<dots> = msetsum (image_mset (multiplicity p) A)"
eberlm@63633
   593
    by (subst prime_elem_multiplicity_msetprod_distrib) (auto dest: prime)
eberlm@63534
   594
  also from assms have "image_mset (multiplicity p) A = image_mset (\<lambda>x. if x = p then 1 else 0) A"
eberlm@63534
   595
    by (intro image_mset_cong) (auto simp: prime_multiplicity_other dest: prime)
eberlm@63534
   596
  also have "msetsum \<dots> = (if p \<in> S then f p else 0)" by (simp add: msetsum_delta count_A g_def)
eberlm@63534
   597
  finally show ?thesis .
eberlm@63534
   598
qed
eberlm@63534
   599
eberlm@63766
   600
lemma prime_dvd_fact_iff:
eberlm@63766
   601
  assumes "prime p"
eberlm@63766
   602
  shows   "p dvd fact n \<longleftrightarrow> p \<le> n"
eberlm@63766
   603
proof (induction n)
eberlm@63766
   604
  case 0
eberlm@63766
   605
  with assms show ?case by auto
eberlm@63766
   606
next
eberlm@63766
   607
  case (Suc n)
eberlm@63766
   608
  have "p dvd fact (Suc n) \<longleftrightarrow> p dvd (Suc n) * fact n" by simp
eberlm@63766
   609
  also from assms have "\<dots> \<longleftrightarrow> p dvd Suc n \<or> p dvd fact n"
eberlm@63766
   610
    by (rule prime_dvd_mult_iff)
eberlm@63766
   611
  also note Suc.IH
eberlm@63766
   612
  also have "p dvd Suc n \<or> p \<le> n \<longleftrightarrow> p \<le> Suc n"
eberlm@63766
   613
    by (auto dest: dvd_imp_le simp: le_Suc_eq)
eberlm@63766
   614
  finally show ?case .
eberlm@63766
   615
qed
eberlm@63766
   616
eberlm@63534
   617
(* TODO Legacy names *)
eberlm@63633
   618
lemmas prime_imp_coprime_nat = prime_imp_coprime[where ?'a = nat]
eberlm@63633
   619
lemmas prime_imp_coprime_int = prime_imp_coprime[where ?'a = int]
eberlm@63633
   620
lemmas prime_dvd_mult_nat = prime_dvd_mult_iff[where ?'a = nat]
eberlm@63633
   621
lemmas prime_dvd_mult_int = prime_dvd_mult_iff[where ?'a = int]
eberlm@63633
   622
lemmas prime_dvd_mult_eq_nat = prime_dvd_mult_iff[where ?'a = nat]
eberlm@63633
   623
lemmas prime_dvd_mult_eq_int = prime_dvd_mult_iff[where ?'a = int]
eberlm@63633
   624
lemmas prime_dvd_power_nat = prime_dvd_power[where ?'a = nat]
eberlm@63633
   625
lemmas prime_dvd_power_int = prime_dvd_power[where ?'a = int]
eberlm@63633
   626
lemmas prime_dvd_power_nat_iff = prime_dvd_power_iff[where ?'a = nat]
eberlm@63633
   627
lemmas prime_dvd_power_int_iff = prime_dvd_power_iff[where ?'a = int]
eberlm@63633
   628
lemmas prime_imp_power_coprime_nat = prime_imp_power_coprime[where ?'a = nat]
eberlm@63633
   629
lemmas prime_imp_power_coprime_int = prime_imp_power_coprime[where ?'a = int]
eberlm@63534
   630
lemmas primes_coprime_nat = primes_coprime[where ?'a = nat]
eberlm@63534
   631
lemmas primes_coprime_int = primes_coprime[where ?'a = nat]
eberlm@63633
   632
lemmas prime_divprod_pow_nat = prime_elem_divprod_pow[where ?'a = nat]
eberlm@63633
   633
lemmas prime_exp = prime_elem_power_iff[where ?'a = nat]
eberlm@63534
   634
eberlm@63635
   635
end