Theory HOL-Algebra.Divisibility

(*  Title:      HOL/Algebra/Divisibility.thy
    Author:     Clemens Ballarin
    Author:     Stephan Hohe
*)

section ‹Divisibility in monoids and rings›

theory Divisibility
  imports "HOL-Combinatorics.List_Permutation" Coset Group
begin

section ‹Factorial Monoids›

subsection ‹Monoids with Cancellation Law›

locale monoid_cancel = monoid +
  assumes l_cancel: "⟦c ⊗ a = c ⊗ b; a ∈ carrier G; b ∈ carrier G; c ∈ carrier G⟧ ⟹ a = b"
    and r_cancel: "⟦a ⊗ c = b ⊗ c; a ∈ carrier G; b ∈ carrier G; c ∈ carrier G⟧ ⟹ a = b"

lemma (in monoid) monoid_cancelI:
  assumes l_cancel: "⋀a b c. ⟦c ⊗ a = c ⊗ b; a ∈ carrier G; b ∈ carrier G; c ∈ carrier G⟧ ⟹ a = b"
    and r_cancel: "⋀a b c. ⟦a ⊗ c = b ⊗ c; a ∈ carrier G; b ∈ carrier G; c ∈ carrier G⟧ ⟹ a = b"
  shows "monoid_cancel G"
    by standard fact+

lemma (in monoid_cancel) is_monoid_cancel: "monoid_cancel G" ..

sublocale group ⊆ monoid_cancel
  by standard simp_all


locale comm_monoid_cancel = monoid_cancel + comm_monoid

lemma comm_monoid_cancelI:
  fixes G (structure)
  assumes "comm_monoid G"
  assumes cancel: "⋀a b c. ⟦a ⊗ c = b ⊗ c; a ∈ carrier G; b ∈ carrier G; c ∈ carrier G⟧ ⟹ a = b"
  shows "comm_monoid_cancel G"
proof -
  interpret comm_monoid G by fact
  show "comm_monoid_cancel G"
    by unfold_locales (metis assms(2) m_ac(2))+
qed

lemma (in comm_monoid_cancel) is_comm_monoid_cancel: "comm_monoid_cancel G"
  by intro_locales

sublocale comm_group ⊆ comm_monoid_cancel ..


subsection ‹Products of Units in Monoids›

lemma (in monoid) prod_unit_l:
  assumes abunit[simp]: "a ⊗ b ∈ Units G"
    and aunit[simp]: "a ∈ Units G"
    and carr[simp]: "a ∈ carrier G"  "b ∈ carrier G"
  shows "b ∈ Units G"
proof -
  have c: "inv (a ⊗ b) ⊗ a ∈ carrier G" by simp

  have "(inv (a ⊗ b) ⊗ a) ⊗ b = inv (a ⊗ b) ⊗ (a ⊗ b)"
    by (simp add: m_assoc)
  also have "… = 𝟭" by simp
  finally have li: "(inv (a ⊗ b) ⊗ a) ⊗ b = 𝟭" .

  have "𝟭 = inv a ⊗ a" by (simp add: Units_l_inv[symmetric])
  also have "… = inv a ⊗ 𝟭 ⊗ a" by simp
  also have "… = inv a ⊗ ((a ⊗ b) ⊗ inv (a ⊗ b)) ⊗ a"
    by (simp add: Units_r_inv[OF abunit, symmetric] del: Units_r_inv)
  also have "… = ((inv a ⊗ a) ⊗ b) ⊗ inv (a ⊗ b) ⊗ a"
    by (simp add: m_assoc del: Units_l_inv)
  also have "… = b ⊗ inv (a ⊗ b) ⊗ a" by simp
  also have "… = b ⊗ (inv (a ⊗ b) ⊗ a)" by (simp add: m_assoc)
  finally have ri: "b ⊗ (inv (a ⊗ b) ⊗ a) = 𝟭 " by simp

  from c li ri show "b ∈ Units G" by (auto simp: Units_def)
qed

lemma (in monoid) prod_unit_r:
  assumes abunit[simp]: "a ⊗ b ∈ Units G"
    and bunit[simp]: "b ∈ Units G"
    and carr[simp]: "a ∈ carrier G"  "b ∈ carrier G"
  shows "a ∈ Units G"
proof -
  have c: "b ⊗ inv (a ⊗ b) ∈ carrier G" by simp

  have "a ⊗ (b ⊗ inv (a ⊗ b)) = (a ⊗ b) ⊗ inv (a ⊗ b)"
    by (simp add: m_assoc del: Units_r_inv)
  also have "… = 𝟭" by simp
  finally have li: "a ⊗ (b ⊗ inv (a ⊗ b)) = 𝟭" .

  have "𝟭 = b ⊗ inv b" by (simp add: Units_r_inv[symmetric])
  also have "… = b ⊗ 𝟭 ⊗ inv b" by simp
  also have "… = b ⊗ (inv (a ⊗ b) ⊗ (a ⊗ b)) ⊗ inv b"
    by (simp add: Units_l_inv[OF abunit, symmetric] del: Units_l_inv)
  also have "… = (b ⊗ inv (a ⊗ b) ⊗ a) ⊗ (b ⊗ inv b)"
    by (simp add: m_assoc del: Units_l_inv)
  also have "… = b ⊗ inv (a ⊗ b) ⊗ a" by simp
  finally have ri: "(b ⊗ inv (a ⊗ b)) ⊗ a = 𝟭 " by simp

  from c li ri show "a ∈ Units G" by (auto simp: Units_def)
qed

lemma (in comm_monoid) unit_factor:
  assumes abunit: "a ⊗ b ∈ Units G"
    and [simp]: "a ∈ carrier G"  "b ∈ carrier G"
  shows "a ∈ Units G"
  using abunit[simplified Units_def]
proof clarsimp
  fix i
  assume [simp]: "i ∈ carrier G"

  have carr': "b ⊗ i ∈ carrier G" by simp

  have "(b ⊗ i) ⊗ a = (i ⊗ b) ⊗ a" by (simp add: m_comm)
  also have "… = i ⊗ (b ⊗ a)" by (simp add: m_assoc)
  also have "… = i ⊗ (a ⊗ b)" by (simp add: m_comm)
  also assume "i ⊗ (a ⊗ b) = 𝟭"
  finally have li': "(b ⊗ i) ⊗ a = 𝟭" .

  have "a ⊗ (b ⊗ i) = a ⊗ b ⊗ i" by (simp add: m_assoc)
  also assume "a ⊗ b ⊗ i = 𝟭"
  finally have ri': "a ⊗ (b ⊗ i) = 𝟭" .

  from carr' li' ri'
  show "a ∈ Units G" by (simp add: Units_def, fast)
qed


subsection ‹Divisibility and Association›

subsubsection ‹Function definitions›

definition factor :: "[_, 'a, 'a] ⇒ bool" (infix ‹dividesı› 65)
  where "a divides⇘G⇙ b ⟷ (∃c∈carrier G. b = a ⊗⇘G⇙ c)"

definition associated :: "[_, 'a, 'a] ⇒ bool" (infix ‹∼ı› 55)
  where "a ∼⇘G⇙ b ⟷ a divides⇘G⇙ b ∧ b divides⇘G⇙ a"

abbreviation "division_rel G ≡ ⦇carrier = carrier G, eq = (∼⇘G⇙), le = (divides⇘G⇙)⦈"

definition properfactor :: "[_, 'a, 'a] ⇒ bool"
  where "properfactor G a b ⟷ a divides⇘G⇙ b ∧ ¬(b divides⇘G⇙ a)"

definition irreducible :: "[_, 'a] ⇒ bool"
  where "irreducible G a ⟷ a ∉ Units G ∧ (∀b∈carrier G. properfactor G b a ⟶ b ∈ Units G)"

definition prime :: "[_, 'a] ⇒ bool"
  where "prime G p ⟷
    p ∉ Units G ∧
    (∀a∈carrier G. ∀b∈carrier G. p divides⇘G⇙ (a ⊗⇘G⇙ b) ⟶ p divides⇘G⇙ a ∨ p divides⇘G⇙ b)"


subsubsection ‹Divisibility›

lemma dividesI:
  fixes G (structure)
  assumes carr: "c ∈ carrier G"
    and p: "b = a ⊗ c"
  shows "a divides b"
  unfolding factor_def using assms by fast

lemma dividesI' [intro]:
  fixes G (structure)
  assumes p: "b = a ⊗ c"
    and carr: "c ∈ carrier G"
  shows "a divides b"
  using assms by (fast intro: dividesI)

lemma dividesD:
  fixes G (structure)
  assumes "a divides b"
  shows "∃c∈carrier G. b = a ⊗ c"
  using assms unfolding factor_def by fast

lemma dividesE [elim]:
  fixes G (structure)
  assumes d: "a divides b"
    and elim: "⋀c. ⟦b = a ⊗ c; c ∈ carrier G⟧ ⟹ P"
  shows "P"
proof -
  from dividesD[OF d] obtain c where "c ∈ carrier G" and "b = a ⊗ c" by auto
  then show P by (elim elim)
qed

lemma (in monoid) divides_refl[simp, intro!]:
  assumes carr: "a ∈ carrier G"
  shows "a divides a"
  by (intro dividesI[of "𝟭"]) (simp_all add: carr)

lemma (in monoid) divides_trans [trans]:
  assumes dvds: "a divides b" "b divides c"
    and acarr: "a ∈ carrier G"
  shows "a divides c"
  using dvds[THEN dividesD] by (blast intro: dividesI m_assoc acarr)

lemma (in monoid) divides_mult_lI [intro]:
  assumes  "a divides b" "a ∈ carrier G" "c ∈ carrier G"
  shows "(c ⊗ a) divides (c ⊗ b)"
  by (metis assms factor_def m_assoc)

lemma (in monoid_cancel) divides_mult_l [simp]:
  assumes carr: "a ∈ carrier G"  "b ∈ carrier G"  "c ∈ carrier G"
  shows "(c ⊗ a) divides (c ⊗ b) = a divides b"
proof
  show "c ⊗ a divides c ⊗ b ⟹ a divides b"
    using carr monoid.m_assoc monoid_axioms monoid_cancel.l_cancel monoid_cancel_axioms by fastforce
  show "a divides b ⟹ c ⊗ a divides c ⊗ b"
  using carr(1) carr(3) by blast
qed

lemma (in comm_monoid) divides_mult_rI [intro]:
  assumes ab: "a divides b"
    and carr: "a ∈ carrier G"  "b ∈ carrier G"  "c ∈ carrier G"
  shows "(a ⊗ c) divides (b ⊗ c)"
  using carr ab by (metis divides_mult_lI m_comm)

lemma (in comm_monoid_cancel) divides_mult_r [simp]:
  assumes carr: "a ∈ carrier G"  "b ∈ carrier G"  "c ∈ carrier G"
  shows "(a ⊗ c) divides (b ⊗ c) = a divides b"
  using carr by (simp add: m_comm[of a c] m_comm[of b c])

lemma (in monoid) divides_prod_r:
  assumes ab: "a divides b"
    and carr: "a ∈ carrier G" "c ∈ carrier G"
  shows "a divides (b ⊗ c)"
  using ab carr by (fast intro: m_assoc)

lemma (in comm_monoid) divides_prod_l:
  assumes "a ∈ carrier G" "b ∈ carrier G" "c ∈ carrier G" "a divides b"
  shows "a divides (c ⊗ b)"
  using assms  by (simp add: divides_prod_r m_comm)

lemma (in monoid) unit_divides:
  assumes uunit: "u ∈ Units G"
    and acarr: "a ∈ carrier G"
  shows "u divides a"
proof (intro dividesI[of "(inv u) ⊗ a"], fast intro: uunit acarr)
  from uunit acarr have xcarr: "inv u ⊗ a ∈ carrier G" by fast
  from uunit acarr have "u ⊗ (inv u ⊗ a) = (u ⊗ inv u) ⊗ a"
    by (fast intro: m_assoc[symmetric])
  also have "… = 𝟭 ⊗ a" by (simp add: Units_r_inv[OF uunit])
  also from acarr have "… = a" by simp
  finally show "a = u ⊗ (inv u ⊗ a)" ..
qed

lemma (in comm_monoid) divides_unit:
  assumes udvd: "a divides u"
    and  carr: "a ∈ carrier G"  "u ∈ Units G"
  shows "a ∈ Units G"
  using udvd carr by (blast intro: unit_factor)

lemma (in comm_monoid) Unit_eq_dividesone:
  assumes ucarr: "u ∈ carrier G"
  shows "u ∈ Units G = u divides 𝟭"
  using ucarr by (fast dest: divides_unit intro: unit_divides)


subsubsection ‹Association›

lemma associatedI:
  fixes G (structure)
  assumes "a divides b" "b divides a"
  shows "a ∼ b"
  using assms by (simp add: associated_def)

lemma (in monoid) associatedI2:
  assumes uunit[simp]: "u ∈ Units G"
    and a: "a = b ⊗ u"
    and bcarr: "b ∈ carrier G"
  shows "a ∼ b"
  using uunit bcarr
  unfolding a
  apply (intro associatedI)
  apply (metis Units_closed divides_mult_lI one_closed r_one unit_divides)
  by blast

lemma (in monoid) associatedI2':
  assumes "a = b ⊗ u"
    and "u ∈ Units G"
    and "b ∈ carrier G"
  shows "a ∼ b"
  using assms by (intro associatedI2)

lemma associatedD:
  fixes G (structure)
  assumes "a ∼ b"
  shows "a divides b"
  using assms by (simp add: associated_def)

lemma (in monoid_cancel) associatedD2:
  assumes assoc: "a ∼ b"
    and carr: "a ∈ carrier G" "b ∈ carrier G"
  shows "∃u∈Units G. a = b ⊗ u"
  using assoc
  unfolding associated_def
proof clarify
  assume "b divides a"
  then obtain u where ucarr: "u ∈ carrier G" and a: "a = b ⊗ u"
    by (rule dividesE)

  assume "a divides b"
  then obtain u' where u'carr: "u' ∈ carrier G" and b: "b = a ⊗ u'"
    by (rule dividesE)
  note carr = carr ucarr u'carr

  from carr have "a ⊗ 𝟭 = a" by simp
  also have "… = b ⊗ u" by (simp add: a)
  also have "… = a ⊗ u' ⊗ u" by (simp add: b)
  also from carr have "… = a ⊗ (u' ⊗ u)" by (simp add: m_assoc)
  finally have "a ⊗ 𝟭 = a ⊗ (u' ⊗ u)" .
  with carr have u1: "𝟭 = u' ⊗ u" by (fast dest: l_cancel)

  from carr have "b ⊗ 𝟭 = b" by simp
  also have "… = a ⊗ u'" by (simp add: b)
  also have "… = b ⊗ u ⊗ u'" by (simp add: a)
  also from carr have "… = b ⊗ (u ⊗ u')" by (simp add: m_assoc)
  finally have "b ⊗ 𝟭 = b ⊗ (u ⊗ u')" .
  with carr have u2: "𝟭 = u ⊗ u'" by (fast dest: l_cancel)

  from u'carr u1[symmetric] u2[symmetric] have "∃u'∈carrier G. u' ⊗ u = 𝟭 ∧ u ⊗ u' = 𝟭"
    by fast
  then have "u ∈ Units G"
    by (simp add: Units_def ucarr)
  with ucarr a show "∃u∈Units G. a = b ⊗ u" by fast
qed

lemma associatedE:
  fixes G (structure)
  assumes assoc: "a ∼ b"
    and e: "⟦a divides b; b divides a⟧ ⟹ P"
  shows "P"
proof -
  from assoc have "a divides b" "b divides a"
    by (simp_all add: associated_def)
  then show P by (elim e)
qed

lemma (in monoid_cancel) associatedE2:
  assumes assoc: "a ∼ b"
    and e: "⋀u. ⟦a = b ⊗ u; u ∈ Units G⟧ ⟹ P"
    and carr: "a ∈ carrier G"  "b ∈ carrier G"
  shows "P"
proof -
  from assoc and carr have "∃u∈Units G. a = b ⊗ u"
    by (rule associatedD2)
  then obtain u where "u ∈ Units G"  "a = b ⊗ u"
    by auto
  then show P by (elim e)
qed

lemma (in monoid) associated_refl [simp, intro!]:
  assumes "a ∈ carrier G"
  shows "a ∼ a"
  using assms by (fast intro: associatedI)

lemma (in monoid) associated_sym [sym]:
  assumes "a ∼ b"
  shows "b ∼ a"
  using assms by (iprover intro: associatedI elim: associatedE)

lemma (in monoid) associated_trans [trans]:
  assumes "a ∼ b"  "b ∼ c"
    and "a ∈ carrier G" "c ∈ carrier G"
  shows "a ∼ c"
  using assms by (iprover intro: associatedI divides_trans elim: associatedE)

lemma (in monoid) division_equiv [intro, simp]: "equivalence (division_rel G)"
  apply unfold_locales
    apply simp_all
   apply (metis associated_def)
  apply (iprover intro: associated_trans)
  done


subsubsection ‹Division and associativity›

lemmas divides_antisym = associatedI

lemma (in monoid) divides_cong_l [trans]:
  assumes "x ∼ x'" "x' divides y" "x ∈ carrier G" 
  shows "x divides y"
  by (meson assms associatedD divides_trans)

lemma (in monoid) divides_cong_r [trans]:
  assumes "x divides y" "y ∼ y'" "x ∈ carrier G" 
  shows "x divides y'"
  by (meson assms associatedD divides_trans)

lemma (in monoid) division_weak_partial_order [simp, intro!]:
  "weak_partial_order (division_rel G)"
  apply unfold_locales
      apply (simp_all add: associated_sym divides_antisym)
     apply (metis associated_trans)
   apply (metis divides_trans)
  by (meson associated_def divides_trans)


subsubsection ‹Multiplication and associativity›

lemma (in monoid) mult_cong_r:
  assumes "b ∼ b'" "a ∈ carrier G"  "b ∈ carrier G"  "b' ∈ carrier G"
  shows "a ⊗ b ∼ a ⊗ b'"
  by (meson assms associated_def divides_mult_lI)

lemma (in comm_monoid) mult_cong_l:
  assumes "a ∼ a'" "a ∈ carrier G"  "a' ∈ carrier G"  "b ∈ carrier G"
  shows "a ⊗ b ∼ a' ⊗ b"
  using assms m_comm mult_cong_r by auto

lemma (in monoid_cancel) assoc_l_cancel:
  assumes "a ∈ carrier G"  "b ∈ carrier G"  "b' ∈ carrier G" "a ⊗ b ∼ a ⊗ b'"
  shows "b ∼ b'"
  by (meson assms associated_def divides_mult_l)

lemma (in comm_monoid_cancel) assoc_r_cancel:
  assumes "a ⊗ b ∼ a' ⊗ b" "a ∈ carrier G"  "a' ∈ carrier G"  "b ∈ carrier G"
  shows "a ∼ a'"
  using assms assoc_l_cancel m_comm by presburger


subsubsection ‹Units›

lemma (in monoid_cancel) assoc_unit_l [trans]:
  assumes "a ∼ b"
    and "b ∈ Units G"
    and "a ∈ carrier G"
  shows "a ∈ Units G"
  using assms by (fast elim: associatedE2)

lemma (in monoid_cancel) assoc_unit_r [trans]:
  assumes aunit: "a ∈ Units G"
    and asc: "a ∼ b"
    and bcarr: "b ∈ carrier G"
  shows "b ∈ Units G"
  using aunit bcarr associated_sym[OF asc] by (blast intro: assoc_unit_l)

lemma (in comm_monoid) Units_cong:
  assumes aunit: "a ∈ Units G" and asc: "a ∼ b"
    and bcarr: "b ∈ carrier G"
  shows "b ∈ Units G"
  using assms by (blast intro: divides_unit elim: associatedE)

lemma (in monoid) Units_assoc:
  assumes units: "a ∈ Units G"  "b ∈ Units G"
  shows "a ∼ b"
  using units by (fast intro: associatedI unit_divides)

lemma (in monoid) Units_are_ones: "Units G {.=}⇘(division_rel G)⇙ {𝟭}"
proof -
  have "a .∈⇘division_rel G⇙ {𝟭}" if "a ∈ Units G" for a
  proof -
    have "a ∼ 𝟭"
      by (rule associatedI) (simp_all add: Units_closed that unit_divides)
    then show ?thesis
      by (simp add: elem_def)
  qed
  moreover have "𝟭 .∈⇘division_rel G⇙ Units G"
    by (simp add: equivalence.mem_imp_elem)
  ultimately show ?thesis
    by (auto simp: set_eq_def)
qed

lemma (in comm_monoid) Units_Lower: "Units G = Lower (division_rel G) (carrier G)"
  apply (auto simp add: Units_def Lower_def)
   apply (metis Units_one_closed unit_divides unit_factor)
  apply (metis Unit_eq_dividesone Units_r_inv_ex m_ac(2) one_closed)
  done

lemma (in monoid_cancel) associated_iff:
  assumes "a ∈ carrier G" "b ∈ carrier G"
  shows "a ∼ b ⟷ (∃c ∈ Units G. a = b ⊗ c)"
  using assms associatedI2' associatedD2 by auto


subsubsection ‹Proper factors›

lemma properfactorI:
  fixes G (structure)
  assumes "a divides b"
    and "¬(b divides a)"
  shows "properfactor G a b"
  using assms unfolding properfactor_def by simp

lemma properfactorI2:
  fixes G (structure)
  assumes advdb: "a divides b"
    and neq: "¬(a ∼ b)"
  shows "properfactor G a b"
proof (rule properfactorI, rule advdb, rule notI)
  assume "b divides a"
  with advdb have "a ∼ b" by (rule associatedI)
  with neq show "False" by fast
qed

lemma (in comm_monoid_cancel) properfactorI3:
  assumes p: "p = a ⊗ b"
    and nunit: "b ∉ Units G"
    and carr: "a ∈ carrier G"  "b ∈ carrier G" 
  shows "properfactor G a p"
  unfolding p
  using carr
  apply (intro properfactorI, fast)
proof (clarsimp, elim dividesE)
  fix c
  assume ccarr: "c ∈ carrier G"
  note [simp] = carr ccarr

  have "a ⊗ 𝟭 = a" by simp
  also assume "a = a ⊗ b ⊗ c"
  also have "… = a ⊗ (b ⊗ c)" by (simp add: m_assoc)
  finally have "a ⊗ 𝟭 = a ⊗ (b ⊗ c)" .

  then have rinv: "𝟭 = b ⊗ c" by (intro l_cancel[of "a" "𝟭" "b ⊗ c"], simp+)
  also have "… = c ⊗ b" by (simp add: m_comm)
  finally have linv: "𝟭 = c ⊗ b" .

  from ccarr linv[symmetric] rinv[symmetric] have "b ∈ Units G"
    unfolding Units_def by fastforce
  with nunit show False ..
qed

lemma properfactorE:
  fixes G (structure)
  assumes pf: "properfactor G a b"
    and r: "⟦a divides b; ¬(b divides a)⟧ ⟹ P"
  shows "P"
  using pf unfolding properfactor_def by (fast intro: r)

lemma properfactorE2:
  fixes G (structure)
  assumes pf: "properfactor G a b"
    and elim: "⟦a divides b; ¬(a ∼ b)⟧ ⟹ P"
  shows "P"
  using pf unfolding properfactor_def by (fast elim: elim associatedE)

lemma (in monoid) properfactor_unitE:
  assumes uunit: "u ∈ Units G"
    and pf: "properfactor G a u"
    and acarr: "a ∈ carrier G"
  shows "P"
  using pf unit_divides[OF uunit acarr] by (fast elim: properfactorE)

lemma (in monoid) properfactor_divides:
  assumes pf: "properfactor G a b"
  shows "a divides b"
  using pf by (elim properfactorE)

lemma (in monoid) properfactor_trans1 [trans]:
  assumes "a divides b"  "properfactor G b c" "a ∈ carrier G"  "c ∈ carrier G"
  shows "properfactor G a c"
  by (meson divides_trans properfactorE properfactorI assms)

lemma (in monoid) properfactor_trans2 [trans]:
  assumes "properfactor G a b"  "b divides c" "a ∈ carrier G"  "b ∈ carrier G"
  shows "properfactor G a c"
  by (meson divides_trans properfactorE properfactorI assms)

lemma properfactor_lless:
  fixes G (structure)
  shows "properfactor G = lless (division_rel G)"
  by (force simp: lless_def properfactor_def associated_def)

lemma (in monoid) properfactor_cong_l [trans]:
  assumes x'x: "x' ∼ x"
    and pf: "properfactor G x y"
    and carr: "x ∈ carrier G"  "x' ∈ carrier G"  "y ∈ carrier G"
  shows "properfactor G x' y"
  using pf
  unfolding properfactor_lless
proof -
  interpret weak_partial_order "division_rel G" ..
  from x'x have "x' .=⇘division_rel G⇙ x" by simp
  also assume "x ⊏⇘division_rel G⇙ y"
  finally show "x' ⊏⇘division_rel G⇙ y" by (simp add: carr)
qed

lemma (in monoid) properfactor_cong_r [trans]:
  assumes pf: "properfactor G x y"
    and yy': "y ∼ y'"
    and carr: "x ∈ carrier G"  "y ∈ carrier G"  "y' ∈ carrier G"
  shows "properfactor G x y'"
  using pf
  unfolding properfactor_lless
proof -
  interpret weak_partial_order "division_rel G" ..
  assume "x ⊏⇘division_rel G⇙ y"
  also from yy'
  have "y .=⇘division_rel G⇙ y'" by simp
  finally show "x ⊏⇘division_rel G⇙ y'" by (simp add: carr)
qed

lemma (in monoid_cancel) properfactor_mult_lI [intro]:
  assumes ab: "properfactor G a b"
    and carr: "a ∈ carrier G" "c ∈ carrier G"
  shows "properfactor G (c ⊗ a) (c ⊗ b)"
  using ab carr by (fastforce elim: properfactorE intro: properfactorI)

lemma (in monoid_cancel) properfactor_mult_l [simp]:
  assumes carr: "a ∈ carrier G"  "b ∈ carrier G"  "c ∈ carrier G"
  shows "properfactor G (c ⊗ a) (c ⊗ b) = properfactor G a b"
  using carr by (fastforce elim: properfactorE intro: properfactorI)

lemma (in comm_monoid_cancel) properfactor_mult_rI [intro]:
  assumes ab: "properfactor G a b"
    and carr: "a ∈ carrier G" "c ∈ carrier G"
  shows "properfactor G (a ⊗ c) (b ⊗ c)"
  using ab carr by (fastforce elim: properfactorE intro: properfactorI)

lemma (in comm_monoid_cancel) properfactor_mult_r [simp]:
  assumes carr: "a ∈ carrier G"  "b ∈ carrier G"  "c ∈ carrier G"
  shows "properfactor G (a ⊗ c) (b ⊗ c) = properfactor G a b"
  using carr by (fastforce elim: properfactorE intro: properfactorI)

lemma (in monoid) properfactor_prod_r:
  assumes ab: "properfactor G a b"
    and carr[simp]: "a ∈ carrier G"  "b ∈ carrier G"  "c ∈ carrier G"
  shows "properfactor G a (b ⊗ c)"
  by (intro properfactor_trans2[OF ab] divides_prod_r) simp_all

lemma (in comm_monoid) properfactor_prod_l:
  assumes ab: "properfactor G a b"
    and carr[simp]: "a ∈ carrier G"  "b ∈ carrier G"  "c ∈ carrier G"
  shows "properfactor G a (c ⊗ b)"
  by (intro properfactor_trans2[OF ab] divides_prod_l) simp_all


subsection ‹Irreducible Elements and Primes›

subsubsection ‹Irreducible elements›

lemma irreducibleI:
  fixes G (structure)
  assumes "a ∉ Units G"
    and "⋀b. ⟦b ∈ carrier G; properfactor G b a⟧ ⟹ b ∈ Units G"
  shows "irreducible G a"
  using assms unfolding irreducible_def by blast

lemma irreducibleE:
  fixes G (structure)
  assumes irr: "irreducible G a"
    and elim: "⟦a ∉ Units G; ∀b. b ∈ carrier G ∧ properfactor G b a ⟶ b ∈ Units G⟧ ⟹ P"
  shows "P"
  using assms unfolding irreducible_def by blast

lemma irreducibleD:
  fixes G (structure)
  assumes irr: "irreducible G a"
    and pf: "properfactor G b a"
    and bcarr: "b ∈ carrier G"
  shows "b ∈ Units G"
  using assms by (fast elim: irreducibleE)

lemma (in monoid_cancel) irreducible_cong [trans]:
  assumes "irreducible G a" "a ∼ a'" "a ∈ carrier G"  "a' ∈ carrier G"
  shows "irreducible G a'"
proof -
  have "a' divides a"
    by (meson ‹a ∼ a'› associated_def)
  then show ?thesis
    by (metis (no_types) assms assoc_unit_l irreducibleE irreducibleI monoid.properfactor_trans2 monoid_axioms)
qed

lemma (in monoid) irreducible_prod_rI:
  assumes "irreducible G a" "b ∈ Units G" "a ∈ carrier G"  "b ∈ carrier G"
  shows "irreducible G (a ⊗ b)"
  using assms
  by (metis (no_types, lifting) associatedI2' irreducible_def monoid.m_closed monoid_axioms prod_unit_r properfactor_cong_r)

lemma (in comm_monoid) irreducible_prod_lI:
  assumes birr: "irreducible G b"
    and aunit: "a ∈ Units G"
    and carr [simp]: "a ∈ carrier G"  "b ∈ carrier G"
  shows "irreducible G (a ⊗ b)"
  by (metis aunit birr carr irreducible_prod_rI m_comm)

lemma (in comm_monoid_cancel) irreducible_prodE [elim]:
  assumes irr: "irreducible G (a ⊗ b)"
    and carr[simp]: "a ∈ carrier G"  "b ∈ carrier G"
    and e1: "⟦irreducible G a; b ∈ Units G⟧ ⟹ P"
    and e2: "⟦a ∈ Units G; irreducible G b⟧ ⟹ P"
  shows P
  using irr
proof (elim irreducibleE)
  assume abnunit: "a ⊗ b ∉ Units G"
    and isunit[rule_format]: "∀ba. ba ∈ carrier G ∧ properfactor G ba (a ⊗ b) ⟶ ba ∈ Units G"
  show P
  proof (cases "a ∈ Units G")
    case aunit: True
    have "irreducible G b"
    proof (rule irreducibleI, rule notI)
      assume "b ∈ Units G"
      with aunit have "(a ⊗ b) ∈ Units G" by fast
      with abnunit show "False" ..
    next
      fix c
      assume ccarr: "c ∈ carrier G"
        and "properfactor G c b"
      then have "properfactor G c (a ⊗ b)" by (simp add: properfactor_prod_l[of c b a])
      with ccarr show "c ∈ Units G" by (fast intro: isunit)
    qed
    with aunit show "P" by (rule e2)
  next
    case anunit: False
    with carr have "properfactor G b (b ⊗ a)" by (fast intro: properfactorI3)
    then have bf: "properfactor G b (a ⊗ b)" by (subst m_comm[of a b], simp+)
    then have bunit: "b ∈ Units G" by (intro isunit, simp)

    have "irreducible G a"
    proof (rule irreducibleI, rule notI)
      assume "a ∈ Units G"
      with bunit have "(a ⊗ b) ∈ Units G" by fast
      with abnunit show "False" ..
    next
      fix c
      assume ccarr: "c ∈ carrier G"
        and "properfactor G c a"
      then have "properfactor G c (a ⊗ b)"
        by (simp add: properfactor_prod_r[of c a b])
      with ccarr show "c ∈ Units G" by (fast intro: isunit)
    qed
    from this bunit show "P" by (rule e1)
  qed
qed

lemma divides_irreducible_condition:
  assumes "irreducible G r" and "a ∈ carrier G"
  shows "a divides⇘G⇙ r ⟹ a ∈ Units G ∨ a ∼⇘G⇙ r"
  using assms unfolding irreducible_def properfactor_def associated_def
  by (cases "r divides⇘G⇙ a", auto)

subsubsection ‹Prime elements›

lemma primeI:
  fixes G (structure)
  assumes "p ∉ Units G"
    and "⋀a b. ⟦a ∈ carrier G; b ∈ carrier G; p divides (a ⊗ b)⟧ ⟹ p divides a ∨ p divides b"
  shows "prime G p"
  using assms unfolding prime_def by blast

lemma primeE:
  fixes G (structure)
  assumes pprime: "prime G p"
    and e: "⟦p ∉ Units G; ∀a∈carrier G. ∀b∈carrier G.
      p divides a ⊗ b ⟶ p divides a ∨ p divides b⟧ ⟹ P"
  shows "P"
  using pprime unfolding prime_def by (blast dest: e)

lemma (in comm_monoid_cancel) prime_divides:
  assumes carr: "a ∈ carrier G"  "b ∈ carrier G"
    and pprime: "prime G p"
    and pdvd: "p divides a ⊗ b"
  shows "p divides a ∨ p divides b"
  using assms by (blast elim: primeE)

lemma (in monoid_cancel) prime_cong [trans]:
  assumes "prime G p"
    and pp': "p ∼ p'" "p ∈ carrier G"  "p' ∈ carrier G"
  shows "prime G p'"
  using assms
  by (auto simp: prime_def assoc_unit_l) (metis pp' associated_sym divides_cong_l)

lemma (in comm_monoid_cancel) prime_irreducible: ✐‹contributor ‹Paulo Emílio de Vilhena››
  assumes "prime G p"
  shows "irreducible G p"
proof (rule irreducibleI)
  show "p ∉ Units G"
    using assms unfolding prime_def by simp
next
  fix b assume A: "b ∈ carrier G" "properfactor G b p"
  then obtain c where c: "c ∈ carrier G" "p = b ⊗ c"
    unfolding properfactor_def factor_def by auto
  hence "p divides c"
    using A assms unfolding prime_def properfactor_def by auto
  then obtain b' where b': "b' ∈ carrier G" "c = p ⊗ b'"
    unfolding factor_def by auto
  hence "𝟭 = b ⊗ b'"
    by (metis A(1) l_cancel m_closed m_lcomm one_closed r_one c)
  thus "b ∈ Units G"
    using A(1) Units_one_closed b'(1) unit_factor by presburger
qed

lemma (in comm_monoid_cancel) prime_pow_divides_iff:
  assumes "p ∈ carrier G" "a ∈ carrier G" "b ∈ carrier G" and "prime G p" and "¬ (p divides a)"
  shows "(p [^] (n :: nat)) divides (a ⊗ b) ⟷ (p [^] n) divides b"
proof
  assume "(p [^] n) divides b" thus "(p [^] n) divides (a ⊗ b)"
    using divides_prod_l[of "p [^] n" b a] assms by simp  
next
  assume "(p [^] n) divides (a ⊗ b)" thus "(p [^] n) divides b"
  proof (induction n)
    case 0 with ‹b ∈ carrier G› show ?case
      by (simp add: unit_divides)
  next
    case (Suc n)
    hence "(p [^] n) divides (a ⊗ b)" and "(p [^] n) divides b"
      using assms(1) divides_prod_r by auto
    with ‹(p [^] (Suc n)) divides (a ⊗ b)› obtain c d
      where c: "c ∈ carrier G" and "b = (p [^] n) ⊗ c"
        and d: "d ∈ carrier G" and "a ⊗ b = (p [^] (Suc n)) ⊗ d"
      using assms by blast
    hence "(p [^] n) ⊗ (a ⊗ c) = (p [^] n) ⊗ (p ⊗ d)"
      using assms by (simp add: m_assoc m_lcomm)
    hence "a ⊗ c = p ⊗ d"
      using c d assms(1) assms(2) l_cancel by blast
    with ‹¬ (p divides a)› and ‹prime G p› have "p divides c"
      by (metis assms(2) c d dividesI' prime_divides)
    with ‹b = (p [^] n) ⊗ c› show ?case
      using assms(1) c by simp
  qed
qed


subsection ‹Factorization and Factorial Monoids›

subsubsection ‹Function definitions›

definition factors :: "('a, _) monoid_scheme ⇒ 'a list ⇒ 'a ⇒ bool"
  where "factors G fs a ⟷ (∀x ∈ (set fs). irreducible G x) ∧ foldr (⊗⇘G⇙) fs 𝟭⇘G⇙ = a"

definition wfactors ::"('a, _) monoid_scheme ⇒ 'a list ⇒ 'a ⇒ bool"
  where "wfactors G fs a ⟷ (∀x ∈ (set fs). irreducible G x) ∧ foldr (⊗⇘G⇙) fs 𝟭⇘G⇙ ∼⇘G⇙ a"

abbreviation list_assoc :: "('a, _) monoid_scheme ⇒ 'a list ⇒ 'a list ⇒ bool" (infix ‹[∼]ı› 44)
  where "list_assoc G ≡ list_all2 (∼⇘G⇙)"

definition essentially_equal :: "('a, _) monoid_scheme ⇒ 'a list ⇒ 'a list ⇒ bool"
  where "essentially_equal G fs1 fs2 ⟷ (∃fs1'. fs1 <~~> fs1' ∧ fs1' [∼]⇘G⇙ fs2)"


locale factorial_monoid = comm_monoid_cancel +
  assumes factors_exist: "⟦a ∈ carrier G; a ∉ Units G⟧ ⟹ ∃fs. set fs ⊆ carrier G ∧ factors G fs a"
    and factors_unique:
      "⟦factors G fs a; factors G fs' a; a ∈ carrier G; a ∉ Units G;
        set fs ⊆ carrier G; set fs' ⊆ carrier G⟧ ⟹ essentially_equal G fs fs'"


subsubsection ‹Comparing lists of elements›

text ‹Association on lists›

lemma (in monoid) listassoc_refl [simp, intro]:
  assumes "set as ⊆ carrier G"
  shows "as [∼] as"
  using assms by (induct as) simp_all

lemma (in monoid) listassoc_sym [sym]:
  assumes "as [∼] bs"
    and "set as ⊆ carrier G"
    and "set bs ⊆ carrier G"
  shows "bs [∼] as"
  using assms
proof (induction as arbitrary: bs)
  case Cons
  then show ?case
    by (induction bs) (use associated_sym in auto)
qed auto

lemma (in monoid) listassoc_trans [trans]:
  assumes "as [∼] bs" and "bs [∼] cs"
    and "set as ⊆ carrier G" and "set bs ⊆ carrier G" and "set cs ⊆ carrier G"
  shows "as [∼] cs"
  using assms
  apply (simp add: list_all2_conv_all_nth set_conv_nth, safe)
  by (metis (mono_tags, lifting) associated_trans nth_mem subsetCE)

lemma (in monoid_cancel) irrlist_listassoc_cong:
  assumes "∀a∈set as. irreducible G a"
    and "as [∼] bs"
    and "set as ⊆ carrier G" and "set bs ⊆ carrier G"
  shows "∀a∈set bs. irreducible G a"
  using assms
  by (fastforce simp add: list_all2_conv_all_nth set_conv_nth intro: irreducible_cong)


text ‹Permutations›

lemma perm_map [intro]:
  assumes p: "a <~~> b"
  shows "map f a <~~> map f b"
  using p by simp

lemma perm_map_switch:
  assumes m: "map f a = map f b" and p: "b <~~> c"
  shows "∃d. a <~~> d ∧ map f d = map f c"
proof -
  from m have ‹length a = length b›
    by (rule map_eq_imp_length_eq)
  from p have ‹mset c = mset b›
    by simp
  then obtain p where ‹p permutes {..<length b}› ‹permute_list p b = c›
    by (rule mset_eq_permutation)
  with ‹length a = length b› have ‹p permutes {..<length a}›
    by simp
  moreover define d where ‹d = permute_list p a›
  ultimately have ‹mset a = mset d› ‹map f d = map f c›
    using m ‹p permutes {..<length b}› ‹permute_list p b = c›
    by (auto simp flip: permute_list_map)
  then show ?thesis
    by auto
qed

lemma (in monoid) perm_assoc_switch:
  assumes a:"as [∼] bs" and p: "bs <~~> cs"
  shows "∃bs'. as <~~> bs' ∧ bs' [∼] cs"
proof -
  from p have ‹mset cs = mset bs›
    by simp
  then obtain p where ‹p permutes {..<length bs}› ‹permute_list p bs = cs›
    by (rule mset_eq_permutation)
  moreover define bs' where ‹bs' = permute_list p as›
  ultimately have ‹as <~~> bs'› and ‹bs' [∼] cs›
    using a by (auto simp add: list_all2_permute_list_iff list_all2_lengthD)
  then show ?thesis by blast
qed

lemma (in monoid) perm_assoc_switch_r:
  assumes p: "as <~~> bs" and a:"bs [∼] cs"
  shows "∃bs'. as [∼] bs' ∧ bs' <~~> cs"
  using a p by (rule list_all2_reorder_left_invariance)

declare perm_sym [sym]

lemma perm_setP:
  assumes perm: "as <~~> bs"
    and as: "P (set as)"
  shows "P (set bs)"
  using assms by (metis set_mset_mset)

lemmas (in monoid) perm_closed = perm_setP[of _ _ "λas. as ⊆ carrier G"]

lemmas (in monoid) irrlist_perm_cong = perm_setP[of _ _ "λas. ∀a∈as. irreducible G a"]


text ‹Essentially equal factorizations›

lemma (in monoid) essentially_equalI:
  assumes ex: "fs1 <~~> fs1'"  "fs1' [∼] fs2"
  shows "essentially_equal G fs1 fs2"
  using ex unfolding essentially_equal_def by fast

lemma (in monoid) essentially_equalE:
  assumes ee: "essentially_equal G fs1 fs2"
    and e: "⋀fs1'. ⟦fs1 <~~> fs1'; fs1' [∼] fs2⟧ ⟹ P"
  shows "P"
  using ee unfolding essentially_equal_def by (fast intro: e)

lemma (in monoid) ee_refl [simp,intro]:
  assumes carr: "set as ⊆ carrier G"
  shows "essentially_equal G as as"
  using carr by (fast intro: essentially_equalI)

lemma (in monoid) ee_sym [sym]:
  assumes ee: "essentially_equal G as bs"
    and carr: "set as ⊆ carrier G"  "set bs ⊆ carrier G"
  shows "essentially_equal G bs as"
  using ee
proof (elim essentially_equalE)
  fix fs
  assume "as <~~> fs"  "fs [∼] bs"
  from perm_assoc_switch_r [OF this] obtain fs' where a: "as [∼] fs'" and p: "fs' <~~> bs"
    by blast
  from p have "bs <~~> fs'" by (rule perm_sym)
  with a[symmetric] carr show ?thesis
    by (iprover intro: essentially_equalI perm_closed)
qed

lemma (in monoid) ee_trans [trans]:
  assumes ab: "essentially_equal G as bs" and bc: "essentially_equal G bs cs"
    and ascarr: "set as ⊆ carrier G"
    and bscarr: "set bs ⊆ carrier G"
    and cscarr: "set cs ⊆ carrier G"
  shows "essentially_equal G as cs"
  using ab bc
proof (elim essentially_equalE)
  fix abs bcs
  assume "abs [∼] bs" and pb: "bs <~~> bcs"
  from perm_assoc_switch [OF this] obtain bs' where p: "abs <~~> bs'" and a: "bs' [∼] bcs"
    by blast
  assume "as <~~> abs"
  with p have pp: "as <~~> bs'" by simp
  from pp ascarr have c1: "set bs' ⊆ carrier G" by (rule perm_closed)
  from pb bscarr have c2: "set bcs ⊆ carrier G" by (rule perm_closed)
  assume "bcs [∼] cs"
  then have "bs' [∼] cs"
    using a c1 c2 cscarr listassoc_trans by blast
  with pp show ?thesis
    by (rule essentially_equalI)
qed


subsubsection ‹Properties of lists of elements›

text ‹Multiplication of factors in a list›

lemma (in monoid) multlist_closed [simp, intro]:
  assumes ascarr: "set fs ⊆ carrier G"
  shows "foldr (⊗) fs 𝟭 ∈ carrier G"
  using ascarr by (induct fs) simp_all

lemma  (in comm_monoid) multlist_dividesI:
  assumes "f ∈ set fs" and "set fs ⊆ carrier G"
  shows "f divides (foldr (⊗) fs 𝟭)"
  using assms
proof (induction fs)
  case (Cons a fs)
  then have f: "f ∈ carrier G"
    by blast
  show ?case
    using Cons.IH Cons.prems(1) Cons.prems(2) divides_prod_l f by auto
qed auto

lemma (in comm_monoid_cancel) multlist_listassoc_cong:
  assumes "fs [∼] fs'"
    and "set fs ⊆ carrier G" and "set fs' ⊆ carrier G"
  shows "foldr (⊗) fs 𝟭 ∼ foldr (⊗) fs' 𝟭"
  using assms
proof (induct fs arbitrary: fs')
  case (Cons a as fs')
  then show ?case
  proof (induction fs')
    case (Cons b bs)
    then have p: "a ⊗ foldr (⊗) as 𝟭 ∼ b ⊗ foldr (⊗) as 𝟭"
      by (simp add: mult_cong_l)
    then have "foldr (⊗) as 𝟭 ∼ foldr (⊗) bs 𝟭"
      using Cons by auto
    with Cons have "b ⊗ foldr (⊗) as 𝟭 ∼ b ⊗ foldr (⊗) bs 𝟭"
      by (simp add: mult_cong_r)
    then show ?case
      using Cons.prems(3) Cons.prems(4) monoid.associated_trans monoid_axioms p by force
  qed auto
qed auto

lemma (in comm_monoid) multlist_perm_cong:
  assumes prm: "as <~~> bs"
    and ascarr: "set as ⊆ carrier G"
  shows "foldr (⊗) as 𝟭 = foldr (⊗) bs 𝟭"
proof -
  from prm have ‹mset (rev as) = mset (rev bs)›
    by simp
  moreover note one_closed
  ultimately have ‹fold (⊗) (rev as) 𝟭 = fold (⊗) (rev bs) 𝟭›
    by (rule fold_permuted_eq) (use ascarr in ‹auto intro: m_lcomm›)
  then show ?thesis
    by (simp add: foldr_conv_fold)
qed

lemma (in comm_monoid_cancel) multlist_ee_cong:
  assumes "essentially_equal G fs fs'"
    and "set fs ⊆ carrier G" and "set fs' ⊆ carrier G"
  shows "foldr (⊗) fs 𝟭 ∼ foldr (⊗) fs' 𝟭"
  using assms
  by (metis essentially_equal_def multlist_listassoc_cong multlist_perm_cong perm_closed)


subsubsection ‹Factorization in irreducible elements›

lemma wfactorsI:
  fixes G (structure)
  assumes "∀f∈set fs. irreducible G f"
    and "foldr (⊗) fs 𝟭 ∼ a"
  shows "wfactors G fs a"
  using assms unfolding wfactors_def by simp

lemma wfactorsE:
  fixes G (structure)
  assumes wf: "wfactors G fs a"
    and e: "⟦∀f∈set fs. irreducible G f; foldr (⊗) fs 𝟭 ∼ a⟧ ⟹ P"
  shows "P"
  using wf unfolding wfactors_def by (fast dest: e)

lemma (in monoid) factorsI:
  assumes "∀f∈set fs. irreducible G f"
    and "foldr (⊗) fs 𝟭 = a"
  shows "factors G fs a"
  using assms unfolding factors_def by simp

lemma factorsE:
  fixes G (structure)
  assumes f: "factors G fs a"
    and e: "⟦∀f∈set fs. irreducible G f; foldr (⊗) fs 𝟭 = a⟧ ⟹ P"
  shows "P"
  using f unfolding factors_def by (simp add: e)

lemma (in monoid) factors_wfactors:
  assumes "factors G as a" and "set as ⊆ carrier G"
  shows "wfactors G as a"
  using assms by (blast elim: factorsE intro: wfactorsI)

lemma (in monoid) wfactors_factors:
  assumes "wfactors G as a" and "set as ⊆ carrier G"
  shows "∃a'. factors G as a' ∧ a' ∼ a"
  using assms by (blast elim: wfactorsE intro: factorsI)

lemma (in monoid) factors_closed [dest]:
  assumes "factors G fs a" and "set fs ⊆ carrier G"
  shows "a ∈ carrier G"
  using assms by (elim factorsE, clarsimp)

lemma (in monoid) nunit_factors:
  assumes anunit: "a ∉ Units G"
    and fs: "factors G as a"
  shows "length as > 0"
proof -
  from anunit Units_one_closed have "a ≠ 𝟭" by auto
  with fs show ?thesis by (auto elim: factorsE)
qed

lemma (in monoid) unit_wfactors [simp]:
  assumes aunit: "a ∈ Units G"
  shows "wfactors G [] a"
  using aunit by (intro wfactorsI) (simp, simp add: Units_assoc)

lemma (in comm_monoid_cancel) unit_wfactors_empty:
  assumes aunit: "a ∈ Units G"
    and wf: "wfactors G fs a"
    and carr[simp]: "set fs ⊆ carrier G"
  shows "fs = []"
proof (cases fs)
  case fs: (Cons f fs')
  from carr have fcarr[simp]: "f ∈ carrier G" and carr'[simp]: "set fs' ⊆ carrier G"
    by (simp_all add: fs)

  from fs wf have "irreducible G f" by (simp add: wfactors_def)
  then have fnunit: "f ∉ Units G" by (fast elim: irreducibleE)

  from fs wf have a: "f ⊗ foldr (⊗) fs' 𝟭 ∼ a" by (simp add: wfactors_def)

  note aunit
  also from fs wf
  have a: "f ⊗ foldr (⊗) fs' 𝟭 ∼ a" by (simp add: wfactors_def)
  have "a ∼ f ⊗ foldr (⊗) fs' 𝟭"
    by (simp add: Units_closed[OF aunit] a[symmetric])
  finally have "f ⊗ foldr (⊗) fs' 𝟭 ∈ Units G" by simp
  then have "f ∈ Units G" by (intro unit_factor[of f], simp+)
  with fnunit show ?thesis by contradiction
qed


text ‹Comparing wfactors›

lemma (in comm_monoid_cancel) wfactors_listassoc_cong_l:
  assumes fact: "wfactors G fs a"
    and asc: "fs [∼] fs'"
    and carr: "a ∈ carrier G"  "set fs ⊆ carrier G"  "set fs' ⊆ carrier G"
  shows "wfactors G fs' a"
proof -
  { from asc[symmetric] have "foldr (⊗) fs' 𝟭 ∼ foldr (⊗) fs 𝟭"
      by (simp add: multlist_listassoc_cong carr)
    also assume "foldr (⊗) fs 𝟭 ∼ a"
    finally have "foldr (⊗) fs' 𝟭 ∼ a" by (simp add: carr) }
  then show ?thesis
  using fact
  by (meson asc carr(2) carr(3) irrlist_listassoc_cong wfactors_def)
qed

lemma (in comm_monoid) wfactors_perm_cong_l:
  assumes "wfactors G fs a"
    and "fs <~~> fs'"
    and "set fs ⊆ carrier G"
  shows "wfactors G fs' a"
  using assms irrlist_perm_cong multlist_perm_cong wfactors_def by fastforce

lemma (in comm_monoid_cancel) wfactors_ee_cong_l [trans]:
  assumes ee: "essentially_equal G as bs"
    and bfs: "wfactors G bs b"
    and carr: "b ∈ carrier G"  "set as ⊆ carrier G"  "set bs ⊆ carrier G"
  shows "wfactors G as b"
  using ee
proof (elim essentially_equalE)
  fix fs
  assume prm: "as <~~> fs"
  with carr have fscarr: "set fs ⊆ carrier G"
    using perm_closed by blast

  note bfs
  also assume [symmetric]: "fs [∼] bs"
  also (wfactors_listassoc_cong_l)
  have ‹mset fs = mset as› using prm by simp
  finally (wfactors_perm_cong_l)
  show "wfactors G as b" by (simp add: carr fscarr)
qed

lemma (in monoid) wfactors_cong_r [trans]:
  assumes fac: "wfactors G fs a" and aa': "a ∼ a'"
    and carr[simp]: "a ∈ carrier G"  "a' ∈ carrier G"  "set fs ⊆ carrier G"
  shows "wfactors G fs a'"
  using fac
proof (elim wfactorsE, intro wfactorsI)
  assume "foldr (⊗) fs 𝟭 ∼ a" also note aa'
  finally show "foldr (⊗) fs 𝟭 ∼ a'" by simp
qed


subsubsection ‹Essentially equal factorizations›

lemma (in comm_monoid_cancel) unitfactor_ee:
  assumes uunit: "u ∈ Units G"
    and carr: "set as ⊆ carrier G"
  shows "essentially_equal G (as[0 := (as!0 ⊗ u)]) as"
    (is "essentially_equal G ?as' as")
proof -
  have "as[0 := as ! 0 ⊗ u] [∼] as"
  proof (cases as)
    case (Cons a as')
    then show ?thesis
      using associatedI2 carr uunit by auto
  qed auto
  then show ?thesis
    using essentially_equal_def by blast
qed

lemma (in comm_monoid_cancel) factors_cong_unit:
  assumes u: "u ∈ Units G"
    and a: "a ∉ Units G"
    and afs: "factors G as a"
    and ascarr: "set as ⊆ carrier G"
  shows "factors G (as[0 := (as!0 ⊗ u)]) (a ⊗ u)"
    (is "factors G ?as' ?a'")
proof (cases as)
  case Nil
  then show ?thesis
    using afs a nunit_factors by auto
next
  case (Cons b bs)
  have *: "∀f∈set as. irreducible G f" "foldr (⊗) as 𝟭 = a"
    using afs  by (auto simp: factors_def)
  show ?thesis
  proof (intro factorsI)
    show "foldr (⊗) (as[0 := as ! 0 ⊗ u]) 𝟭 = a ⊗ u"
      using Cons u ascarr * by (auto simp add: m_ac Units_closed)
    show "∀f∈set (as[0 := as ! 0 ⊗ u]). irreducible G f"
      using Cons u ascarr * by (force intro: irreducible_prod_rI)
  qed 
qed

lemma (in comm_monoid) perm_wfactorsD:
  assumes prm: "as <~~> bs"
    and afs: "wfactors G as a"
    and bfs: "wfactors G bs b"
    and [simp]: "a ∈ carrier G"  "b ∈ carrier G"
    and ascarr [simp]: "set as ⊆ carrier G"
  shows "a ∼ b"
  using afs bfs
proof (elim wfactorsE)
  from prm have [simp]: "set bs ⊆ carrier G" by (simp add: perm_closed)
  assume "foldr (⊗) as 𝟭 ∼ a"
  then have "a ∼ foldr (⊗) as 𝟭"
    by (simp add: associated_sym)
  also from prm
  have "foldr (⊗) as 𝟭 = foldr (⊗) bs 𝟭" by (rule multlist_perm_cong, simp)
  also assume "foldr (⊗) bs 𝟭 ∼ b"
  finally show "a ∼ b" by simp
qed

lemma (in comm_monoid_cancel) listassoc_wfactorsD:
  assumes assoc: "as [∼] bs"
    and afs: "wfactors G as a"
    and bfs: "wfactors G bs b"
    and [simp]: "a ∈ carrier G"  "b ∈ carrier G"
    and [simp]: "set as ⊆ carrier G"  "set bs ⊆ carrier G"
  shows "a ∼ b"
  using afs bfs
proof (elim wfactorsE)
  assume "foldr (⊗) as 𝟭 ∼ a"
  then have "a ∼ foldr (⊗) as 𝟭" by (simp add: associated_sym)
  also from assoc
  have "foldr (⊗) as 𝟭 ∼ foldr (⊗) bs 𝟭" by (rule multlist_listassoc_cong, simp+)
  also assume "foldr (⊗) bs 𝟭 ∼ b"
  finally show "a ∼ b" by simp
qed

lemma (in comm_monoid_cancel) ee_wfactorsD:
  assumes ee: "essentially_equal G as bs"
    and afs: "wfactors G as a" and bfs: "wfactors G bs b"
    and [simp]: "a ∈ carrier G"  "b ∈ carrier G"
    and ascarr[simp]: "set as ⊆ carrier G" and bscarr[simp]: "set bs ⊆ carrier G"
  shows "a ∼ b"
  using ee
proof (elim essentially_equalE)
  fix fs
  assume prm: "as <~~> fs"
  then have as'carr[simp]: "set fs ⊆ carrier G"
    by (simp add: perm_closed)
  from afs prm have afs': "wfactors G fs a"
    by (rule wfactors_perm_cong_l) simp
  assume "fs [∼] bs"
  from this afs' bfs show "a ∼ b"
    by (rule listassoc_wfactorsD) simp_all
qed

lemma (in comm_monoid_cancel) ee_factorsD:
  assumes ee: "essentially_equal G as bs"
    and afs: "factors G as a" and bfs:"factors G bs b"
    and "set as ⊆ carrier G"  "set bs ⊆ carrier G"
  shows "a ∼ b"
  using assms by (blast intro: factors_wfactors dest: ee_wfactorsD)

lemma (in factorial_monoid) ee_factorsI:
  assumes ab: "a ∼ b"
    and afs: "factors G as a" and anunit: "a ∉ Units G"
    and bfs: "factors G bs b" and bnunit: "b ∉ Units G"
    and ascarr: "set as ⊆ carrier G" and bscarr: "set bs ⊆ carrier G"
  shows "essentially_equal G as bs"
proof -
  note carr[simp] = factors_closed[OF afs ascarr] ascarr[THEN subsetD]
    factors_closed[OF bfs bscarr] bscarr[THEN subsetD]

  from ab carr obtain u where uunit: "u ∈ Units G" and a: "a = b ⊗ u"
    by (elim associatedE2)

  from uunit bscarr have ee: "essentially_equal G (bs[0 := (bs!0 ⊗ u)]) bs"
    (is "essentially_equal G ?bs' bs")
    by (rule unitfactor_ee)

  from bscarr uunit have bs'carr: "set ?bs' ⊆ carrier G"
    by (cases bs) (simp_all add: Units_closed)

  from uunit bnunit bfs bscarr have fac: "factors G ?bs' (b ⊗ u)"
    by (rule factors_cong_unit)

  from afs fac[simplified a[symmetric]] ascarr bs'carr anunit
  have "essentially_equal G as ?bs'"
    by (blast intro: factors_unique)
  also note ee
  finally show "essentially_equal G as bs"
    by (simp add: ascarr bscarr bs'carr)
qed

lemma (in factorial_monoid) ee_wfactorsI:
  assumes asc: "a ∼ b"
    and asf: "wfactors G as a" and bsf: "wfactors G bs b"
    and acarr[simp]: "a ∈ carrier G" and bcarr[simp]: "b ∈ carrier G"
    and ascarr[simp]: "set as ⊆ carrier G" and bscarr[simp]: "set bs ⊆ carrier G"
  shows "essentially_equal G as bs"
  using assms
proof (cases "a ∈ Units G")
  case aunit: True
  also note asc
  finally have bunit: "b ∈ Units G" by simp

  from aunit asf ascarr have e: "as = []"
    by (rule unit_wfactors_empty)
  from bunit bsf bscarr have e': "bs = []"
    by (rule unit_wfactors_empty)

  have "essentially_equal G [] []"
    by (fast intro: essentially_equalI)
  then show ?thesis
    by (simp add: e e')
next
  case anunit: False
  have bnunit: "b ∉ Units G"
  proof clarify
    assume "b ∈ Units G"
    also note asc[symmetric]
    finally have "a ∈ Units G" by simp
    with anunit show False ..
  qed

  from wfactors_factors[OF asf ascarr] obtain a' where fa': "factors G as a'" and a': "a' ∼ a"
    by blast
  from fa' ascarr have a'carr[simp]: "a' ∈ carrier G"
    by fast

  have a'nunit: "a' ∉ Units G"
  proof clarify
    assume "a' ∈ Units G"
    also note a'
    finally have "a ∈ Units G" by simp
    with anunit
    show "False" ..
  qed

  from wfactors_factors[OF bsf bscarr] obtain b' where fb': "factors G bs b'" and b': "b' ∼ b"
    by blast
  from fb' bscarr have b'carr[simp]: "b' ∈ carrier G"
    by fast

  have b'nunit: "b' ∉ Units G"
  proof clarify
    assume "b' ∈ Units G"
    also note b'
    finally have "b ∈ Units G" by simp
    with bnunit show False ..
  qed

  note a'
  also note asc
  also note b'[symmetric]
  finally have "a' ∼ b'" by simp
  from this fa' a'nunit fb' b'nunit ascarr bscarr show "essentially_equal G as bs"
    by (rule ee_factorsI)
qed

lemma (in factorial_monoid) ee_wfactors:
  assumes asf: "wfactors G as a"
    and bsf: "wfactors G bs b"
    and acarr: "a ∈ carrier G" and bcarr: "b ∈ carrier G"
    and ascarr: "set as ⊆ carrier G" and bscarr: "set bs ⊆ carrier G"
  shows asc: "a ∼ b = essentially_equal G as bs"
  using assms by (fast intro: ee_wfactorsI ee_wfactorsD)

lemma (in factorial_monoid) wfactors_exist [intro, simp]:
  assumes acarr[simp]: "a ∈ carrier G"
  shows "∃fs. set fs ⊆ carrier G ∧ wfactors G fs a"
proof (cases "a ∈ Units G")
  case True
  then have "wfactors G [] a" by (rule unit_wfactors)
  then show ?thesis by (intro exI) force
next
  case False
  with factors_exist [OF acarr] obtain fs where fscarr: "set fs ⊆ carrier G" and f: "factors G fs a"
    by blast
  from f have "wfactors G fs a" by (rule factors_wfactors) fact
  with fscarr show ?thesis by fast
qed

lemma (in monoid) wfactors_prod_exists [intro, simp]:
  assumes "∀a ∈ set as. irreducible G a" and "set as ⊆ carrier G"
  shows "∃a. a ∈ carrier G ∧ wfactors G as a"
  unfolding wfactors_def using assms by blast

lemma (in factorial_monoid) wfactors_unique:
  assumes "wfactors G fs a"
    and "wfactors G fs' a"
    and "a ∈ carrier G"
    and "set fs ⊆ carrier G"
    and "set fs' ⊆ carrier G"
  shows "essentially_equal G fs fs'"
  using assms by (fast intro: ee_wfactorsI[of a a])

lemma (in monoid) factors_mult_single:
  assumes "irreducible G a" and "factors G fb b" and "a ∈ carrier G"
  shows "factors G (a # fb) (a ⊗ b)"
  using assms unfolding factors_def by simp

lemma (in monoid_cancel) wfactors_mult_single:
  assumes f: "irreducible G a"  "wfactors G fb b"
    "a ∈ carrier G"  "b ∈ carrier G"  "set fb ⊆ carrier G"
  shows "wfactors G (a # fb) (a ⊗ b)"
  using assms unfolding wfactors_def by (simp add: mult_cong_r)

lemma (in monoid) factors_mult:
  assumes factors: "factors G fa a"  "factors G fb b"
    and ascarr: "set fa ⊆ carrier G"
    and bscarr: "set fb ⊆ carrier G"
  shows "factors G (fa @ fb) (a ⊗ b)"
proof -
  have "foldr (⊗) (fa @ fb) 𝟭 = foldr (⊗) fa 𝟭 ⊗ foldr (⊗) fb 𝟭" if "set fa ⊆ carrier G" 
    "Ball (set fa) (irreducible G)"
    using that bscarr by (induct fa) (simp_all add: m_assoc)
  then show ?thesis
    using assms unfolding factors_def by force
qed

lemma (in comm_monoid_cancel) wfactors_mult [intro]:
  assumes asf: "wfactors G as a" and bsf:"wfactors G bs b"
    and acarr: "a ∈ carrier G" and bcarr: "b ∈ carrier G"
    and ascarr: "set as ⊆ carrier G" and bscarr:"set bs ⊆ carrier G"
  shows "wfactors G (as @ bs) (a ⊗ b)"
  using wfactors_factors[OF asf ascarr] and wfactors_factors[OF bsf bscarr]
proof clarsimp
  fix a' b'
  assume asf': "factors G as a'" and a'a: "a' ∼ a"
    and bsf': "factors G bs b'" and b'b: "b' ∼ b"
  from asf' have a'carr: "a' ∈ carrier G" by (rule factors_closed) fact
  from bsf' have b'carr: "b' ∈ carrier G" by (rule factors_closed) fact

  note carr = acarr bcarr a'carr b'carr ascarr bscarr

  from asf' bsf' have "factors G (as @ bs) (a' ⊗ b')"
    by (rule factors_mult) fact+

  with carr have abf': "wfactors G (as @ bs) (a' ⊗ b')"
    by (intro factors_wfactors) simp_all
  also from b'b carr have trb: "a' ⊗ b' ∼ a' ⊗ b"
    by (intro mult_cong_r)
  also from a'a carr have tra: "a' ⊗ b ∼ a ⊗ b"
    by (intro mult_cong_l)
  finally show "wfactors G (as @ bs) (a ⊗ b)"
    by (simp add: carr)
qed

lemma (in comm_monoid) factors_dividesI:
  assumes "factors G fs a"
    and "f ∈ set fs"
    and "set fs ⊆ carrier G"
  shows "f divides a"
  using assms by (fast elim: factorsE intro: multlist_dividesI)

lemma (in comm_monoid) wfactors_dividesI:
  assumes p: "wfactors G fs a"
    and fscarr: "set fs ⊆ carrier G" and acarr: "a ∈ carrier G"
    and f: "f ∈ set fs"
  shows "f divides a"
  using wfactors_factors[OF p fscarr]
proof clarsimp
  fix a'
  assume fsa': "factors G fs a'" and a'a: "a' ∼ a"
  with fscarr have a'carr: "a' ∈ carrier G"
    by (simp add: factors_closed)

  from fsa' fscarr f have "f divides a'"
    by (fast intro: factors_dividesI)
  also note a'a
  finally show "f divides a"
    by (simp add: f fscarr[THEN subsetD] acarr a'carr)
qed


subsubsection ‹Factorial monoids and wfactors›

lemma (in comm_monoid_cancel) factorial_monoidI:
  assumes wfactors_exists: "⋀a. ⟦ a ∈ carrier G; a ∉ Units G ⟧ ⟹ ∃fs. set fs ⊆ carrier G ∧ wfactors G fs a"
    and wfactors_unique:
      "⋀a fs fs'. ⟦a ∈ carrier G; set fs ⊆ carrier G; set fs' ⊆ carrier G;
        wfactors G fs a; wfactors G fs' a⟧ ⟹ essentially_equal G fs fs'"
  shows "factorial_monoid G"
proof
  fix a
  assume acarr: "a ∈ carrier G" and anunit: "a ∉ Units G"
  from wfactors_exists[OF acarr anunit]
  obtain as where ascarr: "set as ⊆ carrier G" and afs: "wfactors G as a"
    by blast
  from wfactors_factors [OF afs ascarr] obtain a' where afs': "factors G as a'" and a'a: "a' ∼ a"
    by blast
  from afs' ascarr have a'carr: "a' ∈ carrier G"
    by fast
  have a'nunit: "a' ∉ Units G"
  proof clarify
    assume "a' ∈ Units G"
    also note a'a
    finally have "a ∈ Units G" by (simp add: acarr)
    with anunit show False ..
  qed

  from a'carr acarr a'a obtain u where uunit: "u ∈ Units G" and a': "a' = a ⊗ u"
    by (blast elim: associatedE2)

  note [simp] = acarr Units_closed[OF uunit] Units_inv_closed[OF uunit]
  have "a = a ⊗ 𝟭" by simp
  also have "… = a ⊗ (u ⊗ inv u)" by (simp add: uunit)
  also have "… = a' ⊗ inv u" by (simp add: m_assoc[symmetric] a'[symmetric])
  finally have a: "a = a' ⊗ inv u" .

  from ascarr uunit have cr: "set (as[0:=(as!0 ⊗ inv u)]) ⊆ carrier G"
    by (cases as) auto
  from afs' uunit a'nunit acarr ascarr have "factors G (as[0:=(as!0 ⊗ inv u)]) a"
    by (simp add: a factors_cong_unit)
  with cr show "∃fs. set fs ⊆ carrier G ∧ factors G fs a"
    by fast
qed (blast intro: factors_wfactors wfactors_unique)


subsection ‹Factorizations as Multisets›

text ‹Gives useful operations like intersection›

(* FIXME: use class_of x instead of closure_of {x} *)

abbreviation "assocs G x ≡ eq_closure_of (division_rel G) {x}"

definition "fmset G as = mset (map (assocs G) as)"


text ‹Helper lemmas›

lemma (in monoid) assocs_repr_independence:
  assumes "y ∈ assocs G x" "x ∈ carrier G"
  shows "assocs G x = assocs G y"
  using assms
  by (simp add: eq_closure_of_def elem_def) (use associated_sym associated_trans in ‹blast+›)

lemma (in monoid) assocs_self:
  assumes "x ∈ carrier G"
  shows "x ∈ assocs G x"
  using assms by (fastforce intro: closure_ofI2)

lemma (in monoid) assocs_repr_independenceD:
  assumes repr: "assocs G x = assocs G y" and ycarr: "y ∈ carrier G"
  shows "y ∈ assocs G x"
  unfolding repr using ycarr by (intro assocs_self)

lemma (in comm_monoid) assocs_assoc:
  assumes "a ∈ assocs G b" "b ∈ carrier G"
  shows "a ∼ b"
  using assms by (elim closure_ofE2) simp

lemmas (in comm_monoid) assocs_eqD = assocs_repr_independenceD[THEN assocs_assoc]


subsubsection ‹Comparing multisets›

lemma (in monoid) fmset_perm_cong:
  assumes prm: "as <~~> bs"
  shows "fmset G as = fmset G bs"
  using perm_map[OF prm] unfolding fmset_def by blast

lemma (in comm_monoid_cancel) eqc_listassoc_cong:
  assumes "as [∼] bs" and "set as ⊆ carrier G" and "set bs ⊆ carrier G"
  shows "map (assocs G) as = map (assocs G) bs"
  using assms
proof (