(* 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 divides⇘_{G⇙}b <-> (∃c∈carrier G. b = a ⊗⇘_{G⇙}c)"

definition

associated :: "[_, 'a, 'a] => bool" (infix "∼\<index>" 55)

where "a ∼⇘_{G⇙}b <-> a divides⇘_{G⇙}b ∧ b divides⇘_{G⇙}a"

abbreviation

"division_rel G == (|carrier = carrier G, eq = op ∼⇘_{G⇙}, le = op divides⇘_{G⇙}|)),"

definition

properfactor :: "[_, 'a, 'a] => bool"

where "properfactor G a b <-> a divides⇘_{G⇙}b ∧ ¬(b divides⇘_{G⇙}a)"

definition

irreducible :: "[_, 'a] => bool"

where "irreducible G a <-> a ∉ Units G ∧ (∀b∈carrier G. properfactor G b a --> b ∈ Units G)"

definition

prime :: "[_, 'a] => bool" where

"prime G p <->

p ∉ Units G ∧

(∀a∈carrier G. ∀b∈carrier G. p divides⇘_{G⇙}(a ⊗⇘_{G⇙}b) --> p divides⇘_{G⇙}a ∨ p divides⇘_{G⇙}b)"

subsubsection {* Divisibility *}

lemma dividesI:

fixes G (structure)

assumes carr: "c ∈ carrier G"

and p: "b = a ⊗ c"

shows "a divides b"

unfolding factor_def

using assms by fast

lemma dividesI' [intro]:

fixes G (structure)

assumes p: "b = a ⊗ c"

and carr: "c ∈ carrier G"

shows "a divides b"

using assms

by (fast intro: dividesI)

lemma dividesD:

fixes G (structure)

assumes "a divides b"

shows "∃c∈carrier G. b = a ⊗ c"

using assms

unfolding factor_def

by fast

lemma dividesE [elim]:

fixes G (structure)

assumes d: "a divides b"

and elim: "!!c. [|b = a ⊗ c; c ∈ carrier G|] ==> P"

shows "P"

proof -

from dividesD[OF d]

obtain c

where "c∈carrier G"

and "b = a ⊗ c"

by auto

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>⇘_{G⇙}∼⇘_{G⇙}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 gcdof⇘_{G⇙}a b <-> x divides⇘_{G⇙}a ∧ x divides⇘_{G⇙}b ∧

(∀y∈carrier G. (y divides⇘_{G⇙}a ∧ y divides⇘_{G⇙}b --> y divides⇘_{G⇙}x))"

definition

islcm :: "[_, 'a, 'a, 'a] => bool" ("(_ lcmof\<index> _ _)" [81,81,81] 80)

where "x lcmof⇘_{G⇙}a b <-> a divides⇘_{G⇙}x ∧ b divides⇘_{G⇙}x ∧

(∀y∈carrier G. (a divides⇘_{G⇙}y ∧ b divides⇘_{G⇙}y --> x divides⇘_{G⇙}y))"

definition

somegcd :: "('a,_) monoid_scheme => 'a => 'a => 'a"

where "somegcd G a b = (SOME x. x ∈ carrier G ∧ x gcdof⇘_{G⇙}a b)"

definition

somelcm :: "('a,_) monoid_scheme => 'a => 'a => 'a"

where "somelcm G a b = (SOME x. x ∈ carrier G ∧ x lcmof⇘_{G⇙}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