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