(* Title: HOL/Computational_Algebra/Factorial_Ring.thy Author: Manuel Eberl, TU Muenchen Author: Florian Haftmann, TU Muenchen *) 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 (* TODO Move *) 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"