src/HOL/Number_Theory/Primes.thy
changeset 63534 523b488b15c9
parent 62481 b5d8e57826df
child 63535 6887fda4541a
     1.1 --- a/src/HOL/Number_Theory/Primes.thy	Wed Jul 20 14:52:09 2016 +0200
     1.2 +++ b/src/HOL/Number_Theory/Primes.thy	Thu Jul 21 10:06:04 2016 +0200
     1.3 @@ -1,5 +1,6 @@
     1.4  (*  Authors:    Christophe Tabacznyj, Lawrence C. Paulson, Amine Chaieb,
     1.5 -                Thomas M. Rasmussen, Jeremy Avigad, Tobias Nipkow
     1.6 +                Thomas M. Rasmussen, Jeremy Avigad, Tobias Nipkow, 
     1.7 +                Manuel Eberl
     1.8  
     1.9  
    1.10  This file deals with properties of primes. Definitions and lemmas are
    1.11 @@ -22,211 +23,246 @@
    1.12  natural numbers and the integers, and added a number of new theorems.
    1.13  
    1.14  Tobias Nipkow cleaned up a lot.
    1.15 +
    1.16 +Florian Haftmann and Manuel Eberl put primality and prime factorisation
    1.17 +onto an algebraic foundation and thus generalised these concepts to 
    1.18 +other rings, such as polynomials. (see also the Factorial_Ring theory).
    1.19 +
    1.20 +There were also previous formalisations of unique factorisation by 
    1.21 +Thomas Marthedal Rasmussen, Jeremy Avigad, and David Gray.
    1.22  *)
    1.23  
    1.24  
    1.25  section \<open>Primes\<close>
    1.26  
    1.27  theory Primes
    1.28 -imports "~~/src/HOL/GCD" "~~/src/HOL/Binomial"
    1.29 +imports "~~/src/HOL/Binomial" Euclidean_Algorithm
    1.30  begin
    1.31  
    1.32 +(* As a simp or intro rule,
    1.33 +
    1.34 +     prime p \<Longrightarrow> p > 0
    1.35 +
    1.36 +   wreaks havoc here. When the premise includes \<forall>x \<in># M. prime x, it
    1.37 +   leads to the backchaining
    1.38 +
    1.39 +     x > 0
    1.40 +     prime x
    1.41 +     x \<in># M   which is, unfortunately,
    1.42 +     count M x > 0
    1.43 +*)
    1.44 +
    1.45  declare [[coercion int]]
    1.46  declare [[coercion_enabled]]
    1.47  
    1.48 -definition prime :: "nat \<Rightarrow> bool"
    1.49 -  where "prime p = (1 < p \<and> (\<forall>m. m dvd p \<longrightarrow> m = 1 \<or> m = p))"
    1.50 +abbreviation (input) "prime \<equiv> is_prime"
    1.51 +
    1.52 +lemma is_prime_elem_nat_iff:
    1.53 +  "is_prime_elem (n :: nat) \<longleftrightarrow> (1 < n \<and> (\<forall>m. m dvd n \<longrightarrow> m = 1 \<or> m = n))"
    1.54 +proof safe
    1.55 +  assume *: "is_prime_elem n"
    1.56 +  from * have "n \<noteq> 0" "n \<noteq> 1" by (intro notI, simp del: One_nat_def)+
    1.57 +  thus "n > 1" by (cases n) simp_all
    1.58 +  fix m assume m: "m dvd n" "m \<noteq> n"
    1.59 +  from * \<open>m dvd n\<close> have "n dvd m \<or> is_unit m"
    1.60 +    by (intro irreducibleD' prime_imp_irreducible)
    1.61 +  with m show "m = 1" by (auto dest: dvd_antisym)
    1.62 +next
    1.63 +  assume "n > 1" "\<forall>m. m dvd n \<longrightarrow> m = 1 \<or> m = n"
    1.64 +  thus "is_prime_elem n"
    1.65 +    by (auto simp: prime_iff_irreducible irreducible_altdef)
    1.66 +qed
    1.67 +
    1.68 +lemma is_prime_nat_iff_is_prime_elem: "is_prime (n :: nat) \<longleftrightarrow> is_prime_elem n"
    1.69 +  by (simp add: is_prime_def)
    1.70  
    1.71 -subsection \<open>Primes\<close>
    1.72 +lemma is_prime_nat_iff:
    1.73 +  "is_prime (n :: nat) \<longleftrightarrow> (1 < n \<and> (\<forall>m. m dvd n \<longrightarrow> m = 1 \<or> m = n))"
    1.74 +  by (simp add: is_prime_nat_iff_is_prime_elem is_prime_elem_nat_iff)
    1.75  
    1.76 -lemma prime_odd_nat: "prime p \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
    1.77 -  using nat_dvd_1_iff_1 odd_one prime_def by blast
    1.78 +lemma is_prime_elem_int_nat_transfer: "is_prime_elem (n::int) \<longleftrightarrow> is_prime_elem (nat (abs n))"
    1.79 +proof
    1.80 +  assume "is_prime_elem n"
    1.81 +  thus "is_prime_elem (nat (abs n))" by (auto simp: is_prime_elem_def nat_dvd_iff)
    1.82 +next
    1.83 +  assume "is_prime_elem (nat (abs n))"
    1.84 +  thus "is_prime_elem n"
    1.85 +    by (auto simp: dvd_int_unfold_dvd_nat is_prime_elem_def abs_mult nat_mult_distrib)
    1.86 +qed
    1.87 +
    1.88 +lemma is_prime_elem_nat_int_transfer [simp]: "is_prime_elem (int n) \<longleftrightarrow> is_prime_elem n"
    1.89 +  by (auto simp: is_prime_elem_int_nat_transfer)
    1.90 +
    1.91 +lemma is_prime_nat_int_transfer [simp]: "is_prime (int n) \<longleftrightarrow> is_prime n"
    1.92 +  by (auto simp: is_prime_elem_int_nat_transfer is_prime_def)
    1.93 +
    1.94 +lemma is_prime_int_nat_transfer: "is_prime (n::int) \<longleftrightarrow> n \<ge> 0 \<and> is_prime (nat n)"
    1.95 +  by (auto simp: is_prime_elem_int_nat_transfer is_prime_def)
    1.96  
    1.97 -lemma prime_gt_0_nat: "prime p \<Longrightarrow> p > 0"
    1.98 -  unfolding prime_def by auto
    1.99 +lemma is_prime_int_iff:
   1.100 +  "is_prime (n::int) \<longleftrightarrow> (1 < n \<and> (\<forall>m. m \<ge> 0 \<and> m dvd n \<longrightarrow> m = 1 \<or> m = n))"
   1.101 +proof (intro iffI conjI allI impI; (elim conjE)?)
   1.102 +  assume *: "is_prime n"
   1.103 +  hence irred: "irreducible n" by (simp add: prime_imp_irreducible)
   1.104 +  from * have "n \<ge> 0" "n \<noteq> 0" "n \<noteq> 1" 
   1.105 +    by (auto simp: is_prime_def zabs_def not_less split: if_splits)
   1.106 +  thus "n > 1" by presburger
   1.107 +  fix m assume "m dvd n" \<open>m \<ge> 0\<close>
   1.108 +  with irred have "m dvd 1 \<or> n dvd m" by (auto simp: irreducible_altdef)
   1.109 +  with \<open>m dvd n\<close> \<open>m \<ge> 0\<close> \<open>n > 1\<close> show "m = 1 \<or> m = n"
   1.110 +    using associated_iff_dvd[of m n] by auto
   1.111 +next
   1.112 +  assume n: "1 < n" "\<forall>m. m \<ge> 0 \<and> m dvd n \<longrightarrow> m = 1 \<or> m = n"
   1.113 +  hence "nat n > 1" by simp
   1.114 +  moreover have "\<forall>m. m dvd nat n \<longrightarrow> m = 1 \<or> m = nat n"
   1.115 +  proof (intro allI impI)
   1.116 +    fix m assume "m dvd nat n"
   1.117 +    with \<open>n > 1\<close> have "int m dvd n" by (auto simp: int_dvd_iff)
   1.118 +    with n(2) have "int m = 1 \<or> int m = n" by auto
   1.119 +    thus "m = 1 \<or> m = nat n" by auto
   1.120 +  qed
   1.121 +  ultimately show "is_prime n" 
   1.122 +    unfolding is_prime_int_nat_transfer is_prime_nat_iff by auto
   1.123 +qed
   1.124  
   1.125 -lemma prime_ge_1_nat: "prime p \<Longrightarrow> p >= 1"
   1.126 -  unfolding prime_def by auto
   1.127 +
   1.128 +lemma prime_nat_not_dvd:
   1.129 +  assumes "prime p" "p > n" "n \<noteq> (1::nat)"
   1.130 +  shows   "\<not>n dvd p"
   1.131 +proof
   1.132 +  assume "n dvd p"
   1.133 +  from assms(1) have "irreducible p" by (simp add: prime_imp_irreducible)
   1.134 +  from irreducibleD'[OF this \<open>n dvd p\<close>] \<open>n dvd p\<close> \<open>p > n\<close> assms show False
   1.135 +    by (cases "n = 0") (auto dest!: dvd_imp_le)
   1.136 +qed
   1.137  
   1.138 -lemma prime_gt_1_nat: "prime p \<Longrightarrow> p > 1"
   1.139 -  unfolding prime_def by auto
   1.140 +lemma prime_int_not_dvd:
   1.141 +  assumes "prime p" "p > n" "n > (1::int)"
   1.142 +  shows   "\<not>n dvd p"
   1.143 +proof
   1.144 +  assume "n dvd p"
   1.145 +  from assms(1) have "irreducible p" by (simp add: prime_imp_irreducible)
   1.146 +  from irreducibleD'[OF this \<open>n dvd p\<close>] \<open>n dvd p\<close> \<open>p > n\<close> assms show False
   1.147 +    by (auto dest!: zdvd_imp_le)
   1.148 +qed
   1.149 +
   1.150 +lemma prime_odd_nat: "prime p \<Longrightarrow> p > (2::nat) \<Longrightarrow> odd p"
   1.151 +  by (intro prime_nat_not_dvd) auto
   1.152 +
   1.153 +lemma prime_odd_int: "prime p \<Longrightarrow> p > (2::int) \<Longrightarrow> odd p"
   1.154 +  by (intro prime_int_not_dvd) auto
   1.155  
   1.156 -lemma prime_ge_Suc_0_nat: "prime p \<Longrightarrow> p >= Suc 0"
   1.157 -  unfolding prime_def by auto
   1.158 +lemma prime_ge_0_int: "prime p \<Longrightarrow> p \<ge> (0::int)"
   1.159 +  unfolding is_prime_int_iff by auto
   1.160 +
   1.161 +lemma prime_gt_0_nat: "prime p \<Longrightarrow> p > (0::nat)"
   1.162 +  unfolding is_prime_nat_iff by auto
   1.163 +
   1.164 +lemma prime_gt_0_int: "prime p \<Longrightarrow> p > (0::int)"
   1.165 +  unfolding is_prime_int_iff by auto
   1.166 +
   1.167 +lemma prime_ge_1_nat: "prime p \<Longrightarrow> p \<ge> (1::nat)"
   1.168 +  unfolding is_prime_nat_iff by auto
   1.169 +
   1.170 +lemma prime_ge_Suc_0_nat: "prime p \<Longrightarrow> p \<ge> Suc 0"
   1.171 +  unfolding is_prime_nat_iff by auto
   1.172 +
   1.173 +lemma prime_ge_1_int: "prime p \<Longrightarrow> p \<ge> (1::int)"
   1.174 +  unfolding is_prime_int_iff by auto
   1.175 +
   1.176 +lemma prime_gt_1_nat: "prime p \<Longrightarrow> p > (1::nat)"
   1.177 +  unfolding is_prime_nat_iff by auto
   1.178  
   1.179  lemma prime_gt_Suc_0_nat: "prime p \<Longrightarrow> p > Suc 0"
   1.180 -  unfolding prime_def by auto
   1.181 +  unfolding is_prime_nat_iff by auto
   1.182  
   1.183 -lemma prime_ge_2_nat: "prime p \<Longrightarrow> p >= 2"
   1.184 -  unfolding prime_def by auto
   1.185 +lemma prime_gt_1_int: "prime p \<Longrightarrow> p > (1::int)"
   1.186 +  unfolding is_prime_int_iff by auto
   1.187  
   1.188 -lemma prime_imp_coprime_nat: "prime p \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
   1.189 -  apply (unfold prime_def)
   1.190 -  apply (metis gcd_dvd1 gcd_dvd2)
   1.191 -  done
   1.192 +lemma prime_ge_2_nat: "prime p \<Longrightarrow> p \<ge> (2::nat)"
   1.193 +  unfolding is_prime_nat_iff by auto
   1.194 +
   1.195 +lemma prime_ge_2_int: "prime p \<Longrightarrow> p \<ge> (2::int)"
   1.196 +  unfolding is_prime_int_iff by auto
   1.197  
   1.198  lemma prime_int_altdef:
   1.199    "prime p = (1 < p \<and> (\<forall>m::int. m \<ge> 0 \<longrightarrow> m dvd p \<longrightarrow>
   1.200      m = 1 \<or> m = p))"
   1.201 -  apply (simp add: prime_def)
   1.202 -  apply (auto simp add: )
   1.203 -  apply (metis One_nat_def of_nat_1 nat_0_le nat_dvd_iff)
   1.204 -  apply (metis zdvd_int One_nat_def le0 of_nat_0 of_nat_1 of_nat_eq_iff of_nat_le_iff)
   1.205 -  done
   1.206 -
   1.207 -lemma prime_imp_coprime_int:
   1.208 -  fixes n::int shows "prime p \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
   1.209 -  apply (unfold prime_int_altdef)
   1.210 -  apply (metis gcd_dvd1 gcd_dvd2 gcd_ge_0_int)
   1.211 -  done
   1.212 -
   1.213 -lemma prime_dvd_mult_nat: "prime p \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
   1.214 -  by (blast intro: coprime_dvd_mult prime_imp_coprime_nat)
   1.215 -
   1.216 -lemma prime_dvd_mult_int:
   1.217 -  fixes n::int shows "prime p \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
   1.218 -  by (blast intro: coprime_dvd_mult prime_imp_coprime_int)
   1.219 -
   1.220 -lemma prime_dvd_mult_eq_nat [simp]: "prime p \<Longrightarrow>
   1.221 -    p dvd m * n = (p dvd m \<or> p dvd n)"
   1.222 -  by (rule iffI, rule prime_dvd_mult_nat, auto)
   1.223 -
   1.224 -lemma prime_dvd_mult_eq_int [simp]:
   1.225 -  fixes n::int
   1.226 -  shows "prime p \<Longrightarrow> p dvd m * n = (p dvd m \<or> p dvd n)"
   1.227 -  by (rule iffI, rule prime_dvd_mult_int, auto)
   1.228 +  unfolding is_prime_int_iff by blast
   1.229  
   1.230  lemma not_prime_eq_prod_nat:
   1.231 -  "1 < n \<Longrightarrow> \<not> prime n \<Longrightarrow>
   1.232 -    \<exists>m k. n = m * k \<and> 1 < m \<and> m < n \<and> 1 < k \<and> k < n"
   1.233 -  unfolding prime_def dvd_def apply (auto simp add: ac_simps)
   1.234 -  by (metis Suc_lessD Suc_lessI n_less_m_mult_n n_less_n_mult_m nat_0_less_mult_iff)
   1.235 -
   1.236 -lemma prime_dvd_power_nat: "prime p \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x"
   1.237 -  by (induct n) auto
   1.238 -
   1.239 -lemma prime_dvd_power_int:
   1.240 -  fixes x::int shows "prime p \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x"
   1.241 -  by (induct n) auto
   1.242 -
   1.243 -lemma prime_dvd_power_nat_iff: "prime p \<Longrightarrow> n > 0 \<Longrightarrow>
   1.244 -    p dvd x^n \<longleftrightarrow> p dvd x"
   1.245 -  by (cases n) (auto elim: prime_dvd_power_nat)
   1.246 -
   1.247 -lemma prime_dvd_power_int_iff:
   1.248 -  fixes x::int
   1.249 -  shows "prime p \<Longrightarrow> n > 0 \<Longrightarrow> p dvd x^n \<longleftrightarrow> p dvd x"
   1.250 -  by (cases n) (auto elim: prime_dvd_power_int)
   1.251 +  assumes "m > 1" "\<not>prime (m::nat)"
   1.252 +  shows   "\<exists>n k. n = m * k \<and> 1 < m \<and> m < n \<and> 1 < k \<and> k < n"
   1.253 +  using assms irreducible_altdef[of m]
   1.254 +  by (auto simp: prime_iff_irreducible is_prime_def irreducible_altdef)
   1.255  
   1.256  
   1.257  subsubsection \<open>Make prime naively executable\<close>
   1.258  
   1.259 -lemma zero_not_prime_nat [simp]: "~prime (0::nat)"
   1.260 -  by (simp add: prime_def)
   1.261 -
   1.262 -lemma one_not_prime_nat [simp]: "~prime (1::nat)"
   1.263 -  by (simp add: prime_def)
   1.264 +lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)"
   1.265 +  unfolding One_nat_def [symmetric] by (rule not_is_prime_1)
   1.266  
   1.267 -lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)"
   1.268 -  by (simp add: prime_def)
   1.269 +lemma prime_nat_code [code_unfold]:
   1.270 +  "prime (p::nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)"
   1.271 +proof safe
   1.272 +  assume "p > 1" and *: "\<forall>n\<in>{1<..<p}. \<not>n dvd p"
   1.273 +  show "is_prime p" unfolding is_prime_nat_iff
   1.274 +  proof (intro conjI allI impI)
   1.275 +    fix m assume "m dvd p"
   1.276 +    with \<open>p > 1\<close> have "m \<noteq> 0" by (intro notI) auto
   1.277 +    hence "m \<ge> 1" by simp
   1.278 +    moreover from \<open>m dvd p\<close> and * have "m \<notin> {1<..<p}" by blast
   1.279 +    with \<open>m dvd p\<close> and \<open>p > 1\<close> have "m \<le> 1 \<or> m = p" by (auto dest: dvd_imp_le)
   1.280 +    ultimately show "m = 1 \<or> m = p" by simp
   1.281 +  qed fact+
   1.282 +qed (auto simp: is_prime_nat_iff)
   1.283  
   1.284 -lemma prime_nat_code [code]:
   1.285 -    "prime p \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)"
   1.286 -  apply (simp add: Ball_def)
   1.287 -  apply (metis One_nat_def less_not_refl prime_def dvd_triv_right not_prime_eq_prod_nat)
   1.288 -  done
   1.289 +lemma prime_int_code [code_unfold]:
   1.290 +  "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)" (is "?lhs \<longleftrightarrow> ?rhs")
   1.291 +proof
   1.292 +  assume "?lhs"
   1.293 +  thus "?rhs" by (auto simp: is_prime_int_nat_transfer dvd_int_unfold_dvd_nat prime_nat_code)
   1.294 +next
   1.295 +  assume "?rhs"
   1.296 +  thus "?lhs" by (auto simp: is_prime_int_nat_transfer zdvd_int prime_nat_code)
   1.297 +qed
   1.298  
   1.299  lemma prime_nat_simp:
   1.300      "prime p \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..<p]. \<not> n dvd p)"
   1.301    by (auto simp add: prime_nat_code)
   1.302  
   1.303 +lemma prime_int_simp:
   1.304 +    "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {2..<p}. \<not> n dvd p)"
   1.305 +  by (auto simp add: prime_int_code)
   1.306 +
   1.307  lemmas prime_nat_simp_numeral [simp] = prime_nat_simp [of "numeral m"] for m
   1.308  
   1.309  lemma two_is_prime_nat [simp]: "prime (2::nat)"
   1.310    by simp
   1.311  
   1.312 +declare is_prime_int_nat_transfer[of "numeral m" for m, simp]
   1.313 +
   1.314 +
   1.315  text\<open>A bit of regression testing:\<close>
   1.316  
   1.317  lemma "prime(97::nat)" by simp
   1.318  lemma "prime(997::nat)" by eval
   1.319 -
   1.320 -
   1.321 -lemma prime_imp_power_coprime_nat: "prime p \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
   1.322 -  by (metis coprime_exp gcd.commute prime_imp_coprime_nat)
   1.323 -
   1.324 -lemma prime_imp_power_coprime_int:
   1.325 -  fixes a::int shows "prime p \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
   1.326 -  by (metis coprime_exp gcd.commute prime_imp_coprime_int)
   1.327 -
   1.328 -lemma primes_coprime_nat: "prime p \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
   1.329 -  by (metis gcd_nat.absorb1 gcd_nat.absorb2 prime_imp_coprime_nat)
   1.330 -
   1.331 -lemma primes_imp_powers_coprime_nat:
   1.332 -    "prime p \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
   1.333 -  by (rule coprime_exp2_nat, rule primes_coprime_nat)
   1.334 -
   1.335 -lemma prime_factor_nat:
   1.336 -  "n \<noteq> (1::nat) \<Longrightarrow> \<exists>p. prime p \<and> p dvd n"
   1.337 -proof (induct n rule: nat_less_induct)
   1.338 -  case (1 n) show ?case
   1.339 -  proof (cases "n = 0")
   1.340 -    case True then show ?thesis
   1.341 -    by (auto intro: two_is_prime_nat)
   1.342 -  next
   1.343 -    case False with "1.prems" have "n > 1" by simp
   1.344 -    with "1.hyps" show ?thesis
   1.345 -    by (metis One_nat_def dvd_mult dvd_refl not_prime_eq_prod_nat order_less_irrefl)
   1.346 -  qed
   1.347 -qed
   1.348 -
   1.349 -text \<open>One property of coprimality is easier to prove via prime factors.\<close>
   1.350 +lemma "prime(97::int)" by simp
   1.351 +lemma "prime(997::int)" by eval
   1.352  
   1.353 -lemma prime_divprod_pow_nat:
   1.354 -  assumes p: "prime p" and ab: "coprime a b" and pab: "p^n dvd a * b"
   1.355 -  shows "p^n dvd a \<or> p^n dvd b"
   1.356 -proof-
   1.357 -  { assume "n = 0 \<or> a = 1 \<or> b = 1" with pab have ?thesis
   1.358 -      apply (cases "n=0", simp_all)
   1.359 -      apply (cases "a=1", simp_all)
   1.360 -      done }
   1.361 -  moreover
   1.362 -  { assume n: "n \<noteq> 0" and a: "a\<noteq>1" and b: "b\<noteq>1"
   1.363 -    then obtain m where m: "n = Suc m" by (cases n) auto
   1.364 -    from n have "p dvd p^n" apply (intro dvd_power) apply auto done
   1.365 -    also note pab
   1.366 -    finally have pab': "p dvd a * b".
   1.367 -    from prime_dvd_mult_nat[OF p pab']
   1.368 -    have "p dvd a \<or> p dvd b" .
   1.369 -    moreover
   1.370 -    { assume pa: "p dvd a"
   1.371 -      from coprime_common_divisor_nat [OF ab, OF pa] p have "\<not> p dvd b" by auto
   1.372 -      with p have "coprime b p"
   1.373 -        by (subst gcd.commute, intro prime_imp_coprime_nat)
   1.374 -      then have pnb: "coprime (p^n) b"
   1.375 -        by (subst gcd.commute, rule coprime_exp)
   1.376 -      from coprime_dvd_mult[OF pnb pab] have ?thesis by blast }
   1.377 -    moreover
   1.378 -    { assume pb: "p dvd b"
   1.379 -      have pnba: "p^n dvd b*a" using pab by (simp add: mult.commute)
   1.380 -      from coprime_common_divisor_nat [OF ab, of p] pb p have "\<not> p dvd a"
   1.381 -        by auto
   1.382 -      with p have "coprime a p"
   1.383 -        by (subst gcd.commute, intro prime_imp_coprime_nat)
   1.384 -      then have pna: "coprime (p^n) a"
   1.385 -        by (subst gcd.commute, rule coprime_exp)
   1.386 -      from coprime_dvd_mult[OF pna pnba] have ?thesis by blast }
   1.387 -    ultimately have ?thesis by blast }
   1.388 -  ultimately show ?thesis by blast
   1.389 -qed
   1.390 +lemma prime_factor_nat: 
   1.391 +  "n \<noteq> (1::nat) \<Longrightarrow> \<exists>p. prime p \<and> p dvd n"
   1.392 +  using prime_divisor_exists[of n]
   1.393 +  by (cases "n = 0") (auto intro: exI[of _ "2::nat"])
   1.394  
   1.395  
   1.396  subsection \<open>Infinitely many primes\<close>
   1.397  
   1.398 -lemma next_prime_bound: "\<exists>p. prime p \<and> n < p \<and> p <= fact n + 1"
   1.399 +lemma next_prime_bound: "\<exists>p::nat. prime p \<and> n < p \<and> p \<le> fact n + 1"
   1.400  proof-
   1.401    have f1: "fact n + 1 \<noteq> (1::nat)" using fact_ge_1 [of n, where 'a=nat] by arith
   1.402    from prime_factor_nat [OF f1]
   1.403 -  obtain p where "prime p" and "p dvd fact n + 1" by auto
   1.404 +  obtain p :: nat where "prime p" and "p dvd fact n + 1" by auto
   1.405    then have "p \<le> fact n + 1" apply (intro dvd_imp_le) apply auto done
   1.406    { assume "p \<le> n"
   1.407      from \<open>prime p\<close> have "p \<ge> 1"
   1.408 @@ -238,7 +274,7 @@
   1.409      then have "p dvd 1" by simp
   1.410      then have "p <= 1" by auto
   1.411      moreover from \<open>prime p\<close> have "p > 1"
   1.412 -      using prime_def by blast
   1.413 +      using is_prime_nat_iff by blast
   1.414      ultimately have False by auto}
   1.415    then have "n < p" by presburger
   1.416    with \<open>prime p\<close> and \<open>p <= fact n + 1\<close> show ?thesis by auto
   1.417 @@ -269,7 +305,7 @@
   1.418  proof -
   1.419    from assms have
   1.420      "1 < p * q" and P: "\<And>m. m dvd p * q \<Longrightarrow> m = 1 \<or> m = p * q"
   1.421 -    unfolding prime_def by auto
   1.422 +    unfolding is_prime_nat_iff by auto
   1.423    from \<open>1 < p * q\<close> have "p \<noteq> 0" by (cases p) auto
   1.424    then have Q: "p = p * q \<longleftrightarrow> q = 1" by auto
   1.425    have "p dvd p * q" by simp
   1.426 @@ -277,30 +313,8 @@
   1.427    then show ?thesis by (simp add: Q)
   1.428  qed
   1.429  
   1.430 -lemma prime_exp:
   1.431 -  fixes p::nat
   1.432 -  shows "prime (p^n) \<longleftrightarrow> prime p \<and> n = 1"
   1.433 -proof(induct n)
   1.434 -  case 0 thus ?case by simp
   1.435 -next
   1.436 -  case (Suc n)
   1.437 -  {assume "p = 0" hence ?case by simp}
   1.438 -  moreover
   1.439 -  {assume "p=1" hence ?case by simp}
   1.440 -  moreover
   1.441 -  {assume p: "p \<noteq> 0" "p\<noteq>1"
   1.442 -    {assume pp: "prime (p^Suc n)"
   1.443 -      hence "p = 1 \<or> p^n = 1" using prime_product[of p "p^n"] by simp
   1.444 -      with p have n: "n = 0"
   1.445 -        by (metis One_nat_def nat_power_eq_Suc_0_iff)
   1.446 -      with pp have "prime p \<and> Suc n = 1" by simp}
   1.447 -    moreover
   1.448 -    {assume n: "prime p \<and> Suc n = 1" hence "prime (p^Suc n)" by simp}
   1.449 -    ultimately have ?case by blast}
   1.450 -  ultimately show ?case by blast
   1.451 -qed
   1.452 -
   1.453 -lemma prime_power_mult:
   1.454 +(* TODO: Generalise? *)
   1.455 +lemma prime_power_mult_nat:
   1.456    fixes p::nat
   1.457    assumes p: "prime p" and xy: "x * y = p ^ k"
   1.458    shows "\<exists>i j. x = p ^i \<and> y = p^ j"
   1.459 @@ -310,7 +324,7 @@
   1.460  next
   1.461    case (Suc k x y)
   1.462    from Suc.prems have pxy: "p dvd x*y" by auto
   1.463 -  from Primes.prime_dvd_mult_nat [OF p pxy] have pxyc: "p dvd x \<or> p dvd y" .
   1.464 +  from is_prime_dvd_multD [OF p pxy] have pxyc: "p dvd x \<or> p dvd y" .
   1.465    from p have p0: "p \<noteq> 0" by - (rule ccontr, simp)
   1.466    {assume px: "p dvd x"
   1.467      then obtain d where d: "x = p*d" unfolding dvd_def by blast
   1.468 @@ -330,7 +344,7 @@
   1.469    ultimately show ?case  using pxyc by blast
   1.470  qed
   1.471  
   1.472 -lemma prime_power_exp:
   1.473 +lemma prime_power_exp_nat:
   1.474    fixes p::nat
   1.475    assumes p: "prime p" and n: "n \<noteq> 0"
   1.476      and xn: "x^n = p^k" shows "\<exists>i. x = p^i"
   1.477 @@ -342,20 +356,20 @@
   1.478    {assume "n = 0" with Suc have ?case by simp (rule exI[where x="k"], simp)}
   1.479    moreover
   1.480    {assume n: "n \<noteq> 0"
   1.481 -    from prime_power_mult[OF p th]
   1.482 +    from prime_power_mult_nat[OF p th]
   1.483      obtain i j where ij: "x = p^i" "x^n = p^j"by blast
   1.484      from Suc.hyps[OF n ij(2)] have ?case .}
   1.485    ultimately show ?case by blast
   1.486  qed
   1.487  
   1.488 -lemma divides_primepow:
   1.489 +lemma divides_primepow_nat:
   1.490    fixes p::nat
   1.491    assumes p: "prime p"
   1.492    shows "d dvd p^k \<longleftrightarrow> (\<exists> i. i \<le> k \<and> d = p ^i)"
   1.493  proof
   1.494    assume H: "d dvd p^k" then obtain e where e: "d*e = p^k"
   1.495      unfolding dvd_def  apply (auto simp add: mult.commute) by blast
   1.496 -  from prime_power_mult[OF p e] obtain i j where ij: "d = p^i" "e=p^j" by blast
   1.497 +  from prime_power_mult_nat[OF p e] obtain i j where ij: "d = p^i" "e=p^j" by blast
   1.498    from e ij have "p^(i + j) = p^k" by (simp add: power_add)
   1.499    hence "i + j = k" using p prime_gt_1_nat power_inject_exp[of p "i+j" k] by simp
   1.500    hence "i \<le> k" by arith
   1.501 @@ -369,6 +383,7 @@
   1.502    thus "\<exists>i\<le>k. d = p ^ i \<Longrightarrow> d dvd p ^ k" by blast
   1.503  qed
   1.504  
   1.505 +
   1.506  subsection \<open>Chinese Remainder Theorem Variants\<close>
   1.507  
   1.508  lemma bezout_gcd_nat:
   1.509 @@ -392,6 +407,7 @@
   1.510  
   1.511  text \<open>A binary form of the Chinese Remainder Theorem.\<close>
   1.512  
   1.513 +(* TODO: Generalise? *)
   1.514  lemma chinese_remainder:
   1.515    fixes a::nat  assumes ab: "coprime a b" and a: "a \<noteq> 0" and b: "b \<noteq> 0"
   1.516    shows "\<exists>x q1 q2. x = u + q1 * a \<and> x = v + q2 * b"
   1.517 @@ -422,11 +438,175 @@
   1.518    shows "\<exists>x y. a*x = Suc (p*y)"
   1.519  proof -
   1.520    have ap: "coprime a p"
   1.521 -    by (metis gcd.commute p pa prime_imp_coprime_nat)
   1.522 +    by (metis gcd.commute p pa is_prime_imp_coprime)
   1.523    moreover from p have "p \<noteq> 1" by auto
   1.524    ultimately have "\<exists>x y. a * x = p * y + 1"
   1.525      by (rule coprime_bezout_strong)
   1.526    then show ?thesis by simp    
   1.527  qed
   1.528 +(* END TODO *)
   1.529  
   1.530 -end
   1.531 +
   1.532 +
   1.533 +subsection \<open>Multiplicity and primality for natural numbers and integers\<close>
   1.534 +
   1.535 +lemma prime_factors_gt_0_nat:
   1.536 +  "p \<in> prime_factors x \<Longrightarrow> p > (0::nat)"
   1.537 +  by (simp add: prime_factors_prime prime_gt_0_nat)
   1.538 +
   1.539 +lemma prime_factors_gt_0_int:
   1.540 +  "p \<in> prime_factors x \<Longrightarrow> p > (0::int)"
   1.541 +  by (simp add: prime_factors_prime prime_gt_0_int)
   1.542 +
   1.543 +lemma prime_factors_ge_0_int [elim]:
   1.544 +  fixes n :: int
   1.545 +  shows "p \<in> prime_factors n \<Longrightarrow> p \<ge> 0"
   1.546 +  unfolding prime_factors_def 
   1.547 +  by (auto split: if_splits simp: is_prime_def dest!: in_prime_factorization_imp_prime)
   1.548 +
   1.549 +lemma msetprod_prime_factorization_int:
   1.550 +  fixes n :: int
   1.551 +  assumes "n > 0"
   1.552 +  shows   "msetprod (prime_factorization n) = n"
   1.553 +  using assms by (simp add: msetprod_prime_factorization)
   1.554 +
   1.555 +lemma prime_factorization_exists_nat:
   1.556 +  "n > 0 \<Longrightarrow> (\<exists>M. (\<forall>p::nat \<in> set_mset M. prime p) \<and> n = (\<Prod>i \<in># M. i))"
   1.557 +  using prime_factorization_exists[of n] by (auto simp: is_prime_def)
   1.558 +
   1.559 +lemma msetprod_prime_factorization_nat [simp]: 
   1.560 +  "(n::nat) > 0 \<Longrightarrow> msetprod (prime_factorization n) = n"
   1.561 +  by (subst msetprod_prime_factorization) simp_all
   1.562 +
   1.563 +lemma prime_factorization_nat:
   1.564 +    "n > (0::nat) \<Longrightarrow> n = (\<Prod>p \<in> prime_factors n. p ^ multiplicity p n)"
   1.565 +  by (simp add: setprod_prime_factors)
   1.566 +
   1.567 +lemma prime_factorization_int:
   1.568 +    "n > (0::int) \<Longrightarrow> n = (\<Prod>p \<in> prime_factors n. p ^ multiplicity p n)"
   1.569 +  by (simp add: setprod_prime_factors)
   1.570 +
   1.571 +lemma prime_factorization_unique_nat:
   1.572 +  fixes f :: "nat \<Rightarrow> _"
   1.573 +  assumes S_eq: "S = {p. 0 < f p}"
   1.574 +    and "finite S"
   1.575 +    and S: "\<forall>p\<in>S. prime p" "n = (\<Prod>p\<in>S. p ^ f p)"
   1.576 +  shows "S = prime_factors n \<and> (\<forall>p. is_prime p \<longrightarrow> f p = multiplicity p n)"
   1.577 +  using assms by (intro prime_factorization_unique'') auto
   1.578 +
   1.579 +lemma prime_factorization_unique_int:
   1.580 +  fixes f :: "int \<Rightarrow> _"
   1.581 +  assumes S_eq: "S = {p. 0 < f p}"
   1.582 +    and "finite S"
   1.583 +    and S: "\<forall>p\<in>S. prime p" "abs n = (\<Prod>p\<in>S. p ^ f p)"
   1.584 +  shows "S = prime_factors n \<and> (\<forall>p. is_prime p \<longrightarrow> f p = multiplicity p n)"
   1.585 +  using assms by (intro prime_factorization_unique'') auto
   1.586 +
   1.587 +lemma prime_factors_characterization_nat:
   1.588 +  "S = {p. 0 < f (p::nat)} \<Longrightarrow>
   1.589 +    finite S \<Longrightarrow> \<forall>p\<in>S. prime p \<Longrightarrow> n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> prime_factors n = S"
   1.590 +  by (rule prime_factorization_unique_nat [THEN conjunct1, symmetric])
   1.591 +
   1.592 +lemma prime_factors_characterization'_nat:
   1.593 +  "finite {p. 0 < f (p::nat)} \<Longrightarrow>
   1.594 +    (\<forall>p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow>
   1.595 +      prime_factors (\<Prod>p | 0 < f p. p ^ f p) = {p. 0 < f p}"
   1.596 +  by (rule prime_factors_characterization_nat) auto
   1.597 +
   1.598 +lemma prime_factors_characterization_int:
   1.599 +  "S = {p. 0 < f (p::int)} \<Longrightarrow> finite S \<Longrightarrow>
   1.600 +    \<forall>p\<in>S. prime p \<Longrightarrow> abs n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> prime_factors n = S"
   1.601 +  by (rule prime_factorization_unique_int [THEN conjunct1, symmetric])
   1.602 +
   1.603 +(* TODO Move *)
   1.604 +lemma abs_setprod: "abs (setprod f A :: 'a :: linordered_idom) = setprod (\<lambda>x. abs (f x)) A"
   1.605 +  by (cases "finite A", induction A rule: finite_induct) (simp_all add: abs_mult)
   1.606 +
   1.607 +lemma primes_characterization'_int [rule_format]:
   1.608 +  "finite {p. p \<ge> 0 \<and> 0 < f (p::int)} \<Longrightarrow> \<forall>p. 0 < f p \<longrightarrow> prime p \<Longrightarrow>
   1.609 +      prime_factors (\<Prod>p | p \<ge> 0 \<and> 0 < f p. p ^ f p) = {p. p \<ge> 0 \<and> 0 < f p}"
   1.610 +  by (rule prime_factors_characterization_int) (auto simp: abs_setprod prime_ge_0_int)
   1.611 +
   1.612 +lemma multiplicity_characterization_nat:
   1.613 +  "S = {p. 0 < f (p::nat)} \<Longrightarrow> finite S \<Longrightarrow> \<forall>p\<in>S. prime p \<Longrightarrow> is_prime p \<Longrightarrow>
   1.614 +    n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> multiplicity p n = f p"
   1.615 +  by (frule prime_factorization_unique_nat [of S f n, THEN conjunct2, rule_format, symmetric]) auto
   1.616 +
   1.617 +lemma multiplicity_characterization'_nat: "finite {p. 0 < f (p::nat)} \<longrightarrow>
   1.618 +    (\<forall>p. 0 < f p \<longrightarrow> prime p) \<longrightarrow> is_prime p \<longrightarrow>
   1.619 +      multiplicity p (\<Prod>p | 0 < f p. p ^ f p) = f p"
   1.620 +  by (intro impI, rule multiplicity_characterization_nat) auto
   1.621 +
   1.622 +lemma multiplicity_characterization_int: "S = {p. 0 < f (p::int)} \<Longrightarrow>
   1.623 +    finite S \<Longrightarrow> \<forall>p\<in>S. prime p \<Longrightarrow> is_prime p \<Longrightarrow> n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> multiplicity p n = f p"
   1.624 +  by (frule prime_factorization_unique_int [of S f n, THEN conjunct2, rule_format, symmetric]) 
   1.625 +     (auto simp: abs_setprod power_abs prime_ge_0_int intro!: setprod.cong)
   1.626 +
   1.627 +lemma multiplicity_characterization'_int [rule_format]:
   1.628 +  "finite {p. p \<ge> 0 \<and> 0 < f (p::int)} \<Longrightarrow>
   1.629 +    (\<forall>p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow> is_prime p \<Longrightarrow>
   1.630 +      multiplicity p (\<Prod>p | p \<ge> 0 \<and> 0 < f p. p ^ f p) = f p"
   1.631 +  by (rule multiplicity_characterization_int) (auto simp: prime_ge_0_int)
   1.632 +
   1.633 +lemma multiplicity_one_nat [simp]: "multiplicity p (Suc 0) = 0"
   1.634 +  unfolding One_nat_def [symmetric] by (rule multiplicity_one)
   1.635 +
   1.636 +lemma multiplicity_eq_nat:
   1.637 +  fixes x and y::nat
   1.638 +  assumes "x > 0" "y > 0" "\<And>p. is_prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
   1.639 +  shows "x = y"
   1.640 +  using multiplicity_eq_imp_eq[of x y] assms by simp
   1.641 +
   1.642 +lemma multiplicity_eq_int:
   1.643 +  fixes x y :: int
   1.644 +  assumes "x > 0" "y > 0" "\<And>p. is_prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
   1.645 +  shows "x = y"
   1.646 +  using multiplicity_eq_imp_eq[of x y] assms by simp
   1.647 +
   1.648 +lemma multiplicity_prod_prime_powers:
   1.649 +  assumes "finite S" "\<And>x. x \<in> S \<Longrightarrow> is_prime x" "is_prime p"
   1.650 +  shows   "multiplicity p (\<Prod>p \<in> S. p ^ f p) = (if p \<in> S then f p else 0)"
   1.651 +proof -
   1.652 +  define g where "g = (\<lambda>x. if x \<in> S then f x else 0)"
   1.653 +  define A where "A = Abs_multiset g"
   1.654 +  have "{x. g x > 0} \<subseteq> S" by (auto simp: g_def)
   1.655 +  from finite_subset[OF this assms(1)] have [simp]: "g :  multiset"
   1.656 +    by (simp add: multiset_def)
   1.657 +  from assms have count_A: "count A x = g x" for x unfolding A_def
   1.658 +    by simp
   1.659 +  have set_mset_A: "set_mset A = {x\<in>S. f x > 0}"
   1.660 +    unfolding set_mset_def count_A by (auto simp: g_def)
   1.661 +  with assms have prime: "prime x" if "x \<in># A" for x using that by auto
   1.662 +  from set_mset_A assms have "(\<Prod>p \<in> S. p ^ f p) = (\<Prod>p \<in> S. p ^ g p) "
   1.663 +    by (intro setprod.cong) (auto simp: g_def)
   1.664 +  also from set_mset_A assms have "\<dots> = (\<Prod>p \<in> set_mset A. p ^ g p)"
   1.665 +    by (intro setprod.mono_neutral_right) (auto simp: g_def set_mset_A)
   1.666 +  also have "\<dots> = msetprod A"
   1.667 +    by (auto simp: msetprod_multiplicity count_A set_mset_A intro!: setprod.cong)
   1.668 +  also from assms have "multiplicity p \<dots> = msetsum (image_mset (multiplicity p) A)"
   1.669 +    by (subst prime_multiplicity_msetprod_distrib) (auto dest: prime)
   1.670 +  also from assms have "image_mset (multiplicity p) A = image_mset (\<lambda>x. if x = p then 1 else 0) A"
   1.671 +    by (intro image_mset_cong) (auto simp: prime_multiplicity_other dest: prime)
   1.672 +  also have "msetsum \<dots> = (if p \<in> S then f p else 0)" by (simp add: msetsum_delta count_A g_def)
   1.673 +  finally show ?thesis .
   1.674 +qed
   1.675 +
   1.676 +(* TODO Legacy names *)
   1.677 +lemmas prime_imp_coprime_nat = is_prime_imp_coprime[where ?'a = nat]
   1.678 +lemmas prime_imp_coprime_int = is_prime_imp_coprime[where ?'a = int]
   1.679 +lemmas prime_dvd_mult_nat = is_prime_dvd_mult_iff[where ?'a = nat]
   1.680 +lemmas prime_dvd_mult_int = is_prime_dvd_mult_iff[where ?'a = int]
   1.681 +lemmas prime_dvd_mult_eq_nat = is_prime_dvd_mult_iff[where ?'a = nat]
   1.682 +lemmas prime_dvd_mult_eq_int = is_prime_dvd_mult_iff[where ?'a = int]
   1.683 +lemmas prime_dvd_power_nat = is_prime_dvd_power[where ?'a = nat]
   1.684 +lemmas prime_dvd_power_int = is_prime_dvd_power[where ?'a = int]
   1.685 +lemmas prime_dvd_power_nat_iff = is_prime_dvd_power_iff[where ?'a = nat]
   1.686 +lemmas prime_dvd_power_int_iff = is_prime_dvd_power_iff[where ?'a = int]
   1.687 +lemmas prime_imp_power_coprime_nat = is_prime_imp_power_coprime[where ?'a = nat]
   1.688 +lemmas prime_imp_power_coprime_int = is_prime_imp_power_coprime[where ?'a = int]
   1.689 +lemmas primes_coprime_nat = primes_coprime[where ?'a = nat]
   1.690 +lemmas primes_coprime_int = primes_coprime[where ?'a = nat]
   1.691 +lemmas prime_divprod_pow_nat = prime_divprod_pow[where ?'a = nat]
   1.692 +lemmas prime_exp = is_prime_elem_power_iff[where ?'a = nat]
   1.693 +
   1.694 +end
   1.695 \ No newline at end of file