Theory Divisibility

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

section ‹Divisibility in monoids and rings›

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

section ‹Factorial Monoids›

subsection ‹Monoids with Cancellation Law›

locale monoid_cancel = monoid +
  assumes l_cancel: "c  a = c  b; a  carrier G; b  carrier G; c  carrier G  a = b"
    and r_cancel: "a  c = b  c; a  carrier G; b  carrier G; c  carrier G  a = b"

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

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

sublocale group  monoid_cancel
  by standard simp_all


locale comm_monoid_cancel = monoid_cancel + comm_monoid

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

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

sublocale comm_group  comm_monoid_cancel ..


subsection ‹Products of Units in Monoids›

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

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

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

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

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

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

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

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

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

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

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

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

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


subsection ‹Divisibility and Association›

subsubsection ‹Function definitions›

definition factor :: "[_, 'a, 'a]  bool" (infix dividesı› 65)
  where "a dividesGb  (ccarrier G. b = a Gc)"

definition associated :: "[_, 'a, 'a]  bool" (infix ı› 55)
  where "a Gb  a dividesGb  b dividesGa"

abbreviation "division_rel G  carrier = carrier G, eq = (∼G), le = (dividesG)"

definition properfactor :: "[_, 'a, 'a]  bool"
  where "properfactor G a b  a dividesGb  ¬(b dividesGa)"

definition irreducible :: "[_, 'a]  bool"
  where "irreducible G a  a  Units G  (bcarrier G. properfactor G b a  b  Units G)"

definition prime :: "[_, 'a]  bool"
  where "prime G p 
    p  Units G 
    (acarrier G. bcarrier G. p dividesG(a Gb)  p dividesGa  p dividesGb)"


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 "ccarrier G. b = a  c"
  using assms unfolding factor_def by fast

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

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

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

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

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

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

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

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

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

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

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

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


subsubsection ‹Association›

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

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

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

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

lemma (in monoid_cancel) associatedD2:
  assumes assoc: "a  b"
    and carr: "a  carrier G" "b  carrier G"
  shows "uUnits 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 "uUnits 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 "uUnits G. a = b  u"
    by (rule associatedD2)
  then obtain u where "u  Units G"  "a = b  u"
    by auto
  then show P by (elim e)
qed

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

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

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

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


subsubsection ‹Division and associativity›

lemmas divides_antisym = associatedI

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

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

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


subsubsection ‹Multiplication and associativity›

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

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

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

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


subsubsection ‹Units›

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

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

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

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

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

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

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


subsubsection ‹Proper factors›

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

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

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

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

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

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

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

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

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

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

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

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

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

lemma (in monoid) properfactor_cong_l [trans]:
  assumes x'x: "x'  x"
    and pf: "properfactor G x y"
    and carr: "x  carrier G"  "x'  carrier G"  "y  carrier G"
  shows "properfactor G x' y"
  using pf
  unfolding properfactor_lless
proof -
  interpret weak_partial_order "division_rel G" ..
  from x'x have "x' .=division_rel Gx" by simp
  also assume "x division_rel Gy"
  finally show "x' division_rel Gy" 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 Gy"
  also from yy'
  have "y .=division_rel Gy'" by simp
  finally show "x division_rel Gy'" by (simp add: carr)
qed

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

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

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

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

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

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


subsection ‹Irreducible Elements and Primes›

subsubsection ‹Irreducible elements›

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

lemma irreducibleE:
  fixes G (structure)
  assumes irr: "irreducible G a"
    and elim: "a  Units G; b. b  carrier G  properfactor G b a  b  Units G  P"
  shows "P"
  using assms unfolding irreducible_def by blast

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

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

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

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

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

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

lemma divides_irreducible_condition:
  assumes "irreducible G r" and "a  carrier G"
  shows "a dividesGr  a  Units G  a Gr"
  using assms unfolding irreducible_def properfactor_def associated_def
  by (cases "r dividesGa", auto)

subsubsection ‹Prime elements›

lemma primeI:
  fixes G (structure)
  assumes "p  Units G"
    and "a b. a  carrier G; b  carrier G; p divides (a  b)  p divides a  p divides b"
  shows "prime G p"
  using assms unfolding prime_def by blast

lemma primeE:
  fixes G (structure)
  assumes pprime: "prime G p"
    and e: "p  Units G; acarrier G. bcarrier G.
      p divides a  b  p divides a  p divides b  P"
  shows "P"
  using pprime unfolding prime_def by (blast dest: e)

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

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

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

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


subsection ‹Factorization and Factorial Monoids›

subsubsection ‹Function definitions›

definition factors :: "('a, _) monoid_scheme  'a list  'a  bool"
  where "factors G fs a  (x  (set fs). irreducible G x)  foldr (⊗G) fs 𝟭G= a"

definition wfactors ::"('a, _) monoid_scheme  'a list  'a  bool"
  where "wfactors G fs a  (x  (set fs). irreducible G x)  foldr (⊗G) fs 𝟭GGa"

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

definition essentially_equal :: "('a, _) monoid_scheme  'a list  'a list  bool"
  where "essentially_equal G fs1 fs2  (fs1'. fs1 <~~> fs1'  fs1' [∼]Gfs2)"


locale factorial_monoid = comm_monoid_cancel +
  assumes factors_exist: "a  carrier G; a  Units G  fs. set fs  carrier G  factors G fs a"
    and factors_unique:
      "factors G fs a; factors G fs' a; a  carrier G; a  Units G;
        set fs  carrier G; set fs'  carrier G  essentially_equal G fs fs'"


subsubsection ‹Comparing lists of elements›

text ‹Association on lists›

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

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

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

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


text ‹Permutations›

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

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

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

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

declare perm_sym [sym]

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

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

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


text ‹Essentially equal factorizations›

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

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

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

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

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


subsubsection ‹Properties of lists of elements›

text ‹Multiplication of factors in a list›

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

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

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

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

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


subsubsection ‹Factorization in irreducible elements›

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

lemma wfactorsE:
  fixes G (structure)
  assumes wf: "wfactors G fs a"
    and e: "fset fs. irreducible G f; foldr (⊗) fs 𝟭  a  P"
  shows "P"
  using wf unfolding wfactors_def by (fast dest: e)

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

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

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

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

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

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

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

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

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

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

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


text ‹Comparing wfactors›

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

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

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

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

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


subsubsection ‹Essentially equal factorizations›

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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


subsubsection ‹Factorial monoids and wfactors›

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

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

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

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


subsection ‹Factorizations as Multisets›

text ‹Gives useful operations like intersection›

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

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

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


text ‹Helper lemmas›

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

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

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

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

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


subsubsection ‹Comparing multisets›

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

lemma (in comm_monoid_cancel) eqc_listassoc_cong:
  assumes "as [∼] bs" and "set as  carrier G" and "set bs  carrier G"
  shows "map (assocs G) as = map (assocs G) bs"
  using assms
proof (induction as arbitrary: bs)
  case Nil
  then show ?case by simp
next
  case (Cons a as)
  then show ?case
  proof (clarsimp simp add: Cons_eq_map_conv list_all2_Cons1)
    fix z zs 
    assume zzs: "a  carrier G" "set as  carrier G" "bs = z # zs" "a  z"
      "as [∼] zs" "z  carrier G" "set zs  carrier G"
    then show "assocs G a = assocs G z"
      apply (simp add: eq_closure_of_def elem_def)
      using a  carrier G z  carrier G a  z associated_sym associated_trans by blast+
  qed
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
  thm essentially_equal_def
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 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 "mset (map (assocs G) bs) = mset (map (assocs G) as)"
    by (simp add: fmset_def)
  then obtain p where p permutes {..<length (map (assocs G) as)}
    permute_list p (map (assocs G) as) = map (assocs G) bs
    by (rule mset_eq_permutation)
  then have p permutes {..<length as}
    map (assocs G) (permute_list p as) = map (assocs G) bs
    by (simp_all add: permute_list_map) 
  moreover define as' where as' = permute_list p as
  ultimately have tp: "as <~~> as'" and tm: "map (assocs G) as' = map (assocs G) bs"
    by simp_all
  from tp show ?thesis
  proof (rule essentially_equalI)
    from tm tp ascarr have as'carr: "set as'  carrier G"
      using perm_closed by blast
    from tm as'carr[THEN subsetD] bscarr[THEN subsetD] show "as' [∼] bs"
      by (induct as' arbitrary: bs) (simp, fastforce dest: assocs_eqD[THEN associated_sym])
  qed
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
  proof (induction Cs')
    case (Cons a Cs')
    then obtain c cs where csP: "xset cs. P x" and mset: "mset (map (assocs G) cs) = mset Cs'"
            and cP: "P c" and a: "a = assocs G c"
      by force
    then have tP: "xset (c#cs). P x"
      by simp
    show ?case
      using tP mset a by fastforce
  qed auto
  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. (cset cs. c  carrier G  irreducible G c)  fmset G cs = Cs"
    by (intro mset_fmsetEx, rule elems)
  then obtain cs where p[rule_format]: "cset 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 "ab" "ab"]) 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"
proof (rule properfactorI)
  show "a divides b"
    using assms asubb fmsubset_divides by blast
  show "¬ b divides a"
    by (meson anb assms asubb factorial_monoid.divides_fmsubset factorial_monoid_axioms subset_mset.antisym)
qed

lemma (in factorial_monoid) properfactor_fmset:
  assumes "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"
  using assms
  by (meson divides_as_fmsubset properfactor_divides)

lemma (in factorial_monoid) properfactor_fmset_ne:
  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"
  using properfactorE [OF pf] assms divides_as_fmsubset by force

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)
  obtain as where ascarr: "set as  carrier G" and afs: "wfactors G as a"
    using wfactors_exist [OF acarr] by blast
  obtain bs where bscarr: "set bs  carrier G" and bfs: "wfactors G bs b"
    using wfactors_exist [OF bcarr] by blast
  obtain cs where cscarr: "set cs  carrier G" and cfs: "wfactors G cs c"
    using wfactors_exist [OF ccarr] by blast
  note carr[simp] = pcarr acarr bcarr ccarr ascarr bscarr cscarr
  from pirr cfs  abpc have "wfactors G (p # cs) (a  b)"
    by (simp add: wfactors_mult_single)
  moreover have  "wfactors G (as @ bs) (a  b)"
    by (rule wfactors_mult [OF afs bfs]) fact+
  ultimately 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 (metis mset (p # cs) = mset ds insert_iff list.set(2) perm_set_eq) 
  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"
    using afs bfs divides_cong_l pp' wfactors_dividesI
    by (meson acarr ascarr bcarr bscarr pcarr)
qed


― ‹A version using constfactors, more complicated›
lemma (in factorial_monoid) factors_irreducible_prime:
  assumes pirr: "irreducible G p" and pcarr: "p  carrier G"
  shows "prime G p"
proof (rule primeI)
  show "p  Units G"
    by (meson irreducibleE pirr)
  have irreduc: "b. b  carrier G; properfactor G b p  b  Units G"
    using pirr by (auto simp: irreducible_def)
  show "p divides a  p divides b" 
    if acarr: "a  carrier G" and bcarr: "b  carrier G" and pdvdab: "p divides (a  b)" for a b
  proof -
    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 True
      then have "p divides b"
        by (metis acarr associatedI2' associated_def bcarr divides_trans m_comm pcarr pdvdab) 
      then show ?thesis ..
    next
      case anunit: False
      show ?thesis
      proof (cases "b  Units G")
        case True 
        then have "p divides a"
          by (meson acarr bcarr divides_unit irreducible_prime pcarr pdvdab pirr prime_def)
        then show ?thesis ..
      next
        case bnunit: False
        then have cnunit: "c  Units G"
          by (metis abpc acarr anunit bcarr ccarr irreducible_prodE irreducible_prod_rI pcarr pirr)
        then have abnunit: "a  b  Units G"
          using acarr anunit bcarr unit_factor by blast
        obtain as where ascarr: "set as  carrier G" and afac: "factors G as a"
          using factors_exist [OF acarr anunit] by blast
        obtain bs where bscarr: "set bs  carrier G" and bfac: "factors G bs b"
          using factors_exist [OF bcarr bnunit] by blast
        obtain cs where cscarr: "set cs  carrier G" and cfac: "factors G cs c"
          using factors_exist [OF ccarr cnunit] by auto
        note [simp] = ascarr bscarr cscarr
        from pirr cfac abpc have abfac': "factors G (p # cs) (a  b)"
          by (simp add: factors_mult_single)
        from afac and bfac have "factors G (as @ bs) (a  b)"
          by (rule factors_mult) fact+
        with abfac' have "essentially_equal G (p # cs) (as @ bs)"
          using abnunit factors_unique by auto
        then obtain ds where "p # cs <~~> ds" and dsassoc: "ds [∼] (as @ bs)"
          by (fast elim: essentially_equalE)
        then have "p  set ds"
          by (metis list.set_intros(1) set_mset_mset)
        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"
          by (meson afac bfac divides_cong_l factors_dividesI pp' ascarr bscarr pcarr)
      qed
    qed
  qed
qed


subsection ‹Greatest Common Divisors and Lowest Common Multiples›

subsubsection ‹Definitions›

definition isgcd :: "[('a,_) monoid_scheme, 'a, 'a, 'a]  bool"
    ((‹notation=‹mixfix gcdof››_ gcdofı _ _) [81,81,81] 80)
  where "x gcdofGa b  x dividesGa  x dividesGb 
    (ycarrier G. (y dividesGa  y dividesGb  y dividesGx))"

definition islcm :: "[_, 'a, 'a, 'a]  bool"
    ((‹notation=‹mixfix lcmof››_ lcmofı _ _) [81,81,81] 80)
  where "x lcmofGa b  a dividesGx  b dividesGx 
    (ycarrier G. (a dividesGy  b dividesGy  x dividesGy))"

definition somegcd :: "('a,_) monoid_scheme  'a  'a  'a"
  where "somegcd G a b = (SOME x. x  carrier G  x gcdofGa b)"

definition somelcm :: "('a,_) monoid_scheme  'a  'a  'a"
  where "somelcm G a b = (SOME x. x  carrier G  x lcmofGa b)"

definition "SomeGcd G A = Lattice.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
    then show "c divides a" by (rule fmsubset_divides) fact+
  next
    from csmset have "fmset G cs ⊆# fmset G bs"
      by simp
    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"
      using subset_eq_diff_conv subset_mset.le_diff_conv2 by fastforce
    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
  proof (unfold_locales, simp_all)
    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 gcdof b c" "a'  carrier G" and carr': "a  carrier G"  "b  carrier G"  "c  carrier G"
  shows "a' gcdof b c"
proof -
  interpret weak_lower_semilattice "division_rel G" by simp
  have "is_glb (division_rel G) a' {b, c}"
    by (subst greatest_Lower_cong_l[of _ a]) (simp_all add: assms gcdof_greatestLower[symmetric])
  then have "a'  carrier G  a' gcdof b c"
    by (simp add: gcdof_greatestLower carr')
  then show ?thesis ..
qed

lemma (in gcd_condition_monoid) gcd_closed [simp]:
  assumes "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
  using  assms meet_closed by (simp add: somegcd_meet)
qed

lemma (in gcd_condition_monoid) gcd_isgcd:
  assumes "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 assms have "somegcd G a b  carrier G  (somegcd G a b) gcdof a b"
    by (simp add: gcdof_greatestLower inf_of_two_greatest meet_def somegcd_meet)
  then show "(somegcd G a b) gcdof a b"
    by simp
qed

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

lemma (in gcd_condition_monoid) gcd_divides_l:
  assumes "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 assms gcd_isgcd isgcd_def)
qed

lemma (in gcd_condition_monoid) gcd_divides_r:
  assumes "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 assms gcd_isgcd isgcd_def)
qed

lemma (in gcd_condition_monoid) gcd_divides:
  assumes "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 "x  x'" "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
    using somegcd_meet assms
    by (metis eq_object.select_convs(1) meet_cong_l partial_object.select_convs(1))
qed

lemma (in gcd_condition_monoid) gcd_cong_r:
  assumes "y  y'" "x  carrier G"  "y  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
    by (meson associated_def assms gcd_closed gcd_divides gcd_divides_l gcd_divides_r monoid.divides_trans monoid_axioms)
qed

lemma (in gcd_condition_monoid) gcdI:
  assumes dvd: "a divides b"  "a divides c"
    and others: "y. ycarrier 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"
proof -
  have "a. a  carrier G  a gcdof b c"
    by (simp add: bcarr ccarr gcdof_exists)
  moreover have "x. x  carrier G  x gcdof b c  a  x"
    by (simp add: acarr associated_def dvd isgcd_def others)
  ultimately show ?thesis
    unfolding somegcd_def by (blast intro: someI2_ex)
qed

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 (simp add: 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
    using finite_inf_closed by (simp add: assms SomeGcd_def)
qed

lemma (in gcd_condition_monoid) gcd_assoc:
  assumes "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
    unfolding associated_def
    by (meson assms divides_trans gcd_divides gcd_divides_l gcd_divides_r gcd_exists)
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"
proof -
  have *: "p divides a  p divides b"
    if pcarr[simp]: "p  carrier G" and acarr[simp]: "a  carrier G" and bcarr[simp]: "b  carrier G"
      and pirr: "irreducible G p" and pdvdab: "p divides a  b"
    for p a b
  proof -
    from pirr have pnunit: "p  Units G"
      and r: "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" and npdvdb: "¬ p divides b"
      have "𝟭  somegcd G p a"
      proof (intro gcdI unit_divides)
        show "y. y  carrier G; y divides p; y divides a  y  Units G"
          by (meson divides_trans npdvda pcarr properfactorI r)
      qed auto
      with pcarr acarr have pa: "somegcd G p a  𝟭"
        by (fast intro: associated_sym[of "𝟭"] gcd_closed)
      have "𝟭  somegcd G p b"
      proof (intro gcdI unit_divides)
        show "y. y  carrier G; y divides p; y divides b  y  Units G"
          by (meson divides_trans npdvdb pcarr properfactorI r)
      qed auto
      with pcarr bcarr have pb: "somegcd G p b  𝟭"
        by (fast intro: associated_sym[of "𝟭"] gcd_closed)
      have "p  somegcd G p (a  b)"
        using pdvdab by (simp add: gcdI2 isgcd_divides_l)
      also from pa pb pcarr acarr bcarr have "somegcd G p (a  b)  𝟭"
        by (rule relprime_mult)
      finally have "p  𝟭"
        by simp
      with pcarr have "p  Units G"
        by (fast intro: assoc_unit_l)
      with pnunit show False ..
    qed
  qed
  show ?thesis
    by unfold_locales (metis * primeI irreducibleE)
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: "a  carrier G  (as. set as  carrier G  wfactors G as a)"
    using division_wellfounded
  proof (induction rule: wf_induct_rule)
    case (less x)
    then have xcarr: "x  carrier G"
      by auto
    show ?case
    proof (cases "x  Units G")
      case True
      then show ?thesis
        by (metis bot.extremum list.set(1) unit_wfactors)
    next
      case xnunit: False
      show ?thesis
      proof (cases "irreducible G x")
        case True
        then show ?thesis
          by (rule_tac x="[x]" in exI) (simp add: wfactors_def xcarr)
      next
        case False
        then obtain y where ycarr: "y  carrier G" and ynunit: "y  Units G" and pfyx: "properfactor G y x"
          by (meson irreducible_def xnunit)
        obtain ys where yscarr: "set ys  carrier G" and yfs: "wfactors G ys y"
          using less ycarr pfyx by blast
        then obtain z where zcarr: "z  carrier G" and x: "x = y  z"
          by (meson dividesE pfyx properfactorE2)
        from zcarr ycarr have "properfactor G z x"
          using m_comm properfactorI3 x ynunit by blast
        with less zcarr 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
        have "wfactors G (ys@zs) (yz)"
          using xscarr ycarr yfs zcarr zfs by auto
        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
  qed
  from acarr show ?thesis by (rule r)
qed


subsubsection ‹Primeness condition›

lemma (in comm_monoid_cancel) multlist_prime_pos:
  assumes aprime: "prime G a" and carr: "a  carrier G" 
     and as: "set as  carrier G" "a divides (foldr (⊗) as 𝟭)"
   shows "i<length as. a divides (as!i)"
  using as
proof (induction as)
  case Nil
  then show ?case
    by simp (meson Units_one_closed aprime carr divides_unit primeE)
next
  case (Cons x as)
  then have "x  carrier G"  "set as  carrier G" and "a divides x  foldr (⊗) as 𝟭"
    by auto
  with carr aprime have "a divides x  a divides foldr (⊗) as 𝟭"
    by (intro prime_divides) simp+
  then show ?case
    using Cons.IH Cons.prems(1) by force
qed

proposition (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'"
  using assms
proof (induct as arbitrary: a as')
  case Nil
  then have "a  𝟭"
    by (simp add: perm_wfactorsD) 
  then have "as' = []"
    using Nil.prems assoc_unit_l unit_wfactors_empty by blast
  then show ?case
    by auto
next
  case (Cons ah as)
  then have ahdvda: "ah divides a"
    using wfactors_dividesI by auto
    then obtain a' where a'carr: "a'  carrier G" and a: "a = ah  a'"
      by blast
    have carr_ah: "ah  carrier G" "set as  carrier G"
      using Cons.prems by fastforce+
    have "ah  foldr (⊗) as 𝟭  a"
      by (rule wfactorsE[OF wfactors G (ah # as) a]) auto
    then have "foldr (⊗) as 𝟭  a'"
      by (metis Cons.prems(4) a a'carr assoc_l_cancel insert_subset list.set(2) monoid.multlist_closed monoid_axioms)
    then
    have a'fs: "wfactors G as a'"
      by (meson Cons.prems(1) set_subset_Cons subset_iff wfactorsE wfactorsI)
    then have ahirr: "irreducible G ah"
      by (meson Cons.prems(1) list.set_intros(1) wfactorsE)
    with Cons have ahprime: "prime G ah"
      by (simp add: irreducible_prime)
    note ahdvda
    also have "a divides (foldr (⊗) as' 𝟭)"
      by (meson Cons.prems(2) associatedE wfactorsE)
    finally have "ah divides (foldr (⊗) as' 𝟭)"
      using Cons.prems(4) by auto
    with ahprime have "i<length as'. ah divides as'!i"
      by (intro multlist_prime_pos) (use Cons.prems in auto)
    then obtain i where len: "i<length as'" and ahdvd: "ah divides as'!i"
      by blast
    then obtain x where "x  carrier G" and asi: "as'!i = ah  x"
      by blast
    have irrasi: "irreducible G (as'!i)"
      using nth_mem[OF len] wfactorsE
      by (metis Cons.prems(2))
    have asicarr[simp]: "as'!i  carrier G"
      using len set as'  carrier G nth_mem by blast
    have asiah: "as'!i  ah"
      by (metis ah  carrier G x  carrier G asi irrasi ahprime associatedI2 irreducible_prodE primeE)
    note setparts = set_take_subset[of i as'] set_drop_subset[of "Suc i" as']
    have "aa_1. aa_1  carrier G  wfactors G (take i as') aa_1"
      using Cons
      by (metis setparts(1) subset_trans in_set_takeD wfactorsE wfactors_prod_exists)
    then obtain aa_1 where aa1carr [simp]: "aa_1  carrier G" and aa1fs: "wfactors G (take i as') aa_1"
      by auto
    obtain aa_2 where aa2carr [simp]: "aa_2  carrier G"
      and aa2fs: "wfactors G (drop (Suc i) as') aa_2"
      by (metis Cons.prems(2) Cons.prems(5) subset_code(1) in_set_dropD wfactors_def wfactors_prod_exists)

    have set_drop: "set (drop (Suc i) as')  carrier G"
      using Cons.prems(5) setparts(2) by blast
    moreover have set_take: "set (take i as')  carrier G"
      using  Cons.prems(5) setparts by auto
    moreover have v1: "wfactors G (take i as' @ drop (Suc i) as') (aa_1  aa_2)"
      using aa1fs aa2fs set as'  carrier G by (force simp add: dest: in_set_takeD in_set_dropD)
    ultimately have v1': "wfactors G (as'!i # take i as' @ drop (Suc i) as') (as'!i  (aa_1  aa_2))"
      using irrasi wfactors_mult_single
        by (simp add: irrasi v1 wfactors_mult_single)      
    have "wfactors G (as'!i # drop (Suc i) as') (as'!i  aa_2)"
      by (simp add: aa2fs irrasi set_drop wfactors_mult_single)
    with len  aa1carr aa2carr aa1fs
    have v2: "wfactors G (take i as' @ as'!i # drop (Suc i) as') (aa_1  (as'!i  aa_2))"
      using wfactors_mult  by (simp add: set_take set_drop) 
    from len have as': "as' = (take i as' @ as'!i # drop (Suc i) as')"
      by (simp add: Cons_nth_drop_Suc)
    have eer: "essentially_equal G (take i as' @ as'!i # drop (Suc i) as') as'"
      using Cons.prems(5) as' by auto
    with v2 aa1carr aa2carr nth_mem[OF len] have "aa_1  (as'!i  aa_2)  a"
      using Cons.prems as' comm_monoid_cancel.ee_wfactorsD is_comm_monoid_cancel by fastforce
    then have t1: "as'!i  (aa_1  aa_2)  a"
      by (metis aa1carr aa2carr asicarr m_lcomm)
    from asiah have "ah  (aa_1  aa_2)  as'!i  (aa_1  aa_2)"
      by (simp add: ah  carrier G associated_sym mult_cong_l)
    also note t1
    finally have "ah  (aa_1  aa_2)  a"
      using Cons.prems(3) carr_ah aa1carr aa2carr by blast
    with aa1carr aa2carr a'carr nth_mem[OF len] have a': "aa_1  aa_2  a'"
      using a assoc_l_cancel carr_ah(1) by blast
    note v1
    also note a'
    finally have "wfactors G (take i as' @ drop (Suc i) as') a'"
      by (simp add: a'carr set_drop set_take)
    from a'fs this have "essentially_equal G as (take i as' @ drop (Suc i) as')"
      using Cons.hyps a'carr carr_ah(2) set_drop set_take by auto
    then obtain bs where mset as = mset bs bs [∼] take i as' @ drop (Suc i) as'
      by (auto simp add: essentially_equal_def)
    with carr_ah have mset (ah # as) = mset (ah # bs) ah # bs [∼] ah # take i as' @ drop (Suc i) as'
      by simp_all
    then have ee1: "essentially_equal G (ah # as) (ah # take i as' @ drop (Suc i) as')"
      unfolding essentially_equal_def by blast
    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: asiah associated_sym set_drop set_take)
    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')"
      by (metis Cons.prems(5) as' essentially_equalI listassoc_refl perm_append_Cons)
    finally have "essentially_equal G (ah # as) (take i as' @ as' ! i # drop (Suc i) as')"
      using Cons.prems(4) set_drop set_take by auto
    then show ?case
      using as' by auto
qed


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: "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
  then have ac: "ac = factorcount G a"
    unfolding factorcount_def using ascarr by (blast intro: theI2 afs)
  from ascarr afs have "ac = length as"
    by (simp add: alen)
  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"
  using assms
  by (auto simp: associated_def factorial_monoid.divides_fcount factorial_monoid_axioms le_antisym)

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"
    by (metis Units_one_closed assoc_unit_r ccarr foldr.simps(1) id_apply length_greater_0_conv wfactors_def)
  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"])
  using properfactor_fcount by auto

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