src/HOL/Computational_Algebra/Primes.thy
author haftmann
Sat Dec 02 16:50:53 2017 +0000 (18 months ago)
changeset 67117 19f627407264
parent 67091 1393c2340eec
child 67118 ccab07d1196c
permissions -rw-r--r--
overhauling of primes
wenzelm@65435
     1
(*  Title:      HOL/Computational_Algebra/Primes.thy
wenzelm@65435
     2
    Author:     Christophe Tabacznyj
wenzelm@65435
     3
    Author:     Lawrence C. Paulson
wenzelm@65435
     4
    Author:     Amine Chaieb
wenzelm@65435
     5
    Author:     Thomas M. Rasmussen
wenzelm@65435
     6
    Author:     Jeremy Avigad
wenzelm@65435
     7
    Author:     Tobias Nipkow
wenzelm@65435
     8
    Author:     Manuel Eberl
huffman@31706
     9
wenzelm@65435
    10
This theory deals with properties of primes. Definitions and lemmas are
haftmann@32479
    11
proved uniformly for the natural numbers and integers.
huffman@31706
    12
huffman@31706
    13
This file combines and revises a number of prior developments.
huffman@31706
    14
huffman@31706
    15
The original theories "GCD" and "Primes" were by Christophe Tabacznyj
wenzelm@58623
    16
and Lawrence C. Paulson, based on @{cite davenport92}. They introduced
huffman@31706
    17
gcd, lcm, and prime for the natural numbers.
huffman@31706
    18
huffman@31706
    19
The original theory "IntPrimes" was by Thomas M. Rasmussen, and
huffman@31706
    20
extended gcd, lcm, primes to the integers. Amine Chaieb provided
huffman@31706
    21
another extension of the notions to the integers, and added a number
huffman@31706
    22
of results to "Primes" and "GCD". IntPrimes also defined and developed
huffman@31706
    23
the congruence relations on the integers. The notion was extended to
webertj@33718
    24
the natural numbers by Chaieb.
huffman@31706
    25
avigad@32036
    26
Jeremy Avigad combined all of these, made everything uniform for the
avigad@32036
    27
natural numbers and the integers, and added a number of new theorems.
avigad@32036
    28
nipkow@31798
    29
Tobias Nipkow cleaned up a lot.
eberlm@63534
    30
eberlm@63534
    31
Florian Haftmann and Manuel Eberl put primality and prime factorisation
eberlm@63534
    32
onto an algebraic foundation and thus generalised these concepts to 
eberlm@63534
    33
other rings, such as polynomials. (see also the Factorial_Ring theory).
eberlm@63534
    34
eberlm@63534
    35
There were also previous formalisations of unique factorisation by 
eberlm@63534
    36
Thomas Marthedal Rasmussen, Jeremy Avigad, and David Gray.
wenzelm@21256
    37
*)
wenzelm@21256
    38
wenzelm@60526
    39
section \<open>Primes\<close>
wenzelm@21256
    40
haftmann@32479
    41
theory Primes
wenzelm@66453
    42
imports HOL.Binomial Euclidean_Algorithm
huffman@31706
    43
begin
huffman@31706
    44
haftmann@67117
    45
subsection \<open>Primes on @{typ nat} and @{typ int}\<close>
haftmann@67117
    46
haftmann@67117
    47
lemma Suc_0_not_prime_nat [simp]: "\<not> prime (Suc 0)"
haftmann@67117
    48
  using not_prime_1 [where ?'a = nat] by simp
haftmann@67117
    49
haftmann@67117
    50
lemma prime_ge_2_nat:
haftmann@67117
    51
  "p \<ge> 2" if "prime p" for p :: nat
haftmann@67117
    52
proof -
haftmann@67117
    53
  from that have "p \<noteq> 0" and "p \<noteq> 1"
haftmann@67117
    54
    by (auto dest: prime_elem_not_zeroI prime_elem_not_unit)
haftmann@67117
    55
  then show ?thesis
haftmann@67117
    56
    by simp
haftmann@67117
    57
qed
haftmann@67117
    58
haftmann@67117
    59
lemma prime_ge_2_int:
haftmann@67117
    60
  "p \<ge> 2" if "prime p" for p :: int
haftmann@67117
    61
proof -
haftmann@67117
    62
  from that have "prime_elem p" and "\<bar>p\<bar> = p"
haftmann@67117
    63
    by (auto dest: normalize_prime)
haftmann@67117
    64
  then have "p \<noteq> 0" and "\<bar>p\<bar> \<noteq> 1" and "p \<ge> 0"
haftmann@67117
    65
    by (auto dest: prime_elem_not_zeroI prime_elem_not_unit)
haftmann@67117
    66
  then show ?thesis
haftmann@67117
    67
    by simp
haftmann@67117
    68
qed
haftmann@67117
    69
haftmann@67117
    70
lemma prime_ge_0_int: "prime p \<Longrightarrow> p \<ge> (0::int)"
haftmann@67117
    71
  using prime_ge_2_int [of p] by simp
haftmann@67117
    72
haftmann@67117
    73
lemma prime_gt_0_nat: "prime p \<Longrightarrow> p > (0::nat)"
haftmann@67117
    74
  using prime_ge_2_nat [of p] by simp
haftmann@67117
    75
eberlm@63534
    76
(* As a simp or intro rule,
eberlm@63534
    77
eberlm@63534
    78
     prime p \<Longrightarrow> p > 0
eberlm@63534
    79
eberlm@63534
    80
   wreaks havoc here. When the premise includes \<forall>x \<in># M. prime x, it
eberlm@63534
    81
   leads to the backchaining
eberlm@63534
    82
eberlm@63534
    83
     x > 0
eberlm@63534
    84
     prime x
eberlm@63534
    85
     x \<in># M   which is, unfortunately,
haftmann@67117
    86
     count M x > 0  FIXME no, this is obsolete
eberlm@63534
    87
*)
eberlm@63534
    88
haftmann@67117
    89
lemma prime_gt_0_int: "prime p \<Longrightarrow> p > (0::int)"
haftmann@67117
    90
  using prime_ge_2_int [of p] by simp
haftmann@67117
    91
haftmann@67117
    92
lemma prime_ge_1_nat: "prime p \<Longrightarrow> p \<ge> (1::nat)"
haftmann@67117
    93
  using prime_ge_2_nat [of p] by simp
haftmann@67117
    94
haftmann@67117
    95
lemma prime_ge_Suc_0_nat: "prime p \<Longrightarrow> p \<ge> Suc 0"
haftmann@67117
    96
  using prime_ge_1_nat [of p] by simp
haftmann@67117
    97
haftmann@67117
    98
lemma prime_ge_1_int: "prime p \<Longrightarrow> p \<ge> (1::int)"
haftmann@67117
    99
  using prime_ge_2_int [of p] by simp
huffman@31706
   100
haftmann@67117
   101
lemma prime_gt_1_nat: "prime p \<Longrightarrow> p > (1::nat)"
haftmann@67117
   102
  using prime_ge_2_nat [of p] by simp
haftmann@67117
   103
haftmann@67117
   104
lemma prime_gt_Suc_0_nat: "prime p \<Longrightarrow> p > Suc 0"
haftmann@67117
   105
  using prime_gt_1_nat [of p] by simp
haftmann@67117
   106
haftmann@67117
   107
lemma prime_gt_1_int: "prime p \<Longrightarrow> p > (1::int)"
haftmann@67117
   108
  using prime_ge_2_int [of p] by simp
haftmann@67117
   109
haftmann@67117
   110
lemma prime_natI:
haftmann@67117
   111
  "prime p" if "p \<ge> 2" and "\<And>m n. p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n" for p :: nat
haftmann@67117
   112
  using that by (auto intro!: primeI prime_elemI)
haftmann@67117
   113
haftmann@67117
   114
lemma prime_intI:
haftmann@67117
   115
  "prime p" if "p \<ge> 2" and "\<And>m n. p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n" for p :: int
haftmann@67117
   116
  using that by (auto intro!: primeI prime_elemI)
haftmann@66837
   117
eberlm@63633
   118
lemma prime_elem_nat_iff:
haftmann@67117
   119
  "prime_elem n \<longleftrightarrow> prime n" for n :: nat
haftmann@67117
   120
  by (simp add: prime_def)
haftmann@67117
   121
haftmann@67117
   122
lemma prime_nat_iff_prime_elem:
haftmann@67117
   123
  "prime n \<longleftrightarrow> prime_elem n" for n :: nat
haftmann@67117
   124
  by (simp add: prime_elem_nat_iff)
haftmann@67117
   125
haftmann@67117
   126
lemma prime_elem_iff_prime_abs:
haftmann@67117
   127
  "prime_elem k \<longleftrightarrow> prime \<bar>k\<bar>" for k :: int
haftmann@67117
   128
  by (auto intro: primeI)
haftmann@67117
   129
haftmann@67117
   130
lemma prime_nat_int_transfer [simp]:
haftmann@67117
   131
  "prime (int n) \<longleftrightarrow> prime n" (is "?P \<longleftrightarrow> ?Q")
haftmann@67117
   132
proof
haftmann@67117
   133
  assume ?P
haftmann@67117
   134
  then have "n \<ge> 2"
haftmann@67117
   135
    by (auto dest: prime_ge_2_int)
haftmann@67117
   136
  then show ?Q
haftmann@67117
   137
  proof (rule prime_natI)
haftmann@67117
   138
    fix r s
haftmann@67117
   139
    assume "n dvd r * s"
haftmann@67117
   140
    then have "int n dvd int (r * s)"
haftmann@67117
   141
      by (simp add: zdvd_int)
haftmann@67117
   142
    then have "int n dvd int r * int s"
haftmann@67117
   143
      by simp
haftmann@67117
   144
    with \<open>?P\<close> have "int n dvd int r \<or> int n dvd int s"
haftmann@67117
   145
      by (auto dest: prime_dvd_mult_iff)
haftmann@67117
   146
    then show "n dvd r \<or> n dvd s"
haftmann@67117
   147
      by (simp add: zdvd_int)
haftmann@67117
   148
  qed
haftmann@67117
   149
next
haftmann@67117
   150
  assume ?Q
haftmann@67117
   151
  then have "int n \<ge> 2"
haftmann@67117
   152
    by (auto dest: prime_ge_2_nat)
haftmann@67117
   153
  then show ?P
haftmann@67117
   154
  proof (rule prime_intI)
haftmann@67117
   155
    fix r s
haftmann@67117
   156
    assume "int n dvd r * s"
haftmann@67117
   157
    then have "n dvd nat \<bar>r * s\<bar>"
haftmann@67117
   158
      by (simp add: zdvd_int)
haftmann@67117
   159
    then have "n dvd nat \<bar>r\<bar> * nat \<bar>s\<bar>"
haftmann@67117
   160
      by (simp add: nat_abs_mult_distrib)
haftmann@67117
   161
    with \<open>?Q\<close> have "n dvd nat \<bar>r\<bar> \<or> n dvd nat \<bar>s\<bar>"
haftmann@67117
   162
      by (auto dest: prime_dvd_mult_iff)
haftmann@67117
   163
    then show "int n dvd r \<or> int n dvd s"
haftmann@67117
   164
      by (simp add: zdvd_int)
haftmann@67117
   165
  qed
haftmann@67117
   166
qed
haftmann@67117
   167
haftmann@67117
   168
lemma prime_nat_iff_prime:
haftmann@67117
   169
  "prime (nat k) \<longleftrightarrow> prime k"
haftmann@67117
   170
proof (cases "k \<ge> 0")
haftmann@67117
   171
  case True
haftmann@67117
   172
  then show ?thesis
haftmann@67117
   173
    using prime_nat_int_transfer [of "nat k"] by simp
haftmann@67117
   174
next
haftmann@67117
   175
  case False
haftmann@67117
   176
  then show ?thesis
haftmann@67117
   177
    by (auto dest: prime_ge_2_int)
haftmann@67117
   178
qed
haftmann@67117
   179
haftmann@67117
   180
lemma prime_elem_int_nat_transfer:
haftmann@67117
   181
  "prime_elem n \<longleftrightarrow> prime_elem (nat \<bar>n\<bar>)"
haftmann@67117
   182
  by (simp add: prime_elem_iff_prime_abs prime_elem_nat_iff prime_nat_iff_prime)
haftmann@67117
   183
haftmann@67117
   184
lemma prime_elem_nat_int_transfer [simp]:
haftmann@67117
   185
  "prime_elem (int n) \<longleftrightarrow> prime_elem n"
haftmann@67117
   186
  by (simp add: prime_elem_nat_iff prime_elem_iff_prime_abs)
haftmann@67117
   187
haftmann@67117
   188
lemma prime_int_nat_transfer:
haftmann@67117
   189
  "prime k \<longleftrightarrow> k \<ge> 0 \<and> prime (nat k)"
haftmann@67117
   190
  by (auto simp add: prime_nat_iff_prime dest: prime_ge_2_int)
haftmann@67117
   191
haftmann@67117
   192
lemma prime_nat_naiveI:
haftmann@67117
   193
  "prime p" if "p \<ge> 2" and dvd: "\<And>n. n dvd p \<Longrightarrow> n = 1 \<or> n = p" for p :: nat
haftmann@67117
   194
proof (rule primeI, rule prime_elemI)
haftmann@67117
   195
  fix m n :: nat
haftmann@67117
   196
  assume "p dvd m * n"
haftmann@67117
   197
  then obtain r s where "p = r * s" "r dvd m" "s dvd n"
haftmann@67117
   198
    by (blast dest: division_decomp)
haftmann@67117
   199
  moreover have "r = 1 \<or> r = p"
haftmann@67117
   200
    using \<open>r dvd m\<close> \<open>p = r * s\<close> dvd [of r] by simp
haftmann@67117
   201
  ultimately show "p dvd m \<or> p dvd n"
haftmann@67117
   202
    by auto
haftmann@67117
   203
qed (use \<open>p \<ge> 2\<close> in simp_all)
haftmann@67117
   204
haftmann@67117
   205
lemma prime_int_naiveI:
haftmann@67117
   206
  "prime p" if "p \<ge> 2" and dvd: "\<And>k. k dvd p \<Longrightarrow> \<bar>k\<bar> = 1 \<or> \<bar>k\<bar> = p" for p :: int
haftmann@67117
   207
proof -
haftmann@67117
   208
  from \<open>p \<ge> 2\<close> have "nat p \<ge> 2"
haftmann@67117
   209
    by simp
haftmann@67117
   210
  then have "prime (nat p)"
haftmann@67117
   211
  proof (rule prime_nat_naiveI)
haftmann@67117
   212
    fix n
haftmann@67117
   213
    assume "n dvd nat p"
haftmann@67117
   214
    with \<open>p \<ge> 2\<close> have "n dvd nat \<bar>p\<bar>"
haftmann@67117
   215
      by simp
haftmann@67117
   216
    then have "int n dvd p"
haftmann@67117
   217
      by (simp add: int_dvd_iff)
haftmann@67117
   218
    with dvd [of "int n"] show "n = 1 \<or> n = nat p"
haftmann@67117
   219
      by auto
haftmann@67117
   220
  qed
haftmann@67117
   221
  then show ?thesis
haftmann@67117
   222
    by (simp add: prime_nat_iff_prime)
haftmann@67117
   223
qed
haftmann@67117
   224
haftmann@67117
   225
lemma prime_nat_iff:
haftmann@67117
   226
  "prime (n :: nat) \<longleftrightarrow> (1 < n \<and> (\<forall>m. m dvd n \<longrightarrow> m = 1 \<or> m = n))"
haftmann@67117
   227
proof (safe intro!: prime_gt_1_nat)
haftmann@67117
   228
  assume "prime n"
haftmann@67117
   229
  then have *: "prime_elem n"
haftmann@67117
   230
    by simp
eberlm@63534
   231
  fix m assume m: "m dvd n" "m \<noteq> n"
eberlm@63534
   232
  from * \<open>m dvd n\<close> have "n dvd m \<or> is_unit m"
eberlm@63633
   233
    by (intro irreducibleD' prime_elem_imp_irreducible)
eberlm@63534
   234
  with m show "m = 1" by (auto dest: dvd_antisym)
eberlm@63534
   235
next
eberlm@63534
   236
  assume "n > 1" "\<forall>m. m dvd n \<longrightarrow> m = 1 \<or> m = n"
haftmann@67117
   237
  then show "prime n"
haftmann@67117
   238
    using prime_nat_naiveI [of n] by auto
eberlm@63534
   239
qed
eberlm@63534
   240
eberlm@63633
   241
lemma prime_int_iff:
eberlm@63633
   242
  "prime (n::int) \<longleftrightarrow> (1 < n \<and> (\<forall>m. m \<ge> 0 \<and> m dvd n \<longrightarrow> m = 1 \<or> m = n))"
eberlm@63534
   243
proof (intro iffI conjI allI impI; (elim conjE)?)
eberlm@63633
   244
  assume *: "prime n"
eberlm@63633
   245
  hence irred: "irreducible n" by (simp add: prime_elem_imp_irreducible)
eberlm@63534
   246
  from * have "n \<ge> 0" "n \<noteq> 0" "n \<noteq> 1" 
eberlm@63633
   247
    by (auto simp: prime_def zabs_def not_less split: if_splits)
eberlm@63534
   248
  thus "n > 1" by presburger
eberlm@63534
   249
  fix m assume "m dvd n" \<open>m \<ge> 0\<close>
eberlm@63534
   250
  with irred have "m dvd 1 \<or> n dvd m" by (auto simp: irreducible_altdef)
eberlm@63534
   251
  with \<open>m dvd n\<close> \<open>m \<ge> 0\<close> \<open>n > 1\<close> show "m = 1 \<or> m = n"
eberlm@63534
   252
    using associated_iff_dvd[of m n] by auto
eberlm@63534
   253
next
eberlm@63534
   254
  assume n: "1 < n" "\<forall>m. m \<ge> 0 \<and> m dvd n \<longrightarrow> m = 1 \<or> m = n"
eberlm@63534
   255
  hence "nat n > 1" by simp
eberlm@63534
   256
  moreover have "\<forall>m. m dvd nat n \<longrightarrow> m = 1 \<or> m = nat n"
eberlm@63534
   257
  proof (intro allI impI)
eberlm@63534
   258
    fix m assume "m dvd nat n"
eberlm@63534
   259
    with \<open>n > 1\<close> have "int m dvd n" by (auto simp: int_dvd_iff)
lp15@65583
   260
    with n(2) have "int m = 1 \<or> int m = n"
lp15@65583
   261
      using of_nat_0_le_iff by blast
eberlm@63534
   262
    thus "m = 1 \<or> m = nat n" by auto
eberlm@63534
   263
  qed
eberlm@63633
   264
  ultimately show "prime n" 
eberlm@63633
   265
    unfolding prime_int_nat_transfer prime_nat_iff by auto
eberlm@63534
   266
qed
chaieb@22027
   267
eberlm@63534
   268
lemma prime_nat_not_dvd:
eberlm@63534
   269
  assumes "prime p" "p > n" "n \<noteq> (1::nat)"
eberlm@63534
   270
  shows   "\<not>n dvd p"
eberlm@63534
   271
proof
eberlm@63534
   272
  assume "n dvd p"
eberlm@63633
   273
  from assms(1) have "irreducible p" by (simp add: prime_elem_imp_irreducible)
eberlm@63534
   274
  from irreducibleD'[OF this \<open>n dvd p\<close>] \<open>n dvd p\<close> \<open>p > n\<close> assms show False
eberlm@63534
   275
    by (cases "n = 0") (auto dest!: dvd_imp_le)
eberlm@63534
   276
qed
chaieb@22027
   277
eberlm@63534
   278
lemma prime_int_not_dvd:
eberlm@63534
   279
  assumes "prime p" "p > n" "n > (1::int)"
eberlm@63534
   280
  shows   "\<not>n dvd p"
eberlm@63534
   281
proof
eberlm@63534
   282
  assume "n dvd p"
eberlm@63633
   283
  from assms(1) have "irreducible p" by (simp add: prime_elem_imp_irreducible)
eberlm@63534
   284
  from irreducibleD'[OF this \<open>n dvd p\<close>] \<open>n dvd p\<close> \<open>p > n\<close> assms show False
eberlm@63534
   285
    by (auto dest!: zdvd_imp_le)
eberlm@63534
   286
qed
eberlm@63534
   287
eberlm@63534
   288
lemma prime_odd_nat: "prime p \<Longrightarrow> p > (2::nat) \<Longrightarrow> odd p"
eberlm@63534
   289
  by (intro prime_nat_not_dvd) auto
eberlm@63534
   290
eberlm@63534
   291
lemma prime_odd_int: "prime p \<Longrightarrow> p > (2::int) \<Longrightarrow> odd p"
eberlm@63534
   292
  by (intro prime_int_not_dvd) auto
wenzelm@22367
   293
lp15@59669
   294
lemma prime_int_altdef:
lp15@55242
   295
  "prime p = (1 < p \<and> (\<forall>m::int. m \<ge> 0 \<longrightarrow> m dvd p \<longrightarrow>
lp15@55242
   296
    m = 1 \<or> m = p))"
eberlm@63633
   297
  unfolding prime_int_iff by blast
chaieb@27568
   298
haftmann@62481
   299
lemma not_prime_eq_prod_nat:
eberlm@63534
   300
  assumes "m > 1" "\<not>prime (m::nat)"
eberlm@63534
   301
  shows   "\<exists>n k. n = m * k \<and> 1 < m \<and> m < n \<and> 1 < k \<and> k < n"
eberlm@63534
   302
  using assms irreducible_altdef[of m]
eberlm@63633
   303
  by (auto simp: prime_elem_iff_irreducible prime_def irreducible_altdef)
huffman@53598
   304
lp15@64773
   305
    
haftmann@67117
   306
subsection \<open>Largest exponent of a prime factor\<close>
haftmann@67117
   307
lp15@64773
   308
text\<open>Possibly duplicates other material, but avoid the complexities of multisets.\<close>
lp15@64773
   309
  
lp15@64773
   310
lemma prime_power_cancel_less:
lp15@64773
   311
  assumes "prime p" and eq: "m * (p ^ k) = m' * (p ^ k')" and less: "k < k'" and "\<not> p dvd m"
lp15@64773
   312
  shows False
lp15@64773
   313
proof -
lp15@64773
   314
  obtain l where l: "k' = k + l" and "l > 0"
lp15@64773
   315
    using less less_imp_add_positive by auto
lp15@64773
   316
  have "m = m * (p ^ k) div (p ^ k)"
lp15@64773
   317
    using \<open>prime p\<close> by simp
lp15@64773
   318
  also have "\<dots> = m' * (p ^ k') div (p ^ k)"
lp15@64773
   319
    using eq by simp
lp15@64773
   320
  also have "\<dots> = m' * (p ^ l) * (p ^ k) div (p ^ k)"
lp15@64773
   321
    by (simp add: l mult.commute mult.left_commute power_add)
lp15@64773
   322
  also have "... = m' * (p ^ l)"
lp15@64773
   323
    using \<open>prime p\<close> by simp
lp15@64773
   324
  finally have "p dvd m"
lp15@64773
   325
    using \<open>l > 0\<close> by simp
lp15@64773
   326
  with assms show False
lp15@64773
   327
    by simp
lp15@64773
   328
qed
lp15@64773
   329
lp15@64773
   330
lemma prime_power_cancel:
lp15@64773
   331
  assumes "prime p" and eq: "m * (p ^ k) = m' * (p ^ k')" and "\<not> p dvd m" "\<not> p dvd m'"
lp15@64773
   332
  shows "k = k'"
lp15@64773
   333
  using prime_power_cancel_less [OF \<open>prime p\<close>] assms
lp15@64773
   334
  by (metis linorder_neqE_nat)
lp15@64773
   335
lp15@64773
   336
lemma prime_power_cancel2:
lp15@64773
   337
  assumes "prime p" "m * (p ^ k) = m' * (p ^ k')" "\<not> p dvd m" "\<not> p dvd m'"
lp15@64773
   338
  obtains "m = m'" "k = k'"
lp15@64773
   339
  using prime_power_cancel [OF assms] assms by auto
lp15@64773
   340
lp15@64773
   341
lemma prime_power_canonical:
haftmann@67051
   342
  fixes m :: nat
lp15@64773
   343
  assumes "prime p" "m > 0"
haftmann@67051
   344
  shows "\<exists>k n. \<not> p dvd n \<and> m = n * p ^ k"
lp15@64773
   345
using \<open>m > 0\<close>
lp15@64773
   346
proof (induction m rule: less_induct)
lp15@64773
   347
  case (less m)
lp15@64773
   348
  show ?case
lp15@64773
   349
  proof (cases "p dvd m")
lp15@64773
   350
    case True
lp15@64773
   351
    then obtain m' where m': "m = p * m'"
lp15@64773
   352
      using dvdE by blast
lp15@64773
   353
    with \<open>prime p\<close> have "0 < m'" "m' < m"
lp15@64773
   354
      using less.prems prime_nat_iff by auto
lp15@64773
   355
    with m' less show ?thesis
lp15@64773
   356
      by (metis power_Suc mult.left_commute)
lp15@64773
   357
  next
lp15@64773
   358
    case False
lp15@64773
   359
    then show ?thesis
lp15@64773
   360
      by (metis mult.right_neutral power_0)
lp15@64773
   361
  qed
lp15@64773
   362
qed
lp15@64773
   363
huffman@53598
   364
wenzelm@60526
   365
subsubsection \<open>Make prime naively executable\<close>
nipkow@32007
   366
eberlm@63633
   367
lemma prime_nat_iff':
wenzelm@67091
   368
  "prime (p :: nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {2..<p}. \<not> n dvd p)"
eberlm@63534
   369
proof safe
haftmann@65025
   370
  assume "p > 1" and *: "\<forall>n\<in>{2..<p}. \<not>n dvd p"
eberlm@63633
   371
  show "prime p" unfolding prime_nat_iff
eberlm@63534
   372
  proof (intro conjI allI impI)
eberlm@63534
   373
    fix m assume "m dvd p"
eberlm@63534
   374
    with \<open>p > 1\<close> have "m \<noteq> 0" by (intro notI) auto
eberlm@63534
   375
    hence "m \<ge> 1" by simp
haftmann@65025
   376
    moreover from \<open>m dvd p\<close> and * have "m \<notin> {2..<p}" by blast
eberlm@63534
   377
    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
   378
    ultimately show "m = 1 \<or> m = p" by simp
eberlm@63534
   379
  qed fact+
eberlm@63633
   380
qed (auto simp: prime_nat_iff)
nipkow@32007
   381
eberlm@63633
   382
lemma prime_int_iff':
wenzelm@67091
   383
  "prime (p :: int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {2..<p}. \<not> n dvd p)" (is "?lhs = ?rhs")
eberlm@63534
   384
proof
eberlm@63534
   385
  assume "?lhs"
haftmann@65025
   386
  thus "?rhs"
haftmann@65025
   387
      by (auto simp: prime_int_nat_transfer dvd_int_unfold_dvd_nat prime_nat_iff')
eberlm@63534
   388
next
eberlm@63534
   389
  assume "?rhs"
haftmann@65025
   390
  thus "?lhs"
haftmann@65025
   391
    by (auto simp: prime_int_nat_transfer zdvd_int prime_nat_iff')
eberlm@63534
   392
qed
nipkow@32007
   393
haftmann@64590
   394
lemma prime_int_numeral_eq [simp]:
haftmann@64590
   395
  "prime (numeral m :: int) \<longleftrightarrow> prime (numeral m :: nat)"
haftmann@64590
   396
  by (simp add: prime_int_nat_transfer)
nipkow@32007
   397
eberlm@63635
   398
lemma two_is_prime_nat [simp]: "prime (2::nat)"
haftmann@65025
   399
  by (simp add: prime_nat_iff')
nipkow@32007
   400
haftmann@64590
   401
lemma prime_nat_numeral_eq [simp]:
haftmann@64590
   402
  "prime (numeral m :: nat) \<longleftrightarrow>
haftmann@64590
   403
    (1::nat) < numeral m \<and>
haftmann@65025
   404
    (\<forall>n::nat \<in> set [2..<numeral m]. \<not> n dvd numeral m)"
haftmann@65025
   405
  by (simp only: prime_nat_iff' set_upt)  \<comment> \<open>TODO Sieve Of Erathosthenes might speed this up\<close>
eberlm@63534
   406
eberlm@63534
   407
wenzelm@60526
   408
text\<open>A bit of regression testing:\<close>
nipkow@32111
   409
haftmann@58954
   410
lemma "prime(97::nat)" by simp
eberlm@63534
   411
lemma "prime(97::int)" by simp
huffman@31706
   412
eberlm@63534
   413
lemma prime_factor_nat: 
eberlm@63534
   414
  "n \<noteq> (1::nat) \<Longrightarrow> \<exists>p. prime p \<and> p dvd n"
eberlm@63534
   415
  using prime_divisor_exists[of n]
eberlm@63534
   416
  by (cases "n = 0") (auto intro: exI[of _ "2::nat"])
nipkow@23983
   417
wenzelm@44872
   418
wenzelm@60526
   419
subsection \<open>Infinitely many primes\<close>
avigad@32036
   420
eberlm@63534
   421
lemma next_prime_bound: "\<exists>p::nat. prime p \<and> n < p \<and> p \<le> fact n + 1"
avigad@32036
   422
proof-
lp15@59730
   423
  have f1: "fact n + 1 \<noteq> (1::nat)" using fact_ge_1 [of n, where 'a=nat] by arith
avigad@32036
   424
  from prime_factor_nat [OF f1]
eberlm@63534
   425
  obtain p :: nat where "prime p" and "p dvd fact n + 1" by auto
wenzelm@44872
   426
  then have "p \<le> fact n + 1" apply (intro dvd_imp_le) apply auto done
wenzelm@44872
   427
  { assume "p \<le> n"
wenzelm@60526
   428
    from \<open>prime p\<close> have "p \<ge> 1"
avigad@32036
   429
      by (cases p, simp_all)
wenzelm@60526
   430
    with \<open>p <= n\<close> have "p dvd fact n"
lp15@59730
   431
      by (intro dvd_fact)
wenzelm@60526
   432
    with \<open>p dvd fact n + 1\<close> have "p dvd fact n + 1 - fact n"
avigad@32036
   433
      by (rule dvd_diff_nat)
wenzelm@44872
   434
    then have "p dvd 1" by simp
wenzelm@44872
   435
    then have "p <= 1" by auto
lp15@61762
   436
    moreover from \<open>prime p\<close> have "p > 1"
eberlm@63633
   437
      using prime_nat_iff by blast
avigad@32036
   438
    ultimately have False by auto}
wenzelm@44872
   439
  then have "n < p" by presburger
wenzelm@60526
   440
  with \<open>prime p\<close> and \<open>p <= fact n + 1\<close> show ?thesis by auto
avigad@32036
   441
qed
avigad@32036
   442
lp15@59669
   443
lemma bigger_prime: "\<exists>p. prime p \<and> p > (n::nat)"
wenzelm@44872
   444
  using next_prime_bound by auto
avigad@32036
   445
avigad@32036
   446
lemma primes_infinite: "\<not> (finite {(p::nat). prime p})"
avigad@32036
   447
proof
avigad@32036
   448
  assume "finite {(p::nat). prime p}"
wenzelm@67091
   449
  with Max_ge have "(\<exists>b. (\<forall>x \<in> {(p::nat). prime p}. x \<le> b))"
avigad@32036
   450
    by auto
wenzelm@67091
   451
  then obtain b where "\<forall>(x::nat). prime x \<longrightarrow> x \<le> b"
avigad@32036
   452
    by auto
wenzelm@44872
   453
  with bigger_prime [of b] show False
wenzelm@44872
   454
    by auto
avigad@32036
   455
qed
avigad@32036
   456
haftmann@67117
   457
subsection \<open>Powers of Primes\<close>
lp15@55215
   458
wenzelm@60526
   459
text\<open>Versions for type nat only\<close>
lp15@55215
   460
lp15@59669
   461
lemma prime_product:
lp15@55215
   462
  fixes p::nat
lp15@55215
   463
  assumes "prime (p * q)"
lp15@55215
   464
  shows "p = 1 \<or> q = 1"
lp15@55215
   465
proof -
lp15@59669
   466
  from assms have
lp15@55215
   467
    "1 < p * q" and P: "\<And>m. m dvd p * q \<Longrightarrow> m = 1 \<or> m = p * q"
eberlm@63633
   468
    unfolding prime_nat_iff by auto
wenzelm@60526
   469
  from \<open>1 < p * q\<close> have "p \<noteq> 0" by (cases p) auto
lp15@55215
   470
  then have Q: "p = p * q \<longleftrightarrow> q = 1" by auto
lp15@55215
   471
  have "p dvd p * q" by simp
lp15@55215
   472
  then have "p = 1 \<or> p = p * q" by (rule P)
lp15@55215
   473
  then show ?thesis by (simp add: Q)
lp15@55215
   474
qed
lp15@55215
   475
eberlm@63534
   476
(* TODO: Generalise? *)
eberlm@63534
   477
lemma prime_power_mult_nat:
haftmann@67051
   478
  fixes p :: nat
lp15@55215
   479
  assumes p: "prime p" and xy: "x * y = p ^ k"
haftmann@67051
   480
  shows "\<exists>i j. x = p ^ i \<and> y = p^ j"
lp15@55215
   481
using xy
lp15@55215
   482
proof(induct k arbitrary: x y)
lp15@55215
   483
  case 0 thus ?case apply simp by (rule exI[where x="0"], simp)
lp15@55215
   484
next
lp15@55215
   485
  case (Suc k x y)
lp15@55215
   486
  from Suc.prems have pxy: "p dvd x*y" by auto
eberlm@63633
   487
  from prime_dvd_multD [OF p pxy] have pxyc: "p dvd x \<or> p dvd y" .
lp15@59669
   488
  from p have p0: "p \<noteq> 0" by - (rule ccontr, simp)
lp15@55215
   489
  {assume px: "p dvd x"
lp15@55215
   490
    then obtain d where d: "x = p*d" unfolding dvd_def by blast
lp15@55215
   491
    from Suc.prems d  have "p*d*y = p^Suc k" by simp
lp15@55215
   492
    hence th: "d*y = p^k" using p0 by simp
lp15@55215
   493
    from Suc.hyps[OF th] obtain i j where ij: "d = p^i" "y = p^j" by blast
lp15@59669
   494
    with d have "x = p^Suc i" by simp
lp15@55215
   495
    with ij(2) have ?case by blast}
lp15@59669
   496
  moreover
lp15@55215
   497
  {assume px: "p dvd y"
lp15@55215
   498
    then obtain d where d: "y = p*d" unfolding dvd_def by blast
haftmann@57512
   499
    from Suc.prems d  have "p*d*x = p^Suc k" by (simp add: mult.commute)
lp15@55215
   500
    hence th: "d*x = p^k" using p0 by simp
lp15@55215
   501
    from Suc.hyps[OF th] obtain i j where ij: "d = p^i" "x = p^j" by blast
lp15@59669
   502
    with d have "y = p^Suc i" by simp
lp15@55215
   503
    with ij(2) have ?case by blast}
lp15@55215
   504
  ultimately show ?case  using pxyc by blast
lp15@55215
   505
qed
lp15@55215
   506
eberlm@63534
   507
lemma prime_power_exp_nat:
lp15@55215
   508
  fixes p::nat
lp15@59669
   509
  assumes p: "prime p" and n: "n \<noteq> 0"
lp15@55215
   510
    and xn: "x^n = p^k" shows "\<exists>i. x = p^i"
lp15@55215
   511
  using n xn
lp15@55215
   512
proof(induct n arbitrary: k)
lp15@55215
   513
  case 0 thus ?case by simp
lp15@55215
   514
next
lp15@55215
   515
  case (Suc n k) hence th: "x*x^n = p^k" by simp
lp15@55215
   516
  {assume "n = 0" with Suc have ?case by simp (rule exI[where x="k"], simp)}
lp15@55215
   517
  moreover
lp15@55215
   518
  {assume n: "n \<noteq> 0"
eberlm@63534
   519
    from prime_power_mult_nat[OF p th]
lp15@55215
   520
    obtain i j where ij: "x = p^i" "x^n = p^j"by blast
lp15@55215
   521
    from Suc.hyps[OF n ij(2)] have ?case .}
lp15@55215
   522
  ultimately show ?case by blast
lp15@55215
   523
qed
lp15@55215
   524
eberlm@63534
   525
lemma divides_primepow_nat:
haftmann@67051
   526
  fixes p :: nat
lp15@59669
   527
  assumes p: "prime p"
haftmann@67051
   528
  shows "d dvd p ^ k \<longleftrightarrow> (\<exists>i\<le>k. d = p ^ i)"
haftmann@67051
   529
  using assms divides_primepow [of p d k] by (auto intro: le_imp_power_dvd)
lp15@55215
   530
eberlm@63534
   531
wenzelm@60526
   532
subsection \<open>Chinese Remainder Theorem Variants\<close>
lp15@55238
   533
lp15@55238
   534
lemma bezout_gcd_nat:
lp15@55238
   535
  fixes a::nat shows "\<exists>x y. a * x - b * y = gcd a b \<or> b * x - a * y = gcd a b"
lp15@55238
   536
  using bezout_nat[of a b]
eberlm@62429
   537
by (metis bezout_nat diff_add_inverse gcd_add_mult gcd.commute
lp15@59669
   538
  gcd_nat.right_neutral mult_0)
lp15@55238
   539
lp15@55238
   540
lemma gcd_bezout_sum_nat:
lp15@59669
   541
  fixes a::nat
lp15@59669
   542
  assumes "a * x + b * y = d"
lp15@55238
   543
  shows "gcd a b dvd d"
lp15@55238
   544
proof-
lp15@55238
   545
  let ?g = "gcd a b"
lp15@59669
   546
    have dv: "?g dvd a*x" "?g dvd b * y"
lp15@55238
   547
      by simp_all
lp15@55238
   548
    from dvd_add[OF dv] assms
lp15@55238
   549
    show ?thesis by auto
lp15@55238
   550
qed
lp15@55238
   551
lp15@55238
   552
wenzelm@60526
   553
text \<open>A binary form of the Chinese Remainder Theorem.\<close>
lp15@55238
   554
eberlm@63534
   555
(* TODO: Generalise? *)
lp15@59669
   556
lemma chinese_remainder:
lp15@55238
   557
  fixes a::nat  assumes ab: "coprime a b" and a: "a \<noteq> 0" and b: "b \<noteq> 0"
lp15@55238
   558
  shows "\<exists>x q1 q2. x = u + q1 * a \<and> x = v + q2 * b"
lp15@55238
   559
proof-
lp15@55238
   560
  from bezout_add_strong_nat[OF a, of b] bezout_add_strong_nat[OF b, of a]
lp15@59669
   561
  obtain d1 x1 y1 d2 x2 y2 where dxy1: "d1 dvd a" "d1 dvd b" "a * x1 = b * y1 + d1"
lp15@55238
   562
    and dxy2: "d2 dvd b" "d2 dvd a" "b * x2 = a * y2 + d2" by blast
haftmann@67051
   563
  then have d12: "d1 = 1" "d2 = 1"
haftmann@67051
   564
    using ab coprime_common_divisor_nat [of a b] by blast+
lp15@55238
   565
  let ?x = "v * a * x1 + u * b * x2"
lp15@55238
   566
  let ?q1 = "v * x1 + u * y2"
lp15@55238
   567
  let ?q2 = "v * y1 + u * x2"
lp15@59669
   568
  from dxy2(3)[simplified d12] dxy1(3)[simplified d12]
lp15@55238
   569
  have "?x = u + ?q1 * a" "?x = v + ?q2 * b"
lp15@55337
   570
    by algebra+
lp15@55238
   571
  thus ?thesis by blast
lp15@55238
   572
qed
lp15@55238
   573
wenzelm@60526
   574
text \<open>Primality\<close>
lp15@55238
   575
lp15@55238
   576
lemma coprime_bezout_strong:
lp15@55238
   577
  fixes a::nat assumes "coprime a b"  "b \<noteq> 1"
lp15@55238
   578
  shows "\<exists>x y. a * x = b * y + 1"
haftmann@67051
   579
  by (metis add.commute add.right_neutral assms(1) assms(2) chinese_remainder coprime_1_left coprime_1_right coprime_crossproduct_nat mult.commute mult.right_neutral mult_cancel_left)
lp15@55238
   580
lp15@59669
   581
lemma bezout_prime:
lp15@55238
   582
  assumes p: "prime p" and pa: "\<not> p dvd a"
lp15@55238
   583
  shows "\<exists>x y. a*x = Suc (p*y)"
haftmann@62349
   584
proof -
lp15@55238
   585
  have ap: "coprime a p"
haftmann@67051
   586
    using coprime_commute p pa prime_imp_coprime by auto
haftmann@62349
   587
  moreover from p have "p \<noteq> 1" by auto
haftmann@62349
   588
  ultimately have "\<exists>x y. a * x = p * y + 1"
haftmann@62349
   589
    by (rule coprime_bezout_strong)
haftmann@62349
   590
  then show ?thesis by simp    
lp15@55238
   591
qed
eberlm@63534
   592
(* END TODO *)
lp15@55238
   593
eberlm@63534
   594
eberlm@63534
   595
eberlm@63534
   596
subsection \<open>Multiplicity and primality for natural numbers and integers\<close>
eberlm@63534
   597
eberlm@63534
   598
lemma prime_factors_gt_0_nat:
eberlm@63534
   599
  "p \<in> prime_factors x \<Longrightarrow> p > (0::nat)"
haftmann@63905
   600
  by (simp add: in_prime_factors_imp_prime prime_gt_0_nat)
eberlm@63534
   601
eberlm@63534
   602
lemma prime_factors_gt_0_int:
eberlm@63534
   603
  "p \<in> prime_factors x \<Longrightarrow> p > (0::int)"
haftmann@63905
   604
  by (simp add: in_prime_factors_imp_prime prime_gt_0_int)
eberlm@63534
   605
haftmann@63905
   606
lemma prime_factors_ge_0_int [elim]: (* FIXME !? *)
eberlm@63534
   607
  fixes n :: int
eberlm@63534
   608
  shows "p \<in> prime_factors n \<Longrightarrow> p \<ge> 0"
haftmann@63905
   609
  by (drule prime_factors_gt_0_int) simp
haftmann@63905
   610
  
nipkow@63830
   611
lemma prod_mset_prime_factorization_int:
eberlm@63534
   612
  fixes n :: int
eberlm@63534
   613
  assumes "n > 0"
nipkow@63830
   614
  shows   "prod_mset (prime_factorization n) = n"
nipkow@63830
   615
  using assms by (simp add: prod_mset_prime_factorization)
eberlm@63534
   616
eberlm@63534
   617
lemma prime_factorization_exists_nat:
eberlm@63534
   618
  "n > 0 \<Longrightarrow> (\<exists>M. (\<forall>p::nat \<in> set_mset M. prime p) \<and> n = (\<Prod>i \<in># M. i))"
eberlm@63633
   619
  using prime_factorization_exists[of n] by (auto simp: prime_def)
eberlm@63534
   620
nipkow@63830
   621
lemma prod_mset_prime_factorization_nat [simp]: 
nipkow@63830
   622
  "(n::nat) > 0 \<Longrightarrow> prod_mset (prime_factorization n) = n"
nipkow@63830
   623
  by (subst prod_mset_prime_factorization) simp_all
eberlm@63534
   624
eberlm@63534
   625
lemma prime_factorization_nat:
eberlm@63534
   626
    "n > (0::nat) \<Longrightarrow> n = (\<Prod>p \<in> prime_factors n. p ^ multiplicity p n)"
nipkow@64272
   627
  by (simp add: prod_prime_factors)
eberlm@63534
   628
eberlm@63534
   629
lemma prime_factorization_int:
eberlm@63534
   630
    "n > (0::int) \<Longrightarrow> n = (\<Prod>p \<in> prime_factors n. p ^ multiplicity p n)"
nipkow@64272
   631
  by (simp add: prod_prime_factors)
eberlm@63534
   632
eberlm@63534
   633
lemma prime_factorization_unique_nat:
eberlm@63534
   634
  fixes f :: "nat \<Rightarrow> _"
eberlm@63534
   635
  assumes S_eq: "S = {p. 0 < f p}"
eberlm@63534
   636
    and "finite S"
eberlm@63534
   637
    and S: "\<forall>p\<in>S. prime p" "n = (\<Prod>p\<in>S. p ^ f p)"
eberlm@63633
   638
  shows "S = prime_factors n \<and> (\<forall>p. prime p \<longrightarrow> f p = multiplicity p n)"
eberlm@63534
   639
  using assms by (intro prime_factorization_unique'') auto
eberlm@63534
   640
eberlm@63534
   641
lemma prime_factorization_unique_int:
eberlm@63534
   642
  fixes f :: "int \<Rightarrow> _"
eberlm@63534
   643
  assumes S_eq: "S = {p. 0 < f p}"
eberlm@63534
   644
    and "finite S"
eberlm@63534
   645
    and S: "\<forall>p\<in>S. prime p" "abs n = (\<Prod>p\<in>S. p ^ f p)"
eberlm@63633
   646
  shows "S = prime_factors n \<and> (\<forall>p. prime p \<longrightarrow> f p = multiplicity p n)"
eberlm@63534
   647
  using assms by (intro prime_factorization_unique'') auto
eberlm@63534
   648
eberlm@63534
   649
lemma prime_factors_characterization_nat:
eberlm@63534
   650
  "S = {p. 0 < f (p::nat)} \<Longrightarrow>
eberlm@63534
   651
    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
   652
  by (rule prime_factorization_unique_nat [THEN conjunct1, symmetric])
eberlm@63534
   653
eberlm@63534
   654
lemma prime_factors_characterization'_nat:
eberlm@63534
   655
  "finite {p. 0 < f (p::nat)} \<Longrightarrow>
eberlm@63534
   656
    (\<forall>p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow>
eberlm@63534
   657
      prime_factors (\<Prod>p | 0 < f p. p ^ f p) = {p. 0 < f p}"
eberlm@63534
   658
  by (rule prime_factors_characterization_nat) auto
eberlm@63534
   659
eberlm@63534
   660
lemma prime_factors_characterization_int:
eberlm@63534
   661
  "S = {p. 0 < f (p::int)} \<Longrightarrow> finite S \<Longrightarrow>
eberlm@63534
   662
    \<forall>p\<in>S. prime p \<Longrightarrow> abs n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> prime_factors n = S"
eberlm@63534
   663
  by (rule prime_factorization_unique_int [THEN conjunct1, symmetric])
eberlm@63534
   664
eberlm@63534
   665
(* TODO Move *)
nipkow@64272
   666
lemma abs_prod: "abs (prod f A :: 'a :: linordered_idom) = prod (\<lambda>x. abs (f x)) A"
eberlm@63534
   667
  by (cases "finite A", induction A rule: finite_induct) (simp_all add: abs_mult)
eberlm@63534
   668
eberlm@63534
   669
lemma primes_characterization'_int [rule_format]:
eberlm@63534
   670
  "finite {p. p \<ge> 0 \<and> 0 < f (p::int)} \<Longrightarrow> \<forall>p. 0 < f p \<longrightarrow> prime p \<Longrightarrow>
eberlm@63534
   671
      prime_factors (\<Prod>p | p \<ge> 0 \<and> 0 < f p. p ^ f p) = {p. p \<ge> 0 \<and> 0 < f p}"
nipkow@64272
   672
  by (rule prime_factors_characterization_int) (auto simp: abs_prod prime_ge_0_int)
eberlm@63534
   673
eberlm@63534
   674
lemma multiplicity_characterization_nat:
eberlm@63633
   675
  "S = {p. 0 < f (p::nat)} \<Longrightarrow> finite S \<Longrightarrow> \<forall>p\<in>S. prime p \<Longrightarrow> prime p \<Longrightarrow>
eberlm@63534
   676
    n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> multiplicity p n = f p"
eberlm@63534
   677
  by (frule prime_factorization_unique_nat [of S f n, THEN conjunct2, rule_format, symmetric]) auto
eberlm@63534
   678
eberlm@63534
   679
lemma multiplicity_characterization'_nat: "finite {p. 0 < f (p::nat)} \<longrightarrow>
eberlm@63633
   680
    (\<forall>p. 0 < f p \<longrightarrow> prime p) \<longrightarrow> prime p \<longrightarrow>
eberlm@63534
   681
      multiplicity p (\<Prod>p | 0 < f p. p ^ f p) = f p"
eberlm@63534
   682
  by (intro impI, rule multiplicity_characterization_nat) auto
eberlm@63534
   683
eberlm@63534
   684
lemma multiplicity_characterization_int: "S = {p. 0 < f (p::int)} \<Longrightarrow>
eberlm@63633
   685
    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
   686
  by (frule prime_factorization_unique_int [of S f n, THEN conjunct2, rule_format, symmetric]) 
nipkow@64272
   687
     (auto simp: abs_prod power_abs prime_ge_0_int intro!: prod.cong)
eberlm@63534
   688
eberlm@63534
   689
lemma multiplicity_characterization'_int [rule_format]:
eberlm@63534
   690
  "finite {p. p \<ge> 0 \<and> 0 < f (p::int)} \<Longrightarrow>
eberlm@63633
   691
    (\<forall>p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow> prime p \<Longrightarrow>
eberlm@63534
   692
      multiplicity p (\<Prod>p | p \<ge> 0 \<and> 0 < f p. p ^ f p) = f p"
eberlm@63534
   693
  by (rule multiplicity_characterization_int) (auto simp: prime_ge_0_int)
eberlm@63534
   694
eberlm@63534
   695
lemma multiplicity_one_nat [simp]: "multiplicity p (Suc 0) = 0"
eberlm@63534
   696
  unfolding One_nat_def [symmetric] by (rule multiplicity_one)
eberlm@63534
   697
eberlm@63534
   698
lemma multiplicity_eq_nat:
eberlm@63534
   699
  fixes x and y::nat
eberlm@63633
   700
  assumes "x > 0" "y > 0" "\<And>p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
eberlm@63534
   701
  shows "x = y"
eberlm@63534
   702
  using multiplicity_eq_imp_eq[of x y] assms by simp
eberlm@63534
   703
eberlm@63534
   704
lemma multiplicity_eq_int:
eberlm@63534
   705
  fixes x y :: int
eberlm@63633
   706
  assumes "x > 0" "y > 0" "\<And>p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
eberlm@63534
   707
  shows "x = y"
eberlm@63534
   708
  using multiplicity_eq_imp_eq[of x y] assms by simp
eberlm@63534
   709
eberlm@63534
   710
lemma multiplicity_prod_prime_powers:
eberlm@63633
   711
  assumes "finite S" "\<And>x. x \<in> S \<Longrightarrow> prime x" "prime p"
eberlm@63534
   712
  shows   "multiplicity p (\<Prod>p \<in> S. p ^ f p) = (if p \<in> S then f p else 0)"
eberlm@63534
   713
proof -
eberlm@63534
   714
  define g where "g = (\<lambda>x. if x \<in> S then f x else 0)"
eberlm@63534
   715
  define A where "A = Abs_multiset g"
eberlm@63534
   716
  have "{x. g x > 0} \<subseteq> S" by (auto simp: g_def)
eberlm@63534
   717
  from finite_subset[OF this assms(1)] have [simp]: "g :  multiset"
eberlm@63534
   718
    by (simp add: multiset_def)
eberlm@63534
   719
  from assms have count_A: "count A x = g x" for x unfolding A_def
eberlm@63534
   720
    by simp
eberlm@63534
   721
  have set_mset_A: "set_mset A = {x\<in>S. f x > 0}"
eberlm@63534
   722
    unfolding set_mset_def count_A by (auto simp: g_def)
eberlm@63534
   723
  with assms have prime: "prime x" if "x \<in># A" for x using that by auto
eberlm@63534
   724
  from set_mset_A assms have "(\<Prod>p \<in> S. p ^ f p) = (\<Prod>p \<in> S. p ^ g p) "
nipkow@64272
   725
    by (intro prod.cong) (auto simp: g_def)
eberlm@63534
   726
  also from set_mset_A assms have "\<dots> = (\<Prod>p \<in> set_mset A. p ^ g p)"
nipkow@64272
   727
    by (intro prod.mono_neutral_right) (auto simp: g_def set_mset_A)
nipkow@63830
   728
  also have "\<dots> = prod_mset A"
nipkow@64272
   729
    by (auto simp: prod_mset_multiplicity count_A set_mset_A intro!: prod.cong)
nipkow@63830
   730
  also from assms have "multiplicity p \<dots> = sum_mset (image_mset (multiplicity p) A)"
nipkow@63830
   731
    by (subst prime_elem_multiplicity_prod_mset_distrib) (auto dest: prime)
eberlm@63534
   732
  also from assms have "image_mset (multiplicity p) A = image_mset (\<lambda>x. if x = p then 1 else 0) A"
eberlm@63534
   733
    by (intro image_mset_cong) (auto simp: prime_multiplicity_other dest: prime)
nipkow@63830
   734
  also have "sum_mset \<dots> = (if p \<in> S then f p else 0)" by (simp add: sum_mset_delta count_A g_def)
eberlm@63534
   735
  finally show ?thesis .
eberlm@63534
   736
qed
eberlm@63534
   737
haftmann@63904
   738
lemma prime_factorization_prod_mset:
haftmann@63904
   739
  assumes "0 \<notin># A"
haftmann@63904
   740
  shows "prime_factorization (prod_mset A) = \<Union>#(image_mset prime_factorization A)"
haftmann@63904
   741
  using assms by (induct A) (auto simp add: prime_factorization_mult)
haftmann@63904
   742
nipkow@64272
   743
lemma prime_factors_prod:
haftmann@63904
   744
  assumes "finite A" and "0 \<notin> f ` A"
nipkow@64272
   745
  shows "prime_factors (prod f A) = UNION A (prime_factors \<circ> f)"
nipkow@64272
   746
  using assms by (simp add: prod_unfold_prod_mset prime_factorization_prod_mset)
haftmann@63904
   747
haftmann@63904
   748
lemma prime_factors_fact:
haftmann@63904
   749
  "prime_factors (fact n) = {p \<in> {2..n}. prime p}" (is "?M = ?N")
haftmann@63904
   750
proof (rule set_eqI)
haftmann@63904
   751
  fix p
haftmann@63904
   752
  { fix m :: nat
haftmann@63904
   753
    assume "p \<in> prime_factors m"
haftmann@63904
   754
    then have "prime p" and "p dvd m" by auto
haftmann@63904
   755
    moreover assume "m > 0" 
haftmann@63904
   756
    ultimately have "2 \<le> p" and "p \<le> m"
haftmann@63904
   757
      by (auto intro: prime_ge_2_nat dest: dvd_imp_le)
haftmann@63904
   758
    moreover assume "m \<le> n"
haftmann@63904
   759
    ultimately have "2 \<le> p" and "p \<le> n"
haftmann@63904
   760
      by (auto intro: order_trans)
haftmann@63904
   761
  } note * = this
haftmann@63904
   762
  show "p \<in> ?M \<longleftrightarrow> p \<in> ?N"
nipkow@64272
   763
    by (auto simp add: fact_prod prime_factors_prod Suc_le_eq dest!: prime_prime_factors intro: *)
haftmann@63904
   764
qed
haftmann@63904
   765
eberlm@63766
   766
lemma prime_dvd_fact_iff:
eberlm@63766
   767
  assumes "prime p"
haftmann@63904
   768
  shows "p dvd fact n \<longleftrightarrow> p \<le> n"
haftmann@63904
   769
  using assms
haftmann@63904
   770
  by (auto simp add: prime_factorization_subset_iff_dvd [symmetric]
haftmann@63905
   771
    prime_factorization_prime prime_factors_fact prime_ge_2_nat)
eberlm@63766
   772
eberlm@63534
   773
(* TODO Legacy names *)
eberlm@63633
   774
lemmas prime_imp_coprime_nat = prime_imp_coprime[where ?'a = nat]
eberlm@63633
   775
lemmas prime_imp_coprime_int = prime_imp_coprime[where ?'a = int]
eberlm@63633
   776
lemmas prime_dvd_mult_nat = prime_dvd_mult_iff[where ?'a = nat]
eberlm@63633
   777
lemmas prime_dvd_mult_int = prime_dvd_mult_iff[where ?'a = int]
eberlm@63633
   778
lemmas prime_dvd_mult_eq_nat = prime_dvd_mult_iff[where ?'a = nat]
eberlm@63633
   779
lemmas prime_dvd_mult_eq_int = prime_dvd_mult_iff[where ?'a = int]
eberlm@63633
   780
lemmas prime_dvd_power_nat = prime_dvd_power[where ?'a = nat]
eberlm@63633
   781
lemmas prime_dvd_power_int = prime_dvd_power[where ?'a = int]
eberlm@63633
   782
lemmas prime_dvd_power_nat_iff = prime_dvd_power_iff[where ?'a = nat]
eberlm@63633
   783
lemmas prime_dvd_power_int_iff = prime_dvd_power_iff[where ?'a = int]
eberlm@63633
   784
lemmas prime_imp_power_coprime_nat = prime_imp_power_coprime[where ?'a = nat]
eberlm@63633
   785
lemmas prime_imp_power_coprime_int = prime_imp_power_coprime[where ?'a = int]
eberlm@63534
   786
lemmas primes_coprime_nat = primes_coprime[where ?'a = nat]
eberlm@63534
   787
lemmas primes_coprime_int = primes_coprime[where ?'a = nat]
eberlm@63633
   788
lemmas prime_divprod_pow_nat = prime_elem_divprod_pow[where ?'a = nat]
eberlm@63633
   789
lemmas prime_exp = prime_elem_power_iff[where ?'a = nat]
eberlm@63534
   790
haftmann@65025
   791
text \<open>Code generation\<close>
haftmann@65025
   792
  
haftmann@65025
   793
context
haftmann@65025
   794
begin
haftmann@65025
   795
haftmann@65025
   796
qualified definition prime_nat :: "nat \<Rightarrow> bool"
haftmann@65025
   797
  where [simp, code_abbrev]: "prime_nat = prime"
haftmann@65025
   798
haftmann@65025
   799
lemma prime_nat_naive [code]:
haftmann@65025
   800
  "prime_nat p \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in>{1<..<p}. \<not> n dvd p)"
haftmann@65025
   801
  by (auto simp add: prime_nat_iff')
haftmann@65025
   802
haftmann@65025
   803
qualified definition prime_int :: "int \<Rightarrow> bool"
haftmann@65025
   804
  where [simp, code_abbrev]: "prime_int = prime"
haftmann@65025
   805
haftmann@65025
   806
lemma prime_int_naive [code]:
haftmann@65025
   807
  "prime_int p \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in>{1<..<p}. \<not> n dvd p)"
haftmann@65025
   808
  by (auto simp add: prime_int_iff')
haftmann@65025
   809
haftmann@65025
   810
lemma "prime(997::nat)" by eval
haftmann@65025
   811
haftmann@65025
   812
lemma "prime(997::int)" by eval
haftmann@65025
   813
  
eberlm@63635
   814
end
haftmann@65025
   815
haftmann@65025
   816
end