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