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