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