src/HOL/Number_Theory/Primes.thy
author nipkow
Mon Oct 17 11:46:22 2016 +0200 (2016-10-17)
changeset 64267 b9a1486e79be
parent 63905 1c3dcb5fe6cb
child 64272 f76b6dda2e56
permissions -rw-r--r--
setsum -> sum
     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: in_prime_factors_imp_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: in_prime_factors_imp_prime prime_gt_0_int)
   466 
   467 lemma prime_factors_ge_0_int [elim]: (* FIXME !? *)
   468   fixes n :: int
   469   shows "p \<in> prime_factors n \<Longrightarrow> p \<ge> 0"
   470   by (drule prime_factors_gt_0_int) simp
   471   
   472 lemma prod_mset_prime_factorization_int:
   473   fixes n :: int
   474   assumes "n > 0"
   475   shows   "prod_mset (prime_factorization n) = n"
   476   using assms by (simp add: prod_mset_prime_factorization)
   477 
   478 lemma prime_factorization_exists_nat:
   479   "n > 0 \<Longrightarrow> (\<exists>M. (\<forall>p::nat \<in> set_mset M. prime p) \<and> n = (\<Prod>i \<in># M. i))"
   480   using prime_factorization_exists[of n] by (auto simp: prime_def)
   481 
   482 lemma prod_mset_prime_factorization_nat [simp]: 
   483   "(n::nat) > 0 \<Longrightarrow> prod_mset (prime_factorization n) = n"
   484   by (subst prod_mset_prime_factorization) simp_all
   485 
   486 lemma prime_factorization_nat:
   487     "n > (0::nat) \<Longrightarrow> n = (\<Prod>p \<in> prime_factors n. p ^ multiplicity p n)"
   488   by (simp add: setprod_prime_factors)
   489 
   490 lemma prime_factorization_int:
   491     "n > (0::int) \<Longrightarrow> n = (\<Prod>p \<in> prime_factors n. p ^ multiplicity p n)"
   492   by (simp add: setprod_prime_factors)
   493 
   494 lemma prime_factorization_unique_nat:
   495   fixes f :: "nat \<Rightarrow> _"
   496   assumes S_eq: "S = {p. 0 < f p}"
   497     and "finite S"
   498     and S: "\<forall>p\<in>S. prime p" "n = (\<Prod>p\<in>S. p ^ f p)"
   499   shows "S = prime_factors n \<and> (\<forall>p. prime p \<longrightarrow> f p = multiplicity p n)"
   500   using assms by (intro prime_factorization_unique'') auto
   501 
   502 lemma prime_factorization_unique_int:
   503   fixes f :: "int \<Rightarrow> _"
   504   assumes S_eq: "S = {p. 0 < f p}"
   505     and "finite S"
   506     and S: "\<forall>p\<in>S. prime p" "abs n = (\<Prod>p\<in>S. p ^ f p)"
   507   shows "S = prime_factors n \<and> (\<forall>p. prime p \<longrightarrow> f p = multiplicity p n)"
   508   using assms by (intro prime_factorization_unique'') auto
   509 
   510 lemma prime_factors_characterization_nat:
   511   "S = {p. 0 < f (p::nat)} \<Longrightarrow>
   512     finite S \<Longrightarrow> \<forall>p\<in>S. prime p \<Longrightarrow> n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> prime_factors n = S"
   513   by (rule prime_factorization_unique_nat [THEN conjunct1, symmetric])
   514 
   515 lemma prime_factors_characterization'_nat:
   516   "finite {p. 0 < f (p::nat)} \<Longrightarrow>
   517     (\<forall>p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow>
   518       prime_factors (\<Prod>p | 0 < f p. p ^ f p) = {p. 0 < f p}"
   519   by (rule prime_factors_characterization_nat) auto
   520 
   521 lemma prime_factors_characterization_int:
   522   "S = {p. 0 < f (p::int)} \<Longrightarrow> finite S \<Longrightarrow>
   523     \<forall>p\<in>S. prime p \<Longrightarrow> abs n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> prime_factors n = S"
   524   by (rule prime_factorization_unique_int [THEN conjunct1, symmetric])
   525 
   526 (* TODO Move *)
   527 lemma abs_setprod: "abs (setprod f A :: 'a :: linordered_idom) = setprod (\<lambda>x. abs (f x)) A"
   528   by (cases "finite A", induction A rule: finite_induct) (simp_all add: abs_mult)
   529 
   530 lemma primes_characterization'_int [rule_format]:
   531   "finite {p. p \<ge> 0 \<and> 0 < f (p::int)} \<Longrightarrow> \<forall>p. 0 < f p \<longrightarrow> prime p \<Longrightarrow>
   532       prime_factors (\<Prod>p | p \<ge> 0 \<and> 0 < f p. p ^ f p) = {p. p \<ge> 0 \<and> 0 < f p}"
   533   by (rule prime_factors_characterization_int) (auto simp: abs_setprod prime_ge_0_int)
   534 
   535 lemma multiplicity_characterization_nat:
   536   "S = {p. 0 < f (p::nat)} \<Longrightarrow> finite S \<Longrightarrow> \<forall>p\<in>S. prime p \<Longrightarrow> prime p \<Longrightarrow>
   537     n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> multiplicity p n = f p"
   538   by (frule prime_factorization_unique_nat [of S f n, THEN conjunct2, rule_format, symmetric]) auto
   539 
   540 lemma multiplicity_characterization'_nat: "finite {p. 0 < f (p::nat)} \<longrightarrow>
   541     (\<forall>p. 0 < f p \<longrightarrow> prime p) \<longrightarrow> prime p \<longrightarrow>
   542       multiplicity p (\<Prod>p | 0 < f p. p ^ f p) = f p"
   543   by (intro impI, rule multiplicity_characterization_nat) auto
   544 
   545 lemma multiplicity_characterization_int: "S = {p. 0 < f (p::int)} \<Longrightarrow>
   546     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"
   547   by (frule prime_factorization_unique_int [of S f n, THEN conjunct2, rule_format, symmetric]) 
   548      (auto simp: abs_setprod power_abs prime_ge_0_int intro!: setprod.cong)
   549 
   550 lemma multiplicity_characterization'_int [rule_format]:
   551   "finite {p. p \<ge> 0 \<and> 0 < f (p::int)} \<Longrightarrow>
   552     (\<forall>p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow> prime p \<Longrightarrow>
   553       multiplicity p (\<Prod>p | p \<ge> 0 \<and> 0 < f p. p ^ f p) = f p"
   554   by (rule multiplicity_characterization_int) (auto simp: prime_ge_0_int)
   555 
   556 lemma multiplicity_one_nat [simp]: "multiplicity p (Suc 0) = 0"
   557   unfolding One_nat_def [symmetric] by (rule multiplicity_one)
   558 
   559 lemma multiplicity_eq_nat:
   560   fixes x and y::nat
   561   assumes "x > 0" "y > 0" "\<And>p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
   562   shows "x = y"
   563   using multiplicity_eq_imp_eq[of x y] assms by simp
   564 
   565 lemma multiplicity_eq_int:
   566   fixes x y :: int
   567   assumes "x > 0" "y > 0" "\<And>p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
   568   shows "x = y"
   569   using multiplicity_eq_imp_eq[of x y] assms by simp
   570 
   571 lemma multiplicity_prod_prime_powers:
   572   assumes "finite S" "\<And>x. x \<in> S \<Longrightarrow> prime x" "prime p"
   573   shows   "multiplicity p (\<Prod>p \<in> S. p ^ f p) = (if p \<in> S then f p else 0)"
   574 proof -
   575   define g where "g = (\<lambda>x. if x \<in> S then f x else 0)"
   576   define A where "A = Abs_multiset g"
   577   have "{x. g x > 0} \<subseteq> S" by (auto simp: g_def)
   578   from finite_subset[OF this assms(1)] have [simp]: "g :  multiset"
   579     by (simp add: multiset_def)
   580   from assms have count_A: "count A x = g x" for x unfolding A_def
   581     by simp
   582   have set_mset_A: "set_mset A = {x\<in>S. f x > 0}"
   583     unfolding set_mset_def count_A by (auto simp: g_def)
   584   with assms have prime: "prime x" if "x \<in># A" for x using that by auto
   585   from set_mset_A assms have "(\<Prod>p \<in> S. p ^ f p) = (\<Prod>p \<in> S. p ^ g p) "
   586     by (intro setprod.cong) (auto simp: g_def)
   587   also from set_mset_A assms have "\<dots> = (\<Prod>p \<in> set_mset A. p ^ g p)"
   588     by (intro setprod.mono_neutral_right) (auto simp: g_def set_mset_A)
   589   also have "\<dots> = prod_mset A"
   590     by (auto simp: prod_mset_multiplicity count_A set_mset_A intro!: setprod.cong)
   591   also from assms have "multiplicity p \<dots> = sum_mset (image_mset (multiplicity p) A)"
   592     by (subst prime_elem_multiplicity_prod_mset_distrib) (auto dest: prime)
   593   also from assms have "image_mset (multiplicity p) A = image_mset (\<lambda>x. if x = p then 1 else 0) A"
   594     by (intro image_mset_cong) (auto simp: prime_multiplicity_other dest: prime)
   595   also have "sum_mset \<dots> = (if p \<in> S then f p else 0)" by (simp add: sum_mset_delta count_A g_def)
   596   finally show ?thesis .
   597 qed
   598 
   599 lemma prime_factorization_prod_mset:
   600   assumes "0 \<notin># A"
   601   shows "prime_factorization (prod_mset A) = \<Union>#(image_mset prime_factorization A)"
   602   using assms by (induct A) (auto simp add: prime_factorization_mult)
   603 
   604 lemma prime_factors_setprod:
   605   assumes "finite A" and "0 \<notin> f ` A"
   606   shows "prime_factors (setprod f A) = UNION A (prime_factors \<circ> f)"
   607   using assms by (simp add: setprod_unfold_prod_mset prime_factorization_prod_mset)
   608 
   609 lemma prime_factors_fact:
   610   "prime_factors (fact n) = {p \<in> {2..n}. prime p}" (is "?M = ?N")
   611 proof (rule set_eqI)
   612   fix p
   613   { fix m :: nat
   614     assume "p \<in> prime_factors m"
   615     then have "prime p" and "p dvd m" by auto
   616     moreover assume "m > 0" 
   617     ultimately have "2 \<le> p" and "p \<le> m"
   618       by (auto intro: prime_ge_2_nat dest: dvd_imp_le)
   619     moreover assume "m \<le> n"
   620     ultimately have "2 \<le> p" and "p \<le> n"
   621       by (auto intro: order_trans)
   622   } note * = this
   623   show "p \<in> ?M \<longleftrightarrow> p \<in> ?N"
   624     by (auto simp add: fact_setprod prime_factors_setprod Suc_le_eq dest!: prime_prime_factors intro: *)
   625 qed
   626 
   627 lemma prime_dvd_fact_iff:
   628   assumes "prime p"
   629   shows "p dvd fact n \<longleftrightarrow> p \<le> n"
   630   using assms
   631   by (auto simp add: prime_factorization_subset_iff_dvd [symmetric]
   632     prime_factorization_prime prime_factors_fact prime_ge_2_nat)
   633 
   634 (* TODO Legacy names *)
   635 lemmas prime_imp_coprime_nat = prime_imp_coprime[where ?'a = nat]
   636 lemmas prime_imp_coprime_int = prime_imp_coprime[where ?'a = int]
   637 lemmas prime_dvd_mult_nat = prime_dvd_mult_iff[where ?'a = nat]
   638 lemmas prime_dvd_mult_int = prime_dvd_mult_iff[where ?'a = int]
   639 lemmas prime_dvd_mult_eq_nat = prime_dvd_mult_iff[where ?'a = nat]
   640 lemmas prime_dvd_mult_eq_int = prime_dvd_mult_iff[where ?'a = int]
   641 lemmas prime_dvd_power_nat = prime_dvd_power[where ?'a = nat]
   642 lemmas prime_dvd_power_int = prime_dvd_power[where ?'a = int]
   643 lemmas prime_dvd_power_nat_iff = prime_dvd_power_iff[where ?'a = nat]
   644 lemmas prime_dvd_power_int_iff = prime_dvd_power_iff[where ?'a = int]
   645 lemmas prime_imp_power_coprime_nat = prime_imp_power_coprime[where ?'a = nat]
   646 lemmas prime_imp_power_coprime_int = prime_imp_power_coprime[where ?'a = int]
   647 lemmas primes_coprime_nat = primes_coprime[where ?'a = nat]
   648 lemmas primes_coprime_int = primes_coprime[where ?'a = nat]
   649 lemmas prime_divprod_pow_nat = prime_elem_divprod_pow[where ?'a = nat]
   650 lemmas prime_exp = prime_elem_power_iff[where ?'a = nat]
   651 
   652 end