Theory Factorial_Ring
section ‹Factorial (semi)rings›
theory Factorial_Ring
imports
Main
"HOL-Library.Multiset"
begin
unbundle multiset.lifting
subsection ‹Irreducible and prime elements›
context comm_semiring_1
begin
definition irreducible :: "'a ⇒ bool" where
"irreducible p ⟷ p ≠ 0 ∧ ¬p dvd 1 ∧ (∀a b. p = a * b ⟶ a dvd 1 ∨ b dvd 1)"
lemma not_irreducible_zero [simp]: "¬irreducible 0"
by (simp add: irreducible_def)
lemma irreducible_not_unit: "irreducible p ⟹ ¬p dvd 1"
by (simp add: irreducible_def)
lemma not_irreducible_one [simp]: "¬irreducible 1"
by (simp add: irreducible_def)
lemma irreducibleI:
"p ≠ 0 ⟹ ¬p dvd 1 ⟹ (⋀a b. p = a * b ⟹ a dvd 1 ∨ b dvd 1) ⟹ irreducible p"
by (simp add: irreducible_def)
lemma irreducibleD: "irreducible p ⟹ p = a * b ⟹ a dvd 1 ∨ b dvd 1"
by (simp add: irreducible_def)
lemma irreducible_mono:
assumes irr: "irreducible b" and "a dvd b" "¬a dvd 1"
shows "irreducible a"
proof (rule irreducibleI)
fix c d assume "a = c * d"
from assms obtain k where [simp]: "b = a * k" by auto
from ‹a = c * d› have "b = c * d * k"
by simp
hence "c dvd 1 ∨ (d * k) dvd 1"
using irreducibleD[OF irr, of c "d * k"] by (auto simp: mult.assoc)
thus "c dvd 1 ∨ d dvd 1"
by auto
qed (use assms in ‹auto simp: irreducible_def›)
definition prime_elem :: "'a ⇒ bool" where
"prime_elem p ⟷ p ≠ 0 ∧ ¬p dvd 1 ∧ (∀a b. p dvd (a * b) ⟶ p dvd a ∨ p dvd b)"
lemma not_prime_elem_zero [simp]: "¬prime_elem 0"
by (simp add: prime_elem_def)
lemma prime_elem_not_unit: "prime_elem p ⟹ ¬p dvd 1"
by (simp add: prime_elem_def)
lemma prime_elemI:
"p ≠ 0 ⟹ ¬p dvd 1 ⟹ (⋀a b. p dvd (a * b) ⟹ p dvd a ∨ p dvd b) ⟹ prime_elem p"
by (simp add: prime_elem_def)
lemma prime_elem_dvd_multD:
"prime_elem p ⟹ p dvd (a * b) ⟹ p dvd a ∨ p dvd b"
by (simp add: prime_elem_def)
lemma prime_elem_dvd_mult_iff:
"prime_elem p ⟹ p dvd (a * b) ⟷ p dvd a ∨ p dvd b"
by (auto simp: prime_elem_def)
lemma not_prime_elem_one [simp]:
"¬ prime_elem 1"
by (auto dest: prime_elem_not_unit)
lemma prime_elem_not_zeroI:
assumes "prime_elem p"
shows "p ≠ 0"
using assms by (auto intro: ccontr)
lemma prime_elem_dvd_power:
"prime_elem p ⟹ p dvd x ^ n ⟹ p dvd x"
by (induction n) (auto dest: prime_elem_dvd_multD intro: dvd_trans[of _ 1])
lemma prime_elem_dvd_power_iff:
"prime_elem p ⟹ n > 0 ⟹ p dvd x ^ n ⟷ p dvd x"
by (auto dest: prime_elem_dvd_power intro: dvd_trans)
lemma prime_elem_imp_nonzero [simp]:
"ASSUMPTION (prime_elem x) ⟹ x ≠ 0"
unfolding ASSUMPTION_def by (rule prime_elem_not_zeroI)
lemma prime_elem_imp_not_one [simp]:
"ASSUMPTION (prime_elem x) ⟹ x ≠ 1"
unfolding ASSUMPTION_def by auto
end
lemma (in normalization_semidom) irreducible_cong:
assumes "normalize a = normalize b"
shows "irreducible a ⟷ irreducible b"
proof (cases "a = 0 ∨ a dvd 1")
case True
hence "¬irreducible a" by (auto simp: irreducible_def)
from True have "normalize a = 0 ∨ normalize a dvd 1"
by auto
also note assms
finally have "b = 0 ∨ b dvd 1" by simp
hence "¬irreducible b" by (auto simp: irreducible_def)
with ‹¬irreducible a› show ?thesis by simp
next
case False
hence b: "b ≠ 0" "¬is_unit b" using assms
by (auto simp: is_unit_normalize[of b])
show ?thesis
proof
assume "irreducible a"
thus "irreducible b"
by (rule irreducible_mono) (use assms False b in ‹auto dest: associatedD2›)
next
assume "irreducible b"
thus "irreducible a"
by (rule irreducible_mono) (use assms False b in ‹auto dest: associatedD1›)
qed
qed
lemma (in normalization_semidom) associatedE1:
assumes "normalize a = normalize b"
obtains u where "is_unit u" "a = u * b"
proof (cases "a = 0")
case [simp]: False
from assms have [simp]: "b ≠ 0" by auto
show ?thesis
proof (rule that)
show "is_unit (unit_factor a div unit_factor b)"
by auto
have "unit_factor a div unit_factor b * b = unit_factor a * (b div unit_factor b)"
using ‹b ≠ 0› unit_div_commute unit_div_mult_swap unit_factor_is_unit by metis
also have "b div unit_factor b = normalize b" by simp
finally show "a = unit_factor a div unit_factor b * b"
by (metis assms unit_factor_mult_normalize)
qed
next
case [simp]: True
hence [simp]: "b = 0"
using assms[symmetric] by auto
show ?thesis
by (intro that[of 1]) auto
qed
lemma (in normalization_semidom) associatedE2:
assumes "normalize a = normalize b"
obtains u where "is_unit u" "b = u * a"
proof -
from assms have "normalize b = normalize a"
by simp
then obtain u where "is_unit u" "b = u * a"
by (elim associatedE1)
thus ?thesis using that by blast
qed
lemma (in normalization_semidom) normalize_power_normalize:
"normalize (normalize x ^ n) = normalize (x ^ n)"
proof (induction n)
case (Suc n)
have "normalize (normalize x ^ Suc n) = normalize (x * normalize (normalize x ^ n))"
by simp
also note Suc.IH
finally show ?case by simp
qed auto
context algebraic_semidom
begin
lemma prime_elem_imp_irreducible:
assumes "prime_elem p"
shows "irreducible p"
proof (rule irreducibleI)
fix a b
assume p_eq: "p = a * b"
with assms have nz: "a ≠ 0" "b ≠ 0" by auto
from p_eq have "p dvd a * b" by simp
with ‹prime_elem p› have "p dvd a ∨ p dvd b" by (rule prime_elem_dvd_multD)
with ‹p = a * b› have "a * b dvd 1 * b ∨ a * b dvd a * 1" by auto
thus "a dvd 1 ∨ b dvd 1"
by (simp only: dvd_times_left_cancel_iff[OF nz(1)] dvd_times_right_cancel_iff[OF nz(2)])
qed (insert assms, simp_all add: prime_elem_def)
lemma (in algebraic_semidom) unit_imp_no_irreducible_divisors:
assumes "is_unit x" "irreducible p"
shows "¬p dvd x"
proof (rule notI)
assume "p dvd x"
with ‹is_unit x› have "is_unit p"
by (auto intro: dvd_trans)
with ‹irreducible p› show False
by (simp add: irreducible_not_unit)
qed
lemma unit_imp_no_prime_divisors:
assumes "is_unit x" "prime_elem p"
shows "¬p dvd x"
using unit_imp_no_irreducible_divisors[OF assms(1) prime_elem_imp_irreducible[OF assms(2)]] .
lemma prime_elem_mono:
assumes "prime_elem p" "¬q dvd 1" "q dvd p"
shows "prime_elem q"
proof -
from ‹q dvd p› obtain r where r: "p = q * r" by (elim dvdE)
hence "p dvd q * r" by simp
with ‹prime_elem p› have "p dvd q ∨ p dvd r" by (rule prime_elem_dvd_multD)
hence "p dvd q"
proof
assume "p dvd r"
then obtain s where s: "r = p * s" by (elim dvdE)
from r have "p * 1 = p * (q * s)" by (subst (asm) s) (simp add: mult_ac)
with ‹prime_elem p› have "q dvd 1"
by (subst (asm) mult_cancel_left) auto
with ‹¬q dvd 1› show ?thesis by contradiction
qed
show ?thesis
proof (rule prime_elemI)
fix a b assume "q dvd (a * b)"
with ‹p dvd q› have "p dvd (a * b)" by (rule dvd_trans)
with ‹prime_elem p› have "p dvd a ∨ p dvd b" by (rule prime_elem_dvd_multD)
with ‹q dvd p› show "q dvd a ∨ q dvd b" by (blast intro: dvd_trans)
qed (insert assms, auto)
qed
lemma irreducibleD':
assumes "irreducible a" "b dvd a"
shows "a dvd b ∨ is_unit b"
proof -
from assms obtain c where c: "a = b * c" by (elim dvdE)
from irreducibleD[OF assms(1) this] have "is_unit b ∨ is_unit c" .
thus ?thesis by (auto simp: c mult_unit_dvd_iff)
qed
lemma irreducibleI':
assumes "a ≠ 0" "¬is_unit a" "⋀b. b dvd a ⟹ a dvd b ∨ is_unit b"
shows "irreducible a"
proof (rule irreducibleI)
fix b c assume a_eq: "a = b * c"
hence "a dvd b ∨ is_unit b" by (intro assms) simp_all
thus "is_unit b ∨ is_unit c"
proof
assume "a dvd b"
hence "b * c dvd b * 1" by (simp add: a_eq)
moreover from ‹a ≠ 0› a_eq have "b ≠ 0" by auto
ultimately show ?thesis by (subst (asm) dvd_times_left_cancel_iff) auto
qed blast
qed (simp_all add: assms(1,2))
lemma irreducible_altdef:
"irreducible x ⟷ x ≠ 0 ∧ ¬is_unit x ∧ (∀b. b dvd x ⟶ x dvd b ∨ is_unit b)"
using irreducibleI'[of x] irreducibleD'[of x] irreducible_not_unit[of x] by auto
lemma prime_elem_multD:
assumes "prime_elem (a * b)"
shows "is_unit a ∨ is_unit b"
proof -
from assms have "a ≠ 0" "b ≠ 0" by (auto dest!: prime_elem_not_zeroI)
moreover from assms prime_elem_dvd_multD [of "a * b"] have "a * b dvd a ∨ a * b dvd b"
by auto
ultimately show ?thesis
using dvd_times_left_cancel_iff [of a b 1]
dvd_times_right_cancel_iff [of b a 1]
by auto
qed
lemma prime_elemD2:
assumes "prime_elem p" and "a dvd p" and "¬ is_unit a"
shows "p dvd a"
proof -
from ‹a dvd p› obtain b where "p = a * b" ..
with ‹prime_elem p› prime_elem_multD ‹¬ is_unit a› have "is_unit b" by auto
with ‹p = a * b› show ?thesis
by (auto simp add: mult_unit_dvd_iff)
qed
lemma prime_elem_dvd_prod_msetE:
assumes "prime_elem p"
assumes dvd: "p dvd prod_mset A"
obtains a where "a ∈# A" and "p dvd a"
proof -
from dvd have "∃a. a ∈# A ∧ p dvd a"
proof (induct A)
case empty then show ?case
using ‹prime_elem p› by (simp add: prime_elem_not_unit)
next
case (add a A)
then have "p dvd a * prod_mset A" by simp
with ‹prime_elem p› consider (A) "p dvd prod_mset A" | (B) "p dvd a"
by (blast dest: prime_elem_dvd_multD)
then show ?case proof cases
case B then show ?thesis by auto
next
case A
with add.hyps obtain b where "b ∈# A" "p dvd b"
by auto
then show ?thesis by auto
qed
qed
with that show thesis by blast
qed
context
begin
lemma prime_elem_powerD:
assumes "prime_elem (p ^ n)"
shows "prime_elem p ∧ n = 1"
proof (cases n)
case (Suc m)
note assms
also from Suc have "p ^ n = p * p^m" by simp
finally have "is_unit p ∨ is_unit (p^m)" by (rule prime_elem_multD)
moreover from assms have "¬is_unit p" by (simp add: prime_elem_def is_unit_power_iff)
ultimately have "is_unit (p ^ m)" by simp
with ‹¬is_unit p› have "m = 0" by (simp add: is_unit_power_iff)
with Suc assms show ?thesis by simp
qed (insert assms, simp_all)
lemma prime_elem_power_iff:
"prime_elem (p ^ n) ⟷ prime_elem p ∧ n = 1"
by (auto dest: prime_elem_powerD)
end
lemma irreducible_mult_unit_left:
"is_unit a ⟹ irreducible (a * p) ⟷ irreducible p"
by (auto simp: irreducible_altdef mult.commute[of a] is_unit_mult_iff
mult_unit_dvd_iff dvd_mult_unit_iff)
lemma prime_elem_mult_unit_left:
"is_unit a ⟹ prime_elem (a * p) ⟷ prime_elem p"
by (auto simp: prime_elem_def mult.commute[of a] is_unit_mult_iff mult_unit_dvd_iff)
lemma prime_elem_dvd_cases:
assumes pk: "p*k dvd m*n" and p: "prime_elem p"
shows "(∃x. k dvd x*n ∧ m = p*x) ∨ (∃y. k dvd m*y ∧ n = p*y)"
proof -
have "p dvd m*n" using dvd_mult_left pk by blast
then consider "p dvd m" | "p dvd n"
using p prime_elem_dvd_mult_iff by blast
then show ?thesis
proof cases
case 1 then obtain a where "m = p * a" by (metis dvd_mult_div_cancel)
then have "∃x. k dvd x * n ∧ m = p * x"
using p pk by (auto simp: mult.assoc)
then show ?thesis ..
next
case 2 then obtain b where "n = p * b" by (metis dvd_mult_div_cancel)
with p pk have "∃y. k dvd m*y ∧ n = p*y"
by (metis dvd_mult_right dvd_times_left_cancel_iff mult.left_commute mult_zero_left)
then show ?thesis ..
qed
qed
lemma prime_elem_power_dvd_prod:
assumes pc: "p^c dvd m*n" and p: "prime_elem p"
shows "∃a b. a+b = c ∧ p^a dvd m ∧ p^b dvd n"
using pc
proof (induct c arbitrary: m n)
case 0 show ?case by simp
next
case (Suc c)
consider x where "p^c dvd x*n" "m = p*x" | y where "p^c dvd m*y" "n = p*y"
using prime_elem_dvd_cases [of _ "p^c", OF _ p] Suc.prems by force
then show ?case
proof cases
case (1 x)
with Suc.hyps[of x n] obtain a b where "a + b = c ∧ p ^ a dvd x ∧ p ^ b dvd n" by blast
with 1 have "Suc a + b = Suc c ∧ p ^ Suc a dvd m ∧ p ^ b dvd n"
by (auto intro: mult_dvd_mono)
thus ?thesis by blast
next
case (2 y)
with Suc.hyps[of m y] obtain a b where "a + b = c ∧ p ^ a dvd m ∧ p ^ b dvd y" by blast
with 2 have "a + Suc b = Suc c ∧ p ^ a dvd m ∧ p ^ Suc b dvd n"
by (auto intro: mult_dvd_mono)
with Suc.hyps [of m y] show "∃a b. a + b = Suc c ∧ p ^ a dvd m ∧ p ^ b dvd n"
by blast
qed
qed
lemma prime_elem_power_dvd_cases:
assumes "p ^ c dvd m * n" and "a + b = Suc c" and "prime_elem p"
shows "p ^ a dvd m ∨ p ^ b dvd n"
proof -
from assms obtain r s
where "r + s = c ∧ p ^ r dvd m ∧ p ^ s dvd n"
by (blast dest: prime_elem_power_dvd_prod)
moreover with assms have
"a ≤ r ∨ b ≤ s" by arith
ultimately show ?thesis by (auto intro: power_le_dvd)
qed
lemma prime_elem_not_unit' [simp]:
"ASSUMPTION (prime_elem x) ⟹ ¬is_unit x"
unfolding ASSUMPTION_def by (rule prime_elem_not_unit)
lemma prime_elem_dvd_power_iff:
assumes "prime_elem p"
shows "p dvd a ^ n ⟷ p dvd a ∧ n > 0"
using assms by (induct n) (auto dest: prime_elem_not_unit prime_elem_dvd_multD)
lemma prime_power_dvd_multD:
assumes "prime_elem p"
assumes "p ^ n dvd a * b" and "n > 0" and "¬ p dvd a"
shows "p ^ n dvd b"
using ‹p ^ n dvd a * b› and ‹n > 0›
proof (induct n arbitrary: b)
case 0 then show ?case by simp
next
case (Suc n) show ?case
proof (cases "n = 0")
case True with Suc ‹prime_elem p› ‹¬ p dvd a› show ?thesis
by (simp add: prime_elem_dvd_mult_iff)
next
case False then have "n > 0" by simp
from ‹prime_elem p› have "p ≠ 0" by auto
from Suc.prems have *: "p * p ^ n dvd a * b"
by simp
then have "p dvd a * b"
by (rule dvd_mult_left)
with Suc ‹prime_elem p› ‹¬ p dvd a› have "p dvd b"
by (simp add: prime_elem_dvd_mult_iff)
moreover define c where "c = b div p"
ultimately have b: "b = p * c" by simp
with * have "p * p ^ n dvd p * (a * c)"
by (simp add: ac_simps)
with ‹p ≠ 0› have "p ^ n dvd a * c"
by simp
with Suc.hyps ‹n > 0› have "p ^ n dvd c"
by blast
with ‹p ≠ 0› show ?thesis
by (simp add: b)
qed
qed
end
subsection ‹Generalized primes: normalized prime elements›
context normalization_semidom
begin
lemma irreducible_normalized_divisors:
assumes "irreducible x" "y dvd x" "normalize y = y"
shows "y = 1 ∨ y = normalize x"
proof -
from assms have "is_unit y ∨ x dvd y" by (auto simp: irreducible_altdef)
thus ?thesis
proof (elim disjE)
assume "is_unit y"
hence "normalize y = 1" by (simp add: is_unit_normalize)
with assms show ?thesis by simp
next
assume "x dvd y"
with ‹y dvd x› have "normalize y = normalize x" by (rule associatedI)
with assms show ?thesis by simp
qed
qed
lemma irreducible_normalize_iff [simp]: "irreducible (normalize x) = irreducible x"
using irreducible_mult_unit_left[of "1 div unit_factor x" x]
by (cases "x = 0") (simp_all add: unit_div_commute)
lemma prime_elem_normalize_iff [simp]: "prime_elem (normalize x) = prime_elem x"
using prime_elem_mult_unit_left[of "1 div unit_factor x" x]
by (cases "x = 0") (simp_all add: unit_div_commute)
lemma prime_elem_associated:
assumes "prime_elem p" and "prime_elem q" and "q dvd p"
shows "normalize q = normalize p"
using ‹q dvd p› proof (rule associatedI)
from ‹prime_elem q› have "¬ is_unit q"
by (auto simp add: prime_elem_not_unit)
with ‹prime_elem p› ‹q dvd p› show "p dvd q"
by (blast intro: prime_elemD2)
qed
definition prime :: "'a ⇒ bool" where
"prime p ⟷ prime_elem p ∧ normalize p = p"
lemma not_prime_0 [simp]: "¬prime 0" by (simp add: prime_def)
lemma not_prime_unit: "is_unit x ⟹ ¬prime x"
using prime_elem_not_unit[of x] by (auto simp add: prime_def)
lemma not_prime_1 [simp]: "¬prime 1" by (simp add: not_prime_unit)
lemma primeI: "prime_elem x ⟹ normalize x = x ⟹ prime x"
by (simp add: prime_def)
lemma prime_imp_prime_elem [dest]: "prime p ⟹ prime_elem p"
by (simp add: prime_def)
lemma normalize_prime: "prime p ⟹ normalize p = p"
by (simp add: prime_def)
lemma prime_normalize_iff [simp]: "prime (normalize p) ⟷ prime_elem p"
by (auto simp add: prime_def)
lemma prime_power_iff:
"prime (p ^ n) ⟷ prime p ∧ n = 1"
by (auto simp: prime_def prime_elem_power_iff)
lemma prime_imp_nonzero [simp]:
"ASSUMPTION (prime x) ⟹ x ≠ 0"
unfolding ASSUMPTION_def prime_def by auto
lemma prime_imp_not_one [simp]:
"ASSUMPTION (prime x) ⟹ x ≠ 1"
unfolding ASSUMPTION_def by auto
lemma prime_not_unit' [simp]:
"ASSUMPTION (prime x) ⟹ ¬is_unit x"
unfolding ASSUMPTION_def prime_def by auto
lemma prime_normalize' [simp]: "ASSUMPTION (prime x) ⟹ normalize x = x"
unfolding ASSUMPTION_def prime_def by simp
lemma unit_factor_prime: "prime x ⟹ unit_factor x = 1"
using unit_factor_normalize[of x] unfolding prime_def by auto
lemma unit_factor_prime' [simp]: "ASSUMPTION (prime x) ⟹ unit_factor x = 1"
unfolding ASSUMPTION_def by (rule unit_factor_prime)
lemma prime_imp_prime_elem' [simp]: "ASSUMPTION (prime x) ⟹ prime_elem x"
by (simp add: prime_def ASSUMPTION_def)
lemma prime_dvd_multD: "prime p ⟹ p dvd a * b ⟹ p dvd a ∨ p dvd b"
by (intro prime_elem_dvd_multD) simp_all
lemma prime_dvd_mult_iff: "prime p ⟹ p dvd a * b ⟷ p dvd a ∨ p dvd b"
by (auto dest: prime_dvd_multD)
lemma prime_dvd_power:
"prime p ⟹ p dvd x ^ n ⟹ p dvd x"
by (auto dest!: prime_elem_dvd_power simp: prime_def)
lemma prime_dvd_power_iff:
"prime p ⟹ n > 0 ⟹ p dvd x ^ n ⟷ p dvd x"
by (subst prime_elem_dvd_power_iff) simp_all
lemma prime_dvd_prod_mset_iff: "prime p ⟹ p dvd prod_mset A ⟷ (∃x. x ∈# A ∧ p dvd x)"
by (induction A) (simp_all add: prime_elem_dvd_mult_iff prime_imp_prime_elem, blast+)
lemma prime_dvd_prod_iff: "finite A ⟹ prime p ⟹ p dvd prod f A ⟷ (∃x∈A. p dvd f x)"
by (auto simp: prime_dvd_prod_mset_iff prod_unfold_prod_mset)
lemma primes_dvd_imp_eq:
assumes "prime p" "prime q" "p dvd q"
shows "p = q"
proof -
from assms have "irreducible q" by (simp add: prime_elem_imp_irreducible prime_def)
from irreducibleD'[OF this ‹p dvd q›] assms have "q dvd p" by simp
with ‹p dvd q› have "normalize p = normalize q" by (rule associatedI)
with assms show "p = q" by simp
qed
lemma prime_dvd_prod_mset_primes_iff:
assumes "prime p" "⋀q. q ∈# A ⟹ prime q"
shows "p dvd prod_mset A ⟷ p ∈# A"
proof -
from assms(1) have "p dvd prod_mset A ⟷ (∃x. x ∈# A ∧ p dvd x)" by (rule prime_dvd_prod_mset_iff)
also from assms have "… ⟷ p ∈# A" by (auto dest: primes_dvd_imp_eq)
finally show ?thesis .
qed
lemma prod_mset_primes_dvd_imp_subset:
assumes "prod_mset A dvd prod_mset B" "⋀p. p ∈# A ⟹ prime p" "⋀p. p ∈# B ⟹ prime p"
shows "A ⊆# B"
using assms
proof (induction A arbitrary: B)
case empty
thus ?case by simp
next
case (add p A B)
hence p: "prime p" by simp
define B' where "B' = B - {#p#}"
from add.prems have "p dvd prod_mset B" by (simp add: dvd_mult_left)
with add.prems have "p ∈# B"
by (subst (asm) (2) prime_dvd_prod_mset_primes_iff) simp_all
hence B: "B = B' + {#p#}" by (simp add: B'_def)
from add.prems p have "A ⊆# B'" by (intro add.IH) (simp_all add: B)
thus ?case by (simp add: B)
qed
lemma prod_mset_dvd_prod_mset_primes_iff:
assumes "⋀x. x ∈# A ⟹ prime x" "⋀x. x ∈# B ⟹ prime x"
shows "prod_mset A dvd prod_mset B ⟷ A ⊆# B"
using assms by (auto intro: prod_mset_subset_imp_dvd prod_mset_primes_dvd_imp_subset)
lemma is_unit_prod_mset_primes_iff:
assumes "⋀x. x ∈# A ⟹ prime x"
shows "is_unit (prod_mset A) ⟷ A = {#}"
by (auto simp add: is_unit_prod_mset_iff)
(meson all_not_in_conv assms not_prime_unit set_mset_eq_empty_iff)
lemma prod_mset_primes_irreducible_imp_prime:
assumes irred: "irreducible (prod_mset A)"
assumes A: "⋀x. x ∈# A ⟹ prime x"
assumes B: "⋀x. x ∈# B ⟹ prime x"
assumes C: "⋀x. x ∈# C ⟹ prime x"
assumes dvd: "prod_mset A dvd prod_mset B * prod_mset C"
shows "prod_mset A dvd prod_mset B ∨ prod_mset A dvd prod_mset C"
proof -
from dvd have "prod_mset A dvd prod_mset (B + C)"
by simp
with A B C have subset: "A ⊆# B + C"
by (subst (asm) prod_mset_dvd_prod_mset_primes_iff) auto
define A1 and A2 where "A1 = A ∩# B" and "A2 = A - A1"
have "A = A1 + A2" unfolding A1_def A2_def
by (rule sym, intro subset_mset.add_diff_inverse) simp_all
from subset have "A1 ⊆# B" "A2 ⊆# C"
by (auto simp: A1_def A2_def Multiset.subset_eq_diff_conv Multiset.union_commute)
from ‹A = A1 + A2› have "prod_mset A = prod_mset A1 * prod_mset A2" by simp
from irred and this have "is_unit (prod_mset A1) ∨ is_unit (prod_mset A2)"
by (rule irreducibleD)
with A have "A1 = {#} ∨ A2 = {#}" unfolding A1_def A2_def
by (subst (asm) (1 2) is_unit_prod_mset_primes_iff) (auto dest: Multiset.in_diffD)
with dvd ‹A = A1 + A2› ‹A1 ⊆# B› ‹A2 ⊆# C› show ?thesis
by (auto intro: prod_mset_subset_imp_dvd)
qed
lemma prod_mset_primes_finite_divisor_powers:
assumes A: "⋀x. x ∈# A ⟹ prime x"
assumes B: "⋀x. x ∈# B ⟹ prime x"
assumes "A ≠ {#}"
shows "finite {n. prod_mset A ^ n dvd prod_mset B}"
proof -
from ‹A ≠ {#}› obtain x where x: "x ∈# A" by blast
define m where "m = count B x"
have "{n. prod_mset A ^ n dvd prod_mset B} ⊆ {..m}"
proof safe
fix n assume dvd: "prod_mset A ^ n dvd prod_mset B"
from x have "x ^ n dvd prod_mset A ^ n" by (intro dvd_power_same dvd_prod_mset)
also note dvd
also have "x ^ n = prod_mset (replicate_mset n x)" by simp
finally have "replicate_mset n x ⊆# B"
by (rule prod_mset_primes_dvd_imp_subset) (insert A B x, simp_all split: if_splits)
thus "n ≤ m" by (simp add: count_le_replicate_mset_subset_eq m_def)
qed
moreover have "finite {..m}" by simp
ultimately show ?thesis by (rule finite_subset)
qed
end
subsection ‹In a semiring with GCD, each irreducible element is a prime element›
context semiring_gcd
begin
lemma irreducible_imp_prime_elem_gcd:
assumes "irreducible x"
shows "prime_elem x"
proof (rule prime_elemI)
fix a b assume "x dvd a * b"
from dvd_productE[OF this] obtain y z where yz: "x = y * z" "y dvd a" "z dvd b" .
from ‹irreducible x› and ‹x = y * z› have "is_unit y ∨ is_unit z" by (rule irreducibleD)
with yz show "x dvd a ∨ x dvd b"
by (auto simp: mult_unit_dvd_iff mult_unit_dvd_iff')
qed (insert assms, auto simp: irreducible_not_unit)
lemma prime_elem_imp_coprime:
assumes "prime_elem p" "¬p dvd n"
shows "coprime p n"
proof (rule coprimeI)
fix d assume "d dvd p" "d dvd n"
show "is_unit d"
proof (rule ccontr)
assume "¬is_unit d"
from ‹prime_elem p› and ‹d dvd p› and this have "p dvd d"
by (rule prime_elemD2)
from this and ‹d dvd n› have "p dvd n" by (rule dvd_trans)
with ‹¬p dvd n› show False by contradiction
qed
qed
lemma prime_imp_coprime:
assumes "prime p" "¬p dvd n"
shows "coprime p n"
using assms by (simp add: prime_elem_imp_coprime)
lemma prime_elem_imp_power_coprime:
"prime_elem p ⟹ ¬ p dvd a ⟹ coprime a (p ^ m)"
by (cases "m > 0") (auto dest: prime_elem_imp_coprime simp add: ac_simps)
lemma prime_imp_power_coprime:
"prime p ⟹ ¬ p dvd a ⟹ coprime a (p ^ m)"
by (rule prime_elem_imp_power_coprime) simp_all
lemma prime_elem_divprod_pow:
assumes p: "prime_elem p" and ab: "coprime a b" and pab: "p^n dvd a * b"
shows "p^n dvd a ∨ p^n dvd b"
using assms
proof -
from p have "¬ is_unit p"
by simp
with ab p have "¬ p dvd a ∨ ¬ p dvd b"
using not_coprimeI by blast
with p have "coprime (p ^ n) a ∨ coprime (p ^ n) b"
by (auto dest: prime_elem_imp_power_coprime simp add: ac_simps)
with pab show ?thesis
by (auto simp add: coprime_dvd_mult_left_iff coprime_dvd_mult_right_iff)
qed
lemma primes_coprime:
"prime p ⟹ prime q ⟹ p ≠ q ⟹ coprime p q"
using prime_imp_coprime primes_dvd_imp_eq by blast
end
subsection ‹Factorial semirings: algebraic structures with unique prime factorizations›
class factorial_semiring = normalization_semidom +
assumes prime_factorization_exists:
"x ≠ 0 ⟹ ∃A. (∀x. x ∈# A ⟶ prime_elem x) ∧ normalize (prod_mset A) = normalize x"
text ‹Alternative characterization›
lemma (in normalization_semidom) factorial_semiring_altI_aux:
assumes finite_divisors: "⋀x. x ≠ 0 ⟹ finite {y. y dvd x ∧ normalize y = y}"
assumes irreducible_imp_prime_elem: "⋀x. irreducible x ⟹ prime_elem x"
assumes "x ≠ 0"
shows "∃A. (∀x. x ∈# A ⟶ prime_elem x) ∧ normalize (prod_mset A) = normalize x"
using ‹x ≠ 0›
proof (induction "card {b. b dvd x ∧ normalize b = b}" arbitrary: x rule: less_induct)
case (less a)
let ?fctrs = "λa. {b. b dvd a ∧ normalize b = b}"
show ?case
proof (cases "is_unit a")
case True
thus ?thesis by (intro exI[of _ "{#}"]) (auto simp: is_unit_normalize)
next
case False
show ?thesis
proof (cases "∃b. b dvd a ∧ ¬is_unit b ∧ ¬a dvd b")
case False
with ‹¬is_unit a› less.prems have "irreducible a" by (auto simp: irreducible_altdef)
hence "prime_elem a" by (rule irreducible_imp_prime_elem)
thus ?thesis by (intro exI[of _ "{#normalize a#}"]) auto
next
case True
then obtain b where b: "b dvd a" "¬ is_unit b" "¬ a dvd b" by auto
from b have "?fctrs b ⊆ ?fctrs a" by (auto intro: dvd_trans)
moreover from b have "normalize a ∉ ?fctrs b" "normalize a ∈ ?fctrs a" by simp_all
hence "?fctrs b ≠ ?fctrs a" by blast
ultimately have "?fctrs b ⊂ ?fctrs a" by (subst subset_not_subset_eq) blast
with finite_divisors[OF ‹a ≠ 0›] have "card (?fctrs b) < card (?fctrs a)"
by (rule psubset_card_mono)
moreover from ‹a ≠ 0› b have "b ≠ 0" by auto
ultimately have "∃A. (∀x. x ∈# A ⟶ prime_elem x) ∧ normalize (prod_mset A) = normalize b"
by (intro less) auto
then obtain A where A: "(∀x. x ∈# A ⟶ prime_elem x) ∧ normalize (∏⇩# A) = normalize b"
by auto
define c where "c = a div b"
from b have c: "a = b * c" by (simp add: c_def)
from less.prems c have "c ≠ 0" by auto
from b c have "?fctrs c ⊆ ?fctrs a" by (auto intro: dvd_trans)
moreover have "normalize a ∉ ?fctrs c"
proof safe
assume "normalize a dvd c"
hence "b * c dvd 1 * c" by (simp add: c)
hence "b dvd 1" by (subst (asm) dvd_times_right_cancel_iff) fact+
with b show False by simp
qed
with ‹normalize a ∈ ?fctrs a› have "?fctrs a ≠ ?fctrs c" by blast
ultimately have "?fctrs c ⊂ ?fctrs a" by (subst subset_not_subset_eq) blast
with finite_divisors[OF ‹a ≠ 0›] have "card (?fctrs c) < card (?fctrs a)"
by (rule psubset_card_mono)
with ‹c ≠ 0› have "∃A. (∀x. x ∈# A ⟶ prime_elem x) ∧ normalize (prod_mset A) = normalize c"
by (intro less) auto
then obtain B where B: "(∀x. x ∈# B ⟶ prime_elem x) ∧ normalize (∏⇩# B) = normalize c"
by auto
show ?thesis
proof (rule exI[of _ "A + B"]; safe)
have "normalize (prod_mset (A + B)) =
normalize (normalize (prod_mset A) * normalize (prod_mset B))"
by simp
also have "… = normalize (b * c)"
by (simp only: A B) auto
also have "b * c = a"
using c by simp
finally show "normalize (prod_mset (A + B)) = normalize a" .
next
qed (use A B in auto)
qed
qed
qed
lemma factorial_semiring_altI:
assumes finite_divisors: "⋀x::'a. x ≠ 0 ⟹ finite {y. y dvd x ∧ normalize y = y}"
assumes irreducible_imp_prime: "⋀x::'a. irreducible x ⟹ prime_elem x"
shows "OFCLASS('a :: normalization_semidom, factorial_semiring_class)"
by intro_classes (rule factorial_semiring_altI_aux[OF assms])
text ‹Properties›
context factorial_semiring
begin
lemma prime_factorization_exists':
assumes "x ≠ 0"
obtains A where "⋀x. x ∈# A ⟹ prime x" "normalize (prod_mset A) = normalize x"
proof -
from prime_factorization_exists[OF assms] obtain A
where A: "⋀x. x ∈# A ⟹ prime_elem x" "normalize (prod_mset A) = normalize x" by blast
define A' where "A' = image_mset normalize A"
have "normalize (prod_mset A') = normalize (prod_mset A)"
by (simp add: A'_def normalize_prod_mset_normalize)
also note A(2)
finally have "normalize (prod_mset A') = normalize x" by simp
moreover from A(1) have "∀x. x ∈# A' ⟶ prime x" by (auto simp: prime_def A'_def)
ultimately show ?thesis by (intro that[of A']) blast
qed
lemma irreducible_imp_prime_elem:
assumes "irreducible x"
shows "prime_elem x"
proof (rule prime_elemI)
fix a b assume dvd: "x dvd a * b"
from assms have "x ≠ 0" by auto
show "x dvd a ∨ x dvd b"
proof (cases "a = 0 ∨ b = 0")
case False
hence "a ≠ 0" "b ≠ 0" by blast+
note nz = ‹x ≠ 0› this
from nz[THEN prime_factorization_exists'] obtain A B C
where ABC:
"⋀z. z ∈# A ⟹ prime z"
"normalize (∏⇩# A) = normalize x"
"⋀z. z ∈# B ⟹ prime z"
"normalize (∏⇩# B) = normalize a"
"⋀z. z ∈# C ⟹ prime z"
"normalize (∏⇩# C) = normalize b"
by this blast
have "irreducible (prod_mset A)"
by (subst irreducible_cong[OF ABC(2)]) fact
moreover have "normalize (prod_mset A) dvd
normalize (normalize (prod_mset B) * normalize (prod_mset C))"
unfolding ABC using dvd by simp
hence "prod_mset A dvd prod_mset B * prod_mset C"
unfolding normalize_mult_normalize_left normalize_mult_normalize_right by simp
ultimately have "prod_mset A dvd prod_mset B ∨ prod_mset A dvd prod_mset C"
by (intro prod_mset_primes_irreducible_imp_prime) (use ABC in auto)
hence "normalize (prod_mset A) dvd normalize (prod_mset B) ∨
normalize (prod_mset A) dvd normalize (prod_mset C)" by simp
thus ?thesis unfolding ABC by simp
qed auto
qed (use assms in ‹simp_all add: irreducible_def›)
lemma finite_divisor_powers:
assumes "y ≠ 0" "¬is_unit x"
shows "finite {n. x ^ n dvd y}"
proof (cases "x = 0")
case True
with assms have "{n. x ^ n dvd y} = {0}" by (auto simp: power_0_left)
thus ?thesis by simp
next
case False
note nz = this ‹y ≠ 0›
from nz[THEN prime_factorization_exists'] obtain A B
where AB:
"⋀z. z ∈# A ⟹ prime z"
"normalize (∏⇩# A) = normalize x"
"⋀z. z ∈# B ⟹ prime z"
"normalize (∏⇩# B) = normalize y"
by this blast
from AB assms have "A ≠ {#}" by (auto simp: normalize_1_iff)
from AB(2,4) prod_mset_primes_finite_divisor_powers [of A B, OF AB(1,3) this]
have "finite {n. prod_mset A ^ n dvd prod_mset B}" by simp
also have "{n. prod_mset A ^ n dvd prod_mset B} =
{n. normalize (normalize (prod_mset A) ^ n) dvd normalize (prod_mset B)}"
unfolding normalize_power_normalize by simp
also have "… = {n. x ^ n dvd y}"
unfolding AB unfolding normalize_power_normalize by simp
finally show ?thesis .
qed
lemma finite_prime_divisors:
assumes "x ≠ 0"
shows "finite {p. prime p ∧ p dvd x}"
proof -
from prime_factorization_exists'[OF assms] obtain A
where A: "⋀z. z ∈# A ⟹ prime z" "normalize (∏⇩# A) = normalize x" by this blast
have "{p. prime p ∧ p dvd x} ⊆ set_mset A"
proof safe
fix p assume p: "prime p" and dvd: "p dvd x"
from dvd have "p dvd normalize x" by simp
also from A have "normalize x = normalize (prod_mset A)" by simp
finally have "p dvd prod_mset A"
by simp
thus "p ∈# A" using p A
by (subst (asm) prime_dvd_prod_mset_primes_iff)
qed
moreover have "finite (set_mset A)" by simp
ultimately show ?thesis by (rule finite_subset)
qed
lemma infinite_unit_divisor_powers:
assumes "y ≠ 0"
assumes "is_unit x"
shows "infinite {n. x^n dvd y}"
proof -
from ‹is_unit x› have "is_unit (x^n)" for n
using is_unit_power_iff by auto
hence "x^n dvd y" for n
by auto
hence "{n. x^n dvd y} = UNIV"
by auto
thus ?thesis
by auto
qed
corollary is_unit_iff_infinite_divisor_powers:
assumes "y ≠ 0"
shows "is_unit x ⟷ infinite {n. x^n dvd y}"
using infinite_unit_divisor_powers finite_divisor_powers assms by auto
lemma prime_elem_iff_irreducible: "prime_elem x ⟷ irreducible x"
by (blast intro: irreducible_imp_prime_elem prime_elem_imp_irreducible)
lemma prime_divisor_exists:
assumes "a ≠ 0" "¬is_unit a"
shows "∃b. b dvd a ∧ prime b"
proof -
from prime_factorization_exists'[OF assms(1)]
obtain A where A: "⋀z. z ∈# A ⟹ prime z" "normalize (∏⇩# A) = normalize a"
by this blast
with assms have "A ≠ {#}" by auto
then obtain x where "x ∈# A" by blast
with A(1) have *: "x dvd normalize (prod_mset A)" "prime x"
by (auto simp: dvd_prod_mset)
hence "x dvd a" by (simp add: A(2))
with * show ?thesis by blast
qed
lemma prime_divisors_induct [case_names zero unit factor]:
assumes "P 0" "⋀x. is_unit x ⟹ P x" "⋀p x. prime p ⟹ P x ⟹ P (p * x)"
shows "P x"
proof (cases "x = 0")
case False
from prime_factorization_exists'[OF this]
obtain A where A: "⋀z. z ∈# A ⟹ prime z" "normalize (∏⇩# A) = normalize x"
by this blast
from A obtain u where u: "is_unit u" "x = u * prod_mset A"
by (elim associatedE2)
from A(1) have "P (u * prod_mset A)"
proof (induction A)
case (add p A)
from add.prems have "prime p" by simp
moreover from add.prems have "P (u * prod_mset A)" by (intro add.IH) simp_all
ultimately have "P (p * (u * prod_mset A))" by (rule assms(3))
thus ?case by (simp add: mult_ac)
qed (simp_all add: assms False u)
with A u show ?thesis by simp
qed (simp_all add: assms(1))
lemma no_prime_divisors_imp_unit:
assumes "a ≠ 0" "⋀b. b dvd a ⟹ normalize b = b ⟹ ¬ prime_elem b"
shows "is_unit a"
proof (rule ccontr)
assume "¬is_unit a"
from prime_divisor_exists[OF assms(1) this] obtain b where "b dvd a" "prime b" by auto
with assms(2)[of b] show False by (simp add: prime_def)
qed
lemma prime_divisorE:
assumes "a ≠ 0" and "¬ is_unit a"
obtains p where "prime p" and "p dvd a"
using assms no_prime_divisors_imp_unit unfolding prime_def by blast
definition multiplicity :: "'a ⇒ 'a ⇒ nat" where
"multiplicity p x = (if finite {n. p ^ n dvd x} then Max {n. p ^ n dvd x} else 0)"
lemma multiplicity_dvd: "p ^ multiplicity p x dvd x"
proof (cases "finite {n. p ^ n dvd x}")
case True
hence "multiplicity p x = Max {n. p ^ n dvd x}"
by (simp add: multiplicity_def)
also have "… ∈ {n. p ^ n dvd x}"
by (rule Max_in) (auto intro!: True exI[of _ "0::nat"])
finally show ?thesis by simp
qed (simp add: multiplicity_def)
lemma multiplicity_dvd': "n ≤ multiplicity p x ⟹ p ^ n dvd x"
by (rule dvd_trans[OF le_imp_power_dvd multiplicity_dvd])
context
fixes x p :: 'a
assumes xp: "x ≠ 0" "¬is_unit p"
begin
lemma multiplicity_eq_Max: "multiplicity p x = Max {n. p ^ n dvd x}"
using finite_divisor_powers[OF xp] by (simp add: multiplicity_def)
lemma multiplicity_geI:
assumes "p ^ n dvd x"
shows "multiplicity p x ≥ n"
proof -
from assms have "n ≤ Max {n. p ^ n dvd x}"
by (intro Max_ge finite_divisor_powers xp) simp_all
thus ?thesis by (subst multiplicity_eq_Max)
qed
lemma multiplicity_lessI:
assumes "¬p ^ n dvd x"
shows "multiplicity p x < n"
proof (rule ccontr)
assume "¬(n > multiplicity p x)"
hence "p ^ n dvd x" by (intro multiplicity_dvd') simp
with assms show False by contradiction
qed
lemma power_dvd_iff_le_multiplicity:
"p ^ n dvd x ⟷ n ≤ multiplicity p x"
using multiplicity_geI[of n] multiplicity_lessI[of n] by (cases "p ^ n dvd x") auto
lemma multiplicity_eq_zero_iff:
shows "multiplicity p x = 0 ⟷ ¬p dvd x"
using power_dvd_iff_le_multiplicity[of 1] by auto
lemma multiplicity_gt_zero_iff:
shows "multiplicity p x > 0 ⟷ p dvd x"
using power_dvd_iff_le_multiplicity[of 1] by auto
lemma multiplicity_decompose:
"¬p dvd (x div p ^ multiplicity p x)"
proof
assume *: "p dvd x div p ^ multiplicity p x"
have "x = x div p ^ multiplicity p x * (p ^ multiplicity p x)"
using multiplicity_dvd[of p x] by simp
also from * have "x div p ^ multiplicity p x = (x div p ^ multiplicity p x div p) * p" by simp
also have "x div p ^ multiplicity p x div p * p * p ^ multiplicity p x =
x div p ^ multiplicity p x div p * p ^ Suc (multiplicity p x)"
by (simp add: mult_assoc)
also have "p ^ Suc (multiplicity p x) dvd …" by (rule dvd_triv_right)
finally show False by (subst (asm) power_dvd_iff_le_multiplicity) simp
qed
lemma multiplicity_decompose':
obtains y where "x = p ^ multiplicity p x * y" "¬p dvd y"
using that[of "x div p ^ multiplicity p x"]
by (simp add: multiplicity_decompose multiplicity_dvd)
end
lemma multiplicity_zero [simp]: "multiplicity p 0 = 0"
by (simp add: multiplicity_def)
lemma prime_elem_multiplicity_eq_zero_iff:
"prime_elem p ⟹ x ≠ 0 ⟹ multiplicity p x = 0 ⟷ ¬p dvd x"
by (rule multiplicity_eq_zero_iff) simp_all
lemma prime_multiplicity_other:
assumes "prime p" "prime q" "p ≠ q"
shows "multiplicity p q = 0"
using assms by (subst prime_elem_multiplicity_eq_zero_iff) (auto dest: primes_dvd_imp_eq)
lemma prime_multiplicity_gt_zero_iff:
"prime_elem p ⟹ x ≠ 0 ⟹ multiplicity p x > 0 ⟷ p dvd x"
by (rule multiplicity_gt_zero_iff) simp_all
lemma multiplicity_unit_left: "is_unit p ⟹ multiplicity p x = 0"
by (simp add: multiplicity_def is_unit_power_iff unit_imp_dvd)
lemma multiplicity_unit_right:
assumes "is_unit x"
shows "multiplicity p x = 0"
proof (cases "is_unit p ∨ x = 0")
case False
with multiplicity_lessI[of x p 1] this assms
show ?thesis by (auto dest: dvd_unit_imp_unit)
qed (auto simp: multiplicity_unit_left)
lemma multiplicity_one [simp]: "multiplicity p 1 = 0"
by (rule multiplicity_unit_right) simp_all
lemma multiplicity_eqI:
assumes "p ^ n dvd x" "¬p ^ Suc n dvd x"
shows "multiplicity p x = n"
proof -
consider "x = 0" | "is_unit p" | "x ≠ 0" "¬is_unit p" by blast
thus ?thesis
proof cases
assume xp: "x ≠ 0" "¬is_unit p"
from xp assms(1) have "multiplicity p x ≥ n" by (intro multiplicity_geI)
moreover from assms(2) xp have "multiplicity p x < Suc n" by (intro multiplicity_lessI)
ultimately show ?thesis by simp
next
assume "is_unit p"
hence "is_unit (p ^ Suc n)" by (simp add: is_unit_power_iff del: power_Suc)
hence "p ^ Suc n dvd x" by (rule unit_imp_dvd)
with ‹¬p ^ Suc n dvd x› show ?thesis by contradiction
qed (insert assms, simp_all)
qed
context
fixes x p :: 'a
assumes xp: "x ≠ 0" "¬is_unit p"
begin
lemma multiplicity_times_same:
assumes "p ≠ 0"
shows "multiplicity p (p * x) = Suc (multiplicity p x)"
proof (rule multiplicity_eqI)
show "p ^ Suc (multiplicity p x) dvd p * x"
by (auto intro!: mult_dvd_mono multiplicity_dvd)
from xp assms show "¬ p ^ Suc (Suc (multiplicity p x)) dvd p * x"
using power_dvd_iff_le_multiplicity[OF xp, of "Suc (multiplicity p x)"] by simp
qed
end
lemma multiplicity_same_power': "multiplicity p (p ^ n) = (if p = 0 ∨ is_unit p then 0 else n)"
proof -
consider "p = 0" | "is_unit p" |"p ≠ 0" "¬is_unit p" by blast
thus ?thesis
proof cases
assume "p ≠ 0" "¬is_unit p"
thus ?thesis by (induction n) (simp_all add: multiplicity_times_same)
qed (simp_all add: power_0_left multiplicity_unit_left)
qed
lemma multiplicity_same_power:
"p ≠ 0 ⟹ ¬is_unit p ⟹ multiplicity p (p ^ n) = n"
by (simp add: multiplicity_same_power')
lemma multiplicity_prime_elem_times_other:
assumes "prime_elem p" "¬p dvd q"
shows "multiplicity p (q * x) = multiplicity p x"
proof (cases "x = 0")
case False
show ?thesis
proof (rule multiplicity_eqI)
have "1 * p ^ multiplicity p x dvd q * x"
by (intro mult_dvd_mono multiplicity_dvd) simp_all
thus "p ^ multiplicity p x dvd q * x" by simp
next
define n where "n = multiplicity p x"
from assms have "¬is_unit p" by simp
from multiplicity_decompose'[OF False this]
obtain y where y [folded n_def]: "x = p ^ multiplicity p x * y" "¬ p dvd y" .
from y have "p ^ Suc n dvd q * x ⟷ p ^ n * p dvd p ^ n * (q * y)" by (simp add: mult_ac)
also from assms have "… ⟷ p dvd q * y" by simp
also have "… ⟷ p dvd q ∨ p dvd y" by (rule prime_elem_dvd_mult_iff) fact+
also from assms y have "… ⟷ False" by simp
finally show "¬(p ^ Suc n dvd q * x)" by blast
qed
qed simp_all
lemma multiplicity_self:
assumes "p ≠ 0" "¬is_unit p"
shows "multiplicity p p = 1"
proof -
from assms have "multiplicity p p = Max {n. p ^ n dvd p}"
by (simp add: multiplicity_eq_Max)
also from assms have "p ^ n dvd p ⟷ n ≤ 1" for n
using dvd_power_iff[of p n 1] by auto
hence "{n. p ^ n dvd p} = {..1}" by auto
also have "… = {0,1}" by auto
finally show ?thesis by simp
qed
lemma multiplicity_times_unit_left:
assumes "is_unit c"
shows "multiplicity (c * p) x = multiplicity p x"
proof -
from assms have "{n. (c * p) ^ n dvd x} = {n. p ^ n dvd x}"
by (subst mult.commute) (simp add: mult_unit_dvd_iff power_mult_distrib is_unit_power_iff)
thus ?thesis by (simp add: multiplicity_def)
qed
lemma multiplicity_times_unit_right:
assumes "is_unit c"
shows "multiplicity p (c * x) = multiplicity p x"
proof -
from assms have "{n. p ^ n dvd c * x} = {n. p ^ n dvd x}"
by (subst mult.commute) (simp add: dvd_mult_unit_iff)
thus ?thesis by (simp add: multiplicity_def)
qed
lemma multiplicity_normalize_left [simp]:
"multiplicity (normalize p) x = multiplicity p x"
proof (cases "p = 0")
case [simp]: False
have "normalize p = (1 div unit_factor p) * p"
by (simp add: unit_div_commute is_unit_unit_factor)
also have "multiplicity … x = multiplicity p x"
by (rule multiplicity_times_unit_left) (simp add: is_unit_unit_factor)
finally show ?thesis .
qed simp_all
lemma multiplicity_normalize_right [simp]:
"multiplicity p (normalize x) = multiplicity p x"
proof (cases "x = 0")
case [simp]: False
have "normalize x = (1 div unit_factor x) * x"
by (simp add: unit_div_commute is_unit_unit_factor)
also have "multiplicity p … = multiplicity p x"
by (rule multiplicity_times_unit_right) (simp add: is_unit_unit_factor)
finally show ?thesis .
qed simp_all
lemma multiplicity_prime [simp]: "prime_elem p ⟹ multiplicity p p = 1"
by (rule multiplicity_self) auto
lemma multiplicity_prime_power [simp]: "prime_elem p ⟹ multiplicity p (p ^ n) = n"
by (subst multiplicity_same_power') auto
lift_definition prime_factorization :: "'a ⇒ 'a multiset" is
"λx p. if prime p then multiplicity p x else 0"
proof -
fix x :: 'a
show "finite {p. 0 < (if prime p then multiplicity p x else 0)}" (is "finite ?A")
proof (cases "x = 0")
case False
from False have "?A ⊆ {p. prime p ∧ p dvd x}"
by (auto simp: multiplicity_gt_zero_iff)
moreover from False have "finite {p. prime p ∧ p dvd x}"
by (rule finite_prime_divisors)
ultimately show ?thesis by (rule finite_subset)
qed simp_all
qed
abbreviation prime_factors :: "'a ⇒ 'a set" where
"prime_factors a ≡ set_mset (prime_factorization a)"
lemma count_prime_factorization_nonprime:
"¬prime p ⟹ count (prime_factorization x) p = 0"
by transfer simp
lemma count_prime_factorization_prime:
"prime p ⟹ count (prime_factorization x) p = multiplicity p x"
by transfer simp
lemma count_prime_factorization:
"count (prime_factorization x) p = (if prime p then multiplicity p x else 0)"
by transfer simp
lemma dvd_imp_multiplicity_le:
assumes "a dvd b" "b ≠ 0"
shows "multiplicity p a ≤ multiplicity p b"
proof (cases "is_unit p")
case False
with assms show ?thesis
by (intro multiplicity_geI ) (auto intro: dvd_trans[OF multiplicity_dvd' assms(1)])
qed (insert assms, auto simp: multiplicity_unit_left)
lemma prime_power_inj:
assumes "prime a" "a ^ m = a ^ n"
shows "m = n"
proof -
have "multiplicity a (a ^ m) = multiplicity a (a ^ n)" by (simp only: assms)
thus ?thesis using assms by (subst (asm) (1 2) multiplicity_prime_power) simp_all
qed
lemma prime_power_inj':
assumes "prime p" "prime q"
assumes "p ^ m = q ^ n" "m > 0" "n > 0"
shows "p = q" "m = n"
proof -
from assms have "p ^ 1 dvd p ^ m" by (intro le_imp_power_dvd) simp
also have "p ^ m = q ^ n" by fact
finally have "p dvd q ^ n" by simp
with assms have "p dvd q" using prime_dvd_power[of p q] by simp
with assms show "p = q" by (simp add: primes_dvd_imp_eq)
with assms show "m = n" by (simp add: prime_power_inj)
qed
lemma prime_power_eq_one_iff [simp]: "prime p ⟹ p ^ n = 1 ⟷ n = 0"
using prime_power_inj[of p n 0] by auto
lemma one_eq_prime_power_iff [simp]: "prime p ⟹ 1 = p ^ n ⟷ n = 0"
using prime_power_inj[of p 0 n] by auto
lemma prime_power_inj'':
assumes "prime p" "prime q"
shows "p ^ m = q ^ n ⟷ (m = 0 ∧ n = 0) ∨ (p = q ∧ m = n)"
using assms
by (cases "m = 0"; cases "n = 0")
(auto dest: prime_power_inj'[OF assms])
lemma prime_factorization_0 [simp]: "prime_factorization 0 = {#}"
by (simp add: multiset_eq_iff count_prime_factorization)
lemma prime_factorization_empty_iff:
"prime_factorization x = {#} ⟷ x = 0 ∨ is_unit x"
proof
assume *: "prime_factorization x = {#}"
{
assume x: "x ≠ 0" "¬is_unit x"
{
fix p assume p: "prime p"
have "count (prime_factorization x) p = 0" by (simp add: *)
also from p have "count (prime_factorization x) p = multiplicity p x"
by (rule count_prime_factorization_prime)
also from x p have "… = 0 ⟷ ¬p dvd x" by (simp add: multiplicity_eq_zero_iff)
finally have "¬p dvd x" .
}
with prime_divisor_exists[OF x] have False by blast
}
thus "x = 0 ∨ is_unit x" by blast
next
assume "x = 0 ∨ is_unit x"
thus "prime_factorization x = {#}"
proof
assume x: "is_unit x"
{
fix p assume p: "prime p"
from p x have "multiplicity p x = 0"
by (subst multiplicity_eq_zero_iff)
(auto simp: multiplicity_eq_zero_iff dest: unit_imp_no_prime_divisors)
}
thus ?thesis by (simp add: multiset_eq_iff count_prime_factorization)
qed simp_all
qed
lemma prime_factorization_unit:
assumes "is_unit x"
shows "prime_factorization x = {#}"
proof (rule multiset_eqI)
fix p :: 'a
show "count (prime_factorization x) p = count {#} p"
proof (cases "prime p")
case True
with assms have "multiplicity p x = 0"
by (subst multiplicity_eq_zero_iff)
(auto simp: multiplicity_eq_zero_iff dest: unit_imp_no_prime_divisors)
with True show ?thesis by (simp add: count_prime_factorization_prime)
qed (simp_all add: count_prime_factorization_nonprime)
qed
lemma prime_factorization_1 [simp]: "prime_factorization 1 = {#}"
by (simp add: prime_factorization_unit)
lemma prime_factorization_times_prime:
assumes "x ≠ 0" "prime p"
shows "prime_factorization (p * x) = {#p#} + prime_factorization x"
proof (rule multiset_eqI)
fix q :: 'a
consider "¬prime q" | "p = q" | "prime q" "p ≠ q" by blast
thus "count (prime_factorization (p * x)) q = count ({#p#} + prime_factorization x) q"
proof cases
assume q: "prime q" "p ≠ q"
with assms primes_dvd_imp_eq[of q p] have "¬q dvd p" by auto
with q assms show ?thesis
by (simp add: multiplicity_prime_elem_times_other count_prime_factorization)
qed (insert assms, auto simp: count_prime_factorization multiplicity_times_same)
qed
lemma prod_mset_prime_factorization_weak:
assumes "x ≠ 0"
shows "normalize (prod_mset (prime_factorization x)) = normalize x"
using assms
proof (induction x rule: prime_divisors_induct)
case (factor p x)
have "normalize (prod_mset (prime_factorization (p * x))) =
normalize (p * normalize (prod_mset (prime_factorization x)))"
using factor.prems factor.hyps by (simp add: prime_factorization_times_prime)
also have "normalize (prod_mset (prime_factorization x)) = normalize x"
by (rule factor.IH) (use factor in auto)
finally show ?case by simp
qed (auto simp: prime_factorization_unit is_unit_normalize)
lemma in_prime_factors_iff:
"p ∈ prime_factors x ⟷ x ≠ 0 ∧ p dvd x ∧ prime p"
proof -
have "p ∈ prime_factors x ⟷ count (prime_factorization x) p > 0" by simp
also have "… ⟷ x ≠ 0 ∧ p dvd x ∧ prime p"
by (subst count_prime_factorization, cases "x = 0")
(auto simp: multiplicity_eq_zero_iff multiplicity_gt_zero_iff)
finally show ?thesis .
qed
lemma in_prime_factors_imp_prime [intro]:
"p ∈ prime_factors x ⟹ prime p"
by (simp add: in_prime_factors_iff)
lemma in_prime_factors_imp_dvd [dest]:
"p ∈ prime_factors x ⟹ p dvd x"
by (simp add: in_prime_factors_iff)
lemma prime_factorsI:
"x ≠ 0 ⟹ prime p ⟹ p dvd x ⟹ p ∈ prime_factors x"
by (auto simp: in_prime_factors_iff)
lemma prime_factors_dvd:
"x ≠ 0 ⟹ prime_factors x = {p. prime p ∧ p dvd x}"
by (auto intro: prime_factorsI)
lemma prime_factors_multiplicity:
"prime_factors n = {p. prime p ∧ multiplicity p n > 0}"
by (cases "n = 0") (auto simp add: prime_factors_dvd prime_multiplicity_gt_zero_iff)
lemma prime_factorization_prime:
assumes "prime p"
shows "prime_factorization p = {#p#}"
proof (rule multiset_eqI)
fix q :: 'a
consider "¬prime q" | "q = p" | "prime q" "q ≠ p" by blast
thus "count (prime_factorization p) q = count {#p#} q"
by cases (insert assms, auto dest: primes_dvd_imp_eq
simp: count_prime_factorization multiplicity_self multiplicity_eq_zero_iff)
qed
lemma prime_factorization_prod_mset_primes:
assumes "⋀p. p ∈# A ⟹ prime p"
shows "prime_factorization (prod_mset A) = A"
using assms
proof (induction A)
case (add p A)
from add.prems[of 0] have "0 ∉# A" by auto
hence "prod_mset A ≠ 0" by auto
with add show ?case
by (simp_all add: mult_ac prime_factorization_times_prime Multiset.union_commute)
qed simp_all
lemma prime_factorization_cong:
"normalize x = normalize y ⟹ prime_factorization x = prime_factorization y"
by (simp add: multiset_eq_iff count_prime_factorization
multiplicity_normalize_right [of _ x, symmetric]
multiplicity_normalize_right [of _ y, symmetric]
del: multiplicity_normalize_right)
lemma prime_factorization_unique:
assumes "x ≠ 0" "y ≠ 0"
shows "prime_factorization x = prime_factorization y ⟷ normalize x = normalize y"
proof
assume "prime_factorization x = prime_factorization y"
hence "prod_mset (prime_factorization x) = prod_mset (prime_factorization y)" by simp
hence "normalize (prod_mset (prime_factorization x)) =
normalize (prod_mset (prime_factorization y))"
by (simp only: )
with assms show "normalize x = normalize y"
by (simp add: prod_mset_prime_factorization_weak)
qed (rule prime_factorization_cong)
lemma prime_factorization_normalize [simp]:
"prime_factorization (normalize x) = prime_factorization x"
by (cases "x = 0", simp, subst prime_factorization_unique) auto
lemma prime_factorization_eqI_strong:
assumes "⋀p. p ∈# P ⟹ prime p" "prod_mset P = n"
shows "prime_factorization n = P"
using prime_factorization_prod_mset_primes[of P] assms by simp
lemma prime_factorization_eqI:
assumes "⋀p. p ∈# P ⟹ prime p" "normalize (prod_mset P) = normalize n"
shows "prime_factorization n = P"
proof -
have "P = prime_factorization (normalize (prod_mset P))"
using prime_factorization_prod_mset_primes[of P] assms(1) by simp
with assms(2) show ?thesis by simp
qed
lemma prime_factorization_mult:
assumes "x ≠ 0" "y ≠ 0"
shows "prime_factorization (x * y) = prime_factorization x + prime_factorization y"
proof -
have "normalize (prod_mset (prime_factorization x) * prod_mset (prime_factorization y)) =
normalize (normalize (prod_mset (prime_factorization x)) *
normalize (prod_mset (prime_factorization y)))"
by (simp only: normalize_mult_normalize_left normalize_mult_normalize_right)
also have "… = normalize (x * y)"
by (subst (1 2) prod_mset_prime_factorization_weak) (use assms in auto)
finally show ?thesis
by (intro prime_factorization_eqI) auto
qed
lemma prime_factorization_prod:
assumes "finite A" "⋀x. x ∈ A ⟹ f x ≠ 0"
shows "prime_factorization (prod f A) = (∑n∈A. prime_factorization (f n))"
using assms by (induction A rule: finite_induct)
(auto simp: Sup_multiset_empty prime_factorization_mult)
lemma prime_elem_multiplicity_mult_distrib:
assumes "prime_elem p" "x ≠ 0" "y ≠ 0"
shows "multiplicity p (x * y) = multiplicity p x + multiplicity p y"
proof -
have "multiplicity p (x * y) = count (prime_factorization (x * y)) (normalize p)"
by (subst count_prime_factorization_prime) (simp_all add: assms)
also from assms
have "prime_factorization (x * y) = prime_factorization x + prime_factorization y"
by (intro prime_factorization_mult)
also have "count … (normalize p) =
count (prime_factorization x) (normalize p) + count (prime_factorization y) (normalize p)"
by simp
also have "… = multiplicity p x + multiplicity p y"