Theory Divisibility
section ‹Divisibility in monoids and rings›
theory Divisibility
imports "HOL-Combinatorics.List_Permutation" Coset Group
begin
section ‹Factorial Monoids›
subsection ‹Monoids with Cancellation Law›
locale monoid_cancel = monoid +
assumes l_cancel: "⟦c ⊗ a = c ⊗ b; a ∈ carrier G; b ∈ carrier G; c ∈ carrier G⟧ ⟹ a = b"
and r_cancel: "⟦a ⊗ c = b ⊗ c; a ∈ carrier G; b ∈ carrier G; c ∈ carrier G⟧ ⟹ a = b"
lemma (in monoid) monoid_cancelI:
assumes l_cancel: "⋀a b c. ⟦c ⊗ a = c ⊗ b; a ∈ carrier G; b ∈ carrier G; c ∈ carrier G⟧ ⟹ a = b"
and r_cancel: "⋀a b c. ⟦a ⊗ c = b ⊗ c; a ∈ carrier G; b ∈ carrier G; c ∈ carrier G⟧ ⟹ a = b"
shows "monoid_cancel G"
by standard fact+
lemma (in monoid_cancel) is_monoid_cancel: "monoid_cancel G" ..
sublocale group ⊆ monoid_cancel
by standard simp_all
locale comm_monoid_cancel = monoid_cancel + comm_monoid
lemma comm_monoid_cancelI:
fixes G (structure)
assumes "comm_monoid G"
assumes cancel: "⋀a b c. ⟦a ⊗ c = b ⊗ c; a ∈ carrier G; b ∈ carrier G; c ∈ carrier G⟧ ⟹ a = b"
shows "comm_monoid_cancel G"
proof -
interpret comm_monoid G by fact
show "comm_monoid_cancel G"
by unfold_locales (metis assms(2) m_ac(2))+
qed
lemma (in comm_monoid_cancel) is_comm_monoid_cancel: "comm_monoid_cancel G"
by intro_locales
sublocale comm_group ⊆ comm_monoid_cancel ..
subsection ‹Products of Units in Monoids›
lemma (in monoid) prod_unit_l:
assumes abunit[simp]: "a ⊗ b ∈ Units G"
and aunit[simp]: "a ∈ Units G"
and carr[simp]: "a ∈ carrier G" "b ∈ carrier G"
shows "b ∈ Units G"
proof -
have c: "inv (a ⊗ b) ⊗ a ∈ carrier G" by simp
have "(inv (a ⊗ b) ⊗ a) ⊗ b = inv (a ⊗ b) ⊗ (a ⊗ b)"
by (simp add: m_assoc)
also have "… = 𝟭" by simp
finally have li: "(inv (a ⊗ b) ⊗ a) ⊗ b = 𝟭" .
have "𝟭 = inv a ⊗ a" by (simp add: Units_l_inv[symmetric])
also have "… = inv a ⊗ 𝟭 ⊗ a" by simp
also have "… = inv a ⊗ ((a ⊗ b) ⊗ inv (a ⊗ b)) ⊗ a"
by (simp add: Units_r_inv[OF abunit, symmetric] del: Units_r_inv)
also have "… = ((inv a ⊗ a) ⊗ b) ⊗ inv (a ⊗ b) ⊗ a"
by (simp add: m_assoc del: Units_l_inv)
also have "… = b ⊗ inv (a ⊗ b) ⊗ a" by simp
also have "… = b ⊗ (inv (a ⊗ b) ⊗ a)" by (simp add: m_assoc)
finally have ri: "b ⊗ (inv (a ⊗ b) ⊗ a) = 𝟭 " by simp
from c li ri show "b ∈ Units G" by (auto simp: Units_def)
qed
lemma (in monoid) prod_unit_r:
assumes abunit[simp]: "a ⊗ b ∈ Units G"
and bunit[simp]: "b ∈ Units G"
and carr[simp]: "a ∈ carrier G" "b ∈ carrier G"
shows "a ∈ Units G"
proof -
have c: "b ⊗ inv (a ⊗ b) ∈ carrier G" by simp
have "a ⊗ (b ⊗ inv (a ⊗ b)) = (a ⊗ b) ⊗ inv (a ⊗ b)"
by (simp add: m_assoc del: Units_r_inv)
also have "… = 𝟭" by simp
finally have li: "a ⊗ (b ⊗ inv (a ⊗ b)) = 𝟭" .
have "𝟭 = b ⊗ inv b" by (simp add: Units_r_inv[symmetric])
also have "… = b ⊗ 𝟭 ⊗ inv b" by simp
also have "… = b ⊗ (inv (a ⊗ b) ⊗ (a ⊗ b)) ⊗ inv b"
by (simp add: Units_l_inv[OF abunit, symmetric] del: Units_l_inv)
also have "… = (b ⊗ inv (a ⊗ b) ⊗ a) ⊗ (b ⊗ inv b)"
by (simp add: m_assoc del: Units_l_inv)
also have "… = b ⊗ inv (a ⊗ b) ⊗ a" by simp
finally have ri: "(b ⊗ inv (a ⊗ b)) ⊗ a = 𝟭 " by simp
from c li ri show "a ∈ Units G" by (auto simp: Units_def)
qed
lemma (in comm_monoid) unit_factor:
assumes abunit: "a ⊗ b ∈ Units G"
and [simp]: "a ∈ carrier G" "b ∈ carrier G"
shows "a ∈ Units G"
using abunit[simplified Units_def]
proof clarsimp
fix i
assume [simp]: "i ∈ carrier G"
have carr': "b ⊗ i ∈ carrier G" by simp
have "(b ⊗ i) ⊗ a = (i ⊗ b) ⊗ a" by (simp add: m_comm)
also have "… = i ⊗ (b ⊗ a)" by (simp add: m_assoc)
also have "… = i ⊗ (a ⊗ b)" by (simp add: m_comm)
also assume "i ⊗ (a ⊗ b) = 𝟭"
finally have li': "(b ⊗ i) ⊗ a = 𝟭" .
have "a ⊗ (b ⊗ i) = a ⊗ b ⊗ i" by (simp add: m_assoc)
also assume "a ⊗ b ⊗ i = 𝟭"
finally have ri': "a ⊗ (b ⊗ i) = 𝟭" .
from carr' li' ri'
show "a ∈ Units G" by (simp add: Units_def, fast)
qed
subsection ‹Divisibility and Association›
subsubsection ‹Function definitions›
definition factor :: "[_, 'a, 'a] ⇒ bool" (infix "dividesı" 65)
where "a divides⇘G⇙ b ⟷ (∃c∈carrier G. b = a ⊗⇘G⇙ c)"
definition associated :: "[_, 'a, 'a] ⇒ bool" (infix "∼ı" 55)
where "a ∼⇘G⇙ b ⟷ a divides⇘G⇙ b ∧ b divides⇘G⇙ a"
abbreviation "division_rel G ≡ ⦇carrier = carrier G, eq = (∼⇘G⇙), le = (divides⇘G⇙)⦈"
definition properfactor :: "[_, 'a, 'a] ⇒ bool"
where "properfactor G a b ⟷ a divides⇘G⇙ b ∧ ¬(b divides⇘G⇙ a)"
definition irreducible :: "[_, 'a] ⇒ bool"
where "irreducible G a ⟷ a ∉ Units G ∧ (∀b∈carrier G. properfactor G b a ⟶ b ∈ Units G)"
definition prime :: "[_, 'a] ⇒ bool"
where "prime G p ⟷
p ∉ Units G ∧
(∀a∈carrier G. ∀b∈carrier G. p divides⇘G⇙ (a ⊗⇘G⇙ b) ⟶ p divides⇘G⇙ a ∨ p divides⇘G⇙ b)"
subsubsection ‹Divisibility›
lemma dividesI:
fixes G (structure)
assumes carr: "c ∈ carrier G"
and p: "b = a ⊗ c"
shows "a divides b"
unfolding factor_def using assms by fast
lemma dividesI' [intro]:
fixes G (structure)
assumes p: "b = a ⊗ c"
and carr: "c ∈ carrier G"
shows "a divides b"
using assms by (fast intro: dividesI)
lemma dividesD:
fixes G (structure)
assumes "a divides b"
shows "∃c∈carrier G. b = a ⊗ c"
using assms unfolding factor_def by fast
lemma dividesE [elim]:
fixes G (structure)
assumes d: "a divides b"
and elim: "⋀c. ⟦b = a ⊗ c; c ∈ carrier G⟧ ⟹ P"
shows "P"
proof -
from dividesD[OF d] obtain c where "c ∈ carrier G" and "b = a ⊗ c" by auto
then show P by (elim elim)
qed
lemma (in monoid) divides_refl[simp, intro!]:
assumes carr: "a ∈ carrier G"
shows "a divides a"
by (intro dividesI[of "𝟭"]) (simp_all add: carr)
lemma (in monoid) divides_trans [trans]:
assumes dvds: "a divides b" "b divides c"
and acarr: "a ∈ carrier G"
shows "a divides c"
using dvds[THEN dividesD] by (blast intro: dividesI m_assoc acarr)
lemma (in monoid) divides_mult_lI [intro]:
assumes "a divides b" "a ∈ carrier G" "c ∈ carrier G"
shows "(c ⊗ a) divides (c ⊗ b)"
by (metis assms factor_def m_assoc)
lemma (in monoid_cancel) divides_mult_l [simp]:
assumes carr: "a ∈ carrier G" "b ∈ carrier G" "c ∈ carrier G"
shows "(c ⊗ a) divides (c ⊗ b) = a divides b"
proof
show "c ⊗ a divides c ⊗ b ⟹ a divides b"
using carr monoid.m_assoc monoid_axioms monoid_cancel.l_cancel monoid_cancel_axioms by fastforce
show "a divides b ⟹ c ⊗ a divides c ⊗ b"
using carr(1) carr(3) by blast
qed
lemma (in comm_monoid) divides_mult_rI [intro]:
assumes ab: "a divides b"
and carr: "a ∈ carrier G" "b ∈ carrier G" "c ∈ carrier G"
shows "(a ⊗ c) divides (b ⊗ c)"
using carr ab by (metis divides_mult_lI m_comm)
lemma (in comm_monoid_cancel) divides_mult_r [simp]:
assumes carr: "a ∈ carrier G" "b ∈ carrier G" "c ∈ carrier G"
shows "(a ⊗ c) divides (b ⊗ c) = a divides b"
using carr by (simp add: m_comm[of a c] m_comm[of b c])
lemma (in monoid) divides_prod_r:
assumes ab: "a divides b"
and carr: "a ∈ carrier G" "c ∈ carrier G"
shows "a divides (b ⊗ c)"
using ab carr by (fast intro: m_assoc)
lemma (in comm_monoid) divides_prod_l:
assumes "a ∈ carrier G" "b ∈ carrier G" "c ∈ carrier G" "a divides b"
shows "a divides (c ⊗ b)"
using assms by (simp add: divides_prod_r m_comm)
lemma (in monoid) unit_divides:
assumes uunit: "u ∈ Units G"
and acarr: "a ∈ carrier G"
shows "u divides a"
proof (intro dividesI[of "(inv u) ⊗ a"], fast intro: uunit acarr)
from uunit acarr have xcarr: "inv u ⊗ a ∈ carrier G" by fast
from uunit acarr have "u ⊗ (inv u ⊗ a) = (u ⊗ inv u) ⊗ a"
by (fast intro: m_assoc[symmetric])
also have "… = 𝟭 ⊗ a" by (simp add: Units_r_inv[OF uunit])
also from acarr have "… = a" by simp
finally show "a = u ⊗ (inv u ⊗ a)" ..
qed
lemma (in comm_monoid) divides_unit:
assumes udvd: "a divides u"
and carr: "a ∈ carrier G" "u ∈ Units G"
shows "a ∈ Units G"
using udvd carr by (blast intro: unit_factor)
lemma (in comm_monoid) Unit_eq_dividesone:
assumes ucarr: "u ∈ carrier G"
shows "u ∈ Units G = u divides 𝟭"
using ucarr by (fast dest: divides_unit intro: unit_divides)
subsubsection ‹Association›
lemma associatedI:
fixes G (structure)
assumes "a divides b" "b divides a"
shows "a ∼ b"
using assms by (simp add: associated_def)
lemma (in monoid) associatedI2:
assumes uunit[simp]: "u ∈ Units G"
and a: "a = b ⊗ u"
and bcarr: "b ∈ carrier G"
shows "a ∼ b"
using uunit bcarr
unfolding a
apply (intro associatedI)
apply (metis Units_closed divides_mult_lI one_closed r_one unit_divides)
by blast
lemma (in monoid) associatedI2':
assumes "a = b ⊗ u"
and "u ∈ Units G"
and "b ∈ carrier G"
shows "a ∼ b"
using assms by (intro associatedI2)
lemma associatedD:
fixes G (structure)
assumes "a ∼ b"
shows "a divides b"
using assms by (simp add: associated_def)
lemma (in monoid_cancel) associatedD2:
assumes assoc: "a ∼ b"
and carr: "a ∈ carrier G" "b ∈ carrier G"
shows "∃u∈Units G. a = b ⊗ u"
using assoc
unfolding associated_def
proof clarify
assume "b divides a"
then obtain u where ucarr: "u ∈ carrier G" and a: "a = b ⊗ u"
by (rule dividesE)
assume "a divides b"
then obtain u' where u'carr: "u' ∈ carrier G" and b: "b = a ⊗ u'"
by (rule dividesE)
note carr = carr ucarr u'carr
from carr have "a ⊗ 𝟭 = a" by simp
also have "… = b ⊗ u" by (simp add: a)
also have "… = a ⊗ u' ⊗ u" by (simp add: b)
also from carr have "… = a ⊗ (u' ⊗ u)" by (simp add: m_assoc)
finally have "a ⊗ 𝟭 = a ⊗ (u' ⊗ u)" .
with carr have u1: "𝟭 = u' ⊗ u" by (fast dest: l_cancel)
from carr have "b ⊗ 𝟭 = b" by simp
also have "… = a ⊗ u'" by (simp add: b)
also have "… = b ⊗ u ⊗ u'" by (simp add: a)
also from carr have "… = b ⊗ (u ⊗ u')" by (simp add: m_assoc)
finally have "b ⊗ 𝟭 = b ⊗ (u ⊗ u')" .
with carr have u2: "𝟭 = u ⊗ u'" by (fast dest: l_cancel)
from u'carr u1[symmetric] u2[symmetric] have "∃u'∈carrier G. u' ⊗ u = 𝟭 ∧ u ⊗ u' = 𝟭"
by fast
then have "u ∈ Units G"
by (simp add: Units_def ucarr)
with ucarr a show "∃u∈Units G. a = b ⊗ u" by fast
qed
lemma associatedE:
fixes G (structure)
assumes assoc: "a ∼ b"
and e: "⟦a divides b; b divides a⟧ ⟹ P"
shows "P"
proof -
from assoc have "a divides b" "b divides a"
by (simp_all add: associated_def)
then show P by (elim e)
qed
lemma (in monoid_cancel) associatedE2:
assumes assoc: "a ∼ b"
and e: "⋀u. ⟦a = b ⊗ u; u ∈ Units G⟧ ⟹ P"
and carr: "a ∈ carrier G" "b ∈ carrier G"
shows "P"
proof -
from assoc and carr have "∃u∈Units G. a = b ⊗ u"
by (rule associatedD2)
then obtain u where "u ∈ Units G" "a = b ⊗ u"
by auto
then show P by (elim e)
qed
lemma (in monoid) associated_refl [simp, intro!]:
assumes "a ∈ carrier G"
shows "a ∼ a"
using assms by (fast intro: associatedI)
lemma (in monoid) associated_sym [sym]:
assumes "a ∼ b"
shows "b ∼ a"
using assms by (iprover intro: associatedI elim: associatedE)
lemma (in monoid) associated_trans [trans]:
assumes "a ∼ b" "b ∼ c"
and "a ∈ carrier G" "c ∈ carrier G"
shows "a ∼ c"
using assms by (iprover intro: associatedI divides_trans elim: associatedE)
lemma (in monoid) division_equiv [intro, simp]: "equivalence (division_rel G)"
apply unfold_locales
apply simp_all
apply (metis associated_def)
apply (iprover intro: associated_trans)
done
subsubsection ‹Division and associativity›
lemmas divides_antisym = associatedI
lemma (in monoid) divides_cong_l [trans]:
assumes "x ∼ x'" "x' divides y" "x ∈ carrier G"
shows "x divides y"
by (meson assms associatedD divides_trans)
lemma (in monoid) divides_cong_r [trans]:
assumes "x divides y" "y ∼ y'" "x ∈ carrier G"
shows "x divides y'"
by (meson assms associatedD divides_trans)
lemma (in monoid) division_weak_partial_order [simp, intro!]:
"weak_partial_order (division_rel G)"
apply unfold_locales
apply (simp_all add: associated_sym divides_antisym)
apply (metis associated_trans)
apply (metis divides_trans)
by (meson associated_def divides_trans)
subsubsection ‹Multiplication and associativity›
lemma (in monoid) mult_cong_r:
assumes "b ∼ b'" "a ∈ carrier G" "b ∈ carrier G" "b' ∈ carrier G"
shows "a ⊗ b ∼ a ⊗ b'"
by (meson assms associated_def divides_mult_lI)
lemma (in comm_monoid) mult_cong_l:
assumes "a ∼ a'" "a ∈ carrier G" "a' ∈ carrier G" "b ∈ carrier G"
shows "a ⊗ b ∼ a' ⊗ b"
using assms m_comm mult_cong_r by auto
lemma (in monoid_cancel) assoc_l_cancel:
assumes "a ∈ carrier G" "b ∈ carrier G" "b' ∈ carrier G" "a ⊗ b ∼ a ⊗ b'"
shows "b ∼ b'"
by (meson assms associated_def divides_mult_l)
lemma (in comm_monoid_cancel) assoc_r_cancel:
assumes "a ⊗ b ∼ a' ⊗ b" "a ∈ carrier G" "a' ∈ carrier G" "b ∈ carrier G"
shows "a ∼ a'"
using assms assoc_l_cancel m_comm by presburger
subsubsection ‹Units›
lemma (in monoid_cancel) assoc_unit_l [trans]:
assumes "a ∼ b"
and "b ∈ Units G"
and "a ∈ carrier G"
shows "a ∈ Units G"
using assms by (fast elim: associatedE2)
lemma (in monoid_cancel) assoc_unit_r [trans]:
assumes aunit: "a ∈ Units G"
and asc: "a ∼ b"
and bcarr: "b ∈ carrier G"
shows "b ∈ Units G"
using aunit bcarr associated_sym[OF asc] by (blast intro: assoc_unit_l)
lemma (in comm_monoid) Units_cong:
assumes aunit: "a ∈ Units G" and asc: "a ∼ b"
and bcarr: "b ∈ carrier G"
shows "b ∈ Units G"
using assms by (blast intro: divides_unit elim: associatedE)
lemma (in monoid) Units_assoc:
assumes units: "a ∈ Units G" "b ∈ Units G"
shows "a ∼ b"
using units by (fast intro: associatedI unit_divides)
lemma (in monoid) Units_are_ones: "Units G {.=}⇘(division_rel G)⇙ {𝟭}"
proof -
have "a .∈⇘division_rel G⇙ {𝟭}" if "a ∈ Units G" for a
proof -
have "a ∼ 𝟭"
by (rule associatedI) (simp_all add: Units_closed that unit_divides)
then show ?thesis
by (simp add: elem_def)
qed
moreover have "𝟭 .∈⇘division_rel G⇙ Units G"
by (simp add: equivalence.mem_imp_elem)
ultimately show ?thesis
by (auto simp: set_eq_def)
qed
lemma (in comm_monoid) Units_Lower: "Units G = Lower (division_rel G) (carrier G)"
apply (auto simp add: Units_def Lower_def)
apply (metis Units_one_closed unit_divides unit_factor)
apply (metis Unit_eq_dividesone Units_r_inv_ex m_ac(2) one_closed)
done
lemma (in monoid_cancel) associated_iff:
assumes "a ∈ carrier G" "b ∈ carrier G"
shows "a ∼ b ⟷ (∃c ∈ Units G. a = b ⊗ c)"
using assms associatedI2' associatedD2 by auto
subsubsection ‹Proper factors›
lemma properfactorI:
fixes G (structure)
assumes "a divides b"
and "¬(b divides a)"
shows "properfactor G a b"
using assms unfolding properfactor_def by simp
lemma properfactorI2:
fixes G (structure)
assumes advdb: "a divides b"
and neq: "¬(a ∼ b)"
shows "properfactor G a b"
proof (rule properfactorI, rule advdb, rule notI)
assume "b divides a"
with advdb have "a ∼ b" by (rule associatedI)
with neq show "False" by fast
qed
lemma (in comm_monoid_cancel) properfactorI3:
assumes p: "p = a ⊗ b"
and nunit: "b ∉ Units G"
and carr: "a ∈ carrier G" "b ∈ carrier G"
shows "properfactor G a p"
unfolding p
using carr
apply (intro properfactorI, fast)
proof (clarsimp, elim dividesE)
fix c
assume ccarr: "c ∈ carrier G"
note [simp] = carr ccarr
have "a ⊗ 𝟭 = a" by simp
also assume "a = a ⊗ b ⊗ c"
also have "… = a ⊗ (b ⊗ c)" by (simp add: m_assoc)
finally have "a ⊗ 𝟭 = a ⊗ (b ⊗ c)" .
then have rinv: "𝟭 = b ⊗ c" by (intro l_cancel[of "a" "𝟭" "b ⊗ c"], simp+)
also have "… = c ⊗ b" by (simp add: m_comm)
finally have linv: "𝟭 = c ⊗ b" .
from ccarr linv[symmetric] rinv[symmetric] have "b ∈ Units G"
unfolding Units_def by fastforce
with nunit show False ..
qed
lemma properfactorE:
fixes G (structure)
assumes pf: "properfactor G a b"
and r: "⟦a divides b; ¬(b divides a)⟧ ⟹ P"
shows "P"
using pf unfolding properfactor_def by (fast intro: r)
lemma properfactorE2:
fixes G (structure)
assumes pf: "properfactor G a b"
and elim: "⟦a divides b; ¬(a ∼ b)⟧ ⟹ P"
shows "P"
using pf unfolding properfactor_def by (fast elim: elim associatedE)
lemma (in monoid) properfactor_unitE:
assumes uunit: "u ∈ Units G"
and pf: "properfactor G a u"
and acarr: "a ∈ carrier G"
shows "P"
using pf unit_divides[OF uunit acarr] by (fast elim: properfactorE)
lemma (in monoid) properfactor_divides:
assumes pf: "properfactor G a b"
shows "a divides b"
using pf by (elim properfactorE)
lemma (in monoid) properfactor_trans1 [trans]:
assumes "a divides b" "properfactor G b c" "a ∈ carrier G" "c ∈ carrier G"
shows "properfactor G a c"
by (meson divides_trans properfactorE properfactorI assms)
lemma (in monoid) properfactor_trans2 [trans]:
assumes "properfactor G a b" "b divides c" "a ∈ carrier G" "b ∈ carrier G"
shows "properfactor G a c"
by (meson divides_trans properfactorE properfactorI assms)
lemma properfactor_lless:
fixes G (structure)
shows "properfactor G = lless (division_rel G)"
by (force simp: lless_def properfactor_def associated_def)
lemma (in monoid) properfactor_cong_l [trans]:
assumes x'x: "x' ∼ x"
and pf: "properfactor G x y"
and carr: "x ∈ carrier G" "x' ∈ carrier G" "y ∈ carrier G"
shows "properfactor G x' y"
using pf
unfolding properfactor_lless
proof -
interpret weak_partial_order "division_rel G" ..
from x'x have "x' .=⇘division_rel G⇙ x" by simp
also assume "x ⊏⇘division_rel G⇙ y"
finally show "x' ⊏⇘division_rel G⇙ y" by (simp add: carr)
qed
lemma (in monoid) properfactor_cong_r [trans]:
assumes pf: "properfactor G x y"
and yy': "y ∼ y'"
and carr: "x ∈ carrier G" "y ∈ carrier G" "y' ∈ carrier G"
shows "properfactor G x y'"
using pf
unfolding properfactor_lless
proof -
interpret weak_partial_order "division_rel G" ..
assume "x ⊏⇘division_rel G⇙ y"
also from yy'
have "y .=⇘division_rel G⇙ y'" by simp
finally show "x ⊏⇘division_rel G⇙ y'" by (simp add: carr)
qed
lemma (in monoid_cancel) properfactor_mult_lI [intro]:
assumes ab: "properfactor G a b"
and carr: "a ∈ carrier G" "c ∈ carrier G"
shows "properfactor G (c ⊗ a) (c ⊗ b)"
using ab carr by (fastforce elim: properfactorE intro: properfactorI)
lemma (in monoid_cancel) properfactor_mult_l [simp]:
assumes carr: "a ∈ carrier G" "b ∈ carrier G" "c ∈ carrier G"
shows "properfactor G (c ⊗ a) (c ⊗ b) = properfactor G a b"
using carr by (fastforce elim: properfactorE intro: properfactorI)
lemma (in comm_monoid_cancel) properfactor_mult_rI [intro]:
assumes ab: "properfactor G a b"
and carr: "a ∈ carrier G" "c ∈ carrier G"
shows "properfactor G (a ⊗ c) (b ⊗ c)"
using ab carr by (fastforce elim: properfactorE intro: properfactorI)
lemma (in comm_monoid_cancel) properfactor_mult_r [simp]:
assumes carr: "a ∈ carrier G" "b ∈ carrier G" "c ∈ carrier G"
shows "properfactor G (a ⊗ c) (b ⊗ c) = properfactor G a b"
using carr by (fastforce elim: properfactorE intro: properfactorI)
lemma (in monoid) properfactor_prod_r:
assumes ab: "properfactor G a b"
and carr[simp]: "a ∈ carrier G" "b ∈ carrier G" "c ∈ carrier G"
shows "properfactor G a (b ⊗ c)"
by (intro properfactor_trans2[OF ab] divides_prod_r) simp_all
lemma (in comm_monoid) properfactor_prod_l:
assumes ab: "properfactor G a b"
and carr[simp]: "a ∈ carrier G" "b ∈ carrier G" "c ∈ carrier G"
shows "properfactor G a (c ⊗ b)"
by (intro properfactor_trans2[OF ab] divides_prod_l) simp_all
subsection ‹Irreducible Elements and Primes›
subsubsection ‹Irreducible elements›
lemma irreducibleI:
fixes G (structure)
assumes "a ∉ Units G"
and "⋀b. ⟦b ∈ carrier G; properfactor G b a⟧ ⟹ b ∈ Units G"
shows "irreducible G a"
using assms unfolding irreducible_def by blast
lemma irreducibleE:
fixes G (structure)
assumes irr: "irreducible G a"
and elim: "⟦a ∉ Units G; ∀b. b ∈ carrier G ∧ properfactor G b a ⟶ b ∈ Units G⟧ ⟹ P"
shows "P"
using assms unfolding irreducible_def by blast
lemma irreducibleD:
fixes G (structure)
assumes irr: "irreducible G a"
and pf: "properfactor G b a"
and bcarr: "b ∈ carrier G"
shows "b ∈ Units G"
using assms by (fast elim: irreducibleE)
lemma (in monoid_cancel) irreducible_cong [trans]:
assumes "irreducible G a" "a ∼ a'" "a ∈ carrier G" "a' ∈ carrier G"
shows "irreducible G a'"
proof -
have "a' divides a"
by (meson ‹a ∼ a'› associated_def)
then show ?thesis
by (metis (no_types) assms assoc_unit_l irreducibleE irreducibleI monoid.properfactor_trans2 monoid_axioms)
qed
lemma (in monoid) irreducible_prod_rI:
assumes "irreducible G a" "b ∈ Units G" "a ∈ carrier G" "b ∈ carrier G"
shows "irreducible G (a ⊗ b)"
using assms
by (metis (no_types, lifting) associatedI2' irreducible_def monoid.m_closed monoid_axioms prod_unit_r properfactor_cong_r)
lemma (in comm_monoid) irreducible_prod_lI:
assumes birr: "irreducible G b"
and aunit: "a ∈ Units G"
and carr [simp]: "a ∈ carrier G" "b ∈ carrier G"
shows "irreducible G (a ⊗ b)"
by (metis aunit birr carr irreducible_prod_rI m_comm)
lemma (in comm_monoid_cancel) irreducible_prodE [elim]:
assumes irr: "irreducible G (a ⊗ b)"
and carr[simp]: "a ∈ carrier G" "b ∈ carrier G"
and e1: "⟦irreducible G a; b ∈ Units G⟧ ⟹ P"
and e2: "⟦a ∈ Units G; irreducible G b⟧ ⟹ P"
shows P
using irr
proof (elim irreducibleE)
assume abnunit: "a ⊗ b ∉ Units G"
and isunit[rule_format]: "∀ba. ba ∈ carrier G ∧ properfactor G ba (a ⊗ b) ⟶ ba ∈ Units G"
show P
proof (cases "a ∈ Units G")
case aunit: True
have "irreducible G b"
proof (rule irreducibleI, rule notI)
assume "b ∈ Units G"
with aunit have "(a ⊗ b) ∈ Units G" by fast
with abnunit show "False" ..
next
fix c
assume ccarr: "c ∈ carrier G"
and "properfactor G c b"
then have "properfactor G c (a ⊗ b)" by (simp add: properfactor_prod_l[of c b a])
with ccarr show "c ∈ Units G" by (fast intro: isunit)
qed
with aunit show "P" by (rule e2)
next
case anunit: False
with carr have "properfactor G b (b ⊗ a)" by (fast intro: properfactorI3)
then have bf: "properfactor G b (a ⊗ b)" by (subst m_comm[of a b], simp+)
then have bunit: "b ∈ Units G" by (intro isunit, simp)
have "irreducible G a"
proof (rule irreducibleI, rule notI)
assume "a ∈ Units G"
with bunit have "(a ⊗ b) ∈ Units G" by fast
with abnunit show "False" ..
next
fix c
assume ccarr: "c ∈ carrier G"
and "properfactor G c a"
then have "properfactor G c (a ⊗ b)"
by (simp add: properfactor_prod_r[of c a b])
with ccarr show "c ∈ Units G" by (fast intro: isunit)
qed
from this bunit show "P" by (rule e1)
qed
qed
lemma divides_irreducible_condition:
assumes "irreducible G r" and "a ∈ carrier G"
shows "a divides⇘G⇙ r ⟹ a ∈ Units G ∨ a ∼⇘G⇙ r"
using assms unfolding irreducible_def properfactor_def associated_def
by (cases "r divides⇘G⇙ a", auto)
subsubsection ‹Prime elements›
lemma primeI:
fixes G (structure)
assumes "p ∉ Units G"
and "⋀a b. ⟦a ∈ carrier G; b ∈ carrier G; p divides (a ⊗ b)⟧ ⟹ p divides a ∨ p divides b"
shows "prime G p"
using assms unfolding prime_def by blast
lemma primeE:
fixes G (structure)
assumes pprime: "prime G p"
and e: "⟦p ∉ Units G; ∀a∈carrier G. ∀b∈carrier G.
p divides a ⊗ b ⟶ p divides a ∨ p divides b⟧ ⟹ P"
shows "P"
using pprime unfolding prime_def by (blast dest: e)
lemma (in comm_monoid_cancel) prime_divides:
assumes carr: "a ∈ carrier G" "b ∈ carrier G"
and pprime: "prime G p"
and pdvd: "p divides a ⊗ b"
shows "p divides a ∨ p divides b"
using assms by (blast elim: primeE)
lemma (in monoid_cancel) prime_cong [trans]:
assumes "prime G p"
and pp': "p ∼ p'" "p ∈ carrier G" "p' ∈ carrier G"
shows "prime G p'"
using assms
by (auto simp: prime_def assoc_unit_l) (metis pp' associated_sym divides_cong_l)
lemma (in comm_monoid_cancel) prime_irreducible:
assumes "prime G p"
shows "irreducible G p"
proof (rule irreducibleI)
show "p ∉ Units G"
using assms unfolding prime_def by simp
next
fix b assume A: "b ∈ carrier G" "properfactor G b p"
then obtain c where c: "c ∈ carrier G" "p = b ⊗ c"
unfolding properfactor_def factor_def by auto
hence "p divides c"
using A assms unfolding prime_def properfactor_def by auto
then obtain b' where b': "b' ∈ carrier G" "c = p ⊗ b'"
unfolding factor_def by auto
hence "𝟭 = b ⊗ b'"
by (metis A(1) l_cancel m_closed m_lcomm one_closed r_one c)
thus "b ∈ Units G"
using A(1) Units_one_closed b'(1) unit_factor by presburger
qed
lemma (in comm_monoid_cancel) prime_pow_divides_iff:
assumes "p ∈ carrier G" "a ∈ carrier G" "b ∈ carrier G" and "prime G p" and "¬ (p divides a)"
shows "(p [^] (n :: nat)) divides (a ⊗ b) ⟷ (p [^] n) divides b"
proof
assume "(p [^] n) divides b" thus "(p [^] n) divides (a ⊗ b)"
using divides_prod_l[of "p [^] n" b a] assms by simp
next
assume "(p [^] n) divides (a ⊗ b)" thus "(p [^] n) divides b"
proof (induction n)
case 0 with ‹b ∈ carrier G› show ?case
by (simp add: unit_divides)
next
case (Suc n)
hence "(p [^] n) divides (a ⊗ b)" and "(p [^] n) divides b"
using assms(1) divides_prod_r by auto
with ‹(p [^] (Suc n)) divides (a ⊗ b)› obtain c d
where c: "c ∈ carrier G" and "b = (p [^] n) ⊗ c"
and d: "d ∈ carrier G" and "a ⊗ b = (p [^] (Suc n)) ⊗ d"
using assms by blast
hence "(p [^] n) ⊗ (a ⊗ c) = (p [^] n) ⊗ (p ⊗ d)"
using assms by (simp add: m_assoc m_lcomm)
hence "a ⊗ c = p ⊗ d"
using c d assms(1) assms(2) l_cancel by blast
with ‹¬ (p divides a)› and ‹prime G p› have "p divides c"
by (metis assms(2) c d dividesI' prime_divides)
with ‹b = (p [^] n) ⊗ c› show ?case
using assms(1) c by simp
qed
qed
subsection ‹Factorization and Factorial Monoids›
subsubsection ‹Function definitions›
definition factors :: "('a, _) monoid_scheme ⇒ 'a list ⇒ 'a ⇒ bool"
where "factors G fs a ⟷ (∀x ∈ (set fs). irreducible G x) ∧ foldr (⊗⇘G⇙) fs 𝟭⇘G⇙ = a"
definition wfactors ::"('a, _) monoid_scheme ⇒ 'a list ⇒ 'a ⇒ bool"
where "wfactors G fs a ⟷ (∀x ∈ (set fs). irreducible G x) ∧ foldr (⊗⇘G⇙) fs 𝟭⇘G⇙ ∼⇘G⇙ a"
abbreviation list_assoc :: "('a, _) monoid_scheme ⇒ 'a list ⇒ 'a list ⇒ bool" (infix "[∼]ı" 44)
where "list_assoc G ≡ list_all2 (∼⇘G⇙)"
definition essentially_equal :: "('a, _) monoid_scheme ⇒ 'a list ⇒ 'a list ⇒ bool"
where "essentially_equal G fs1 fs2 ⟷ (∃fs1'. fs1 <~~> fs1' ∧ fs1' [∼]⇘G⇙ fs2)"
locale factorial_monoid = comm_monoid_cancel +
assumes factors_exist: "⟦a ∈ carrier G; a ∉ Units G⟧ ⟹ ∃fs. set fs ⊆ carrier G ∧ factors G fs a"
and factors_unique:
"⟦factors G fs a; factors G fs' a; a ∈ carrier G; a ∉ Units G;
set fs ⊆ carrier G; set fs' ⊆ carrier G⟧ ⟹ essentially_equal G fs fs'"
subsubsection ‹Comparing lists of elements›
text ‹Association on lists›
lemma (in monoid) listassoc_refl [simp, intro]:
assumes "set as ⊆ carrier G"
shows "as [∼] as"
using assms by (induct as) simp_all
lemma (in monoid) listassoc_sym [sym]:
assumes "as [∼] bs"
and "set as ⊆ carrier G"
and "set bs ⊆ carrier G"
shows "bs [∼] as"
using assms
proof (induction as arbitrary: bs)
case Cons
then show ?case
by (induction bs) (use associated_sym in auto)
qed auto
lemma (in monoid) listassoc_trans [trans]:
assumes "as [∼] bs" and "bs [∼] cs"
and "set as ⊆ carrier G" and "set bs ⊆ carrier G" and "set cs ⊆ carrier G"
shows "as [∼] cs"
using assms
apply (simp add: list_all2_conv_all_nth set_conv_nth, safe)
by (metis (mono_tags, lifting) associated_trans nth_mem subsetCE)
lemma (in monoid_cancel) irrlist_listassoc_cong:
assumes "∀a∈set as. irreducible G a"
and "as [∼] bs"
and "set as ⊆ carrier G" and "set bs ⊆ carrier G"
shows "∀a∈set bs. irreducible G a"
using assms
by (fastforce simp add: list_all2_conv_all_nth set_conv_nth intro: irreducible_cong)
text ‹Permutations›
lemma perm_map [intro]:
assumes p: "a <~~> b"
shows "map f a <~~> map f b"
using p by simp
lemma perm_map_switch:
assumes m: "map f a = map f b" and p: "b <~~> c"
shows "∃d. a <~~> d ∧ map f d = map f c"
proof -
from m have ‹length a = length b›
by (rule map_eq_imp_length_eq)
from p have ‹mset c = mset b›
by simp
then obtain p where ‹p permutes {..<length b}› ‹permute_list p b = c›
by (rule mset_eq_permutation)
with ‹length a = length b› have ‹p permutes {..<length a}›
by simp
moreover define d where ‹d = permute_list p a›
ultimately have ‹mset a = mset d› ‹map f d = map f c›
using m ‹p permutes {..<length b}› ‹permute_list p b = c›
by (auto simp flip: permute_list_map)
then show ?thesis
by auto
qed
lemma (in monoid) perm_assoc_switch:
assumes a:"as [∼] bs" and p: "bs <~~> cs"
shows "∃bs'. as <~~> bs' ∧ bs' [∼] cs"
proof -
from p have ‹mset cs = mset bs›
by simp
then obtain p where ‹p permutes {..<length bs}› ‹permute_list p bs = cs›
by (rule mset_eq_permutation)
moreover define bs' where ‹bs' = permute_list p as›
ultimately have ‹as <~~> bs'› and ‹bs' [∼] cs›
using a by (auto simp add: list_all2_permute_list_iff list_all2_lengthD)
then show ?thesis by blast
qed
lemma (in monoid) perm_assoc_switch_r:
assumes p: "as <~~> bs" and a:"bs [∼] cs"
shows "∃bs'. as [∼] bs' ∧ bs' <~~> cs"
using a p by (rule list_all2_reorder_left_invariance)
declare perm_sym [sym]
lemma perm_setP:
assumes perm: "as <~~> bs"
and as: "P (set as)"
shows "P (set bs)"
using assms by (metis set_mset_mset)
lemmas (in monoid) perm_closed = perm_setP[of _ _ "λas. as ⊆ carrier G"]
lemmas (in monoid) irrlist_perm_cong = perm_setP[of _ _ "λas. ∀a∈as. irreducible G a"]
text ‹Essentially equal factorizations›
lemma (in monoid) essentially_equalI:
assumes ex: "fs1 <~~> fs1'" "fs1' [∼] fs2"
shows "essentially_equal G fs1 fs2"
using ex unfolding essentially_equal_def by fast
lemma (in monoid) essentially_equalE:
assumes ee: "essentially_equal G fs1 fs2"
and e: "⋀fs1'. ⟦fs1 <~~> fs1'; fs1' [∼] fs2⟧ ⟹ P"
shows "P"
using ee unfolding essentially_equal_def by (fast intro: e)
lemma (in monoid) ee_refl [simp,intro]:
assumes carr: "set as ⊆ carrier G"
shows "essentially_equal G as as"
using carr by (fast intro: essentially_equalI)
lemma (in monoid) ee_sym [sym]:
assumes ee: "essentially_equal G as bs"
and carr: "set as ⊆ carrier G" "set bs ⊆ carrier G"
shows "essentially_equal G bs as"
using ee
proof (elim essentially_equalE)
fix fs
assume "as <~~> fs" "fs [∼] bs"
from perm_assoc_switch_r [OF this] obtain fs' where a: "as [∼] fs'" and p: "fs' <~~> bs"
by blast
from p have "bs <~~> fs'" by (rule perm_sym)
with a[symmetric] carr show ?thesis
by (iprover intro: essentially_equalI perm_closed)
qed
lemma (in monoid) ee_trans [trans]:
assumes ab: "essentially_equal G as bs" and bc: "essentially_equal G bs cs"
and ascarr: "set as ⊆ carrier G"
and bscarr: "set bs ⊆ carrier G"
and cscarr: "set cs ⊆ carrier G"
shows "essentially_equal G as cs"
using ab bc
proof (elim essentially_equalE)
fix abs bcs
assume "abs [∼] bs" and pb: "bs <~~> bcs"
from perm_assoc_switch [OF this] obtain bs' where p: "abs <~~> bs'" and a: "bs' [∼] bcs"
by blast
assume "as <~~> abs"
with p have pp: "as <~~> bs'" by simp
from pp ascarr have c1: "set bs' ⊆ carrier G" by (rule perm_closed)
from pb bscarr have c2: "set bcs ⊆ carrier G" by (rule perm_closed)
assume "bcs [∼] cs"
then have "bs' [∼] cs"
using a c1 c2 cscarr listassoc_trans by blast
with pp show ?thesis
by (rule essentially_equalI)
qed
subsubsection ‹Properties of lists of elements›
text ‹Multiplication of factors in a list›
lemma (in monoid) multlist_closed [simp, intro]:
assumes ascarr: "set fs ⊆ carrier G"
shows "foldr (⊗) fs 𝟭 ∈ carrier G"
using ascarr by (induct fs) simp_all
lemma (in comm_monoid) multlist_dividesI:
assumes "f ∈ set fs" and "set fs ⊆ carrier G"
shows "f divides (foldr (⊗) fs 𝟭)"
using assms
proof (induction fs)
case (Cons a fs)
then have f: "f ∈ carrier G"
by blast
show ?case
using Cons.IH Cons.prems(1) Cons.prems(2) divides_prod_l f by auto
qed auto
lemma (in comm_monoid_cancel) multlist_listassoc_cong:
assumes "fs [∼] fs'"
and "set fs ⊆ carrier G" and "set fs' ⊆ carrier G"
shows "foldr (⊗) fs 𝟭 ∼ foldr (⊗) fs' 𝟭"
using assms
proof (induct fs arbitrary: fs')
case (Cons a as fs')
then show ?case
proof (induction fs')
case (Cons b bs)
then have p: "a ⊗ foldr (⊗) as 𝟭 ∼ b ⊗ foldr (⊗) as 𝟭"
by (simp add: mult_cong_l)
then have "foldr (⊗) as 𝟭 ∼ foldr (⊗) bs 𝟭"
using Cons by auto
with Cons have "b ⊗ foldr (⊗) as 𝟭 ∼ b ⊗ foldr (⊗) bs 𝟭"
by (simp add: mult_cong_r)
then show ?case
using Cons.prems(3) Cons.prems(4) monoid.associated_trans monoid_axioms p by force
qed auto
qed auto
lemma (in comm_monoid) multlist_perm_cong:
assumes prm: "as <~~> bs"
and ascarr: "set as ⊆ carrier G"
shows "foldr (⊗) as 𝟭 = foldr (⊗) bs 𝟭"
proof -
from prm have ‹mset (rev as) = mset (rev bs)›
by simp
moreover note one_closed
ultimately have ‹fold (⊗) (rev as) 𝟭 = fold (⊗) (rev bs) 𝟭›
by (rule fold_permuted_eq) (use ascarr in ‹auto intro: m_lcomm›)
then show ?thesis
by (simp add: foldr_conv_fold)
qed
lemma (in comm_monoid_cancel) multlist_ee_cong:
assumes "essentially_equal G fs fs'"
and "set fs ⊆ carrier G" and "set fs' ⊆ carrier G"
shows "foldr (⊗) fs 𝟭 ∼ foldr (⊗) fs' 𝟭"
using assms
by (metis essentially_equal_def multlist_listassoc_cong multlist_perm_cong perm_closed)
subsubsection ‹Factorization in irreducible elements›
lemma wfactorsI:
fixes G (structure)
assumes "∀f∈set fs. irreducible G f"
and "foldr (⊗) fs 𝟭 ∼ a"
shows "wfactors G fs a"
using assms unfolding wfactors_def by simp
lemma wfactorsE:
fixes G (structure)
assumes wf: "wfactors G fs a"
and e: "⟦∀f∈set fs. irreducible G f; foldr (⊗) fs 𝟭 ∼ a⟧ ⟹ P"
shows "P"
using wf unfolding wfactors_def by (fast dest: e)
lemma (in monoid) factorsI:
assumes "∀f∈set fs. irreducible G f"
and "foldr (⊗) fs 𝟭 = a"
shows "factors G fs a"
using assms unfolding factors_def by simp
lemma factorsE:
fixes G (structure)
assumes f: "factors G fs a"
and e: "⟦∀f∈set fs. irreducible G f; foldr (⊗) fs 𝟭 = a⟧ ⟹ P"
shows "P"
using f unfolding factors_def by (simp add: e)
lemma (in monoid) factors_wfactors:
assumes "factors G as a" and "set as ⊆ carrier G"
shows "wfactors G as a"
using assms by (blast elim: factorsE intro: wfactorsI)
lemma (in monoid) wfactors_factors:
assumes "wfactors G as a" and "set as ⊆ carrier G"
shows "∃a'. factors G as a' ∧ a' ∼ a"
using assms by (blast elim: wfactorsE intro: factorsI)
lemma (in monoid) factors_closed [dest]:
assumes "factors G fs a" and "set fs ⊆ carrier G"
shows "a ∈ carrier G"
using assms by (elim factorsE, clarsimp)
lemma (in monoid) nunit_factors:
assumes anunit: "a ∉ Units G"
and fs: "factors G as a"
shows "length as > 0"
proof -
from anunit Units_one_closed have "a ≠ 𝟭" by auto
with fs show ?thesis by (auto elim: factorsE)
qed
lemma (in monoid) unit_wfactors [simp]:
assumes aunit: "a ∈ Units G"
shows "wfactors G [] a"
using aunit by (intro wfactorsI) (simp, simp add: Units_assoc)
lemma (in comm_monoid_cancel) unit_wfactors_empty:
assumes aunit: "a ∈ Units G"
and wf: "wfactors G fs a"
and carr[simp]: "set fs ⊆ carrier G"
shows "fs = []"
proof (cases fs)
case fs: (Cons f fs')
from carr have fcarr[simp]: "f ∈ carrier G" and carr'[simp]: "set fs' ⊆ carrier G"
by (simp_all add: fs)
from fs wf have "irreducible G f" by (simp add: wfactors_def)
then have fnunit: "f ∉ Units G" by (fast elim: irreducibleE)
from fs wf have a: "f ⊗ foldr (⊗) fs' 𝟭 ∼ a" by (simp add: wfactors_def)
note aunit
also from fs wf
have a: "f ⊗ foldr (⊗) fs' 𝟭 ∼ a" by (simp add: wfactors_def)
have "a ∼ f ⊗ foldr (⊗) fs' 𝟭"
by (simp add: Units_closed[OF aunit] a[symmetric])
finally have "f ⊗ foldr (⊗) fs' 𝟭 ∈ Units G" by simp
then have "f ∈ Units G" by (intro unit_factor[of f], simp+)
with fnunit show ?thesis by contradiction
qed
text ‹Comparing wfactors›
lemma (in comm_monoid_cancel) wfactors_listassoc_cong_l:
assumes fact: "wfactors G fs a"
and asc: "fs [∼] fs'"
and carr: "a ∈ carrier G" "set fs ⊆ carrier G" "set fs' ⊆ carrier G"
shows "wfactors G fs' a"
proof -
{ from asc[symmetric] have "foldr (⊗) fs' 𝟭 ∼ foldr (⊗) fs 𝟭"
by (simp add: multlist_listassoc_cong carr)
also assume "foldr (⊗) fs 𝟭 ∼ a"
finally have "foldr (⊗) fs' 𝟭 ∼ a" by (simp add: carr) }
then show ?thesis
using fact
by (meson asc carr(2) carr(3) irrlist_listassoc_cong wfactors_def)
qed
lemma (in comm_monoid) wfactors_perm_cong_l:
assumes "wfactors G fs a"
and "fs <~~> fs'"
and "set fs ⊆ carrier G"
shows "wfactors G fs' a"
using assms irrlist_perm_cong multlist_perm_cong wfactors_def by fastforce
lemma (in comm_monoid_cancel) wfactors_ee_cong_l [trans]:
assumes ee: "essentially_equal G as bs"
and bfs: "wfactors G bs b"
and carr: "b ∈ carrier G" "set as ⊆ carrier G" "set bs ⊆ carrier G"
shows "wfactors G as b"
using ee
proof (elim essentially_equalE)
fix fs
assume prm: "as <~~> fs"
with carr have fscarr: "set fs ⊆ carrier G"
using perm_closed by blast
note bfs
also assume [symmetric]: "fs [∼] bs"
also (wfactors_listassoc_cong_l)
have ‹mset fs = mset as› using prm by simp
finally (wfactors_perm_cong_l)
show "wfactors G as b" by (simp add: carr fscarr)
qed
lemma (in monoid) wfactors_cong_r [trans]:
assumes fac: "wfactors G fs a" and aa': "a ∼ a'"
and carr[simp]: "a ∈ carrier G" "a' ∈ carrier G" "set fs ⊆ carrier G"
shows "wfactors G fs a'"
using fac
proof (elim wfactorsE, intro wfactorsI)
assume "foldr (⊗) fs 𝟭 ∼ a" also note aa'
finally show "foldr (⊗) fs 𝟭 ∼ a'" by simp
qed
subsubsection ‹Essentially equal factorizations›
lemma (in comm_monoid_cancel) unitfactor_ee:
assumes uunit: "u ∈ Units G"
and carr: "set as ⊆ carrier G"
shows "essentially_equal G (as[0 := (as!0 ⊗ u)]) as"
(is "essentially_equal G ?as' as")
proof -
have "as[0 := as ! 0 ⊗ u] [∼] as"
proof (cases as)
case (Cons a as')
then show ?thesis
using associatedI2 carr uunit by auto
qed auto
then show ?thesis
using essentially_equal_def by blast
qed
lemma (in comm_monoid_cancel) factors_cong_unit:
assumes u: "u ∈ Units G"
and a: "a ∉ Units G"
and afs: "factors G as a"
and ascarr: "set as ⊆ carrier G"
shows "factors G (as[0 := (as!0 ⊗ u)]) (a ⊗ u)"
(is "factors G ?as' ?a'")
proof (cases as)
case Nil
then show ?thesis
using afs a nunit_factors by auto
next
case (Cons b bs)
have *: "∀f∈set as. irreducible G f" "foldr (⊗) as 𝟭 = a"
using afs by (auto simp: factors_def)
show ?thesis
proof (intro factorsI)
show "foldr (⊗) (as[0 := as ! 0 ⊗ u]) 𝟭 = a ⊗ u"
using Cons u ascarr * by (auto simp add: m_ac Units_closed)
show "∀f∈set (as[0 := as ! 0 ⊗ u]). irreducible G f"
using Cons u ascarr * by (force intro: irreducible_prod_rI)
qed
qed
lemma (in comm_monoid) perm_wfactorsD:
assumes prm: "as <~~> bs"
and afs: "wfactors G as a"
and bfs: "wfactors G bs b"
and [simp]: "a ∈ carrier G" "b ∈ carrier G"
and ascarr [simp]: "set as ⊆ carrier G"
shows "a ∼ b"
using afs bfs
proof (elim wfactorsE)
from prm have [simp]: "set bs ⊆ carrier G" by (simp add: perm_closed)
assume "foldr (⊗) as 𝟭 ∼ a"
then have "a ∼ foldr (⊗) as 𝟭"
by (simp add: associated_sym)
also from prm
have "foldr (⊗) as 𝟭 = foldr (⊗) bs 𝟭" by (rule multlist_perm_cong, simp)
also assume "foldr (⊗) bs 𝟭 ∼ b"
finally show "a ∼ b" by simp
qed
lemma (in comm_monoid_cancel) listassoc_wfactorsD:
assumes assoc: "as [∼] bs"
and afs: "wfactors G as a"
and bfs: "wfactors G bs b"
and [simp]: "a ∈ carrier G" "b ∈ carrier G"
and [simp]: "set as ⊆ carrier G" "set bs ⊆ carrier G"
shows "a ∼ b"
using afs bfs
proof (elim wfactorsE)
assume "foldr (⊗) as 𝟭 ∼ a"
then have "a ∼ foldr (⊗) as 𝟭" by (simp add: associated_sym)
also from assoc
have "foldr (⊗) as 𝟭 ∼ foldr (⊗) bs 𝟭" by (rule multlist_listassoc_cong, simp+)
also assume "foldr (⊗) bs 𝟭 ∼ b"
finally show "a ∼ b" by simp
qed
lemma (in comm_monoid_cancel) ee_wfactorsD:
assumes ee: "essentially_equal G as bs"
and afs: "wfactors G as a" and bfs: "wfactors G bs b"
and [simp]: "a ∈ carrier G" "b ∈ carrier G"
and ascarr[simp]: "set as ⊆ carrier G" and bscarr[simp]: "set bs ⊆ carrier G"
shows "a ∼ b"
using ee
proof (elim essentially_equalE)
fix fs
assume prm: "as <~~> fs"
then have as'carr[simp]: "set fs ⊆ carrier G"
by (simp add: perm_closed)
from afs prm have afs': "wfactors G fs a"
by (rule wfactors_perm_cong_l) simp
assume "fs [∼] bs"
from this afs' bfs show "a ∼ b"
by (rule listassoc_wfactorsD) simp_all
qed
lemma (in comm_monoid_cancel) ee_factorsD:
assumes ee: "essentially_equal G as bs"
and afs: "factors G as a" and bfs:"factors G bs b"
and "set as ⊆ carrier G" "set bs ⊆ carrier G"
shows "a ∼ b"
using assms by (blast intro: factors_wfactors dest: ee_wfactorsD)
lemma (in factorial_monoid) ee_factorsI:
assumes ab: "a ∼ b"
and afs: "factors G as a" and anunit: "a ∉ Units G"
and bfs: "factors G bs b" and bnunit: "b ∉ Units G"
and ascarr: "set as ⊆ carrier G" and bscarr: "set bs ⊆ carrier G"
shows "essentially_equal G as bs"
proof -
note carr[simp] = factors_closed[OF afs ascarr] ascarr[THEN subsetD]
factors_closed[OF bfs bscarr] bscarr[THEN subsetD]
from ab carr obtain u where uunit: "u ∈ Units G" and a: "a = b ⊗ u"
by (elim associatedE2)
from uunit bscarr have ee: "essentially_equal G (bs[0 := (bs!0 ⊗ u)]) bs"
(is "essentially_equal G ?bs' bs")
by (rule unitfactor_ee)
from bscarr uunit have bs'carr: "set ?bs' ⊆ carrier G"
by (cases bs) (simp_all add: Units_closed)
from uunit bnunit bfs bscarr have fac: "factors G ?bs' (b ⊗ u)"
by (rule factors_cong_unit)
from afs fac[simplified a[symmetric]] ascarr bs'carr anunit
have "essentially_equal G as ?bs'"
by (blast intro: factors_unique)
also note ee
finally show "essentially_equal G as bs"
by (simp add: ascarr bscarr bs'carr)
qed
lemma (in factorial_monoid) ee_wfactorsI:
assumes asc: "a ∼ b"
and asf: "wfactors G as a" and bsf: "wfactors G bs b"
and acarr[simp]: "a ∈ carrier G" and bcarr[simp]: "b ∈ carrier G"
and ascarr[simp]: "set as ⊆ carrier G" and bscarr[simp]: "set bs ⊆ carrier G"
shows "essentially_equal G as bs"
using assms
proof (cases "a ∈ Units G")
case aunit: True
also note asc
finally have bunit: "b ∈ Units G" by simp
from aunit asf ascarr have e: "as = []"
by (rule unit_wfactors_empty)
from bunit bsf bscarr have e': "bs = []"
by (rule unit_wfactors_empty)
have "essentially_equal G [] []"
by (fast intro: essentially_equalI)
then show ?thesis
by (simp add: e e')
next
case anunit: False
have bnunit: "b ∉ Units G"
proof clarify
assume "b ∈ Units G"
also note asc[symmetric]
finally have "a ∈ Units G" by simp
with anunit show False ..
qed
from wfactors_factors[OF asf ascarr] obtain a' where fa': "factors G as a'" and a': "a' ∼ a"
by blast
from fa' ascarr have a'carr[simp]: "a' ∈ carrier G"
by fast
have a'nunit: "a' ∉ Units G"
proof clarify
assume "a' ∈ Units G"
also note a'
finally have "a ∈ Units G" by simp
with anunit
show "False" ..
qed
from wfactors_factors[OF bsf bscarr] obtain b' where fb': "factors G bs b'" and b': "b' ∼ b"
by blast
from fb' bscarr have b'carr[simp]: "b' ∈ carrier G"
by fast
have b'nunit: "b' ∉ Units G"
proof clarify
assume "b' ∈ Units G"
also note b'
finally have "b ∈ Units G" by simp
with bnunit show False ..
qed
note a'
also note asc
also note b'[symmetric]
finally have "a' ∼ b'" by simp
from this fa' a'nunit fb' b'nunit ascarr bscarr show "essentially_equal G as bs"
by (rule ee_factorsI)
qed
lemma (in factorial_monoid) ee_wfactors:
assumes asf: "wfactors G as a"
and bsf: "wfactors G bs b"
and acarr: "a ∈ carrier G" and bcarr: "b ∈ carrier G"
and ascarr: "set as ⊆ carrier G" and bscarr: "set bs ⊆ carrier G"
shows asc: "a ∼ b = essentially_equal G as bs"
using assms by (fast intro: ee_wfactorsI ee_wfactorsD)
lemma (in factorial_monoid) wfactors_exist [intro, simp]:
assumes acarr[simp]: "a ∈ carrier G"
shows "∃fs. set fs ⊆ carrier G ∧ wfactors G fs a"
proof (cases "a ∈ Units G")
case True
then have "wfactors G [] a" by (rule unit_wfactors)
then show ?thesis by (intro exI) force
next
case False
with factors_exist [OF acarr] obtain fs where fscarr: "set fs ⊆ carrier G" and f: "factors G fs a"
by blast
from f have "wfactors G fs a" by (rule factors_wfactors) fact
with fscarr show ?thesis by fast
qed
lemma (in monoid) wfactors_prod_exists [intro, simp]:
assumes "∀a ∈ set as. irreducible G a" and "set as ⊆ carrier G"
shows "∃a. a ∈ carrier G ∧ wfactors G as a"
unfolding wfactors_def using assms by blast
lemma (in factorial_monoid) wfactors_unique:
assumes "wfactors G fs a"
and "wfactors G fs' a"
and "a ∈ carrier G"
and "set fs ⊆ carrier G"
and "set fs' ⊆ carrier G"
shows "essentially_equal G fs fs'"
using assms by (fast intro: ee_wfactorsI[of a a])
lemma (in monoid) factors_mult_single:
assumes "irreducible G a" and "factors G fb b" and "a ∈ carrier G"
shows "factors G (a # fb) (a ⊗ b)"
using assms unfolding factors_def by simp
lemma (in monoid_cancel) wfactors_mult_single:
assumes f: "irreducible G a" "wfactors G fb b"
"a ∈ carrier G" "b ∈ carrier G" "set fb ⊆ carrier G"
shows "wfactors G (a # fb) (a ⊗ b)"
using assms unfolding wfactors_def by (simp add: mult_cong_r)
lemma (in monoid) factors_mult:
assumes factors: "factors G fa a" "factors G fb b"
and ascarr: "set fa ⊆ carrier G"
and bscarr: "set fb ⊆ carrier G"
shows "factors G (fa @ fb) (a ⊗ b)"
proof -
have "foldr (⊗) (fa @ fb) 𝟭 = foldr (⊗) fa 𝟭 ⊗ foldr (⊗) fb 𝟭" if "set fa ⊆ carrier G"
"Ball (set fa) (irreducible G)"
using that bscarr by (induct fa) (simp_all add: m_assoc)
then show ?thesis
using assms unfolding factors_def by force
qed
lemma (in comm_monoid_cancel) wfactors_mult [intro]:
assumes asf: "wfactors G as a" and bsf:"wfactors G bs b"
and acarr: "a ∈ carrier G" and bcarr: "b ∈ carrier G"
and ascarr: "set as ⊆ carrier G" and bscarr:"set bs ⊆ carrier G"
shows "wfactors G (as @ bs) (a ⊗ b)"
using wfactors_factors[OF asf ascarr] and wfactors_factors[OF bsf bscarr]
proof clarsimp
fix a' b'
assume asf': "factors G as a'" and a'a: "a' ∼ a"
and bsf': "factors G bs b'" and b'b: "b' ∼ b"
from asf' have a'carr: "a' ∈ carrier G" by (rule factors_closed) fact
from bsf' have b'carr: "b' ∈ carrier G" by (rule factors_closed) fact
note carr = acarr bcarr a'carr b'carr ascarr bscarr
from asf' bsf' have "factors G (as @ bs) (a' ⊗ b')"
by (rule factors_mult) fact+
with carr have abf': "wfactors G (as @ bs) (a' ⊗ b')"
by (intro factors_wfactors) simp_all
also from b'b carr have trb: "a' ⊗ b' ∼ a' ⊗ b"
by (intro mult_cong_r)
also from a'a carr have tra: "a' ⊗ b ∼ a ⊗ b"
by (intro mult_cong_l)
finally show "wfactors G (as @ bs) (a ⊗ b)"
by (simp add: carr)
qed
lemma (in comm_monoid) factors_dividesI:
assumes "factors G fs a"
and "f ∈ set fs"
and "set fs ⊆ carrier G"
shows "f divides a"
using assms by (fast elim: factorsE intro: multlist_dividesI)
lemma (in comm_monoid) wfactors_dividesI:
assumes p: "wfactors G fs a"
and fscarr: "set fs ⊆ carrier G" and acarr: "a ∈ carrier G"
and f: "f ∈ set fs"
shows "f divides a"
using wfactors_factors[OF p fscarr]
proof clarsimp
fix a'
assume fsa': "factors G fs a'" and a'a: "a' ∼ a"
with fscarr have a'carr: "a' ∈ carrier G"
by (simp add: factors_closed)
from fsa' fscarr f have "f divides a'"
by (fast intro: factors_dividesI)
also note a'a
finally show "f divides a"
by (simp add: f fscarr[THEN subsetD] acarr a'carr)
qed
subsubsection ‹Factorial monoids and wfactors›
lemma (in comm_monoid_cancel) factorial_monoidI:
assumes wfactors_exists: "⋀a. ⟦ a ∈ carrier G; a ∉ Units G ⟧ ⟹ ∃fs. set fs ⊆ carrier G ∧ wfactors G fs a"
and wfactors_unique:
"⋀a fs fs'. ⟦a ∈ carrier G; set fs ⊆ carrier G; set fs' ⊆ carrier G;
wfactors G fs a; wfactors G fs' a⟧ ⟹ essentially_equal G fs fs'"
shows "factorial_monoid G"
proof
fix a
assume acarr: "a ∈ carrier G" and anunit: "a ∉ Units G"
from wfactors_exists[OF acarr anunit]
obtain as where ascarr: "set as ⊆ carrier G" and afs: "wfactors G as a"
by blast
from wfactors_factors [OF afs ascarr] obtain a' where afs': "factors G as a'" and a'a: "a' ∼ a"
by blast
from afs' ascarr have a'carr: "a' ∈ carrier G"
by fast
have a'nunit: "a' ∉ Units G"
proof clarify
assume "a' ∈ Units G"
also note a'a
finally have "a ∈ Units G" by (simp add: acarr)
with anunit show False ..
qed
from a'carr acarr a'a obtain u where uunit: "u ∈ Units G" and a': "a' = a ⊗ u"
by (blast elim: associatedE2)
note [simp] = acarr Units_closed[OF uunit] Units_inv_closed[OF uunit]
have "a = a ⊗ 𝟭" by simp
also have "… = a ⊗ (u ⊗ inv u)" by (simp add: uunit)
also have "… = a' ⊗ inv u" by (simp add: m_assoc[symmetric] a'[symmetric])
finally have a: "a = a' ⊗ inv u" .
from ascarr uunit have cr: "set (as[0:=(as!0 ⊗ inv u)]) ⊆ carrier G"
by (cases as) auto
from afs' uunit a'nunit acarr ascarr have "factors G (as[0:=(as!0 ⊗ inv u)]) a"
by (simp add: a factors_cong_unit)
with cr show "∃fs. set fs ⊆ carrier G ∧ factors G fs a"
by fast
qed (blast intro: factors_wfactors wfactors_unique)
subsection ‹Factorizations as Multisets›
text ‹Gives useful operations like intersection›
abbreviation "assocs G x ≡ eq_closure_of (division_rel G) {x}"
definition "fmset G as = mset (map (assocs G) as)"
text ‹Helper lemmas›
lemma (in monoid) assocs_repr_independence:
assumes "y ∈ assocs G x" "x ∈ carrier G"
shows "assocs G x = assocs G y"
using assms
by (simp add: eq_closure_of_def elem_def) (use associated_sym associated_trans in ‹blast+›)
lemma (in monoid) assocs_self:
assumes "x ∈ carrier G"
shows "x ∈ assocs G x"
using assms by (fastforce intro: closure_ofI2)
lemma (in monoid) assocs_repr_independenceD:
assumes repr: "assocs G x = assocs G y" and ycarr: "y ∈ carrier G"
shows "y ∈ assocs G x"
unfolding repr using ycarr by (intro assocs_self)
lemma (in comm_monoid) assocs_assoc:
assumes "a ∈ assocs G b" "b ∈ carrier G"
shows "a ∼ b"
using assms by (elim closure_ofE2) simp
lemmas (in comm_monoid) assocs_eqD = assocs_repr_independenceD[THEN assocs_assoc]
subsubsection ‹Comparing multisets›
lemma (in monoid) fmset_perm_cong:
assumes prm: "as <~~> bs"
shows "fmset G as = fmset G bs"
using perm_map[OF prm] unfolding fmset_def by blast
lemma (in comm_monoid_cancel) eqc_listassoc_cong:
assumes "as [∼] bs" and "set as ⊆ carrier G" and "set bs ⊆ carrier G"
shows "map (assocs G) as = map (assocs G) bs"
using assms
proof (induction as arbitrary: bs)
case Nil
then show ?case by simp
next
case (Cons a as)
then show ?case
proof (clarsimp simp add: Cons_eq_map_conv list_all2_Cons1)
fix z zs
assume zzs: "a ∈ carrier G" "set as ⊆ carrier G" "bs = z # zs" "a ∼ z"
"as [∼] zs" "z ∈ carrier G" "set zs ⊆ carrier G"
then show "assocs G a = assocs G z"
apply (simp add: eq_closure_of_def elem_def)
using ‹a ∈ carrier G› ‹z ∈ carrier G› ‹a ∼ z› associated_sym associated_trans by blast+
qed
qed
lemma (in comm_monoid_cancel) fmset_listassoc_cong:
assumes "as [∼] bs"
and "set as ⊆ carrier G" and "set bs ⊆ carrier G"
shows "fmset G as = fmset G bs"
using assms unfolding fmset_def by (simp add: eqc_listassoc_cong)
lemma (in comm_monoid_cancel) ee_fmset:
assumes ee: "essentially_equal G as bs"
and ascarr: "set as ⊆ carrier G" and bscarr: "set bs ⊆ carrier G"
shows "fmset G as = fmset G bs"
using ee
thm essentially_equal_def
proof (elim essentially_equalE)
fix as'
assume prm: "as <~~> as'"
from prm ascarr have as'carr: "set as' ⊆ carrier G"
by (rule perm_closed)
from prm have "fmset G as = fmset G as'"
by (rule fmset_perm_cong)
also assume "as' [∼] bs"
with as'carr bscarr have "fmset G as' = fmset G bs"
by (simp add: fmset_listassoc_cong)
finally show "fmset G as = fmset G bs" .
qed
lemma (in comm_monoid_cancel) fmset_ee:
assumes mset: "fmset G as = fmset G bs"
and ascarr: "set as ⊆ carrier G" and bscarr: "set bs ⊆ carrier G"
shows "essentially_equal G as bs"
proof -
from mset have "mset (map (assocs G) bs) = mset (map (assocs G) as)"
by (simp add: fmset_def)
then obtain p where ‹p permutes {..<length (map (assocs G) as)}›
‹permute_list p (map (assocs G) as) = map (assocs G) bs›
by (rule mset_eq_permutation)
then have ‹p permutes {..<length as}›
‹map (assocs G) (permute_list p as) = map (assocs G) bs›
by (simp_all add: permute_list_map)
moreover define as' where ‹as' = permute_list p as›
ultimately have tp: "as <~~> as'" and tm: "map (assocs G) as' = map (assocs G) bs"
by simp_all
from tp show ?thesis
proof (rule essentially_equalI)
from tm tp ascarr have as'carr: "set as' ⊆ carrier G"
using perm_closed by blast
from tm as'carr[THEN subsetD] bscarr[THEN subsetD] show "as' [∼] bs"
by (induct as' arbitrary: bs) (simp, fastforce dest: assocs_eqD[THEN associated_sym])
qed
qed
lemma (in comm_monoid_cancel) ee_is_fmset:
assumes "set as ⊆ carrier G" and "set bs ⊆ carrier G"
shows "essentially_equal G as bs = (fmset G as = fmset G bs)"
using assms by (fast intro: ee_fmset fmset_ee)
subsubsection ‹Interpreting multisets as factorizations›
lemma (in monoid) mset_fmsetEx:
assumes elems: "⋀X. X ∈ set_mset Cs ⟹ ∃x. P x ∧ X = assocs G x"
shows "∃cs. (∀c ∈ set cs. P c) ∧ fmset G cs = Cs"
proof -
from surjE[OF surj_mset] obtain Cs' where Cs: "Cs = mset Cs'"
by blast
have "∃cs. (∀c ∈ set cs. P c) ∧ mset (map (assocs G) cs) = Cs"
using elems unfolding Cs
proof (induction Cs')
case (Cons a Cs')
then obtain c cs where csP: "∀x∈set cs. P x" and mset: "mset (map (assocs G) cs) = mset Cs'"
and cP: "P c" and a: "a = assocs G c"
by force
then have tP: "∀x∈set (c#cs). P x"
by simp
show ?case
using tP mset a by fastforce
qed auto
then show ?thesis by (simp add: fmset_def)
qed
lemma (in monoid) mset_wfactorsEx:
assumes elems: "⋀X. X ∈ set_mset Cs ⟹ ∃x. (x ∈ carrier G ∧ irreducible G x) ∧ X = assocs G x"
shows "∃c cs. c ∈ carrier G ∧ set cs ⊆ carrier G ∧ wfactors G cs c ∧ fmset G cs = Cs"
proof -
have "∃cs. (∀c∈set cs. c ∈ carrier G ∧ irreducible G c) ∧ fmset G cs = Cs"
by (intro mset_fmsetEx, rule elems)
then obtain cs where p[rule_format]: "∀c∈set cs. c ∈ carrier G ∧ irreducible G c"
and Cs[symmetric]: "fmset G cs = Cs" by auto
from p have cscarr: "set cs ⊆ carrier G" by fast
from p have "∃c. c ∈ carrier G ∧ wfactors G cs c"
by (intro wfactors_prod_exists) auto
then obtain c where ccarr: "c ∈ carrier G" and cfs: "wfactors G cs c" by auto
with cscarr Cs show ?thesis by fast
qed
subsubsection ‹Multiplication on multisets›
lemma (in factorial_monoid) mult_wfactors_fmset:
assumes afs: "wfactors G as a"
and bfs: "wfactors G bs b"
and cfs: "wfactors G cs (a ⊗ b)"
and carr: "a ∈ carrier G" "b ∈ carrier G"
"set as ⊆ carrier G" "set bs ⊆ carrier G" "set cs ⊆ carrier G"
shows "fmset G cs = fmset G as + fmset G bs"
proof -
from assms have "wfactors G (as @ bs) (a ⊗ b)"
by (intro wfactors_mult)
with carr cfs have "essentially_equal G cs (as@bs)"
by (intro ee_wfactorsI[of "a⊗b" "a⊗b"]) simp_all
with carr have "fmset G cs = fmset G (as@bs)"
by (intro ee_fmset) simp_all
also have "fmset G (as@bs) = fmset G as + fmset G bs"
by (simp add: fmset_def)
finally show "fmset G cs = fmset G as + fmset G bs" .
qed
lemma (in factorial_monoid) mult_factors_fmset:
assumes afs: "factors G as a"
and bfs: "factors G bs b"
and cfs: "factors G cs (a ⊗ b)"
and "set as ⊆ carrier G" "set bs ⊆ carrier G" "set cs ⊆ carrier G"
shows "fmset G cs = fmset G as + fmset G bs"
using assms by (blast intro: factors_wfactors mult_wfactors_fmset)
lemma (in comm_monoid_cancel) fmset_wfactors_mult:
assumes mset: "fmset G cs = fmset G as + fmset G bs"
and carr: "a ∈ carrier G" "b ∈ carrier G" "c ∈ carrier G"
"set as ⊆ carrier G" "set bs ⊆ carrier G" "set cs ⊆ carrier G"
and fs: "wfactors G as a" "wfactors G bs b" "wfactors G cs c"
shows "c ∼ a ⊗ b"
proof -
from carr fs have m: "wfactors G (as @ bs) (a ⊗ b)"
by (intro wfactors_mult)
from mset have "fmset G cs = fmset G (as@bs)"
by (simp add: fmset_def)
then have "essentially_equal G cs (as@bs)"
by (rule fmset_ee) (simp_all add: carr)
then show "c ∼ a ⊗ b"
by (rule ee_wfactorsD[of "cs" "as@bs"]) (simp_all add: assms m)
qed
subsubsection ‹Divisibility on multisets›
lemma (in factorial_monoid) divides_fmsubset:
assumes ab: "a divides b"
and afs: "wfactors G as a"
and bfs: "wfactors G bs b"
and carr: "a ∈ carrier G" "b ∈ carrier G" "set as ⊆ carrier G" "set bs ⊆ carrier G"
shows "fmset G as ⊆# fmset G bs"
using ab
proof (elim dividesE)
fix c
assume ccarr: "c ∈ carrier G"
from wfactors_exist [OF this]
obtain cs where cscarr: "set cs ⊆ carrier G" and cfs: "wfactors G cs c"
by blast
note carr = carr ccarr cscarr
assume "b = a ⊗ c"
with afs bfs cfs carr have "fmset G bs = fmset G as + fmset G cs"
by (intro mult_wfactors_fmset[OF afs cfs]) simp_all
then show ?thesis by simp
qed
lemma (in comm_monoid_cancel) fmsubset_divides:
assumes msubset: "fmset G as ⊆# fmset G bs"
and afs: "wfactors G as a"
and bfs: "wfactors G bs b"
and acarr: "a ∈ carrier G"
and bcarr: "b ∈ carrier G"
and ascarr: "set as ⊆ carrier G"
and bscarr: "set bs ⊆ carrier G"
shows "a divides b"
proof -
from afs have airr: "∀a ∈ set as. irreducible G a" by (fast elim: wfactorsE)
from bfs have birr: "∀b ∈ set bs. irreducible G b" by (fast elim: wfactorsE)
have "∃c cs. c ∈ carrier G ∧ set cs ⊆ carrier G ∧ wfactors G cs c ∧ fmset G cs = fmset G bs - fmset G as"
proof (intro mset_wfactorsEx, simp)
fix X
assume "X ∈# fmset G bs - fmset G as"
then have "X ∈# fmset G bs" by (rule in_diffD)
then have "X ∈ set (map (assocs G) bs)" by (simp add: fmset_def)
then have "∃x. x ∈ set bs ∧ X = assocs G x" by (induct bs) auto
then obtain x where xbs: "x ∈ set bs" and X: "X = assocs G x" by auto
with bscarr have xcarr: "x ∈ carrier G" by fast
from xbs birr have xirr: "irreducible G x" by simp
from xcarr and xirr and X show "∃x. x ∈ carrier G ∧ irreducible G x ∧ X = assocs G x"
by fast
qed
then obtain c cs
where ccarr: "c ∈ carrier G"
and cscarr: "set cs ⊆ carrier G"
and csf: "wfactors G cs c"
and csmset: "fmset G cs = fmset G bs - fmset G as" by auto
from csmset msubset
have "fmset G bs = fmset G as + fmset G cs"
by (simp add: multiset_eq_iff subseteq_mset_def)
then have basc: "b ∼ a ⊗ c"
by (rule fmset_wfactors_mult) fact+
then show ?thesis
proof (elim associatedE2)
fix u
assume "u ∈ Units G" "b = a ⊗ c ⊗ u"
with acarr ccarr show "a divides b"
by (fast intro: dividesI[of "c ⊗ u"] m_assoc)
qed (simp_all add: acarr bcarr ccarr)
qed
lemma (in factorial_monoid) divides_as_fmsubset:
assumes "wfactors G as a"
and "wfactors G bs b"
and "a ∈ carrier G"
and "b ∈ carrier G"
and "set as ⊆ carrier G"
and "set bs ⊆ carrier G"
shows "a divides b = (fmset G as ⊆# fmset G bs)"
using assms
by (blast intro: divides_fmsubset fmsubset_divides)
text ‹Proper factors on multisets›
lemma (in factorial_monoid) fmset_properfactor:
assumes asubb: "fmset G as ⊆# fmset G bs"
and anb: "fmset G as ≠ fmset G bs"
and "wfactors G as a"
and "wfactors G bs b"
and "a ∈ carrier G"
and "b ∈ carrier G"
and "set as ⊆ carrier G"
and "set bs ⊆ carrier G"
shows "properfactor G a b"
proof (rule properfactorI)
show "a divides b"
using assms asubb fmsubset_divides by blast
show "¬ b divides a"
by (meson anb assms asubb factorial_monoid.divides_fmsubset factorial_monoid_axioms subset_mset.antisym)
qed
lemma (in factorial_monoid) properfactor_fmset:
assumes "properfactor G a b"
and "wfactors G as a"
and "wfactors G bs b"
and "a ∈ carrier G"
and "b ∈ carrier G"
and "set as ⊆ carrier G"
and "set bs ⊆ carrier G"
shows "fmset G as ⊆# fmset G bs"
using assms
by (meson divides_as_fmsubset properfactor_divides)
lemma (in factorial_monoid) properfactor_fmset_ne:
assumes pf: "properfactor G a b"
and "wfactors G as a"
and "wfactors G bs b"
and "a ∈ carrier G"
and "b ∈ carrier G"
and "set as ⊆ carrier G"
and "set bs ⊆ carrier G"
shows "fmset G as ≠ fmset G bs"
using properfactorE [OF pf] assms divides_as_fmsubset by force
subsection ‹Irreducible Elements are Prime›
lemma (in factorial_monoid) irreducible_prime:
assumes pirr: "irreducible G p" and pcarr: "p ∈ carrier G"
shows "prime G p"
using pirr
proof (elim irreducibleE, intro primeI)
fix a b
assume acarr: "a ∈ carrier G" and bcarr: "b ∈ carrier G"
and pdvdab: "p divides (a ⊗ b)"
and pnunit: "p ∉ Units G"
assume irreduc[rule_format]:
"∀b. b ∈ carrier G ∧ properfactor G b p ⟶ b ∈ Units G"
from pdvdab obtain c where ccarr: "c ∈ carrier G" and abpc: "a ⊗ b = p ⊗ c"
by (rule dividesE)
obtain as where ascarr: "set as ⊆ carrier G" and afs: "wfactors G as a"
using wfactors_exist [OF acarr] by blast
obtain bs where bscarr: "set bs ⊆ carrier G" and bfs: "wfactors G bs b"
using wfactors_exist [OF bcarr] by blast
obtain cs where cscarr: "set cs ⊆ carrier G" and cfs: "wfactors G cs c"
using wfactors_exist [OF ccarr] by blast
note carr[simp] = pcarr acarr bcarr ccarr ascarr bscarr cscarr
from pirr cfs abpc have "wfactors G (p # cs) (a ⊗ b)"
by (simp add: wfactors_mult_single)
moreover have "wfactors G (as @ bs) (a ⊗ b)"
by (rule wfactors_mult [OF afs bfs]) fact+
ultimately have "essentially_equal G (p # cs) (as @ bs)"
by (rule wfactors_unique) simp+
then obtain ds where "p # cs <~~> ds" and dsassoc: "ds [∼] (as @ bs)"
by (fast elim: essentially_equalE)
then have "p ∈ set ds"
by (metis ‹mset (p # cs) = mset ds› insert_iff list.set(2) perm_set_eq)
with dsassoc obtain p' where "p' ∈ set (as@bs)" and pp': "p ∼ p'"
unfolding list_all2_conv_all_nth set_conv_nth by force
then consider "p' ∈ set as" | "p' ∈ set bs" by auto
then show "p divides a ∨ p divides b"
using afs bfs divides_cong_l pp' wfactors_dividesI
by (meson acarr ascarr bcarr bscarr pcarr)
qed
lemma (in factorial_monoid) factors_irreducible_prime:
assumes pirr: "irreducible G p" and pcarr: "p ∈ carrier G"
shows "prime G p"
proof (rule primeI)
show "p ∉ Units G"
by (meson irreducibleE pirr)
have irreduc: "⋀b. ⟦b ∈ carrier G; properfactor G b p⟧ ⟹ b ∈ Units G"
using pirr by (auto simp: irreducible_def)
show "p divides a ∨ p divides b"
if acarr: "a ∈ carrier G" and bcarr: "b ∈ carrier G" and pdvdab: "p divides (a ⊗ b)" for a b
proof -
from pdvdab obtain c where ccarr: "c ∈ carrier G" and abpc: "a ⊗ b = p ⊗ c"
by (rule dividesE)
note [simp] = pcarr acarr bcarr ccarr
show "p divides a ∨ p divides b"
proof (cases "a ∈ Units G")
case True
then have "p divides b"
by (metis acarr associatedI2' associated_def bcarr divides_trans m_comm pcarr pdvdab)
then show ?thesis ..
next
case anunit: False
show ?thesis
proof (cases "b ∈ Units G")
case True
then have "p divides a"
by (meson acarr bcarr divides_unit irreducible_prime pcarr pdvdab pirr prime_def)
then show ?thesis ..
next
case bnunit: False
then have cnunit: "c ∉ Units G"
by (metis abpc acarr anunit bcarr ccarr irreducible_prodE irreducible_prod_rI pcarr pirr)
then have abnunit: "a ⊗ b ∉ Units G"
using acarr anunit bcarr unit_factor by blast
obtain as where ascarr: "set as ⊆ carrier G" and afac: "factors G as a"
using factors_exist [OF acarr anunit] by blast
obtain bs where bscarr: "set bs ⊆ carrier G" and bfac: "factors G bs b"
using factors_exist [OF bcarr bnunit] by blast
obtain cs where cscarr: "set cs ⊆ carrier G" and cfac: "factors G cs c"
using factors_exist [OF ccarr cnunit] by auto
note [simp] = ascarr bscarr cscarr
from pirr cfac abpc have abfac': "factors G (p # cs) (a ⊗ b)"
by (simp add: factors_mult_single)
from afac and bfac have "factors G (as @ bs) (a ⊗ b)"
by (rule factors_mult) fact+
with abfac' have "essentially_equal G (p # cs) (as @ bs)"
using abnunit factors_unique by auto
then obtain ds where "p # cs <~~> ds" and dsassoc: "ds [∼] (as @ bs)"
by (fast elim: essentially_equalE)
then have "p ∈ set ds"
by (metis list.set_intros(1) set_mset_mset)
with dsassoc obtain p' where "p' ∈ set (as@bs)" and pp': "p ∼ p'"
unfolding list_all2_conv_all_nth set_conv_nth by force
then consider "p' ∈ set as" | "p' ∈ set bs" by auto
then show "p divides a ∨ p divides b"
by (meson afac bfac divides_cong_l factors_dividesI pp' ascarr bscarr pcarr)
qed
qed
qed
qed
subsection ‹Greatest Common Divisors and Lowest Common Multiples›
subsubsection ‹Definitions›
definition isgcd :: "[('a,_) monoid_scheme, 'a, 'a, 'a] ⇒ bool" ("(_ gcdofı _ _)" [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ı _ _)" [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 = Lattice.inf (division_rel G) A"
locale gcd_condition_monoid = comm_monoid_cancel +
assumes gcdof_exists: "⟦a ∈ carrier G; b ∈ carrier G⟧ ⟹ ∃c. c ∈ carrier G ∧ c gcdof a b"
locale primeness_condition_monoid = comm_monoid_cancel +
assumes irreducible_prime: "⟦a ∈ carrier G; irreducible G a⟧ ⟹ prime G a"
locale divisor_chain_condition_monoid = comm_monoid_cancel +
assumes division_wellfounded: "wf {(x, y). x ∈ carrier G ∧ y ∈ carrier G ∧ properfactor G x y}"
subsubsection ‹Connections to \texttt{Lattice.thy}›
lemma gcdof_greatestLower:
fixes G (structure)
assumes carr[simp]: "a ∈ carrier G" "b ∈ carrier G"
shows "(x ∈ carrier G ∧ x gcdof a b) = greatest (division_rel G) x (Lower (division_rel G) {a, b})"
by (auto simp: isgcd_def greatest_def Lower_def elem_def)
lemma lcmof_leastUpper:
fixes G (structure)
assumes carr[simp]: "a ∈ carrier G" "b ∈ carrier G"
shows "(x ∈ carrier G ∧ x lcmof a b) = least (division_rel G) x (Upper (division_rel G) {a, b})"
by (auto simp: islcm_def least_def Upper_def elem_def)
lemma somegcd_meet:
fixes G (structure)
assumes carr: "a ∈ carrier G" "b ∈ carrier G"
shows "somegcd G a b = meet (division_rel G) a b"
by (simp add: somegcd_def meet_def inf_def gcdof_greatestLower[OF carr])
lemma (in monoid) isgcd_divides_l:
assumes "a divides b"
and "a ∈ carrier G" "b ∈ carrier G"
shows "a gcdof a b"
using assms unfolding isgcd_def by fast
lemma (in monoid) isgcd_divides_r:
assumes "b divides a"
and "a ∈ carrier G" "b ∈ carrier G"
shows "b gcdof a b"
using assms unfolding isgcd_def by fast
subsubsection ‹Existence of gcd and lcm›
lemma (in factorial_monoid) gcdof_exists:
assumes acarr: "a ∈ carrier G"
and bcarr: "b ∈ carrier G"
shows "∃c. c ∈ carrier G ∧ c gcdof a b"
proof -
from wfactors_exist [OF acarr]
obtain as where ascarr: "set as ⊆ carrier G" and afs: "wfactors G as a"
by blast
from afs have airr: "∀a ∈ set as. irreducible G a"
by (fast elim: wfactorsE)
from wfactors_exist [OF bcarr]
obtain bs where bscarr: "set bs ⊆ carrier G" and bfs: "wfactors G bs b"
by blast
from bfs have birr: "∀b ∈ set bs. irreducible G b"
by (fast elim: wfactorsE)
have "∃c cs. c ∈ carrier G ∧ set cs ⊆ carrier G ∧ wfactors G cs c ∧
fmset G cs = fmset G as ∩# fmset G bs"
proof (intro mset_wfactorsEx)
fix X
assume "X ∈# fmset G as ∩# fmset G bs"
then have "X ∈# fmset G as" by simp
then have "X ∈ set (map (assocs G) as)"
by (simp add: fmset_def)
then have "∃x. X = assocs G x ∧ x ∈ set as"
by (induct as) auto
then obtain x where X: "X = assocs G x" and xas: "x ∈ set as"
by blast
with ascarr have xcarr: "x ∈ carrier G"
by blast
from xas airr have xirr: "irreducible G x"
by simp
from xcarr and xirr and X show "∃x. (x ∈ carrier G ∧ irreducible G x) ∧ X = assocs G x"
by blast
qed
then obtain c cs
where ccarr: "c ∈ carrier G"
and cscarr: "set cs ⊆ carrier G"
and csirr: "wfactors G cs c"
and csmset: "fmset G cs = fmset G as ∩# fmset G bs"
by auto
have "c gcdof a b"
proof (simp add: isgcd_def, safe)
from csmset
have "fmset G cs ⊆# fmset G as"
by simp
then show "c divides a" by (rule fmsubset_divides) fact+
next
from csmset have "fmset G cs ⊆# fmset G bs"
by simp
then show "c divides b"
by (rule fmsubset_divides) fact+
next
fix y
assume "y ∈ carrier G"
from wfactors_exist [OF this]
obtain ys where yscarr: "set ys ⊆ carrier G" and yfs: "wfactors G ys y"
by blast
assume "y divides a"
then have ya: "fmset G ys ⊆# fmset G as"
by (rule divides_fmsubset) fact+
assume "y divides b"
then have yb: "fmset G ys ⊆# fmset G bs"
by (rule divides_fmsubset) fact+
from ya yb csmset have "fmset G ys ⊆# fmset G cs"
by (simp add: subset_mset_def)
then show "y divides c"
by (rule fmsubset_divides) fact+
qed
with ccarr show "∃c. c ∈ carrier G ∧ c gcdof a b"
by fast
qed
lemma (in factorial_monoid) lcmof_exists:
assumes acarr: "a ∈ carrier G"
and bcarr: "b ∈ carrier G"
shows "∃c. c ∈ carrier G ∧ c lcmof a b"
proof -
from wfactors_exist [OF acarr]
obtain as where ascarr: "set as ⊆ carrier G" and afs: "wfactors G as a"
by blast
from afs have airr: "∀a ∈ set as. irreducible G a"
by (fast elim: wfactorsE)
from wfactors_exist [OF bcarr]
obtain bs where bscarr: "set bs ⊆ carrier G" and bfs: "wfactors G bs b"
by blast
from bfs have birr: "∀b ∈ set bs. irreducible G b"
by (fast elim: wfactorsE)
have "∃c cs. c ∈ carrier G ∧ set cs ⊆ carrier G ∧ wfactors G cs c ∧
fmset G cs = (fmset G as - fmset G bs) + fmset G bs"
proof (intro mset_wfactorsEx)
fix X
assume "X ∈# (fmset G as - fmset G bs) + fmset G bs"
then have "X ∈# fmset G as ∨ X ∈# fmset G bs"
by (auto dest: in_diffD)
then consider "X ∈ set_mset (fmset G as)" | "X ∈ set_mset (fmset G bs)"
by fast
then show "∃x. (x ∈ carrier G ∧ irreducible G x) ∧ X = assocs G x"
proof cases
case 1
then have "X ∈ set (map (assocs G) as)" by (simp add: fmset_def)
then have "∃x. x ∈ set as ∧ X = assocs G x" by (induct as) auto
then obtain x where xas: "x ∈ set as" and X: "X = assocs G x" by auto
with ascarr have xcarr: "x ∈ carrier G" by fast
from xas airr have xirr: "irreducible G x" by simp
from xcarr and xirr and X show ?thesis by fast
next
case 2
then have "X ∈ set (map (assocs G) bs)" by (simp add: fmset_def)
then have "∃x. x ∈ set bs ∧ X = assocs G x" by (induct as) auto
then obtain x where xbs: "x ∈ set bs" and X: "X = assocs G x" by auto
with bscarr have xcarr: "x ∈ carrier G" by fast
from xbs birr have xirr: "irreducible G x" by simp
from xcarr and xirr and X show ?thesis by fast
qed
qed
then obtain c cs
where ccarr: "c ∈ carrier G"
and cscarr: "set cs ⊆ carrier G"
and csirr: "wfactors G cs c"
and csmset: "fmset G cs = fmset G as - fmset G bs + fmset G bs"
by auto
have "c lcmof a b"
proof (simp add: islcm_def, safe)
from csmset have "fmset G as ⊆# fmset G cs"
by (simp add: subseteq_mset_def, force)
then show "a divides c"
by (rule fmsubset_divides) fact+
next
from csmset have "fmset G bs ⊆# fmset G cs"
by (simp add: subset_mset_def)
then show "b divides c"
by (rule fmsubset_divides) fact+
next
fix y
assume "y ∈ carrier G"
from wfactors_exist [OF this]
obtain ys where yscarr: "set ys ⊆ carrier G" and yfs: "wfactors G ys y"
by blast
assume "a divides y"
then have ya: "fmset G as ⊆# fmset G ys"
by (rule divides_fmsubset) fact+
assume "b divides y"
then have yb: "fmset G bs ⊆# fmset G ys"
by (rule divides_fmsubset) fact+
from ya yb csmset have "fmset G cs ⊆# fmset G ys"
using subset_eq_diff_conv subset_mset.le_diff_conv2 by fastforce
then show "c divides y"
by (rule fmsubset_divides) fact+
qed
with ccarr show "∃c. c ∈ carrier G ∧ c lcmof a b"
by fast
qed
subsection ‹Conditions for Factoriality›
subsubsection ‹Gcd condition›
lemma (in gcd_condition_monoid) division_weak_lower_semilattice [simp]:
"weak_lower_semilattice (division_rel G)"
proof -
interpret weak_partial_order "division_rel G" ..
show ?thesis
proof (unfold_locales, simp_all)
fix x y
assume carr: "x ∈ carrier G" "y ∈ carrier G"
from gcdof_exists [OF this] obtain z where zcarr: "z ∈ carrier G" and isgcd: "z gcdof x y"
by blast
with carr have "greatest (division_rel G) z (Lower (division_rel G) {x, y})"
by (subst gcdof_greatestLower[symmetric], simp+)
then show "∃z. greatest (division_rel G) z (Lower (division_rel G) {x, y})"
by fast
qed
qed
lemma (in gcd_condition_monoid) gcdof_cong_l:
assumes "a' ∼ a" "a gcdof b c" "a' ∈ carrier G" and carr': "a ∈ carrier G" "b ∈ carrier G" "c ∈ carrier G"
shows "a' gcdof b c"
proof -
interpret weak_lower_semilattice "division_rel G" by simp
have "is_glb (division_rel G) a' {b, c}"
by (subst greatest_Lower_cong_l[of _ a]) (simp_all add: assms gcdof_greatestLower[symmetric])
then have "a' ∈ carrier G ∧ a' gcdof b c"
by (simp add: gcdof_greatestLower carr')
then show ?thesis ..
qed
lemma (in gcd_condition_monoid) gcd_closed [simp]:
assumes "a ∈ carrier G" "b ∈ carrier G"
shows "somegcd G a b ∈ carrier G"
proof -
interpret weak_lower_semilattice "division_rel G" by simp
show ?thesis
using assms meet_closed by (simp add: somegcd_meet)
qed
lemma (in gcd_condition_monoid) gcd_isgcd:
assumes "a ∈ carrier G" "b ∈ carrier G"
shows "(somegcd G a b) gcdof a b"
proof -
interpret weak_lower_semilattice "division_rel G"
by simp
from assms have "somegcd G a b ∈ carrier G ∧ (somegcd G a b) gcdof a b"
by (simp add: gcdof_greatestLower inf_of_two_greatest meet_def somegcd_meet)
then show "(somegcd G a b) gcdof a b"
by simp
qed
lemma (in gcd_condition_monoid) gcd_exists:
assumes "a ∈ carrier G" "b ∈ carrier G"
shows "∃x∈carrier G. x = somegcd G a b"
proof -
interpret weak_lower_semilattice "division_rel G"
by simp
show ?thesis
by (metis assms gcd_closed)
qed
lemma (in gcd_condition_monoid) gcd_divides_l:
assumes "a ∈ carrier G" "b ∈ carrier G"
shows "(somegcd G a b) divides a"
proof -
interpret weak_lower_semilattice "division_rel G"
by simp
show ?thesis
by (metis assms gcd_isgcd isgcd_def)
qed
lemma (in gcd_condition_monoid) gcd_divides_r:
assumes "a ∈ carrier G" "b ∈ carrier G"
shows "(somegcd G a b) divides b"
proof -
interpret weak_lower_semilattice "division_rel G"
by simp
show ?thesis
by (metis assms gcd_isgcd isgcd_def)
qed
lemma (in gcd_condition_monoid) gcd_divides:
assumes "z divides x" "z divides y"
and L: "x ∈ carrier G" "y ∈ carrier G" "z ∈ carrier G"
shows "z divides (somegcd G x y)"
proof -
interpret weak_lower_semilattice "division_rel G"
by simp
show ?thesis
by (metis gcd_isgcd isgcd_def assms)
qed
lemma (in gcd_condition_monoid) gcd_cong_l:
assumes "x ∼ x'" "x ∈ carrier G" "x' ∈ carrier G" "y ∈ carrier G"
shows "somegcd G x y ∼ somegcd G x' y"
proof -
interpret weak_lower_semilattice "division_rel G"
by simp
show ?thesis
using somegcd_meet assms
by (metis eq_object.select_convs(1) meet_cong_l partial_object.select_convs(1))
qed
lemma (in gcd_condition_monoid) gcd_cong_r:
assumes "y ∼ y'" "x ∈ carrier G" "y ∈ carrier G" "y' ∈ carrier G"
shows "somegcd G x y ∼ somegcd G x y'"
proof -
interpret weak_lower_semilattice "division_rel G" by simp
show ?thesis
by (meson associated_def assms gcd_closed gcd_divides gcd_divides_l gcd_divides_r monoid.divides_trans monoid_axioms)
qed
lemma (in gcd_condition_monoid) gcdI:
assumes dvd: "a divides b" "a divides c"
and others: "⋀y. ⟦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"
proof -
have "∃a. a ∈ carrier G ∧ a gcdof b c"
by (simp add: bcarr ccarr gcdof_exists)
moreover have "⋀x. x ∈ carrier G ∧ x gcdof b c ⟹ a ∼ x"
by (simp add: acarr associated_def dvd isgcd_def others)
ultimately show ?thesis
unfolding somegcd_def by (blast intro: someI2_ex)
qed
lemma (in gcd_condition_monoid) gcdI2:
assumes "a gcdof b c" and "a ∈ carrier G" and "b ∈ carrier G" and "c ∈ carrier G"
shows "a ∼ somegcd G b c"
using assms unfolding isgcd_def
by (simp add: gcdI)
lemma (in gcd_condition_monoid) SomeGcd_ex:
assumes "finite A" "A ⊆ carrier G" "A ≠ {}"
shows "∃x ∈ carrier G. x = SomeGcd G A"
proof -
interpret weak_lower_semilattice "division_rel G"
by simp
show ?thesis
using finite_inf_closed by (simp add: assms SomeGcd_def)
qed
lemma (in gcd_condition_monoid) gcd_assoc:
assumes "a ∈ carrier G" "b ∈ carrier G" "c ∈ carrier G"
shows "somegcd G (somegcd G a b) c ∼ somegcd G a (somegcd G b c)"
proof -
interpret weak_lower_semilattice "division_rel G"
by simp
show ?thesis
unfolding associated_def
by (meson assms divides_trans gcd_divides gcd_divides_l gcd_divides_r gcd_exists)
qed
lemma (in gcd_condition_monoid) gcd_mult:
assumes acarr: "a ∈ carrier G" and bcarr: "b ∈ carrier G" and ccarr: "c ∈ carrier G"
shows "c ⊗ somegcd G a b ∼ somegcd G (c ⊗ a) (c ⊗ b)"
proof -
let ?d = "somegcd G a b"
let ?e = "somegcd G (c ⊗ a) (c ⊗ b)"
note carr[simp] = acarr bcarr ccarr
have dcarr: "?d ∈ carrier G" by simp
have ecarr: "?e ∈ carrier G" by simp
note carr = carr dcarr ecarr
have "?d divides a" by (simp add: gcd_divides_l)
then have cd'ca: "c ⊗ ?d divides (c ⊗ a)" by (simp add: divides_mult_lI)
have "?d divides b" by (simp add: gcd_divides_r)
then have cd'cb: "c ⊗ ?d divides (c ⊗ b)" by (simp add: divides_mult_lI)
from cd'ca cd'cb have cd'e: "c ⊗ ?d divides ?e"
by (rule gcd_divides) simp_all
then obtain u where ucarr[simp]: "u ∈ carrier G" and e_cdu: "?e = c ⊗ ?d ⊗ u"
by blast
note carr = carr ucarr
have "?e divides c ⊗ a" by (rule gcd_divides_l) simp_all
then obtain x where xcarr: "x ∈ carrier G" and ca_ex: "c ⊗ a = ?e ⊗ x"
by blast
with e_cdu have ca_cdux: "c ⊗ a = c ⊗ ?d ⊗ u ⊗ x"
by simp
from ca_cdux xcarr have "c ⊗ a = c ⊗ (?d ⊗ u ⊗ x)"
by (simp add: m_assoc)
then have "a = ?d ⊗ u ⊗ x"
by (rule l_cancel[of c a]) (simp add: xcarr)+
then have du'a: "?d ⊗ u divides a"
by (rule dividesI[OF xcarr])
have "?e divides c ⊗ b" by (intro gcd_divides_r) simp_all
then obtain x where xcarr: "x ∈ carrier G" and cb_ex: "c ⊗ b = ?e ⊗ x"
by blast
with e_cdu have cb_cdux: "c ⊗ b = c ⊗ ?d ⊗ u ⊗ x"
by simp
from cb_cdux xcarr have "c ⊗ b = c ⊗ (?d ⊗ u ⊗ x)"
by (simp add: m_assoc)
with xcarr have "b = ?d ⊗ u ⊗ x"
by (intro l_cancel[of c b]) simp_all
then have du'b: "?d ⊗ u divides b"
by (intro dividesI[OF xcarr])
from du'a du'b carr have du'd: "?d ⊗ u divides ?d"
by (intro gcd_divides) simp_all
then have uunit: "u ∈ Units G"
proof (elim dividesE)
fix v
assume vcarr[simp]: "v ∈ carrier G"
assume d: "?d = ?d ⊗ u ⊗ v"
have "?d ⊗ 𝟭 = ?d ⊗ u ⊗ v" by simp fact
also have "?d ⊗ u ⊗ v = ?d ⊗ (u ⊗ v)" by (simp add: m_assoc)
finally have "?d ⊗ 𝟭 = ?d ⊗ (u ⊗ v)" .
then have i2: "𝟭 = u ⊗ v" by (rule l_cancel) simp_all
then have i1: "𝟭 = v ⊗ u" by (simp add: m_comm)
from vcarr i1[symmetric] i2[symmetric] show "u ∈ Units G"
by (auto simp: Units_def)
qed
from e_cdu uunit have "somegcd G (c ⊗ a) (c ⊗ b) ∼ c ⊗ somegcd G a b"
by (intro associatedI2[of u]) simp_all
from this[symmetric] show "c ⊗ somegcd G a b ∼ somegcd G (c ⊗ a) (c ⊗ b)"
by simp
qed
lemma (in monoid) assoc_subst:
assumes ab: "a ∼ b"
and cP: "∀a b. a ∈ carrier G ∧ b ∈ carrier G ∧ a ∼ b
⟶ f a ∈ carrier G ∧ f b ∈ carrier G ∧ f a ∼ f b"
and carr: "a ∈ carrier G" "b ∈ carrier G"
shows "f a ∼ f b"
using assms by auto
lemma (in gcd_condition_monoid) relprime_mult:
assumes abrelprime: "somegcd G a b ∼ 𝟭"
and acrelprime: "somegcd G a c ∼ 𝟭"
and carr[simp]: "a ∈ carrier G" "b ∈ carrier G" "c ∈ carrier G"
shows "somegcd G a (b ⊗ c) ∼ 𝟭"
proof -
have "c = c ⊗ 𝟭" by simp
also from abrelprime[symmetric]
have "… ∼ c ⊗ somegcd G a b"
by (rule assoc_subst) (simp add: mult_cong_r)+
also have "… ∼ somegcd G (c ⊗ a) (c ⊗ b)"
by (rule gcd_mult) fact+
finally have c: "c ∼ somegcd G (c ⊗ a) (c ⊗ b)"
by simp
from carr have a: "a ∼ somegcd G a (c ⊗ a)"
by (fast intro: gcdI divides_prod_l)
have "somegcd G a (b ⊗ c) ∼ somegcd G a (c ⊗ b)"
by (simp add: m_comm)
also from a have "… ∼ somegcd G (somegcd G a (c ⊗ a)) (c ⊗ b)"
by (rule assoc_subst) (simp add: gcd_cong_l)+
also from gcd_assoc have "… ∼ somegcd G a (somegcd G (c ⊗ a) (c ⊗ b))"
by (rule assoc_subst) simp+
also from c[symmetric] have "… ∼ somegcd G a c"
by (rule assoc_subst) (simp add: gcd_cong_r)+
also note acrelprime
finally show "somegcd G a (b ⊗ c) ∼ 𝟭"
by simp
qed
lemma (in gcd_condition_monoid) primeness_condition: "primeness_condition_monoid G"
proof -
have *: "p divides a ∨ p divides b"
if pcarr[simp]: "p ∈ carrier G" and acarr[simp]: "a ∈ carrier G" and bcarr[simp]: "b ∈ carrier G"
and pirr: "irreducible G p" and pdvdab: "p divides a ⊗ b"
for p a b
proof -
from pirr have pnunit: "p ∉ Units G"
and r: "⋀b. ⟦b ∈ carrier G; properfactor G b p⟧ ⟹ b ∈ Units G"
by (fast elim: irreducibleE)+
show "p divides a ∨ p divides b"
proof (rule ccontr, clarsimp)
assume npdvda: "¬ p divides a" and npdvdb: "¬ p divides b"
have "𝟭 ∼ somegcd G p a"
proof (intro gcdI unit_divides)
show "⋀y. ⟦y ∈ carrier G; y divides p; y divides a⟧ ⟹ y ∈ Units G"
by (meson divides_trans npdvda pcarr properfactorI r)
qed auto
with pcarr acarr have pa: "somegcd G p a ∼ 𝟭"
by (fast intro: associated_sym[of "𝟭"] gcd_closed)
have "𝟭 ∼ somegcd G p b"
proof (intro gcdI unit_divides)
show "⋀y. ⟦y ∈ carrier G; y divides p; y divides b⟧ ⟹ y ∈ Units G"
by (meson divides_trans npdvdb pcarr properfactorI r)
qed auto
with pcarr bcarr have pb: "somegcd G p b ∼ 𝟭"
by (fast intro: associated_sym[of "𝟭"] gcd_closed)
have "p ∼ somegcd G p (a ⊗ b)"
using pdvdab by (simp add: gcdI2 isgcd_divides_l)
also from pa pb pcarr acarr bcarr have "somegcd G p (a ⊗ b) ∼ 𝟭"
by (rule relprime_mult)
finally have "p ∼ 𝟭"
by simp
with pcarr have "p ∈ Units G"
by (fast intro: assoc_unit_l)
with pnunit show False ..
qed
qed
show ?thesis
by unfold_locales (metis * primeI irreducibleE)
qed
sublocale gcd_condition_monoid ⊆ primeness_condition_monoid
by (rule primeness_condition)
subsubsection ‹Divisor chain condition›
lemma (in divisor_chain_condition_monoid) wfactors_exist:
assumes acarr: "a ∈ carrier G"
shows "∃as. set as ⊆ carrier G ∧ wfactors G as a"
proof -
have r: "a ∈ carrier G ⟹ (∃as. set as ⊆ carrier G ∧ wfactors G as a)"
using division_wellfounded
proof (induction rule: wf_induct_rule)
case (less x)
then have xcarr: "x ∈ carrier G"
by auto
show ?case
proof (cases "x ∈ Units G")
case True
then show ?thesis
by (metis bot.extremum list.set(1) unit_wfactors)
next
case xnunit: False
show ?thesis
proof (cases "irreducible G x")
case True
then show ?thesis
by (rule_tac x="[x]" in exI) (simp add: wfactors_def xcarr)
next
case False
then obtain y where ycarr: "y ∈ carrier G" and ynunit: "y ∉ Units G" and pfyx: "properfactor G y x"
by (meson irreducible_def xnunit)
obtain ys where yscarr: "set ys ⊆ carrier G" and yfs: "wfactors G ys y"
using less ycarr pfyx by blast
then obtain z where zcarr: "z ∈ carrier G" and x: "x = y ⊗ z"
by (meson dividesE pfyx properfactorE2)
from zcarr ycarr have "properfactor G z x"
using m_comm properfactorI3 x ynunit by blast
with less zcarr obtain zs where zscarr: "set zs ⊆ carrier G" and zfs: "wfactors G zs z"
by blast
from yscarr zscarr have xscarr: "set (ys@zs) ⊆ carrier G"
by simp
have "wfactors G (ys@zs) (y⊗z)"
using xscarr ycarr yfs zcarr zfs by auto
then have "wfactors G (ys@zs) x"
by (simp add: x)
with xscarr show "∃xs. set xs ⊆ carrier G ∧ wfactors G xs x"
by fast
qed
qed
qed
from acarr show ?thesis by (rule r)
qed
subsubsection ‹Primeness condition›
lemma (in comm_monoid_cancel) multlist_prime_pos:
assumes aprime: "prime G a" and carr: "a ∈ carrier G"
and as: "set as ⊆ carrier G" "a divides (foldr (⊗) as 𝟭)"
shows "∃i<length as. a divides (as!i)"
using as
proof (induction as)
case Nil
then show ?case
by simp (meson Units_one_closed aprime carr divides_unit primeE)
next
case (Cons x as)
then have "x ∈ carrier G" "set as ⊆ carrier G" and "a divides x ⊗ foldr (⊗) as 𝟭"
by auto
with carr aprime have "a divides x ∨ a divides foldr (⊗) as 𝟭"
by (intro prime_divides) simp+
then show ?case
using Cons.IH Cons.prems(1) by force
qed
proposition (in primeness_condition_monoid) wfactors_unique:
assumes "wfactors G as a" "wfactors G as' a"
and "a ∈ carrier G" "set as ⊆ carrier G" "set as' ⊆ carrier G"
shows "essentially_equal G as as'"
using assms
proof (induct as arbitrary: a as')
case Nil
then have "a ∼ 𝟭"
by (simp add: perm_wfactorsD)
then have "as' = []"
using Nil.prems assoc_unit_l unit_wfactors_empty by blast
then show ?case
by auto
next
case (Cons ah as)
then have ahdvda: "ah divides a"
using wfactors_dividesI by auto
then obtain a' where a'carr: "a' ∈ carrier G" and a: "a = ah ⊗ a'"
by blast
have carr_ah: "ah ∈ carrier G" "set as ⊆ carrier G"
using Cons.prems by fastforce+
have "ah ⊗ foldr (⊗) as 𝟭 ∼ a"
by (rule wfactorsE[OF ‹wfactors G (ah # as) a›]) auto
then have "foldr (⊗) as 𝟭 ∼ a'"
by (metis Cons.prems(4) a a'carr assoc_l_cancel insert_subset list.set(2) monoid.multlist_closed monoid_axioms)
then
have a'fs: "wfactors G as a'"
by (meson Cons.prems(1) set_subset_Cons subset_iff wfactorsE wfactorsI)
then have ahirr: "irreducible G ah"
by (meson Cons.prems(1) list.set_intros(1) wfactorsE)
with Cons have ahprime: "prime G ah"
by (simp add: irreducible_prime)
note ahdvda
also have "a divides (foldr (⊗) as' 𝟭)"
by (meson Cons.prems(2) associatedE wfactorsE)
finally have "ah divides (foldr (⊗) as' 𝟭)"
using Cons.prems(4) by auto
with ahprime have "∃i<length as'. ah divides as'!i"
by (intro multlist_prime_pos) (use Cons.prems in auto)
then obtain i where len: "i<length as'" and ahdvd: "ah divides as'!i"
by blast
then obtain x where "x ∈ carrier G" and asi: "as'!i = ah ⊗ x"
by blast
have irrasi: "irreducible G (as'!i)"
using nth_mem[OF len] wfactorsE
by (metis Cons.prems(2))
have asicarr[simp]: "as'!i ∈ carrier G"
using len ‹set as' ⊆ carrier G› nth_mem by blast
have asiah: "as'!i ∼ ah"
by (metis ‹ah ∈ carrier G› ‹x ∈ carrier G› asi irrasi ahprime associatedI2 irreducible_prodE primeE)
note setparts = set_take_subset[of i as'] set_drop_subset[of "Suc i" as']
have "∃aa_1. aa_1 ∈ carrier G ∧ wfactors G (take i as') aa_1"
using Cons
by (metis setparts(1) subset_trans in_set_takeD wfactorsE wfactors_prod_exists)
then obtain aa_1 where aa1carr [simp]: "aa_1 ∈ carrier G" and aa1fs: "wfactors G (take i as') aa_1"
by auto
obtain aa_2 where aa2carr [simp]: "aa_2 ∈ carrier G"
and aa2fs: "wfactors G (drop (Suc i) as') aa_2"
by (metis Cons.prems(2) Cons.prems(5) subset_code(1) in_set_dropD wfactors_def wfactors_prod_exists)
have set_drop: "set (drop (Suc i) as') ⊆ carrier G"
using Cons.prems(5) setparts(2) by blast
moreover have set_take: "set (take i as') ⊆ carrier G"
using Cons.prems(5) setparts by auto
moreover have v1: "wfactors G (take i as' @ drop (Suc i) as') (aa_1 ⊗ aa_2)"
using aa1fs aa2fs ‹set as' ⊆ carrier G› by (force simp add: dest: in_set_takeD in_set_dropD)
ultimately have v1': "wfactors G (as'!i # take i as' @ drop (Suc i) as') (as'!i ⊗ (aa_1 ⊗ aa_2))"
using irrasi wfactors_mult_single
by (simp add: irrasi v1 wfactors_mult_single)
have "wfactors G (as'!i # drop (Suc i) as') (as'!i ⊗ aa_2)"
by (simp add: aa2fs irrasi set_drop wfactors_mult_single)
with len aa1carr aa2carr aa1fs
have v2: "wfactors G (take i as' @ as'!i # drop (Suc i) as') (aa_1 ⊗ (as'!i ⊗ aa_2))"
using wfactors_mult by (simp add: set_take set_drop)
from len have as': "as' = (take i as' @ as'!i # drop (Suc i) as')"
by (simp add: Cons_nth_drop_Suc)
have eer: "essentially_equal G (take i as' @ as'!i # drop (Suc i) as') as'"
using Cons.prems(5) as' by auto
with v2 aa1carr aa2carr nth_mem[OF len] have "aa_1 ⊗ (as'!i ⊗ aa_2) ∼ a"
using Cons.prems as' comm_monoid_cancel.ee_wfactorsD is_comm_monoid_cancel by fastforce
then have t1: "as'!i ⊗ (aa_1 ⊗ aa_2) ∼ a"
by (metis aa1carr aa2carr asicarr m_lcomm)
from asiah have "ah ⊗ (aa_1 ⊗ aa_2) ∼ as'!i ⊗ (aa_1 ⊗ aa_2)"
by (simp add: ‹ah ∈ carrier G› associated_sym mult_cong_l)
also note t1
finally have "ah ⊗ (aa_1 ⊗ aa_2) ∼ a"
using Cons.prems(3) carr_ah aa1carr aa2carr by blast
with aa1carr aa2carr a'carr nth_mem[OF len] have a': "aa_1 ⊗ aa_2 ∼ a'"
using a assoc_l_cancel carr_ah(1) by blast
note v1
also note a'
finally have "wfactors G (take i as' @ drop (Suc i) as') a'"
by (simp add: a'carr set_drop set_take)
from a'fs this have "essentially_equal G as (take i as' @ drop (Suc i) as')"
using Cons.hyps a'carr carr_ah(2) set_drop set_take by auto
then obtain bs where ‹mset as = mset bs› ‹bs [∼] take i as' @ drop (Suc i) as'›
by (auto simp add: essentially_equal_def)
with carr_ah have ‹mset (ah # as) = mset (ah # bs)› ‹ah # bs [∼] ah # take i as' @ drop (Suc i) as'›
by simp_all
then have ee1: "essentially_equal G (ah # as) (ah # take i as' @ drop (Suc i) as')"
unfolding essentially_equal_def by blast
have ee2: "essentially_equal G (ah # take i as' @ drop (Suc i) as')
(as' ! i # take i as' @ drop (Suc i) as')"
proof (intro essentially_equalI)
show "ah # take i as' @ drop (Suc i) as' <~~> ah # take i as' @ drop (Suc i) as'"
by simp
next
show "ah # take i as' @ drop (Suc i) as' [∼] as' ! i # take i as' @ drop (Suc i) as'"
by (simp add: asiah associated_sym set_drop set_take)
qed
note ee1
also note ee2
also have "essentially_equal G (as' ! i # take i as' @ drop (Suc i) as')
(take i as' @ as' ! i # drop (Suc i) as')"
by (metis Cons.prems(5) as' essentially_equalI listassoc_refl perm_append_Cons)
finally have "essentially_equal G (ah # as) (take i as' @ as' ! i # drop (Suc i) as')"
using Cons.prems(4) set_drop set_take by auto
then show ?case
using as' by auto
qed
subsubsection ‹Application to factorial monoids›
text ‹Number of factors for wellfoundedness›
definition factorcount :: "_ ⇒ 'a ⇒ nat"
where "factorcount G a =
(THE c. ∀as. set as ⊆ carrier G ∧ wfactors G as a ⟶ c = length as)"
lemma (in monoid) ee_length:
assumes ee: "essentially_equal G as bs"
shows "length as = length bs"
by (rule essentially_equalE[OF ee]) (metis list_all2_conv_all_nth perm_length)
lemma (in factorial_monoid) factorcount_exists:
assumes carr[simp]: "a ∈ carrier G"
shows "∃c. ∀as. set as ⊆ carrier G ∧ wfactors G as a ⟶ c = length as"
proof -
have "∃as. set as ⊆ carrier G ∧ wfactors G as a"
by (intro wfactors_exist) simp
then obtain as where ascarr[simp]: "set as ⊆ carrier G" and afs: "wfactors G as a"
by (auto simp del: carr)
have "∀as'. set as' ⊆ carrier G ∧ wfactors G as' a ⟶ length as = length as'"
by (metis afs ascarr assms ee_length wfactors_unique)
then show "∃c. ∀as'. set as' ⊆ carrier G ∧ wfactors G as' a ⟶ c = length as'" ..
qed
lemma (in factorial_monoid) factorcount_unique:
assumes afs: "wfactors G as a"
and acarr[simp]: "a ∈ carrier G" and ascarr: "set as ⊆ carrier G"
shows "factorcount G a = length as"
proof -
have "∃ac. ∀as. set as ⊆ carrier G ∧ wfactors G as a ⟶ ac = length as"
by (rule factorcount_exists) simp
then obtain ac where alen: "∀as. set as ⊆ carrier G ∧ wfactors G as a ⟶ ac = length as"
by auto
then have ac: "ac = factorcount G a"
unfolding factorcount_def using ascarr by (blast intro: theI2 afs)
from ascarr afs have "ac = length as"
by (simp add: alen)
with ac show ?thesis
by simp
qed
lemma (in factorial_monoid) divides_fcount:
assumes dvd: "a divides b"
and acarr: "a ∈ carrier G"
and bcarr:"b ∈ carrier G"
shows "factorcount G a ≤ factorcount G b"
proof (rule dividesE[OF dvd])
fix c
from assms have "∃as. set as ⊆ carrier G ∧ wfactors G as a"
by blast
then obtain as where ascarr: "set as ⊆ carrier G" and afs: "wfactors G as a"
by blast
with acarr have fca: "factorcount G a = length as"
by (intro factorcount_unique)
assume ccarr: "c ∈ carrier G"
then have "∃cs. set cs ⊆ carrier G ∧ wfactors G cs c"
by blast
then obtain cs where cscarr: "set cs ⊆ carrier G" and cfs: "wfactors G cs c"
by blast
note [simp] = acarr bcarr ccarr ascarr cscarr
assume b: "b = a ⊗ c"
from afs cfs have "wfactors G (as@cs) (a ⊗ c)"
by (intro wfactors_mult) simp_all
with b have "wfactors G (as@cs) b"
by simp
then have "factorcount G b = length (as@cs)"
by (intro factorcount_unique) simp_all
then have "factorcount G b = length as + length cs"
by simp
with fca show ?thesis
by simp
qed
lemma (in factorial_monoid) associated_fcount:
assumes acarr: "a ∈ carrier G"
and bcarr: "b ∈ carrier G"
and asc: "a ∼ b"
shows "factorcount G a = factorcount G b"
using assms
by (auto simp: associated_def factorial_monoid.divides_fcount factorial_monoid_axioms le_antisym)
lemma (in factorial_monoid) properfactor_fcount:
assumes acarr: "a ∈ carrier G" and bcarr:"b ∈ carrier G"
and pf: "properfactor G a b"
shows "factorcount G a < factorcount G b"
proof (rule properfactorE[OF pf], elim dividesE)
fix c
from assms have "∃as. set as ⊆ carrier G ∧ wfactors G as a"
by blast
then obtain as where ascarr: "set as ⊆ carrier G" and afs: "wfactors G as a"
by blast
with acarr have fca: "factorcount G a = length as"
by (intro factorcount_unique)
assume ccarr: "c ∈ carrier G"
then have "∃cs. set cs ⊆ carrier G ∧ wfactors G cs c"
by blast
then obtain cs where cscarr: "set cs ⊆ carrier G" and cfs: "wfactors G cs c"
by blast
assume b: "b = a ⊗ c"
have "wfactors G (as@cs) (a ⊗ c)"
by (rule wfactors_mult) fact+
with b have "wfactors G (as@cs) b"
by simp
with ascarr cscarr bcarr have "factorcount G b = length (as@cs)"
by (simp add: factorcount_unique)
then have fcb: "factorcount G b = length as + length cs"
by simp
assume nbdvda: "¬ b divides a"
have "c ∉ Units G"
proof
assume cunit:"c ∈ Units G"
have "b ⊗ inv c = a ⊗ c ⊗ inv c"
by (simp add: b)
also from ccarr acarr cunit have "… = a ⊗ (c ⊗ inv c)"
by (fast intro: m_assoc)
also from ccarr cunit have "… = a ⊗ 𝟭" by simp
also from acarr have "… = a" by simp
finally have "a = b ⊗ inv c" by simp
with ccarr cunit have "b divides a"
by (fast intro: dividesI[of "inv c"])
with nbdvda show False by simp
qed
with cfs have "length cs > 0"
by (metis Units_one_closed assoc_unit_r ccarr foldr.simps(1) id_apply length_greater_0_conv wfactors_def)
with fca fcb show ?thesis
by simp
qed
sublocale factorial_monoid ⊆ divisor_chain_condition_monoid
apply unfold_locales
apply (rule wfUNIVI)
apply (rule measure_induct[of "factorcount G"])
using properfactor_fcount by auto
sublocale factorial_monoid ⊆ primeness_condition_monoid
by standard (rule irreducible_prime)
lemma (in factorial_monoid) primeness_condition: "primeness_condition_monoid G" ..
lemma (in factorial_monoid) gcd_condition [simp]: "gcd_condition_monoid G"
by standard (rule gcdof_exists)
sublocale factorial_monoid ⊆ gcd_condition_monoid
by standard (rule gcdof_exists)
lemma (in factorial_monoid) division_weak_lattice [simp]: "weak_lattice (division_rel G)"
proof -
interpret weak_lower_semilattice "division_rel G"
by simp
show "weak_lattice (division_rel G)"
proof (unfold_locales, simp_all)
fix x y
assume carr: "x ∈ carrier G" "y ∈ carrier G"
from lcmof_exists [OF this] obtain z where zcarr: "z ∈ carrier G" and isgcd: "z lcmof x y"
by blast
with carr have "least (division_rel G) z (Upper (division_rel G) {x, y})"
by (simp add: lcmof_leastUpper[symmetric])
then show "∃z. least (division_rel G) z (Upper (division_rel G) {x, y})"
by blast
qed
qed
subsection ‹Factoriality Theorems›
theorem factorial_condition_one:
"divisor_chain_condition_monoid G ∧ primeness_condition_monoid G ⟷ factorial_monoid G"
proof (rule iffI, clarify)
assume dcc: "divisor_chain_condition_monoid G"
and pc: "primeness_condition_monoid G"
interpret divisor_chain_condition_monoid "G" by (rule dcc)
interpret primeness_condition_monoid "G" by (rule pc)
show "factorial_monoid G"
by (fast intro: factorial_monoidI wfactors_exist wfactors_unique)
next
assume "factorial_monoid G"
then interpret factorial_monoid "G" .
show "divisor_chain_condition_monoid G ∧ primeness_condition_monoid G"
by rule unfold_locales
qed
theorem factorial_condition_two:
"divisor_chain_condition_monoid G ∧ gcd_condition_monoid G ⟷ factorial_monoid G"
proof (rule iffI, clarify)
assume dcc: "divisor_chain_condition_monoid G"
and gc: "gcd_condition_monoid G"
interpret divisor_chain_condition_monoid "G" by (rule dcc)
interpret gcd_condition_monoid "G" by (rule gc)
show "factorial_monoid G"
by (simp add: factorial_condition_one[symmetric], rule, unfold_locales)
next
assume "factorial_monoid G"
then interpret factorial_monoid "G" .
show "divisor_chain_condition_monoid G ∧ gcd_condition_monoid G"
by rule unfold_locales
qed
end