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