(* 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 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) 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 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 private 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 normalize_prod_mset_primes: "(⋀p. p ∈# A ⟹ prime p) ⟹ normalize (prod_mset A) = prod_mset A" proof (induction A) case (add p A) hence "prime p" by simp hence "normalize p = p" by simp with add show ?case by (simp add: normalize_mult) qed simp_all 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) ∧ 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) ∧ 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 guess b by (elim exE conjE) note b = this 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) ∧ prod_mset A = normalize b" by (intro less) auto then guess A .. note A = this 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) ∧ prod_mset A = normalize c" by (intro less) auto then guess B .. note B = this from A B show ?thesis by (intro exI[of _ "A + B"]) (auto simp: c normalize_mult) 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" "prod_mset A = normalize x" proof - from prime_factorization_exists[OF assms] obtain A where A: "⋀x. x ∈# A ⟹ prime_elem x" "prod_mset A = normalize x" by blast define A' where "A' = image_mset normalize A" have "prod_mset A' = normalize (prod_mset A)" by (simp add: A'_def normalize_prod_mset) also note A(2) finally have "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'] guess A B C . note ABC = this from assms ABC have "irreducible (prod_mset A)" by simp from dvd prod_mset_primes_irreducible_imp_prime[of A B C, OF this ABC(1,3,5)] ABC(2,4,6) show ?thesis by (simp add: normalize_mult [symmetric]) qed auto qed (insert assms, 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'] guess A B . note AB = this 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] show ?thesis by (simp add: normalize_power [symmetric]) qed lemma finite_prime_divisors: assumes "x ≠ 0" shows "finite {p. prime p ∧ p dvd x}" proof - from prime_factorization_exists'[OF assms] guess A . note A = this 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 = prod_mset A" by simp finally show "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 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)] guess A . note A = this moreover from A and assms have "A ≠ {#}" by auto then obtain x where "x ∈# A" by blast with A(1) have *: "x dvd prod_mset A" "prime x" by (auto simp: dvd_prod_mset) with A have "x dvd a" by simp 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] guess A . note A = this from A(1) have "P (unit_factor x * prod_mset A)" proof (induction A) case (add p A) from add.prems have "prime p" by simp moreover from add.prems have "P (unit_factor x * prod_mset A)" by (intro add.IH) simp_all ultimately have "P (p * (unit_factor x * prod_mset A))" by (rule assms(3)) thus ?case by (simp add: mult_ac) qed (simp_all add: assms False) with A 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] guess b by (elim exE conjE) 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] guess y . note y = this [folded n_def] 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" unfolding multiset_def proof clarify 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: assumes "x ≠ 0" shows "prod_mset (prime_factorization x) = normalize x" using assms by (induction x rule: prime_divisors_induct) (simp_all add: prime_factorization_unit prime_factorization_times_prime is_unit_normalize normalize_mult) 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 with assms show "normalize x = normalize y" by (simp add: prod_mset_prime_factorization) qed (rule prime_factorization_cong) lemma prime_factorization_eqI: 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_mult: assumes "x ≠ 0" "y ≠ 0" shows "prime_factorization (x * y) = prime_factorization x + prime_factorization y" proof - have "prime_factorization (prod_mset (prime_factorization (x * y))) = prime_factorization (prod_mset (prime_factorization x + prime_factorization y))" by (simp add: prod_mset_prime_factorization assms normalize_mult) also have "prime_factorization (prod_mset (prime_factorization (x * y))) = prime_factorization (x * y)" by (rule prime_factorization_prod_mset_primes) (simp_all add: in_prime_factors_imp_prime) also have "prime_factorization (prod_mset (prime_factorization x + prime_factorization y)) = prime_factorization x + prime_factorization y" by (rule prime_factorization_prod_mset_primes) (auto simp: in_prime_factors_imp_prime) finally show ?thesis . 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" by (subst (1 2) count_prime_factorization_prime) (simp_all add: assms) finally show ?thesis . qed lemma prime_elem_multiplicity_prod_mset_distrib: assumes "prime_elem p" "0 ∉# A" shows "multiplicity p (prod_mset A) = sum_mset (image_mset (multiplicity p) A)" using assms by (induction A) (auto simp: prime_elem_multiplicity_mult_distrib) lemma prime_elem_multiplicity_power_distrib: assumes "prime_elem p" "x ≠ 0" shows "multiplicity p (x ^ n) = n * multiplicity p x" using assms prime_elem_multiplicity_prod_mset_distrib [of p "replicate_mset n x"] by simp lemma prime_elem_multiplicity_prod_distrib: assumes "prime_elem p" "0 ∉ f ` A" "finite A" shows "multiplicity p (prod f A) = (∑x∈A. multiplicity p (f x))" proof - have "multiplicity p (prod f A) = (∑x∈#mset_set A. multiplicity p (f x))" using assms by (subst prod_unfold_prod_mset) (simp_all add: prime_elem_multiplicity_prod_mset_distrib sum_unfold_sum_mset multiset.map_comp o_def) also from ‹finite A› have "… = (∑x∈A. multiplicity p (f x))" by (induction A rule: finite_induct) simp_all finally show ?thesis . qed lemma multiplicity_distinct_prime_power: "prime p ⟹ prime q ⟹ p ≠ q ⟹ multiplicity p (q ^ n) = 0" by (subst prime_elem_multiplicity_power_distrib) (auto simp: prime_multiplicity_other) lemma prime_factorization_prime_power: "prime p ⟹ prime_factorization (p ^ n) = replicate_mset n p" by (induction n) (simp_all add: prime_factorization_mult prime_factorization_prime Multiset.union_commute) lemma prime_decomposition: "unit_factor x * prod_mset (prime_factorization x) = x" by (cases "x = 0") (simp_all add: prod_mset_prime_factorization) lemma prime_factorization_subset_iff_dvd: assumes [simp]: "x ≠ 0" "y ≠ 0" shows "prime_factorization x ⊆# prime_factorization y ⟷ x dvd y" proof - have "x dvd y ⟷ prod_mset (prime_factorization x) dvd prod_mset (prime_factorization y)" by (simp add: prod_mset_prime_factorization) also have "… ⟷ prime_factorization x ⊆# prime_factorization y" by (auto intro!: prod_mset_primes_dvd_imp_subset prod_mset_subset_imp_dvd) finally show ?thesis .. qed lemma prime_factorization_subset_imp_dvd: "x ≠ 0 ⟹ (prime_factorization x ⊆# prime_factorization y) ⟹ x dvd y" by (cases "y = 0") (simp_all add: prime_factorization_subset_iff_dvd) lemma prime_factorization_divide: assumes "b dvd a" shows "prime_factorization (a div b) = prime_factorization a - prime_factorization b" proof (cases "a = 0") case [simp]: False from assms have [simp]: "b ≠ 0" by auto have "prime_factorization ((a div b) * b) = prime_factorization (a div b) + prime_factorization b" by (intro prime_factorization_mult) (insert assms, auto elim!: dvdE) with assms show ?thesis by simp qed simp_all lemma zero_not_in_prime_factors [simp]: "0 ∉ prime_factors x" by (auto dest: in_prime_factors_imp_prime) lemma prime_prime_factors: "prime p ⟹ prime_factors p = {p}" by (drule prime_factorization_prime) simp lemma prod_prime_factors: assumes "x ≠ 0" shows "(∏p ∈ prime_factors x. p ^ multiplicity p x) = normalize x" proof - have "normalize x = prod_mset (prime_factorization x)" by (simp add: prod_mset_prime_factorization assms) also have "… = (∏p ∈ prime_factors x. p ^ count (prime_factorization x) p)" by (subst prod_mset_multiplicity) simp_all also have "… = (∏p ∈ prime_factors x. p ^ multiplicity p x)" by (intro prod.cong) (simp_all add: assms count_prime_factorization_prime in_prime_factors_imp_prime) finally show ?thesis .. qed lemma prime_factorization_unique'': assumes S_eq: "S = {p. 0 < f p}" and "finite S" and S: "∀p∈S. prime p" "normalize n = (∏p∈S. p ^ f p)" shows "S = prime_factors n ∧ (∀p. prime p ⟶ f p = multiplicity p n)" proof define A where "A = Abs_multiset f" from ‹finite S› S(1) have "(∏p∈S. p ^ f p) ≠ 0" by auto with S(2) have nz: "n ≠ 0" by auto from S_eq ‹finite S› have count_A: "count A = f" unfolding A_def by (subst multiset.Abs_multiset_inverse) (simp_all add: multiset_def) from S_eq count_A have set_mset_A: "set_mset A = S" by (simp only: set_mset_def) from S(2) have "normalize n = (∏p∈S. p ^ f p)" . also have "… = prod_mset A" by (simp add: prod_mset_multiplicity S_eq set_mset_A count_A) also from nz have "normalize n = prod_mset (prime_factorization n)" by (simp add: prod_mset_prime_factorization) finally have "prime_factorization (prod_mset A) = prime_factorization (prod_mset (prime_factorization n))" by simp also from S(1) have "prime_factorization (prod_mset A) = A" by (intro prime_factorization_prod_mset_primes) (auto simp: set_mset_A) also have "prime_factorization (prod_mset (prime_factorization n)) = prime_factorization n" by (intro prime_factorization_prod_mset_primes) auto finally show "S = prime_factors n" by (simp add: set_mset_A [symmetric]) show "(∀p. prime p ⟶ f p = multiplicity p n)" proof safe fix p :: 'a assume p: "prime p" have "multiplicity p n = multiplicity p (normalize n)" by simp also have "normalize n = prod_mset A" by (simp add: prod_mset_multiplicity S_eq set_mset_A count_A S) also from p set_mset_A S(1) have "multiplicity p … = sum_mset (image_mset (multiplicity p) A)" by (intro prime_elem_multiplicity_prod_mset_distrib) auto also from S(1) p have "image_mset (multiplicity p) A = image_mset (λq. if p = q then 1 else 0) A" by (intro image_mset_cong) (auto simp: set_mset_A multiplicity_self prime_multiplicity_other) also have "sum_mset … = f p" by (simp add: semiring_1_class.sum_mset_delta' count_A) finally show "f p = multiplicity p n" .. qed qed lemma prime_factors_product: "x ≠ 0 ⟹ y ≠ 0 ⟹ prime_factors (x * y) = prime_factors x ∪ prime_factors y" by (simp add: prime_factorization_mult) lemma dvd_prime_factors [intro]: "y ≠ 0 ⟹ x dvd y ⟹ prime_factors x ⊆ prime_factors y" by (intro set_mset_mono, subst prime_factorization_subset_iff_dvd) auto (* RENAMED multiplicity_dvd *) lemma multiplicity_le_imp_dvd: assumes "x ≠ 0" "⋀p. prime p ⟹ multiplicity p x ≤ multiplicity p y" shows "x dvd y" proof (cases "y = 0") case False from assms this have "prime_factorization x ⊆# prime_factorization y" by (intro mset_subset_eqI) (auto simp: count_prime_factorization) with assms False show ?thesis by (subst (asm) prime_factorization_subset_iff_dvd) qed auto lemma dvd_multiplicity_eq: "x ≠ 0 ⟹ y ≠ 0 ⟹ x dvd y ⟷ (∀p. multiplicity p x ≤ multiplicity p y)" by (auto intro: dvd_imp_multiplicity_le multiplicity_le_imp_dvd) lemma multiplicity_eq_imp_eq: assumes "x ≠ 0" "y ≠ 0" assumes "⋀p. prime p ⟹ multiplicity p x = multiplicity p y" shows "normalize x = normalize y" using assms by (intro associatedI multiplicity_le_imp_dvd) simp_all lemma prime_factorization_unique': assumes "∀p ∈# M. prime p" "∀p ∈# N. prime p" "(∏i ∈# M. i) = (∏i ∈# N. i)" shows "M = N" proof - have "prime_factorization (∏i ∈# M. i) = prime_factorization (∏i ∈# N. i)" by (simp only: assms) also from assms have "prime_factorization (∏i ∈# M. i) = M" by (subst prime_factorization_prod_mset_primes) simp_all also from assms have "prime_factorization (∏i ∈# N. i) = N" by (subst prime_factorization_prod_mset_primes) simp_all finally show ?thesis . qed lemma multiplicity_cong: "(⋀r. p ^ r dvd a ⟷ p ^ r dvd b) ⟹ multiplicity p a = multiplicity p b" by (simp add: multiplicity_def) lemma not_dvd_imp_multiplicity_0: assumes "¬p dvd x" shows "multiplicity p x = 0" proof - from assms have "multiplicity p x < 1" by (intro multiplicity_lessI) auto thus ?thesis by simp qed lemma inj_on_Prod_primes: assumes "⋀P p. P ∈ A ⟹ p ∈ P ⟹ prime p" assumes "⋀P. P ∈ A ⟹ finite P" shows "inj_on Prod A" proof (rule inj_onI) fix P Q assume PQ: "P ∈ A" "Q ∈ A" "∏P = ∏Q" with prime_factorization_unique'[of "mset_set P" "mset_set Q"] assms[of P] assms[of Q] have "mset_set P = mset_set Q" by (auto simp: prod_unfold_prod_mset) with assms[of P] assms[of Q] PQ show "P = Q" by simp qed lemma divides_primepow: assumes "prime p" and "a dvd p ^ n" obtains m where "m ≤ n" and "normalize a = p ^ m" proof - from assms have "a ≠ 0" by auto with assms have "prod_mset (prime_factorization a) dvd prod_mset (prime_factorization (p ^ n))" by (simp add: prod_mset_prime_factorization) then have "prime_factorization a ⊆# prime_factorization (p ^ n)" by (simp add: in_prime_factors_imp_prime prod_mset_dvd_prod_mset_primes_iff) with assms have "prime_factorization a ⊆# replicate_mset n p" by (simp add: prime_factorization_prime_power) then obtain m where "m ≤ n" and "prime_factorization a = replicate_mset m p" by (rule msubseteq_replicate_msetE) then have "prod_mset (prime_factorization a) = prod_mset (replicate_mset m p)" by simp with ‹a ≠ 0› have "normalize a = p ^ m" by (simp add: prod_mset_prime_factorization) with ‹m ≤ n› show thesis .. qed lemma divide_out_primepow_ex: assumes "n ≠ 0" "∃p∈prime_factors n. P p" obtains p k n' where "P p" "prime p" "p dvd n" "¬p dvd n'" "k > 0" "n = p ^ k * n'" proof - from assms obtain p where p: "P p" "prime p" "p dvd n" by auto define k where "k = multiplicity p n" define n' where "n' = n div p ^ k" have n': "n = p ^ k * n'" "¬p dvd n'" using assms p multiplicity_decompose[of n p] by (auto simp: n'_def k_def multiplicity_dvd) from n' p have "k > 0" by (intro Nat.gr0I) auto with n' p that[of p n' k] show ?thesis by auto qed lemma divide_out_primepow: assumes "n ≠ 0" "¬is_unit n" obtains p k n' where "prime p" "p dvd n" "¬p dvd n'" "k > 0" "n = p ^ k * n'" using divide_out_primepow_ex[OF assms(1), of "λ_. True"] prime_divisor_exists[OF assms] assms prime_factorsI by metis lemma Ex_other_prime_factor: assumes "n ≠ 0" and "¬(∃k. normalize n = p ^ k)" "prime p" shows "∃q∈prime_factors n. q ≠ p" proof (rule ccontr) assume *: "¬(∃q∈prime_factors n. q ≠ p)" have "normalize n = (∏p∈prime_factors n. p ^ multiplicity p n)" using assms(1) by (intro prod_prime_factors [symmetric]) auto also from * have "… = (∏p∈{p}. p ^ multiplicity p n)" using assms(3) by (intro prod.mono_neutral_left) (auto simp: prime_factors_multiplicity) finally have "normalize n = p ^ multiplicity p n" by auto with assms show False by auto qed subsection ‹GCD and LCM computation with unique factorizations› definition "gcd_factorial a b = (if a = 0 then normalize b else if b = 0 then normalize a else prod_mset (prime_factorization a ∩# prime_factorization b))" definition "lcm_factorial a b = (if a = 0 ∨ b = 0 then 0 else prod_mset (prime_factorization a ∪# prime_factorization b))" definition "Gcd_factorial A = (if A ⊆ {0} then 0 else prod_mset (Inf (prime_factorization ` (A - {0}))))" definition "Lcm_factorial A = (if A = {} then 1 else if 0 ∉ A ∧ subset_mset.bdd_above (prime_factorization ` (A - {0})) then prod_mset (Sup (prime_factorization ` A)) else 0)" lemma prime_factorization_gcd_factorial: assumes [simp]: "a ≠ 0" "b ≠ 0" shows "prime_factorization (gcd_factorial a b) = prime_factorization a ∩# prime_factorization b" proof - have "prime_factorization (gcd_factorial a b) = prime_factorization (prod_mset (prime_factorization a ∩# prime_factorization b))" by (simp add: gcd_factorial_def) also have "… = prime_factorization a ∩# prime_factorization b" by (subst prime_factorization_prod_mset_primes) auto finally show ?thesis . qed lemma prime_factorization_lcm_factorial: assumes [simp]: "a ≠ 0" "b ≠ 0" shows "prime_factorization (lcm_factorial a b) = prime_factorization a ∪# prime_factorization b" proof - have "prime_factorization (lcm_factorial a b) = prime_factorization (prod_mset (prime_factorization a ∪# prime_factorization b))" by (simp add: lcm_factorial_def) also have "… = prime_factorization a ∪# prime_factorization b" by (subst prime_factorization_prod_mset_primes) auto finally show ?thesis . qed lemma prime_factorization_Gcd_factorial: assumes "¬A ⊆ {0}" shows "prime_factorization (Gcd_factorial A) = Inf (prime_factorization ` (A - {0}))" proof - from assms obtain x where x: "x ∈ A - {0}" by auto hence "Inf (prime_factorization ` (A - {0})) ⊆# prime_factorization x" by (intro subset_mset.cInf_lower) simp_all hence "∀y. y ∈# Inf (prime_factorization ` (A - {0})) ⟶ y ∈ prime_factors x" by (auto dest: mset_subset_eqD) with in_prime_factors_imp_prime[of _ x] have "∀p. p ∈# Inf (prime_factorization ` (A - {0})) ⟶ prime p" by blast with assms show ?thesis by (simp add: Gcd_factorial_def prime_factorization_prod_mset_primes) qed lemma prime_factorization_Lcm_factorial: assumes "0 ∉ A" "subset_mset.bdd_above (prime_factorization ` A)" shows "prime_factorization (Lcm_factorial A) = Sup (prime_factorization ` A)" proof (cases "A = {}") case True hence "prime_factorization ` A = {}" by auto also have "Sup … = {#}" by (simp add: Sup_multiset_empty) finally show ?thesis by (simp add: Lcm_factorial_def) next case False have "∀y. y ∈# Sup (prime_factorization ` A) ⟶ prime y" by (auto simp: in_Sup_multiset_iff assms) with assms False show ?thesis by (simp add: Lcm_factorial_def prime_factorization_prod_mset_primes) qed lemma gcd_factorial_commute: "gcd_factorial a b = gcd_factorial b a" by (simp add: gcd_factorial_def multiset_inter_commute) lemma gcd_factorial_dvd1: "gcd_factorial a b dvd a" proof (cases "a = 0 ∨ b = 0") case False hence "gcd_factorial a b ≠ 0" by (auto simp: gcd_factorial_def) with False show ?thesis by (subst prime_factorization_subset_iff_dvd [symmetric]) (auto simp: prime_factorization_gcd_factorial) qed (auto simp: gcd_factorial_def) lemma gcd_factorial_dvd2: "gcd_factorial a b dvd b" by (subst gcd_factorial_commute) (rule gcd_factorial_dvd1) lemma normalize_gcd_factorial: "normalize (gcd_factorial a b) = gcd_factorial a b" proof - have "normalize (prod_mset (prime_factorization a ∩# prime_factorization b)) = prod_mset (prime_factorization a ∩# prime_factorization b)" by (intro normalize_prod_mset_primes) auto thus ?thesis by (simp add: gcd_factorial_def) qed lemma gcd_factorial_greatest: "c dvd gcd_factorial a b" if "c dvd a" "c dvd b" for a b c proof (cases "a = 0 ∨ b = 0") case False with that have [simp]: "c ≠ 0" by auto let ?p = "prime_factorization" from that False have "?p c ⊆# ?p a" "?p c ⊆# ?p b" by (simp_all add: prime_factorization_subset_iff_dvd) hence "prime_factorization c ⊆# prime_factorization (prod_mset (prime_factorization a ∩# prime_factorization b))" using False by (subst prime_factorization_prod_mset_primes) auto with False show ?thesis by (auto simp: gcd_factorial_def prime_factorization_subset_iff_dvd [symmetric]) qed (auto simp: gcd_factorial_def that) lemma lcm_factorial_gcd_factorial: "lcm_factorial a b = normalize (a * b) div gcd_factorial a b" for a b proof (cases "a = 0 ∨ b = 0") case False let ?p = "prime_factorization" from False have "prod_mset (?p (a * b)) div gcd_factorial a b = prod_mset (?p a + ?p b - ?p a ∩# ?p b)" by (subst prod_mset_diff) (auto simp: lcm_factorial_def gcd_factorial_def prime_factorization_mult subset_mset.le_infI1) also from False have "prod_mset (?p (a * b)) = normalize (a * b)" by (intro prod_mset_prime_factorization) simp_all also from False have "prod_mset (?p a + ?p b - ?p a ∩# ?p b) = lcm_factorial a b" by (simp add: union_diff_inter_eq_sup lcm_factorial_def) finally show ?thesis .. qed (auto simp: lcm_factorial_def) lemma normalize_Gcd_factorial: "normalize (Gcd_factorial A) = Gcd_factorial A" proof (cases "A ⊆ {0}") case False then obtain x where "x ∈ A" "x ≠ 0" by blast hence "Inf (prime_factorization ` (A - {0})) ⊆# prime_factorization x" by (intro subset_mset.cInf_lower) auto hence "prime p" if "p ∈# Inf (prime_factorization ` (A - {0}))" for p using that by (auto dest: mset_subset_eqD) with False show ?thesis by (auto simp add: Gcd_factorial_def normalize_prod_mset_primes) qed (simp_all add: Gcd_factorial_def) lemma Gcd_factorial_eq_0_iff: "Gcd_factorial A = 0 ⟷ A ⊆ {0}" by (auto simp: Gcd_factorial_def in_Inf_multiset_iff split: if_splits) lemma Gcd_factorial_dvd: assumes "x ∈ A" shows "Gcd_factorial A dvd x" proof (cases "x = 0") case False with assms have "prime_factorization (Gcd_factorial A) = Inf (prime_factorization ` (A - {0}))" by (intro prime_factorization_Gcd_factorial) auto also from False assms have "… ⊆# prime_factorization x" by (intro subset_mset.cInf_lower) auto finally show ?thesis by (subst (asm) prime_factorization_subset_iff_dvd) (insert assms False, auto simp: Gcd_factorial_eq_0_iff) qed simp_all lemma Gcd_factorial_greatest: assumes "⋀y. y ∈ A ⟹ x dvd y" shows "x dvd Gcd_factorial A" proof (cases "A ⊆ {0}") case False from False obtain y where "y ∈ A" "y ≠ 0" by auto with assms[of y] have nz: "x ≠ 0" by auto from nz assms have "prime_factorization x ⊆# prime_factorization y" if "y ∈ A - {0}" for y using that by (subst prime_factorization_subset_iff_dvd) auto with False have "prime_factorization x ⊆# Inf (prime_factorization ` (A - {0}))" by (intro subset_mset.cInf_greatest) auto also from False have "… = prime_factorization (Gcd_factorial A)" by (rule prime_factorization_Gcd_factorial [symmetric]) finally show ?thesis by (subst (asm) prime_factorization_subset_iff_dvd) (insert nz False, auto simp: Gcd_factorial_eq_0_iff) qed (simp_all add: Gcd_factorial_def) lemma normalize_Lcm_factorial: "normalize (Lcm_factorial A) = Lcm_factorial A" proof (cases "subset_mset.bdd_above (prime_factorization ` A)") case True hence "normalize (prod_mset (Sup (prime_factorization ` A))) = prod_mset (Sup (prime_factorization ` A))" by (intro normalize_prod_mset_primes) (auto simp: in_Sup_multiset_iff) with True show ?thesis by (simp add: Lcm_factorial_def) qed (auto simp: Lcm_factorial_def) lemma Lcm_factorial_eq_0_iff: "Lcm_factorial A = 0 ⟷ 0 ∈ A ∨ ¬subset_mset.bdd_above (prime_factorization ` A)" by (auto simp: Lcm_factorial_def in_Sup_multiset_iff) lemma dvd_Lcm_factorial: assumes "x ∈ A" shows "x dvd Lcm_factorial A" proof (cases "0 ∉ A ∧ subset_mset.bdd_above (prime_factorization ` A)") case True with assms have [simp]: "0 ∉ A" "x ≠ 0" "A ≠ {}" by auto from assms True have "prime_factorization x ⊆# Sup (prime_factorization ` A)" by (intro subset_mset.cSup_upper) auto also have "… = prime_factorization (Lcm_factorial A)" by (rule prime_factorization_Lcm_factorial [symmetric]) (insert True, simp_all) finally show ?thesis by (subst (asm) prime_factorization_subset_iff_dvd) (insert True, auto simp: Lcm_factorial_eq_0_iff) qed (insert assms, auto simp: Lcm_factorial_def) lemma Lcm_factorial_least: assumes "⋀y. y ∈ A ⟹ y dvd x" shows "Lcm_factorial A dvd x" proof - consider "A = {}" | "0 ∈ A" | "x = 0" | "A ≠ {}" "0 ∉ A" "x ≠ 0" by blast thus ?thesis proof cases assume *: "A ≠ {}" "0 ∉ A" "x ≠ 0" hence nz: "x ≠ 0" if "x ∈ A" for x using that by auto from * have bdd: "subset_mset.bdd_above (prime_factorization ` A)" by (intro subset_mset.bdd_aboveI[of _ "prime_factorization x"]) (auto simp: prime_factorization_subset_iff_dvd nz dest: assms) have "prime_factorization (Lcm_factorial A) = Sup (prime_factorization ` A)" by (rule prime_factorization_Lcm_factorial) fact+ also from * have "… ⊆# prime_factorization x" by (intro subset_mset.cSup_least) (auto simp: prime_factorization_subset_iff_dvd nz dest: assms) finally show ?thesis by (subst (asm) prime_factorization_subset_iff_dvd) (insert * bdd, auto simp: Lcm_factorial_eq_0_iff) qed (auto simp: Lcm_factorial_def dest: assms) qed lemmas gcd_lcm_factorial = gcd_factorial_dvd1 gcd_factorial_dvd2 gcd_factorial_greatest normalize_gcd_factorial lcm_factorial_gcd_factorial normalize_Gcd_factorial Gcd_factorial_dvd Gcd_factorial_greatest normalize_Lcm_factorial dvd_Lcm_factorial Lcm_factorial_least end class factorial_semiring_gcd = factorial_semiring + gcd + Gcd + assumes gcd_eq_gcd_factorial: "gcd a b = gcd_factorial a b" and lcm_eq_lcm_factorial: "lcm a b = lcm_factorial a b" and Gcd_eq_Gcd_factorial: "Gcd A = Gcd_factorial A" and Lcm_eq_Lcm_factorial: "Lcm A = Lcm_factorial A" begin lemma prime_factorization_gcd: assumes [simp]: "a ≠ 0" "b ≠ 0" shows "prime_factorization (gcd a b) = prime_factorization a ∩# prime_factorization b" by (simp add: gcd_eq_gcd_factorial prime_factorization_gcd_factorial) lemma prime_factorization_lcm: assumes [simp]: "a ≠ 0" "b ≠ 0" shows "prime_factorization (lcm a b) = prime_factorization a ∪# prime_factorization b" by (simp add: lcm_eq_lcm_factorial prime_factorization_lcm_factorial) lemma prime_factorization_Gcd: assumes "Gcd A ≠ 0" shows "prime_factorization (Gcd A) = Inf (prime_factorization ` (A - {0}))" using assms by (simp add: prime_factorization_Gcd_factorial Gcd_eq_Gcd_factorial Gcd_factorial_eq_0_iff) lemma prime_factorization_Lcm: assumes "Lcm A ≠ 0" shows "prime_factorization (Lcm A) = Sup (prime_factorization ` A)" using assms by (simp add: prime_factorization_Lcm_factorial Lcm_eq_Lcm_factorial Lcm_factorial_eq_0_iff) lemma prime_factors_gcd [simp]: "a ≠ 0 ⟹ b ≠ 0 ⟹ prime_factors (gcd a b) = prime_factors a ∩ prime_factors b" by (subst prime_factorization_gcd) auto lemma prime_factors_lcm [simp]: "a ≠ 0 ⟹ b ≠ 0 ⟹ prime_factors (lcm a b) = prime_factors a ∪ prime_factors b" by (subst prime_factorization_lcm) auto subclass semiring_gcd by (standard, unfold gcd_eq_gcd_factorial lcm_eq_lcm_factorial) (rule gcd_lcm_factorial; assumption)+ subclass semiring_Gcd by (standard, unfold Gcd_eq_Gcd_factorial Lcm_eq_Lcm_factorial) (rule gcd_lcm_factorial; assumption)+ lemma assumes "x ≠ 0" "y ≠ 0" shows gcd_eq_factorial': "gcd x y = (∏p ∈ prime_factors x ∩ prime_factors y. p ^ min (multiplicity p x) (multiplicity p y))" (is "_ = ?rhs1") and lcm_eq_factorial': "lcm x y = (∏p ∈ prime_factors x ∪ prime_factors y. p ^ max (multiplicity p x) (multiplicity p y))" (is "_ = ?rhs2") proof - have "gcd x y = gcd_factorial x y" by (rule gcd_eq_gcd_factorial) also have "… = ?rhs1" by (auto simp: gcd_factorial_def assms prod_mset_multiplicity count_prime_factorization_prime dest: in_prime_factors_imp_prime intro!: prod.cong) finally show "gcd x y = ?rhs1" . have "lcm x y = lcm_factorial x y" by (rule lcm_eq_lcm_factorial) also have "… = ?rhs2" by (auto simp: lcm_factorial_def assms prod_mset_multiplicity count_prime_factorization_prime dest: in_prime_factors_imp_prime intro!: prod.cong) finally show "lcm x y = ?rhs2" . qed lemma assumes "x ≠ 0" "y ≠ 0" "prime p" shows multiplicity_gcd: "multiplicity p (gcd x y) = min (multiplicity p x) (multiplicity p y)" and multiplicity_lcm: "multiplicity p (lcm x y) = max (multiplicity p x) (multiplicity p y)" proof - have "gcd x y = gcd_factorial x y" by (rule gcd_eq_gcd_factorial) also from assms have "multiplicity p … = min (multiplicity p x) (multiplicity p y)" by (simp add: count_prime_factorization_prime [symmetric] prime_factorization_gcd_factorial) finally show "multiplicity p (gcd x y) = min (multiplicity p x) (multiplicity p y)" . have "lcm x y = lcm_factorial x y" by (rule lcm_eq_lcm_factorial) also from assms have "multiplicity p … = max (multiplicity p x) (multiplicity p y)" by (simp add: count_prime_factorization_prime [symmetric] prime_factorization_lcm_factorial) finally show "multiplicity p (lcm x y) = max (multiplicity p x) (multiplicity p y)" . qed lemma gcd_lcm_distrib: "gcd x (lcm y z) = lcm (gcd x y) (gcd x z)" proof (cases "x = 0 ∨ y = 0 ∨ z = 0") case True thus ?thesis by (auto simp: lcm_proj1_if_dvd lcm_proj2_if_dvd) next case False hence "normalize (gcd x (lcm y z)) = normalize (lcm (gcd x y) (gcd x z))" by (intro associatedI prime_factorization_subset_imp_dvd) (auto simp: lcm_eq_0_iff prime_factorization_gcd prime_factorization_lcm subset_mset.inf_sup_distrib1) thus ?thesis by simp qed lemma lcm_gcd_distrib: "lcm x (gcd y z) = gcd (lcm x y) (lcm x z)" proof (cases "x = 0 ∨ y = 0 ∨ z = 0") case True thus ?thesis by (auto simp: lcm_proj1_if_dvd lcm_proj2_if_dvd) next case False hence "normalize (lcm x (gcd y z)) = normalize (gcd (lcm x y) (lcm x z))" by (intro associatedI prime_factorization_subset_imp_dvd) (auto simp: lcm_eq_0_iff prime_factorization_gcd prime_factorization_lcm subset_mset.sup_inf_distrib1) thus ?thesis by simp qed end class factorial_ring_gcd = factorial_semiring_gcd + idom begin subclass ring_gcd .. subclass idom_divide .. end end