src/HOL/Number_Theory/Primes.thy
author wenzelm
Tue Jan 17 13:59:10 2017 +0100 (2017-01-17)
changeset 64911 f0e07600de47
parent 64773 223b2ebdda79
child 65025 8c32ce2a01c6
permissions -rw-r--r--
isabelle update_cartouches -c -t;
     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 subsection\<open>Largest exponent of a prime factor\<close>
   199 text\<open>Possibly duplicates other material, but avoid the complexities of multisets.\<close>
   200   
   201 lemma prime_power_cancel_less:
   202   assumes "prime p" and eq: "m * (p ^ k) = m' * (p ^ k')" and less: "k < k'" and "\<not> p dvd m"
   203   shows False
   204 proof -
   205   obtain l where l: "k' = k + l" and "l > 0"
   206     using less less_imp_add_positive by auto
   207   have "m = m * (p ^ k) div (p ^ k)"
   208     using \<open>prime p\<close> by simp
   209   also have "\<dots> = m' * (p ^ k') div (p ^ k)"
   210     using eq by simp
   211   also have "\<dots> = m' * (p ^ l) * (p ^ k) div (p ^ k)"
   212     by (simp add: l mult.commute mult.left_commute power_add)
   213   also have "... = m' * (p ^ l)"
   214     using \<open>prime p\<close> by simp
   215   finally have "p dvd m"
   216     using \<open>l > 0\<close> by simp
   217   with assms show False
   218     by simp
   219 qed
   220 
   221 lemma prime_power_cancel:
   222   assumes "prime p" and eq: "m * (p ^ k) = m' * (p ^ k')" and "\<not> p dvd m" "\<not> p dvd m'"
   223   shows "k = k'"
   224   using prime_power_cancel_less [OF \<open>prime p\<close>] assms
   225   by (metis linorder_neqE_nat)
   226 
   227 lemma prime_power_cancel2:
   228   assumes "prime p" "m * (p ^ k) = m' * (p ^ k')" "\<not> p dvd m" "\<not> p dvd m'"
   229   obtains "m = m'" "k = k'"
   230   using prime_power_cancel [OF assms] assms by auto
   231 
   232 lemma prime_power_canonical:
   233   fixes m::nat
   234   assumes "prime p" "m > 0"
   235   shows "\<exists>k n. \<not> p dvd n \<and> m = n * p^k"
   236 using \<open>m > 0\<close>
   237 proof (induction m rule: less_induct)
   238   case (less m)
   239   show ?case
   240   proof (cases "p dvd m")
   241     case True
   242     then obtain m' where m': "m = p * m'"
   243       using dvdE by blast
   244     with \<open>prime p\<close> have "0 < m'" "m' < m"
   245       using less.prems prime_nat_iff by auto
   246     with m' less show ?thesis
   247       by (metis power_Suc mult.left_commute)
   248   next
   249     case False
   250     then show ?thesis
   251       by (metis mult.right_neutral power_0)
   252   qed
   253 qed
   254 
   255 
   256 subsubsection \<open>Make prime naively executable\<close>
   257 
   258 lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)"
   259   unfolding One_nat_def [symmetric] by (rule not_prime_1)
   260 
   261 lemma prime_nat_iff':
   262   "prime (p :: nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)"
   263 proof safe
   264   assume "p > 1" and *: "\<forall>n\<in>{1<..<p}. \<not>n dvd p"
   265   show "prime p" unfolding prime_nat_iff
   266   proof (intro conjI allI impI)
   267     fix m assume "m dvd p"
   268     with \<open>p > 1\<close> have "m \<noteq> 0" by (intro notI) auto
   269     hence "m \<ge> 1" by simp
   270     moreover from \<open>m dvd p\<close> and * have "m \<notin> {1<..<p}" by blast
   271     with \<open>m dvd p\<close> and \<open>p > 1\<close> have "m \<le> 1 \<or> m = p" by (auto dest: dvd_imp_le)
   272     ultimately show "m = 1 \<or> m = p" by simp
   273   qed fact+
   274 qed (auto simp: prime_nat_iff)
   275 
   276 lemma prime_nat_code [code_unfold]:
   277   "(prime :: nat \<Rightarrow> bool) = (\<lambda>p. p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p))"
   278   by (rule ext, rule prime_nat_iff')
   279 
   280 lemma prime_int_iff':
   281   "prime (p :: int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)" (is "?lhs = ?rhs")
   282 proof
   283   assume "?lhs"
   284   thus "?rhs" by (auto simp: prime_int_nat_transfer dvd_int_unfold_dvd_nat prime_nat_code)
   285 next
   286   assume "?rhs"
   287   thus "?lhs" by (auto simp: prime_int_nat_transfer zdvd_int prime_nat_code)
   288 qed
   289 
   290 lemma prime_int_code [code_unfold]:
   291   "(prime :: int \<Rightarrow> bool) = (\<lambda>p. p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p))" 
   292   by (rule ext, rule prime_int_iff')
   293 
   294 lemma prime_nat_simp:
   295     "prime p \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..<p]. \<not> n dvd p)"
   296   by (auto simp add: prime_nat_code)
   297 
   298 lemma prime_int_simp:
   299     "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {2..<p}. \<not> n dvd p)"
   300   by (auto simp add: prime_int_code)
   301 
   302 lemma prime_int_numeral_eq [simp]:
   303   "prime (numeral m :: int) \<longleftrightarrow> prime (numeral m :: nat)"
   304   by (simp add: prime_int_nat_transfer)
   305 
   306 lemma two_is_prime_nat [simp]: "prime (2::nat)"
   307   by (simp add: prime_nat_simp)
   308 
   309 lemma prime_nat_numeral_eq [simp]:
   310   "prime (numeral m :: nat) \<longleftrightarrow>
   311     (1::nat) < numeral m \<and>
   312     (\<forall>n::nat\<in>set [2..<numeral m]. \<not> n dvd numeral m)"
   313   by (fact prime_nat_simp) \<comment> \<open>TODO Sieve Of Erathosthenes might speed this up\<close>
   314 
   315 
   316 text\<open>A bit of regression testing:\<close>
   317 
   318 lemma "prime(97::nat)" by simp
   319 lemma "prime(997::nat)" by eval
   320 lemma "prime(97::int)" by simp
   321 lemma "prime(997::int)" by eval
   322 
   323 lemma prime_factor_nat: 
   324   "n \<noteq> (1::nat) \<Longrightarrow> \<exists>p. prime p \<and> p dvd n"
   325   using prime_divisor_exists[of n]
   326   by (cases "n = 0") (auto intro: exI[of _ "2::nat"])
   327 
   328 
   329 subsection \<open>Infinitely many primes\<close>
   330 
   331 lemma next_prime_bound: "\<exists>p::nat. prime p \<and> n < p \<and> p \<le> fact n + 1"
   332 proof-
   333   have f1: "fact n + 1 \<noteq> (1::nat)" using fact_ge_1 [of n, where 'a=nat] by arith
   334   from prime_factor_nat [OF f1]
   335   obtain p :: nat where "prime p" and "p dvd fact n + 1" by auto
   336   then have "p \<le> fact n + 1" apply (intro dvd_imp_le) apply auto done
   337   { assume "p \<le> n"
   338     from \<open>prime p\<close> have "p \<ge> 1"
   339       by (cases p, simp_all)
   340     with \<open>p <= n\<close> have "p dvd fact n"
   341       by (intro dvd_fact)
   342     with \<open>p dvd fact n + 1\<close> have "p dvd fact n + 1 - fact n"
   343       by (rule dvd_diff_nat)
   344     then have "p dvd 1" by simp
   345     then have "p <= 1" by auto
   346     moreover from \<open>prime p\<close> have "p > 1"
   347       using prime_nat_iff by blast
   348     ultimately have False by auto}
   349   then have "n < p" by presburger
   350   with \<open>prime p\<close> and \<open>p <= fact n + 1\<close> show ?thesis by auto
   351 qed
   352 
   353 lemma bigger_prime: "\<exists>p. prime p \<and> p > (n::nat)"
   354   using next_prime_bound by auto
   355 
   356 lemma primes_infinite: "\<not> (finite {(p::nat). prime p})"
   357 proof
   358   assume "finite {(p::nat). prime p}"
   359   with Max_ge have "(EX b. (ALL x : {(p::nat). prime p}. x <= b))"
   360     by auto
   361   then obtain b where "ALL (x::nat). prime x \<longrightarrow> x <= b"
   362     by auto
   363   with bigger_prime [of b] show False
   364     by auto
   365 qed
   366 
   367 subsection\<open>Powers of Primes\<close>
   368 
   369 text\<open>Versions for type nat only\<close>
   370 
   371 lemma prime_product:
   372   fixes p::nat
   373   assumes "prime (p * q)"
   374   shows "p = 1 \<or> q = 1"
   375 proof -
   376   from assms have
   377     "1 < p * q" and P: "\<And>m. m dvd p * q \<Longrightarrow> m = 1 \<or> m = p * q"
   378     unfolding prime_nat_iff by auto
   379   from \<open>1 < p * q\<close> have "p \<noteq> 0" by (cases p) auto
   380   then have Q: "p = p * q \<longleftrightarrow> q = 1" by auto
   381   have "p dvd p * q" by simp
   382   then have "p = 1 \<or> p = p * q" by (rule P)
   383   then show ?thesis by (simp add: Q)
   384 qed
   385 
   386 (* TODO: Generalise? *)
   387 lemma prime_power_mult_nat:
   388   fixes p::nat
   389   assumes p: "prime p" and xy: "x * y = p ^ k"
   390   shows "\<exists>i j. x = p ^i \<and> y = p^ j"
   391 using xy
   392 proof(induct k arbitrary: x y)
   393   case 0 thus ?case apply simp by (rule exI[where x="0"], simp)
   394 next
   395   case (Suc k x y)
   396   from Suc.prems have pxy: "p dvd x*y" by auto
   397   from prime_dvd_multD [OF p pxy] have pxyc: "p dvd x \<or> p dvd y" .
   398   from p have p0: "p \<noteq> 0" by - (rule ccontr, simp)
   399   {assume px: "p dvd x"
   400     then obtain d where d: "x = p*d" unfolding dvd_def by blast
   401     from Suc.prems d  have "p*d*y = p^Suc k" by simp
   402     hence th: "d*y = p^k" using p0 by simp
   403     from Suc.hyps[OF th] obtain i j where ij: "d = p^i" "y = p^j" by blast
   404     with d have "x = p^Suc i" by simp
   405     with ij(2) have ?case by blast}
   406   moreover
   407   {assume px: "p dvd y"
   408     then obtain d where d: "y = p*d" unfolding dvd_def by blast
   409     from Suc.prems d  have "p*d*x = p^Suc k" by (simp add: mult.commute)
   410     hence th: "d*x = p^k" using p0 by simp
   411     from Suc.hyps[OF th] obtain i j where ij: "d = p^i" "x = p^j" by blast
   412     with d have "y = p^Suc i" by simp
   413     with ij(2) have ?case by blast}
   414   ultimately show ?case  using pxyc by blast
   415 qed
   416 
   417 lemma prime_power_exp_nat:
   418   fixes p::nat
   419   assumes p: "prime p" and n: "n \<noteq> 0"
   420     and xn: "x^n = p^k" shows "\<exists>i. x = p^i"
   421   using n xn
   422 proof(induct n arbitrary: k)
   423   case 0 thus ?case by simp
   424 next
   425   case (Suc n k) hence th: "x*x^n = p^k" by simp
   426   {assume "n = 0" with Suc have ?case by simp (rule exI[where x="k"], simp)}
   427   moreover
   428   {assume n: "n \<noteq> 0"
   429     from prime_power_mult_nat[OF p th]
   430     obtain i j where ij: "x = p^i" "x^n = p^j"by blast
   431     from Suc.hyps[OF n ij(2)] have ?case .}
   432   ultimately show ?case by blast
   433 qed
   434 
   435 lemma divides_primepow_nat:
   436   fixes p::nat
   437   assumes p: "prime p"
   438   shows "d dvd p^k \<longleftrightarrow> (\<exists> i. i \<le> k \<and> d = p ^i)"
   439 proof
   440   assume H: "d dvd p^k" then obtain e where e: "d*e = p^k"
   441     unfolding dvd_def  apply (auto simp add: mult.commute) by blast
   442   from prime_power_mult_nat[OF p e] obtain i j where ij: "d = p^i" "e=p^j" by blast
   443   from e ij have "p^(i + j) = p^k" by (simp add: power_add)
   444   hence "i + j = k" using p prime_gt_1_nat power_inject_exp[of p "i+j" k] by simp
   445   hence "i \<le> k" by arith
   446   with ij(1) show "\<exists>i\<le>k. d = p ^ i" by blast
   447 next
   448   {fix i assume H: "i \<le> k" "d = p^i"
   449     then obtain j where j: "k = i + j"
   450       by (metis le_add_diff_inverse)
   451     hence "p^k = p^j*d" using H(2) by (simp add: power_add)
   452     hence "d dvd p^k" unfolding dvd_def by auto}
   453   thus "\<exists>i\<le>k. d = p ^ i \<Longrightarrow> d dvd p ^ k" by blast
   454 qed
   455 
   456 
   457 subsection \<open>Chinese Remainder Theorem Variants\<close>
   458 
   459 lemma bezout_gcd_nat:
   460   fixes a::nat shows "\<exists>x y. a * x - b * y = gcd a b \<or> b * x - a * y = gcd a b"
   461   using bezout_nat[of a b]
   462 by (metis bezout_nat diff_add_inverse gcd_add_mult gcd.commute
   463   gcd_nat.right_neutral mult_0)
   464 
   465 lemma gcd_bezout_sum_nat:
   466   fixes a::nat
   467   assumes "a * x + b * y = d"
   468   shows "gcd a b dvd d"
   469 proof-
   470   let ?g = "gcd a b"
   471     have dv: "?g dvd a*x" "?g dvd b * y"
   472       by simp_all
   473     from dvd_add[OF dv] assms
   474     show ?thesis by auto
   475 qed
   476 
   477 
   478 text \<open>A binary form of the Chinese Remainder Theorem.\<close>
   479 
   480 (* TODO: Generalise? *)
   481 lemma chinese_remainder:
   482   fixes a::nat  assumes ab: "coprime a b" and a: "a \<noteq> 0" and b: "b \<noteq> 0"
   483   shows "\<exists>x q1 q2. x = u + q1 * a \<and> x = v + q2 * b"
   484 proof-
   485   from bezout_add_strong_nat[OF a, of b] bezout_add_strong_nat[OF b, of a]
   486   obtain d1 x1 y1 d2 x2 y2 where dxy1: "d1 dvd a" "d1 dvd b" "a * x1 = b * y1 + d1"
   487     and dxy2: "d2 dvd b" "d2 dvd a" "b * x2 = a * y2 + d2" by blast
   488   then have d12: "d1 = 1" "d2 =1"
   489     by (metis ab coprime_nat)+
   490   let ?x = "v * a * x1 + u * b * x2"
   491   let ?q1 = "v * x1 + u * y2"
   492   let ?q2 = "v * y1 + u * x2"
   493   from dxy2(3)[simplified d12] dxy1(3)[simplified d12]
   494   have "?x = u + ?q1 * a" "?x = v + ?q2 * b"
   495     by algebra+
   496   thus ?thesis by blast
   497 qed
   498 
   499 text \<open>Primality\<close>
   500 
   501 lemma coprime_bezout_strong:
   502   fixes a::nat assumes "coprime a b"  "b \<noteq> 1"
   503   shows "\<exists>x y. a * x = b * y + 1"
   504 by (metis assms bezout_nat gcd_nat.left_neutral)
   505 
   506 lemma bezout_prime:
   507   assumes p: "prime p" and pa: "\<not> p dvd a"
   508   shows "\<exists>x y. a*x = Suc (p*y)"
   509 proof -
   510   have ap: "coprime a p"
   511     by (metis gcd.commute p pa prime_imp_coprime)
   512   moreover from p have "p \<noteq> 1" by auto
   513   ultimately have "\<exists>x y. a * x = p * y + 1"
   514     by (rule coprime_bezout_strong)
   515   then show ?thesis by simp    
   516 qed
   517 (* END TODO *)
   518 
   519 
   520 
   521 subsection \<open>Multiplicity and primality for natural numbers and integers\<close>
   522 
   523 lemma prime_factors_gt_0_nat:
   524   "p \<in> prime_factors x \<Longrightarrow> p > (0::nat)"
   525   by (simp add: in_prime_factors_imp_prime prime_gt_0_nat)
   526 
   527 lemma prime_factors_gt_0_int:
   528   "p \<in> prime_factors x \<Longrightarrow> p > (0::int)"
   529   by (simp add: in_prime_factors_imp_prime prime_gt_0_int)
   530 
   531 lemma prime_factors_ge_0_int [elim]: (* FIXME !? *)
   532   fixes n :: int
   533   shows "p \<in> prime_factors n \<Longrightarrow> p \<ge> 0"
   534   by (drule prime_factors_gt_0_int) simp
   535   
   536 lemma prod_mset_prime_factorization_int:
   537   fixes n :: int
   538   assumes "n > 0"
   539   shows   "prod_mset (prime_factorization n) = n"
   540   using assms by (simp add: prod_mset_prime_factorization)
   541 
   542 lemma prime_factorization_exists_nat:
   543   "n > 0 \<Longrightarrow> (\<exists>M. (\<forall>p::nat \<in> set_mset M. prime p) \<and> n = (\<Prod>i \<in># M. i))"
   544   using prime_factorization_exists[of n] by (auto simp: prime_def)
   545 
   546 lemma prod_mset_prime_factorization_nat [simp]: 
   547   "(n::nat) > 0 \<Longrightarrow> prod_mset (prime_factorization n) = n"
   548   by (subst prod_mset_prime_factorization) simp_all
   549 
   550 lemma prime_factorization_nat:
   551     "n > (0::nat) \<Longrightarrow> n = (\<Prod>p \<in> prime_factors n. p ^ multiplicity p n)"
   552   by (simp add: prod_prime_factors)
   553 
   554 lemma prime_factorization_int:
   555     "n > (0::int) \<Longrightarrow> n = (\<Prod>p \<in> prime_factors n. p ^ multiplicity p n)"
   556   by (simp add: prod_prime_factors)
   557 
   558 lemma prime_factorization_unique_nat:
   559   fixes f :: "nat \<Rightarrow> _"
   560   assumes S_eq: "S = {p. 0 < f p}"
   561     and "finite S"
   562     and S: "\<forall>p\<in>S. prime p" "n = (\<Prod>p\<in>S. p ^ f p)"
   563   shows "S = prime_factors n \<and> (\<forall>p. prime p \<longrightarrow> f p = multiplicity p n)"
   564   using assms by (intro prime_factorization_unique'') auto
   565 
   566 lemma prime_factorization_unique_int:
   567   fixes f :: "int \<Rightarrow> _"
   568   assumes S_eq: "S = {p. 0 < f p}"
   569     and "finite S"
   570     and S: "\<forall>p\<in>S. prime p" "abs n = (\<Prod>p\<in>S. p ^ f p)"
   571   shows "S = prime_factors n \<and> (\<forall>p. prime p \<longrightarrow> f p = multiplicity p n)"
   572   using assms by (intro prime_factorization_unique'') auto
   573 
   574 lemma prime_factors_characterization_nat:
   575   "S = {p. 0 < f (p::nat)} \<Longrightarrow>
   576     finite S \<Longrightarrow> \<forall>p\<in>S. prime p \<Longrightarrow> n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> prime_factors n = S"
   577   by (rule prime_factorization_unique_nat [THEN conjunct1, symmetric])
   578 
   579 lemma prime_factors_characterization'_nat:
   580   "finite {p. 0 < f (p::nat)} \<Longrightarrow>
   581     (\<forall>p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow>
   582       prime_factors (\<Prod>p | 0 < f p. p ^ f p) = {p. 0 < f p}"
   583   by (rule prime_factors_characterization_nat) auto
   584 
   585 lemma prime_factors_characterization_int:
   586   "S = {p. 0 < f (p::int)} \<Longrightarrow> finite S \<Longrightarrow>
   587     \<forall>p\<in>S. prime p \<Longrightarrow> abs n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> prime_factors n = S"
   588   by (rule prime_factorization_unique_int [THEN conjunct1, symmetric])
   589 
   590 (* TODO Move *)
   591 lemma abs_prod: "abs (prod f A :: 'a :: linordered_idom) = prod (\<lambda>x. abs (f x)) A"
   592   by (cases "finite A", induction A rule: finite_induct) (simp_all add: abs_mult)
   593 
   594 lemma primes_characterization'_int [rule_format]:
   595   "finite {p. p \<ge> 0 \<and> 0 < f (p::int)} \<Longrightarrow> \<forall>p. 0 < f p \<longrightarrow> prime p \<Longrightarrow>
   596       prime_factors (\<Prod>p | p \<ge> 0 \<and> 0 < f p. p ^ f p) = {p. p \<ge> 0 \<and> 0 < f p}"
   597   by (rule prime_factors_characterization_int) (auto simp: abs_prod prime_ge_0_int)
   598 
   599 lemma multiplicity_characterization_nat:
   600   "S = {p. 0 < f (p::nat)} \<Longrightarrow> finite S \<Longrightarrow> \<forall>p\<in>S. prime p \<Longrightarrow> prime p \<Longrightarrow>
   601     n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> multiplicity p n = f p"
   602   by (frule prime_factorization_unique_nat [of S f n, THEN conjunct2, rule_format, symmetric]) auto
   603 
   604 lemma multiplicity_characterization'_nat: "finite {p. 0 < f (p::nat)} \<longrightarrow>
   605     (\<forall>p. 0 < f p \<longrightarrow> prime p) \<longrightarrow> prime p \<longrightarrow>
   606       multiplicity p (\<Prod>p | 0 < f p. p ^ f p) = f p"
   607   by (intro impI, rule multiplicity_characterization_nat) auto
   608 
   609 lemma multiplicity_characterization_int: "S = {p. 0 < f (p::int)} \<Longrightarrow>
   610     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"
   611   by (frule prime_factorization_unique_int [of S f n, THEN conjunct2, rule_format, symmetric]) 
   612      (auto simp: abs_prod power_abs prime_ge_0_int intro!: prod.cong)
   613 
   614 lemma multiplicity_characterization'_int [rule_format]:
   615   "finite {p. p \<ge> 0 \<and> 0 < f (p::int)} \<Longrightarrow>
   616     (\<forall>p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow> prime p \<Longrightarrow>
   617       multiplicity p (\<Prod>p | p \<ge> 0 \<and> 0 < f p. p ^ f p) = f p"
   618   by (rule multiplicity_characterization_int) (auto simp: prime_ge_0_int)
   619 
   620 lemma multiplicity_one_nat [simp]: "multiplicity p (Suc 0) = 0"
   621   unfolding One_nat_def [symmetric] by (rule multiplicity_one)
   622 
   623 lemma multiplicity_eq_nat:
   624   fixes x and y::nat
   625   assumes "x > 0" "y > 0" "\<And>p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
   626   shows "x = y"
   627   using multiplicity_eq_imp_eq[of x y] assms by simp
   628 
   629 lemma multiplicity_eq_int:
   630   fixes x y :: int
   631   assumes "x > 0" "y > 0" "\<And>p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
   632   shows "x = y"
   633   using multiplicity_eq_imp_eq[of x y] assms by simp
   634 
   635 lemma multiplicity_prod_prime_powers:
   636   assumes "finite S" "\<And>x. x \<in> S \<Longrightarrow> prime x" "prime p"
   637   shows   "multiplicity p (\<Prod>p \<in> S. p ^ f p) = (if p \<in> S then f p else 0)"
   638 proof -
   639   define g where "g = (\<lambda>x. if x \<in> S then f x else 0)"
   640   define A where "A = Abs_multiset g"
   641   have "{x. g x > 0} \<subseteq> S" by (auto simp: g_def)
   642   from finite_subset[OF this assms(1)] have [simp]: "g :  multiset"
   643     by (simp add: multiset_def)
   644   from assms have count_A: "count A x = g x" for x unfolding A_def
   645     by simp
   646   have set_mset_A: "set_mset A = {x\<in>S. f x > 0}"
   647     unfolding set_mset_def count_A by (auto simp: g_def)
   648   with assms have prime: "prime x" if "x \<in># A" for x using that by auto
   649   from set_mset_A assms have "(\<Prod>p \<in> S. p ^ f p) = (\<Prod>p \<in> S. p ^ g p) "
   650     by (intro prod.cong) (auto simp: g_def)
   651   also from set_mset_A assms have "\<dots> = (\<Prod>p \<in> set_mset A. p ^ g p)"
   652     by (intro prod.mono_neutral_right) (auto simp: g_def set_mset_A)
   653   also have "\<dots> = prod_mset A"
   654     by (auto simp: prod_mset_multiplicity count_A set_mset_A intro!: prod.cong)
   655   also from assms have "multiplicity p \<dots> = sum_mset (image_mset (multiplicity p) A)"
   656     by (subst prime_elem_multiplicity_prod_mset_distrib) (auto dest: prime)
   657   also from assms have "image_mset (multiplicity p) A = image_mset (\<lambda>x. if x = p then 1 else 0) A"
   658     by (intro image_mset_cong) (auto simp: prime_multiplicity_other dest: prime)
   659   also have "sum_mset \<dots> = (if p \<in> S then f p else 0)" by (simp add: sum_mset_delta count_A g_def)
   660   finally show ?thesis .
   661 qed
   662 
   663 lemma prime_factorization_prod_mset:
   664   assumes "0 \<notin># A"
   665   shows "prime_factorization (prod_mset A) = \<Union>#(image_mset prime_factorization A)"
   666   using assms by (induct A) (auto simp add: prime_factorization_mult)
   667 
   668 lemma prime_factors_prod:
   669   assumes "finite A" and "0 \<notin> f ` A"
   670   shows "prime_factors (prod f A) = UNION A (prime_factors \<circ> f)"
   671   using assms by (simp add: prod_unfold_prod_mset prime_factorization_prod_mset)
   672 
   673 lemma prime_factors_fact:
   674   "prime_factors (fact n) = {p \<in> {2..n}. prime p}" (is "?M = ?N")
   675 proof (rule set_eqI)
   676   fix p
   677   { fix m :: nat
   678     assume "p \<in> prime_factors m"
   679     then have "prime p" and "p dvd m" by auto
   680     moreover assume "m > 0" 
   681     ultimately have "2 \<le> p" and "p \<le> m"
   682       by (auto intro: prime_ge_2_nat dest: dvd_imp_le)
   683     moreover assume "m \<le> n"
   684     ultimately have "2 \<le> p" and "p \<le> n"
   685       by (auto intro: order_trans)
   686   } note * = this
   687   show "p \<in> ?M \<longleftrightarrow> p \<in> ?N"
   688     by (auto simp add: fact_prod prime_factors_prod Suc_le_eq dest!: prime_prime_factors intro: *)
   689 qed
   690 
   691 lemma prime_dvd_fact_iff:
   692   assumes "prime p"
   693   shows "p dvd fact n \<longleftrightarrow> p \<le> n"
   694   using assms
   695   by (auto simp add: prime_factorization_subset_iff_dvd [symmetric]
   696     prime_factorization_prime prime_factors_fact prime_ge_2_nat)
   697 
   698 (* TODO Legacy names *)
   699 lemmas prime_imp_coprime_nat = prime_imp_coprime[where ?'a = nat]
   700 lemmas prime_imp_coprime_int = prime_imp_coprime[where ?'a = int]
   701 lemmas prime_dvd_mult_nat = prime_dvd_mult_iff[where ?'a = nat]
   702 lemmas prime_dvd_mult_int = prime_dvd_mult_iff[where ?'a = int]
   703 lemmas prime_dvd_mult_eq_nat = prime_dvd_mult_iff[where ?'a = nat]
   704 lemmas prime_dvd_mult_eq_int = prime_dvd_mult_iff[where ?'a = int]
   705 lemmas prime_dvd_power_nat = prime_dvd_power[where ?'a = nat]
   706 lemmas prime_dvd_power_int = prime_dvd_power[where ?'a = int]
   707 lemmas prime_dvd_power_nat_iff = prime_dvd_power_iff[where ?'a = nat]
   708 lemmas prime_dvd_power_int_iff = prime_dvd_power_iff[where ?'a = int]
   709 lemmas prime_imp_power_coprime_nat = prime_imp_power_coprime[where ?'a = nat]
   710 lemmas prime_imp_power_coprime_int = prime_imp_power_coprime[where ?'a = int]
   711 lemmas primes_coprime_nat = primes_coprime[where ?'a = nat]
   712 lemmas primes_coprime_int = primes_coprime[where ?'a = nat]
   713 lemmas prime_divprod_pow_nat = prime_elem_divprod_pow[where ?'a = nat]
   714 lemmas prime_exp = prime_elem_power_iff[where ?'a = nat]
   715 
   716 end