Theory HOL-Computational_Algebra.Factorial_Ring

(*  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›)

lemma irreducible_multD:
  assumes l: "irreducible (a*b)"
  shows "a dvd 1 ∧ irreducible b ∨ b dvd 1 ∧ irreducible a"
proof-
  have *: "irreducible b" if l: "irreducible (a*b)" and a: "a dvd 1" for a b :: 'a
  proof (rule irreducibleI)
    show "¬(b dvd 1)"
    proof
      assume "b dvd 1"
      hence "a * b dvd 1 * 1"
        using ‹a dvd 1› by (intro mult_dvd_mono) auto
      with l show False
        by (auto simp: irreducible_def)
    qed
  next
    fix x y assume "b = x * y"
    have "a * x dvd 1 ∨ y dvd 1"
      using l by (rule irreducibleD) (use ‹b = x * y› in ‹auto simp: mult_ac›)
    thus "x dvd 1 ∨ y dvd 1"
      by auto
  qed (use l a in auto)

  from irreducibleD[OF assms refl] have "a dvd 1 ∨ b dvd 1"
    by (auto simp: irreducible_def)
  with *[of a b] *[of b a] l show ?thesis
    by (auto simp: mult.commute)
qed

lemma irreducible_power_iff [simp]:
  "irreducible (p ^ n) ⟷ irreducible p ∧ n = 1"
proof
  assume *: "irreducible (p ^ n)"
  have "irreducible p"
    using * by (induction n) (auto dest!: irreducible_multD)
  hence [simp]: "¬p dvd 1"
    using * by (auto simp: irreducible_def)

  consider "n = 0" | "n = 1" | "n > 1"
    by linarith
  thus "irreducible p ∧ n = 1"
  proof cases
    assume "n > 1"
    hence "p ^ n = p * p ^ (n - 1)"
      by (cases n) auto
    with * ‹¬ p dvd 1› have "p ^ (n - 1) dvd 1"
      using irreducible_multD[of p "p ^ (n - 1)"] by auto
    with ‹¬p dvd 1› and ‹n > 1› have False
      by (meson dvd_power dvd_trans zero_less_diff)
    thus ?thesis ..
  qed (use * in auto)
qed auto


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"
    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_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 ⟷
    normalize (prod_mset (prime_factorization x)) dvd normalize (prod_mset (prime_factorization y))"
    using assms by (subst (1 2) prod_mset_prime_factorization_weak) auto
  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 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 prime_factorization_unique'':
  assumes "∀p ∈# M. prime p" "∀p ∈# N. prime p" "normalize (∏i ∈# M. i) = normalize (∏i ∈# N. i)"
  shows   "M = N"
proof -
  have "prime_factorization (normalize (∏i ∈# M. i)) =
        prime_factorization (normalize (∏i ∈# N. i))"
    by (simp only: assms)
  also from assms have "prime_factorization (normalize (∏i ∈# M. i)) = M"
    by (subst prime_factorization_normalize, subst prime_factorization_prod_mset_primes) simp_all
  also from assms have "prime_factorization (normalize (∏i ∈# N. i)) = N"
    by (subst prime_factorization_normalize, 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 multiplicity_zero_left [simp]: "multiplicity 0 x = 0"
 by (cases "x = 0") (auto intro: not_dvd_imp_multiplicity_0)

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_weak:
  assumes "prime p" and "a dvd p ^ n"
  obtains m where "m ≤ n" and "normalize a = normalize (p ^ m)"
proof -
  from assms have "a ≠ 0"
    by auto
  with assms
  have "normalize (prod_mset (prime_factorization a)) dvd
          normalize (prod_mset (prime_factorization (p ^ n)))"
    by (subst (1 2) prod_mset_prime_factorization_weak) auto
  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 *: "normalize (prod_mset (prime_factorization a)) =
                  normalize (prod_mset (replicate_mset m p))" by metis
  also have "normalize (prod_mset (prime_factorization a)) = normalize a"
    using ‹a ≠ 0› by (simp add: prod_mset_prime_factorization_weak)
  also have "prod_mset (replicate_mset m p) = p ^ m"
    by simp
  finally show ?thesis using ‹m ≤ n› 
    by (intro that[of m])
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


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 normalize (prod_mset (prime_factorization a ∩# prime_factorization b)))"

definition "lcm_factorial a b = (if a = 0 ∨ b = 0 then 0
     else normalize (prod_mset (prime_factorization a ∪# prime_factorization b)))"

definition "Gcd_factorial A =
  (if A ⊆ {0} then 0 else normalize (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
     normalize (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 [simp]: "normalize (gcd_factorial a b) = gcd_factorial a b"
  by (simp add: gcd_factorial_def)

lemma normalize_lcm_factorial [simp]: "normalize (lcm_factorial a b) = lcm_factorial a b"
  by (simp add: lcm_factorial_def)

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"
  have 1: "normalize x * normalize y dvd z ⟷ x * y dvd z" for x y z :: 'a
  proof -
    have "normalize (normalize x * normalize y) dvd z ⟷ x * y dvd z"
      unfolding normalize_mult_normalize_left normalize_mult_normalize_right by simp
    thus ?thesis unfolding normalize_dvd_iff by simp
  qed

  have "?p (a * b) = (?p a ∪# ?p b) + (?p a ∩# ?p b)"
    using False by (subst prime_factorization_mult) (auto intro!: multiset_eqI)
  hence "normalize (prod_mset (?p (a * b))) =
           normalize (prod_mset ((?p a ∪# ?p b) + (?p a ∩# ?p b)))"
    by (simp only:)
  hence *: "normalize (a * b) = normalize (lcm_factorial a b * gcd_factorial a b)" using False
    by (subst (asm) prod_mset_prime_factorization_weak)
       (auto simp: lcm_factorial_def gcd_factorial_def)

  have [simp]: "gcd_factorial a b dvd a * b" "lcm_factorial a b dvd a * b"
    using associatedD2[OF *] by auto
  from False have [simp]: "gcd_factorial a b ≠ 0" "lcm_factorial a b ≠ 0"
    by (auto simp: gcd_factorial_def lcm_factorial_def)
  
  show ?thesis
    by (rule associated_eqI)
       (use * in ‹auto simp: dvd_div_iff_mult div_dvd_iff_mult dest: associatedD1 associatedD2›)
qed (auto simp: lcm_factorial_def)

lemma normalize_Gcd_factorial:
  "normalize (Gcd_factorial A) = Gcd_factorial A"
  by (simp 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"
  by (simp add: 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 = normalize (∏p ∈ prime_factors x ∩ prime_factors y.
                          p ^ min (multiplicity p x) (multiplicity p y))" (is "_ = ?rhs1")
    and lcm_eq_factorial':
          "lcm x y = normalize (∏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
          intro!: arg_cong[of _ _ normalize] 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 intro!: arg_cong[of _ _ normalize] 
          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


class factorial_semiring_multiplicative =
  factorial_semiring + normalization_semidom_multiplicative
begin

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_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 prime_decomposition: "unit_factor x * prod_mset (prime_factorization x) = x"
  by (cases "x = 0") (simp_all add: prod_mset_prime_factorization)

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
  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 divides_primepow:
  assumes "prime p" and "a dvd p ^ n"
  obtains m where "m ≤ n" and "normalize a = p ^ m"
  using divides_primepow_weak[OF assms] that assms
  by (auto simp add: normalize_power)

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

text ‹Now a string of results due to Maya Kądziołka›

lemma multiplicity_dvd_iff_dvd:
 assumes "x ≠ 0"
 shows "p^k dvd x ⟷ p^k dvd p^multiplicity p x"
proof (cases "is_unit p")
 case True
 then have "is_unit (p^k)"
   using is_unit_power_iff by simp
 hence "p^k dvd x"
   by auto
 moreover from ‹is_unit p› have "p^k dvd p^multiplicity p x"
   using multiplicity_unit_left is_unit_power_iff by simp
 ultimately show ?thesis by simp
next
 case False
 show ?thesis
 proof (cases "p = 0")
   case True
   then have "p^multiplicity p x = 1"
     by simp
   moreover have "p^k dvd x ⟹ k = 0"
   proof (rule ccontr)
     assume "p^k dvd x" and "k ≠ 0"
     with ‹p = 0› have "p^k = 0" by auto
     with ‹p^k dvd x› have "0 dvd x" by auto
     hence "x = 0" by auto
     with ‹x ≠ 0› show False by auto
   qed
   ultimately show ?thesis
     by (auto simp add: is_unit_power_iff ‹¬ is_unit p›)
 next
   case False
   with ‹x ≠ 0› ‹¬ is_unit p› show ?thesis
     by (simp add: power_dvd_iff_le_multiplicity dvd_power_iff multiplicity_same_power)
 qed
qed

lemma multiplicity_decomposeI:
 assumes "x = p^k * x'" and "¬ p dvd x'" and "p ≠ 0"
 shows "multiplicity p x = k"
  using assms local.multiplicity_eqI local.power_Suc2 by force

lemma multiplicity_sum_lt:
 assumes "multiplicity p a < multiplicity p b" "a ≠ 0" "b ≠ 0"
 shows "multiplicity p (a + b) = multiplicity p a"
proof -
 let ?vp = "multiplicity p"
 have unit: "¬ is_unit p"
 proof
   assume "is_unit p"
   then have "?vp a = 0" and "?vp b = 0" using multiplicity_unit_left by auto
   with assms show False by auto
 qed

 from multiplicity_decompose' obtain a' where a': "a = p^?vp a * a'" "¬ p dvd a'"
   using unit assms by metis
 from multiplicity_decompose' obtain b' where b': "b = p^?vp b * b'"
   using unit assms by metis

 show "?vp (a + b) = ?vp a"
 proof (rule multiplicity_decomposeI)
   let ?k = "?vp b - ?vp a"
   from assms have k: "?k > 0" by simp
   with b' have "b = p^?vp a * p^?k * b'"
     by (simp flip: power_add)
   with a' show *: "a + b = p^?vp a * (a' + p^?k * b')"
     by (simp add: ac_simps distrib_left)
   moreover show "¬ p dvd a' + p^?k * b'"
     using a' k dvd_add_left_iff by auto
   show "p ≠ 0" using assms by auto
 qed
qed

corollary multiplicity_sum_min:
 assumes "multiplicity p a ≠ multiplicity p b" "a ≠ 0" "b ≠ 0"
 shows "multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)"
proof -
 let ?vp = "multiplicity p"
 from assms have "?vp a < ?vp b ∨ ?vp a > ?vp b"
   by auto
 then show ?thesis
   by (metis assms multiplicity_sum_lt min.commute add_commute min.strict_order_iff)    
qed

end

lifting_update multiset.lifting
lifting_forget multiset.lifting

end