Theory Divisibility

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


header {* Divisibility in monoids and rings *}

theory Divisibility
imports "~~/src/HOL/Library/Permutation" Coset Group
begin

section {* Factorial Monoids *}

subsection {* Monoids with Cancellation Law *}

locale monoid_cancel = monoid +
assumes l_cancel:
"[|c ⊗ a = c ⊗ b; a ∈ carrier G; b ∈ carrier G; c ∈ carrier G|] ==> a = b"
and r_cancel:
"[|a ⊗ c = b ⊗ c; a ∈ carrier G; b ∈ carrier G; c ∈ carrier G|] ==> a = b"

lemma (in monoid) monoid_cancelI:
assumes l_cancel:
"!!a b c. [|c ⊗ a = c ⊗ b; a ∈ carrier G; b ∈ carrier G; c ∈ carrier G|] ==> a = b"
and r_cancel:
"!!a b c. [|a ⊗ c = b ⊗ c; a ∈ carrier G; b ∈ carrier G; c ∈ carrier G|] ==> a = b"
shows "monoid_cancel G"
by default fact+

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

sublocale group monoid_cancel
by default simp_all


locale comm_monoid_cancel = monoid_cancel + comm_monoid

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

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

sublocale comm_group comm_monoid_cancel
..


subsection {* Products of Units in Monoids *}

lemma (in monoid) Units_m_closed[simp, intro]:
assumes h1unit: "h1 ∈ Units G" and h2unit: "h2 ∈ Units G"
shows "h1 ⊗ h2 ∈ Units G"
unfolding Units_def
using assms
by auto (metis Units_inv_closed Units_l_inv Units_m_closed Units_r_inv)

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

have "(inv (a ⊗ b) ⊗ a) ⊗ b = inv (a ⊗ b) ⊗ (a ⊗ b)" by (simp add: m_assoc)
also have "… = \<one>" by (simp add: Units_l_inv)
finally have li: "(inv (a ⊗ b) ⊗ a) ⊗ b = \<one>" .

have "\<one> = inv a ⊗ a" by (simp add: Units_l_inv[symmetric])
also have "… = inv a ⊗ \<one> ⊗ 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 add: Units_l_inv)
also have "… = b ⊗ (inv (a ⊗ b) ⊗ a)" by (simp add: m_assoc)
finally have ri: "b ⊗ (inv (a ⊗ b) ⊗ a) = \<one> " by simp

from c li ri
show "b ∈ Units G" by (simp add: Units_def, fast)
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 "… = \<one>" by simp
finally have li: "a ⊗ (b ⊗ inv (a ⊗ b)) = \<one>" .

have "\<one> = b ⊗ inv b" by (simp add: Units_r_inv[symmetric])
also have "… = b ⊗ \<one> ⊗ 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 = \<one> " by simp

from c li ri
show "a ∈ Units G" by (simp add: Units_def, fast)
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"
and li: "i ⊗ (a ⊗ b) = \<one>"
and ri: "a ⊗ b ⊗ i = \<one>"

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 note li
finally have li': "(b ⊗ i) ⊗ a = \<one>" .

have "a ⊗ (b ⊗ i) = a ⊗ b ⊗ i" by (simp add: m_assoc)
also note ri
finally have ri': "a ⊗ (b ⊗ i) = \<one>" .

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

definition
associated :: "[_, 'a, 'a] => bool" (infix "∼\<index>" 55)
where "a ∼G b <-> a dividesG b ∧ b dividesG a"

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

definition
properfactor :: "[_, 'a, 'a] => bool"
where "properfactor G a b <-> a dividesG b ∧ ¬(b dividesG a)"

definition
irreducible :: "[_, 'a] => bool"
where "irreducible G a <-> a ∉ Units G ∧ (∀b∈carrier G. properfactor G b a --> b ∈ Units G)"

definition
prime :: "[_, 'a] => bool" where
"prime G p <->
p ∉ Units G ∧
(∀a∈carrier G. ∀b∈carrier G. p dividesG (a ⊗G b) --> p dividesG a ∨ p dividesG b)"



subsubsection {* Divisibility *}

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

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

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

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

lemma (in monoid) divides_refl[simp, intro!]:
assumes carr: "a ∈ carrier G"
shows "a divides a"
apply (intro dividesI[of "\<one>"])
apply (simp, simp add: carr)
done

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

lemma (in monoid) divides_mult_lI [intro]:
assumes ab: "a divides b"
and carr: "a ∈ carrier G" "b ∈ carrier G" "c ∈ carrier G"
shows "(c ⊗ a) divides (c ⊗ b)"
using ab
apply (elim dividesE, simp add: m_assoc[symmetric] carr)
apply (fast intro: dividesI)
done

lemma (in monoid_cancel) divides_mult_l [simp]:
assumes carr: "a ∈ carrier G" "b ∈ carrier G" "c ∈ carrier G"
shows "(c ⊗ a) divides (c ⊗ b) = a divides b"
apply safe
apply (elim dividesE, intro dividesI, assumption)
apply (rule l_cancel[of c])
apply (simp add: m_assoc carr)+
apply (fast intro: carr)
done

lemma (in comm_monoid) divides_mult_rI [intro]:
assumes ab: "a divides b"
and carr: "a ∈ carrier G" "b ∈ carrier G" "c ∈ carrier G"
shows "(a ⊗ c) divides (b ⊗ c)"
using carr ab
apply (simp add: m_comm[of a c] m_comm[of b c])
apply (rule divides_mult_lI, assumption+)
done

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

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

lemma (in comm_monoid) divides_prod_l:
assumes carr[intro]: "a ∈ carrier G" "b ∈ carrier G" "c ∈ carrier G"
and ab: "a divides b"
shows "a divides (c ⊗ b)"
using ab carr
apply (simp add: m_comm[of c b])
apply (fast intro: divides_prod_r)
done

lemma (in monoid) unit_divides:
assumes uunit: "u ∈ Units G"
and acarr: "a ∈ carrier G"
shows "u divides a"
proof (intro dividesI[of "(inv u) ⊗ a"], fast intro: uunit acarr)
from uunit acarr
have xcarr: "inv u ⊗ a ∈ carrier G" by fast

from uunit acarr
have "u ⊗ (inv u ⊗ a) = (u ⊗ inv u) ⊗ a" by (fast intro: m_assoc[symmetric])
also have "… = \<one> ⊗ 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 \<one>"
using ucarr
by (fast dest: divides_unit intro: unit_divides)


subsubsection {* Association *}

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

lemma (in monoid) associatedI2:
assumes uunit[simp]: "u ∈ Units G"
and a: "a = b ⊗ u"
and bcarr[simp]: "b ∈ carrier G"
shows "a ∼ b"
using uunit bcarr
unfolding a
apply (intro associatedI)
apply (rule dividesI[of "inv u"], simp)
apply (simp add: m_assoc Units_closed Units_r_inv)
apply fast
done

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

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

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

assume "a divides b"
hence "∃u'∈carrier G. b = a ⊗ u'" by (rule dividesD)
from this obtain u'
where u'carr: "u' ∈ carrier G" and b: "b = a ⊗ u'"
by auto
note carr = carr ucarr u'carr

from carr
have "a ⊗ \<one> = 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 ⊗ \<one> = a ⊗ (u' ⊗ u)" .
with carr
have u1: "\<one> = u' ⊗ u" by (fast dest: l_cancel)

from carr
have "b ⊗ \<one> = 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 ⊗ \<one> = b ⊗ (u ⊗ u')" .
with carr
have u2: "\<one> = u ⊗ u'" by (fast dest: l_cancel)

from u'carr u1[symmetric] u2[symmetric]
have "∃u'∈carrier G. u' ⊗ u = \<one> ∧ u ⊗ u' = \<one>" by fast
hence "u ∈ Units G" by (simp add: Units_def ucarr)

from ucarr this a
show "∃u∈Units G. a = b ⊗ u" by fast
qed

lemma associatedE:
fixes G (structure)
assumes assoc: "a ∼ b"
and e: "[|a divides b; b divides a|] ==> P"
shows "P"
proof -
from assoc
have "a divides b" "b divides a"
by (simp add: associated_def)+
thus "P" by (elim e)
qed

lemma (in monoid_cancel) associatedE2:
assumes assoc: "a ∼ b"
and e: "!!u. [|a = b ⊗ u; u ∈ Units G|] ==> P"
and carr: "a ∈ carrier G" "b ∈ carrier G"
shows "P"
proof -
from assoc and carr
have "∃u∈Units G. a = b ⊗ u" by (rule associatedD2)
from this obtain u
where "u ∈ Units G" "a = b ⊗ u"
by auto
thus "P" by (elim e)
qed

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

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

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

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


subsubsection {* Division and associativity *}

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

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

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

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


subsubsection {* Multiplication and associativity *}

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

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

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

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


subsubsection {* Units *}

lemma (in monoid_cancel) assoc_unit_l [trans]:
assumes asc: "a ∼ b" and bunit: "b ∈ Units G"
and carr: "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) {\<one>}"
apply (simp add: set_eq_def elem_def, rule, simp_all)
proof clarsimp
fix a
assume aunit: "a ∈ Units G"
show "a ∼ \<one>"
apply (rule associatedI)
apply (fast intro: dividesI[of "inv a"] aunit Units_r_inv[symmetric])
apply (fast intro: dividesI[of "a"] l_one[symmetric] Units_closed[OF aunit])
done
next
have "\<one> ∈ Units G" by simp
moreover have "\<one> ∼ \<one>" by simp
ultimately show "∃a ∈ Units G. \<one> ∼ a" by fast
qed

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


subsubsection {* Proper factors *}

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

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

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

have "a ⊗ \<one> = a" by simp
also assume "a = a ⊗ b ⊗ c"
also have "… = a ⊗ (b ⊗ c)" by (simp add: m_assoc)
finally have "a ⊗ \<one> = a ⊗ (b ⊗ c)" .

hence rinv: "\<one> = b ⊗ c" by (intro l_cancel[of "a" "\<one>" "b ⊗ c"], simp+)
also have "… = c ⊗ b" by (simp add: m_comm)
finally have linv: "\<one> = c ⊗ b" .

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

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

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

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


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

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

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

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

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

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

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

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

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

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

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

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+)


subsection {* Irreducible Elements and Primes *}

subsubsection {* Irreducible elements *}

lemma irreducibleI:
fixes G (structure)
assumes "a ∉ Units G"
and "!!b. [|b ∈ carrier G; properfactor G b a|] ==> b ∈ Units G"
shows "irreducible G a"
using assms
unfolding irreducible_def
by blast

lemma irreducibleE:
fixes G (structure)
assumes irr: "irreducible G a"
and elim: "[|a ∉ Units G; ∀b. b ∈ carrier G ∧ properfactor G b a --> b ∈ Units G|] ==> P"
shows "P"
using assms
unfolding irreducible_def
by blast

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

lemma (in monoid_cancel) irreducible_cong [trans]:
assumes irred: "irreducible G a"
and aa': "a ∼ a'"
and carr[simp]: "a ∈ carrier G" "a' ∈ carrier G"
shows "irreducible G a'"
using assms
apply (elim irreducibleE, intro irreducibleI)
apply simp_all
apply (metis assms(2) assms(3) assoc_unit_l)
apply (metis assms(2) assms(3) assms(4) associated_sym properfactor_cong_r)
done

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

lemma (in comm_monoid) irreducible_prod_lI:
assumes birr: "irreducible G b"
and aunit: "a ∈ Units G"
and carr [simp]: "a ∈ carrier G" "b ∈ carrier G"
shows "irreducible G (a ⊗ b)"
apply (subst m_comm, simp+)
apply (intro irreducible_prod_rI assms)
done

lemma (in comm_monoid_cancel) irreducible_prodE [elim]:
assumes irr: "irreducible G (a ⊗ b)"
and carr[simp]: "a ∈ carrier G" "b ∈ carrier G"
and e1: "[|irreducible G a; b ∈ Units G|] ==> P"
and e2: "[|a ∈ Units G; irreducible G b|] ==> P"
shows "P"
using irr
proof (elim irreducibleE)
assume abnunit: "a ⊗ b ∉ Units G"
and isunit[rule_format]: "∀ba. ba ∈ carrier G ∧ properfactor G ba (a ⊗ b) --> ba ∈ Units G"

show "P"
proof (cases "a ∈ Units G")
assume aunit: "a ∈ Units G"
have "irreducible G b"
apply (rule irreducibleI)
proof (rule ccontr, simp)
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"
hence "properfactor G c (a ⊗ b)" by (simp add: properfactor_prod_l[of c b a])
from ccarr this show "c ∈ Units G" by (fast intro: isunit)
qed

from aunit this show "P" by (rule e2)
next
assume anunit: "a ∉ Units G"
with carr have "properfactor G b (b ⊗ a)" by (fast intro: properfactorI3)
hence bf: "properfactor G b (a ⊗ b)" by (subst m_comm[of a b], simp+)
hence bunit: "b ∈ Units G" by (intro isunit, simp)

have "irreducible G a"
apply (rule irreducibleI)
proof (rule ccontr, simp)
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"
hence "properfactor G c (a ⊗ b)" by (simp add: properfactor_prod_r[of c a b])
from ccarr this show "c ∈ Units G" by (fast intro: isunit)
qed

from this bunit show "P" by (rule e1)
qed
qed


subsubsection {* Prime elements *}

lemma primeI:
fixes G (structure)
assumes "p ∉ Units G"
and "!!a b. [|a ∈ carrier G; b ∈ carrier G; p divides (a ⊗ b)|] ==> p divides a ∨ p divides b"
shows "prime G p"
using assms
unfolding prime_def
by blast

lemma primeE:
fixes G (structure)
assumes pprime: "prime G p"
and e: "[|p ∉ Units G; ∀a∈carrier G. ∀b∈carrier G.
p divides a ⊗ b --> p divides a ∨ p divides b|] ==> P"

shows "P"
using pprime
unfolding prime_def
by (blast dest: e)

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

lemma (in monoid_cancel) prime_cong [trans]:
assumes pprime: "prime G p"
and pp': "p ∼ p'"
and carr[simp]: "p ∈ carrier G" "p' ∈ carrier G"
shows "prime G p'"
using pprime
apply (elim primeE, intro primeI)
apply (metis assms(2) assms(3) assoc_unit_l)
apply (metis assms(2) assms(3) assms(4) associated_sym divides_cong_l m_closed)
done

subsection {* Factorization and Factorial Monoids *}

subsubsection {* Function definitions *}

definition
factors :: "[_, 'a list, 'a] => bool"
where "factors G fs a <-> (∀x ∈ (set fs). irreducible G x) ∧ foldr (op ⊗G) fs \<one>G = a"

definition
wfactors ::"[_, 'a list, 'a] => bool"
where "wfactors G fs a <-> (∀x ∈ (set fs). irreducible G x) ∧ foldr (op ⊗G) fs \<one>GG a"

abbreviation
list_assoc :: "('a,_) monoid_scheme => 'a list => 'a list => bool" (infix "[∼]\<index>" 44)
where "list_assoc G == list_all2 (op ∼G)"

definition
essentially_equal :: "[_, 'a list, 'a list] => bool"
where "essentially_equal G fs1 fs2 <-> (∃fs1'. fs1 <~~> fs1' ∧ fs1' [∼]G fs2)"


locale factorial_monoid = comm_monoid_cancel +
assumes factors_exist:
"[|a ∈ carrier G; a ∉ Units G|] ==> ∃fs. set fs ⊆ carrier G ∧ factors G fs a"
and factors_unique:
"[|factors G fs a; factors G fs' a; a ∈ carrier G; a ∉ Units G;
set fs ⊆ carrier G; set fs' ⊆ carrier G|] ==> essentially_equal G fs fs'"



subsubsection {* Comparing lists of elements *}

text {* Association on lists *}

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

lemma (in monoid) listassoc_sym [sym]:
assumes "as [∼] bs"
and "set as ⊆ carrier G" and "set bs ⊆ carrier G"
shows "bs [∼] as"
using assms
proof (induct as arbitrary: bs, simp)
case Cons
thus ?case
apply (induct bs, simp)
apply clarsimp
apply (iprover intro: associated_sym)
done
qed

lemma (in monoid) listassoc_trans [trans]:
assumes "as [∼] bs" and "bs [∼] cs"
and "set as ⊆ carrier G" and "set bs ⊆ carrier G" and "set cs ⊆ carrier G"
shows "as [∼] cs"
using assms
apply (simp add: list_all2_conv_all_nth set_conv_nth, safe)
apply (rule associated_trans)
apply (subgoal_tac "as ! i ∼ bs ! i", assumption)
apply (simp, simp)
apply blast+
done

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


text {* Permutations *}

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

lemma perm_map_switch:
assumes m: "map f a = map f b" and p: "b <~~> c"
shows "∃d. a <~~> d ∧ map f d = map f c"
using p m
by (induct arbitrary: a) (simp, force, force, blast)

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

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

declare perm_sym [sym]

lemma perm_setP:
assumes perm: "as <~~> bs"
and as: "P (set as)"
shows "P (set bs)"
proof -
from perm
have "multiset_of as = multiset_of bs"
by (simp add: multiset_of_eq_perm)
hence "set as = set bs" by (rule multiset_of_eq_setD)
with as
show "P (set bs)" by simp
qed

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

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


text {* Essentially equal factorizations *}

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

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

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

lemma (in monoid) ee_sym [sym]:
assumes ee: "essentially_equal G as bs"
and carr: "set as ⊆ carrier G" "set bs ⊆ carrier G"
shows "essentially_equal G bs as"
using ee
proof (elim essentially_equalE)
fix fs
assume "as <~~> fs" "fs [∼] bs"
hence "∃fs'. as [∼] fs' ∧ fs' <~~> bs" by (rule perm_assoc_switch_r)
from this obtain fs'
where a: "as [∼] fs'" and p: "fs' <~~> bs"
by auto
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"
hence "∃bs'. abs <~~> bs' ∧ bs' [∼] bcs" by (rule perm_assoc_switch)
from this obtain bs'
where p: "abs <~~> bs'" and a: "bs' [∼] bcs"
by auto

assume "as <~~> abs"
with p
have pp: "as <~~> bs'" by fast

from pp ascarr have c1: "set bs' ⊆ carrier G" by (rule perm_closed)
from pb bscarr have c2: "set bcs ⊆ carrier G" by (rule perm_closed)
note a
also assume "bcs [∼] cs"
finally (listassoc_trans) have"bs' [∼] cs" by (simp add: c1 c2 cscarr)

with pp
show ?thesis
by (rule essentially_equalI)
qed


subsubsection {* Properties of lists of elements *}

text {* Multiplication of factors in a list *}

lemma (in monoid) multlist_closed [simp, intro]:
assumes ascarr: "set fs ⊆ carrier G"
shows "foldr (op ⊗) fs \<one> ∈ carrier G"
by (insert ascarr, induct fs, simp+)

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

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

lemma (in comm_monoid) multlist_perm_cong:
assumes prm: "as <~~> bs"
and ascarr: "set as ⊆ carrier G"
shows "foldr (op ⊗) as \<one> = foldr (op ⊗) bs \<one>"
using prm ascarr
apply (induct, simp, clarsimp simp add: m_ac, clarsimp)
proof clarsimp
fix xs ys zs
assume "xs <~~> ys" "set xs ⊆ carrier G"
hence "set ys ⊆ carrier G" by (rule perm_closed)
moreover assume "set ys ⊆ carrier G ==> foldr op ⊗ ys \<one> = foldr op ⊗ zs \<one>"
ultimately show "foldr op ⊗ ys \<one> = foldr op ⊗ zs \<one>" by simp
qed

lemma (in comm_monoid_cancel) multlist_ee_cong:
assumes "essentially_equal G fs fs'"
and "set fs ⊆ carrier G" and "set fs' ⊆ carrier G"
shows "foldr (op ⊗) fs \<one> ∼ foldr (op ⊗) fs' \<one>"
using assms
apply (elim essentially_equalE)
apply (simp add: multlist_perm_cong multlist_listassoc_cong perm_closed)
done


subsubsection {* Factorization in irreducible elements *}

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

lemma wfactorsE:
fixes G (structure)
assumes wf: "wfactors G fs a"
and e: "[|∀f∈set fs. irreducible G f; foldr (op ⊗) fs \<one> ∼ a|] ==> P"
shows "P"
using wf
unfolding wfactors_def
by (fast dest: e)

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

lemma factorsE:
fixes G (structure)
assumes f: "factors G fs a"
and e: "[|∀f∈set fs. irreducible G f; foldr (op ⊗) fs \<one> = 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 ≠ \<one>" 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 (rule ccontr, cases fs, simp)
fix f fs'
assume fs: "fs = f # fs'"

from carr
have fcarr[simp]: "f ∈ carrier G"
and carr'[simp]: "set fs' ⊆ carrier G"
by (simp add: fs)+

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

from fs wf
have a: "f ⊗ foldr (op ⊗) fs' \<one> ∼ a" by (simp add: wfactors_def)

note aunit
also from fs wf
have a: "f ⊗ foldr (op ⊗) fs' \<one> ∼ a" by (simp add: wfactors_def)
have "a ∼ f ⊗ foldr (op ⊗) fs' \<one>"
by (simp add: Units_closed[OF aunit] a[symmetric])
finally
have "f ⊗ foldr (op ⊗) fs' \<one> ∈ Units G" by simp
hence "f ∈ Units G" by (intro unit_factor[of f], simp+)

with fnunit show "False" by simp
qed


text {* Comparing wfactors *}

lemma (in comm_monoid_cancel) wfactors_listassoc_cong_l:
assumes fact: "wfactors G fs a"
and asc: "fs [∼] fs'"
and carr: "a ∈ carrier G" "set fs ⊆ carrier G" "set fs' ⊆ carrier G"
shows "wfactors G fs' a"
using fact
apply (elim wfactorsE, intro wfactorsI)
apply (metis assms(2) assms(4) assms(5) irrlist_listassoc_cong)
proof -
from asc[symmetric]
have "foldr op ⊗ fs' \<one> ∼ foldr op ⊗ fs \<one>"
by (simp add: multlist_listassoc_cong carr)
also assume "foldr op ⊗ fs \<one> ∼ a"
finally
show "foldr op ⊗ fs' \<one> ∼ a" by (simp add: carr)
qed

lemma (in comm_monoid) wfactors_perm_cong_l:
assumes "wfactors G fs a"
and "fs <~~> fs'"
and "set fs ⊆ carrier G"
shows "wfactors G fs' a"
using assms
apply (elim wfactorsE, intro wfactorsI)
apply (rule irrlist_perm_cong, assumption+)
apply (simp add: multlist_perm_cong[symmetric])
done

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

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

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


subsubsection {* Essentially equal factorizations *}

lemma (in comm_monoid_cancel) unitfactor_ee:
assumes uunit: "u ∈ Units G"
and carr: "set as ⊆ carrier G"
shows "essentially_equal G (as[0 := (as!0 ⊗ u)]) as" (is "essentially_equal G ?as' as")
using assms
apply (intro essentially_equalI[of _ ?as'], simp)
apply (cases as, simp)
apply (clarsimp, fast intro: associatedI2[of u])
done

lemma (in comm_monoid_cancel) factors_cong_unit:
assumes uunit: "u ∈ Units G" and anunit: "a ∉ Units G"
and afs: "factors G as a"
and ascarr: "set as ⊆ carrier G"
shows "factors G (as[0 := (as!0 ⊗ u)]) (a ⊗ u)" (is "factors G ?as' ?a'")
using assms
apply (elim factorsE, clarify)
apply (cases as)
apply (simp add: nunit_factors)
apply clarsimp
apply (elim factorsE, intro factorsI)
apply (clarsimp, fast intro: irreducible_prod_rI)
apply (simp add: m_ac Units_closed)
done

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

lemma (in comm_monoid_cancel) listassoc_wfactorsD:
assumes assoc: "as [∼] bs"
and afs: "wfactors G as a" and bfs: "wfactors G bs b"
and [simp]: "a ∈ carrier G" "b ∈ carrier G"
and [simp]: "set as ⊆ carrier G" "set bs ⊆ carrier G"
shows "a ∼ b"
using afs bfs
proof (elim wfactorsE)
assume "foldr op ⊗ as \<one> ∼ a"
hence "a ∼ foldr op ⊗ as \<one>" by (rule associated_sym, simp+)
also from assoc
have "foldr op ⊗ as \<one> ∼ foldr op ⊗ bs \<one>" by (rule multlist_listassoc_cong, simp+)
also assume "foldr op ⊗ bs \<one> ∼ 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"
hence 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+)
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
have "∃u∈Units G. a = b ⊗ u" by (fast elim: associatedE2)
from this obtain u
where uunit: "u ∈ Units G"
and a: "a = b ⊗ u" by auto

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 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")
assume aunit: "a ∈ Units G"
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)
thus ?thesis by (simp add: e e')
next
assume anunit: "a ∉ Units G"
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

have "∃a'. factors G as a' ∧ a' ∼ a" by (rule wfactors_factors[OF asf ascarr])
from this obtain a'
where fa': "factors G as a'"
and a': "a' ∼ a"
by auto
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

have "∃b'. factors G bs b' ∧ b' ∼ b" by (rule wfactors_factors[OF bsf bscarr])
from this obtain b'
where fb': "factors G bs b'"
and b': "b' ∼ b"
by auto
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")
assume "a ∈ Units G"
hence "wfactors G [] a" by (rule unit_wfactors)
thus ?thesis by (intro exI) force
next
assume "a ∉ Units G"
hence "∃fs. set fs ⊆ carrier G ∧ factors G fs a" by (intro factors_exist acarr)
from this obtain fs
where fscarr: "set fs ⊆ carrier G"
and f: "factors G fs a"
by auto
from f have "wfactors G fs a" by (rule factors_wfactors) fact
from fscarr this
show ?thesis by fast
qed

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

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

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

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

lemma (in monoid) factors_mult:
assumes factors: "factors G fa a" "factors G fb b"
and ascarr: "set fa ⊆ carrier G" and bscarr:"set fb ⊆ carrier G"
shows "factors G (fa @ fb) (a ⊗ b)"
using assms
unfolding factors_def
apply (safe, force)
apply (induct fa)
apply simp
apply (simp add: m_assoc)
done

lemma (in comm_monoid_cancel) wfactors_mult [intro]:
assumes asf: "wfactors G as a" and bsf:"wfactors G bs b"
and acarr: "a ∈ carrier G" and bcarr: "b ∈ carrier G"
and ascarr: "set as ⊆ carrier G" and bscarr:"set bs ⊆ carrier G"
shows "wfactors G (as @ bs) (a ⊗ b)"
apply (insert wfactors_factors[OF asf ascarr])
apply (insert 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+
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"
apply (insert wfactors_factors[OF p fscarr], clarsimp)
proof -
fix a'
assume fsa': "factors G fs a'"
and a'a: "a' ∼ a"
with fscarr
have a'carr: "a' ∈ carrier G" by (simp add: factors_closed)

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


subsubsection {* Factorial monoids and wfactors *}

lemma (in comm_monoid_cancel) factorial_monoidI:
assumes wfactors_exists:
"!!a. a ∈ carrier G ==> ∃fs. set fs ⊆ carrier G ∧ wfactors G fs a"
and wfactors_unique:
"!!a fs fs'. [|a ∈ carrier G; set fs ⊆ carrier G; set fs' ⊆ carrier G;
wfactors G fs a; wfactors G fs' a|] ==> essentially_equal G fs fs'"

shows "factorial_monoid G"
proof
fix a
assume acarr: "a ∈ carrier G" and anunit: "a ∉ Units G"

from wfactors_exists[OF acarr]
obtain as
where ascarr: "set as ⊆ carrier G"
and afs: "wfactors G as a"
by auto
from afs ascarr
have "∃a'. factors G as a' ∧ a' ∼ a" by (rule wfactors_factors)
from this obtain a'
where afs': "factors G as a'"
and a'a: "a' ∼ a"
by auto
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
have "∃u. u ∈ Units G ∧ a' = a ⊗ u" by (blast elim: associatedE2)
from this obtain u
where uunit: "u ∈ Units G"
and a': "a' = a ⊗ u"
by auto

note [simp] = acarr Units_closed[OF uunit] Units_inv_closed[OF uunit]

have "a = a ⊗ \<one>" by simp
also have "… = a ⊗ (u ⊗ inv u)" by (simp add: Units_r_inv 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, clarsimp+)

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 = multiset_of (map (λa. assocs G a) as)"


text {* Helper lemmas *}

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

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

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

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

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


subsubsection {* Comparing multisets *}

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

lemma (in comm_monoid_cancel) eqc_listassoc_cong:
assumes "as [∼] bs"
and "set as ⊆ carrier G" and "set bs ⊆ carrier G"
shows "map (assocs G) as = map (assocs G) bs"
using assms
apply (induct as arbitrary: bs, simp)
apply (clarsimp simp add: Cons_eq_map_conv list_all2_Cons1, safe)
apply (clarsimp elim!: closure_ofE2) defer 1
apply (clarsimp elim!: closure_ofE2) defer 1
proof -
fix a x z
assume carr[simp]: "a ∈ carrier G" "x ∈ carrier G" "z ∈ carrier G"
assume "x ∼ a"
also assume "a ∼ z"
finally have "x ∼ z" by simp
with carr
show "x ∈ assocs G z"
by (intro closure_ofI2) simp+
next
fix a x z
assume carr[simp]: "a ∈ carrier G" "x ∈ carrier G" "z ∈ carrier G"
assume "x ∼ z"
also assume [symmetric]: "a ∼ z"
finally have "x ∼ a" by simp
with carr
show "x ∈ assocs G a"
by (intro closure_ofI2) simp+
qed

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

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

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

lemma (in monoid_cancel) fmset_ee__hlp_induct:
assumes prm: "cas <~~> cbs"
and cdef: "cas = map (assocs G) as" "cbs = map (assocs G) bs"
shows "∀as bs. (cas <~~> cbs ∧ cas = map (assocs G) as ∧
cbs = map (assocs G) bs) --> (∃as'. as <~~> as' ∧ map (assocs G) as' = cbs)"

apply (rule perm.induct[of cas cbs], rule prm)
apply safe apply simp_all
apply (simp add: map_eq_Cons_conv, blast)
apply force
proof -
fix ys as bs
assume p1: "map (assocs G) as <~~> ys"
and r1[rule_format]:
"∀asa bs. map (assocs G) as = map (assocs G) asa ∧
ys = map (assocs G) bs
--> (∃as'. asa <~~> as' ∧ map (assocs G) as' = map (assocs G) bs)"

and p2: "ys <~~> map (assocs G) bs"
and r2[rule_format]:
"∀as bsa. ys = map (assocs G) as ∧
map (assocs G) bs = map (assocs G) bsa
--> (∃as'. as <~~> as' ∧ map (assocs G) as' = map (assocs G) bsa)"

and p3: "map (assocs G) as <~~> map (assocs G) bs"

from p1
have "multiset_of (map (assocs G) as) = multiset_of ys"
by (simp add: multiset_of_eq_perm)
hence setys: "set (map (assocs G) as) = set ys" by (rule multiset_of_eq_setD)

have "set (map (assocs G) as) = { assocs G x | x. x ∈ set as}" by clarsimp fast
with setys have "set ys ⊆ { assocs G x | x. x ∈ set as}" by simp
hence "∃yy. ys = map (assocs G) yy"
apply (induct ys, simp, clarsimp)
proof -
fix yy x
show "∃yya. (assocs G x) # map (assocs G) yy =
map (assocs G) yya"

by (rule exI[of _ "x#yy"], simp)
qed
from this obtain yy
where ys: "ys = map (assocs G) yy"
by auto

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

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

from as'yy and yyas''
have "∃cs. as' <~~> cs ∧ map (assocs G) cs = map (assocs G) as''"
by (rule perm_map_switch)
from this obtain cs
where as'cs: "as' <~~> cs"
and csas'': "map (assocs G) cs = map (assocs G) as''"
by auto

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

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

have "∃cas. cas = map (assocs G) as" by simp
from this obtain cas where cas: "cas = map (assocs G) as" by simp

have "∃cbs. cbs = map (assocs G) bs" by simp
from this obtain cbs where cbs: "cbs = map (assocs G) bs" by simp

from cas cbs mpp
have [rule_format]:
"∀as bs. (cas <~~> cbs ∧ cas = map (assocs G) as ∧
cbs = map (assocs G) bs)
--> (∃as'. as <~~> as' ∧ map (assocs G) as' = cbs)"

by (intro fmset_ee__hlp_induct, simp+)
with mpp cas cbs
have "∃as'. as <~~> as' ∧ map (assocs G) as' = map (assocs G) bs"
by simp

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

from tm as'carr[THEN subsetD] bscarr[THEN subsetD]
have "as' [∼] bs"
by (induct as' arbitrary: bs) (simp, fastforce dest: assocs_eqD[THEN associated_sym])

from tp and this
show "essentially_equal G as bs" by (fast intro: essentially_equalI)
qed

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


subsubsection {* Interpreting multisets as factorizations *}

lemma (in monoid) mset_fmsetEx:
assumes elems: "!!X. X ∈ set_of Cs ==> ∃x. P x ∧ X = assocs G x"
shows "∃cs. (∀c ∈ set cs. P c) ∧ fmset G cs = Cs"
proof -
have "∃Cs'. Cs = multiset_of Cs'"
by (rule surjE[OF surj_multiset_of], fast)
from this obtain Cs'
where Cs: "Cs = multiset_of Cs'"
by auto

have "∃cs. (∀c ∈ set cs. P c) ∧ multiset_of (map (assocs G) cs) = Cs"
using elems
unfolding Cs
apply (induct Cs', simp)
apply clarsimp
apply (subgoal_tac "∃cs. (∀x∈set cs. P x) ∧
multiset_of (map (assocs G) cs) = multiset_of Cs'"
)
proof clarsimp
fix a Cs' cs
assume ih: "!!X. X = a ∨ X ∈ set Cs' ==> ∃x. P x ∧ X = assocs G x"
and csP: "∀x∈set cs. P x"
and mset: "multiset_of (map (assocs G) cs) = multiset_of Cs'"
from ih
have "∃x. P x ∧ a = assocs G x" by fast
from this obtain c
where cP: "P c"
and a: "a = assocs G c"
by auto
from cP csP
have tP: "∀x∈set (c#cs). P x" by simp
from mset a
have "multiset_of (map (assocs G) (c#cs)) = multiset_of Cs' + {#a#}" by simp
from tP this
show "∃cs. (∀x∈set cs. P x) ∧
multiset_of (map (assocs G) cs) =
multiset_of Cs' + {#a#}"
by fast
qed simp
thus ?thesis by (simp add: fmset_def)
qed

lemma (in monoid) mset_wfactorsEx:
assumes elems: "!!X. X ∈ set_of Cs
==> ∃x. (x ∈ carrier G ∧ irreducible G x) ∧ X = assocs G x"

shows "∃c cs. c ∈ carrier G ∧ set cs ⊆ carrier G ∧ wfactors G cs c ∧ fmset G cs = Cs"
proof -
have "∃cs. (∀c∈set cs. c ∈ carrier G ∧ irreducible G c) ∧ fmset G cs = Cs"
by (intro mset_fmsetEx, rule elems)
from this obtain cs
where p[rule_format]: "∀c∈set cs. c ∈ carrier G ∧ irreducible G c"
and Cs[symmetric]: "fmset G cs = Cs"
by auto

from p
have cscarr: "set cs ⊆ carrier G" by fast

from p
have "∃c. c ∈ carrier G ∧ wfactors G cs c"
by (intro wfactors_prod_exists) fast+
from this obtain c
where ccarr: "c ∈ carrier G"
and cfs: "wfactors G cs c"
by auto

with cscarr Cs
show ?thesis by fast
qed


subsubsection {* Multiplication on multisets *}

lemma (in factorial_monoid) mult_wfactors_fmset:
assumes afs: "wfactors G as a" and bfs: "wfactors G bs b" and cfs: "wfactors G cs (a ⊗ b)"
and carr: "a ∈ carrier G" "b ∈ carrier G"
"set as ⊆ carrier G" "set bs ⊆ carrier G" "set cs ⊆ carrier G"
shows "fmset G cs = fmset G as + fmset G bs"
proof -
from assms
have "wfactors G (as @ bs) (a ⊗ b)" by (intro wfactors_mult)
with carr cfs
have "essentially_equal G cs (as@bs)" by (intro ee_wfactorsI[of "a⊗b" "a⊗b"], simp+)
with carr
have "fmset G cs = fmset G (as@bs)" by (intro ee_fmset, simp+)
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 add: carr)+
then show "c ∼ a ⊗ b" by (rule ee_wfactorsD[of "cs" "as@bs"]) (simp 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"
hence "∃cs. set cs ⊆ carrier G ∧ wfactors G cs c" by (rule wfactors_exist)
from this obtain cs
where cscarr: "set cs ⊆ carrier G"
and cfs: "wfactors G cs c" by auto
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+

thus ?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 "count (fmset G as) X < count (fmset G bs) X"
hence "0 < count (fmset G bs) X" by simp
hence "X ∈ set_of (fmset G bs)" by simp
hence "X ∈ set (map (assocs G) bs)" by (simp add: fmset_def)
hence "∃x. x ∈ set bs ∧ X = assocs G x" by (induct bs) auto
from this 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
from this 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 mset_le_def)
hence basc: "b ∼ a ⊗ c"
by (rule fmset_wfactors_mult) fact+

thus ?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 add: acarr bcarr ccarr)+
qed

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


text {* Proper factors on multisets *}

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

lemma (in factorial_monoid) properfactor_fmset:
assumes pf: "properfactor G a b"
and "wfactors G as a" and "wfactors G bs b"
and "a ∈ carrier G" and "b ∈ carrier G"
and "set as ⊆ carrier G" and "set bs ⊆ carrier G"
shows "fmset G as ≤ fmset G bs ∧ fmset G as ≠ fmset G bs"
using pf
apply (elim properfactorE)
apply rule
apply (intro divides_fmsubset, assumption)
apply (rule assms)+
apply (metis assms divides_fmsubset fmsubset_divides)
done

subsection {* Irreducible Elements are Prime *}

lemma (in factorial_monoid) irreducible_is_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
have "∃c∈carrier G. a ⊗ b = p ⊗ c" by (rule dividesD)
from this obtain c
where ccarr: "c ∈ carrier G"
and abpc: "a ⊗ b = p ⊗ c"
by auto

from acarr have "∃fs. set fs ⊆ carrier G ∧ wfactors G fs a" by (rule wfactors_exist)
from this obtain as where ascarr: "set as ⊆ carrier G" and afs: "wfactors G as a" by auto

from bcarr have "∃fs. set fs ⊆ carrier G ∧ wfactors G fs b" by (rule wfactors_exist)
from this obtain bs where bscarr: "set bs ⊆ carrier G" and bfs: "wfactors G bs b" by auto

from ccarr have "∃fs. set fs ⊆ carrier G ∧ wfactors G fs c" by (rule wfactors_exist)
from this obtain cs where cscarr: "set cs ⊆ carrier G" and cfs: "wfactors G cs c" by auto

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

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

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

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

hence "∃ds. p # cs <~~> ds ∧ ds [∼] (as @ bs)"
by (fast elim: essentially_equalE)
from this obtain ds
where "p # cs <~~> ds"
and dsassoc: "ds [∼] (as @ bs)"
by auto

then have "p ∈ set ds"
by (simp add: perm_set_eq[symmetric])
with dsassoc
have "∃p'. p' ∈ set (as@bs) ∧ p ∼ p'"
unfolding list_all2_conv_all_nth set_conv_nth
by force

from this obtain p'
where "p' ∈ set (as@bs)"
and pp': "p ∼ p'"
by auto

hence "p' ∈ set as ∨ p' ∈ set bs" by simp
moreover
{
assume p'elem: "p' ∈ set as"
with ascarr have [simp]: "p' ∈ carrier G" by fast

note pp'
also from afs
have "p' divides a" by (rule wfactors_dividesI) fact+
finally
have "p divides a" by simp
}
moreover
{
assume p'elem: "p' ∈ set bs"
with bscarr have [simp]: "p' ∈ carrier G" by fast

note pp'
also from bfs
have "p' divides b" by (rule wfactors_dividesI) fact+
finally
have "p divides b" by simp
}
ultimately
show "p divides a ∨ p divides b" by fast
qed


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

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

note pdvdab
also have "a ⊗ b = b ⊗ a" by (simp add: m_comm)
also from aunit
have bab: "b ⊗ a ∼ b"
by (intro associatedI2[of "a"], simp+)
finally
have "p divides b" by simp
thus "p divides a ∨ p divides b" ..
next
assume anunit: "a ∉ Units G"

show "p divides a ∨ p divides b"
proof (cases "b ∈ Units G")
assume bunit: "b ∈ Units G"

note pdvdab
also from bunit
have baa: "a ⊗ b ∼ a"
by (intro associatedI2[of "b"], simp+)
finally
have "p divides a" by simp
thus "p divides a ∨ p divides b" ..
next
assume bnunit: "b ∉ Units G"

have cnunit: "c ∉ Units G"
proof (rule ccontr, simp)
assume cunit: "c ∈ Units G"
from bnunit
have "properfactor G a (a ⊗ b)"
by (intro properfactorI3[of _ _ b], simp+)
also note abpc
also from cunit
have "p ⊗ c ∼ p"
by (intro associatedI2[of c], simp+)
finally
have "properfactor G a p" by simp

with acarr
have "a ∈ Units G" by (fast intro: irreduc)
with anunit
show "False" ..
qed

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

from acarr anunit have "∃fs. set fs ⊆ carrier G ∧ factors G fs a" by (rule factors_exist)
then obtain as where ascarr: "set as ⊆ carrier G" and afac: "factors G as a" by auto

from bcarr bnunit have "∃fs. set fs ⊆ carrier G ∧ factors G fs b" by (rule factors_exist)
then obtain bs where bscarr: "set bs ⊆ carrier G" and bfac: "factors G bs b" by auto

from ccarr cnunit have "∃fs. set fs ⊆ carrier G ∧ factors G fs c" by (rule factors_exist)
then obtain cs where cscarr: "set cs ⊆ carrier G" and cfac: "factors G cs c" by auto

note [simp] = ascarr bscarr cscarr

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

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

from abfac' abfac
have "essentially_equal G (p # cs) (as @ bs)"
by (rule factors_unique) (fact | simp)+

hence "∃ds. p # cs <~~> ds ∧ ds [∼] (as @ bs)"
by (fast elim: essentially_equalE)
from this obtain ds
where "p # cs <~~> ds"
and dsassoc: "ds [∼] (as @ bs)"
by auto

then have "p ∈ set ds"
by (simp add: perm_set_eq[symmetric])
with dsassoc
have "∃p'. p' ∈ set (as@bs) ∧ p ∼ p'"
unfolding list_all2_conv_all_nth set_conv_nth
by force

from this obtain p'
where "p' ∈ set (as@bs)"
and pp': "p ∼ p'" by auto

hence "p' ∈ set as ∨ p' ∈ set bs" by simp
moreover
{
assume p'elem: "p' ∈ set as"
with ascarr have [simp]: "p' ∈ carrier G" by fast

note pp'
also from afac p'elem
have "p' divides a" by (rule factors_dividesI) fact+
finally
have "p divides a" by simp
}
moreover
{
assume p'elem: "p' ∈ set bs"
with bscarr have [simp]: "p' ∈ carrier G" by fast

note pp'
also from bfac
have "p' divides b" by (rule factors_dividesI) fact+
finally have "p divides b" by simp
}
ultimately
show "p divides a ∨ p divides b" by fast
qed
qed
qed


subsection {* Greatest Common Divisors and Lowest Common Multiples *}

subsubsection {* Definitions *}

definition
isgcd :: "[('a,_) monoid_scheme, 'a, 'a, 'a] => bool" ("(_ gcdof\<index> _ _)" [81,81,81] 80)
where "x gcdofG a b <-> x dividesG a ∧ x dividesG b ∧
(∀y∈carrier G. (y dividesG a ∧ y dividesG b --> y dividesG x))"


definition
islcm :: "[_, 'a, 'a, 'a] => bool" ("(_ lcmof\<index> _ _)" [81,81,81] 80)
where "x lcmofG a b <-> a dividesG x ∧ b dividesG x ∧
(∀y∈carrier G. (a dividesG y ∧ b dividesG y --> x dividesG y))"


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

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

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


locale gcd_condition_monoid = comm_monoid_cancel +
assumes gcdof_exists:
"[|a ∈ carrier G; b ∈ carrier G|] ==> ∃c. c ∈ carrier G ∧ c gcdof a b"

locale primeness_condition_monoid = comm_monoid_cancel +
assumes irreducible_prime:
"[|a ∈ carrier G; irreducible G a|] ==> prime G a"

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


subsubsection {* Connections to \texttt{Lattice.thy} *}

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

unfolding isgcd_def greatest_def Lower_def elem_def
by auto

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})"

unfolding islcm_def least_def Upper_def elem_def
by auto

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"
unfolding somegcd_def meet_def inf_def
by (simp add: 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 acarr have "∃as. set as ⊆ carrier G ∧ wfactors G as a" by (rule wfactors_exist)
from this obtain as
where ascarr: "set as ⊆ carrier G"
and afs: "wfactors G as a"
by auto
from afs have airr: "∀a ∈ set as. irreducible G a" by (fast elim: wfactorsE)

from bcarr have "∃bs. set bs ⊆ carrier G ∧ wfactors G bs b" by (rule wfactors_exist)
from this obtain bs
where bscarr: "set bs ⊆ carrier G"
and bfs: "wfactors G bs b"
by auto
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 ∈ set_of (fmset G as #∩ fmset G bs)"
hence "X ∈ set_of (fmset G as)" by (simp add: multiset_inter_def)
hence "X ∈ set (map (assocs G) as)" by (simp add: fmset_def)
hence "∃x. X = assocs G x ∧ x ∈ set as" by (induct as) auto
from this obtain x
where X: "X = assocs G x"
and xas: "x ∈ set as"
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 "∃x. (x ∈ carrier G ∧ irreducible G x) ∧ X = assocs G x" by fast
qed

from this obtain c cs
where ccarr: "c ∈ carrier G"
and cscarr: "set cs ⊆ carrier G"
and csirr: "wfactors G cs c"
and csmset: "fmset G cs = fmset G as #∩ fmset G bs" by auto

have "c gcdof a b"
proof (simp add: isgcd_def, safe)
from csmset
have "fmset G cs ≤ fmset G as"
by (simp add: multiset_inter_def mset_le_def)
thus "c divides a" by (rule fmsubset_divides) fact+
next
from csmset
have "fmset G cs ≤ fmset G bs"
by (simp add: multiset_inter_def mset_le_def, force)
thus "c divides b" by (rule fmsubset_divides) fact+
next
fix y
assume ycarr: "y ∈ carrier G"
hence "∃ys. set ys ⊆ carrier G ∧ wfactors G ys y" by (rule wfactors_exist)
from this obtain ys
where yscarr: "set ys ⊆ carrier G"
and yfs: "wfactors G ys y"
by auto

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

assume "y divides b"
hence 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: mset_le_def multiset_inter_count)
thus "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 acarr have "∃as. set as ⊆ carrier G ∧ wfactors G as a" by (rule wfactors_exist)
from this obtain as
where ascarr: "set as ⊆ carrier G"
and afs: "wfactors G as a"
by auto
from afs have airr: "∀a ∈ set as. irreducible G a" by (fast elim: wfactorsE)

from bcarr have "∃bs. set bs ⊆ carrier G ∧ wfactors G bs b" by (rule wfactors_exist)
from this obtain bs
where bscarr: "set bs ⊆ carrier G"
and bfs: "wfactors G bs b"
by auto
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 ∈ set_of ((fmset G as - fmset G bs) + fmset G bs)"
hence "X ∈ set_of (fmset G as) ∨ X ∈ set_of (fmset G bs)"
by (cases "X :# fmset G bs", simp, simp)
moreover
{
assume "X ∈ set_of (fmset G as)"
hence "X ∈ set (map (assocs G) as)" by (simp add: fmset_def)
hence "∃x. x ∈ set as ∧ X = assocs G x" by (induct as) auto
from this 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
have "∃x. (x ∈ carrier G ∧ irreducible G x) ∧ X = assocs G x" by fast
}
moreover
{
assume "X ∈ set_of (fmset G bs)"
hence "X ∈ set (map (assocs G) bs)" by (simp add: fmset_def)
hence "∃x. x ∈ set bs ∧ X = assocs G x" by (induct as) auto
from this 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
have "∃x. (x ∈ carrier G ∧ irreducible G x) ∧ X = assocs G x" by fast
}
ultimately
show "∃x. (x ∈ carrier G ∧ irreducible G x) ∧ X = assocs G x" by fast
qed

from this 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: mset_le_def, force)
thus "a divides c" by (rule fmsubset_divides) fact+
next
from csmset have "fmset G bs ≤ fmset G cs" by (simp add: mset_le_def)
thus "b divides c" by (rule fmsubset_divides) fact+
next
fix y
assume ycarr: "y ∈ carrier G"
hence "∃ys. set ys ⊆ carrier G ∧ wfactors G ys y" by (rule wfactors_exist)
from this obtain ys
where yscarr: "set ys ⊆ carrier G"
and yfs: "wfactors G ys y"
by auto

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

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

from ya yb csmset
have "fmset G cs ≤ fmset G ys"
apply (simp add: mset_le_def, clarify)
apply (case_tac "count (fmset G as) a < count (fmset G bs) a")
apply simp
apply simp
done
thus "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]:
shows "weak_lower_semilattice (division_rel G)"
proof -
interpret weak_partial_order "division_rel G" ..
show ?thesis
apply (unfold_locales, simp_all)
proof -
fix x y
assume carr: "x ∈ carrier G" "y ∈ carrier G"
hence "∃z. z ∈ carrier G ∧ z gcdof x y" by (rule gcdof_exists)
from this obtain z
where zcarr: "z ∈ carrier G"
and isgcd: "z gcdof x y"
by auto
with carr
have "greatest (division_rel G) z (Lower (division_rel G) {x, y})"
by (subst gcdof_greatestLower[symmetric], simp+)
thus "∃z. greatest (division_rel G) z (Lower (division_rel G) {x, y})" by fast
qed
qed

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

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

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

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

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

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

lemma (in gcd_condition_monoid) gcd_divides:
assumes sub: "z divides x" "z divides y"
and L: "x ∈ carrier G" "y ∈ carrier G" "z ∈ carrier G"
shows "z divides (somegcd G x y)"
proof -
interpret weak_lower_semilattice "division_rel G" by simp
show ?thesis
apply (simp add: somegcd_meet L)
apply (rule meet_le[simplified], fact+)
done
qed

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

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

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

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

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


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

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

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

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

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

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

have "?d divides b" by (simp add: gcd_divides_r)
hence 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+

hence "∃u. u ∈ carrier G ∧ ?e = c ⊗ ?d ⊗ u"
by (elim dividesE, fast)
from this obtain u
where ucarr[simp]: "u ∈ carrier G"
and e_cdu: "?e = c ⊗ ?d ⊗ u"
by auto

note carr = carr ucarr

have "?e divides c ⊗ a" by (rule gcd_divides_l) simp+
hence "∃x. x ∈ carrier G ∧ c ⊗ a = ?e ⊗ x"
by (elim dividesE, fast)
from this obtain x
where xcarr: "x ∈ carrier G"
and ca_ex: "c ⊗ a = ?e ⊗ x"
by auto
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)+
hence du'a: "?d ⊗ u divides a" by (rule dividesI[OF xcarr])

have "?e divides c ⊗ b" by (intro gcd_divides_r, simp+)
hence "∃x. x ∈ carrier G ∧ c ⊗ b = ?e ⊗ x"
by (elim dividesE, fast)
from this obtain x
where xcarr: "x ∈ carrier G"
and cb_ex: "c ⊗ b = ?e ⊗ x"
by auto
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+)
hence 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+)
hence uunit: "u ∈ Units G"
proof (elim dividesE)
fix v
assume vcarr[simp]: "v ∈ carrier G"
assume d: "?d = ?d ⊗ u ⊗ v"
have "?d ⊗ \<one> = ?d ⊗ u ⊗ v" by simp fact
also have "?d ⊗ u ⊗ v = ?d ⊗ (u ⊗ v)" by (simp add: m_assoc)
finally have "?d ⊗ \<one> = ?d ⊗ (u ⊗ v)" .
hence i2: "\<one> = u ⊗ v" by (rule l_cancel) simp+
hence i1: "\<one> = v ⊗ u" by (simp add: m_comm)
from vcarr i1[symmetric] i2[symmetric]
show "u ∈ Units G"
by (unfold Units_def, simp, fast)
qed

from e_cdu uunit
have "somegcd G (c ⊗ a) (c ⊗ b) ∼ c ⊗ somegcd G a b"
by (intro associatedI2[of u], simp+)
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: "ALL 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 ∼ \<one>" and acrelprime: "somegcd G a c ∼ \<one>"
and carr[simp]: "a ∈ carrier G" "b ∈ carrier G" "c ∈ carrier G"
shows "somegcd G a (b ⊗ c) ∼ \<one>"
proof -
have "c = c ⊗ \<one>" 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) ∼ \<one>" by simp
qed

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

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

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

from pcarr acarr bcarr pdvdab
have "p gcdof p (a ⊗ b)" by (fast intro: isgcd_divides_l)

with pcarr acarr bcarr
have "p ∼ somegcd G p (a ⊗ b)" by (fast intro: gcdI2)
also from pa pb pcarr acarr bcarr
have "somegcd G p (a ⊗ b) ∼ \<one>" by (rule relprime_mult)
finally have "p ∼ \<one>" by (simp add: pcarr acarr bcarr)

with pcarr
have "p ∈ Units G" by (fast intro: assoc_unit_l)
with pnunit
show "False" ..
qed
qed

sublocale gcd_condition_monoid primeness_condition_monoid
by (rule primeness_condition)


subsubsection {* Divisor chain condition *}

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


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

have ih':
"!!y. [|y ∈ carrier G; properfactor G y x|]
==> ∃as. set as ⊆ carrier G ∧ wfactors G as y"

by (rule ih[rule_format, simplified]) (simp add: xcarr)+

from ycarr pfyx
have "∃as. set as ⊆ carrier G ∧ wfactors G as y"
by (rule ih')
from this obtain ys
where yscarr: "set ys ⊆ carrier G"
and yfs: "wfactors G ys y"
by auto

from pfyx
have "y divides x"
and nyx: "¬ y ∼ x"
by - (fast elim: properfactorE2)+
hence "∃z. z ∈ carrier G ∧ x = y ⊗ z"
by (fast elim: dividesE)

from this obtain z
where zcarr: "z ∈ carrier G"
and x: "x = y ⊗ z"
by auto

from zcarr ycarr
have "properfactor G z x"
apply (subst x)
apply (intro properfactorI3[of _ _ y])
apply (simp add: m_comm)
apply (simp add: ynunit)+
done
with zcarr
have "∃as. set as ⊆ carrier G ∧ wfactors G as z"
by (rule ih')
from this obtain zs
where zscarr: "set zs ⊆ carrier G"
and zfs: "wfactors G zs z"
by auto

from yscarr zscarr
have xscarr: "set (ys@zs) ⊆ carrier G" by simp
from yfs zfs ycarr zcarr yscarr zscarr
have "wfactors G (ys@zs) (y⊗z)" by (rule wfactors_mult)
hence "wfactors G (ys@zs) x" by (simp add: x)

from xscarr this
show "∃xs. set xs ⊆ carrier G ∧ wfactors G xs x" by fast
qed
qed

from acarr
show ?thesis by (rule r)
qed


subsubsection {* Primeness condition *}

lemma (in comm_monoid_cancel) multlist_prime_pos:
assumes carr: "a ∈ carrier G" "set as ⊆ carrier G"
and aprime: "prime G a"
and "a divides (foldr (op ⊗) as \<one>)"
shows "∃i<length as. a divides (as!i)"
proof -
have r[rule_format]:
"set as ⊆ carrier G ∧ a divides (foldr (op ⊗) as \<one>)
--> (∃i. i < length as ∧ a divides (as!i))"

apply (induct as)
apply clarsimp defer 1
apply clarsimp defer 1
proof -
assume "a divides \<one>"
with carr
have "a ∈ Units G"
by (fast intro: divides_unit[of a \<one>])
with aprime
show "False" by (elim primeE, simp)
next
fix aa as
assume ih[rule_format]: "a divides foldr op ⊗ as \<one> --> (∃i<length as. a divides as ! i)"
and carr': "aa ∈ carrier G" "set as ⊆ carrier G"
and "a divides aa ⊗ foldr op ⊗ as \<one>"
with carr aprime
have "a divides aa ∨ a divides foldr op ⊗ as \<one>"
by (intro prime_divides) simp+
moreover {
assume "a divides aa"
hence p1: "a divides (aa#as)!0" by simp
have "0 < Suc (length as)" by simp
with p1 have "∃i<Suc (length as). a divides (aa # as) ! i" by fast
}
moreover {
assume "a divides foldr op ⊗ as \<one>"
hence "∃i. i < length as ∧ a divides as ! i" by (rule ih)
from this obtain i where "a divides as ! i" and len: "i < length as" by auto
hence p1: "a divides (aa#as) ! (Suc i)" by simp
from len have "Suc i < Suc (length as)" by simp
with p1 have "∃i<Suc (length as). a divides (aa # as) ! i" by force
}
ultimately
show "∃i<Suc (length as). a divides (aa # as) ! i" by fast
qed

from assms
show ?thesis
by (intro r, safe)
qed

lemma (in primeness_condition_monoid) wfactors_unique__hlp_induct:
"∀a as'. a ∈ carrier G ∧ set as ⊆ carrier G ∧ set as' ⊆ carrier G ∧
wfactors G as a ∧ wfactors G as' a --> essentially_equal G as as'"

proof (induct as)
case Nil show ?case apply auto
proof -
fix a as'
assume a: "a ∈ carrier G"
assume "wfactors G [] a"
then obtain "\<one> ∼ a" by (auto elim: wfactorsE)
with a have "a ∈ Units G" by (auto intro: assoc_unit_r)
moreover assume "wfactors G as' a"
moreover assume "set as' ⊆ carrier G"
ultimately have "as' = []" by (rule unit_wfactors_empty)
then show "essentially_equal G [] as'" by simp
qed
next
case (Cons ah as) then show ?case apply clarsimp
proof -
fix a as'
assume ih [rule_format]:
"∀a as'. a ∈ carrier G ∧ set as' ⊆ carrier G ∧ wfactors G as a ∧
wfactors G as' a --> essentially_equal G as as'"

and acarr: "a ∈ carrier G" and ahcarr: "ah ∈ carrier G"
and ascarr: "set as ⊆ carrier G" and as'carr: "set as' ⊆ carrier G"
and afs: "wfactors G (ah # as) a"
and afs': "wfactors G as' a"
hence ahdvda: "ah divides a"
by (intro wfactors_dividesI[of "ah#as" "a"], simp+)
hence "∃a'∈ carrier G. a = ah ⊗ a'" by (fast elim: dividesE)
from this obtain a'
where a'carr: "a' ∈ carrier G"
and a: "a = ah ⊗ a'"
by auto
have a'fs: "wfactors G as a'"
apply (rule wfactorsE[OF afs], rule wfactorsI, simp)
apply (simp add: a, insert ascarr a'carr)
apply (intro assoc_l_cancel[of ah _ a'] multlist_closed ahcarr, assumption+)
done
from afs have ahirr: "irreducible G ah" by (elim wfactorsE, simp)
with ascarr have ahprime: "prime G ah" by (intro irreducible_prime ahcarr)

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

note ahdvda
also from afs'
have "a divides (foldr (op ⊗) as' \<one>)"
by (elim wfactorsE associatedE, simp)
finally have "ah divides (foldr (op ⊗) as' \<one>)" by simp

with ahprime
have "∃i<length as'. ah divides as'!i"
by (intro multlist_prime_pos, simp+)
from this obtain i
where len: "i<length as'" and ahdvd: "ah divides as'!i"
by auto
from afs' carr have irrasi: "irreducible G (as'!i)"
by (fast intro: nth_mem[OF len] elim: wfactorsE)
from len carr
have asicarr[simp]: "as'!i ∈ carrier G" by (unfold set_conv_nth, force)
note carr = carr asicarr

from ahdvd have "∃x ∈ carrier G. as'!i = ah ⊗ x" by (fast elim: dividesE)
from this obtain x where "x ∈ carrier G" and asi: "as'!i = ah ⊗ x" by auto

with carr irrasi[simplified asi]
have asiah: "as'!i ∼ ah" apply -
apply (elim irreducible_prodE[of "ah" "x"], assumption+)
apply (rule associatedI2[of x], assumption+)
apply (rule irreducibleE[OF ahirr], simp)
done

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

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

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

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

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

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

from len
have as': "as' = (take i as' @ as'!i # drop (Suc i) as')"
by (simp add: drop_Suc_conv_tl)
with carr
have eer: "essentially_equal G (take i as' @ as'!i # drop (Suc i) as') as'"
by simp

with v2 afs' carr aa1carr aa2carr nth_mem[OF len]
have "aa_1 ⊗ (as'!i ⊗ aa_2) ∼ a"
apply (intro ee_wfactorsD[of "take i as' @ as'!i # drop (Suc i) as'" "as'"])
apply fast+
apply (simp, fast)
done
then
have t1: "as'!i ⊗ (aa_1 ⊗ aa_2) ∼ a"
apply (simp add: m_assoc[symmetric])
apply (simp add: m_comm)
done
from carr asiah
have "ah ⊗ (aa_1 ⊗ aa_2) ∼ as'!i ⊗ (aa_1 ⊗ aa_2)"
apply (intro mult_cong_l)
apply (fast intro: associated_sym, simp+)
done
also note t1
finally
have "ah ⊗ (aa_1 ⊗ aa_2) ∼ a" by simp

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

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

from a'fs this carr
have "essentially_equal G as (take i as' @ drop (Suc i) as')"
by (intro ih[of a']) simp

hence ee1: "essentially_equal G (ah # as) (ah # take i as' @ drop (Suc i) as')"
apply (elim essentially_equalE) apply (fastforce intro: essentially_equalI)
done

from carr
have ee2: "essentially_equal G (ah # take i as' @ drop (Suc i) as')
(as' ! i # take i as' @ drop (Suc i) as')"

proof (intro essentially_equalI)
show "ah # take i as' @ drop (Suc i) as' <~~> ah # take i as' @ drop (Suc i) as'"
by simp
next
show "ah # take i as' @ drop (Suc i) as' [∼] as' ! i # take i as' @ drop (Suc i) as'"
apply (simp add: list_all2_append)
apply (simp add: asiah[symmetric] ahcarr asicarr)
done
qed

note ee1
also note ee2
also have "essentially_equal G (as' ! i # take i as' @ drop (Suc i) as')
(take i as' @ as' ! i # drop (Suc i) as')"

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

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


subsubsection {* Application to factorial monoids *}

text {* Number of factors for wellfoundedness *}

definition
factorcount :: "_ => 'a => nat" where
"factorcount G a =
(THE c. (ALL 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"
apply (rule essentially_equalE[OF ee])
apply (metis list_all2_conv_all_nth perm_length)
done

lemma (in factorial_monoid) factorcount_exists:
assumes carr[simp]: "a ∈ carrier G"
shows "EX c. ALL 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)
from this obtain as
where ascarr[simp]: "set as ⊆ carrier G"
and afs: "wfactors G as a"
by (auto simp del: carr)

have "ALL as'. set as' ⊆ carrier G ∧ wfactors G as' a --> length as = length as'"
by (metis afs ascarr assms ee_length wfactors_unique)
thus "EX c. ALL as'. set as' ⊆ carrier G ∧ wfactors G as' a --> c = length as'" ..
qed

lemma (in factorial_monoid) factorcount_unique:
assumes afs: "wfactors G as a"
and acarr[simp]: "a ∈ carrier G" and ascarr[simp]: "set as ⊆ carrier G"
shows "factorcount G a = length as"
proof -
have "EX ac. ALL as. set as ⊆ carrier G ∧ wfactors G as a --> ac = length as" by (rule factorcount_exists, simp)
from this obtain ac where
alen: "ALL as. set as ⊆ carrier G ∧ wfactors G as a --> ac = length as"
by auto
have ac: "ac = factorcount G a"
apply (simp add: factorcount_def)
apply (rule theI2)
apply (rule alen)
apply (elim allE[of _ "as"], rule allE[OF alen, of "as"], simp add: ascarr afs)
apply (elim allE[of _ "as"], rule allE[OF alen, of "as"], simp add: ascarr afs)
done

from ascarr afs have "ac = length as" by (iprover intro: alen[rule_format])
with ac show ?thesis by simp
qed

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

assume ccarr: "c ∈ carrier G"
hence "∃cs. set cs ⊆ carrier G ∧ wfactors G cs c" by fast
from this obtain cs
where cscarr: "set cs ⊆ carrier G"
and cfs: "wfactors G cs c"
by auto

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+)
with b have "wfactors G (as@cs) b" by simp
hence "factorcount G b = length (as@cs)" by (intro factorcount_unique, simp+)
hence "factorcount G b = length as + length cs" by simp
with fca show ?thesis by simp
qed

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

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

assume ccarr: "c ∈ carrier G"
hence "∃cs. set cs ⊆ carrier G ∧ wfactors G cs c" by fast
from this obtain cs
where cscarr: "set cs ⊆ carrier G"
and cfs: "wfactors G cs c"
by auto

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)
hence fcb: "factorcount G b = length as + length cs" by simp

assume nbdvda: "¬ b divides a"
have "c ∉ Units G"
proof (rule ccontr, simp)
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 ⊗ \<one>" by (simp add: Units_r_inv)
also from acarr
have "… = a" by simp
finally have "a = b ⊗ inv c" by simp
with ccarr cunit
have "b divides a" by (fast intro: dividesI[of "inv c"])
with nbdvda show False by simp
qed

with cfs have "length cs > 0"
apply -
apply (rule ccontr, simp)
apply (metis Units_one_closed ccarr cscarr l_one one_closed properfactorI3 properfactor_fmset unit_wfactors)
done
with fca fcb show ?thesis by simp
qed

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

sublocale factorial_monoid primeness_condition_monoid
by default (rule irreducible_is_prime)


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

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

sublocale factorial_monoid gcd_condition_monoid
by default (rule gcdof_exists)

lemma (in factorial_monoid) division_weak_lattice [simp]:
shows "weak_lattice (division_rel G)"
proof -
interpret weak_lower_semilattice "division_rel G" by simp

show "weak_lattice (division_rel G)"
apply (unfold_locales, simp_all)
proof -
fix x y
assume carr: "x ∈ carrier G" "y ∈ carrier G"

hence "∃z. z ∈ carrier G ∧ z lcmof x y" by (rule lcmof_exists)
from this obtain z
where zcarr: "z ∈ carrier G"
and isgcd: "z lcmof x y"
by auto
with carr
have "least (division_rel G) z (Upper (division_rel G) {x, y})"
by (simp add: lcmof_leastUpper[symmetric])
thus "∃z. least (division_rel G) z (Upper (division_rel G) {x, y})" by fast
qed
qed


subsection {* Factoriality Theorems *}

theorem factorial_condition_one: (* Jacobson theorem 2.21 *)
shows "(divisor_chain_condition_monoid G ∧ primeness_condition_monoid G) =
factorial_monoid G"

apply rule
proof 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 fm: "factorial_monoid G"
interpret factorial_monoid "G" by (rule fm)
show "divisor_chain_condition_monoid G ∧ primeness_condition_monoid G"
by rule unfold_locales
qed

theorem factorial_condition_two: (* Jacobson theorem 2.22 *)
shows "(divisor_chain_condition_monoid G ∧ gcd_condition_monoid G) = factorial_monoid G"
apply rule
proof 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 fm: "factorial_monoid G"
interpret factorial_monoid "G" by (rule fm)
show "divisor_chain_condition_monoid G ∧ gcd_condition_monoid G"
by rule unfold_locales
qed

end