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