Theory HOL-Computational_Algebra.Primes
section ‹Primes›
theory Primes
imports Euclidean_Algorithm
begin
subsection ‹Primes on \<^typ>‹nat› and \<^typ>‹int››
lemma Suc_0_not_prime_nat [simp]: "¬ prime (Suc 0)"
using not_prime_1 [where ?'a = nat] by simp
lemma prime_ge_2_nat:
"p ≥ 2" if "prime p" for p :: nat
proof -
from that have "p ≠ 0" and "p ≠ 1"
by (auto dest: prime_elem_not_zeroI prime_elem_not_unit)
then show ?thesis
by simp
qed
lemma prime_ge_2_int:
"p ≥ 2" if "prime p" for p :: int
proof -
from that have "prime_elem p" and "¦p¦ = p"
by (auto dest: normalize_prime)
then have "p ≠ 0" and "¦p¦ ≠ 1" and "p ≥ 0"
by (auto dest: prime_elem_not_zeroI prime_elem_not_unit)
then show ?thesis
by simp
qed
lemma prime_ge_0_int: "prime p ⟹ p ≥ (0::int)"
using prime_ge_2_int [of p] by simp
lemma prime_gt_0_nat: "prime p ⟹ p > (0::nat)"
using prime_ge_2_nat [of p] by simp
lemma prime_gt_0_int: "prime p ⟹ p > (0::int)"
using prime_ge_2_int [of p] by simp
lemma prime_ge_1_nat: "prime p ⟹ p ≥ (1::nat)"
using prime_ge_2_nat [of p] by simp
lemma prime_ge_Suc_0_nat: "prime p ⟹ p ≥ Suc 0"
using prime_ge_1_nat [of p] by simp
lemma prime_ge_1_int: "prime p ⟹ p ≥ (1::int)"
using prime_ge_2_int [of p] by simp
lemma prime_gt_1_nat: "prime p ⟹ p > (1::nat)"
using prime_ge_2_nat [of p] by simp
lemma prime_gt_Suc_0_nat: "prime p ⟹ p > Suc 0"
using prime_gt_1_nat [of p] by simp
lemma prime_gt_1_int: "prime p ⟹ p > (1::int)"
using prime_ge_2_int [of p] by simp
lemma prime_natI:
"prime p" if "p ≥ 2" and "⋀m n. p dvd m * n ⟹ p dvd m ∨ p dvd n" for p :: nat
using that by (auto intro!: primeI prime_elemI)
lemma prime_intI:
"prime p" if "p ≥ 2" and "⋀m n. p dvd m * n ⟹ p dvd m ∨ p dvd n" for p :: int
using that by (auto intro!: primeI prime_elemI)
lemma prime_elem_nat_iff [simp]:
"prime_elem n ⟷ prime n" for n :: nat
by (simp add: prime_def)
lemma prime_elem_iff_prime_abs [simp]:
"prime_elem k ⟷ prime ¦k¦" for k :: int
by (auto intro: primeI)
lemma prime_nat_int_transfer [simp]:
"prime (int n) ⟷ prime n" (is "?P ⟷ ?Q")
proof
assume ?P
then have "n ≥ 2"
by (auto dest: prime_ge_2_int)
then show ?Q
proof (rule prime_natI)
fix r s
assume "n dvd r * s"
with of_nat_dvd_iff [of n "r * s"] have "int n dvd int r * int s"
by simp
with ‹?P› have "int n dvd int r ∨ int n dvd int s"
using prime_dvd_mult_iff [of "int n" "int r" "int s"]
by simp
then show "n dvd r ∨ n dvd s"
by simp
qed
next
assume ?Q
then have "int n ≥ 2"
by (auto dest: prime_ge_2_nat)
then show ?P
proof (rule prime_intI)
fix r s
assume "int n dvd r * s"
then have "n dvd nat ¦r * s¦"
by simp
then have "n dvd nat ¦r¦ * nat ¦s¦"
by (simp add: nat_abs_mult_distrib)
with ‹?Q› have "n dvd nat ¦r¦ ∨ n dvd nat ¦s¦"
using prime_dvd_mult_iff [of "n" "nat ¦r¦" "nat ¦s¦"]
by simp
then show "int n dvd r ∨ int n dvd s"
by simp
qed
qed
lemma prime_nat_iff_prime [simp]:
"prime (nat k) ⟷ prime k"
proof (cases "k ≥ 0")
case True
then show ?thesis
using prime_nat_int_transfer [of "nat k"] by simp
next
case False
then show ?thesis
by (auto dest: prime_ge_2_int)
qed
lemma prime_int_nat_transfer:
"prime k ⟷ k ≥ 0 ∧ prime (nat k)"
by (auto dest: prime_ge_2_int)
lemma prime_nat_naiveI:
"prime p" if "p ≥ 2" and dvd: "⋀n. n dvd p ⟹ n = 1 ∨ n = p" for p :: nat
proof (rule primeI, rule prime_elemI)
fix m n :: nat
assume "p dvd m * n"
then obtain r s where "p = r * s" "r dvd m" "s dvd n"
by (blast dest: division_decomp)
moreover have "r = 1 ∨ r = p"
using ‹r dvd m› ‹p = r * s› dvd [of r] by simp
ultimately show "p dvd m ∨ p dvd n"
by auto
qed (use ‹p ≥ 2› in simp_all)
lemma prime_int_naiveI:
"prime p" if "p ≥ 2" and dvd: "⋀k. k dvd p ⟹ ¦k¦ = 1 ∨ ¦k¦ = p" for p :: int
proof -
from ‹p ≥ 2› have "nat p ≥ 2"
by simp
then have "prime (nat p)"
proof (rule prime_nat_naiveI)
fix n
assume "n dvd nat p"
with ‹p ≥ 2› have "n dvd nat ¦p¦"
by simp
then have "int n dvd p"
by simp
with dvd [of "int n"] show "n = 1 ∨ n = nat p"
by auto
qed
then show ?thesis
by simp
qed
lemma prime_nat_iff:
"prime (n :: nat) ⟷ (1 < n ∧ (∀m. m dvd n ⟶ m = 1 ∨ m = n))"
proof (safe intro!: prime_gt_1_nat)
assume "prime n"
then have *: "prime_elem n"
by simp
fix m assume m: "m dvd n" "m ≠ n"
from * ‹m dvd n› have "n dvd m ∨ is_unit m"
by (intro irreducibleD' prime_elem_imp_irreducible)
with m show "m = 1" by (auto dest: dvd_antisym)
next
assume "n > 1" "∀m. m dvd n ⟶ m = 1 ∨ m = n"
then show "prime n"
using prime_nat_naiveI [of n] by auto
qed
lemma prime_int_iff:
"prime (n::int) ⟷ (1 < n ∧ (∀m. m ≥ 0 ∧ m dvd n ⟶ m = 1 ∨ m = n))"
proof (intro iffI conjI allI impI; (elim conjE)?)
assume *: "prime n"
hence irred: "irreducible n" by (auto intro: prime_elem_imp_irreducible)
from * have "n ≥ 0" "n ≠ 0" "n ≠ 1"
by (auto simp add: prime_ge_0_int)
thus "n > 1" by presburger
fix m assume "m dvd n" ‹m ≥ 0›
with irred have "m dvd 1 ∨ n dvd m" by (auto simp: irreducible_altdef)
with ‹m dvd n› ‹m ≥ 0› ‹n > 1› show "m = 1 ∨ m = n"
using associated_iff_dvd[of m n] by auto
next
assume n: "1 < n" "∀m. m ≥ 0 ∧ m dvd n ⟶ m = 1 ∨ m = n"
hence "nat n > 1" by simp
moreover have "∀m. m dvd nat n ⟶ m = 1 ∨ m = nat n"
proof (intro allI impI)
fix m assume "m dvd nat n"
with ‹n > 1› have "m dvd nat ¦n¦"
by simp
then have "int m dvd n"
by simp
with n(2) have "int m = 1 ∨ int m = n"
using of_nat_0_le_iff by blast
thus "m = 1 ∨ m = nat n" by auto
qed
ultimately show "prime n"
unfolding prime_int_nat_transfer prime_nat_iff by auto
qed
lemma prime_nat_not_dvd:
assumes "prime p" "p > n" "n ≠ (1::nat)"
shows "¬n dvd p"
proof
assume "n dvd p"
from assms(1) have "irreducible p" by (simp add: prime_elem_imp_irreducible)
from irreducibleD'[OF this ‹n dvd p›] ‹n dvd p› ‹p > n› assms show False
by (cases "n = 0") (auto dest!: dvd_imp_le)
qed
lemma prime_int_not_dvd:
assumes "prime p" "p > n" "n > (1::int)"
shows "¬n dvd p"
proof
assume "n dvd p"
from assms(1) have "irreducible p" by (auto intro: prime_elem_imp_irreducible)
from irreducibleD'[OF this ‹n dvd p›] ‹n dvd p› ‹p > n› assms show False
by (auto dest!: zdvd_imp_le)
qed
lemma prime_odd_nat: "prime p ⟹ p > (2::nat) ⟹ odd p"
by (intro prime_nat_not_dvd) auto
lemma prime_odd_int: "prime p ⟹ p > (2::int) ⟹ odd p"
by (intro prime_int_not_dvd) auto
lemma prime_int_altdef:
"prime p = (1 < p ∧ (∀m::int. m ≥ 0 ⟶ m dvd p ⟶
m = 1 ∨ m = p))"
unfolding prime_int_iff by blast
lemma not_prime_eq_prod_nat:
assumes "m > 1" "¬ prime (m::nat)"
shows "∃n k. n = m * k ∧ 1 < m ∧ m < n ∧ 1 < k ∧ k < n"
using assms irreducible_altdef[of m]
by (auto simp: prime_elem_iff_irreducible irreducible_altdef)
subsection ‹Largest exponent of a prime factor›
text‹Possibly duplicates other material, but avoid the complexities of multisets.›
lemma prime_power_cancel_less:
assumes "prime p" and eq: "m * (p ^ k) = m' * (p ^ k')" and less: "k < k'" and "¬ p dvd m"
shows False
proof -
obtain l where l: "k' = k + l" and "l > 0"
using less less_imp_add_positive by auto
have "m = m * (p ^ k) div (p ^ k)"
using ‹prime p› by simp
also have "… = m' * (p ^ k') div (p ^ k)"
using eq by simp
also have "… = m' * (p ^ l) * (p ^ k) div (p ^ k)"
by (simp add: l mult.commute mult.left_commute power_add)
also have "... = m' * (p ^ l)"
using ‹prime p› by simp
finally have "p dvd m"
using ‹l > 0› by simp
with assms show False
by simp
qed
lemma prime_power_cancel:
assumes "prime p" and eq: "m * (p ^ k) = m' * (p ^ k')" and "¬ p dvd m" "¬ p dvd m'"
shows "k = k'"
using prime_power_cancel_less [OF ‹prime p›] assms
by (metis linorder_neqE_nat)
lemma prime_power_cancel2:
assumes "prime p" "m * (p ^ k) = m' * (p ^ k')" "¬ p dvd m" "¬ p dvd m'"
obtains "m = m'" "k = k'"
using prime_power_cancel [OF assms] assms by auto
lemma prime_power_canonical:
fixes m :: nat
assumes "prime p" "m > 0"
shows "∃k n. ¬ p dvd n ∧ m = n * p ^ k"
using ‹m > 0›
proof (induction m rule: less_induct)
case (less m)
show ?case
proof (cases "p dvd m")
case True
then obtain m' where m': "m = p * m'"
using dvdE by blast
with ‹prime p› have "0 < m'" "m' < m"
using less.prems prime_nat_iff by auto
with m' less show ?thesis
by (metis power_Suc mult.left_commute)
next
case False
then show ?thesis
by (metis mult.right_neutral power_0)
qed
qed
subsubsection ‹Make prime naively executable›
lemma prime_nat_iff':
"prime (p :: nat) ⟷ p > 1 ∧ (∀n ∈ {2..<p}. ¬ n dvd p)"
proof safe
assume "p > 1" and *: "∀n∈{2..<p}. ¬n dvd p"
show "prime p" unfolding prime_nat_iff
proof (intro conjI allI impI)
fix m assume "m dvd p"
with ‹p > 1› have "m ≠ 0" by (intro notI) auto
hence "m ≥ 1" by simp
moreover from ‹m dvd p› and * have "m ∉ {2..<p}" by blast
with ‹m dvd p› and ‹p > 1› have "m ≤ 1 ∨ m = p" by (auto dest: dvd_imp_le)
ultimately show "m = 1 ∨ m = p" by simp
qed fact+
qed (auto simp: prime_nat_iff)
lemma prime_int_iff':
"prime (p :: int) ⟷ p > 1 ∧ (∀n ∈ {2..<p}. ¬ n dvd p)" (is "?P ⟷ ?Q")
proof (cases "p ≥ 0")
case True
have "?P ⟷ prime (nat p)"
by simp
also have "… ⟷ p > 1 ∧ (∀n∈{2..<nat p}. ¬ n dvd nat ¦p¦)"
using True by (simp add: prime_nat_iff')
also have "{2..<nat p} = nat ` {2..<p}"
using True int_eq_iff by fastforce
finally show "?P ⟷ ?Q" by simp
next
case False
then show ?thesis
by (auto simp add: prime_ge_0_int)
qed
lemma prime_int_numeral_eq [simp]:
"prime (numeral m :: int) ⟷ prime (numeral m :: nat)"
by (simp add: prime_int_nat_transfer)
lemma two_is_prime_nat [simp]: "prime (2::nat)"
by (simp add: prime_nat_iff')
lemma prime_nat_numeral_eq [simp]:
"prime (numeral m :: nat) ⟷
(1::nat) < numeral m ∧
(∀n::nat ∈ set [2..<numeral m]. ¬ n dvd numeral m)"
by (simp only: prime_nat_iff' set_upt)
text‹A bit of regression testing:›
lemma "prime(97::nat)" by simp
lemma "prime(97::int)" by simp
lemma prime_factor_nat:
"n ≠ (1::nat) ⟹ ∃p. prime p ∧ p dvd n"
using prime_divisor_exists[of n]
by (cases "n = 0") (auto intro: exI[of _ "2::nat"])
lemma prime_factor_int:
fixes k :: int
assumes "¦k¦ ≠ 1"
obtains p where "prime p" "p dvd k"
proof (cases "k = 0")
case True
then have "prime (2::int)" and "2 dvd k"
by simp_all
with that show thesis
by blast
next
case False
with assms prime_divisor_exists [of k] obtain p where "prime p" "p dvd k"
by auto
with that show thesis
by blast
qed
subsection ‹Infinitely many primes›
lemma next_prime_bound: "∃p::nat. prime p ∧ n < p ∧ p ≤ fact n + 1"
proof-
have f1: "fact n + 1 ≠ (1::nat)" using fact_ge_1 [of n, where 'a=nat] by arith
from prime_factor_nat [OF f1]
obtain p :: nat where "prime p" and "p dvd fact n + 1" by auto
then have "p ≤ fact n + 1" apply (intro dvd_imp_le) apply auto done
{ assume "p ≤ n"
from ‹prime p› have "p ≥ 1"
by (cases p, simp_all)
with ‹p <= n› have "p dvd fact n"
by (intro dvd_fact)
with ‹p dvd fact n + 1› have "p dvd fact n + 1 - fact n"
by (rule dvd_diff_nat)
then have "p dvd 1" by simp
then have "p <= 1" by auto
moreover from ‹prime p› have "p > 1"
using prime_nat_iff by blast
ultimately have False by auto}
then have "n < p" by presburger
with ‹prime p› and ‹p <= fact n + 1› show ?thesis by auto
qed
lemma bigger_prime: "∃p. prime p ∧ p > (n::nat)"
using next_prime_bound by auto
lemma primes_infinite: "¬ (finite {(p::nat). prime p})"
proof
assume "finite {(p::nat). prime p}"
with Max_ge have "(∃b. (∀x ∈ {(p::nat). prime p}. x ≤ b))"
by auto
then obtain b where "∀(x::nat). prime x ⟶ x ≤ b"
by auto
with bigger_prime [of b] show False
by auto
qed
subsection ‹Powers of Primes›
text‹Versions for type nat only›
lemma prime_product:
fixes p::nat
assumes "prime (p * q)"
shows "p = 1 ∨ q = 1"
proof -
from assms have
"1 < p * q" and P: "⋀m. m dvd p * q ⟹ m = 1 ∨ m = p * q"
unfolding prime_nat_iff by auto
from ‹1 < p * q› have "p ≠ 0" by (cases p) auto
then have Q: "p = p * q ⟷ q = 1" by auto
have "p dvd p * q" by simp
then have "p = 1 ∨ p = p * q" by (rule P)
then show ?thesis by (simp add: Q)
qed
lemma prime_power_mult_nat:
fixes p :: nat
assumes p: "prime p" and xy: "x * y = p ^ k"
shows "∃i j. x = p ^ i ∧ y = p^ j"
using xy
proof(induct k arbitrary: x y)
case 0 thus ?case apply simp by (rule exI[where x="0"], simp)
next
case (Suc k x y)
from Suc.prems have pxy: "p dvd x*y" by auto
from prime_dvd_multD [OF p pxy] have pxyc: "p dvd x ∨ p dvd y" .
from p have p0: "p ≠ 0" by - (rule ccontr, simp)
{assume px: "p dvd x"
then obtain d where d: "x = p*d" unfolding dvd_def by blast
from Suc.prems d have "p*d*y = p^Suc k" by simp
hence th: "d*y = p^k" using p0 by simp
from Suc.hyps[OF th] obtain i j where ij: "d = p^i" "y = p^j" by blast
with d have "x = p^Suc i" by simp
with ij(2) have ?case by blast}
moreover
{assume px: "p dvd y"
then obtain d where d: "y = p*d" unfolding dvd_def by blast
from Suc.prems d have "p*d*x = p^Suc k" by (simp add: mult.commute)
hence th: "d*x = p^k" using p0 by simp
from Suc.hyps[OF th] obtain i j where ij: "d = p^i" "x = p^j" by blast
with d have "y = p^Suc i" by simp
with ij(2) have ?case by blast}
ultimately show ?case using pxyc by blast
qed
lemma prime_power_exp_nat:
fixes p::nat
assumes p: "prime p" and n: "n ≠ 0"
and xn: "x^n = p^k" shows "∃i. x = p^i"
using n xn
proof(induct n arbitrary: k)
case 0 thus ?case by simp
next
case (Suc n k) hence th: "x*x^n = p^k" by simp
{assume "n = 0" with Suc have ?case by simp (rule exI[where x="k"], simp)}
moreover
{assume n: "n ≠ 0"
from prime_power_mult_nat[OF p th]
obtain i j where ij: "x = p^i" "x^n = p^j"by blast
from Suc.hyps[OF n ij(2)] have ?case .}
ultimately show ?case by blast
qed
lemma divides_primepow_nat:
fixes p :: nat
assumes p: "prime p"
shows "d dvd p ^ k ⟷ (∃i≤k. d = p ^ i)"
using assms divides_primepow [of p d k] by (auto intro: le_imp_power_dvd)
subsection ‹Chinese Remainder Theorem Variants›
lemma bezout_gcd_nat:
fixes a::nat shows "∃x y. a * x - b * y = gcd a b ∨ b * x - a * y = gcd a b"
using bezout_nat[of a b]
by (metis bezout_nat diff_add_inverse gcd_add_mult gcd.commute
gcd_nat.right_neutral mult_0)
lemma gcd_bezout_sum_nat:
fixes a::nat
assumes "a * x + b * y = d"
shows "gcd a b dvd d"
proof-
let ?g = "gcd a b"
have dv: "?g dvd a*x" "?g dvd b * y"
by simp_all
from dvd_add[OF dv] assms
show ?thesis by auto
qed
text ‹A binary form of the Chinese Remainder Theorem.›
lemma chinese_remainder:
fixes a::nat assumes ab: "coprime a b" and a: "a ≠ 0" and b: "b ≠ 0"
shows "∃x q1 q2. x = u + q1 * a ∧ x = v + q2 * b"
proof-
from bezout_add_strong_nat[OF a, of b] bezout_add_strong_nat[OF b, of a]
obtain d1 x1 y1 d2 x2 y2 where dxy1: "d1 dvd a" "d1 dvd b" "a * x1 = b * y1 + d1"
and dxy2: "d2 dvd b" "d2 dvd a" "b * x2 = a * y2 + d2" by blast
then have d12: "d1 = 1" "d2 = 1"
using ab coprime_common_divisor_nat [of a b] by blast+
let ?x = "v * a * x1 + u * b * x2"
let ?q1 = "v * x1 + u * y2"
let ?q2 = "v * y1 + u * x2"
from dxy2(3)[simplified d12] dxy1(3)[simplified d12]
have "?x = u + ?q1 * a" "?x = v + ?q2 * b"
by algebra+
thus ?thesis by blast
qed
text ‹Primality›
lemma coprime_bezout_strong:
fixes a::nat assumes "coprime a b" "b ≠ 1"
shows "∃x y. a * x = b * y + 1"
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)
lemma bezout_prime:
assumes p: "prime p" and pa: "¬ p dvd a"
shows "∃x y. a*x = Suc (p*y)"
proof -
have ap: "coprime a p"
using coprime_commute p pa prime_imp_coprime by auto
moreover from p have "p ≠ 1" by auto
ultimately have "∃x y. a * x = p * y + 1"
by (rule coprime_bezout_strong)
then show ?thesis by simp
qed
subsection ‹Multiplicity and primality for natural numbers and integers›
lemma prime_factors_gt_0_nat:
"p ∈ prime_factors x ⟹ p > (0::nat)"
by (simp add: in_prime_factors_imp_prime prime_gt_0_nat)
lemma prime_factors_gt_0_int:
"p ∈ prime_factors x ⟹ p > (0::int)"
by (simp add: in_prime_factors_imp_prime prime_gt_0_int)
lemma prime_factors_ge_0_int [elim]:
fixes n :: int
shows "p ∈ prime_factors n ⟹ p ≥ 0"
by (drule prime_factors_gt_0_int) simp
lemma prod_mset_prime_factorization_int:
fixes n :: int
assumes "n > 0"
shows "prod_mset (prime_factorization n) = n"
using assms by (simp add: prod_mset_prime_factorization)
lemma prime_factorization_exists_nat:
"n > 0 ⟹ (∃M. (∀p::nat ∈ set_mset M. prime p) ∧ n = (∏i ∈# M. i))"
using prime_factorization_exists[of n] by auto
lemma prod_mset_prime_factorization_nat [simp]:
"(n::nat) > 0 ⟹ prod_mset (prime_factorization n) = n"
by (subst prod_mset_prime_factorization) simp_all
lemma prime_factorization_nat:
"n > (0::nat) ⟹ n = (∏p ∈ prime_factors n. p ^ multiplicity p n)"
by (simp add: prod_prime_factors)
lemma prime_factorization_int:
"n > (0::int) ⟹ n = (∏p ∈ prime_factors n. p ^ multiplicity p n)"
by (simp add: prod_prime_factors)
lemma prime_factorization_unique_nat:
fixes f :: "nat ⇒ _"
assumes S_eq: "S = {p. 0 < f p}"
and "finite S"
and S: "∀p∈S. prime p" "n = (∏p∈S. p ^ f p)"
shows "S = prime_factors n ∧ (∀p. prime p ⟶ f p = multiplicity p n)"
using assms by (intro prime_factorization_unique'') auto
lemma prime_factorization_unique_int:
fixes f :: "int ⇒ _"
assumes S_eq: "S = {p. 0 < f p}"
and "finite S"
and S: "∀p∈S. prime p" "abs n = (∏p∈S. p ^ f p)"
shows "S = prime_factors n ∧ (∀p. prime p ⟶ f p = multiplicity p n)"
using assms by (intro prime_factorization_unique'') auto
lemma prime_factors_characterization_nat:
"S = {p. 0 < f (p::nat)} ⟹
finite S ⟹ ∀p∈S. prime p ⟹ n = (∏p∈S. p ^ f p) ⟹ prime_factors n = S"
by (rule prime_factorization_unique_nat [THEN conjunct1, symmetric])
lemma prime_factors_characterization'_nat:
"finite {p. 0 < f (p::nat)} ⟹
(∀p. 0 < f p ⟶ prime p) ⟹
prime_factors (∏p | 0 < f p. p ^ f p) = {p. 0 < f p}"
by (rule prime_factors_characterization_nat) auto
lemma prime_factors_characterization_int:
"S = {p. 0 < f (p::int)} ⟹ finite S ⟹
∀p∈S. prime p ⟹ abs n = (∏p∈S. p ^ f p) ⟹ prime_factors n = S"
by (rule prime_factorization_unique_int [THEN conjunct1, symmetric])
lemma abs_prod: "abs (prod f A :: 'a :: linordered_idom) = prod (λx. abs (f x)) A"
by (cases "finite A", induction A rule: finite_induct) (simp_all add: abs_mult)
lemma primes_characterization'_int [rule_format]:
"finite {p. p ≥ 0 ∧ 0 < f (p::int)} ⟹ ∀p. 0 < f p ⟶ prime p ⟹
prime_factors (∏p | p ≥ 0 ∧ 0 < f p. p ^ f p) = {p. p ≥ 0 ∧ 0 < f p}"
by (rule prime_factors_characterization_int) (auto simp: abs_prod prime_ge_0_int)
lemma multiplicity_characterization_nat:
"S = {p. 0 < f (p::nat)} ⟹ finite S ⟹ ∀p∈S. prime p ⟹ prime p ⟹
n = (∏p∈S. p ^ f p) ⟹ multiplicity p n = f p"
by (frule prime_factorization_unique_nat [of S f n, THEN conjunct2, rule_format, symmetric]) auto
lemma multiplicity_characterization'_nat: "finite {p. 0 < f (p::nat)} ⟶
(∀p. 0 < f p ⟶ prime p) ⟶ prime p ⟶
multiplicity p (∏p | 0 < f p. p ^ f p) = f p"
by (intro impI, rule multiplicity_characterization_nat) auto
lemma multiplicity_characterization_int: "S = {p. 0 < f (p::int)} ⟹
finite S ⟹ ∀p∈S. prime p ⟹ prime p ⟹ n = (∏p∈S. p ^ f p) ⟹ multiplicity p n = f p"
by (frule prime_factorization_unique_int [of S f n, THEN conjunct2, rule_format, symmetric])
(auto simp: abs_prod power_abs prime_ge_0_int intro!: prod.cong)
lemma multiplicity_characterization'_int [rule_format]:
"finite {p. p ≥ 0 ∧ 0 < f (p::int)} ⟹
(∀p. 0 < f p ⟶ prime p) ⟹ prime p ⟹
multiplicity p (∏p | p ≥ 0 ∧ 0 < f p. p ^ f p) = f p"
by (rule multiplicity_characterization_int) (auto simp: prime_ge_0_int)
lemma multiplicity_one_nat [simp]: "multiplicity p (Suc 0) = 0"
unfolding One_nat_def [symmetric] by (rule multiplicity_one)
lemma multiplicity_eq_nat:
fixes x and y::nat
assumes "x > 0" "y > 0" "⋀p. prime p ⟹ multiplicity p x = multiplicity p y"
shows "x = y"
using multiplicity_eq_imp_eq[of x y] assms by simp
lemma multiplicity_eq_int:
fixes x y :: int
assumes "x > 0" "y > 0" "⋀p. prime p ⟹ multiplicity p x = multiplicity p y"
shows "x = y"
using multiplicity_eq_imp_eq[of x y] assms by simp
lemma multiplicity_prod_prime_powers:
assumes "finite S" "⋀x. x ∈ S ⟹ prime x" "prime p"
shows "multiplicity p (∏p ∈ S. p ^ f p) = (if p ∈ S then f p else 0)"
proof -
define g where "g = (λx. if x ∈ S then f x else 0)"
define A where "A = Abs_multiset g"
have "{x. g x > 0} ⊆ S" by (auto simp: g_def)
from finite_subset[OF this assms(1)] have [simp]: "finite {x. 0 < g x}"
by simp
from assms have count_A: "count A x = g x" for x unfolding A_def
by simp
have set_mset_A: "set_mset A = {x∈S. f x > 0}"
unfolding set_mset_def count_A by (auto simp: g_def)
with assms have prime: "prime x" if "x ∈# A" for x using that by auto
from set_mset_A assms have "(∏p ∈ S. p ^ f p) = (∏p ∈ S. p ^ g p) "
by (intro prod.cong) (auto simp: g_def)
also from set_mset_A assms have "… = (∏p ∈ set_mset A. p ^ g p)"
by (intro prod.mono_neutral_right) (auto simp: g_def set_mset_A)
also have "… = prod_mset A"
by (auto simp: prod_mset_multiplicity count_A set_mset_A intro!: prod.cong)
also from assms have "multiplicity p … = sum_mset (image_mset (multiplicity p) A)"
by (subst prime_elem_multiplicity_prod_mset_distrib) (auto dest: prime)
also from assms have "image_mset (multiplicity p) A = image_mset (λx. if x = p then 1 else 0) A"
by (intro image_mset_cong) (auto simp: prime_multiplicity_other dest: prime)
also have "sum_mset … = (if p ∈ S then f p else 0)" by (simp add: sum_mset_delta count_A g_def)
finally show ?thesis .
qed
lemma prime_factorization_prod_mset:
assumes "0 ∉# A"
shows "prime_factorization (prod_mset A) = ∑⇩#(image_mset prime_factorization A)"
using assms by (induct A) (auto simp add: prime_factorization_mult)
lemma prime_factors_prod:
assumes "finite A" and "0 ∉ f ` A"
shows "prime_factors (prod f A) = ⋃((prime_factors ∘ f) ` A)"
using assms by (simp add: prod_unfold_prod_mset prime_factorization_prod_mset)
lemma prime_factors_fact:
"prime_factors (fact n) = {p ∈ {2..n}. prime p}" (is "?M = ?N")
proof (rule set_eqI)
fix p
{ fix m :: nat
assume "p ∈ prime_factors m"
then have "prime p" and "p dvd m" by auto
moreover assume "m > 0"
ultimately have "2 ≤ p" and "p ≤ m"
by (auto intro: prime_ge_2_nat dest: dvd_imp_le)
moreover assume "m ≤ n"
ultimately have "2 ≤ p" and "p ≤ n"
by (auto intro: order_trans)
} note * = this
show "p ∈ ?M ⟷ p ∈ ?N"
by (auto simp add: fact_prod prime_factors_prod Suc_le_eq dest!: prime_prime_factors intro: *)
qed
lemma prime_dvd_fact_iff:
assumes "prime p"
shows "p dvd fact n ⟷ p ≤ n"
using assms
by (auto simp add: prime_factorization_subset_iff_dvd [symmetric]
prime_factorization_prime prime_factors_fact prime_ge_2_nat)
lemma dvd_choose_prime:
assumes kn: "k < n" and k: "k ≠ 0" and n: "n ≠ 0" and prime_n: "prime n"
shows "n dvd (n choose k)"
proof -
have "n dvd (fact n)" by (simp add: fact_num_eq_if n)
moreover have "¬ n dvd (fact k * fact (n-k))"
by (metis prime_dvd_fact_iff prime_dvd_mult_iff assms neq0_conv diff_less linorder_not_less)
moreover have "(fact n::nat) = fact k * fact (n-k) * (n choose k)"
using binomial_fact_lemma kn by auto
ultimately show ?thesis using prime_n
by (auto simp add: prime_dvd_mult_iff)
qed
lemma (in ring_1) minus_power_prime_CHAR:
assumes "p = CHAR('a)" "prime p"
shows "(-x :: 'a) ^ p = -(x ^ p)"
proof (cases "p = 2")
case False
have "prime p"
using assms by blast
hence "odd p"
using prime_imp_coprime assms False coprime_right_2_iff_odd gcd_nat.strict_iff_not by blast
thus ?thesis
by simp
qed (use assms in ‹auto simp: uminus_CHAR_2›)
subsection ‹Rings and fields with prime characteristic›
text ‹
We introduce some type classes for rings and fields with prime characteristic.
›
class semiring_prime_char = semiring_1 +
assumes prime_char_aux: "∃n. prime n ∧ of_nat n = (0 :: 'a)"
begin
lemma CHAR_pos [intro, simp]: "CHAR('a) > 0"
using local.CHAR_pos_iff local.prime_char_aux prime_gt_0_nat by blast
lemma CHAR_nonzero [simp]: "CHAR('a) ≠ 0"
using CHAR_pos by auto
lemma CHAR_prime [intro, simp]: "prime CHAR('a)"
by (metis (mono_tags, lifting) gcd_nat.order_iff_strict local.of_nat_1 local.of_nat_eq_0_iff_char_dvd
local.one_neq_zero local.prime_char_aux prime_nat_iff)
end
lemma semiring_prime_charI [intro?]:
"prime CHAR('a :: semiring_1) ⟹ OFCLASS('a, semiring_prime_char_class)"
by standard auto
lemma idom_prime_charI [intro?]:
assumes "CHAR('a :: idom) > 0"
shows "OFCLASS('a, semiring_prime_char_class)"
proof
show "prime CHAR('a)"
using assms prime_CHAR_semidom by blast
qed
class comm_semiring_prime_char = comm_semiring_1 + semiring_prime_char
class comm_ring_prime_char = comm_ring_1 + semiring_prime_char
begin
subclass comm_semiring_prime_char ..
end
class idom_prime_char = idom + semiring_prime_char
begin
subclass comm_ring_prime_char ..
end
class field_prime_char = field +
assumes pos_char_exists: "∃n>0. of_nat n = (0 :: 'a)"
begin
subclass idom_prime_char
apply standard
using pos_char_exists local.CHAR_pos_iff local.of_nat_CHAR local.prime_CHAR_semidom by blast
end
lemma field_prime_charI [intro?]:
"n > 0 ⟹ of_nat n = (0 :: 'a :: field) ⟹ OFCLASS('a, field_prime_char_class)"
by standard auto
lemma field_prime_charI' [intro?]:
"CHAR('a :: field) > 0 ⟹ OFCLASS('a, field_prime_char_class)"
by standard auto
subsection ‹Finite fields›
class finite_field = field_prime_char + finite
lemma finite_fieldI [intro?]:
assumes "finite (UNIV :: 'a :: field set)"
shows "OFCLASS('a, finite_field_class)"
proof standard
show "∃n>0. of_nat n = (0 :: 'a)"
using assms prime_CHAR_semidom[where ?'a = 'a] finite_imp_CHAR_pos[OF assms]
by (intro exI[of _ "CHAR('a)"]) auto
qed fact+
text ‹
On a finite field with ‹n› elements, taking the ‹n›-th power of an element
is the identity. This is an obvious consequence of the fact that the multiplicative group of
the field is a finite group of order ‹n - 1›, so ‹x^n = 1› for any non-zero ‹x›.
Note that this result is sharp in the sense that the multiplicative group of a
finite field is cyclic, i.e.\ it contains an element of order ‹n - 1›.
(We don't prove this here.)
›
lemma finite_field_power_card_eq_same:
fixes x :: "'a :: finite_field"
shows "x ^ card (UNIV :: 'a set) = x"
proof (cases "x = 0")
case False
have "x * (∏y∈UNIV-{0}. x * y) = x * x ^ (card (UNIV :: 'a set) - 1) * ∏(UNIV-{0})"
by (simp add: prod.distrib mult_ac)
also have "x * x ^ (card (UNIV :: 'a set) - 1) = x ^ Suc (card (UNIV :: 'a set) - 1)"
by (subst power_Suc) auto
also have "Suc (card (UNIV :: 'a set) - 1) = card (UNIV :: 'a set)"
using finite_UNIV_card_ge_0[where ?'a = 'a] by simp
also have "(∏y∈UNIV-{0}. x * y) = (∏y∈UNIV-{0}. y)"
by (rule prod.reindex_bij_witness[of _ "λy. y / x" "λy. x * y"]) (use False in auto)
finally show ?thesis
by simp
qed (use finite_UNIV_card_ge_0[where ?'a = 'a] in auto)
lemma finite_field_power_card_power_eq_same:
fixes x :: "'a :: finite_field"
assumes "m = card (UNIV :: 'a set) ^ n"
shows "x ^ m = x"
unfolding assms
by (induction n) (simp_all add: finite_field_power_card_eq_same power_mult)
class enum_finite_field = finite_field +
fixes enum_finite_field :: "nat ⇒ 'a"
assumes enum_finite_field: "enum_finite_field ` {..<card (UNIV :: 'a set)} = UNIV"
begin
lemma inj_on_enum_finite_field: "inj_on enum_finite_field {..<card (UNIV :: 'a set)}"
using enum_finite_field by (simp add: eq_card_imp_inj_on)
end
text ‹
To get rid of the pending sort hypotheses, we prove that the field with 2 elements is indeed
a finite field.
›
typedef gf2 = "{0, 1 :: nat}"
by auto
setup_lifting type_definition_gf2
instantiation gf2 :: field
begin
lift_definition zero_gf2 :: "gf2" is "0" by auto
lift_definition one_gf2 :: "gf2" is "1" by auto
lift_definition uminus_gf2 :: "gf2 ⇒ gf2" is "λx. x" .
lift_definition plus_gf2 :: "gf2 ⇒ gf2 ⇒ gf2" is "λx y. if x = y then 0 else 1" by auto
lift_definition minus_gf2 :: "gf2 ⇒ gf2 ⇒ gf2" is "λx y. if x = y then 0 else 1" by auto
lift_definition times_gf2 :: "gf2 ⇒ gf2 ⇒ gf2" is "λx y. x * y" by auto
lift_definition inverse_gf2 :: "gf2 ⇒ gf2" is "λx. x" .
lift_definition divide_gf2 :: "gf2 ⇒ gf2 ⇒ gf2" is "λx y. x * y" by auto
instance
by standard (transfer; fastforce)+
end
instance gf2 :: finite_field
proof
interpret type_definition Rep_gf2 Abs_gf2 "{0, 1 :: nat}"
by (rule type_definition_gf2)
show "finite (UNIV :: gf2 set)"
by (metis Abs_image finite.emptyI finite.insertI finite_imageI)
qed
subsection ‹The Freshman's Dream in rings of prime characteristic›
lemma (in comm_semiring_1) freshmans_dream:
fixes x y :: 'a and n :: nat
assumes "prime CHAR('a)"
assumes n_def: "n = CHAR('a)"
shows "(x + y) ^ n = x ^ n + y ^ n"
proof -
interpret comm_semiring_prime_char
by standard (auto intro!: exI[of _ "CHAR('a)"] assms)
have "n > 0"
unfolding n_def by simp
have "(x + y) ^ n = (∑k≤n. of_nat (n choose k) * x ^ k * y ^ (n - k))"
by (rule binomial_ring)
also have "… = (∑k∈{0,n}. of_nat (n choose k) * x ^ k * y ^ (n - k))"
proof (intro sum.mono_neutral_right ballI)
fix k assume "k ∈ {..n} - {0, n}"
hence k: "k > 0" "k < n"
by auto
have "CHAR('a) dvd (n choose k)"
unfolding n_def
by (rule dvd_choose_prime) (use k in ‹auto simp: n_def›)
hence "of_nat (n choose k) = (0 :: 'a)"
using of_nat_eq_0_iff_char_dvd by blast
thus "of_nat (n choose k) * x ^ k * y ^ (n - k) = 0"
by simp
qed auto
finally show ?thesis
using ‹n > 0› by (simp add: add_ac)
qed
lemma (in comm_semiring_1) freshmans_dream':
assumes [simp]: "prime CHAR('a)" and "m = CHAR('a) ^ n"
shows "(x + y :: 'a) ^ m = x ^ m + y ^ m"
unfolding assms(2)
proof (induction n)
case (Suc n)
have "(x + y) ^ (CHAR('a) ^ n * CHAR('a)) = ((x + y) ^ (CHAR('a) ^ n)) ^ CHAR('a)"
by (rule power_mult)
thus ?case
by (simp add: Suc.IH freshmans_dream Groups.mult_ac flip: power_mult)
qed auto
lemma (in comm_semiring_1) freshmans_dream_sum:
fixes f :: "'b ⇒ 'a"
assumes "prime CHAR('a)" and "n = CHAR('a)"
shows "sum f A ^ n = sum (λi. f i ^ n) A"
using assms
by (induct A rule: infinite_finite_induct)
(auto simp add: power_0_left freshmans_dream)
lemma (in comm_semiring_1) freshmans_dream_sum':
fixes f :: "'b ⇒ 'a"
assumes "prime CHAR('a)" "m = CHAR('a) ^ n"
shows "sum f A ^ m = sum (λi. f i ^ m) A"
using assms
by (induction A rule: infinite_finite_induct)
(auto simp: freshmans_dream' power_0_left)
lemmas prime_imp_coprime_nat = prime_imp_coprime[where ?'a = nat]
lemmas prime_imp_coprime_int = prime_imp_coprime[where ?'a = int]
lemmas prime_dvd_mult_nat = prime_dvd_mult_iff[where ?'a = nat]
lemmas prime_dvd_mult_int = prime_dvd_mult_iff[where ?'a = int]
lemmas prime_dvd_mult_eq_nat = prime_dvd_mult_iff[where ?'a = nat]
lemmas prime_dvd_mult_eq_int = prime_dvd_mult_iff[where ?'a = int]
lemmas prime_dvd_power_nat = prime_dvd_power[where ?'a = nat]
lemmas prime_dvd_power_int = prime_dvd_power[where ?'a = int]
lemmas prime_dvd_power_nat_iff = prime_dvd_power_iff[where ?'a = nat]
lemmas prime_dvd_power_int_iff = prime_dvd_power_iff[where ?'a = int]
lemmas prime_imp_power_coprime_nat = prime_imp_power_coprime[where ?'a = nat]
lemmas prime_imp_power_coprime_int = prime_imp_power_coprime[where ?'a = int]
lemmas primes_coprime_nat = primes_coprime[where ?'a = nat]
lemmas primes_coprime_int = primes_coprime[where ?'a = nat]
lemmas prime_divprod_pow_nat = prime_elem_divprod_pow[where ?'a = nat]
lemmas prime_exp = prime_elem_power_iff[where ?'a = nat]
text ‹Code generation›
context
begin
qualified definition prime_nat :: "nat ⇒ bool"
where [simp, code_abbrev]: "prime_nat = prime"
lemma prime_nat_naive [code]:
"prime_nat p ⟷ p > 1 ∧ (∀n ∈{1<..<p}. ¬ n dvd p)"
by (auto simp add: prime_nat_iff')
qualified definition prime_int :: "int ⇒ bool"
where [simp, code_abbrev]: "prime_int = prime"
lemma prime_int_naive [code]:
"prime_int p ⟷ p > 1 ∧ (∀n ∈{1<..<p}. ¬ n dvd p)"
by (auto simp add: prime_int_iff')
lemma "prime(997::nat)" by eval
lemma "prime(997::int)" by eval
end
end