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