Theory Divisibility

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

section ‹Divisibility in monoids and rings›

theory Divisibility
  imports "~~/src/HOL/Library/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) Units_m_closed[simp, intro]:
  assumes h1unit: "h1 ∈ Units G"
    and h2unit: "h2 ∈ Units G"
  shows "h1 ⊗ h2 ∈ Units G"
  unfolding Units_def
  using assms
  by auto (metis Units_inv_closed Units_l_inv Units_m_closed Units_r_inv)

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 dividesG b ⟷ (∃c∈carrier G. b = a ⊗G c)"

definition associated :: "[_, 'a, 'a] ⇒ bool" (infix "∼ı" 55)
  where "a ∼G b ⟷ a dividesG b ∧ b dividesG a"

abbreviation "division_rel G ≡ ⦇carrier = carrier G, eq = op ∼G, le = op dividesG⦈"

definition properfactor :: "[_, 'a, 'a] ⇒ bool"
  where "properfactor G a b ⟷ a dividesG b ∧ ¬(b dividesG 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 dividesG (a ⊗G b) ⟶ p dividesG a ∨ p dividesG 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 ab: "a divides b"
    and carr: "a ∈ carrier G"  "b ∈ carrier G"  "c ∈ carrier G"
  shows "(c ⊗ a) divides (c ⊗ b)"
  using ab
  apply (elim dividesE)
  apply (simp add: m_assoc[symmetric] carr)
  apply (fast intro: dividesI)
  done

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"
  apply safe
   apply (elim dividesE, intro dividesI, assumption)
   apply (rule l_cancel[of c])
      apply (simp add: m_assoc carr)+
  apply (fast intro: carr)
  done

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
  apply (simp add: m_comm[of a c] m_comm[of b c])
  apply (rule divides_mult_lI, assumption+)
  done

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"  "b ∈ 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 carr[intro]: "a ∈ carrier G"  "b ∈ carrier G"  "c ∈ carrier G"
    and ab: "a divides b"
  shows "a divides (c ⊗ b)"
  using ab carr
  apply (simp add: m_comm[of c b])
  apply (fast intro: divides_prod_r)
  done

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[simp]: "b ∈ carrier G"
  shows "a ∼ b"
  using uunit bcarr
  unfolding a
  apply (intro associatedI)
   apply (rule dividesI[of "inv u"], simp)
   apply (simp add: m_assoc Units_closed)
  apply fast
  done

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"
    and "a ∈ carrier G"  "b ∈ carrier G"
  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"  "b ∈ 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›

lemma divides_antisym:
  fixes G (structure)
  assumes "a divides b"  "b divides a"
    and "a ∈ carrier G"  "b ∈ carrier G"
  shows "a ∼ b"
  using assms by (fast intro: associatedI)

lemma (in monoid) divides_cong_l [trans]:
  assumes "x ∼ x'"
    and "x' divides y"
    and [simp]: "x ∈ carrier G"  "x' ∈ carrier G"  "y ∈ carrier G"
  shows "x divides y"
proof -
  from assms(1) have "x divides x'" by (simp add: associatedD)
  also note assms(2)
  finally show "x divides y" by simp
qed

lemma (in monoid) divides_cong_r [trans]:
  assumes "x divides y"
    and "y ∼ y'"
    and [simp]: "x ∈ carrier G"  "y ∈ carrier G"  "y' ∈ carrier G"
  shows "x divides y'"
proof -
  note assms(1)
  also from assms(2) have "y divides y'" by (simp add: associatedD)
  finally show "x divides y'" by simp
qed

lemma (in monoid) division_weak_partial_order [simp, intro!]:
  "weak_partial_order (division_rel G)"
  apply unfold_locales
        apply simp_all
      apply (simp add: associated_sym)
     apply (blast intro: associated_trans)
    apply (simp add: divides_antisym)
   apply (blast intro: divides_trans)
  apply (blast intro: divides_cong_l divides_cong_r associated_sym)
  done


subsubsection ‹Multiplication and associativity›

lemma (in monoid_cancel) mult_cong_r:
  assumes "b ∼ b'"
    and carr: "a ∈ carrier G"  "b ∈ carrier G"  "b' ∈ carrier G"
  shows "a ⊗ b ∼ a ⊗ b'"
  using assms
  apply (elim associatedE2, intro associatedI2)
      apply (auto intro: m_assoc[symmetric])
  done

lemma (in comm_monoid_cancel) mult_cong_l:
  assumes "a ∼ a'"
    and carr: "a ∈ carrier G"  "a' ∈ carrier G"  "b ∈ carrier G"
  shows "a ⊗ b ∼ a' ⊗ b"
  using assms
  apply (elim associatedE2, intro associatedI2)
      apply assumption
     apply (simp add: m_assoc Units_closed)
     apply (simp add: m_comm Units_closed)
    apply simp_all
  done

lemma (in monoid_cancel) assoc_l_cancel:
  assumes carr: "a ∈ carrier G"  "b ∈ carrier G"  "b' ∈ carrier G"
    and "a ⊗ b ∼ a ⊗ b'"
  shows "b ∼ b'"
  using assms
  apply (elim associatedE2, intro associatedI2)
      apply assumption
     apply (rule l_cancel[of a])
        apply (simp add: m_assoc Units_closed)
       apply fast+
  done

lemma (in comm_monoid_cancel) assoc_r_cancel:
  assumes "a ⊗ b ∼ a' ⊗ b"
    and carr: "a ∈ carrier G"  "a' ∈ carrier G"  "b ∈ carrier G"
  shows "a ∼ a'"
  using assms
  apply (elim associatedE2, intro associatedI2)
      apply assumption
     apply (rule r_cancel[of a b])
        apply (metis Units_closed assms(3) assms(4) m_ac)
       apply fast+
  done


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) {𝟭}"
  apply (simp add: set_eq_def elem_def, rule, simp_all)
proof clarsimp
  fix a
  assume aunit: "a ∈ Units G"
  show "a ∼ 𝟭"
    apply (rule associatedI)
     apply (fast intro: dividesI[of "inv a"] aunit Units_r_inv[symmetric])
    apply (fast intro: dividesI[of "a"] l_one[symmetric] Units_closed[OF aunit])
    done
next
  have "𝟭 ∈ Units G" by simp
  moreover have "𝟭 ∼ 𝟭" by simp
  ultimately show "∃a ∈ Units G. 𝟭 ∼ a" by fast
qed

lemma (in comm_monoid) Units_Lower: "Units G = Lower (division_rel G) (carrier G)"
  apply (simp add: Units_def Lower_def)
  apply (rule, rule)
   apply clarsimp
   apply (rule unit_divides)
    apply (unfold Units_def, fast)
   apply assumption
  apply clarsimp
  apply (metis Unit_eq_dividesone Units_r_inv_ex m_ac(2) one_closed)
  done


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"  "p ∈ 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 dvds: "a divides b"  "properfactor G b c"
    and carr: "a ∈ carrier G"  "b ∈ carrier G"  "c ∈ carrier G"
  shows "properfactor G a c"
  using dvds carr
  apply (elim properfactorE, intro properfactorI)
   apply (iprover intro: divides_trans)+
  done

lemma (in monoid) properfactor_trans2 [trans]:
  assumes dvds: "properfactor G a b"  "b divides c"
    and carr: "a ∈ carrier G"  "b ∈ carrier G"  "c ∈ carrier G"
  shows "properfactor G a c"
  using dvds carr
  apply (elim properfactorE, intro properfactorI)
   apply (iprover intro: divides_trans)+
  done

lemma properfactor_lless:
  fixes G (structure)
  shows "properfactor G = lless (division_rel G)"
  apply (rule ext)
  apply (rule ext)
  apply rule
   apply (fastforce elim: properfactorE2 intro: weak_llessI)
  apply (fastforce elim: weak_llessE intro: properfactorI2)
  done

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"  "b ∈ 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"  "b ∈ 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 irred: "irreducible G a"
    and aa': "a ∼ a'"
    and carr[simp]: "a ∈ carrier G"  "a' ∈ carrier G"
  shows "irreducible G a'"
  using assms
  apply (elim irreducibleE, intro irreducibleI)
   apply simp_all
   apply (metis assms(2) assms(3) assoc_unit_l)
  apply (metis assms(2) assms(3) assms(4) associated_sym properfactor_cong_r)
  done

lemma (in monoid) irreducible_prod_rI:
  assumes airr: "irreducible G a"
    and bunit: "b ∈ Units G"
    and carr[simp]: "a ∈ carrier G"  "b ∈ carrier G"
  shows "irreducible G (a ⊗ b)"
  using airr carr bunit
  apply (elim irreducibleE, intro irreducibleI, clarify)
   apply (subgoal_tac "a ∈ Units G", simp)
   apply (intro prod_unit_r[of a b] carr bunit, assumption)
  apply (metis assms(2,3) associatedI2 m_closed properfactor_cong_r)
  done

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)"
  apply (subst m_comm, simp+)
  apply (intro irreducible_prod_rI assms)
  done

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


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 pprime: "prime G p"
    and pp': "p ∼ p'"
    and carr[simp]: "p ∈ carrier G"  "p' ∈ carrier G"
  shows "prime G p'"
  using pprime
  apply (elim primeE, intro primeI)
   apply (metis assms(2) assms(3) assoc_unit_l)
  apply (metis assms(2) assms(3) assms(4) associated_sym divides_cong_l m_closed)
  done


subsection ‹Factorization and Factorial Monoids›

subsubsection ‹Function definitions›

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

definition wfactors ::"[_, 'a list, 'a] ⇒ bool"
  where "wfactors G fs a ⟷ (∀x ∈ (set fs). irreducible G x) ∧ foldr (op ⊗G) fs 𝟭GG a"

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

definition essentially_equal :: "[_, '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 (induct as arbitrary: bs, simp)
  case Cons
  then show ?case
    apply (induct bs)
     apply simp
    apply clarsimp
    apply (iprover intro: associated_sym)
    done
qed

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)
  apply (rule associated_trans)
      apply (subgoal_tac "as ! i ∼ bs ! i", assumption)
      apply (simp, simp)
    apply blast+
  done

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
  apply (clarsimp simp add: list_all2_conv_all_nth set_conv_nth)
  apply (blast intro: irreducible_cong)
  done


text ‹Permutations›

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

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"
  using p m by (induct arbitrary: a) (simp, force, force, blast)

lemma (in monoid) perm_assoc_switch:
  assumes a:"as [∼] bs" and p: "bs <~~> cs"
  shows "∃bs'. as <~~> bs' ∧ bs' [∼] cs"
  using p a
  apply (induct bs cs arbitrary: as, simp)
    apply (clarsimp simp add: list_all2_Cons2, blast)
   apply (clarsimp simp add: list_all2_Cons2)
   apply blast
  apply blast
  done

lemma (in monoid) perm_assoc_switch_r:
  assumes p: "as <~~> bs" and a:"bs [∼] cs"
  shows "∃bs'. as [∼] bs' ∧ bs' <~~> cs"
  using p a
  apply (induct as bs arbitrary: cs, simp)
    apply (clarsimp simp add: list_all2_Cons1, blast)
   apply (clarsimp simp add: list_all2_Cons1)
   apply blast
  apply blast
  done

declare perm_sym [sym]

lemma perm_setP:
  assumes perm: "as <~~> bs"
    and as: "P (set as)"
  shows "P (set bs)"
proof -
  from perm have "mset as = mset bs"
    by (simp add: mset_eq_perm)
  then have "set as = set bs"
    by (rule mset_eq_setD)
  with as show "P (set bs)"
    by simp
qed

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 fast

  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)
  note a
  also assume "bcs [∼] cs"
  finally (listassoc_trans) have "bs' [∼] cs" by (simp add: c1 c2 cscarr)
  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 (op ⊗) fs 𝟭 ∈ carrier G"
  using ascarr by (induct fs) simp_all

lemma  (in comm_monoid) multlist_dividesI (*[intro]*):
  assumes "f ∈ set fs" and "f ∈ carrier G" and "set fs ⊆ carrier G"
  shows "f divides (foldr (op ⊗) fs 𝟭)"
  using assms
  apply (induct fs)
   apply simp
  apply (case_tac "f = a")
   apply simp
   apply (fast intro: dividesI)
  apply clarsimp
  apply (metis assms(2) divides_prod_l multlist_closed)
  done

lemma (in comm_monoid_cancel) multlist_listassoc_cong:
  assumes "fs [∼] fs'"
    and "set fs ⊆ carrier G" and "set fs' ⊆ carrier G"
  shows "foldr (op ⊗) fs 𝟭 ∼ foldr (op ⊗) fs' 𝟭"
  using assms
proof (induct fs arbitrary: fs', simp)
  case (Cons a as fs')
  then show ?case
    apply (induct fs', simp)
  proof clarsimp
    fix b bs
    assume "a ∼ b"
      and acarr: "a ∈ carrier G" and bcarr: "b ∈ carrier G"
      and ascarr: "set as ⊆ carrier G"
    then have p: "a ⊗ foldr op ⊗ as 𝟭 ∼ b ⊗ foldr op ⊗ as 𝟭"
      by (fast intro: mult_cong_l)
    also
    assume "as [∼] bs"
      and bscarr: "set bs ⊆ carrier G"
      and "⋀fs'. ⟦as [∼] fs'; set fs' ⊆ carrier G⟧ ⟹ foldr op ⊗ as 𝟭 ∼ foldr op ⊗ fs' 𝟭"
    then have "foldr op ⊗ as 𝟭 ∼ foldr op ⊗ bs 𝟭" by simp
    with ascarr bscarr bcarr have "b ⊗ foldr op ⊗ as 𝟭 ∼ b ⊗ foldr op ⊗ bs 𝟭"
      by (fast intro: mult_cong_r)
    finally show "a ⊗ foldr op ⊗ as 𝟭 ∼ b ⊗ foldr op ⊗ bs 𝟭"
      by (simp add: ascarr bscarr acarr bcarr)
  qed
qed

lemma (in comm_monoid) multlist_perm_cong:
  assumes prm: "as <~~> bs"
    and ascarr: "set as ⊆ carrier G"
  shows "foldr (op ⊗) as 𝟭 = foldr (op ⊗) bs 𝟭"
  using prm ascarr
  apply (induct, simp, clarsimp simp add: m_ac, clarsimp)
proof clarsimp
  fix xs ys zs
  assume "xs <~~> ys"  "set xs ⊆ carrier G"
  then have "set ys ⊆ carrier G" by (rule perm_closed)
  moreover assume "set ys ⊆ carrier G ⟹ foldr op ⊗ ys 𝟭 = foldr op ⊗ zs 𝟭"
  ultimately show "foldr op ⊗ ys 𝟭 = foldr op ⊗ zs 𝟭" by simp
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 (op ⊗) fs 𝟭 ∼ foldr (op ⊗) fs' 𝟭"
  using assms
  apply (elim essentially_equalE)
  apply (simp add: multlist_perm_cong multlist_listassoc_cong perm_closed)
  done


subsubsection ‹Factorization in irreducible elements›

lemma wfactorsI:
  fixes G (structure)
  assumes "∀f∈set fs. irreducible G f"
    and "foldr (op ⊗) 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 (op ⊗) 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 (op ⊗) 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 (op ⊗) 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 Nil
  then show ?thesis .
next
  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 (op ⊗) fs' 𝟭 ∼ a" by (simp add: wfactors_def)

  note aunit
  also from fs wf
  have a: "f ⊗ foldr (op ⊗) fs' 𝟭 ∼ a" by (simp add: wfactors_def)
  have "a ∼ f ⊗ foldr (op ⊗) fs' 𝟭"
    by (simp add: Units_closed[OF aunit] a[symmetric])
  finally have "f ⊗ foldr (op ⊗) 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"
  using fact
  apply (elim wfactorsE, intro wfactorsI)
   apply (metis assms(2) assms(4) assms(5) irrlist_listassoc_cong)
proof -
  from asc[symmetric] have "foldr op ⊗ fs' 𝟭 ∼ foldr op ⊗ fs 𝟭"
    by (simp add: multlist_listassoc_cong carr)
  also assume "foldr op ⊗ fs 𝟭 ∼ a"
  finally show "foldr op ⊗ fs' 𝟭 ∼ a" by (simp add: carr)
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
  apply (elim wfactorsE, intro wfactorsI)
   apply (rule irrlist_perm_cong, assumption+)
  apply (simp add: multlist_perm_cong[symmetric])
  done

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" by (simp add: perm_closed)

  note bfs
  also assume [symmetric]: "fs [∼] bs"
  also (wfactors_listassoc_cong_l)
  note prm[symmetric]
  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 op ⊗ fs 𝟭 ∼ a" also note aa'
  finally show "foldr op ⊗ 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")
  using assms
  apply (intro essentially_equalI[of _ ?as'], simp)
  apply (cases as, simp)
  apply (clarsimp, fast intro: associatedI2[of u])
  done

lemma (in comm_monoid_cancel) factors_cong_unit:
  assumes uunit: "u ∈ Units G"
    and anunit: "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'")
  using assms
  apply (elim factorsE, clarify)
  apply (cases as)
   apply (simp add: nunit_factors)
  apply clarsimp
  apply (elim factorsE, intro factorsI)
   apply (clarsimp, fast intro: irreducible_prod_rI)
  apply (simp add: m_ac Units_closed)
  done

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 op ⊗ as 𝟭 ∼ a"
  then have "a ∼ foldr op ⊗ as 𝟭" by (rule associated_sym, simp+)
  also from prm
  have "foldr op ⊗ as 𝟭 = foldr op ⊗ bs 𝟭" by (rule multlist_perm_cong, simp)
  also assume "foldr op ⊗ 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 op ⊗ as 𝟭 ∼ a"
  then have "a ∼ foldr op ⊗ as 𝟭" by (rule associated_sym, simp+)
  also from assoc
  have "foldr op ⊗ as 𝟭 ∼ foldr op ⊗ bs 𝟭" by (rule multlist_listassoc_cong, simp+)
  also assume "foldr op ⊗ 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)"
  using assms
  unfolding factors_def
  apply safe
   apply force
  apply hypsubst_thin
  apply (induct fa)
   apply simp
  apply (simp add: m_assoc)
  done

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 ⟹ ∃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]
  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 (λa. assocs G a) as)"


text ‹Helper lemmas›

lemma (in monoid) assocs_repr_independence:
  assumes "y ∈ assocs G x"
    and "x ∈ carrier G"
  shows "assocs G x = assocs G y"
  using assms
  apply safe
   apply (elim closure_ofE2, intro closure_ofI2[of _ _ y])
     apply (clarsimp, iprover intro: associated_trans associated_sym, simp+)
  apply (elim closure_ofE2, intro closure_ofI2[of _ _ x])
    apply (clarsimp, iprover intro: associated_trans, simp+)
  done

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"
    and "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 mset_eq_perm 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
  apply (induct as arbitrary: bs, simp)
  apply (clarsimp simp add: Cons_eq_map_conv list_all2_Cons1, safe)
   apply (clarsimp elim!: closure_ofE2) defer 1
   apply (clarsimp elim!: closure_ofE2) defer 1
proof -
  fix a x z
  assume carr[simp]: "a ∈ carrier G"  "x ∈ carrier G"  "z ∈ carrier G"
  assume "x ∼ a"
  also assume "a ∼ z"
  finally have "x ∼ z" by simp
  with carr show "x ∈ assocs G z"
    by (intro closure_ofI2) simp_all
next
  fix a x z
  assume carr[simp]: "a ∈ carrier G"  "x ∈ carrier G"  "z ∈ carrier G"
  assume "x ∼ z"
  also assume [symmetric]: "a ∼ z"
  finally have "x ∼ a" by simp
  with carr show "x ∈ assocs G a"
    by (intro closure_ofI2) simp_all
qed

lemma (in comm_monoid_cancel) fmset_listassoc_cong:
  assumes "as [∼] bs"
    and "set as ⊆ carrier G" and "set bs ⊆ carrier G"
  shows "fmset G as = fmset G bs"
  using assms unfolding fmset_def by (simp add: eqc_listassoc_cong)

lemma (in comm_monoid_cancel) ee_fmset:
  assumes ee: "essentially_equal G as bs"
    and ascarr: "set as ⊆ carrier G" and bscarr: "set bs ⊆ carrier G"
  shows "fmset G as = fmset G bs"
  using ee
proof (elim essentially_equalE)
  fix as'
  assume prm: "as <~~> as'"
  from prm ascarr have as'carr: "set as' ⊆ carrier G"
    by (rule perm_closed)

  from prm have "fmset G as = fmset G as'"
    by (rule fmset_perm_cong)
  also assume "as' [∼] bs"
  with as'carr bscarr have "fmset G as' = fmset G bs"
    by (simp add: fmset_listassoc_cong)
  finally show "fmset G as = fmset G bs" .
qed

lemma (in monoid_cancel) fmset_ee__hlp_induct:
  assumes prm: "cas <~~> cbs"
    and cdef: "cas = map (assocs G) as"  "cbs = map (assocs G) bs"
  shows "∀as bs. (cas <~~> cbs ∧ cas = map (assocs G) as ∧
    cbs = map (assocs G) bs) ⟶ (∃as'. as <~~> as' ∧ map (assocs G) as' = cbs)"
  apply (rule perm.induct[of cas cbs], rule prm)
     apply safe
     apply (simp_all del: mset_map)
    apply (simp add: map_eq_Cons_conv)
    apply blast
   apply force
proof -
  fix ys as bs
  assume p1: "map (assocs G) as <~~> ys"
    and r1[rule_format]:
      "∀asa bs. map (assocs G) as = map (assocs G) asa ∧ ys = map (assocs G) bs
        ⟶ (∃as'. asa <~~> as' ∧ map (assocs G) as' = map (assocs G) bs)"
    and p2: "ys <~~> map (assocs G) bs"
    and r2[rule_format]: "∀as bsa. ys = map (assocs G) as ∧ map (assocs G) bs = map (assocs G) bsa
      ⟶ (∃as'. as <~~> as' ∧ map (assocs G) as' = map (assocs G) bsa)"
    and p3: "map (assocs G) as <~~> map (assocs G) bs"

  from p1 have "mset (map (assocs G) as) = mset ys"
    by (simp add: mset_eq_perm del: mset_map)
  then have setys: "set (map (assocs G) as) = set ys"
    by (rule mset_eq_setD)

  have "set (map (assocs G) as) = {assocs G x | x. x ∈ set as}" by auto
  with setys have "set ys ⊆ { assocs G x | x. x ∈ set as}" by simp
  then have "∃yy. ys = map (assocs G) yy"
  proof (induct ys)
    case Nil
    then show ?case by simp
  next
    case Cons
    then show ?case
    proof clarsimp
      fix yy x
      show "∃yya. assocs G x # map (assocs G) yy = map (assocs G) yya"
        by (rule exI[of _ "x#yy"]) simp
    qed
  qed
  then obtain yy where ys: "ys = map (assocs G) yy" ..

  from p1 ys have "∃as'. as <~~> as' ∧ map (assocs G) as' = map (assocs G) yy"
    by (intro r1) simp
  then obtain as' where asas': "as <~~> as'" and as'yy: "map (assocs G) as' = map (assocs G) yy"
    by auto

  from p2 ys have "∃as'. yy <~~> as' ∧ map (assocs G) as' = map (assocs G) bs"
    by (intro r2) simp
  then obtain as'' where yyas'': "yy <~~> as''" and as''bs: "map (assocs G) as'' = map (assocs G) bs"
    by auto

  from perm_map_switch [OF as'yy yyas'']
  obtain cs where as'cs: "as' <~~> cs" and csas'': "map (assocs G) cs = map (assocs G) as''"
    by blast

  from asas' and as'cs have ascs: "as <~~> cs"
    by fast
  from csas'' and as''bs have "map (assocs G) cs = map (assocs G) bs"
    by simp
  with ascs show "∃as'. as <~~> as' ∧ map (assocs G) as' = map (assocs G) bs"
    by fast
qed

lemma (in comm_monoid_cancel) fmset_ee:
  assumes mset: "fmset G as = fmset G bs"
    and ascarr: "set as ⊆ carrier G" and bscarr: "set bs ⊆ carrier G"
  shows "essentially_equal G as bs"
proof -
  from mset have mpp: "map (assocs G) as <~~> map (assocs G) bs"
    by (simp add: fmset_def mset_eq_perm del: mset_map)

  define cas where "cas = map (assocs G) as"
  define cbs where "cbs = map (assocs G) bs"

  from cas_def cbs_def mpp have [rule_format]:
    "∀as bs. (cas <~~> cbs ∧ cas = map (assocs G) as ∧ cbs = map (assocs G) bs)
      ⟶ (∃as'. as <~~> as' ∧ map (assocs G) as' = cbs)"
    by (intro fmset_ee__hlp_induct, simp+)
  with mpp cas_def cbs_def have "∃as'. as <~~> as' ∧ map (assocs G) as' = map (assocs G) bs"
    by simp

  then obtain as' where tp: "as <~~> as'" and tm: "map (assocs G) as' = map (assocs G) bs"
    by auto
  from tm have lene: "length as' = length bs"
    by (rule map_eq_imp_length_eq)
  from tp have "set as = set as'"
    by (simp add: mset_eq_perm mset_eq_setD)
  with ascarr have as'carr: "set as' ⊆ carrier G"
    by simp

  from tm as'carr[THEN subsetD] bscarr[THEN subsetD] have "as' [∼] bs"
    by (induct as' arbitrary: bs) (simp, fastforce dest: assocs_eqD[THEN associated_sym])
  with tp show "essentially_equal G as bs"
    by (fast intro: essentially_equalI)
qed

lemma (in comm_monoid_cancel) ee_is_fmset:
  assumes "set as ⊆ carrier G" and "set bs ⊆ carrier G"
  shows "essentially_equal G as bs = (fmset G as = fmset G bs)"
  using assms by (fast intro: ee_fmset fmset_ee)


subsubsection ‹Interpreting multisets as factorizations›

lemma (in monoid) mset_fmsetEx:
  assumes elems: "⋀X. X ∈ set_mset Cs ⟹ ∃x. P x ∧ X = assocs G x"
  shows "∃cs. (∀c ∈ set cs. P c) ∧ fmset G cs = Cs"
proof -
  from surjE[OF surj_mset] obtain Cs' where Cs: "Cs = mset Cs'"
    by blast
  have "∃cs. (∀c ∈ set cs. P c) ∧ mset (map (assocs G) cs) = Cs"
    using elems
    unfolding Cs
    apply (induct Cs', simp)
  proof (clarsimp simp del: mset_map)
    fix a Cs' cs
    assume ih: "⋀X. X = a ∨ X ∈ set Cs' ⟹ ∃x. P x ∧ X = assocs G x"
      and csP: "∀x∈set cs. P x"
      and mset: "mset (map (assocs G) cs) = mset Cs'"
    from ih obtain c where cP: "P c" and a: "a = assocs G c"
      by auto
    from cP csP have tP: "∀x∈set (c#cs). P x"
      by simp
    from mset a have "mset (map (assocs G) (c#cs)) = add_mset a (mset Cs')"
      by simp
    with tP show "∃cs. (∀x∈set cs. P x) ∧ mset (map (assocs G) cs) = add_mset a (mset Cs')"
      by fast
  qed
  then show ?thesis by (simp add: fmset_def)
qed

lemma (in monoid) mset_wfactorsEx:
  assumes elems: "⋀X. X ∈ set_mset Cs ⟹ ∃x. (x ∈ carrier G ∧ irreducible G x) ∧ X = assocs G x"
  shows "∃c cs. c ∈ carrier G ∧ set cs ⊆ carrier G ∧ wfactors G cs c ∧ fmset G cs = Cs"
proof -
  have "∃cs. (∀c∈set cs. c ∈ carrier G ∧ irreducible G c) ∧ fmset G cs = Cs"
    by (intro mset_fmsetEx, rule elems)
  then obtain cs where p[rule_format]: "∀c∈set cs. c ∈ carrier G ∧ irreducible G c"
    and Cs[symmetric]: "fmset G cs = Cs" by auto
  from p have cscarr: "set cs ⊆ carrier G" by fast
  from p have "∃c. c ∈ carrier G ∧ wfactors G cs c"
    by (intro wfactors_prod_exists) auto
  then obtain c where ccarr: "c ∈ carrier G" and cfs: "wfactors G cs c" by auto
  with cscarr Cs show ?thesis by fast
qed


subsubsection ‹Multiplication on multisets›

lemma (in factorial_monoid) mult_wfactors_fmset:
  assumes afs: "wfactors G as a"
    and bfs: "wfactors G bs b"
    and cfs: "wfactors G cs (a ⊗ b)"
    and carr: "a ∈ carrier G"  "b ∈ carrier G"
              "set as ⊆ carrier G"  "set bs ⊆ carrier G"  "set cs ⊆ carrier G"
  shows "fmset G cs = fmset G as + fmset G bs"
proof -
  from assms have "wfactors G (as @ bs) (a ⊗ b)"
    by (intro wfactors_mult)
  with carr cfs have "essentially_equal G cs (as@bs)"
    by (intro ee_wfactorsI[of "a⊗b" "a⊗b"]) simp_all
  with carr have "fmset G cs = fmset G (as@bs)"
    by (intro ee_fmset) simp_all
  also have "fmset G (as@bs) = fmset G as + fmset G bs"
    by (simp add: fmset_def)
  finally show "fmset G cs = fmset G as + fmset G bs" .
qed

lemma (in factorial_monoid) mult_factors_fmset:
  assumes afs: "factors G as a"
    and bfs: "factors G bs b"
    and cfs: "factors G cs (a ⊗ b)"
    and "set as ⊆ carrier G"  "set bs ⊆ carrier G"  "set cs ⊆ carrier G"
  shows "fmset G cs = fmset G as + fmset G bs"
  using assms by (blast intro: factors_wfactors mult_wfactors_fmset)

lemma (in comm_monoid_cancel) fmset_wfactors_mult:
  assumes mset: "fmset G cs = fmset G as + fmset G bs"
    and carr: "a ∈ carrier G"  "b ∈ carrier G"  "c ∈ carrier G"
      "set as ⊆ carrier G"  "set bs ⊆ carrier G"  "set cs ⊆ carrier G"
    and fs: "wfactors G as a"  "wfactors G bs b"  "wfactors G cs c"
  shows "c ∼ a ⊗ b"
proof -
  from carr fs have m: "wfactors G (as @ bs) (a ⊗ b)"
    by (intro wfactors_mult)

  from mset have "fmset G cs = fmset G (as@bs)"
    by (simp add: fmset_def)
  then have "essentially_equal G cs (as@bs)"
    by (rule fmset_ee) (simp_all add: carr)
  then show "c ∼ a ⊗ b"
    by (rule ee_wfactorsD[of "cs" "as@bs"]) (simp_all add: assms m)
qed


subsubsection ‹Divisibility on multisets›

lemma (in factorial_monoid) divides_fmsubset:
  assumes ab: "a divides b"
    and afs: "wfactors G as a"
    and bfs: "wfactors G bs b"
    and carr: "a ∈ carrier G"  "b ∈ carrier G"  "set as ⊆ carrier G"  "set bs ⊆ carrier G"
  shows "fmset G as ≤# fmset G bs"
  using ab
proof (elim dividesE)
  fix c
  assume ccarr: "c ∈ carrier G"
  from wfactors_exist [OF this]
  obtain cs where cscarr: "set cs ⊆ carrier G" and cfs: "wfactors G cs c"
    by blast
  note carr = carr ccarr cscarr

  assume "b = a ⊗ c"
  with afs bfs cfs carr have "fmset G bs = fmset G as + fmset G cs"
    by (intro mult_wfactors_fmset[OF afs cfs]) simp_all
  then show ?thesis by simp
qed

lemma (in comm_monoid_cancel) fmsubset_divides:
  assumes msubset: "fmset G as ≤# fmset G bs"
    and afs: "wfactors G as a"
    and bfs: "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 "a divides b"
proof -
  from afs have airr: "∀a ∈ set as. irreducible G a" by (fast elim: wfactorsE)
  from bfs have birr: "∀b ∈ set bs. irreducible G b" by (fast elim: wfactorsE)

  have "∃c cs. c ∈ carrier G ∧ set cs ⊆ carrier G ∧ wfactors G cs c ∧ fmset G cs = fmset G bs - fmset G as"
  proof (intro mset_wfactorsEx, simp)
    fix X
    assume "X ∈# fmset G bs - fmset G as"
    then have "X ∈# fmset G bs" by (rule in_diffD)
    then have "X ∈ set (map (assocs G) bs)" by (simp add: fmset_def)
    then have "∃x. x ∈ set bs ∧ X = assocs G x" by (induct bs) auto
    then obtain x where xbs: "x ∈ set bs" and X: "X = assocs G x" by auto
    with bscarr have xcarr: "x ∈ carrier G" by fast
    from xbs birr have xirr: "irreducible G x" by simp

    from xcarr and xirr and X show "∃x. x ∈ carrier G ∧ irreducible G x ∧ X = assocs G x"
      by fast
  qed
  then obtain c cs
    where ccarr: "c ∈ carrier G"
      and cscarr: "set cs ⊆ carrier G"
      and csf: "wfactors G cs c"
      and csmset: "fmset G cs = fmset G bs - fmset G as" by auto

  from csmset msubset
  have "fmset G bs = fmset G as + fmset G cs"
    by (simp add: multiset_eq_iff subseteq_mset_def)
  then have basc: "b ∼ a ⊗ c"
    by (rule fmset_wfactors_mult) fact+
  then show ?thesis
  proof (elim associatedE2)
    fix u
    assume "u ∈ Units G"  "b = a ⊗ c ⊗ u"
    with acarr ccarr show "a divides b"
      by (fast intro: dividesI[of "c ⊗ u"] m_assoc)
  qed (simp_all add: acarr bcarr ccarr)
qed

lemma (in factorial_monoid) divides_as_fmsubset:
  assumes "wfactors G as a"
    and "wfactors G bs b"
    and "a ∈ carrier G"
    and "b ∈ carrier G"
    and "set as ⊆ carrier G"
    and "set bs ⊆ carrier G"
  shows "a divides b = (fmset G as ≤# fmset G bs)"
  using assms
  by (blast intro: divides_fmsubset fmsubset_divides)


text ‹Proper factors on multisets›

lemma (in factorial_monoid) fmset_properfactor:
  assumes asubb: "fmset G as ≤# fmset G bs"
    and anb: "fmset G as ≠ fmset G bs"
    and "wfactors G as a"
    and "wfactors G bs b"
    and "a ∈ carrier G"
    and "b ∈ carrier G"
    and "set as ⊆ carrier G"
    and "set bs ⊆ carrier G"
  shows "properfactor G a b"
  apply (rule properfactorI)
   apply (rule fmsubset_divides[of as bs], fact+)
proof
  assume "b divides a"
  then have "fmset G bs ≤# fmset G as"
    by (rule divides_fmsubset) fact+
  with asubb have "fmset G as = fmset G bs"
    by (rule subset_mset.antisym)
  with anb show False ..
qed

lemma (in factorial_monoid) properfactor_fmset:
  assumes pf: "properfactor G a b"
    and "wfactors G as a"
    and "wfactors G bs b"
    and "a ∈ carrier G"
    and "b ∈ carrier G"
    and "set as ⊆ carrier G"
    and "set bs ⊆ carrier G"
  shows "fmset G as ≤# fmset G bs ∧ fmset G as ≠ fmset G bs"
  using pf
  apply (elim properfactorE)
  apply rule
   apply (intro divides_fmsubset, assumption)
        apply (rule assms)+
  using assms(2,3,4,6,7) divides_as_fmsubset
  apply auto
  done

subsection ‹Irreducible Elements are Prime›

lemma (in factorial_monoid) irreducible_prime:
  assumes pirr: "irreducible G p"
    and pcarr: "p ∈ carrier G"
  shows "prime G p"
  using pirr
proof (elim irreducibleE, intro primeI)
  fix a b
  assume acarr: "a ∈ carrier G"  and bcarr: "b ∈ carrier G"
    and pdvdab: "p divides (a ⊗ b)"
    and pnunit: "p ∉ Units G"
  assume irreduc[rule_format]:
    "∀b. b ∈ carrier G ∧ properfactor G b p ⟶ b ∈ Units G"
  from pdvdab obtain c where ccarr: "c ∈ carrier G" and abpc: "a ⊗ b = p ⊗ c"
    by (rule dividesE)

  from wfactors_exist [OF acarr]
  obtain as where ascarr: "set as ⊆ carrier G" and afs: "wfactors G as a"
    by blast

  from wfactors_exist [OF bcarr]
  obtain bs where bscarr: "set bs ⊆ carrier G" and bfs: "wfactors G bs b"
    by auto

  from wfactors_exist [OF ccarr]
  obtain cs where cscarr: "set cs ⊆ carrier G" and cfs: "wfactors G cs c"
    by auto

  note carr[simp] = pcarr acarr bcarr ccarr ascarr bscarr cscarr

  from afs and bfs have abfs: "wfactors G (as @ bs) (a ⊗ b)"
    by (rule wfactors_mult) fact+

  from pirr cfs have pcfs: "wfactors G (p # cs) (p ⊗ c)"
    by (rule wfactors_mult_single) fact+
  with abpc have abfs': "wfactors G (p # cs) (a ⊗ b)"
    by simp

  from abfs' abfs have "essentially_equal G (p # cs) (as @ bs)"
    by (rule wfactors_unique) simp+

  then obtain ds where "p # cs <~~> ds" and dsassoc: "ds [∼] (as @ bs)"
    by (fast elim: essentially_equalE)
  then have "p ∈ set ds"
    by (simp add: perm_set_eq[symmetric])
  with dsassoc obtain p' where "p' ∈ set (as@bs)" and pp': "p ∼ p'"
    unfolding list_all2_conv_all_nth set_conv_nth by force
  then consider "p' ∈ set as" | "p' ∈ set bs" by auto
  then show "p divides a ∨ p divides b"
  proof cases
    case 1
    with ascarr have [simp]: "p' ∈ carrier G" by fast

    note pp'
    also from afs
    have "p' divides a" by (rule wfactors_dividesI) fact+
    finally have "p divides a" by simp
    then show ?thesis ..
  next
    case 2
    with bscarr have [simp]: "p' ∈ carrier G" by fast

    note pp'
    also from bfs
    have "p' divides b" by (rule wfactors_dividesI) fact+
    finally have "p divides b" by simp
    then show ?thesis ..
  qed
qed


"A version using @{const factors}, more complicated"
lemma (in factorial_monoid) factors_irreducible_prime:
  assumes pirr: "irreducible G p"
    and pcarr: "p ∈ carrier G"
  shows "prime G p"
  using pirr
  apply (elim irreducibleE, intro primeI)
   apply assumption
proof -
  fix a b
  assume acarr: "a ∈ carrier G"
    and bcarr: "b ∈ carrier G"
    and pdvdab: "p divides (a ⊗ b)"
  assume irreduc[rule_format]: "∀b. b ∈ carrier G ∧ properfactor G b p ⟶ b ∈ Units G"
  from pdvdab obtain c where ccarr: "c ∈ carrier G" and abpc: "a ⊗ b = p ⊗ c"
    by (rule dividesE)
  note [simp] = pcarr acarr bcarr ccarr

  show "p divides a ∨ p divides b"
  proof (cases "a ∈ Units G")
    case aunit: True

    note pdvdab
    also have "a ⊗ b = b ⊗ a" by (simp add: m_comm)
    also from aunit have bab: "b ⊗ a ∼ b"
      by (intro associatedI2[of "a"], simp+)
    finally have "p divides b" by simp
    then show ?thesis ..
  next
    case anunit: False
    show ?thesis
    proof (cases "b ∈ Units G")
      case bunit: True
      note pdvdab
      also from bunit
      have baa: "a ⊗ b ∼ a"
        by (intro associatedI2[of "b"], simp+)
      finally have "p divides a" by simp
      then show ?thesis ..
    next
      case bnunit: False
      have cnunit: "c ∉ Units G"
      proof
        assume cunit: "c ∈ Units G"
        from bnunit have "properfactor G a (a ⊗ b)"
          by (intro properfactorI3[of _ _ b], simp+)
        also note abpc
        also from cunit have "p ⊗ c ∼ p"
          by (intro associatedI2[of c], simp+)
        finally have "properfactor G a p" by simp
        with acarr have "a ∈ Units G" by (fast intro: irreduc)
        with anunit show False ..
      qed

      have abnunit: "a ⊗ b ∉ Units G"
      proof clarsimp
        assume "a ⊗ b ∈ Units G"
        then have "a ∈ Units G" by (rule unit_factor) fact+
        with anunit show False ..
      qed

      from factors_exist [OF acarr anunit]
      obtain as where ascarr: "set as ⊆ carrier G" and afac: "factors G as a"
        by blast

      from factors_exist [OF bcarr bnunit]
      obtain bs where bscarr: "set bs ⊆ carrier G" and bfac: "factors G bs b"
        by blast

      from factors_exist [OF ccarr cnunit]
      obtain cs where cscarr: "set cs ⊆ carrier G" and cfac: "factors G cs c"
        by auto

      note [simp] = ascarr bscarr cscarr

      from afac and bfac have abfac: "factors G (as @ bs) (a ⊗ b)"
        by (rule factors_mult) fact+

      from pirr cfac have pcfac: "factors G (p # cs) (p ⊗ c)"
        by (rule factors_mult_single) fact+
      with abpc have abfac': "factors G (p # cs) (a ⊗ b)"
        by simp

      from abfac' abfac have "essentially_equal G (p # cs) (as @ bs)"
        by (rule factors_unique) (fact | simp)+
      then obtain ds where "p # cs <~~> ds" and dsassoc: "ds [∼] (as @ bs)"
        by (fast elim: essentially_equalE)
      then have "p ∈ set ds"
        by (simp add: perm_set_eq[symmetric])
      with dsassoc obtain p' where "p' ∈ set (as@bs)" and pp': "p ∼ p'"
        unfolding list_all2_conv_all_nth set_conv_nth by force
      then consider "p' ∈ set as" | "p' ∈ set bs" by auto
      then show "p divides a ∨ p divides b"
      proof cases
        case 1
        with ascarr have [simp]: "p' ∈ carrier G" by fast

        note pp'
        also from afac 1 have "p' divides a" by (rule factors_dividesI) fact+
        finally have "p divides a" by simp
        then show ?thesis ..
      next
        case 2
        with bscarr have [simp]: "p' ∈ carrier G" by fast

        note pp'
        also from bfac
        have "p' divides b" by (rule factors_dividesI) fact+
        finally have "p divides b" by simp
        then show ?thesis ..
      qed
    qed
  qed
qed


subsection ‹Greatest Common Divisors and Lowest Common Multiples›

subsubsection ‹Definitions›

definition isgcd :: "[('a,_) monoid_scheme, 'a, 'a, 'a] ⇒ bool"  ("(_ gcdofı _ _)" [81,81,81] 80)
  where "x gcdofG a b ⟷ x dividesG a ∧ x dividesG b ∧
    (∀y∈carrier G. (y dividesG a ∧ y dividesG b ⟶ y dividesG x))"

definition islcm :: "[_, 'a, 'a, 'a] ⇒ bool"  ("(_ lcmofı _ _)" [81,81,81] 80)
  where "x lcmofG a b ⟷ a dividesG x ∧ b dividesG x ∧
    (∀y∈carrier G. (a dividesG y ∧ b dividesG y ⟶ x dividesG y))"

definition somegcd :: "('a,_) monoid_scheme ⇒ 'a ⇒ 'a ⇒ 'a"
  where "somegcd G a b = (SOME x. x ∈ carrier G ∧ x gcdofG a b)"

definition somelcm :: "('a,_) monoid_scheme ⇒ 'a ⇒ 'a ⇒ 'a"
  where "somelcm G a b = (SOME x. x ∈ carrier G ∧ x lcmofG a b)"

definition "SomeGcd G A = inf (division_rel G) A"


locale gcd_condition_monoid = comm_monoid_cancel +
  assumes gcdof_exists: "⟦a ∈ carrier G; b ∈ carrier G⟧ ⟹ ∃c. c ∈ carrier G ∧ c gcdof a b"

locale primeness_condition_monoid = comm_monoid_cancel +
  assumes irreducible_prime: "⟦a ∈ carrier G; irreducible G a⟧ ⟹ prime G a"

locale divisor_chain_condition_monoid = comm_monoid_cancel +
  assumes division_wellfounded: "wf {(x, y). x ∈ carrier G ∧ y ∈ carrier G ∧ properfactor G x y}"


subsubsection ‹Connections to \texttt{Lattice.thy}›

lemma gcdof_greatestLower:
  fixes G (structure)
  assumes carr[simp]: "a ∈ carrier G"  "b ∈ carrier G"
  shows "(x ∈ carrier G ∧ x gcdof a b) = greatest (division_rel G) x (Lower (division_rel G) {a, b})"
  by (auto simp: isgcd_def greatest_def Lower_def elem_def)

lemma lcmof_leastUpper:
  fixes G (structure)
  assumes carr[simp]: "a ∈ carrier G"  "b ∈ carrier G"
  shows "(x ∈ carrier G ∧ x lcmof a b) = least (division_rel G) x (Upper (division_rel G) {a, b})"
  by (auto simp: islcm_def least_def Upper_def elem_def)

lemma somegcd_meet:
  fixes G (structure)
  assumes carr: "a ∈ carrier G"  "b ∈ carrier G"
  shows "somegcd G a b = meet (division_rel G) a b"
  by (simp add: somegcd_def meet_def inf_def gcdof_greatestLower[OF carr])

lemma (in monoid) isgcd_divides_l:
  assumes "a divides b"
    and "a ∈ carrier G"  "b ∈ carrier G"
  shows "a gcdof a b"
  using assms unfolding isgcd_def by fast

lemma (in monoid) isgcd_divides_r:
  assumes "b divides a"
    and "a ∈ carrier G"  "b ∈ carrier G"
  shows "b gcdof a b"
  using assms unfolding isgcd_def by fast


subsubsection ‹Existence of gcd and lcm›

lemma (in factorial_monoid) gcdof_exists:
  assumes acarr: "a ∈ carrier G"
    and bcarr: "b ∈ carrier G"
  shows "∃c. c ∈ carrier G ∧ c gcdof a b"
proof -
  from wfactors_exist [OF acarr]
  obtain as where ascarr: "set as ⊆ carrier G" and afs: "wfactors G as a"
    by blast
  from afs have airr: "∀a ∈ set as. irreducible G a"
    by (fast elim: wfactorsE)

  from wfactors_exist [OF bcarr]
  obtain bs where bscarr: "set bs ⊆ carrier G" and bfs: "wfactors G bs b"
    by blast
  from bfs have birr: "∀b ∈ set bs. irreducible G b"
    by (fast elim: wfactorsE)

  have "∃c cs. c ∈ carrier G ∧ set cs ⊆ carrier G ∧ wfactors G cs c ∧
    fmset G cs = fmset G as ∩# fmset G bs"
  proof (intro mset_wfactorsEx)
    fix X
    assume "X ∈# fmset G as ∩# fmset G bs"
    then have "X ∈# fmset G as" by simp
    then have "X ∈ set (map (assocs G) as)"
      by (simp add: fmset_def)
    then have "∃x. X = assocs G x ∧ x ∈ set as"
      by (induct as) auto
    then obtain x where X: "X = assocs G x" and xas: "x ∈ set as"
      by blast
    with ascarr have xcarr: "x ∈ carrier G"
      by blast
    from xas airr have xirr: "irreducible G x"
      by simp
    from xcarr and xirr and X show "∃x. (x ∈ carrier G ∧ irreducible G x) ∧ X = assocs G x"
      by blast
  qed
  then obtain c cs
    where ccarr: "c ∈ carrier G"
      and cscarr: "set cs ⊆ carrier G"
      and csirr: "wfactors G cs c"
      and csmset: "fmset G cs = fmset G as ∩# fmset G bs"
    by auto

  have "c gcdof a b"
  proof (simp add: isgcd_def, safe)
    from csmset
    have "fmset G cs ≤# fmset G as"
      by (simp add: multiset_inter_def subset_mset_def)
    then show "c divides a" by (rule fmsubset_divides) fact+
  next
    from csmset have "fmset G cs ≤# fmset G bs"
      by (simp add: multiset_inter_def subseteq_mset_def, force)
    then show "c divides b"
      by (rule fmsubset_divides) fact+
  next
    fix y
    assume "y ∈ carrier G"
    from wfactors_exist [OF this]
    obtain ys where yscarr: "set ys ⊆ carrier G" and yfs: "wfactors G ys y"
      by blast

    assume "y divides a"
    then have ya: "fmset G ys ≤# fmset G as"
      by (rule divides_fmsubset) fact+

    assume "y divides b"
    then have yb: "fmset G ys ≤# fmset G bs"
      by (rule divides_fmsubset) fact+

    from ya yb csmset have "fmset G ys ≤# fmset G cs"
      by (simp add: subset_mset_def)
    then show "y divides c"
      by (rule fmsubset_divides) fact+
  qed
  with ccarr show "∃c. c ∈ carrier G ∧ c gcdof a b"
    by fast
qed

lemma (in factorial_monoid) lcmof_exists:
  assumes acarr: "a ∈ carrier G"
    and bcarr: "b ∈ carrier G"
  shows "∃c. c ∈ carrier G ∧ c lcmof a b"
proof -
  from wfactors_exist [OF acarr]
  obtain as where ascarr: "set as ⊆ carrier G" and afs: "wfactors G as a"
    by blast
  from afs have airr: "∀a ∈ set as. irreducible G a"
    by (fast elim: wfactorsE)

  from wfactors_exist [OF bcarr]
  obtain bs where bscarr: "set bs ⊆ carrier G" and bfs: "wfactors G bs b"
    by blast
  from bfs have birr: "∀b ∈ set bs. irreducible G b"
    by (fast elim: wfactorsE)

  have "∃c cs. c ∈ carrier G ∧ set cs ⊆ carrier G ∧ wfactors G cs c ∧
    fmset G cs = (fmset G as - fmset G bs) + fmset G bs"
  proof (intro mset_wfactorsEx)
    fix X
    assume "X ∈# (fmset G as - fmset G bs) + fmset G bs"
    then have "X ∈# fmset G as ∨ X ∈# fmset G bs"
      by (auto dest: in_diffD)
    then consider "X ∈ set_mset (fmset G as)" | "X ∈ set_mset (fmset G bs)"
      by fast
    then show "∃x. (x ∈ carrier G ∧ irreducible G x) ∧ X = assocs G x"
    proof cases
      case 1
      then have "X ∈ set (map (assocs G) as)" by (simp add: fmset_def)
      then have "∃x. x ∈ set as ∧ X = assocs G x" by (induct as) auto
      then obtain x where xas: "x ∈ set as" and X: "X = assocs G x" by auto
      with ascarr have xcarr: "x ∈ carrier G" by fast
      from xas airr have xirr: "irreducible G x" by simp
      from xcarr and xirr and X show ?thesis by fast
    next
      case 2
      then have "X ∈ set (map (assocs G) bs)" by (simp add: fmset_def)
      then have "∃x. x ∈ set bs ∧ X = assocs G x" by (induct as) auto
      then obtain x where xbs: "x ∈ set bs" and X: "X = assocs G x" by auto
      with bscarr have xcarr: "x ∈ carrier G" by fast
      from xbs birr have xirr: "irreducible G x" by simp
      from xcarr and xirr and X show ?thesis by fast
    qed
  qed
  then obtain c cs
    where ccarr: "c ∈ carrier G"
      and cscarr: "set cs ⊆ carrier G"
      and csirr: "wfactors G cs c"
      and csmset: "fmset G cs = fmset G as - fmset G bs + fmset G bs"
    by auto

  have "c lcmof a b"
  proof (simp add: islcm_def, safe)
    from csmset have "fmset G as ≤# fmset G cs"
      by (simp add: subseteq_mset_def, force)
    then show "a divides c"
      by (rule fmsubset_divides) fact+
  next
    from csmset have "fmset G bs ≤# fmset G cs"
      by (simp add: subset_mset_def)
    then show "b divides c"
      by (rule fmsubset_divides) fact+
  next
    fix y
    assume "y ∈ carrier G"
    from wfactors_exist [OF this]
    obtain ys where yscarr: "set ys ⊆ carrier G" and yfs: "wfactors G ys y"
      by blast

    assume "a divides y"
    then have ya: "fmset G as ≤# fmset G ys"
      by (rule divides_fmsubset) fact+

    assume "b divides y"
    then have yb: "fmset G bs ≤# fmset G ys"
      by (rule divides_fmsubset) fact+

    from ya yb csmset have "fmset G cs ≤# fmset G ys"
      apply (simp add: subseteq_mset_def, clarify)
      apply (case_tac "count (fmset G as) a < count (fmset G bs) a")
       apply simp
      apply simp
      done
    then show "c divides y"
      by (rule fmsubset_divides) fact+
  qed
  with ccarr show "∃c. c ∈ carrier G ∧ c lcmof a b"
    by fast
qed


subsection ‹Conditions for Factoriality›

subsubsection ‹Gcd condition›

lemma (in gcd_condition_monoid) division_weak_lower_semilattice [simp]:
  "weak_lower_semilattice (division_rel G)"
proof -
  interpret weak_partial_order "division_rel G" ..
  show ?thesis
    apply (unfold_locales, simp_all)
  proof -
    fix x y
    assume carr: "x ∈ carrier G"  "y ∈ carrier G"
    from gcdof_exists [OF this] obtain z where zcarr: "z ∈ carrier G" and isgcd: "z gcdof x y"
      by blast
    with carr have "greatest (division_rel G) z (Lower (division_rel G) {x, y})"
      by (subst gcdof_greatestLower[symmetric], simp+)
    then show "∃z. greatest (division_rel G) z (Lower (division_rel G) {x, y})"
      by fast
  qed
qed

lemma (in gcd_condition_monoid) gcdof_cong_l:
  assumes a'a: "a' ∼ a"
    and agcd: "a gcdof b c"
    and a'carr: "a' ∈ carrier G" and carr': "a ∈ carrier G"  "b ∈ carrier G"  "c ∈ carrier G"
  shows "a' gcdof b c"
proof -
  note carr = a'carr carr'
  interpret weak_lower_semilattice "division_rel G" by simp
  have "a' ∈ carrier G ∧ a' gcdof b c"
    apply (simp add: gcdof_greatestLower carr')
    apply (subst greatest_Lower_cong_l[of _ a])
        apply (simp add: a'a)
       apply (simp add: carr)
      apply (simp add: carr)
     apply (simp add: carr)
    apply (simp add: gcdof_greatestLower[symmetric] agcd carr)
    done
  then show ?thesis ..
qed

lemma (in gcd_condition_monoid) gcd_closed [simp]:
  assumes carr: "a ∈ carrier G"  "b ∈ carrier G"
  shows "somegcd G a b ∈ carrier G"
proof -
  interpret weak_lower_semilattice "division_rel G" by simp
  show ?thesis
    apply (simp add: somegcd_meet[OF carr])
    apply (rule meet_closed[simplified], fact+)
    done
qed

lemma (in gcd_condition_monoid) gcd_isgcd:
  assumes carr: "a ∈ carrier G"  "b ∈ carrier G"
  shows "(somegcd G a b) gcdof a b"
proof -
  interpret weak_lower_semilattice "division_rel G"
    by simp
  from carr have "somegcd G a b ∈ carrier G ∧ (somegcd G a b) gcdof a b"
    apply (subst gcdof_greatestLower, simp, simp)
    apply (simp add: somegcd_meet[OF carr] meet_def)
    apply (rule inf_of_two_greatest[simplified], assumption+)
    done
  then show "(somegcd G a b) gcdof a b"
    by simp
qed

lemma (in gcd_condition_monoid) gcd_exists:
  assumes carr: "a ∈ carrier G"  "b ∈ carrier G"
  shows "∃x∈carrier G. x = somegcd G a b"
proof -
  interpret weak_lower_semilattice "division_rel G"
    by simp
  show ?thesis
    by (metis carr(1) carr(2) gcd_closed)
qed

lemma (in gcd_condition_monoid) gcd_divides_l:
  assumes carr: "a ∈ carrier G"  "b ∈ carrier G"
  shows "(somegcd G a b) divides a"
proof -
  interpret weak_lower_semilattice "division_rel G"
    by simp
  show ?thesis
    by (metis carr(1) carr(2) gcd_isgcd isgcd_def)
qed

lemma (in gcd_condition_monoid) gcd_divides_r:
  assumes carr: "a ∈ carrier G"  "b ∈ carrier G"
  shows "(somegcd G a b) divides b"
proof -
  interpret weak_lower_semilattice "division_rel G"
    by simp
  show ?thesis
    by (metis carr gcd_isgcd isgcd_def)
qed

lemma (in gcd_condition_monoid) gcd_divides:
  assumes sub: "z divides x"  "z divides y"
    and L: "x ∈ carrier G"  "y ∈ carrier G"  "z ∈ carrier G"
  shows "z divides (somegcd G x y)"
proof -
  interpret weak_lower_semilattice "division_rel G"
    by simp
  show ?thesis
    by (metis gcd_isgcd isgcd_def assms)
qed

lemma (in gcd_condition_monoid) gcd_cong_l:
  assumes xx': "x ∼ x'"
    and carr: "x ∈ carrier G"  "x' ∈ carrier G"  "y ∈ carrier G"
  shows "somegcd G x y ∼ somegcd G x' y"
proof -
  interpret weak_lower_semilattice "division_rel G"
    by simp
  show ?thesis
    apply (simp add: somegcd_meet carr)
    apply (rule meet_cong_l[simplified], fact+)
    done
qed

lemma (in gcd_condition_monoid) gcd_cong_r:
  assumes carr: "x ∈ carrier G"  "y ∈ carrier G"  "y' ∈ carrier G"
    and yy': "y ∼ y'"
  shows "somegcd G x y ∼ somegcd G x y'"
proof -
  interpret weak_lower_semilattice "division_rel G" by simp
  show ?thesis
    apply (simp add: somegcd_meet carr)
    apply (rule meet_cong_r[simplified], fact+)
    done
qed

(*
lemma (in gcd_condition_monoid) asc_cong_gcd_l [intro]:
  assumes carr: "b ∈ carrier G"
  shows "asc_cong (λa. somegcd G a b)"
using carr
unfolding CONG_def
by clarsimp (blast intro: gcd_cong_l)

lemma (in gcd_condition_monoid) asc_cong_gcd_r [intro]:
  assumes carr: "a ∈ carrier G"
  shows "asc_cong (λb. somegcd G a b)"
using carr
unfolding CONG_def
by clarsimp (blast intro: gcd_cong_r)

lemmas (in gcd_condition_monoid) asc_cong_gcd_split [simp] =
    assoc_split[OF _ asc_cong_gcd_l] assoc_split[OF _ asc_cong_gcd_r]
*)

lemma (in gcd_condition_monoid) gcdI:
  assumes dvd: "a divides b"  "a divides c"
    and others: "∀y∈carrier G. y divides b ∧ y divides c ⟶ y divides a"
    and acarr: "a ∈ carrier G" and bcarr: "b ∈ carrier G" and ccarr: "c ∈ carrier G"
  shows "a ∼ somegcd G b c"
  apply (simp add: somegcd_def)
  apply (rule someI2_ex)
   apply (rule exI[of _ a], simp add: isgcd_def)
   apply (simp add: assms)
  apply (simp add: isgcd_def assms, clarify)
  apply (insert assms, blast intro: associatedI)
  done

lemma (in gcd_condition_monoid) gcdI2:
  assumes "a gcdof b c" and "a ∈ carrier G" and "b ∈ carrier G" and "c ∈ carrier G"
  shows "a ∼ somegcd G b c"
  using assms unfolding isgcd_def by (blast intro: gcdI)

lemma (in gcd_condition_monoid) SomeGcd_ex:
  assumes "finite A"  "A ⊆ carrier G"  "A ≠ {}"
  shows "∃x∈ carrier G. x = SomeGcd G A"
proof -
  interpret weak_lower_semilattice "division_rel G"
    by simp
  show ?thesis
    apply (simp add: SomeGcd_def)
    apply (rule finite_inf_closed[simplified], fact+)
    done
qed

lemma (in gcd_condition_monoid) gcd_assoc:
  assumes carr: "a ∈ carrier G"  "b ∈ carrier G"  "c ∈ carrier G"
  shows "somegcd G (somegcd G a b) c ∼ somegcd G a (somegcd G b c)"
proof -
  interpret weak_lower_semilattice "division_rel G"
    by simp
  show ?thesis
    apply (subst (2 3) somegcd_meet, (simp add: carr)+)
    apply (simp add: somegcd_meet carr)
    apply (rule weak_meet_assoc[simplified], fact+)
    done
qed

lemma (in gcd_condition_monoid) gcd_mult:
  assumes acarr: "a ∈ carrier G" and bcarr: "b ∈ carrier G" and ccarr: "c ∈ carrier G"
  shows "c ⊗ somegcd G a b ∼ somegcd G (c ⊗ a) (c ⊗ b)"
proof - (* following Jacobson, Basic Algebra, p.140 *)
  let ?d = "somegcd G a b"
  let ?e = "somegcd G (c ⊗ a) (c ⊗ b)"
  note carr[simp] = acarr bcarr ccarr
  have dcarr: "?d ∈ carrier G" by simp
  have ecarr: "?e ∈ carrier G" by simp
  note carr = carr dcarr ecarr

  have "?d divides a" by (simp add: gcd_divides_l)
  then have cd'ca: "c ⊗ ?d divides (c ⊗ a)" by (simp add: divides_mult_lI)

  have "?d divides b" by (simp add: gcd_divides_r)
  then have cd'cb: "c ⊗ ?d divides (c ⊗ b)" by (simp add: divides_mult_lI)

  from cd'ca cd'cb have cd'e: "c ⊗ ?d divides ?e"
    by (rule gcd_divides) simp_all
  then obtain u where ucarr[simp]: "u ∈ carrier G" and e_cdu: "?e = c ⊗ ?d ⊗ u"
    by blast

  note carr = carr ucarr

  have "?e divides c ⊗ a" by (rule gcd_divides_l) simp_all
  then obtain x where xcarr: "x ∈ carrier G" and ca_ex: "c ⊗ a = ?e ⊗ x"
    by blast
  with e_cdu have ca_cdux: "c ⊗ a = c ⊗ ?d ⊗ u ⊗ x"
    by simp

  from ca_cdux xcarr have "c ⊗ a = c ⊗ (?d ⊗ u ⊗ x)"
    by (simp add: m_assoc)
  then have "a = ?d ⊗ u ⊗ x"
    by (rule l_cancel[of c a]) (simp add: xcarr)+
  then have du'a: "?d ⊗ u divides a"
    by (rule dividesI[OF xcarr])

  have "?e divides c ⊗ b" by (intro gcd_divides_r) simp_all
  then obtain x where xcarr: "x ∈ carrier G" and cb_ex: "c ⊗ b = ?e ⊗ x"
    by blast
  with e_cdu have cb_cdux: "c ⊗ b = c ⊗ ?d ⊗ u ⊗ x"
    by simp

  from cb_cdux xcarr have "c ⊗ b = c ⊗ (?d ⊗ u ⊗ x)"
    by (simp add: m_assoc)
  with xcarr have "b = ?d ⊗ u ⊗ x"
    by (intro l_cancel[of c b]) simp_all
  then have du'b: "?d ⊗ u divides b"
    by (intro dividesI[OF xcarr])

  from du'a du'b carr have du'd: "?d ⊗ u divides ?d"
    by (intro gcd_divides) simp_all
  then have uunit: "u ∈ Units G"
  proof (elim dividesE)
    fix v
    assume vcarr[simp]: "v ∈ carrier G"
    assume d: "?d = ?d ⊗ u ⊗ v"
    have "?d ⊗ 𝟭 = ?d ⊗ u ⊗ v" by simp fact
    also have "?d ⊗ u ⊗ v = ?d ⊗ (u ⊗ v)" by (simp add: m_assoc)
    finally have "?d ⊗ 𝟭 = ?d ⊗ (u ⊗ v)" .
    then have i2: "𝟭 = u ⊗ v" by (rule l_cancel) simp_all
    then have i1: "𝟭 = v ⊗ u" by (simp add: m_comm)
    from vcarr i1[symmetric] i2[symmetric] show "u ∈ Units G"
      by (auto simp: Units_def)
  qed

  from e_cdu uunit have "somegcd G (c ⊗ a) (c ⊗ b) ∼ c ⊗ somegcd G a b"
    by (intro associatedI2[of u]) simp_all
  from this[symmetric] show "c ⊗ somegcd G a b ∼ somegcd G (c ⊗ a) (c ⊗ b)"
    by simp
qed

lemma (in monoid) assoc_subst:
  assumes ab: "a ∼ b"
    and cP: "∀a b. a ∈ carrier G ∧ b ∈ carrier G ∧ a ∼ b
      ⟶ f a ∈ carrier G ∧ f b ∈ carrier G ∧ f a ∼ f b"
    and carr: "a ∈ carrier G"  "b ∈ carrier G"
  shows "f a ∼ f b"
  using assms by auto

lemma (in gcd_condition_monoid) relprime_mult:
  assumes abrelprime: "somegcd G a b ∼ 𝟭"
    and acrelprime: "somegcd G a c ∼ 𝟭"
    and carr[simp]: "a ∈ carrier G"  "b ∈ carrier G"  "c ∈ carrier G"
  shows "somegcd G a (b ⊗ c) ∼ 𝟭"
proof -
  have "c = c ⊗ 𝟭" by simp
  also from abrelprime[symmetric]
  have "… ∼ c ⊗ somegcd G a b"
    by (rule assoc_subst) (simp add: mult_cong_r)+
  also have "… ∼ somegcd G (c ⊗ a) (c ⊗ b)"
    by (rule gcd_mult) fact+
  finally have c: "c ∼ somegcd G (c ⊗ a) (c ⊗ b)"
    by simp

  from carr have a: "a ∼ somegcd G a (c ⊗ a)"
    by (fast intro: gcdI divides_prod_l)

  have "somegcd G a (b ⊗ c) ∼ somegcd G a (c ⊗ b)"
    by (simp add: m_comm)
  also from a have "… ∼ somegcd G (somegcd G a (c ⊗ a)) (c ⊗ b)"
    by (rule assoc_subst) (simp add: gcd_cong_l)+
  also from gcd_assoc have "… ∼ somegcd G a (somegcd G (c ⊗ a) (c ⊗ b))"
    by (rule assoc_subst) simp+
  also from c[symmetric] have "… ∼ somegcd G a c"
    by (rule assoc_subst) (simp add: gcd_cong_r)+
  also note acrelprime
  finally show "somegcd G a (b ⊗ c) ∼ 𝟭"
    by simp
qed

lemma (in gcd_condition_monoid) primeness_condition: "primeness_condition_monoid G"
  apply unfold_locales
  apply (rule primeI)
   apply (elim irreducibleE, assumption)
proof -
  fix p a b
  assume pcarr: "p ∈ carrier G" and acarr: "a ∈ carrier G" and bcarr: "b ∈ carrier G"
    and pirr: "irreducible G p"
    and pdvdab: "p divides a ⊗ b"
  from pirr have pnunit: "p ∉ Units G"
    and r[rule_format]: "∀b. b ∈ carrier G ∧ properfactor G b p ⟶ b ∈ Units G"
    by (fast elim: irreducibleE)+

  show "p divides a ∨ p divides b"
  proof (rule ccontr, clarsimp)
    assume npdvda: "¬ p divides a"
    with pcarr acarr have "𝟭 ∼ somegcd G p a"
      apply (intro gcdI, simp, simp, simp)
           apply (fast intro: unit_divides)
          apply (fast intro: unit_divides)
         apply (clarsimp simp add: Unit_eq_dividesone[symmetric])
         apply (rule r, rule, assumption)
         apply (rule properfactorI, assumption)
    proof
      fix y
      assume ycarr: "y ∈ carrier G"
      assume "p divides y"
      also assume "y divides a"
      finally have "p divides a"
        by (simp add: pcarr ycarr acarr)
      with npdvda show False ..
    qed simp_all
    with pcarr acarr have pa: "somegcd G p a ∼ 𝟭"
      by (fast intro: associated_sym[of "𝟭"] gcd_closed)

    assume npdvdb: "¬ p divides b"
    with pcarr bcarr have "𝟭 ∼ somegcd G p b"
      apply (intro gcdI, simp, simp, simp)
           apply (fast intro: unit_divides)
          apply (fast intro: unit_divides)
         apply (clarsimp simp add: Unit_eq_dividesone[symmetric])
         apply (rule r, rule, assumption)
         apply (rule properfactorI, assumption)
    proof
      fix y
      assume ycarr: "y ∈ carrier G"
      assume "p divides y"
      also assume "y divides b"
      finally have "p divides b" by (simp add: pcarr ycarr bcarr)
      with npdvdb
      show "False" ..
    qed simp_all
    with pcarr bcarr have pb: "somegcd G p b ∼ 𝟭"
      by (fast intro: associated_sym[of "𝟭"] gcd_closed)

    from pcarr acarr bcarr pdvdab have "p gcdof p (a ⊗ b)"
      by (fast intro: isgcd_divides_l)
    with pcarr acarr bcarr have "p ∼ somegcd G p (a ⊗ b)"
      by (fast intro: gcdI2)
    also from pa pb pcarr acarr bcarr have "somegcd G p (a ⊗ b) ∼ 𝟭"
      by (rule relprime_mult)
    finally have "p ∼ 𝟭"
      by (simp add: pcarr acarr bcarr)
    with pcarr have "p ∈ Units G"
      by (fast intro: assoc_unit_l)
    with pnunit show False ..
  qed
qed

sublocale gcd_condition_monoid  primeness_condition_monoid
  by (rule primeness_condition)


subsubsection ‹Divisor chain condition›

lemma (in divisor_chain_condition_monoid) wfactors_exist:
  assumes acarr: "a ∈ carrier G"
  shows "∃as. set as ⊆ carrier G ∧ wfactors G as a"
proof -
  have r[rule_format]: "a ∈ carrier G ⟶ (∃as. set as ⊆ carrier G ∧ wfactors G as a)"
  proof (rule wf_induct[OF division_wellfounded])
    fix x
    assume ih: "∀y. (y, x) ∈ {(x, y). x ∈ carrier G ∧ y ∈ carrier G ∧ properfactor G x y}
                    ⟶ y ∈ carrier G ⟶ (∃as. set as ⊆ carrier G ∧ wfactors G as y)"

    show "x ∈ carrier G ⟶ (∃as. set as ⊆ carrier G ∧ wfactors G as x)"
      apply clarify
      apply (cases "x ∈ Units G")
       apply (rule exI[of _ "[]"], simp)
      apply (cases "irreducible G x")
       apply (rule exI[of _ "[x]"], simp add: wfactors_def)
    proof -
      assume xcarr: "x ∈ carrier G"
        and xnunit: "x ∉ Units G"
        and xnirr: "¬ irreducible G x"
      then have "∃y. y ∈ carrier G ∧ properfactor G y x ∧ y ∉ Units G"
        apply -
        apply (rule ccontr)
        apply simp
        apply (subgoal_tac "irreducible G x", simp)
        apply (rule irreducibleI, simp, simp)
        done
      then obtain y where ycarr: "y ∈ carrier G" and ynunit: "y ∉ Units G"
        and pfyx: "properfactor G y x"
        by blast

      have ih': "⋀y. ⟦y ∈ carrier G; properfactor G y x⟧
          ⟹ ∃as. set as ⊆ carrier G ∧ wfactors G as y"
        by (rule ih[rule_format, simplified]) (simp add: xcarr)+

      from ih' [OF ycarr pfyx]
      obtain ys where yscarr: "set ys ⊆ carrier G" and yfs: "wfactors G ys y"
        by blast

      from pfyx have "y divides x" and nyx: "¬ y ∼ x"
        by (fast elim: properfactorE2)+
      then obtain z where zcarr: "z ∈ carrier G" and x: "x = y ⊗ z"
        by blast

      from zcarr ycarr have "properfactor G z x"
        apply (subst x)
        apply (intro properfactorI3[of _ _ y])
            apply (simp add: m_comm)
           apply (simp add: ynunit)+
        done
      from ih' [OF zcarr this]
      obtain zs where zscarr: "set zs ⊆ carrier G" and zfs: "wfactors G zs z"
        by blast
      from yscarr zscarr have xscarr: "set (ys@zs) ⊆ carrier G"
        by simp
      from yfs zfs ycarr zcarr yscarr zscarr have "wfactors G (ys@zs) (y⊗z)"
        by (rule wfactors_mult)
      then have "wfactors G (ys@zs) x"
        by (simp add: x)
      with xscarr show "∃xs. set xs ⊆ carrier G ∧ wfactors G xs x"
        by fast
    qed
  qed
  from acarr show ?thesis by (rule r)
qed


subsubsection ‹Primeness condition›

lemma (in comm_monoid_cancel) multlist_prime_pos:
  assumes carr: "a ∈ carrier G"  "set as ⊆ carrier G"
    and aprime: "prime G a"
    and "a divides (foldr (op ⊗) as 𝟭)"
  shows "∃i<length as. a divides (as!i)"
proof -
  have r[rule_format]: "set as ⊆ carrier G ∧ a divides (foldr (op ⊗) as 𝟭)
    ⟶ (∃i. i < length as ∧ a divides (as!i))"
    apply (induct as)
     apply clarsimp defer 1
     apply clarsimp defer 1
  proof -
    assume "a divides 𝟭"
    with carr have "a ∈ Units G"
      by (fast intro: divides_unit[of a 𝟭])
    with aprime show False
      by (elim primeE, simp)
  next
    fix aa as
    assume ih[rule_format]: "a divides foldr op ⊗ as 𝟭 ⟶ (∃i<length as. a divides as ! i)"
      and carr': "aa ∈ carrier G"  "set as ⊆ carrier G"
      and "a divides aa ⊗ foldr op ⊗ as 𝟭"
    with carr aprime have "a divides aa ∨ a divides foldr op ⊗ as 𝟭"
      by (intro prime_divides) simp+
    then show "∃i<Suc (length as). a divides (aa # as) ! i"
    proof
      assume "a divides aa"
      then have p1: "a divides (aa#as)!0" by simp
      have "0 < Suc (length as)" by simp
      with p1 show ?thesis by fast
    next
      assume "a divides foldr op ⊗ as 𝟭"
      from ih [OF this] obtain i where "a divides as ! i" and len: "i < length as" by auto
      then have p1: "a divides (aa#as) ! (Suc i)" by simp
      from len have "Suc i < Suc (length as)" by simp
      with p1 show ?thesis by force
   qed
  qed
  from assms show ?thesis
    by (intro r) auto
qed

lemma (in primeness_condition_monoid) wfactors_unique__hlp_induct:
  "∀a as'. a ∈ carrier G ∧ set as ⊆ carrier G ∧ set as' ⊆ carrier G ∧
           wfactors G as a ∧ wfactors G as' a ⟶ essentially_equal G as as'"
proof (induct as)
  case Nil
  show ?case
  proof auto
    fix a as'
    assume a: "a ∈ carrier G"
    assume "wfactors G [] a"
    then obtain "𝟭 ∼ a" by (auto elim: wfactorsE)
    with a have "a ∈ Units G" by (auto intro: assoc_unit_r)
    moreover assume "wfactors G as' a"
    moreover assume "set as' ⊆ carrier G"
    ultimately have "as' = []" by (rule unit_wfactors_empty)
    then show "essentially_equal G [] as'" by simp
  qed
next
  case (Cons ah as)
  then show ?case
  proof clarsimp
    fix a as'
    assume ih [rule_format]:
      "∀a as'. a ∈ carrier G ∧ set as' ⊆ carrier G ∧ wfactors G as a ∧
        wfactors G as' a ⟶ essentially_equal G as as'"
      and acarr: "a ∈ carrier G" and ahcarr: "ah ∈ carrier G"
      and ascarr: "set as ⊆ carrier G" and as'carr: "set as' ⊆ carrier G"
      and afs: "wfactors G (ah # as) a"
      and afs': "wfactors G as' a"
    then have ahdvda: "ah divides a"
      by (intro wfactors_dividesI[of "ah#as" "a"]) simp_all
    then obtain a' where a'carr: "a' ∈ carrier G" and a: "a = ah ⊗ a'"
      by blast
    have a'fs: "wfactors G as a'"
      apply (rule wfactorsE[OF afs], rule wfactorsI, simp)
      apply (simp add: a)
      apply (insert ascarr a'carr)
      apply (intro assoc_l_cancel[of ah _ a'] multlist_closed ahcarr, assumption+)
      done
    from afs have ahirr: "irreducible G ah"
      by (elim wfactorsE) simp
    with ascarr have ahprime: "prime G ah"
      by (intro irreducible_prime ahcarr)

    note carr [simp] = acarr ahcarr ascarr as'carr a'carr

    note ahdvda
    also from afs' have "a divides (foldr (op ⊗) as' 𝟭)"
      by (elim wfactorsE associatedE, simp)
    finally have "ah divides (foldr (op ⊗) as' 𝟭)"
      by simp
    with ahprime have "∃i<length as'. ah divides as'!i"
      by (intro multlist_prime_pos) simp_all
    then obtain i where len: "i<length as'" and ahdvd: "ah divides as'!i"
      by blast
    from afs' carr have irrasi: "irreducible G (as'!i)"
      by (fast intro: nth_mem[OF len] elim: wfactorsE)
    from len carr have asicarr[simp]: "as'!i ∈ carrier G"
      unfolding set_conv_nth by force
    note carr = carr asicarr

    from ahdvd obtain x where "x ∈ carrier G" and asi: "as'!i = ah ⊗ x"
      by blast
    with carr irrasi[simplified asi] have asiah: "as'!i ∼ ah"
      apply -
      apply (elim irreducible_prodE[of "ah" "x"], assumption+)
       apply (rule associatedI2[of x], assumption+)
      apply (rule irreducibleE[OF ahirr], simp)
      done

    note setparts = set_take_subset[of i as'] set_drop_subset[of "Suc i" as']
    note partscarr [simp] = setparts[THEN subset_trans[OF _ as'carr]]
    note carr = carr partscarr

    have "∃aa_1. aa_1 ∈ carrier G ∧ wfactors G (take i as') aa_1"
      apply (intro wfactors_prod_exists)
      using setparts afs'
       apply (fast elim: wfactorsE)
      apply simp
      done
    then obtain aa_1 where aa1carr: "aa_1 ∈ carrier G" and aa1fs: "wfactors G (take i as') aa_1"
      by auto

    have "∃aa_2. aa_2 ∈ carrier G ∧ wfactors G (drop (Suc i) as') aa_2"
      apply (intro wfactors_prod_exists)
      using setparts afs'
       apply (fast elim: wfactorsE)
      apply simp
      done
    then obtain aa_2 where aa2carr: "aa_2 ∈ carrier G"
      and aa2fs: "wfactors G (drop (Suc i) as') aa_2"
      by auto

    note carr = carr aa1carr[simp] aa2carr[simp]

    from aa1fs aa2fs
    have v1: "wfactors G (take i as' @ drop (Suc i) as') (aa_1 ⊗ aa_2)"
      by (intro wfactors_mult, simp+)
    then have v1': "wfactors G (as'!i # take i as' @ drop (Suc i) as') (as'!i ⊗ (aa_1 ⊗ aa_2))"
      apply (intro wfactors_mult_single)
      using setparts afs'
          apply (fast intro: nth_mem[OF len] elim: wfactorsE)
         apply simp_all
      done

    from aa2carr carr aa1fs aa2fs have "wfactors G (as'!i # drop (Suc i) as') (as'!i ⊗ aa_2)"
      by (metis irrasi wfactors_mult_single)
    with len carr aa1carr aa2carr aa1fs
    have v2: "wfactors G (take i as' @ as'!i # drop (Suc i) as') (aa_1 ⊗ (as'!i ⊗ aa_2))"
      apply (intro wfactors_mult)
           apply fast
          apply (simp, (fast intro: nth_mem[OF len])?)+
      done

    from len have as': "as' = (take i as' @ as'!i # drop (Suc i) as')"
      by (simp add: Cons_nth_drop_Suc)
    with carr have eer: "essentially_equal G (take i as' @ as'!i # drop (Suc i) as') as'"
      by simp
    with v2 afs' carr aa1carr aa2carr nth_mem[OF len] have "aa_1 ⊗ (as'!i ⊗ aa_2) ∼ a"
      by (metis as' ee_wfactorsD m_closed)
    then have t1: "as'!i ⊗ (aa_1 ⊗ aa_2) ∼ a"
      by (metis aa1carr aa2carr asicarr m_lcomm)
    from carr asiah have "ah ⊗ (aa_1 ⊗ aa_2) ∼ as'!i ⊗ (aa_1 ⊗ aa_2)"
      by (metis associated_sym m_closed mult_cong_l)
    also note t1
    finally have "ah ⊗ (aa_1 ⊗ aa_2) ∼ a" by simp

    with carr aa1carr aa2carr a'carr nth_mem[OF len] have a': "aa_1 ⊗ aa_2 ∼ a'"
      by (simp add: a, fast intro: assoc_l_cancel[of ah _ a'])

    note v1
    also note a'
    finally have "wfactors G (take i as' @ drop (Suc i) as') a'"
      by simp

    from a'fs this carr have "essentially_equal G as (take i as' @ drop (Suc i) as')"
      by (intro ih[of a']) simp
    then have ee1: "essentially_equal G (ah # as) (ah # take i as' @ drop (Suc i) as')"
      by (elim essentially_equalE) (fastforce intro: essentially_equalI)

    from carr have ee2: "essentially_equal G (ah # take i as' @ drop (Suc i) as')
      (as' ! i # take i as' @ drop (Suc i) as')"
    proof (intro essentially_equalI)
      show "ah # take i as' @ drop (Suc i) as' <~~> ah # take i as' @ drop (Suc i) as'"
        by simp
    next
      show "ah # take i as' @ drop (Suc i) as' [∼] as' ! i # take i as' @ drop (Suc i) as'"
        by (simp add: list_all2_append) (simp add: asiah[symmetric])
    qed

    note ee1
    also note ee2
    also have "essentially_equal G (as' ! i # take i as' @ drop (Suc i) as')
      (take i as' @ as' ! i # drop (Suc i) as')"
      apply (intro essentially_equalI)
       apply (subgoal_tac "as' ! i # take i as' @ drop (Suc i) as' <~~>
          take i as' @ as' ! i # drop (Suc i) as'")
        apply simp
       apply (rule perm_append_Cons)
      apply simp
      done
    finally have "essentially_equal G (ah # as) (take i as' @ as' ! i # drop (Suc i) as')"
      by simp
    then show "essentially_equal G (ah # as) as'"
      by (subst as')
  qed
qed

lemma (in primeness_condition_monoid) wfactors_unique:
  assumes "wfactors G as a"  "wfactors G as' a"
    and "a ∈ carrier G"  "set as ⊆ carrier G"  "set as' ⊆ carrier G"
  shows "essentially_equal G as as'"
  by (rule wfactors_unique__hlp_induct[rule_format, of a]) (simp add: assms)


subsubsection ‹Application to factorial monoids›

text ‹Number of factors for wellfoundedness›

definition factorcount :: "_ ⇒ 'a ⇒ nat"
  where "factorcount G a =
    (THE c. ∀as. set as ⊆ carrier G ∧ wfactors G as a ⟶ c = length as)"

lemma (in monoid) ee_length:
  assumes ee: "essentially_equal G as bs"
  shows "length as = length bs"
  by (rule essentially_equalE[OF ee]) (metis list_all2_conv_all_nth perm_length)

lemma (in factorial_monoid) factorcount_exists:
  assumes carr[simp]: "a ∈ carrier G"
  shows "∃c. ∀as. set as ⊆ carrier G ∧ wfactors G as a ⟶ c = length as"
proof -
  have "∃as. set as ⊆ carrier G ∧ wfactors G as a"
    by (intro wfactors_exist) simp
  then obtain as where ascarr[simp]: "set as ⊆ carrier G" and afs: "wfactors G as a"
    by (auto simp del: carr)
  have "∀as'. set as' ⊆ carrier G ∧ wfactors G as' a ⟶ length as = length as'"
    by (metis afs ascarr assms ee_length wfactors_unique)
  then show "∃c. ∀as'. set as' ⊆ carrier G ∧ wfactors G as' a ⟶ c = length as'" ..
qed

lemma (in factorial_monoid) factorcount_unique:
  assumes afs: "wfactors G as a"
    and acarr[simp]: "a ∈ carrier G" and ascarr[simp]: "set as ⊆ carrier G"
  shows "factorcount G a = length as"
proof -
  have "∃ac. ∀as. set as ⊆ carrier G ∧ wfactors G as a ⟶ ac = length as"
    by (rule factorcount_exists) simp
  then obtain ac where alen: "∀as. set as ⊆ carrier G ∧ wfactors G as a ⟶ ac = length as"
    by auto
  have ac: "ac = factorcount G a"
    apply (simp add: factorcount_def)
    apply (rule theI2)
      apply (rule alen)
     apply (metis afs alen ascarr)+
    done
  from ascarr afs have "ac = length as"
    by (iprover intro: alen[rule_format])
  with ac show ?thesis
    by simp
qed

lemma (in factorial_monoid) divides_fcount:
  assumes dvd: "a divides b"
    and acarr: "a ∈ carrier G"
    and bcarr:"b ∈ carrier G"
  shows "factorcount G a ≤ factorcount G b"
proof (rule dividesE[OF dvd])
  fix c
  from assms have "∃as. set as ⊆ carrier G ∧ wfactors G as a"
    by blast
  then obtain as where ascarr: "set as ⊆ carrier G" and afs: "wfactors G as a"
    by blast
  with acarr have fca: "factorcount G a = length as"
    by (intro factorcount_unique)

  assume ccarr: "c ∈ carrier G"
  then have "∃cs. set cs ⊆ carrier G ∧ wfactors G cs c"
    by blast
  then obtain cs where cscarr: "set cs ⊆ carrier G" and cfs: "wfactors G cs c"
    by blast

  note [simp] = acarr bcarr ccarr ascarr cscarr

  assume b: "b = a ⊗ c"
  from afs cfs have "wfactors G (as@cs) (a ⊗ c)"
    by (intro wfactors_mult) simp_all
  with b have "wfactors G (as@cs) b"
    by simp
  then have "factorcount G b = length (as@cs)"
    by (intro factorcount_unique) simp_all
  then have "factorcount G b = length as + length cs"
    by simp
  with fca show ?thesis
    by simp
qed

lemma (in factorial_monoid) associated_fcount:
  assumes acarr: "a ∈ carrier G"
    and bcarr: "b ∈ carrier G"
    and asc: "a ∼ b"
  shows "factorcount G a = factorcount G b"
  apply (rule associatedE[OF asc])
  apply (drule divides_fcount[OF _ acarr bcarr])
  apply (drule divides_fcount[OF _ bcarr acarr])
  apply simp
  done

lemma (in factorial_monoid) properfactor_fcount:
  assumes acarr: "a ∈ carrier G" and bcarr:"b ∈ carrier G"
    and pf: "properfactor G a b"
  shows "factorcount G a < factorcount G b"
proof (rule properfactorE[OF pf], elim dividesE)
  fix c
  from assms have "∃as. set as ⊆ carrier G ∧ wfactors G as a"
    by blast
  then obtain as where ascarr: "set as ⊆ carrier G" and afs: "wfactors G as a"
    by blast
  with acarr have fca: "factorcount G a = length as"
    by (intro factorcount_unique)

  assume ccarr: "c ∈ carrier G"
  then have "∃cs. set cs ⊆ carrier G ∧ wfactors G cs c"
    by blast
  then obtain cs where cscarr: "set cs ⊆ carrier G" and cfs: "wfactors G cs c"
    by blast

  assume b: "b = a ⊗ c"

  have "wfactors G (as@cs) (a ⊗ c)"
    by (rule wfactors_mult) fact+
  with b have "wfactors G (as@cs) b"
    by simp
  with ascarr cscarr bcarr have "factorcount G b = length (as@cs)"
    by (simp add: factorcount_unique)
  then have fcb: "factorcount G b = length as + length cs"
    by simp

  assume nbdvda: "¬ b divides a"
  have "c ∉ Units G"
  proof
    assume cunit:"c ∈ Units G"
    have "b ⊗ inv c = a ⊗ c ⊗ inv c"
      by (simp add: b)
    also from ccarr acarr cunit have "… = a ⊗ (c ⊗ inv c)"
      by (fast intro: m_assoc)
    also from ccarr cunit have "… = a ⊗ 𝟭" by simp
    also from acarr have "… = a" by simp
    finally have "a = b ⊗ inv c" by simp
    with ccarr cunit have "b divides a"
      by (fast intro: dividesI[of "inv c"])
    with nbdvda show False by simp
  qed
  with cfs have "length cs > 0"
    apply -
    apply (rule ccontr, simp)
    apply (metis Units_one_closed ccarr cscarr l_one one_closed properfactorI3 properfactor_fmset unit_wfactors)
    done
  with fca fcb show ?thesis
    by simp
qed

sublocale factorial_monoid  divisor_chain_condition_monoid
  apply unfold_locales
  apply (rule wfUNIVI)
  apply (rule measure_induct[of "factorcount G"])
  apply simp
  apply (metis properfactor_fcount)
  done

sublocale factorial_monoid  primeness_condition_monoid
  by standard (rule irreducible_prime)


lemma (in factorial_monoid) primeness_condition: "primeness_condition_monoid G" ..

lemma (in factorial_monoid) gcd_condition [simp]: "gcd_condition_monoid G"
  by standard (rule gcdof_exists)

sublocale factorial_monoid  gcd_condition_monoid
  by standard (rule gcdof_exists)

lemma (in factorial_monoid) division_weak_lattice [simp]: "weak_lattice (division_rel G)"
proof -
  interpret weak_lower_semilattice "division_rel G"
    by simp
  show "weak_lattice (division_rel G)"
  proof (unfold_locales, simp_all)
    fix x y
    assume carr: "x ∈ carrier G"  "y ∈ carrier G"
    from lcmof_exists [OF this] obtain z where zcarr: "z ∈ carrier G" and isgcd: "z lcmof x y"
      by blast
    with carr have "least (division_rel G) z (Upper (division_rel G) {x, y})"
      by (simp add: lcmof_leastUpper[symmetric])
    then show "∃z. least (division_rel G) z (Upper (division_rel G) {x, y})"
      by blast
  qed
qed


subsection ‹Factoriality Theorems›

theorem factorial_condition_one: (* Jacobson theorem 2.21 *)
  "divisor_chain_condition_monoid G ∧ primeness_condition_monoid G ⟷ factorial_monoid G"
proof (rule iffI, clarify)
  assume dcc: "divisor_chain_condition_monoid G"
    and pc: "primeness_condition_monoid G"
  interpret divisor_chain_condition_monoid "G" by (rule dcc)
  interpret primeness_condition_monoid "G" by (rule pc)
  show "factorial_monoid G"
    by (fast intro: factorial_monoidI wfactors_exist wfactors_unique)
next
  assume "factorial_monoid G"
  then interpret factorial_monoid "G" .
  show "divisor_chain_condition_monoid G ∧ primeness_condition_monoid G"
    by rule unfold_locales
qed

theorem factorial_condition_two: (* Jacobson theorem 2.22 *)
  "divisor_chain_condition_monoid G ∧ gcd_condition_monoid G ⟷ factorial_monoid G"
proof (rule iffI, clarify)
  assume dcc: "divisor_chain_condition_monoid G"
    and gc: "gcd_condition_monoid G"
  interpret divisor_chain_condition_monoid "G" by (rule dcc)
  interpret gcd_condition_monoid "G" by (rule gc)
  show "factorial_monoid G"
    by (simp add: factorial_condition_one[symmetric], rule, unfold_locales)
next
  assume "factorial_monoid G"
  then interpret factorial_monoid "G" .
  show "divisor_chain_condition_monoid G ∧ gcd_condition_monoid G"
    by rule unfold_locales
qed

end