(* Title: HOL/Algebra/Divisibility.thy Author: Clemens Ballarin Author: Stephan Hohe *) section ‹Divisibility in monoids and rings› theory Divisibility imports "HOL-Combinatorics.List_Permutation" Coset Group begin section ‹Factorial Monoids› subsection ‹Monoids with Cancellation Law› locale monoid_cancel = monoid + assumes l_cancel: "⟦c ⊗ a = c ⊗ b; a ∈ carrier G; b ∈ carrier G; c ∈ carrier G⟧ ⟹ a = b" and r_cancel: "⟦a ⊗ c = b ⊗ c; a ∈ carrier G; b ∈ carrier G; c ∈ carrier G⟧ ⟹ a = b" lemma (in monoid) monoid_cancelI: assumes l_cancel: "⋀a b c. ⟦c ⊗ a = c ⊗ b; a ∈ carrier G; b ∈ carrier G; c ∈ carrier G⟧ ⟹ a = b" and r_cancel: "⋀a b c. ⟦a ⊗ c = b ⊗ c; a ∈ carrier G; b ∈ carrier G; c ∈ carrier G⟧ ⟹ a = b" shows "monoid_cancel G" by standard fact+ lemma (in monoid_cancel) is_monoid_cancel: "monoid_cancel G" .. sublocale group ⊆ monoid_cancel by standard simp_all locale comm_monoid_cancel = monoid_cancel + comm_monoid lemma comm_monoid_cancelI: fixes G (structure) assumes "comm_monoid G" assumes cancel: "⋀a b c. ⟦a ⊗ c = b ⊗ c; a ∈ carrier G; b ∈ carrier G; c ∈ carrier G⟧ ⟹ a = b" shows "comm_monoid_cancel G" proof - interpret comm_monoid G by fact show "comm_monoid_cancel G" by unfold_locales (metis assms(2) m_ac(2))+ qed lemma (in comm_monoid_cancel) is_comm_monoid_cancel: "comm_monoid_cancel G" by intro_locales sublocale comm_group ⊆ comm_monoid_cancel .. subsection ‹Products of Units in Monoids› lemma (in monoid) prod_unit_l: assumes abunit[simp]: "a ⊗ b ∈ Units G" and aunit[simp]: "a ∈ Units G" and carr[simp]: "a ∈ carrier G" "b ∈ carrier G" shows "b ∈ Units G" proof - have c: "inv (a ⊗ b) ⊗ a ∈ carrier G" by simp have "(inv (a ⊗ b) ⊗ a) ⊗ b = inv (a ⊗ b) ⊗ (a ⊗ b)" by (simp add: m_assoc) also have "… = 𝟭" by simp finally have li: "(inv (a ⊗ b) ⊗ a) ⊗ b = 𝟭" . have "𝟭 = inv a ⊗ a" by (simp add: Units_l_inv[symmetric]) also have "… = inv a ⊗ 𝟭 ⊗ a" by simp also have "… = inv a ⊗ ((a ⊗ b) ⊗ inv (a ⊗ b)) ⊗ a" by (simp add: Units_r_inv[OF abunit, symmetric] del: Units_r_inv) also have "… = ((inv a ⊗ a) ⊗ b) ⊗ inv (a ⊗ b) ⊗ a" by (simp add: m_assoc del: Units_l_inv) also have "… = b ⊗ inv (a ⊗ b) ⊗ a" by simp also have "… = b ⊗ (inv (a ⊗ b) ⊗ a)" by (simp add: m_assoc) finally have ri: "b ⊗ (inv (a ⊗ b) ⊗ a) = 𝟭 " by simp from c li ri show "b ∈ Units G" by (auto simp: Units_def) qed lemma (in monoid) prod_unit_r: assumes abunit[simp]: "a ⊗ b ∈ Units G" and bunit[simp]: "b ∈ Units G" and carr[simp]: "a ∈ carrier G" "b ∈ carrier G" shows "a ∈ Units G" proof - have c: "b ⊗ inv (a ⊗ b) ∈ carrier G" by simp have "a ⊗ (b ⊗ inv (a ⊗ b)) = (a ⊗ b) ⊗ inv (a ⊗ b)" by (simp add: m_assoc del: Units_r_inv) also have "… = 𝟭" by simp finally have li: "a ⊗ (b ⊗ inv (a ⊗ b)) = 𝟭" . have "𝟭 = b ⊗ inv b" by (simp add: Units_r_inv[symmetric]) also have "… = b ⊗ 𝟭 ⊗ inv b" by simp also have "… = b ⊗ (inv (a ⊗ b) ⊗ (a ⊗ b)) ⊗ inv b" by (simp add: Units_l_inv[OF abunit, symmetric] del: Units_l_inv) also have "… = (b ⊗ inv (a ⊗ b) ⊗ a) ⊗ (b ⊗ inv b)" by (simp add: m_assoc del: Units_l_inv) also have "… = b ⊗ inv (a ⊗ b) ⊗ a" by simp finally have ri: "(b ⊗ inv (a ⊗ b)) ⊗ a = 𝟭 " by simp from c li ri show "a ∈ Units G" by (auto simp: Units_def) qed lemma (in comm_monoid) unit_factor: assumes abunit: "a ⊗ b ∈ Units G" and [simp]: "a ∈ carrier G" "b ∈ carrier G" shows "a ∈ Units G" using abunit[simplified Units_def] proof clarsimp fix i assume [simp]: "i ∈ carrier G" have carr': "b ⊗ i ∈ carrier G" by simp have "(b ⊗ i) ⊗ a = (i ⊗ b) ⊗ a" by (simp add: m_comm) also have "… = i ⊗ (b ⊗ a)" by (simp add: m_assoc) also have "… = i ⊗ (a ⊗ b)" by (simp add: m_comm) also assume "i ⊗ (a ⊗ b) = 𝟭" finally have li': "(b ⊗ i) ⊗ a = 𝟭" . have "a ⊗ (b ⊗ i) = a ⊗ b ⊗ i" by (simp add: m_assoc) also assume "a ⊗ b ⊗ i = 𝟭" finally have ri': "a ⊗ (b ⊗ i) = 𝟭" . from carr' li' ri' show "a ∈ Units G" by (simp add: Units_def, fast) qed subsection ‹Divisibility and Association› subsubsection ‹Function definitions› definition factor :: "[_, 'a, 'a] ⇒ bool" (infix "dividesı" 65) where "a 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: ✐‹contributor ‹Paulo Emílio de Vilhena›› assumes "prime G p" shows "irreducible G p" proof (rule irreducibleI) show "p ∉ Units G" using assms unfolding prime_def by simp next fix b assume A: "b ∈ carrier G" "properfactor G b p" then obtain c where c: "c ∈ carrier G" "p = b ⊗ c" unfolding properfactor_def factor_def by auto hence "p divides c" using A assms unfolding prime_def properfactor_def by auto then obtain b' where b': "b' ∈ carrier G" "c = p ⊗ b'" unfolding factor_def by auto hence "𝟭 = b ⊗ b'" by (metis A(1) l_cancel m_closed m_lcomm one_closed r_one c) thus "b ∈ Units G" using A(1) Units_one_closed b'(1) unit_factor by presburger qed lemma (in comm_monoid_cancel) prime_pow_divides_iff: assumes "p ∈ carrier G" "a ∈ carrier G" "b ∈ carrier G" and "prime G p" and "¬ (p divides a)" shows "(p [^] (n :: nat)) divides (a ⊗ b) ⟷ (p [^] n) divides b" proof assume "(p [^] n) divides b" thus "(p [^] n) divides (a ⊗ b)" using divides_prod_l[of "p [^] n" b a] assms by simp next assume "(p [^] n) divides (a ⊗ b)" thus "(p [^] n) divides b" proof (induction n) case 0 with ‹b ∈ carrier G› show ?case by (simp add: unit_divides) next case (Suc n) hence "(p [^] n) divides (a ⊗ b)" and "(p [^] n) divides b" using assms(1) divides_prod_r by auto with ‹(p [^] (Suc n)) divides (a ⊗ b)› obtain c d where c: "c ∈ carrier G" and "b = (p [^] n) ⊗ c" and d: "d ∈ carrier G" and "a ⊗ b = (p [^] (Suc n)) ⊗ d" using assms by blast hence "(p [^] n) ⊗ (a ⊗ c) = (p [^] n) ⊗ (p ⊗ d)" using assms by (simp add: m_assoc m_lcomm) hence "a ⊗ c = p ⊗ d" using c d assms(1) assms(2) l_cancel by blast with ‹¬ (p divides a)› and ‹prime G p› have "p divides c" by (metis assms(2) c d dividesI' prime_divides) with ‹b = (p [^] n) ⊗ c› show ?case using assms(1) c by simp qed qed subsection ‹Factorization and Factorial Monoids› subsubsection ‹Function definitions› definition factors :: "('a, _) monoid_scheme ⇒ 'a list ⇒ 'a ⇒ bool" where "factors G fs a ⟷ (∀x ∈ (set fs). irreducible G x) ∧ foldr (⊗⇘G⇙) fs 𝟭⇘G⇙ = a" definition wfactors ::"('a, _) monoid_scheme ⇒ 'a list ⇒ 'a ⇒ bool" where "wfactors G fs a ⟷ (∀x ∈ (set fs). irreducible G x) ∧ foldr (⊗⇘G⇙) fs 𝟭⇘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› (* FIXME: use class_of x instead of closure_of {x} *) abbreviation "assocs G x ≡ eq_closure_of (division_rel G) {x}" definition "fmset G as = mset (map (assocs G) as)" text ‹Helper lemmas› lemma (in monoid) assocs_repr_independence: assumes "y ∈ assocs G x" "x ∈ carrier G" shows "assocs G x = assocs G y" using assms by (simp add: eq_closure_of_def elem_def) (use associated_sym associated_trans in ‹blast+›) lemma (in monoid) assocs_self: assumes "x ∈ carrier G" shows "x ∈ assocs G x" using assms by (fastforce intro: closure_ofI2) lemma (in monoid) assocs_repr_independenceD: assumes repr: "assocs G x = assocs G y" and ycarr: "y ∈ carrier G" shows "y ∈ assocs G x" unfolding repr using ycarr by (intro assocs_self) lemma (in comm_monoid) assocs_assoc: assumes "a ∈ assocs G b" "b ∈ carrier G" shows "a ∼ b" using assms by (elim closure_ofE2) simp lemmas (in comm_monoid) assocs_eqD = assocs_repr_independenceD[THEN assocs_assoc] subsubsection ‹Comparing multisets› lemma (in monoid) fmset_perm_cong: assumes prm: "as <~~> bs" shows "fmset G as = fmset G bs" using perm_map[OF prm] unfolding fmset_def by blast lemma (in comm_monoid_cancel) eqc_listassoc_cong: assumes "as [∼] bs" and "set as ⊆ carrier G" and "set bs ⊆ carrier G" shows "map (assocs G) as = map (assocs G) bs" using assms proof (induction as arbitrary: bs) case Nil then show ?case by simp next case (Cons a as) then show ?case proof (clarsimp simp add: Cons_eq_map_conv list_all2_Cons1) fix z zs assume zzs: "a ∈ carrier G" "set as ⊆ carrier G" "bs = z # zs" "a ∼ z" "as [∼] zs" "z ∈ carrier G" "set zs ⊆ carrier G" then show "assocs G a = assocs G z" apply (simp add: eq_closure_of_def elem_def) using ‹a ∈ carrier G› ‹z ∈ carrier G› ‹a ∼ z› associated_sym associated_trans by blast+ qed qed lemma (in comm_monoid_cancel) fmset_listassoc_cong: assumes "as [∼] bs" and "set as ⊆ carrier G" and "set bs ⊆ carrier G" shows "fmset G as = fmset G bs" using assms unfolding fmset_def by (simp add: eqc_listassoc_cong) lemma (in comm_monoid_cancel) ee_fmset: assumes ee: "essentially_equal G as bs" and ascarr: "set as ⊆ carrier G" and bscarr: "set bs ⊆ carrier G" shows "fmset G as = fmset G bs" using ee thm essentially_equal_def proof (elim essentially_equalE) fix as' assume prm: "as <~~> as'" from prm ascarr have as'carr: "set as' ⊆ carrier G" by (rule perm_closed) from prm have "fmset G as = fmset G as'" by (rule fmset_perm_cong) also assume "as' [∼] bs" with as'carr bscarr have "fmset G as' = fmset G bs" by (simp add: fmset_listassoc_cong) finally show "fmset G as = fmset G bs" . qed lemma (in comm_monoid_cancel) fmset_ee: assumes mset: "fmset G as = fmset G bs" and ascarr: "set as ⊆ carrier G" and bscarr: "set bs ⊆ carrier G" shows "essentially_equal G as bs" proof - from mset have "mset (map (assocs G) bs) = mset (map (assocs G) as)" by (simp add: fmset_def) then obtain p where ‹p permutes {..<length (map (assocs G) as)}› ‹permute_list p (map (assocs G) as) = map (assocs G) bs› by (rule mset_eq_permutation) then have ‹p permutes {..<length as}› ‹map (assocs G) (permute_list p as) = map (assocs G) bs› by (simp_all add: permute_list_map) moreover define as' where ‹as' = permute_list p as› ultimately have tp: "as <~~> as'" and tm: "map (assocs G) as' = map (assocs G) bs" by <