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.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
```