src/HOL/Algebra/Divisibility.thy
 author paulson Sat Jun 30 15:44:04 2018 +0100 (12 months ago) changeset 68551 b680e74eb6f2 parent 68488 dfbd80c3d180 child 68604 57721285d4ef permissions -rw-r--r--
More on Algebra by Paulo and Martin
```     1 (*  Title:      HOL/Algebra/Divisibility.thy
```
```     2     Author:     Clemens Ballarin
```
```     3     Author:     Stephan Hohe
```
```     4 *)
```
```     5
```
```     6 section \<open>Divisibility in monoids and rings\<close>
```
```     7
```
```     8 theory Divisibility
```
```     9   imports "HOL-Library.Permutation" Coset Group
```
```    10 begin
```
```    11
```
```    12 section \<open>Factorial Monoids\<close>
```
```    13
```
```    14 subsection \<open>Monoids with Cancellation Law\<close>
```
```    15
```
```    16 locale monoid_cancel = monoid +
```
```    17   assumes l_cancel: "\<lbrakk>c \<otimes> a = c \<otimes> b; a \<in> carrier G; b \<in> carrier G; c \<in> carrier G\<rbrakk> \<Longrightarrow> a = b"
```
```    18     and r_cancel: "\<lbrakk>a \<otimes> c = b \<otimes> c; a \<in> carrier G; b \<in> carrier G; c \<in> carrier G\<rbrakk> \<Longrightarrow> a = b"
```
```    19
```
```    20 lemma (in monoid) monoid_cancelI:
```
```    21   assumes l_cancel: "\<And>a b c. \<lbrakk>c \<otimes> a = c \<otimes> b; a \<in> carrier G; b \<in> carrier G; c \<in> carrier G\<rbrakk> \<Longrightarrow> a = b"
```
```    22     and r_cancel: "\<And>a b c. \<lbrakk>a \<otimes> c = b \<otimes> c; a \<in> carrier G; b \<in> carrier G; c \<in> carrier G\<rbrakk> \<Longrightarrow> a = b"
```
```    23   shows "monoid_cancel G"
```
```    24     by standard fact+
```
```    25
```
```    26 lemma (in monoid_cancel) is_monoid_cancel: "monoid_cancel G" ..
```
```    27
```
```    28 sublocale group \<subseteq> monoid_cancel
```
```    29   by standard simp_all
```
```    30
```
```    31
```
```    32 locale comm_monoid_cancel = monoid_cancel + comm_monoid
```
```    33
```
```    34 lemma comm_monoid_cancelI:
```
```    35   fixes G (structure)
```
```    36   assumes "comm_monoid G"
```
```    37   assumes cancel: "\<And>a b c. \<lbrakk>a \<otimes> c = b \<otimes> c; a \<in> carrier G; b \<in> carrier G; c \<in> carrier G\<rbrakk> \<Longrightarrow> a = b"
```
```    38   shows "comm_monoid_cancel G"
```
```    39 proof -
```
```    40   interpret comm_monoid G by fact
```
```    41   show "comm_monoid_cancel G"
```
```    42     by unfold_locales (metis assms(2) m_ac(2))+
```
```    43 qed
```
```    44
```
```    45 lemma (in comm_monoid_cancel) is_comm_monoid_cancel: "comm_monoid_cancel G"
```
```    46   by intro_locales
```
```    47
```
```    48 sublocale comm_group \<subseteq> comm_monoid_cancel ..
```
```    49
```
```    50
```
```    51 subsection \<open>Products of Units in Monoids\<close>
```
```    52
```
```    53 lemma (in monoid) prod_unit_l:
```
```    54   assumes abunit[simp]: "a \<otimes> b \<in> Units G"
```
```    55     and aunit[simp]: "a \<in> Units G"
```
```    56     and carr[simp]: "a \<in> carrier G"  "b \<in> carrier G"
```
```    57   shows "b \<in> Units G"
```
```    58 proof -
```
```    59   have c: "inv (a \<otimes> b) \<otimes> a \<in> carrier G" by simp
```
```    60
```
```    61   have "(inv (a \<otimes> b) \<otimes> a) \<otimes> b = inv (a \<otimes> b) \<otimes> (a \<otimes> b)"
```
```    62     by (simp add: m_assoc)
```
```    63   also have "\<dots> = \<one>" by simp
```
```    64   finally have li: "(inv (a \<otimes> b) \<otimes> a) \<otimes> b = \<one>" .
```
```    65
```
```    66   have "\<one> = inv a \<otimes> a" by (simp add: Units_l_inv[symmetric])
```
```    67   also have "\<dots> = inv a \<otimes> \<one> \<otimes> a" by simp
```
```    68   also have "\<dots> = inv a \<otimes> ((a \<otimes> b) \<otimes> inv (a \<otimes> b)) \<otimes> a"
```
```    69     by (simp add: Units_r_inv[OF abunit, symmetric] del: Units_r_inv)
```
```    70   also have "\<dots> = ((inv a \<otimes> a) \<otimes> b) \<otimes> inv (a \<otimes> b) \<otimes> a"
```
```    71     by (simp add: m_assoc del: Units_l_inv)
```
```    72   also have "\<dots> = b \<otimes> inv (a \<otimes> b) \<otimes> a" by simp
```
```    73   also have "\<dots> = b \<otimes> (inv (a \<otimes> b) \<otimes> a)" by (simp add: m_assoc)
```
```    74   finally have ri: "b \<otimes> (inv (a \<otimes> b) \<otimes> a) = \<one> " by simp
```
```    75
```
```    76   from c li ri show "b \<in> Units G" by (auto simp: Units_def)
```
```    77 qed
```
```    78
```
```    79 lemma (in monoid) prod_unit_r:
```
```    80   assumes abunit[simp]: "a \<otimes> b \<in> Units G"
```
```    81     and bunit[simp]: "b \<in> Units G"
```
```    82     and carr[simp]: "a \<in> carrier G"  "b \<in> carrier G"
```
```    83   shows "a \<in> Units G"
```
```    84 proof -
```
```    85   have c: "b \<otimes> inv (a \<otimes> b) \<in> carrier G" by simp
```
```    86
```
```    87   have "a \<otimes> (b \<otimes> inv (a \<otimes> b)) = (a \<otimes> b) \<otimes> inv (a \<otimes> b)"
```
```    88     by (simp add: m_assoc del: Units_r_inv)
```
```    89   also have "\<dots> = \<one>" by simp
```
```    90   finally have li: "a \<otimes> (b \<otimes> inv (a \<otimes> b)) = \<one>" .
```
```    91
```
```    92   have "\<one> = b \<otimes> inv b" by (simp add: Units_r_inv[symmetric])
```
```    93   also have "\<dots> = b \<otimes> \<one> \<otimes> inv b" by simp
```
```    94   also have "\<dots> = b \<otimes> (inv (a \<otimes> b) \<otimes> (a \<otimes> b)) \<otimes> inv b"
```
```    95     by (simp add: Units_l_inv[OF abunit, symmetric] del: Units_l_inv)
```
```    96   also have "\<dots> = (b \<otimes> inv (a \<otimes> b) \<otimes> a) \<otimes> (b \<otimes> inv b)"
```
```    97     by (simp add: m_assoc del: Units_l_inv)
```
```    98   also have "\<dots> = b \<otimes> inv (a \<otimes> b) \<otimes> a" by simp
```
```    99   finally have ri: "(b \<otimes> inv (a \<otimes> b)) \<otimes> a = \<one> " by simp
```
```   100
```
```   101   from c li ri show "a \<in> Units G" by (auto simp: Units_def)
```
```   102 qed
```
```   103
```
```   104 lemma (in comm_monoid) unit_factor:
```
```   105   assumes abunit: "a \<otimes> b \<in> Units G"
```
```   106     and [simp]: "a \<in> carrier G"  "b \<in> carrier G"
```
```   107   shows "a \<in> Units G"
```
```   108   using abunit[simplified Units_def]
```
```   109 proof clarsimp
```
```   110   fix i
```
```   111   assume [simp]: "i \<in> carrier G"
```
```   112
```
```   113   have carr': "b \<otimes> i \<in> carrier G" by simp
```
```   114
```
```   115   have "(b \<otimes> i) \<otimes> a = (i \<otimes> b) \<otimes> a" by (simp add: m_comm)
```
```   116   also have "\<dots> = i \<otimes> (b \<otimes> a)" by (simp add: m_assoc)
```
```   117   also have "\<dots> = i \<otimes> (a \<otimes> b)" by (simp add: m_comm)
```
```   118   also assume "i \<otimes> (a \<otimes> b) = \<one>"
```
```   119   finally have li': "(b \<otimes> i) \<otimes> a = \<one>" .
```
```   120
```
```   121   have "a \<otimes> (b \<otimes> i) = a \<otimes> b \<otimes> i" by (simp add: m_assoc)
```
```   122   also assume "a \<otimes> b \<otimes> i = \<one>"
```
```   123   finally have ri': "a \<otimes> (b \<otimes> i) = \<one>" .
```
```   124
```
```   125   from carr' li' ri'
```
```   126   show "a \<in> Units G" by (simp add: Units_def, fast)
```
```   127 qed
```
```   128
```
```   129
```
```   130 subsection \<open>Divisibility and Association\<close>
```
```   131
```
```   132 subsubsection \<open>Function definitions\<close>
```
```   133
```
```   134 definition factor :: "[_, 'a, 'a] \<Rightarrow> bool" (infix "divides\<index>" 65)
```
```   135   where "a divides\<^bsub>G\<^esub> b \<longleftrightarrow> (\<exists>c\<in>carrier G. b = a \<otimes>\<^bsub>G\<^esub> c)"
```
```   136
```
```   137 definition associated :: "[_, 'a, 'a] \<Rightarrow> bool" (infix "\<sim>\<index>" 55)
```
```   138   where "a \<sim>\<^bsub>G\<^esub> b \<longleftrightarrow> a divides\<^bsub>G\<^esub> b \<and> b divides\<^bsub>G\<^esub> a"
```
```   139
```
```   140 abbreviation "division_rel G \<equiv> \<lparr>carrier = carrier G, eq = (\<sim>\<^bsub>G\<^esub>), le = (divides\<^bsub>G\<^esub>)\<rparr>"
```
```   141
```
```   142 definition properfactor :: "[_, 'a, 'a] \<Rightarrow> bool"
```
```   143   where "properfactor G a b \<longleftrightarrow> a divides\<^bsub>G\<^esub> b \<and> \<not>(b divides\<^bsub>G\<^esub> a)"
```
```   144
```
```   145 definition irreducible :: "[_, 'a] \<Rightarrow> bool"
```
```   146   where "irreducible G a \<longleftrightarrow> a \<notin> Units G \<and> (\<forall>b\<in>carrier G. properfactor G b a \<longrightarrow> b \<in> Units G)"
```
```   147
```
```   148 definition prime :: "[_, 'a] \<Rightarrow> bool"
```
```   149   where "prime G p \<longleftrightarrow>
```
```   150     p \<notin> Units G \<and>
```
```   151     (\<forall>a\<in>carrier G. \<forall>b\<in>carrier G. p divides\<^bsub>G\<^esub> (a \<otimes>\<^bsub>G\<^esub> b) \<longrightarrow> p divides\<^bsub>G\<^esub> a \<or> p divides\<^bsub>G\<^esub> b)"
```
```   152
```
```   153
```
```   154 subsubsection \<open>Divisibility\<close>
```
```   155
```
```   156 lemma dividesI:
```
```   157   fixes G (structure)
```
```   158   assumes carr: "c \<in> carrier G"
```
```   159     and p: "b = a \<otimes> c"
```
```   160   shows "a divides b"
```
```   161   unfolding factor_def using assms by fast
```
```   162
```
```   163 lemma dividesI' [intro]:
```
```   164   fixes G (structure)
```
```   165   assumes p: "b = a \<otimes> c"
```
```   166     and carr: "c \<in> carrier G"
```
```   167   shows "a divides b"
```
```   168   using assms by (fast intro: dividesI)
```
```   169
```
```   170 lemma dividesD:
```
```   171   fixes G (structure)
```
```   172   assumes "a divides b"
```
```   173   shows "\<exists>c\<in>carrier G. b = a \<otimes> c"
```
```   174   using assms unfolding factor_def by fast
```
```   175
```
```   176 lemma dividesE [elim]:
```
```   177   fixes G (structure)
```
```   178   assumes d: "a divides b"
```
```   179     and elim: "\<And>c. \<lbrakk>b = a \<otimes> c; c \<in> carrier G\<rbrakk> \<Longrightarrow> P"
```
```   180   shows "P"
```
```   181 proof -
```
```   182   from dividesD[OF d] obtain c where "c \<in> carrier G" and "b = a \<otimes> c" by auto
```
```   183   then show P by (elim elim)
```
```   184 qed
```
```   185
```
```   186 lemma (in monoid) divides_refl[simp, intro!]:
```
```   187   assumes carr: "a \<in> carrier G"
```
```   188   shows "a divides a"
```
```   189   by (intro dividesI[of "\<one>"]) (simp_all add: carr)
```
```   190
```
```   191 lemma (in monoid) divides_trans [trans]:
```
```   192   assumes dvds: "a divides b" "b divides c"
```
```   193     and acarr: "a \<in> carrier G"
```
```   194   shows "a divides c"
```
```   195   using dvds[THEN dividesD] by (blast intro: dividesI m_assoc acarr)
```
```   196
```
```   197 lemma (in monoid) divides_mult_lI [intro]:
```
```   198   assumes  "a divides b" "a \<in> carrier G" "c \<in> carrier G"
```
```   199   shows "(c \<otimes> a) divides (c \<otimes> b)"
```
```   200   by (metis assms factor_def m_assoc)
```
```   201
```
```   202 lemma (in monoid_cancel) divides_mult_l [simp]:
```
```   203   assumes carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
```
```   204   shows "(c \<otimes> a) divides (c \<otimes> b) = a divides b"
```
```   205 proof
```
```   206   show "c \<otimes> a divides c \<otimes> b \<Longrightarrow> a divides b"
```
```   207     using carr monoid.m_assoc monoid_axioms monoid_cancel.l_cancel monoid_cancel_axioms by fastforce
```
```   208   show "a divides b \<Longrightarrow> c \<otimes> a divides c \<otimes> b"
```
```   209   using carr(1) carr(3) by blast
```
```   210 qed
```
```   211
```
```   212 lemma (in comm_monoid) divides_mult_rI [intro]:
```
```   213   assumes ab: "a divides b"
```
```   214     and carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
```
```   215   shows "(a \<otimes> c) divides (b \<otimes> c)"
```
```   216   using carr ab by (metis divides_mult_lI m_comm)
```
```   217
```
```   218 lemma (in comm_monoid_cancel) divides_mult_r [simp]:
```
```   219   assumes carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
```
```   220   shows "(a \<otimes> c) divides (b \<otimes> c) = a divides b"
```
```   221   using carr by (simp add: m_comm[of a c] m_comm[of b c])
```
```   222
```
```   223 lemma (in monoid) divides_prod_r:
```
```   224   assumes ab: "a divides b"
```
```   225     and carr: "a \<in> carrier G" "c \<in> carrier G"
```
```   226   shows "a divides (b \<otimes> c)"
```
```   227   using ab carr by (fast intro: m_assoc)
```
```   228
```
```   229 lemma (in comm_monoid) divides_prod_l:
```
```   230   assumes "a \<in> carrier G" "b \<in> carrier G" "c \<in> carrier G" "a divides b"
```
```   231   shows "a divides (c \<otimes> b)"
```
```   232   using assms  by (simp add: divides_prod_r m_comm)
```
```   233
```
```   234 lemma (in monoid) unit_divides:
```
```   235   assumes uunit: "u \<in> Units G"
```
```   236     and acarr: "a \<in> carrier G"
```
```   237   shows "u divides a"
```
```   238 proof (intro dividesI[of "(inv u) \<otimes> a"], fast intro: uunit acarr)
```
```   239   from uunit acarr have xcarr: "inv u \<otimes> a \<in> carrier G" by fast
```
```   240   from uunit acarr have "u \<otimes> (inv u \<otimes> a) = (u \<otimes> inv u) \<otimes> a"
```
```   241     by (fast intro: m_assoc[symmetric])
```
```   242   also have "\<dots> = \<one> \<otimes> a" by (simp add: Units_r_inv[OF uunit])
```
```   243   also from acarr have "\<dots> = a" by simp
```
```   244   finally show "a = u \<otimes> (inv u \<otimes> a)" ..
```
```   245 qed
```
```   246
```
```   247 lemma (in comm_monoid) divides_unit:
```
```   248   assumes udvd: "a divides u"
```
```   249     and  carr: "a \<in> carrier G"  "u \<in> Units G"
```
```   250   shows "a \<in> Units G"
```
```   251   using udvd carr by (blast intro: unit_factor)
```
```   252
```
```   253 lemma (in comm_monoid) Unit_eq_dividesone:
```
```   254   assumes ucarr: "u \<in> carrier G"
```
```   255   shows "u \<in> Units G = u divides \<one>"
```
```   256   using ucarr by (fast dest: divides_unit intro: unit_divides)
```
```   257
```
```   258
```
```   259 subsubsection \<open>Association\<close>
```
```   260
```
```   261 lemma associatedI:
```
```   262   fixes G (structure)
```
```   263   assumes "a divides b" "b divides a"
```
```   264   shows "a \<sim> b"
```
```   265   using assms by (simp add: associated_def)
```
```   266
```
```   267 lemma (in monoid) associatedI2:
```
```   268   assumes uunit[simp]: "u \<in> Units G"
```
```   269     and a: "a = b \<otimes> u"
```
```   270     and bcarr: "b \<in> carrier G"
```
```   271   shows "a \<sim> b"
```
```   272   using uunit bcarr
```
```   273   unfolding a
```
```   274   apply (intro associatedI)
```
```   275   apply (metis Units_closed divides_mult_lI one_closed r_one unit_divides)
```
```   276   by blast
```
```   277
```
```   278 lemma (in monoid) associatedI2':
```
```   279   assumes "a = b \<otimes> u"
```
```   280     and "u \<in> Units G"
```
```   281     and "b \<in> carrier G"
```
```   282   shows "a \<sim> b"
```
```   283   using assms by (intro associatedI2)
```
```   284
```
```   285 lemma associatedD:
```
```   286   fixes G (structure)
```
```   287   assumes "a \<sim> b"
```
```   288   shows "a divides b"
```
```   289   using assms by (simp add: associated_def)
```
```   290
```
```   291 lemma (in monoid_cancel) associatedD2:
```
```   292   assumes assoc: "a \<sim> b"
```
```   293     and carr: "a \<in> carrier G" "b \<in> carrier G"
```
```   294   shows "\<exists>u\<in>Units G. a = b \<otimes> u"
```
```   295   using assoc
```
```   296   unfolding associated_def
```
```   297 proof clarify
```
```   298   assume "b divides a"
```
```   299   then obtain u where ucarr: "u \<in> carrier G" and a: "a = b \<otimes> u"
```
```   300     by (rule dividesE)
```
```   301
```
```   302   assume "a divides b"
```
```   303   then obtain u' where u'carr: "u' \<in> carrier G" and b: "b = a \<otimes> u'"
```
```   304     by (rule dividesE)
```
```   305   note carr = carr ucarr u'carr
```
```   306
```
```   307   from carr have "a \<otimes> \<one> = a" by simp
```
```   308   also have "\<dots> = b \<otimes> u" by (simp add: a)
```
```   309   also have "\<dots> = a \<otimes> u' \<otimes> u" by (simp add: b)
```
```   310   also from carr have "\<dots> = a \<otimes> (u' \<otimes> u)" by (simp add: m_assoc)
```
```   311   finally have "a \<otimes> \<one> = a \<otimes> (u' \<otimes> u)" .
```
```   312   with carr have u1: "\<one> = u' \<otimes> u" by (fast dest: l_cancel)
```
```   313
```
```   314   from carr have "b \<otimes> \<one> = b" by simp
```
```   315   also have "\<dots> = a \<otimes> u'" by (simp add: b)
```
```   316   also have "\<dots> = b \<otimes> u \<otimes> u'" by (simp add: a)
```
```   317   also from carr have "\<dots> = b \<otimes> (u \<otimes> u')" by (simp add: m_assoc)
```
```   318   finally have "b \<otimes> \<one> = b \<otimes> (u \<otimes> u')" .
```
```   319   with carr have u2: "\<one> = u \<otimes> u'" by (fast dest: l_cancel)
```
```   320
```
```   321   from u'carr u1[symmetric] u2[symmetric] have "\<exists>u'\<in>carrier G. u' \<otimes> u = \<one> \<and> u \<otimes> u' = \<one>"
```
```   322     by fast
```
```   323   then have "u \<in> Units G"
```
```   324     by (simp add: Units_def ucarr)
```
```   325   with ucarr a show "\<exists>u\<in>Units G. a = b \<otimes> u" by fast
```
```   326 qed
```
```   327
```
```   328 lemma associatedE:
```
```   329   fixes G (structure)
```
```   330   assumes assoc: "a \<sim> b"
```
```   331     and e: "\<lbrakk>a divides b; b divides a\<rbrakk> \<Longrightarrow> P"
```
```   332   shows "P"
```
```   333 proof -
```
```   334   from assoc have "a divides b" "b divides a"
```
```   335     by (simp_all add: associated_def)
```
```   336   then show P by (elim e)
```
```   337 qed
```
```   338
```
```   339 lemma (in monoid_cancel) associatedE2:
```
```   340   assumes assoc: "a \<sim> b"
```
```   341     and e: "\<And>u. \<lbrakk>a = b \<otimes> u; u \<in> Units G\<rbrakk> \<Longrightarrow> P"
```
```   342     and carr: "a \<in> carrier G"  "b \<in> carrier G"
```
```   343   shows "P"
```
```   344 proof -
```
```   345   from assoc and carr have "\<exists>u\<in>Units G. a = b \<otimes> u"
```
```   346     by (rule associatedD2)
```
```   347   then obtain u where "u \<in> Units G"  "a = b \<otimes> u"
```
```   348     by auto
```
```   349   then show P by (elim e)
```
```   350 qed
```
```   351
```
```   352 lemma (in monoid) associated_refl [simp, intro!]:
```
```   353   assumes "a \<in> carrier G"
```
```   354   shows "a \<sim> a"
```
```   355   using assms by (fast intro: associatedI)
```
```   356
```
```   357 lemma (in monoid) associated_sym [sym]:
```
```   358   assumes "a \<sim> b"
```
```   359   shows "b \<sim> a"
```
```   360   using assms by (iprover intro: associatedI elim: associatedE)
```
```   361
```
```   362 lemma (in monoid) associated_trans [trans]:
```
```   363   assumes "a \<sim> b"  "b \<sim> c"
```
```   364     and "a \<in> carrier G" "c \<in> carrier G"
```
```   365   shows "a \<sim> c"
```
```   366   using assms by (iprover intro: associatedI divides_trans elim: associatedE)
```
```   367
```
```   368 lemma (in monoid) division_equiv [intro, simp]: "equivalence (division_rel G)"
```
```   369   apply unfold_locales
```
```   370     apply simp_all
```
```   371    apply (metis associated_def)
```
```   372   apply (iprover intro: associated_trans)
```
```   373   done
```
```   374
```
```   375
```
```   376 subsubsection \<open>Division and associativity\<close>
```
```   377
```
```   378 lemmas divides_antisym = associatedI
```
```   379
```
```   380 lemma (in monoid) divides_cong_l [trans]:
```
```   381   assumes "x \<sim> x'" "x' divides y" "x \<in> carrier G"
```
```   382   shows "x divides y"
```
```   383   by (meson assms associatedD divides_trans)
```
```   384
```
```   385 lemma (in monoid) divides_cong_r [trans]:
```
```   386   assumes "x divides y" "y \<sim> y'" "x \<in> carrier G"
```
```   387   shows "x divides y'"
```
```   388   by (meson assms associatedD divides_trans)
```
```   389
```
```   390 lemma (in monoid) division_weak_partial_order [simp, intro!]:
```
```   391   "weak_partial_order (division_rel G)"
```
```   392   apply unfold_locales
```
```   393       apply (simp_all add: associated_sym divides_antisym)
```
```   394      apply (metis associated_trans)
```
```   395    apply (metis divides_trans)
```
```   396   by (meson associated_def divides_trans)
```
```   397
```
```   398
```
```   399 subsubsection \<open>Multiplication and associativity\<close>
```
```   400
```
```   401 lemma (in monoid_cancel) mult_cong_r:
```
```   402   assumes "b \<sim> b'" "a \<in> carrier G"  "b \<in> carrier G"  "b' \<in> carrier G"
```
```   403   shows "a \<otimes> b \<sim> a \<otimes> b'"
```
```   404   by (meson assms associated_def divides_mult_lI)
```
```   405
```
```   406 lemma (in comm_monoid_cancel) mult_cong_l:
```
```   407   assumes "a \<sim> a'" "a \<in> carrier G"  "a' \<in> carrier G"  "b \<in> carrier G"
```
```   408   shows "a \<otimes> b \<sim> a' \<otimes> b"
```
```   409   using assms m_comm mult_cong_r by auto
```
```   410
```
```   411 lemma (in monoid_cancel) assoc_l_cancel:
```
```   412   assumes "a \<in> carrier G"  "b \<in> carrier G"  "b' \<in> carrier G" "a \<otimes> b \<sim> a \<otimes> b'"
```
```   413   shows "b \<sim> b'"
```
```   414   by (meson assms associated_def divides_mult_l)
```
```   415
```
```   416 lemma (in comm_monoid_cancel) assoc_r_cancel:
```
```   417   assumes "a \<otimes> b \<sim> a' \<otimes> b" "a \<in> carrier G"  "a' \<in> carrier G"  "b \<in> carrier G"
```
```   418   shows "a \<sim> a'"
```
```   419   using assms assoc_l_cancel m_comm by presburger
```
```   420
```
```   421
```
```   422 subsubsection \<open>Units\<close>
```
```   423
```
```   424 lemma (in monoid_cancel) assoc_unit_l [trans]:
```
```   425   assumes "a \<sim> b"
```
```   426     and "b \<in> Units G"
```
```   427     and "a \<in> carrier G"
```
```   428   shows "a \<in> Units G"
```
```   429   using assms by (fast elim: associatedE2)
```
```   430
```
```   431 lemma (in monoid_cancel) assoc_unit_r [trans]:
```
```   432   assumes aunit: "a \<in> Units G"
```
```   433     and asc: "a \<sim> b"
```
```   434     and bcarr: "b \<in> carrier G"
```
```   435   shows "b \<in> Units G"
```
```   436   using aunit bcarr associated_sym[OF asc] by (blast intro: assoc_unit_l)
```
```   437
```
```   438 lemma (in comm_monoid) Units_cong:
```
```   439   assumes aunit: "a \<in> Units G" and asc: "a \<sim> b"
```
```   440     and bcarr: "b \<in> carrier G"
```
```   441   shows "b \<in> Units G"
```
```   442   using assms by (blast intro: divides_unit elim: associatedE)
```
```   443
```
```   444 lemma (in monoid) Units_assoc:
```
```   445   assumes units: "a \<in> Units G"  "b \<in> Units G"
```
```   446   shows "a \<sim> b"
```
```   447   using units by (fast intro: associatedI unit_divides)
```
```   448
```
```   449 lemma (in monoid) Units_are_ones: "Units G {.=}\<^bsub>(division_rel G)\<^esub> {\<one>}"
```
```   450 proof -
```
```   451   have "a .\<in>\<^bsub>division_rel G\<^esub> {\<one>}" if "a \<in> Units G" for a
```
```   452   proof -
```
```   453     have "a \<sim> \<one>"
```
```   454       by (rule associatedI) (simp_all add: Units_closed that unit_divides)
```
```   455     then show ?thesis
```
```   456       by (simp add: elem_def)
```
```   457   qed
```
```   458   moreover have "\<one> .\<in>\<^bsub>division_rel G\<^esub> Units G"
```
```   459     by (simp add: equivalence.mem_imp_elem)
```
```   460   ultimately show ?thesis
```
```   461     by (auto simp: set_eq_def)
```
```   462 qed
```
```   463
```
```   464 lemma (in comm_monoid) Units_Lower: "Units G = Lower (division_rel G) (carrier G)"
```
```   465   apply (auto simp add: Units_def Lower_def)
```
```   466    apply (metis Units_one_closed unit_divides unit_factor)
```
```   467   apply (metis Unit_eq_dividesone Units_r_inv_ex m_ac(2) one_closed)
```
```   468   done
```
```   469
```
```   470
```
```   471 subsubsection \<open>Proper factors\<close>
```
```   472
```
```   473 lemma properfactorI:
```
```   474   fixes G (structure)
```
```   475   assumes "a divides b"
```
```   476     and "\<not>(b divides a)"
```
```   477   shows "properfactor G a b"
```
```   478   using assms unfolding properfactor_def by simp
```
```   479
```
```   480 lemma properfactorI2:
```
```   481   fixes G (structure)
```
```   482   assumes advdb: "a divides b"
```
```   483     and neq: "\<not>(a \<sim> b)"
```
```   484   shows "properfactor G a b"
```
```   485 proof (rule properfactorI, rule advdb, rule notI)
```
```   486   assume "b divides a"
```
```   487   with advdb have "a \<sim> b" by (rule associatedI)
```
```   488   with neq show "False" by fast
```
```   489 qed
```
```   490
```
```   491 lemma (in comm_monoid_cancel) properfactorI3:
```
```   492   assumes p: "p = a \<otimes> b"
```
```   493     and nunit: "b \<notin> Units G"
```
```   494     and carr: "a \<in> carrier G"  "b \<in> carrier G"
```
```   495   shows "properfactor G a p"
```
```   496   unfolding p
```
```   497   using carr
```
```   498   apply (intro properfactorI, fast)
```
```   499 proof (clarsimp, elim dividesE)
```
```   500   fix c
```
```   501   assume ccarr: "c \<in> carrier G"
```
```   502   note [simp] = carr ccarr
```
```   503
```
```   504   have "a \<otimes> \<one> = a" by simp
```
```   505   also assume "a = a \<otimes> b \<otimes> c"
```
```   506   also have "\<dots> = a \<otimes> (b \<otimes> c)" by (simp add: m_assoc)
```
```   507   finally have "a \<otimes> \<one> = a \<otimes> (b \<otimes> c)" .
```
```   508
```
```   509   then have rinv: "\<one> = b \<otimes> c" by (intro l_cancel[of "a" "\<one>" "b \<otimes> c"], simp+)
```
```   510   also have "\<dots> = c \<otimes> b" by (simp add: m_comm)
```
```   511   finally have linv: "\<one> = c \<otimes> b" .
```
```   512
```
```   513   from ccarr linv[symmetric] rinv[symmetric] have "b \<in> Units G"
```
```   514     unfolding Units_def by fastforce
```
```   515   with nunit show False ..
```
```   516 qed
```
```   517
```
```   518 lemma properfactorE:
```
```   519   fixes G (structure)
```
```   520   assumes pf: "properfactor G a b"
```
```   521     and r: "\<lbrakk>a divides b; \<not>(b divides a)\<rbrakk> \<Longrightarrow> P"
```
```   522   shows "P"
```
```   523   using pf unfolding properfactor_def by (fast intro: r)
```
```   524
```
```   525 lemma properfactorE2:
```
```   526   fixes G (structure)
```
```   527   assumes pf: "properfactor G a b"
```
```   528     and elim: "\<lbrakk>a divides b; \<not>(a \<sim> b)\<rbrakk> \<Longrightarrow> P"
```
```   529   shows "P"
```
```   530   using pf unfolding properfactor_def by (fast elim: elim associatedE)
```
```   531
```
```   532 lemma (in monoid) properfactor_unitE:
```
```   533   assumes uunit: "u \<in> Units G"
```
```   534     and pf: "properfactor G a u"
```
```   535     and acarr: "a \<in> carrier G"
```
```   536   shows "P"
```
```   537   using pf unit_divides[OF uunit acarr] by (fast elim: properfactorE)
```
```   538
```
```   539 lemma (in monoid) properfactor_divides:
```
```   540   assumes pf: "properfactor G a b"
```
```   541   shows "a divides b"
```
```   542   using pf by (elim properfactorE)
```
```   543
```
```   544 lemma (in monoid) properfactor_trans1 [trans]:
```
```   545   assumes dvds: "a divides b"  "properfactor G b c"
```
```   546     and carr: "a \<in> carrier G"  "c \<in> carrier G"
```
```   547   shows "properfactor G a c"
```
```   548   using dvds carr
```
```   549   apply (elim properfactorE, intro properfactorI)
```
```   550    apply (iprover intro: divides_trans)+
```
```   551   done
```
```   552
```
```   553 lemma (in monoid) properfactor_trans2 [trans]:
```
```   554   assumes dvds: "properfactor G a b"  "b divides c"
```
```   555     and carr: "a \<in> carrier G"  "b \<in> carrier G"
```
```   556   shows "properfactor G a c"
```
```   557   using dvds carr
```
```   558   apply (elim properfactorE, intro properfactorI)
```
```   559    apply (iprover intro: divides_trans)+
```
```   560   done
```
```   561
```
```   562 lemma properfactor_lless:
```
```   563   fixes G (structure)
```
```   564   shows "properfactor G = lless (division_rel G)"
```
```   565   by (force simp: lless_def properfactor_def associated_def)
```
```   566
```
```   567 lemma (in monoid) properfactor_cong_l [trans]:
```
```   568   assumes x'x: "x' \<sim> x"
```
```   569     and pf: "properfactor G x y"
```
```   570     and carr: "x \<in> carrier G"  "x' \<in> carrier G"  "y \<in> carrier G"
```
```   571   shows "properfactor G x' y"
```
```   572   using pf
```
```   573   unfolding properfactor_lless
```
```   574 proof -
```
```   575   interpret weak_partial_order "division_rel G" ..
```
```   576   from x'x have "x' .=\<^bsub>division_rel G\<^esub> x" by simp
```
```   577   also assume "x \<sqsubset>\<^bsub>division_rel G\<^esub> y"
```
```   578   finally show "x' \<sqsubset>\<^bsub>division_rel G\<^esub> y" by (simp add: carr)
```
```   579 qed
```
```   580
```
```   581 lemma (in monoid) properfactor_cong_r [trans]:
```
```   582   assumes pf: "properfactor G x y"
```
```   583     and yy': "y \<sim> y'"
```
```   584     and carr: "x \<in> carrier G"  "y \<in> carrier G"  "y' \<in> carrier G"
```
```   585   shows "properfactor G x y'"
```
```   586   using pf
```
```   587   unfolding properfactor_lless
```
```   588 proof -
```
```   589   interpret weak_partial_order "division_rel G" ..
```
```   590   assume "x \<sqsubset>\<^bsub>division_rel G\<^esub> y"
```
```   591   also from yy'
```
```   592   have "y .=\<^bsub>division_rel G\<^esub> y'" by simp
```
```   593   finally show "x \<sqsubset>\<^bsub>division_rel G\<^esub> y'" by (simp add: carr)
```
```   594 qed
```
```   595
```
```   596 lemma (in monoid_cancel) properfactor_mult_lI [intro]:
```
```   597   assumes ab: "properfactor G a b"
```
```   598     and carr: "a \<in> carrier G" "c \<in> carrier G"
```
```   599   shows "properfactor G (c \<otimes> a) (c \<otimes> b)"
```
```   600   using ab carr by (fastforce elim: properfactorE intro: properfactorI)
```
```   601
```
```   602 lemma (in monoid_cancel) properfactor_mult_l [simp]:
```
```   603   assumes carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
```
```   604   shows "properfactor G (c \<otimes> a) (c \<otimes> b) = properfactor G a b"
```
```   605   using carr by (fastforce elim: properfactorE intro: properfactorI)
```
```   606
```
```   607 lemma (in comm_monoid_cancel) properfactor_mult_rI [intro]:
```
```   608   assumes ab: "properfactor G a b"
```
```   609     and carr: "a \<in> carrier G" "c \<in> carrier G"
```
```   610   shows "properfactor G (a \<otimes> c) (b \<otimes> c)"
```
```   611   using ab carr by (fastforce elim: properfactorE intro: properfactorI)
```
```   612
```
```   613 lemma (in comm_monoid_cancel) properfactor_mult_r [simp]:
```
```   614   assumes carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
```
```   615   shows "properfactor G (a \<otimes> c) (b \<otimes> c) = properfactor G a b"
```
```   616   using carr by (fastforce elim: properfactorE intro: properfactorI)
```
```   617
```
```   618 lemma (in monoid) properfactor_prod_r:
```
```   619   assumes ab: "properfactor G a b"
```
```   620     and carr[simp]: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
```
```   621   shows "properfactor G a (b \<otimes> c)"
```
```   622   by (intro properfactor_trans2[OF ab] divides_prod_r) simp_all
```
```   623
```
```   624 lemma (in comm_monoid) properfactor_prod_l:
```
```   625   assumes ab: "properfactor G a b"
```
```   626     and carr[simp]: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
```
```   627   shows "properfactor G a (c \<otimes> b)"
```
```   628   by (intro properfactor_trans2[OF ab] divides_prod_l) simp_all
```
```   629
```
```   630
```
```   631 subsection \<open>Irreducible Elements and Primes\<close>
```
```   632
```
```   633 subsubsection \<open>Irreducible elements\<close>
```
```   634
```
```   635 lemma irreducibleI:
```
```   636   fixes G (structure)
```
```   637   assumes "a \<notin> Units G"
```
```   638     and "\<And>b. \<lbrakk>b \<in> carrier G; properfactor G b a\<rbrakk> \<Longrightarrow> b \<in> Units G"
```
```   639   shows "irreducible G a"
```
```   640   using assms unfolding irreducible_def by blast
```
```   641
```
```   642 lemma irreducibleE:
```
```   643   fixes G (structure)
```
```   644   assumes irr: "irreducible G a"
```
```   645     and elim: "\<lbrakk>a \<notin> Units G; \<forall>b. b \<in> carrier G \<and> properfactor G b a \<longrightarrow> b \<in> Units G\<rbrakk> \<Longrightarrow> P"
```
```   646   shows "P"
```
```   647   using assms unfolding irreducible_def by blast
```
```   648
```
```   649 lemma irreducibleD:
```
```   650   fixes G (structure)
```
```   651   assumes irr: "irreducible G a"
```
```   652     and pf: "properfactor G b a"
```
```   653     and bcarr: "b \<in> carrier G"
```
```   654   shows "b \<in> Units G"
```
```   655   using assms by (fast elim: irreducibleE)
```
```   656
```
```   657 lemma (in monoid_cancel) irreducible_cong [trans]:
```
```   658   assumes irred: "irreducible G a"
```
```   659     and aa': "a \<sim> a'" "a \<in> carrier G"  "a' \<in> carrier G"
```
```   660   shows "irreducible G a'"
```
```   661   using assms
```
```   662   apply (auto simp: irreducible_def assoc_unit_l)
```
```   663   apply (metis aa' associated_sym properfactor_cong_r)
```
```   664   done
```
```   665
```
```   666 lemma (in monoid) irreducible_prod_rI:
```
```   667   assumes airr: "irreducible G a"
```
```   668     and bunit: "b \<in> Units G"
```
```   669     and carr[simp]: "a \<in> carrier G"  "b \<in> carrier G"
```
```   670   shows "irreducible G (a \<otimes> b)"
```
```   671   using airr carr bunit
```
```   672   apply (elim irreducibleE, intro irreducibleI)
```
```   673   using prod_unit_r apply blast
```
```   674   using associatedI2' properfactor_cong_r by auto
```
```   675
```
```   676 lemma (in comm_monoid) irreducible_prod_lI:
```
```   677   assumes birr: "irreducible G b"
```
```   678     and aunit: "a \<in> Units G"
```
```   679     and carr [simp]: "a \<in> carrier G"  "b \<in> carrier G"
```
```   680   shows "irreducible G (a \<otimes> b)"
```
```   681   by (metis aunit birr carr irreducible_prod_rI m_comm)
```
```   682
```
```   683 lemma (in comm_monoid_cancel) irreducible_prodE [elim]:
```
```   684   assumes irr: "irreducible G (a \<otimes> b)"
```
```   685     and carr[simp]: "a \<in> carrier G"  "b \<in> carrier G"
```
```   686     and e1: "\<lbrakk>irreducible G a; b \<in> Units G\<rbrakk> \<Longrightarrow> P"
```
```   687     and e2: "\<lbrakk>a \<in> Units G; irreducible G b\<rbrakk> \<Longrightarrow> P"
```
```   688   shows P
```
```   689   using irr
```
```   690 proof (elim irreducibleE)
```
```   691   assume abnunit: "a \<otimes> b \<notin> Units G"
```
```   692     and isunit[rule_format]: "\<forall>ba. ba \<in> carrier G \<and> properfactor G ba (a \<otimes> b) \<longrightarrow> ba \<in> Units G"
```
```   693   show P
```
```   694   proof (cases "a \<in> Units G")
```
```   695     case aunit: True
```
```   696     have "irreducible G b"
```
```   697     proof (rule irreducibleI, rule notI)
```
```   698       assume "b \<in> Units G"
```
```   699       with aunit have "(a \<otimes> b) \<in> Units G" by fast
```
```   700       with abnunit show "False" ..
```
```   701     next
```
```   702       fix c
```
```   703       assume ccarr: "c \<in> carrier G"
```
```   704         and "properfactor G c b"
```
```   705       then have "properfactor G c (a \<otimes> b)" by (simp add: properfactor_prod_l[of c b a])
```
```   706       with ccarr show "c \<in> Units G" by (fast intro: isunit)
```
```   707     qed
```
```   708     with aunit show "P" by (rule e2)
```
```   709   next
```
```   710     case anunit: False
```
```   711     with carr have "properfactor G b (b \<otimes> a)" by (fast intro: properfactorI3)
```
```   712     then have bf: "properfactor G b (a \<otimes> b)" by (subst m_comm[of a b], simp+)
```
```   713     then have bunit: "b \<in> Units G" by (intro isunit, simp)
```
```   714
```
```   715     have "irreducible G a"
```
```   716     proof (rule irreducibleI, rule notI)
```
```   717       assume "a \<in> Units G"
```
```   718       with bunit have "(a \<otimes> b) \<in> Units G" by fast
```
```   719       with abnunit show "False" ..
```
```   720     next
```
```   721       fix c
```
```   722       assume ccarr: "c \<in> carrier G"
```
```   723         and "properfactor G c a"
```
```   724       then have "properfactor G c (a \<otimes> b)"
```
```   725         by (simp add: properfactor_prod_r[of c a b])
```
```   726       with ccarr show "c \<in> Units G" by (fast intro: isunit)
```
```   727     qed
```
```   728     from this bunit show "P" by (rule e1)
```
```   729   qed
```
```   730 qed
```
```   731
```
```   732
```
```   733 subsubsection \<open>Prime elements\<close>
```
```   734
```
```   735 lemma primeI:
```
```   736   fixes G (structure)
```
```   737   assumes "p \<notin> Units G"
```
```   738     and "\<And>a b. \<lbrakk>a \<in> carrier G; b \<in> carrier G; p divides (a \<otimes> b)\<rbrakk> \<Longrightarrow> p divides a \<or> p divides b"
```
```   739   shows "prime G p"
```
```   740   using assms unfolding prime_def by blast
```
```   741
```
```   742 lemma primeE:
```
```   743   fixes G (structure)
```
```   744   assumes pprime: "prime G p"
```
```   745     and e: "\<lbrakk>p \<notin> Units G; \<forall>a\<in>carrier G. \<forall>b\<in>carrier G.
```
```   746       p divides a \<otimes> b \<longrightarrow> p divides a \<or> p divides b\<rbrakk> \<Longrightarrow> P"
```
```   747   shows "P"
```
```   748   using pprime unfolding prime_def by (blast dest: e)
```
```   749
```
```   750 lemma (in comm_monoid_cancel) prime_divides:
```
```   751   assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
```
```   752     and pprime: "prime G p"
```
```   753     and pdvd: "p divides a \<otimes> b"
```
```   754   shows "p divides a \<or> p divides b"
```
```   755   using assms by (blast elim: primeE)
```
```   756
```
```   757 lemma (in monoid_cancel) prime_cong [trans]:
```
```   758   assumes "prime G p"
```
```   759     and pp': "p \<sim> p'" "p \<in> carrier G"  "p' \<in> carrier G"
```
```   760   shows "prime G p'"
```
```   761   using assms
```
```   762   apply (auto simp: prime_def assoc_unit_l)
```
```   763   apply (metis pp' associated_sym divides_cong_l)
```
```   764   done
```
```   765
```
```   766 (*by Paulo EmÃ­lio de Vilhena*)
```
```   767 lemma (in comm_monoid_cancel) prime_irreducible:
```
```   768   assumes "prime G p"
```
```   769   shows "irreducible G p"
```
```   770 proof (rule irreducibleI)
```
```   771   show "p \<notin> Units G"
```
```   772     using assms unfolding prime_def by simp
```
```   773 next
```
```   774   fix b assume A: "b \<in> carrier G" "properfactor G b p"
```
```   775   then obtain c where c: "c \<in> carrier G" "p = b \<otimes> c"
```
```   776     unfolding properfactor_def factor_def by auto
```
```   777   hence "p divides c"
```
```   778     using A assms unfolding prime_def properfactor_def by auto
```
```   779   then obtain b' where b': "b' \<in> carrier G" "c = p \<otimes> b'"
```
```   780     unfolding factor_def by auto
```
```   781   hence "\<one> = b \<otimes> b'"
```
```   782     by (metis A(1) l_cancel m_closed m_lcomm one_closed r_one c)
```
```   783   thus "b \<in> Units G"
```
```   784     using A(1) Units_one_closed b'(1) unit_factor by presburger
```
```   785 qed
```
```   786
```
```   787
```
```   788 subsection \<open>Factorization and Factorial Monoids\<close>
```
```   789
```
```   790 subsubsection \<open>Function definitions\<close>
```
```   791
```
```   792 definition factors :: "[_, 'a list, 'a] \<Rightarrow> bool"
```
```   793   where "factors G fs a \<longleftrightarrow> (\<forall>x \<in> (set fs). irreducible G x) \<and> foldr (\<otimes>\<^bsub>G\<^esub>) fs \<one>\<^bsub>G\<^esub> = a"
```
```   794
```
```   795 definition wfactors ::"[_, 'a list, 'a] \<Rightarrow> bool"
```
```   796   where "wfactors G fs a \<longleftrightarrow> (\<forall>x \<in> (set fs). irreducible G x) \<and> foldr (\<otimes>\<^bsub>G\<^esub>) fs \<one>\<^bsub>G\<^esub> \<sim>\<^bsub>G\<^esub> a"
```
```   797
```
```   798 abbreviation list_assoc :: "('a,_) monoid_scheme \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "[\<sim>]\<index>" 44)
```
```   799   where "list_assoc G \<equiv> list_all2 (\<sim>\<^bsub>G\<^esub>)"
```
```   800
```
```   801 definition essentially_equal :: "[_, 'a list, 'a list] \<Rightarrow> bool"
```
```   802   where "essentially_equal G fs1 fs2 \<longleftrightarrow> (\<exists>fs1'. fs1 <~~> fs1' \<and> fs1' [\<sim>]\<^bsub>G\<^esub> fs2)"
```
```   803
```
```   804
```
```   805 locale factorial_monoid = comm_monoid_cancel +
```
```   806   assumes factors_exist: "\<lbrakk>a \<in> carrier G; a \<notin> Units G\<rbrakk> \<Longrightarrow> \<exists>fs. set fs \<subseteq> carrier G \<and> factors G fs a"
```
```   807     and factors_unique:
```
```   808       "\<lbrakk>factors G fs a; factors G fs' a; a \<in> carrier G; a \<notin> Units G;
```
```   809         set fs \<subseteq> carrier G; set fs' \<subseteq> carrier G\<rbrakk> \<Longrightarrow> essentially_equal G fs fs'"
```
```   810
```
```   811
```
```   812 subsubsection \<open>Comparing lists of elements\<close>
```
```   813
```
```   814 text \<open>Association on lists\<close>
```
```   815
```
```   816 lemma (in monoid) listassoc_refl [simp, intro]:
```
```   817   assumes "set as \<subseteq> carrier G"
```
```   818   shows "as [\<sim>] as"
```
```   819   using assms by (induct as) simp_all
```
```   820
```
```   821 lemma (in monoid) listassoc_sym [sym]:
```
```   822   assumes "as [\<sim>] bs"
```
```   823     and "set as \<subseteq> carrier G"
```
```   824     and "set bs \<subseteq> carrier G"
```
```   825   shows "bs [\<sim>] as"
```
```   826   using assms
```
```   827 proof (induction as arbitrary: bs)
```
```   828   case Cons
```
```   829   then show ?case
```
```   830     by (induction bs) (use associated_sym in auto)
```
```   831 qed auto
```
```   832
```
```   833 lemma (in monoid) listassoc_trans [trans]:
```
```   834   assumes "as [\<sim>] bs" and "bs [\<sim>] cs"
```
```   835     and "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G" and "set cs \<subseteq> carrier G"
```
```   836   shows "as [\<sim>] cs"
```
```   837   using assms
```
```   838   apply (simp add: list_all2_conv_all_nth set_conv_nth, safe)
```
```   839   by (metis (mono_tags, lifting) associated_trans nth_mem subsetCE)
```
```   840
```
```   841 lemma (in monoid_cancel) irrlist_listassoc_cong:
```
```   842   assumes "\<forall>a\<in>set as. irreducible G a"
```
```   843     and "as [\<sim>] bs"
```
```   844     and "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G"
```
```   845   shows "\<forall>a\<in>set bs. irreducible G a"
```
```   846   using assms
```
```   847   apply (clarsimp simp add: list_all2_conv_all_nth set_conv_nth)
```
```   848   apply (blast intro: irreducible_cong)
```
```   849   done
```
```   850
```
```   851
```
```   852 text \<open>Permutations\<close>
```
```   853
```
```   854 lemma perm_map [intro]:
```
```   855   assumes p: "a <~~> b"
```
```   856   shows "map f a <~~> map f b"
```
```   857   using p by induct auto
```
```   858
```
```   859 lemma perm_map_switch:
```
```   860   assumes m: "map f a = map f b" and p: "b <~~> c"
```
```   861   shows "\<exists>d. a <~~> d \<and> map f d = map f c"
```
```   862   using p m by (induct arbitrary: a) (simp, force, force, blast)
```
```   863
```
```   864 lemma (in monoid) perm_assoc_switch:
```
```   865   assumes a:"as [\<sim>] bs" and p: "bs <~~> cs"
```
```   866   shows "\<exists>bs'. as <~~> bs' \<and> bs' [\<sim>] cs"
```
```   867   using p a
```
```   868 proof (induction bs cs arbitrary: as)
```
```   869   case (swap y x l)
```
```   870   then show ?case
```
```   871     by (metis (no_types, hide_lams) list_all2_Cons2 perm.swap)
```
```   872 next
```
```   873 case (Cons xs ys z)
```
```   874   then show ?case
```
```   875     by (metis list_all2_Cons2 perm.Cons)
```
```   876 next
```
```   877   case (trans xs ys zs)
```
```   878   then show ?case
```
```   879     by (meson perm.trans)
```
```   880 qed auto
```
```   881
```
```   882 lemma (in monoid) perm_assoc_switch_r:
```
```   883   assumes p: "as <~~> bs" and a:"bs [\<sim>] cs"
```
```   884   shows "\<exists>bs'. as [\<sim>] bs' \<and> bs' <~~> cs"
```
```   885   using p a
```
```   886 proof (induction as bs arbitrary: cs)
```
```   887   case Nil
```
```   888   then show ?case
```
```   889     by auto
```
```   890 next
```
```   891   case (swap y x l)
```
```   892   then show ?case
```
```   893     by (metis (no_types, hide_lams) list_all2_Cons1 perm.swap)
```
```   894 next
```
```   895   case (Cons xs ys z)
```
```   896   then show ?case
```
```   897     by (metis list_all2_Cons1 perm.Cons)
```
```   898 next
```
```   899   case (trans xs ys zs)
```
```   900   then show ?case
```
```   901     by (blast intro:  elim: )
```
```   902 qed
```
```   903
```
```   904 declare perm_sym [sym]
```
```   905
```
```   906 lemma perm_setP:
```
```   907   assumes perm: "as <~~> bs"
```
```   908     and as: "P (set as)"
```
```   909   shows "P (set bs)"
```
```   910 proof -
```
```   911   from perm have "mset as = mset bs"
```
```   912     by (simp add: mset_eq_perm)
```
```   913   then have "set as = set bs"
```
```   914     by (rule mset_eq_setD)
```
```   915   with as show "P (set bs)"
```
```   916     by simp
```
```   917 qed
```
```   918
```
```   919 lemmas (in monoid) perm_closed = perm_setP[of _ _ "\<lambda>as. as \<subseteq> carrier G"]
```
```   920
```
```   921 lemmas (in monoid) irrlist_perm_cong = perm_setP[of _ _ "\<lambda>as. \<forall>a\<in>as. irreducible G a"]
```
```   922
```
```   923
```
```   924 text \<open>Essentially equal factorizations\<close>
```
```   925
```
```   926 lemma (in monoid) essentially_equalI:
```
```   927   assumes ex: "fs1 <~~> fs1'"  "fs1' [\<sim>] fs2"
```
```   928   shows "essentially_equal G fs1 fs2"
```
```   929   using ex unfolding essentially_equal_def by fast
```
```   930
```
```   931 lemma (in monoid) essentially_equalE:
```
```   932   assumes ee: "essentially_equal G fs1 fs2"
```
```   933     and e: "\<And>fs1'. \<lbrakk>fs1 <~~> fs1'; fs1' [\<sim>] fs2\<rbrakk> \<Longrightarrow> P"
```
```   934   shows "P"
```
```   935   using ee unfolding essentially_equal_def by (fast intro: e)
```
```   936
```
```   937 lemma (in monoid) ee_refl [simp,intro]:
```
```   938   assumes carr: "set as \<subseteq> carrier G"
```
```   939   shows "essentially_equal G as as"
```
```   940   using carr by (fast intro: essentially_equalI)
```
```   941
```
```   942 lemma (in monoid) ee_sym [sym]:
```
```   943   assumes ee: "essentially_equal G as bs"
```
```   944     and carr: "set as \<subseteq> carrier G"  "set bs \<subseteq> carrier G"
```
```   945   shows "essentially_equal G bs as"
```
```   946   using ee
```
```   947 proof (elim essentially_equalE)
```
```   948   fix fs
```
```   949   assume "as <~~> fs"  "fs [\<sim>] bs"
```
```   950   from perm_assoc_switch_r [OF this] obtain fs' where a: "as [\<sim>] fs'" and p: "fs' <~~> bs"
```
```   951     by blast
```
```   952   from p have "bs <~~> fs'" by (rule perm_sym)
```
```   953   with a[symmetric] carr show ?thesis
```
```   954     by (iprover intro: essentially_equalI perm_closed)
```
```   955 qed
```
```   956
```
```   957 lemma (in monoid) ee_trans [trans]:
```
```   958   assumes ab: "essentially_equal G as bs" and bc: "essentially_equal G bs cs"
```
```   959     and ascarr: "set as \<subseteq> carrier G"
```
```   960     and bscarr: "set bs \<subseteq> carrier G"
```
```   961     and cscarr: "set cs \<subseteq> carrier G"
```
```   962   shows "essentially_equal G as cs"
```
```   963   using ab bc
```
```   964 proof (elim essentially_equalE)
```
```   965   fix abs bcs
```
```   966   assume "abs [\<sim>] bs" and pb: "bs <~~> bcs"
```
```   967   from perm_assoc_switch [OF this] obtain bs' where p: "abs <~~> bs'" and a: "bs' [\<sim>] bcs"
```
```   968     by blast
```
```   969   assume "as <~~> abs"
```
```   970   with p have pp: "as <~~> bs'" by fast
```
```   971   from pp ascarr have c1: "set bs' \<subseteq> carrier G" by (rule perm_closed)
```
```   972   from pb bscarr have c2: "set bcs \<subseteq> carrier G" by (rule perm_closed)
```
```   973   assume "bcs [\<sim>] cs"
```
```   974   then have "bs' [\<sim>] cs"
```
```   975     using a c1 c2 cscarr listassoc_trans by blast
```
```   976   with pp show ?thesis
```
```   977     by (rule essentially_equalI)
```
```   978 qed
```
```   979
```
```   980
```
```   981 subsubsection \<open>Properties of lists of elements\<close>
```
```   982
```
```   983 text \<open>Multiplication of factors in a list\<close>
```
```   984
```
```   985 lemma (in monoid) multlist_closed [simp, intro]:
```
```   986   assumes ascarr: "set fs \<subseteq> carrier G"
```
```   987   shows "foldr (\<otimes>) fs \<one> \<in> carrier G"
```
```   988   using ascarr by (induct fs) simp_all
```
```   989
```
```   990 lemma  (in comm_monoid) multlist_dividesI:
```
```   991   assumes "f \<in> set fs" and "set fs \<subseteq> carrier G"
```
```   992   shows "f divides (foldr (\<otimes>) fs \<one>)"
```
```   993   using assms
```
```   994 proof (induction fs)
```
```   995   case (Cons a fs)
```
```   996   then have f: "f \<in> carrier G"
```
```   997     by blast
```
```   998   show ?case
```
```   999   proof (cases "f = a")
```
```  1000     case True
```
```  1001     then show ?thesis
```
```  1002       using Cons.prems by auto
```
```  1003   next
```
```  1004     case False
```
```  1005     with Cons show ?thesis
```
```  1006       by clarsimp (metis f divides_prod_l multlist_closed)
```
```  1007   qed
```
```  1008 qed auto
```
```  1009
```
```  1010 lemma (in comm_monoid_cancel) multlist_listassoc_cong:
```
```  1011   assumes "fs [\<sim>] fs'"
```
```  1012     and "set fs \<subseteq> carrier G" and "set fs' \<subseteq> carrier G"
```
```  1013   shows "foldr (\<otimes>) fs \<one> \<sim> foldr (\<otimes>) fs' \<one>"
```
```  1014   using assms
```
```  1015 proof (induct fs arbitrary: fs')
```
```  1016   case (Cons a as fs')
```
```  1017   then show ?case
```
```  1018   proof (induction fs')
```
```  1019     case (Cons b bs)
```
```  1020     then have p: "a \<otimes> foldr (\<otimes>) as \<one> \<sim> b \<otimes> foldr (\<otimes>) as \<one>"
```
```  1021       by (simp add: mult_cong_l)
```
```  1022     then have "foldr (\<otimes>) as \<one> \<sim> foldr (\<otimes>) bs \<one>"
```
```  1023       using Cons by auto
```
```  1024     with Cons have "b \<otimes> foldr (\<otimes>) as \<one> \<sim> b \<otimes> foldr (\<otimes>) bs \<one>"
```
```  1025       by (simp add: mult_cong_r)
```
```  1026     then show ?case
```
```  1027       using Cons.prems(3) Cons.prems(4) monoid.associated_trans monoid_axioms p by force
```
```  1028   qed auto
```
```  1029 qed auto
```
```  1030
```
```  1031 lemma (in comm_monoid) multlist_perm_cong:
```
```  1032   assumes prm: "as <~~> bs"
```
```  1033     and ascarr: "set as \<subseteq> carrier G"
```
```  1034   shows "foldr (\<otimes>) as \<one> = foldr (\<otimes>) bs \<one>"
```
```  1035   using prm ascarr
```
```  1036 proof induction
```
```  1037   case (swap y x l) then show ?case
```
```  1038     by (simp add: m_lcomm)
```
```  1039 next
```
```  1040   case (trans xs ys zs) then show ?case
```
```  1041     using perm_closed by auto
```
```  1042 qed auto
```
```  1043
```
```  1044 lemma (in comm_monoid_cancel) multlist_ee_cong:
```
```  1045   assumes "essentially_equal G fs fs'"
```
```  1046     and "set fs \<subseteq> carrier G" and "set fs' \<subseteq> carrier G"
```
```  1047   shows "foldr (\<otimes>) fs \<one> \<sim> foldr (\<otimes>) fs' \<one>"
```
```  1048   using assms
```
```  1049   apply (elim essentially_equalE)
```
```  1050   apply (simp add: multlist_perm_cong multlist_listassoc_cong perm_closed)
```
```  1051   done
```
```  1052
```
```  1053
```
```  1054 subsubsection \<open>Factorization in irreducible elements\<close>
```
```  1055
```
```  1056 lemma wfactorsI:
```
```  1057   fixes G (structure)
```
```  1058   assumes "\<forall>f\<in>set fs. irreducible G f"
```
```  1059     and "foldr (\<otimes>) fs \<one> \<sim> a"
```
```  1060   shows "wfactors G fs a"
```
```  1061   using assms unfolding wfactors_def by simp
```
```  1062
```
```  1063 lemma wfactorsE:
```
```  1064   fixes G (structure)
```
```  1065   assumes wf: "wfactors G fs a"
```
```  1066     and e: "\<lbrakk>\<forall>f\<in>set fs. irreducible G f; foldr (\<otimes>) fs \<one> \<sim> a\<rbrakk> \<Longrightarrow> P"
```
```  1067   shows "P"
```
```  1068   using wf unfolding wfactors_def by (fast dest: e)
```
```  1069
```
```  1070 lemma (in monoid) factorsI:
```
```  1071   assumes "\<forall>f\<in>set fs. irreducible G f"
```
```  1072     and "foldr (\<otimes>) fs \<one> = a"
```
```  1073   shows "factors G fs a"
```
```  1074   using assms unfolding factors_def by simp
```
```  1075
```
```  1076 lemma factorsE:
```
```  1077   fixes G (structure)
```
```  1078   assumes f: "factors G fs a"
```
```  1079     and e: "\<lbrakk>\<forall>f\<in>set fs. irreducible G f; foldr (\<otimes>) fs \<one> = a\<rbrakk> \<Longrightarrow> P"
```
```  1080   shows "P"
```
```  1081   using f unfolding factors_def by (simp add: e)
```
```  1082
```
```  1083 lemma (in monoid) factors_wfactors:
```
```  1084   assumes "factors G as a" and "set as \<subseteq> carrier G"
```
```  1085   shows "wfactors G as a"
```
```  1086   using assms by (blast elim: factorsE intro: wfactorsI)
```
```  1087
```
```  1088 lemma (in monoid) wfactors_factors:
```
```  1089   assumes "wfactors G as a" and "set as \<subseteq> carrier G"
```
```  1090   shows "\<exists>a'. factors G as a' \<and> a' \<sim> a"
```
```  1091   using assms by (blast elim: wfactorsE intro: factorsI)
```
```  1092
```
```  1093 lemma (in monoid) factors_closed [dest]:
```
```  1094   assumes "factors G fs a" and "set fs \<subseteq> carrier G"
```
```  1095   shows "a \<in> carrier G"
```
```  1096   using assms by (elim factorsE, clarsimp)
```
```  1097
```
```  1098 lemma (in monoid) nunit_factors:
```
```  1099   assumes anunit: "a \<notin> Units G"
```
```  1100     and fs: "factors G as a"
```
```  1101   shows "length as > 0"
```
```  1102 proof -
```
```  1103   from anunit Units_one_closed have "a \<noteq> \<one>" by auto
```
```  1104   with fs show ?thesis by (auto elim: factorsE)
```
```  1105 qed
```
```  1106
```
```  1107 lemma (in monoid) unit_wfactors [simp]:
```
```  1108   assumes aunit: "a \<in> Units G"
```
```  1109   shows "wfactors G [] a"
```
```  1110   using aunit by (intro wfactorsI) (simp, simp add: Units_assoc)
```
```  1111
```
```  1112 lemma (in comm_monoid_cancel) unit_wfactors_empty:
```
```  1113   assumes aunit: "a \<in> Units G"
```
```  1114     and wf: "wfactors G fs a"
```
```  1115     and carr[simp]: "set fs \<subseteq> carrier G"
```
```  1116   shows "fs = []"
```
```  1117 proof (cases fs)
```
```  1118   case Nil
```
```  1119   then show ?thesis .
```
```  1120 next
```
```  1121   case fs: (Cons f fs')
```
```  1122   from carr have fcarr[simp]: "f \<in> carrier G" and carr'[simp]: "set fs' \<subseteq> carrier G"
```
```  1123     by (simp_all add: fs)
```
```  1124
```
```  1125   from fs wf have "irreducible G f" by (simp add: wfactors_def)
```
```  1126   then have fnunit: "f \<notin> Units G" by (fast elim: irreducibleE)
```
```  1127
```
```  1128   from fs wf have a: "f \<otimes> foldr (\<otimes>) fs' \<one> \<sim> a" by (simp add: wfactors_def)
```
```  1129
```
```  1130   note aunit
```
```  1131   also from fs wf
```
```  1132   have a: "f \<otimes> foldr (\<otimes>) fs' \<one> \<sim> a" by (simp add: wfactors_def)
```
```  1133   have "a \<sim> f \<otimes> foldr (\<otimes>) fs' \<one>"
```
```  1134     by (simp add: Units_closed[OF aunit] a[symmetric])
```
```  1135   finally have "f \<otimes> foldr (\<otimes>) fs' \<one> \<in> Units G" by simp
```
```  1136   then have "f \<in> Units G" by (intro unit_factor[of f], simp+)
```
```  1137   with fnunit show ?thesis by contradiction
```
```  1138 qed
```
```  1139
```
```  1140
```
```  1141 text \<open>Comparing wfactors\<close>
```
```  1142
```
```  1143 lemma (in comm_monoid_cancel) wfactors_listassoc_cong_l:
```
```  1144   assumes fact: "wfactors G fs a"
```
```  1145     and asc: "fs [\<sim>] fs'"
```
```  1146     and carr: "a \<in> carrier G"  "set fs \<subseteq> carrier G"  "set fs' \<subseteq> carrier G"
```
```  1147   shows "wfactors G fs' a"
```
```  1148 proof -
```
```  1149   { from asc[symmetric] have "foldr (\<otimes>) fs' \<one> \<sim> foldr (\<otimes>) fs \<one>"
```
```  1150       by (simp add: multlist_listassoc_cong carr)
```
```  1151     also assume "foldr (\<otimes>) fs \<one> \<sim> a"
```
```  1152     finally have "foldr (\<otimes>) fs' \<one> \<sim> a" by (simp add: carr) }
```
```  1153   then show ?thesis
```
```  1154   using fact
```
```  1155   by (meson asc carr(2) carr(3) irrlist_listassoc_cong wfactors_def)
```
```  1156 qed
```
```  1157
```
```  1158 lemma (in comm_monoid) wfactors_perm_cong_l:
```
```  1159   assumes "wfactors G fs a"
```
```  1160     and "fs <~~> fs'"
```
```  1161     and "set fs \<subseteq> carrier G"
```
```  1162   shows "wfactors G fs' a"
```
```  1163   using assms irrlist_perm_cong multlist_perm_cong wfactors_def by fastforce
```
```  1164
```
```  1165 lemma (in comm_monoid_cancel) wfactors_ee_cong_l [trans]:
```
```  1166   assumes ee: "essentially_equal G as bs"
```
```  1167     and bfs: "wfactors G bs b"
```
```  1168     and carr: "b \<in> carrier G"  "set as \<subseteq> carrier G"  "set bs \<subseteq> carrier G"
```
```  1169   shows "wfactors G as b"
```
```  1170   using ee
```
```  1171 proof (elim essentially_equalE)
```
```  1172   fix fs
```
```  1173   assume prm: "as <~~> fs"
```
```  1174   with carr have fscarr: "set fs \<subseteq> carrier G" by (simp add: perm_closed)
```
```  1175
```
```  1176   note bfs
```
```  1177   also assume [symmetric]: "fs [\<sim>] bs"
```
```  1178   also (wfactors_listassoc_cong_l)
```
```  1179   note prm[symmetric]
```
```  1180   finally (wfactors_perm_cong_l)
```
```  1181   show "wfactors G as b" by (simp add: carr fscarr)
```
```  1182 qed
```
```  1183
```
```  1184 lemma (in monoid) wfactors_cong_r [trans]:
```
```  1185   assumes fac: "wfactors G fs a" and aa': "a \<sim> a'"
```
```  1186     and carr[simp]: "a \<in> carrier G"  "a' \<in> carrier G"  "set fs \<subseteq> carrier G"
```
```  1187   shows "wfactors G fs a'"
```
```  1188   using fac
```
```  1189 proof (elim wfactorsE, intro wfactorsI)
```
```  1190   assume "foldr (\<otimes>) fs \<one> \<sim> a" also note aa'
```
```  1191   finally show "foldr (\<otimes>) fs \<one> \<sim> a'" by simp
```
```  1192 qed
```
```  1193
```
```  1194
```
```  1195 subsubsection \<open>Essentially equal factorizations\<close>
```
```  1196
```
```  1197 lemma (in comm_monoid_cancel) unitfactor_ee:
```
```  1198   assumes uunit: "u \<in> Units G"
```
```  1199     and carr: "set as \<subseteq> carrier G"
```
```  1200   shows "essentially_equal G (as[0 := (as!0 \<otimes> u)]) as"
```
```  1201     (is "essentially_equal G ?as' as")
```
```  1202 proof -
```
```  1203   have "as[0 := as ! 0 \<otimes> u] [\<sim>] as"
```
```  1204   proof (cases as)
```
```  1205     case (Cons a as')
```
```  1206     then show ?thesis
```
```  1207       using associatedI2 carr uunit by auto
```
```  1208   qed auto
```
```  1209   then show ?thesis
```
```  1210     using essentially_equal_def by blast
```
```  1211 qed
```
```  1212
```
```  1213 lemma (in comm_monoid_cancel) factors_cong_unit:
```
```  1214   assumes u: "u \<in> Units G"
```
```  1215     and a: "a \<notin> Units G"
```
```  1216     and afs: "factors G as a"
```
```  1217     and ascarr: "set as \<subseteq> carrier G"
```
```  1218   shows "factors G (as[0 := (as!0 \<otimes> u)]) (a \<otimes> u)"
```
```  1219     (is "factors G ?as' ?a'")
```
```  1220 proof (cases as)
```
```  1221   case Nil
```
```  1222   then show ?thesis
```
```  1223     using afs a nunit_factors by auto
```
```  1224 next
```
```  1225   case (Cons b bs)
```
```  1226   have *: "\<forall>f\<in>set as. irreducible G f" "foldr (\<otimes>) as \<one> = a"
```
```  1227     using afs  by (auto simp: factors_def)
```
```  1228   show ?thesis
```
```  1229   proof (intro factorsI)
```
```  1230     show "foldr (\<otimes>) (as[0 := as ! 0 \<otimes> u]) \<one> = a \<otimes> u"
```
```  1231       using Cons u ascarr * by (auto simp add: m_ac Units_closed)
```
```  1232     show "\<forall>f\<in>set (as[0 := as ! 0 \<otimes> u]). irreducible G f"
```
```  1233       using Cons u ascarr * by (force intro: irreducible_prod_rI)
```
```  1234   qed
```
```  1235 qed
```
```  1236
```
```  1237 lemma (in comm_monoid) perm_wfactorsD:
```
```  1238   assumes prm: "as <~~> bs"
```
```  1239     and afs: "wfactors G as a"
```
```  1240     and bfs: "wfactors G bs b"
```
```  1241     and [simp]: "a \<in> carrier G"  "b \<in> carrier G"
```
```  1242     and ascarr [simp]: "set as \<subseteq> carrier G"
```
```  1243   shows "a \<sim> b"
```
```  1244   using afs bfs
```
```  1245 proof (elim wfactorsE)
```
```  1246   from prm have [simp]: "set bs \<subseteq> carrier G" by (simp add: perm_closed)
```
```  1247   assume "foldr (\<otimes>) as \<one> \<sim> a"
```
```  1248   then have "a \<sim> foldr (\<otimes>) as \<one>"
```
```  1249     by (simp add: associated_sym)
```
```  1250   also from prm
```
```  1251   have "foldr (\<otimes>) as \<one> = foldr (\<otimes>) bs \<one>" by (rule multlist_perm_cong, simp)
```
```  1252   also assume "foldr (\<otimes>) bs \<one> \<sim> b"
```
```  1253   finally show "a \<sim> b" by simp
```
```  1254 qed
```
```  1255
```
```  1256 lemma (in comm_monoid_cancel) listassoc_wfactorsD:
```
```  1257   assumes assoc: "as [\<sim>] bs"
```
```  1258     and afs: "wfactors G as a"
```
```  1259     and bfs: "wfactors G bs b"
```
```  1260     and [simp]: "a \<in> carrier G"  "b \<in> carrier G"
```
```  1261     and [simp]: "set as \<subseteq> carrier G"  "set bs \<subseteq> carrier G"
```
```  1262   shows "a \<sim> b"
```
```  1263   using afs bfs
```
```  1264 proof (elim wfactorsE)
```
```  1265   assume "foldr (\<otimes>) as \<one> \<sim> a"
```
```  1266   then have "a \<sim> foldr (\<otimes>) as \<one>" by (simp add: associated_sym)
```
```  1267   also from assoc
```
```  1268   have "foldr (\<otimes>) as \<one> \<sim> foldr (\<otimes>) bs \<one>" by (rule multlist_listassoc_cong, simp+)
```
```  1269   also assume "foldr (\<otimes>) bs \<one> \<sim> b"
```
```  1270   finally show "a \<sim> b" by simp
```
```  1271 qed
```
```  1272
```
```  1273 lemma (in comm_monoid_cancel) ee_wfactorsD:
```
```  1274   assumes ee: "essentially_equal G as bs"
```
```  1275     and afs: "wfactors G as a" and bfs: "wfactors G bs b"
```
```  1276     and [simp]: "a \<in> carrier G"  "b \<in> carrier G"
```
```  1277     and ascarr[simp]: "set as \<subseteq> carrier G" and bscarr[simp]: "set bs \<subseteq> carrier G"
```
```  1278   shows "a \<sim> b"
```
```  1279   using ee
```
```  1280 proof (elim essentially_equalE)
```
```  1281   fix fs
```
```  1282   assume prm: "as <~~> fs"
```
```  1283   then have as'carr[simp]: "set fs \<subseteq> carrier G"
```
```  1284     by (simp add: perm_closed)
```
```  1285   from afs prm have afs': "wfactors G fs a"
```
```  1286     by (rule wfactors_perm_cong_l) simp
```
```  1287   assume "fs [\<sim>] bs"
```
```  1288   from this afs' bfs show "a \<sim> b"
```
```  1289     by (rule listassoc_wfactorsD) simp_all
```
```  1290 qed
```
```  1291
```
```  1292 lemma (in comm_monoid_cancel) ee_factorsD:
```
```  1293   assumes ee: "essentially_equal G as bs"
```
```  1294     and afs: "factors G as a" and bfs:"factors G bs b"
```
```  1295     and "set as \<subseteq> carrier G"  "set bs \<subseteq> carrier G"
```
```  1296   shows "a \<sim> b"
```
```  1297   using assms by (blast intro: factors_wfactors dest: ee_wfactorsD)
```
```  1298
```
```  1299 lemma (in factorial_monoid) ee_factorsI:
```
```  1300   assumes ab: "a \<sim> b"
```
```  1301     and afs: "factors G as a" and anunit: "a \<notin> Units G"
```
```  1302     and bfs: "factors G bs b" and bnunit: "b \<notin> Units G"
```
```  1303     and ascarr: "set as \<subseteq> carrier G" and bscarr: "set bs \<subseteq> carrier G"
```
```  1304   shows "essentially_equal G as bs"
```
```  1305 proof -
```
```  1306   note carr[simp] = factors_closed[OF afs ascarr] ascarr[THEN subsetD]
```
```  1307     factors_closed[OF bfs bscarr] bscarr[THEN subsetD]
```
```  1308
```
```  1309   from ab carr obtain u where uunit: "u \<in> Units G" and a: "a = b \<otimes> u"
```
```  1310     by (elim associatedE2)
```
```  1311
```
```  1312   from uunit bscarr have ee: "essentially_equal G (bs[0 := (bs!0 \<otimes> u)]) bs"
```
```  1313     (is "essentially_equal G ?bs' bs")
```
```  1314     by (rule unitfactor_ee)
```
```  1315
```
```  1316   from bscarr uunit have bs'carr: "set ?bs' \<subseteq> carrier G"
```
```  1317     by (cases bs) (simp_all add: Units_closed)
```
```  1318
```
```  1319   from uunit bnunit bfs bscarr have fac: "factors G ?bs' (b \<otimes> u)"
```
```  1320     by (rule factors_cong_unit)
```
```  1321
```
```  1322   from afs fac[simplified a[symmetric]] ascarr bs'carr anunit
```
```  1323   have "essentially_equal G as ?bs'"
```
```  1324     by (blast intro: factors_unique)
```
```  1325   also note ee
```
```  1326   finally show "essentially_equal G as bs"
```
```  1327     by (simp add: ascarr bscarr bs'carr)
```
```  1328 qed
```
```  1329
```
```  1330 lemma (in factorial_monoid) ee_wfactorsI:
```
```  1331   assumes asc: "a \<sim> b"
```
```  1332     and asf: "wfactors G as a" and bsf: "wfactors G bs b"
```
```  1333     and acarr[simp]: "a \<in> carrier G" and bcarr[simp]: "b \<in> carrier G"
```
```  1334     and ascarr[simp]: "set as \<subseteq> carrier G" and bscarr[simp]: "set bs \<subseteq> carrier G"
```
```  1335   shows "essentially_equal G as bs"
```
```  1336   using assms
```
```  1337 proof (cases "a \<in> Units G")
```
```  1338   case aunit: True
```
```  1339   also note asc
```
```  1340   finally have bunit: "b \<in> Units G" by simp
```
```  1341
```
```  1342   from aunit asf ascarr have e: "as = []"
```
```  1343     by (rule unit_wfactors_empty)
```
```  1344   from bunit bsf bscarr have e': "bs = []"
```
```  1345     by (rule unit_wfactors_empty)
```
```  1346
```
```  1347   have "essentially_equal G [] []"
```
```  1348     by (fast intro: essentially_equalI)
```
```  1349   then show ?thesis
```
```  1350     by (simp add: e e')
```
```  1351 next
```
```  1352   case anunit: False
```
```  1353   have bnunit: "b \<notin> Units G"
```
```  1354   proof clarify
```
```  1355     assume "b \<in> Units G"
```
```  1356     also note asc[symmetric]
```
```  1357     finally have "a \<in> Units G" by simp
```
```  1358     with anunit show False ..
```
```  1359   qed
```
```  1360
```
```  1361   from wfactors_factors[OF asf ascarr] obtain a' where fa': "factors G as a'" and a': "a' \<sim> a"
```
```  1362     by blast
```
```  1363   from fa' ascarr have a'carr[simp]: "a' \<in> carrier G"
```
```  1364     by fast
```
```  1365
```
```  1366   have a'nunit: "a' \<notin> Units G"
```
```  1367   proof clarify
```
```  1368     assume "a' \<in> Units G"
```
```  1369     also note a'
```
```  1370     finally have "a \<in> Units G" by simp
```
```  1371     with anunit
```
```  1372     show "False" ..
```
```  1373   qed
```
```  1374
```
```  1375   from wfactors_factors[OF bsf bscarr] obtain b' where fb': "factors G bs b'" and b': "b' \<sim> b"
```
```  1376     by blast
```
```  1377   from fb' bscarr have b'carr[simp]: "b' \<in> carrier G"
```
```  1378     by fast
```
```  1379
```
```  1380   have b'nunit: "b' \<notin> Units G"
```
```  1381   proof clarify
```
```  1382     assume "b' \<in> Units G"
```
```  1383     also note b'
```
```  1384     finally have "b \<in> Units G" by simp
```
```  1385     with bnunit show False ..
```
```  1386   qed
```
```  1387
```
```  1388   note a'
```
```  1389   also note asc
```
```  1390   also note b'[symmetric]
```
```  1391   finally have "a' \<sim> b'" by simp
```
```  1392   from this fa' a'nunit fb' b'nunit ascarr bscarr show "essentially_equal G as bs"
```
```  1393     by (rule ee_factorsI)
```
```  1394 qed
```
```  1395
```
```  1396 lemma (in factorial_monoid) ee_wfactors:
```
```  1397   assumes asf: "wfactors G as a"
```
```  1398     and bsf: "wfactors G bs b"
```
```  1399     and acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G"
```
```  1400     and ascarr: "set as \<subseteq> carrier G" and bscarr: "set bs \<subseteq> carrier G"
```
```  1401   shows asc: "a \<sim> b = essentially_equal G as bs"
```
```  1402   using assms by (fast intro: ee_wfactorsI ee_wfactorsD)
```
```  1403
```
```  1404 lemma (in factorial_monoid) wfactors_exist [intro, simp]:
```
```  1405   assumes acarr[simp]: "a \<in> carrier G"
```
```  1406   shows "\<exists>fs. set fs \<subseteq> carrier G \<and> wfactors G fs a"
```
```  1407 proof (cases "a \<in> Units G")
```
```  1408   case True
```
```  1409   then have "wfactors G [] a" by (rule unit_wfactors)
```
```  1410   then show ?thesis by (intro exI) force
```
```  1411 next
```
```  1412   case False
```
```  1413   with factors_exist [OF acarr] obtain fs where fscarr: "set fs \<subseteq> carrier G" and f: "factors G fs a"
```
```  1414     by blast
```
```  1415   from f have "wfactors G fs a" by (rule factors_wfactors) fact
```
```  1416   with fscarr show ?thesis by fast
```
```  1417 qed
```
```  1418
```
```  1419 lemma (in monoid) wfactors_prod_exists [intro, simp]:
```
```  1420   assumes "\<forall>a \<in> set as. irreducible G a" and "set as \<subseteq> carrier G"
```
```  1421   shows "\<exists>a. a \<in> carrier G \<and> wfactors G as a"
```
```  1422   unfolding wfactors_def using assms by blast
```
```  1423
```
```  1424 lemma (in factorial_monoid) wfactors_unique:
```
```  1425   assumes "wfactors G fs a"
```
```  1426     and "wfactors G fs' a"
```
```  1427     and "a \<in> carrier G"
```
```  1428     and "set fs \<subseteq> carrier G"
```
```  1429     and "set fs' \<subseteq> carrier G"
```
```  1430   shows "essentially_equal G fs fs'"
```
```  1431   using assms by (fast intro: ee_wfactorsI[of a a])
```
```  1432
```
```  1433 lemma (in monoid) factors_mult_single:
```
```  1434   assumes "irreducible G a" and "factors G fb b" and "a \<in> carrier G"
```
```  1435   shows "factors G (a # fb) (a \<otimes> b)"
```
```  1436   using assms unfolding factors_def by simp
```
```  1437
```
```  1438 lemma (in monoid_cancel) wfactors_mult_single:
```
```  1439   assumes f: "irreducible G a"  "wfactors G fb b"
```
```  1440     "a \<in> carrier G"  "b \<in> carrier G"  "set fb \<subseteq> carrier G"
```
```  1441   shows "wfactors G (a # fb) (a \<otimes> b)"
```
```  1442   using assms unfolding wfactors_def by (simp add: mult_cong_r)
```
```  1443
```
```  1444 lemma (in monoid) factors_mult:
```
```  1445   assumes factors: "factors G fa a"  "factors G fb b"
```
```  1446     and ascarr: "set fa \<subseteq> carrier G"
```
```  1447     and bscarr: "set fb \<subseteq> carrier G"
```
```  1448   shows "factors G (fa @ fb) (a \<otimes> b)"
```
```  1449 proof -
```
```  1450   have "foldr (\<otimes>) (fa @ fb) \<one> = foldr (\<otimes>) fa \<one> \<otimes> foldr (\<otimes>) fb \<one>" if "set fa \<subseteq> carrier G"
```
```  1451     "Ball (set fa) (irreducible G)"
```
```  1452     using that bscarr by (induct fa) (simp_all add: m_assoc)
```
```  1453   then show ?thesis
```
```  1454     using assms unfolding factors_def by force
```
```  1455 qed
```
```  1456
```
```  1457 lemma (in comm_monoid_cancel) wfactors_mult [intro]:
```
```  1458   assumes asf: "wfactors G as a" and bsf:"wfactors G bs b"
```
```  1459     and acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G"
```
```  1460     and ascarr: "set as \<subseteq> carrier G" and bscarr:"set bs \<subseteq> carrier G"
```
```  1461   shows "wfactors G (as @ bs) (a \<otimes> b)"
```
```  1462   using wfactors_factors[OF asf ascarr] and wfactors_factors[OF bsf bscarr]
```
```  1463 proof clarsimp
```
```  1464   fix a' b'
```
```  1465   assume asf': "factors G as a'" and a'a: "a' \<sim> a"
```
```  1466     and bsf': "factors G bs b'" and b'b: "b' \<sim> b"
```
```  1467   from asf' have a'carr: "a' \<in> carrier G" by (rule factors_closed) fact
```
```  1468   from bsf' have b'carr: "b' \<in> carrier G" by (rule factors_closed) fact
```
```  1469
```
```  1470   note carr = acarr bcarr a'carr b'carr ascarr bscarr
```
```  1471
```
```  1472   from asf' bsf' have "factors G (as @ bs) (a' \<otimes> b')"
```
```  1473     by (rule factors_mult) fact+
```
```  1474
```
```  1475   with carr have abf': "wfactors G (as @ bs) (a' \<otimes> b')"
```
```  1476     by (intro factors_wfactors) simp_all
```
```  1477   also from b'b carr have trb: "a' \<otimes> b' \<sim> a' \<otimes> b"
```
```  1478     by (intro mult_cong_r)
```
```  1479   also from a'a carr have tra: "a' \<otimes> b \<sim> a \<otimes> b"
```
```  1480     by (intro mult_cong_l)
```
```  1481   finally show "wfactors G (as @ bs) (a \<otimes> b)"
```
```  1482     by (simp add: carr)
```
```  1483 qed
```
```  1484
```
```  1485 lemma (in comm_monoid) factors_dividesI:
```
```  1486   assumes "factors G fs a"
```
```  1487     and "f \<in> set fs"
```
```  1488     and "set fs \<subseteq> carrier G"
```
```  1489   shows "f divides a"
```
```  1490   using assms by (fast elim: factorsE intro: multlist_dividesI)
```
```  1491
```
```  1492 lemma (in comm_monoid) wfactors_dividesI:
```
```  1493   assumes p: "wfactors G fs a"
```
```  1494     and fscarr: "set fs \<subseteq> carrier G" and acarr: "a \<in> carrier G"
```
```  1495     and f: "f \<in> set fs"
```
```  1496   shows "f divides a"
```
```  1497   using wfactors_factors[OF p fscarr]
```
```  1498 proof clarsimp
```
```  1499   fix a'
```
```  1500   assume fsa': "factors G fs a'" and a'a: "a' \<sim> a"
```
```  1501   with fscarr have a'carr: "a' \<in> carrier G"
```
```  1502     by (simp add: factors_closed)
```
```  1503
```
```  1504   from fsa' fscarr f have "f divides a'"
```
```  1505     by (fast intro: factors_dividesI)
```
```  1506   also note a'a
```
```  1507   finally show "f divides a"
```
```  1508     by (simp add: f fscarr[THEN subsetD] acarr a'carr)
```
```  1509 qed
```
```  1510
```
```  1511
```
```  1512 subsubsection \<open>Factorial monoids and wfactors\<close>
```
```  1513
```
```  1514 lemma (in comm_monoid_cancel) factorial_monoidI:
```
```  1515   assumes wfactors_exists: "\<And>a. a \<in> carrier G \<Longrightarrow> \<exists>fs. set fs \<subseteq> carrier G \<and> wfactors G fs a"
```
```  1516     and wfactors_unique:
```
```  1517       "\<And>a fs fs'. \<lbrakk>a \<in> carrier G; set fs \<subseteq> carrier G; set fs' \<subseteq> carrier G;
```
```  1518         wfactors G fs a; wfactors G fs' a\<rbrakk> \<Longrightarrow> essentially_equal G fs fs'"
```
```  1519   shows "factorial_monoid G"
```
```  1520 proof
```
```  1521   fix a
```
```  1522   assume acarr: "a \<in> carrier G" and anunit: "a \<notin> Units G"
```
```  1523
```
```  1524   from wfactors_exists[OF acarr]
```
```  1525   obtain as where ascarr: "set as \<subseteq> carrier G" and afs: "wfactors G as a"
```
```  1526     by blast
```
```  1527   from wfactors_factors [OF afs ascarr] obtain a' where afs': "factors G as a'" and a'a: "a' \<sim> a"
```
```  1528     by blast
```
```  1529   from afs' ascarr have a'carr: "a' \<in> carrier G"
```
```  1530     by fast
```
```  1531   have a'nunit: "a' \<notin> Units G"
```
```  1532   proof clarify
```
```  1533     assume "a' \<in> Units G"
```
```  1534     also note a'a
```
```  1535     finally have "a \<in> Units G" by (simp add: acarr)
```
```  1536     with anunit show False ..
```
```  1537   qed
```
```  1538
```
```  1539   from a'carr acarr a'a obtain u where uunit: "u \<in> Units G" and a': "a' = a \<otimes> u"
```
```  1540     by (blast elim: associatedE2)
```
```  1541
```
```  1542   note [simp] = acarr Units_closed[OF uunit] Units_inv_closed[OF uunit]
```
```  1543
```
```  1544   have "a = a \<otimes> \<one>" by simp
```
```  1545   also have "\<dots> = a \<otimes> (u \<otimes> inv u)" by (simp add: uunit)
```
```  1546   also have "\<dots> = a' \<otimes> inv u" by (simp add: m_assoc[symmetric] a'[symmetric])
```
```  1547   finally have a: "a = a' \<otimes> inv u" .
```
```  1548
```
```  1549   from ascarr uunit have cr: "set (as[0:=(as!0 \<otimes> inv u)]) \<subseteq> carrier G"
```
```  1550     by (cases as) auto
```
```  1551
```
```  1552   from afs' uunit a'nunit acarr ascarr have "factors G (as[0:=(as!0 \<otimes> inv u)]) a"
```
```  1553     by (simp add: a factors_cong_unit)
```
```  1554   with cr show "\<exists>fs. set fs \<subseteq> carrier G \<and> factors G fs a"
```
```  1555     by fast
```
```  1556 qed (blast intro: factors_wfactors wfactors_unique)
```
```  1557
```
```  1558
```
```  1559 subsection \<open>Factorizations as Multisets\<close>
```
```  1560
```
```  1561 text \<open>Gives useful operations like intersection\<close>
```
```  1562
```
```  1563 (* FIXME: use class_of x instead of closure_of {x} *)
```
```  1564
```
```  1565 abbreviation "assocs G x \<equiv> eq_closure_of (division_rel G) {x}"
```
```  1566
```
```  1567 definition "fmset G as = mset (map (\<lambda>a. assocs G a) as)"
```
```  1568
```
```  1569
```
```  1570 text \<open>Helper lemmas\<close>
```
```  1571
```
```  1572 lemma (in monoid) assocs_repr_independence:
```
```  1573   assumes "y \<in> assocs G x" "x \<in> carrier G"
```
```  1574   shows "assocs G x = assocs G y"
```
```  1575   using assms
```
```  1576   by (simp add: eq_closure_of_def elem_def) (use associated_sym associated_trans in \<open>blast+\<close>)
```
```  1577
```
```  1578 lemma (in monoid) assocs_self:
```
```  1579   assumes "x \<in> carrier G"
```
```  1580   shows "x \<in> assocs G x"
```
```  1581   using assms by (fastforce intro: closure_ofI2)
```
```  1582
```
```  1583 lemma (in monoid) assocs_repr_independenceD:
```
```  1584   assumes repr: "assocs G x = assocs G y" and ycarr: "y \<in> carrier G"
```
```  1585   shows "y \<in> assocs G x"
```
```  1586   unfolding repr using ycarr by (intro assocs_self)
```
```  1587
```
```  1588 lemma (in comm_monoid) assocs_assoc:
```
```  1589   assumes "a \<in> assocs G b" "b \<in> carrier G"
```
```  1590   shows "a \<sim> b"
```
```  1591   using assms by (elim closure_ofE2) simp
```
```  1592
```
```  1593 lemmas (in comm_monoid) assocs_eqD = assocs_repr_independenceD[THEN assocs_assoc]
```
```  1594
```
```  1595
```
```  1596 subsubsection \<open>Comparing multisets\<close>
```
```  1597
```
```  1598 lemma (in monoid) fmset_perm_cong:
```
```  1599   assumes prm: "as <~~> bs"
```
```  1600   shows "fmset G as = fmset G bs"
```
```  1601   using perm_map[OF prm] unfolding mset_eq_perm fmset_def by blast
```
```  1602
```
```  1603 lemma (in comm_monoid_cancel) eqc_listassoc_cong:
```
```  1604   assumes "as [\<sim>] bs" and "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G"
```
```  1605   shows "map (assocs G) as = map (assocs G) bs"
```
```  1606   using assms
```
```  1607 proof (induction as arbitrary: bs)
```
```  1608   case Nil
```
```  1609   then show ?case by simp
```
```  1610 next
```
```  1611   case (Cons a as)
```
```  1612   then show ?case
```
```  1613   proof (clarsimp simp add: Cons_eq_map_conv list_all2_Cons1)
```
```  1614     fix z zs
```
```  1615     assume zzs: "a \<in> carrier G" "set as \<subseteq> carrier G" "bs = z # zs" "a \<sim> z"
```
```  1616       "as [\<sim>] zs" "z \<in> carrier G" "set zs \<subseteq> carrier G"
```
```  1617     then show "assocs G a = assocs G z"
```
```  1618       apply (simp add: eq_closure_of_def elem_def)
```
```  1619       using \<open>a \<in> carrier G\<close> \<open>z \<in> carrier G\<close> \<open>a \<sim> z\<close> associated_sym associated_trans by blast+
```
```  1620   qed
```
```  1621 qed
```
```  1622
```
```  1623 lemma (in comm_monoid_cancel) fmset_listassoc_cong:
```
```  1624   assumes "as [\<sim>] bs"
```
```  1625     and "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G"
```
```  1626   shows "fmset G as = fmset G bs"
```
```  1627   using assms unfolding fmset_def by (simp add: eqc_listassoc_cong)
```
```  1628
```
```  1629 lemma (in comm_monoid_cancel) ee_fmset:
```
```  1630   assumes ee: "essentially_equal G as bs"
```
```  1631     and ascarr: "set as \<subseteq> carrier G" and bscarr: "set bs \<subseteq> carrier G"
```
```  1632   shows "fmset G as = fmset G bs"
```
```  1633   using ee
```
```  1634 proof (elim essentially_equalE)
```
```  1635   fix as'
```
```  1636   assume prm: "as <~~> as'"
```
```  1637   from prm ascarr have as'carr: "set as' \<subseteq> carrier G"
```
```  1638     by (rule perm_closed)
```
```  1639   from prm have "fmset G as = fmset G as'"
```
```  1640     by (rule fmset_perm_cong)
```
```  1641   also assume "as' [\<sim>] bs"
```
```  1642   with as'carr bscarr have "fmset G as' = fmset G bs"
```
```  1643     by (simp add: fmset_listassoc_cong)
```
```  1644   finally show "fmset G as = fmset G bs" .
```
```  1645 qed
```
```  1646
```
```  1647 lemma (in monoid_cancel) fmset_ee_aux:
```
```  1648   assumes "cas <~~> cbs" "cas = map (assocs G) as" "cbs = map (assocs G) bs"
```
```  1649   shows "\<exists>as'. as <~~> as' \<and> map (assocs G) as' = cbs"
```
```  1650   using assms
```
```  1651 proof (induction cas cbs arbitrary: as bs rule: perm.induct)
```
```  1652   case (Cons xs ys z)
```
```  1653   then show ?case
```
```  1654     by (clarsimp simp add: map_eq_Cons_conv) blast
```
```  1655 next
```
```  1656   case (trans xs ys zs)
```
```  1657   then show ?case
```
```  1658     by (smt ex_map_conv perm.trans perm_setP)
```
```  1659 qed auto
```
```  1660
```
```  1661 lemma (in comm_monoid_cancel) fmset_ee:
```
```  1662   assumes mset: "fmset G as = fmset G bs"
```
```  1663     and ascarr: "set as \<subseteq> carrier G" and bscarr: "set bs \<subseteq> carrier G"
```
```  1664   shows "essentially_equal G as bs"
```
```  1665 proof -
```
```  1666   from mset have "map (assocs G) as <~~> map (assocs G) bs"
```
```  1667     by (simp add: fmset_def mset_eq_perm del: mset_map)
```
```  1668   then obtain as' where tp: "as <~~> as'" and tm: "map (assocs G) as' = map (assocs G) bs"
```
```  1669     using fmset_ee_aux by blast
```
```  1670   with ascarr have as'carr: "set as' \<subseteq> carrier G"
```
```  1671     using perm_closed by blast
```
```  1672   from tm as'carr[THEN subsetD] bscarr[THEN subsetD] have "as' [\<sim>] bs"
```
```  1673     by (induct as' arbitrary: bs) (simp, fastforce dest: assocs_eqD[THEN associated_sym])
```
```  1674   with tp show "essentially_equal G as bs"
```
```  1675     by (fast intro: essentially_equalI)
```
```  1676 qed
```
```  1677
```
```  1678 lemma (in comm_monoid_cancel) ee_is_fmset:
```
```  1679   assumes "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G"
```
```  1680   shows "essentially_equal G as bs = (fmset G as = fmset G bs)"
```
```  1681   using assms by (fast intro: ee_fmset fmset_ee)
```
```  1682
```
```  1683
```
```  1684 subsubsection \<open>Interpreting multisets as factorizations\<close>
```
```  1685
```
```  1686 lemma (in monoid) mset_fmsetEx:
```
```  1687   assumes elems: "\<And>X. X \<in> set_mset Cs \<Longrightarrow> \<exists>x. P x \<and> X = assocs G x"
```
```  1688   shows "\<exists>cs. (\<forall>c \<in> set cs. P c) \<and> fmset G cs = Cs"
```
```  1689 proof -
```
```  1690   from surjE[OF surj_mset] obtain Cs' where Cs: "Cs = mset Cs'"
```
```  1691     by blast
```
```  1692   have "\<exists>cs. (\<forall>c \<in> set cs. P c) \<and> mset (map (assocs G) cs) = Cs"
```
```  1693     using elems unfolding Cs
```
```  1694   proof (induction Cs')
```
```  1695     case (Cons a Cs')
```
```  1696     then obtain c cs where csP: "\<forall>x\<in>set cs. P x" and mset: "mset (map (assocs G) cs) = mset Cs'"
```
```  1697             and cP: "P c" and a: "a = assocs G c"
```
```  1698       by force
```
```  1699     then have tP: "\<forall>x\<in>set (c#cs). P x"
```
```  1700       by simp
```
```  1701     show ?case
```
```  1702       using tP mset a by fastforce
```
```  1703   qed auto
```
```  1704   then show ?thesis by (simp add: fmset_def)
```
```  1705 qed
```
```  1706
```
```  1707 lemma (in monoid) mset_wfactorsEx:
```
```  1708   assumes elems: "\<And>X. X \<in> set_mset Cs \<Longrightarrow> \<exists>x. (x \<in> carrier G \<and> irreducible G x) \<and> X = assocs G x"
```
```  1709   shows "\<exists>c cs. c \<in> carrier G \<and> set cs \<subseteq> carrier G \<and> wfactors G cs c \<and> fmset G cs = Cs"
```
```  1710 proof -
```
```  1711   have "\<exists>cs. (\<forall>c\<in>set cs. c \<in> carrier G \<and> irreducible G c) \<and> fmset G cs = Cs"
```
```  1712     by (intro mset_fmsetEx, rule elems)
```
```  1713   then obtain cs where p[rule_format]: "\<forall>c\<in>set cs. c \<in> carrier G \<and> irreducible G c"
```
```  1714     and Cs[symmetric]: "fmset G cs = Cs" by auto
```
```  1715   from p have cscarr: "set cs \<subseteq> carrier G" by fast
```
```  1716   from p have "\<exists>c. c \<in> carrier G \<and> wfactors G cs c"
```
```  1717     by (intro wfactors_prod_exists) auto
```
```  1718   then obtain c where ccarr: "c \<in> carrier G" and cfs: "wfactors G cs c" by auto
```
```  1719   with cscarr Cs show ?thesis by fast
```
```  1720 qed
```
```  1721
```
```  1722
```
```  1723 subsubsection \<open>Multiplication on multisets\<close>
```
```  1724
```
```  1725 lemma (in factorial_monoid) mult_wfactors_fmset:
```
```  1726   assumes afs: "wfactors G as a"
```
```  1727     and bfs: "wfactors G bs b"
```
```  1728     and cfs: "wfactors G cs (a \<otimes> b)"
```
```  1729     and carr: "a \<in> carrier G"  "b \<in> carrier G"
```
```  1730               "set as \<subseteq> carrier G"  "set bs \<subseteq> carrier G"  "set cs \<subseteq> carrier G"
```
```  1731   shows "fmset G cs = fmset G as + fmset G bs"
```
```  1732 proof -
```
```  1733   from assms have "wfactors G (as @ bs) (a \<otimes> b)"
```
```  1734     by (intro wfactors_mult)
```
```  1735   with carr cfs have "essentially_equal G cs (as@bs)"
```
```  1736     by (intro ee_wfactorsI[of "a\<otimes>b" "a\<otimes>b"]) simp_all
```
```  1737   with carr have "fmset G cs = fmset G (as@bs)"
```
```  1738     by (intro ee_fmset) simp_all
```
```  1739   also have "fmset G (as@bs) = fmset G as + fmset G bs"
```
```  1740     by (simp add: fmset_def)
```
```  1741   finally show "fmset G cs = fmset G as + fmset G bs" .
```
```  1742 qed
```
```  1743
```
```  1744 lemma (in factorial_monoid) mult_factors_fmset:
```
```  1745   assumes afs: "factors G as a"
```
```  1746     and bfs: "factors G bs b"
```
```  1747     and cfs: "factors G cs (a \<otimes> b)"
```
```  1748     and "set as \<subseteq> carrier G"  "set bs \<subseteq> carrier G"  "set cs \<subseteq> carrier G"
```
```  1749   shows "fmset G cs = fmset G as + fmset G bs"
```
```  1750   using assms by (blast intro: factors_wfactors mult_wfactors_fmset)
```
```  1751
```
```  1752 lemma (in comm_monoid_cancel) fmset_wfactors_mult:
```
```  1753   assumes mset: "fmset G cs = fmset G as + fmset G bs"
```
```  1754     and carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
```
```  1755       "set as \<subseteq> carrier G"  "set bs \<subseteq> carrier G"  "set cs \<subseteq> carrier G"
```
```  1756     and fs: "wfactors G as a"  "wfactors G bs b"  "wfactors G cs c"
```
```  1757   shows "c \<sim> a \<otimes> b"
```
```  1758 proof -
```
```  1759   from carr fs have m: "wfactors G (as @ bs) (a \<otimes> b)"
```
```  1760     by (intro wfactors_mult)
```
```  1761
```
```  1762   from mset have "fmset G cs = fmset G (as@bs)"
```
```  1763     by (simp add: fmset_def)
```
```  1764   then have "essentially_equal G cs (as@bs)"
```
```  1765     by (rule fmset_ee) (simp_all add: carr)
```
```  1766   then show "c \<sim> a \<otimes> b"
```
```  1767     by (rule ee_wfactorsD[of "cs" "as@bs"]) (simp_all add: assms m)
```
```  1768 qed
```
```  1769
```
```  1770
```
```  1771 subsubsection \<open>Divisibility on multisets\<close>
```
```  1772
```
```  1773 lemma (in factorial_monoid) divides_fmsubset:
```
```  1774   assumes ab: "a divides b"
```
```  1775     and afs: "wfactors G as a"
```
```  1776     and bfs: "wfactors G bs b"
```
```  1777     and carr: "a \<in> carrier G"  "b \<in> carrier G"  "set as \<subseteq> carrier G"  "set bs \<subseteq> carrier G"
```
```  1778   shows "fmset G as \<subseteq># fmset G bs"
```
```  1779   using ab
```
```  1780 proof (elim dividesE)
```
```  1781   fix c
```
```  1782   assume ccarr: "c \<in> carrier G"
```
```  1783   from wfactors_exist [OF this]
```
```  1784   obtain cs where cscarr: "set cs \<subseteq> carrier G" and cfs: "wfactors G cs c"
```
```  1785     by blast
```
```  1786   note carr = carr ccarr cscarr
```
```  1787
```
```  1788   assume "b = a \<otimes> c"
```
```  1789   with afs bfs cfs carr have "fmset G bs = fmset G as + fmset G cs"
```
```  1790     by (intro mult_wfactors_fmset[OF afs cfs]) simp_all
```
```  1791   then show ?thesis by simp
```
```  1792 qed
```
```  1793
```
```  1794 lemma (in comm_monoid_cancel) fmsubset_divides:
```
```  1795   assumes msubset: "fmset G as \<subseteq># fmset G bs"
```
```  1796     and afs: "wfactors G as a"
```
```  1797     and bfs: "wfactors G bs b"
```
```  1798     and acarr: "a \<in> carrier G"
```
```  1799     and bcarr: "b \<in> carrier G"
```
```  1800     and ascarr: "set as \<subseteq> carrier G"
```
```  1801     and bscarr: "set bs \<subseteq> carrier G"
```
```  1802   shows "a divides b"
```
```  1803 proof -
```
```  1804   from afs have airr: "\<forall>a \<in> set as. irreducible G a" by (fast elim: wfactorsE)
```
```  1805   from bfs have birr: "\<forall>b \<in> set bs. irreducible G b" by (fast elim: wfactorsE)
```
```  1806
```
```  1807   have "\<exists>c cs. c \<in> carrier G \<and> set cs \<subseteq> carrier G \<and> wfactors G cs c \<and> fmset G cs = fmset G bs - fmset G as"
```
```  1808   proof (intro mset_wfactorsEx, simp)
```
```  1809     fix X
```
```  1810     assume "X \<in># fmset G bs - fmset G as"
```
```  1811     then have "X \<in># fmset G bs" by (rule in_diffD)
```
```  1812     then have "X \<in> set (map (assocs G) bs)" by (simp add: fmset_def)
```
```  1813     then have "\<exists>x. x \<in> set bs \<and> X = assocs G x" by (induct bs) auto
```
```  1814     then obtain x where xbs: "x \<in> set bs" and X: "X = assocs G x" by auto
```
```  1815     with bscarr have xcarr: "x \<in> carrier G" by fast
```
```  1816     from xbs birr have xirr: "irreducible G x" by simp
```
```  1817
```
```  1818     from xcarr and xirr and X show "\<exists>x. x \<in> carrier G \<and> irreducible G x \<and> X = assocs G x"
```
```  1819       by fast
```
```  1820   qed
```
```  1821   then obtain c cs
```
```  1822     where ccarr: "c \<in> carrier G"
```
```  1823       and cscarr: "set cs \<subseteq> carrier G"
```
```  1824       and csf: "wfactors G cs c"
```
```  1825       and csmset: "fmset G cs = fmset G bs - fmset G as" by auto
```
```  1826
```
```  1827   from csmset msubset
```
```  1828   have "fmset G bs = fmset G as + fmset G cs"
```
```  1829     by (simp add: multiset_eq_iff subseteq_mset_def)
```
```  1830   then have basc: "b \<sim> a \<otimes> c"
```
```  1831     by (rule fmset_wfactors_mult) fact+
```
```  1832   then show ?thesis
```
```  1833   proof (elim associatedE2)
```
```  1834     fix u
```
```  1835     assume "u \<in> Units G"  "b = a \<otimes> c \<otimes> u"
```
```  1836     with acarr ccarr show "a divides b"
```
```  1837       by (fast intro: dividesI[of "c \<otimes> u"] m_assoc)
```
```  1838   qed (simp_all add: acarr bcarr ccarr)
```
```  1839 qed
```
```  1840
```
```  1841 lemma (in factorial_monoid) divides_as_fmsubset:
```
```  1842   assumes "wfactors G as a"
```
```  1843     and "wfactors G bs b"
```
```  1844     and "a \<in> carrier G"
```
```  1845     and "b \<in> carrier G"
```
```  1846     and "set as \<subseteq> carrier G"
```
```  1847     and "set bs \<subseteq> carrier G"
```
```  1848   shows "a divides b = (fmset G as \<subseteq># fmset G bs)"
```
```  1849   using assms
```
```  1850   by (blast intro: divides_fmsubset fmsubset_divides)
```
```  1851
```
```  1852
```
```  1853 text \<open>Proper factors on multisets\<close>
```
```  1854
```
```  1855 lemma (in factorial_monoid) fmset_properfactor:
```
```  1856   assumes asubb: "fmset G as \<subseteq># fmset G bs"
```
```  1857     and anb: "fmset G as \<noteq> fmset G bs"
```
```  1858     and "wfactors G as a"
```
```  1859     and "wfactors G bs b"
```
```  1860     and "a \<in> carrier G"
```
```  1861     and "b \<in> carrier G"
```
```  1862     and "set as \<subseteq> carrier G"
```
```  1863     and "set bs \<subseteq> carrier G"
```
```  1864   shows "properfactor G a b"
```
```  1865 proof (rule properfactorI)
```
```  1866   show "a divides b"
```
```  1867     using assms asubb fmsubset_divides by blast
```
```  1868   show "\<not> b divides a"
```
```  1869     by (meson anb assms asubb factorial_monoid.divides_fmsubset factorial_monoid_axioms subset_mset.antisym)
```
```  1870 qed
```
```  1871
```
```  1872 lemma (in factorial_monoid) properfactor_fmset:
```
```  1873   assumes pf: "properfactor G a b"
```
```  1874     and "wfactors G as a"
```
```  1875     and "wfactors G bs b"
```
```  1876     and "a \<in> carrier G"
```
```  1877     and "b \<in> carrier G"
```
```  1878     and "set as \<subseteq> carrier G"
```
```  1879     and "set bs \<subseteq> carrier G"
```
```  1880   shows "fmset G as \<subseteq># fmset G bs \<and> fmset G as \<noteq> fmset G bs"
```
```  1881   using pf
```
```  1882   apply safe
```
```  1883    apply (meson assms divides_as_fmsubset monoid.properfactor_divides monoid_axioms)
```
```  1884   by (meson assms associated_def comm_monoid_cancel.ee_wfactorsD comm_monoid_cancel.fmset_ee factorial_monoid_axioms factorial_monoid_def properfactorE)
```
```  1885
```
```  1886 subsection \<open>Irreducible Elements are Prime\<close>
```
```  1887
```
```  1888 lemma (in factorial_monoid) irreducible_prime:
```
```  1889   assumes pirr: "irreducible G p" and pcarr: "p \<in> carrier G"
```
```  1890   shows "prime G p"
```
```  1891   using pirr
```
```  1892 proof (elim irreducibleE, intro primeI)
```
```  1893   fix a b
```
```  1894   assume acarr: "a \<in> carrier G"  and bcarr: "b \<in> carrier G"
```
```  1895     and pdvdab: "p divides (a \<otimes> b)"
```
```  1896     and pnunit: "p \<notin> Units G"
```
```  1897   assume irreduc[rule_format]:
```
```  1898     "\<forall>b. b \<in> carrier G \<and> properfactor G b p \<longrightarrow> b \<in> Units G"
```
```  1899   from pdvdab obtain c where ccarr: "c \<in> carrier G" and abpc: "a \<otimes> b = p \<otimes> c"
```
```  1900     by (rule dividesE)
```
```  1901   obtain as where ascarr: "set as \<subseteq> carrier G" and afs: "wfactors G as a"
```
```  1902     using wfactors_exist [OF acarr] by blast
```
```  1903   obtain bs where bscarr: "set bs \<subseteq> carrier G" and bfs: "wfactors G bs b"
```
```  1904     using wfactors_exist [OF bcarr] by blast
```
```  1905   obtain cs where cscarr: "set cs \<subseteq> carrier G" and cfs: "wfactors G cs c"
```
```  1906     using wfactors_exist [OF ccarr] by blast
```
```  1907   note carr[simp] = pcarr acarr bcarr ccarr ascarr bscarr cscarr
```
```  1908   from pirr cfs  abpc have "wfactors G (p # cs) (a \<otimes> b)"
```
```  1909     by (simp add: wfactors_mult_single)
```
```  1910   moreover have  "wfactors G (as @ bs) (a \<otimes> b)"
```
```  1911     by (rule wfactors_mult [OF afs bfs]) fact+
```
```  1912   ultimately have "essentially_equal G (p # cs) (as @ bs)"
```
```  1913     by (rule wfactors_unique) simp+
```
```  1914   then obtain ds where "p # cs <~~> ds" and dsassoc: "ds [\<sim>] (as @ bs)"
```
```  1915     by (fast elim: essentially_equalE)
```
```  1916   then have "p \<in> set ds"
```
```  1917     by (simp add: perm_set_eq[symmetric])
```
```  1918   with dsassoc obtain p' where "p' \<in> set (as@bs)" and pp': "p \<sim> p'"
```
```  1919     unfolding list_all2_conv_all_nth set_conv_nth by force
```
```  1920   then consider "p' \<in> set as" | "p' \<in> set bs" by auto
```
```  1921   then show "p divides a \<or> p divides b"
```
```  1922     using afs bfs divides_cong_l pp' wfactors_dividesI
```
```  1923     by (meson acarr ascarr bcarr bscarr pcarr)
```
```  1924 qed
```
```  1925
```
```  1926
```
```  1927 \<comment> \<open>A version using @{const factors}, more complicated\<close>
```
```  1928 lemma (in factorial_monoid) factors_irreducible_prime:
```
```  1929   assumes pirr: "irreducible G p" and pcarr: "p \<in> carrier G"
```
```  1930   shows "prime G p"
```
```  1931 proof (rule primeI)
```
```  1932   show "p \<notin> Units G"
```
```  1933     by (meson irreducibleE pirr)
```
```  1934   have irreduc: "\<And>b. \<lbrakk>b \<in> carrier G; properfactor G b p\<rbrakk> \<Longrightarrow> b \<in> Units G"
```
```  1935     using pirr by (auto simp: irreducible_def)
```
```  1936   show "p divides a \<or> p divides b"
```
```  1937     if acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G" and pdvdab: "p divides (a \<otimes> b)" for a b
```
```  1938   proof -
```
```  1939     from pdvdab obtain c where ccarr: "c \<in> carrier G" and abpc: "a \<otimes> b = p \<otimes> c"
```
```  1940       by (rule dividesE)
```
```  1941     note [simp] = pcarr acarr bcarr ccarr
```
```  1942
```
```  1943     show "p divides a \<or> p divides b"
```
```  1944     proof (cases "a \<in> Units G")
```
```  1945       case True
```
```  1946       then have "p divides b"
```
```  1947         by (metis acarr associatedI2' associated_def bcarr divides_trans m_comm pcarr pdvdab)
```
```  1948       then show ?thesis ..
```
```  1949     next
```
```  1950       case anunit: False
```
```  1951       show ?thesis
```
```  1952       proof (cases "b \<in> Units G")
```
```  1953         case True
```
```  1954         then have "p divides a"
```
```  1955           by (meson acarr bcarr divides_unit irreducible_prime pcarr pdvdab pirr prime_def)
```
```  1956         then show ?thesis ..
```
```  1957       next
```
```  1958         case bnunit: False
```
```  1959         then have cnunit: "c \<notin> Units G"
```
```  1960           by (metis abpc acarr anunit bcarr ccarr irreducible_prodE irreducible_prod_rI pcarr pirr)
```
```  1961         then have abnunit: "a \<otimes> b \<notin> Units G"
```
```  1962           using acarr anunit bcarr unit_factor by blast
```
```  1963         obtain as where ascarr: "set as \<subseteq> carrier G" and afac: "factors G as a"
```
```  1964           using factors_exist [OF acarr anunit] by blast
```
```  1965         obtain bs where bscarr: "set bs \<subseteq> carrier G" and bfac: "factors G bs b"
```
```  1966           using factors_exist [OF bcarr bnunit] by blast
```
```  1967         obtain cs where cscarr: "set cs \<subseteq> carrier G" and cfac: "factors G cs c"
```
```  1968           using factors_exist [OF ccarr cnunit] by auto
```
```  1969         note [simp] = ascarr bscarr cscarr
```
```  1970         from pirr cfac abpc have abfac': "factors G (p # cs) (a \<otimes> b)"
```
```  1971           by (simp add: factors_mult_single)
```
```  1972         from afac and bfac have "factors G (as @ bs) (a \<otimes> b)"
```
```  1973           by (rule factors_mult) fact+
```
```  1974         with abfac' have "essentially_equal G (p # cs) (as @ bs)"
```
```  1975           using abnunit factors_unique by auto
```
```  1976         then obtain ds where "p # cs <~~> ds" and dsassoc: "ds [\<sim>] (as @ bs)"
```
```  1977           by (fast elim: essentially_equalE)
```
```  1978         then have "p \<in> set ds"
```
```  1979           by (simp add: perm_set_eq[symmetric])
```
```  1980         with dsassoc obtain p' where "p' \<in> set (as@bs)" and pp': "p \<sim> p'"
```
```  1981           unfolding list_all2_conv_all_nth set_conv_nth by force
```
```  1982         then consider "p' \<in> set as" | "p' \<in> set bs" by auto
```
```  1983         then show "p divides a \<or> p divides b"
```
```  1984           by (meson afac bfac divides_cong_l factors_dividesI pp' ascarr bscarr pcarr)
```
```  1985       qed
```
```  1986     qed
```
```  1987   qed
```
```  1988 qed
```
```  1989
```
```  1990
```
```  1991 subsection \<open>Greatest Common Divisors and Lowest Common Multiples\<close>
```
```  1992
```
```  1993 subsubsection \<open>Definitions\<close>
```
```  1994
```
```  1995 definition isgcd :: "[('a,_) monoid_scheme, 'a, 'a, 'a] \<Rightarrow> bool"  ("(_ gcdof\<index> _ _)" [81,81,81] 80)
```
```  1996   where "x gcdof\<^bsub>G\<^esub> a b \<longleftrightarrow> x divides\<^bsub>G\<^esub> a \<and> x divides\<^bsub>G\<^esub> b \<and>
```
```  1997     (\<forall>y\<in>carrier G. (y divides\<^bsub>G\<^esub> a \<and> y divides\<^bsub>G\<^esub> b \<longrightarrow> y divides\<^bsub>G\<^esub> x))"
```
```  1998
```
```  1999 definition islcm :: "[_, 'a, 'a, 'a] \<Rightarrow> bool"  ("(_ lcmof\<index> _ _)" [81,81,81] 80)
```
```  2000   where "x lcmof\<^bsub>G\<^esub> a b \<longleftrightarrow> a divides\<^bsub>G\<^esub> x \<and> b divides\<^bsub>G\<^esub> x \<and>
```
```  2001     (\<forall>y\<in>carrier G. (a divides\<^bsub>G\<^esub> y \<and> b divides\<^bsub>G\<^esub> y \<longrightarrow> x divides\<^bsub>G\<^esub> y))"
```
```  2002
```
```  2003 definition somegcd :: "('a,_) monoid_scheme \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"
```
```  2004   where "somegcd G a b = (SOME x. x \<in> carrier G \<and> x gcdof\<^bsub>G\<^esub> a b)"
```
```  2005
```
```  2006 definition somelcm :: "('a,_) monoid_scheme \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"
```
```  2007   where "somelcm G a b = (SOME x. x \<in> carrier G \<and> x lcmof\<^bsub>G\<^esub> a b)"
```
```  2008
```
```  2009 definition "SomeGcd G A = inf (division_rel G) A"
```
```  2010
```
```  2011
```
```  2012 locale gcd_condition_monoid = comm_monoid_cancel +
```
```  2013   assumes gcdof_exists: "\<lbrakk>a \<in> carrier G; b \<in> carrier G\<rbrakk> \<Longrightarrow> \<exists>c. c \<in> carrier G \<and> c gcdof a b"
```
```  2014
```
```  2015 locale primeness_condition_monoid = comm_monoid_cancel +
```
```  2016   assumes irreducible_prime: "\<lbrakk>a \<in> carrier G; irreducible G a\<rbrakk> \<Longrightarrow> prime G a"
```
```  2017
```
```  2018 locale divisor_chain_condition_monoid = comm_monoid_cancel +
```
```  2019   assumes division_wellfounded: "wf {(x, y). x \<in> carrier G \<and> y \<in> carrier G \<and> properfactor G x y}"
```
```  2020
```
```  2021
```
```  2022 subsubsection \<open>Connections to \texttt{Lattice.thy}\<close>
```
```  2023
```
```  2024 lemma gcdof_greatestLower:
```
```  2025   fixes G (structure)
```
```  2026   assumes carr[simp]: "a \<in> carrier G"  "b \<in> carrier G"
```
```  2027   shows "(x \<in> carrier G \<and> x gcdof a b) = greatest (division_rel G) x (Lower (division_rel G) {a, b})"
```
```  2028   by (auto simp: isgcd_def greatest_def Lower_def elem_def)
```
```  2029
```
```  2030 lemma lcmof_leastUpper:
```
```  2031   fixes G (structure)
```
```  2032   assumes carr[simp]: "a \<in> carrier G"  "b \<in> carrier G"
```
```  2033   shows "(x \<in> carrier G \<and> x lcmof a b) = least (division_rel G) x (Upper (division_rel G) {a, b})"
```
```  2034   by (auto simp: islcm_def least_def Upper_def elem_def)
```
```  2035
```
```  2036 lemma somegcd_meet:
```
```  2037   fixes G (structure)
```
```  2038   assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
```
```  2039   shows "somegcd G a b = meet (division_rel G) a b"
```
```  2040   by (simp add: somegcd_def meet_def inf_def gcdof_greatestLower[OF carr])
```
```  2041
```
```  2042 lemma (in monoid) isgcd_divides_l:
```
```  2043   assumes "a divides b"
```
```  2044     and "a \<in> carrier G"  "b \<in> carrier G"
```
```  2045   shows "a gcdof a b"
```
```  2046   using assms unfolding isgcd_def by fast
```
```  2047
```
```  2048 lemma (in monoid) isgcd_divides_r:
```
```  2049   assumes "b divides a"
```
```  2050     and "a \<in> carrier G"  "b \<in> carrier G"
```
```  2051   shows "b gcdof a b"
```
```  2052   using assms unfolding isgcd_def by fast
```
```  2053
```
```  2054
```
```  2055 subsubsection \<open>Existence of gcd and lcm\<close>
```
```  2056
```
```  2057 lemma (in factorial_monoid) gcdof_exists:
```
```  2058   assumes acarr: "a \<in> carrier G"
```
```  2059     and bcarr: "b \<in> carrier G"
```
```  2060   shows "\<exists>c. c \<in> carrier G \<and> c gcdof a b"
```
```  2061 proof -
```
```  2062   from wfactors_exist [OF acarr]
```
```  2063   obtain as where ascarr: "set as \<subseteq> carrier G" and afs: "wfactors G as a"
```
```  2064     by blast
```
```  2065   from afs have airr: "\<forall>a \<in> set as. irreducible G a"
```
```  2066     by (fast elim: wfactorsE)
```
```  2067
```
```  2068   from wfactors_exist [OF bcarr]
```
```  2069   obtain bs where bscarr: "set bs \<subseteq> carrier G" and bfs: "wfactors G bs b"
```
```  2070     by blast
```
```  2071   from bfs have birr: "\<forall>b \<in> set bs. irreducible G b"
```
```  2072     by (fast elim: wfactorsE)
```
```  2073
```
```  2074   have "\<exists>c cs. c \<in> carrier G \<and> set cs \<subseteq> carrier G \<and> wfactors G cs c \<and>
```
```  2075     fmset G cs = fmset G as \<inter># fmset G bs"
```
```  2076   proof (intro mset_wfactorsEx)
```
```  2077     fix X
```
```  2078     assume "X \<in># fmset G as \<inter># fmset G bs"
```
```  2079     then have "X \<in># fmset G as" by simp
```
```  2080     then have "X \<in> set (map (assocs G) as)"
```
```  2081       by (simp add: fmset_def)
```
```  2082     then have "\<exists>x. X = assocs G x \<and> x \<in> set as"
```
```  2083       by (induct as) auto
```
```  2084     then obtain x where X: "X = assocs G x" and xas: "x \<in> set as"
```
```  2085       by blast
```
```  2086     with ascarr have xcarr: "x \<in> carrier G"
```
```  2087       by blast
```
```  2088     from xas airr have xirr: "irreducible G x"
```
```  2089       by simp
```
```  2090     from xcarr and xirr and X show "\<exists>x. (x \<in> carrier G \<and> irreducible G x) \<and> X = assocs G x"
```
```  2091       by blast
```
```  2092   qed
```
```  2093   then obtain c cs
```
```  2094     where ccarr: "c \<in> carrier G"
```
```  2095       and cscarr: "set cs \<subseteq> carrier G"
```
```  2096       and csirr: "wfactors G cs c"
```
```  2097       and csmset: "fmset G cs = fmset G as \<inter># fmset G bs"
```
```  2098     by auto
```
```  2099
```
```  2100   have "c gcdof a b"
```
```  2101   proof (simp add: isgcd_def, safe)
```
```  2102     from csmset
```
```  2103     have "fmset G cs \<subseteq># fmset G as"
```
```  2104       by (simp add: multiset_inter_def subset_mset_def)
```
```  2105     then show "c divides a" by (rule fmsubset_divides) fact+
```
```  2106   next
```
```  2107     from csmset have "fmset G cs \<subseteq># fmset G bs"
```
```  2108       by (simp add: multiset_inter_def subseteq_mset_def, force)
```
```  2109     then show "c divides b"
```
```  2110       by (rule fmsubset_divides) fact+
```
```  2111   next
```
```  2112     fix y
```
```  2113     assume "y \<in> carrier G"
```
```  2114     from wfactors_exist [OF this]
```
```  2115     obtain ys where yscarr: "set ys \<subseteq> carrier G" and yfs: "wfactors G ys y"
```
```  2116       by blast
```
```  2117
```
```  2118     assume "y divides a"
```
```  2119     then have ya: "fmset G ys \<subseteq># fmset G as"
```
```  2120       by (rule divides_fmsubset) fact+
```
```  2121
```
```  2122     assume "y divides b"
```
```  2123     then have yb: "fmset G ys \<subseteq># fmset G bs"
```
```  2124       by (rule divides_fmsubset) fact+
```
```  2125
```
```  2126     from ya yb csmset have "fmset G ys \<subseteq># fmset G cs"
```
```  2127       by (simp add: subset_mset_def)
```
```  2128     then show "y divides c"
```
```  2129       by (rule fmsubset_divides) fact+
```
```  2130   qed
```
```  2131   with ccarr show "\<exists>c. c \<in> carrier G \<and> c gcdof a b"
```
```  2132     by fast
```
```  2133 qed
```
```  2134
```
```  2135 lemma (in factorial_monoid) lcmof_exists:
```
```  2136   assumes acarr: "a \<in> carrier G"
```
```  2137     and bcarr: "b \<in> carrier G"
```
```  2138   shows "\<exists>c. c \<in> carrier G \<and> c lcmof a b"
```
```  2139 proof -
```
```  2140   from wfactors_exist [OF acarr]
```
```  2141   obtain as where ascarr: "set as \<subseteq> carrier G" and afs: "wfactors G as a"
```
```  2142     by blast
```
```  2143   from afs have airr: "\<forall>a \<in> set as. irreducible G a"
```
```  2144     by (fast elim: wfactorsE)
```
```  2145
```
```  2146   from wfactors_exist [OF bcarr]
```
```  2147   obtain bs where bscarr: "set bs \<subseteq> carrier G" and bfs: "wfactors G bs b"
```
```  2148     by blast
```
```  2149   from bfs have birr: "\<forall>b \<in> set bs. irreducible G b"
```
```  2150     by (fast elim: wfactorsE)
```
```  2151
```
```  2152   have "\<exists>c cs. c \<in> carrier G \<and> set cs \<subseteq> carrier G \<and> wfactors G cs c \<and>
```
```  2153     fmset G cs = (fmset G as - fmset G bs) + fmset G bs"
```
```  2154   proof (intro mset_wfactorsEx)
```
```  2155     fix X
```
```  2156     assume "X \<in># (fmset G as - fmset G bs) + fmset G bs"
```
```  2157     then have "X \<in># fmset G as \<or> X \<in># fmset G bs"
```
```  2158       by (auto dest: in_diffD)
```
```  2159     then consider "X \<in> set_mset (fmset G as)" | "X \<in> set_mset (fmset G bs)"
```
```  2160       by fast
```
```  2161     then show "\<exists>x. (x \<in> carrier G \<and> irreducible G x) \<and> X = assocs G x"
```
```  2162     proof cases
```
```  2163       case 1
```
```  2164       then have "X \<in> set (map (assocs G) as)" by (simp add: fmset_def)
```
```  2165       then have "\<exists>x. x \<in> set as \<and> X = assocs G x" by (induct as) auto
```
```  2166       then obtain x where xas: "x \<in> set as" and X: "X = assocs G x" by auto
```
```  2167       with ascarr have xcarr: "x \<in> carrier G" by fast
```
```  2168       from xas airr have xirr: "irreducible G x" by simp
```
```  2169       from xcarr and xirr and X show ?thesis by fast
```
```  2170     next
```
```  2171       case 2
```
```  2172       then have "X \<in> set (map (assocs G) bs)" by (simp add: fmset_def)
```
```  2173       then have "\<exists>x. x \<in> set bs \<and> X = assocs G x" by (induct as) auto
```
```  2174       then obtain x where xbs: "x \<in> set bs" and X: "X = assocs G x" by auto
```
```  2175       with bscarr have xcarr: "x \<in> carrier G" by fast
```
```  2176       from xbs birr have xirr: "irreducible G x" by simp
```
```  2177       from xcarr and xirr and X show ?thesis by fast
```
```  2178     qed
```
```  2179   qed
```
```  2180   then obtain c cs
```
```  2181     where ccarr: "c \<in> carrier G"
```
```  2182       and cscarr: "set cs \<subseteq> carrier G"
```
```  2183       and csirr: "wfactors G cs c"
```
```  2184       and csmset: "fmset G cs = fmset G as - fmset G bs + fmset G bs"
```
```  2185     by auto
```
```  2186
```
```  2187   have "c lcmof a b"
```
```  2188   proof (simp add: islcm_def, safe)
```
```  2189     from csmset have "fmset G as \<subseteq># fmset G cs"
```
```  2190       by (simp add: subseteq_mset_def, force)
```
```  2191     then show "a divides c"
```
```  2192       by (rule fmsubset_divides) fact+
```
```  2193   next
```
```  2194     from csmset have "fmset G bs \<subseteq># fmset G cs"
```
```  2195       by (simp add: subset_mset_def)
```
```  2196     then show "b divides c"
```
```  2197       by (rule fmsubset_divides) fact+
```
```  2198   next
```
```  2199     fix y
```
```  2200     assume "y \<in> carrier G"
```
```  2201     from wfactors_exist [OF this]
```
```  2202     obtain ys where yscarr: "set ys \<subseteq> carrier G" and yfs: "wfactors G ys y"
```
```  2203       by blast
```
```  2204
```
```  2205     assume "a divides y"
```
```  2206     then have ya: "fmset G as \<subseteq># fmset G ys"
```
```  2207       by (rule divides_fmsubset) fact+
```
```  2208
```
```  2209     assume "b divides y"
```
```  2210     then have yb: "fmset G bs \<subseteq># fmset G ys"
```
```  2211       by (rule divides_fmsubset) fact+
```
```  2212
```
```  2213     from ya yb csmset have "fmset G cs \<subseteq># fmset G ys"
```
```  2214       using subset_eq_diff_conv subset_mset.le_diff_conv2 by fastforce
```
```  2215     then show "c divides y"
```
```  2216       by (rule fmsubset_divides) fact+
```
```  2217   qed
```
```  2218   with ccarr show "\<exists>c. c \<in> carrier G \<and> c lcmof a b"
```
```  2219     by fast
```
```  2220 qed
```
```  2221
```
```  2222
```
```  2223 subsection \<open>Conditions for Factoriality\<close>
```
```  2224
```
```  2225 subsubsection \<open>Gcd condition\<close>
```
```  2226
```
```  2227 lemma (in gcd_condition_monoid) division_weak_lower_semilattice [simp]:
```
```  2228   "weak_lower_semilattice (division_rel G)"
```
```  2229 proof -
```
```  2230   interpret weak_partial_order "division_rel G" ..
```
```  2231   show ?thesis
```
```  2232   proof (unfold_locales, simp_all)
```
```  2233     fix x y
```
```  2234     assume carr: "x \<in> carrier G"  "y \<in> carrier G"
```
```  2235     from gcdof_exists [OF this] obtain z where zcarr: "z \<in> carrier G" and isgcd: "z gcdof x y"
```
```  2236       by blast
```
```  2237     with carr have "greatest (division_rel G) z (Lower (division_rel G) {x, y})"
```
```  2238       by (subst gcdof_greatestLower[symmetric], simp+)
```
```  2239     then show "\<exists>z. greatest (division_rel G) z (Lower (division_rel G) {x, y})"
```
```  2240       by fast
```
```  2241   qed
```
```  2242 qed
```
```  2243
```
```  2244 lemma (in gcd_condition_monoid) gcdof_cong_l:
```
```  2245   assumes a'a: "a' \<sim> a"
```
```  2246     and agcd: "a gcdof b c"
```
```  2247     and a'carr: "a' \<in> carrier G" and carr': "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
```
```  2248   shows "a' gcdof b c"
```
```  2249 proof -
```
```  2250   note carr = a'carr carr'
```
```  2251   interpret weak_lower_semilattice "division_rel G" by simp
```
```  2252   have "is_glb (division_rel G) a' {b, c}"
```
```  2253     by (subst greatest_Lower_cong_l[of _ a]) (simp_all add: a'a carr gcdof_greatestLower[symmetric] agcd)
```
```  2254   then have "a' \<in> carrier G \<and> a' gcdof b c"
```
```  2255     by (simp add: gcdof_greatestLower carr')
```
```  2256   then show ?thesis ..
```
```  2257 qed
```
```  2258
```
```  2259 lemma (in gcd_condition_monoid) gcd_closed [simp]:
```
```  2260   assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
```
```  2261   shows "somegcd G a b \<in> carrier G"
```
```  2262 proof -
```
```  2263   interpret weak_lower_semilattice "division_rel G" by simp
```
```  2264   show ?thesis
```
```  2265     apply (simp add: somegcd_meet[OF carr])
```
```  2266     apply (rule meet_closed[simplified], fact+)
```
```  2267     done
```
```  2268 qed
```
```  2269
```
```  2270 lemma (in gcd_condition_monoid) gcd_isgcd:
```
```  2271   assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
```
```  2272   shows "(somegcd G a b) gcdof a b"
```
```  2273 proof -
```
```  2274   interpret weak_lower_semilattice "division_rel G"
```
```  2275     by simp
```
```  2276   from carr have "somegcd G a b \<in> carrier G \<and> (somegcd G a b) gcdof a b"
```
```  2277     by (simp add: gcdof_greatestLower inf_of_two_greatest meet_def somegcd_meet)
```
```  2278   then show "(somegcd G a b) gcdof a b"
```
```  2279     by simp
```
```  2280 qed
```
```  2281
```
```  2282 lemma (in gcd_condition_monoid) gcd_exists:
```
```  2283   assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
```
```  2284   shows "\<exists>x\<in>carrier G. x = somegcd G a b"
```
```  2285 proof -
```
```  2286   interpret weak_lower_semilattice "division_rel G"
```
```  2287     by simp
```
```  2288   show ?thesis
```
```  2289     by (metis carr(1) carr(2) gcd_closed)
```
```  2290 qed
```
```  2291
```
```  2292 lemma (in gcd_condition_monoid) gcd_divides_l:
```
```  2293   assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
```
```  2294   shows "(somegcd G a b) divides a"
```
```  2295 proof -
```
```  2296   interpret weak_lower_semilattice "division_rel G"
```
```  2297     by simp
```
```  2298   show ?thesis
```
```  2299     by (metis carr(1) carr(2) gcd_isgcd isgcd_def)
```
```  2300 qed
```
```  2301
```
```  2302 lemma (in gcd_condition_monoid) gcd_divides_r:
```
```  2303   assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
```
```  2304   shows "(somegcd G a b) divides b"
```
```  2305 proof -
```
```  2306   interpret weak_lower_semilattice "division_rel G"
```
```  2307     by simp
```
```  2308   show ?thesis
```
```  2309     by (metis carr gcd_isgcd isgcd_def)
```
```  2310 qed
```
```  2311
```
```  2312 lemma (in gcd_condition_monoid) gcd_divides:
```
```  2313   assumes sub: "z divides x"  "z divides y"
```
```  2314     and L: "x \<in> carrier G"  "y \<in> carrier G"  "z \<in> carrier G"
```
```  2315   shows "z divides (somegcd G x y)"
```
```  2316 proof -
```
```  2317   interpret weak_lower_semilattice "division_rel G"
```
```  2318     by simp
```
```  2319   show ?thesis
```
```  2320     by (metis gcd_isgcd isgcd_def assms)
```
```  2321 qed
```
```  2322
```
```  2323 lemma (in gcd_condition_monoid) gcd_cong_l:
```
```  2324   assumes xx': "x \<sim> x'"
```
```  2325     and carr: "x \<in> carrier G"  "x' \<in> carrier G"  "y \<in> carrier G"
```
```  2326   shows "somegcd G x y \<sim> somegcd G x' y"
```
```  2327 proof -
```
```  2328   interpret weak_lower_semilattice "division_rel G"
```
```  2329     by simp
```
```  2330   show ?thesis
```
```  2331     apply (simp add: somegcd_meet carr)
```
```  2332     apply (rule meet_cong_l[simplified], fact+)
```
```  2333     done
```
```  2334 qed
```
```  2335
```
```  2336 lemma (in gcd_condition_monoid) gcd_cong_r:
```
```  2337   assumes carr: "x \<in> carrier G"  "y \<in> carrier G"  "y' \<in> carrier G"
```
```  2338     and yy': "y \<sim> y'"
```
```  2339   shows "somegcd G x y \<sim> somegcd G x y'"
```
```  2340 proof -
```
```  2341   interpret weak_lower_semilattice "division_rel G" by simp
```
```  2342   show ?thesis
```
```  2343     apply (simp add: somegcd_meet carr)
```
```  2344     apply (rule meet_cong_r[simplified], fact+)
```
```  2345     done
```
```  2346 qed
```
```  2347
```
```  2348 (*
```
```  2349 lemma (in gcd_condition_monoid) asc_cong_gcd_l [intro]:
```
```  2350   assumes carr: "b \<in> carrier G"
```
```  2351   shows "asc_cong (\<lambda>a. somegcd G a b)"
```
```  2352 using carr
```
```  2353 unfolding CONG_def
```
```  2354 by clarsimp (blast intro: gcd_cong_l)
```
```  2355
```
```  2356 lemma (in gcd_condition_monoid) asc_cong_gcd_r [intro]:
```
```  2357   assumes carr: "a \<in> carrier G"
```
```  2358   shows "asc_cong (\<lambda>b. somegcd G a b)"
```
```  2359 using carr
```
```  2360 unfolding CONG_def
```
```  2361 by clarsimp (blast intro: gcd_cong_r)
```
```  2362
```
```  2363 lemmas (in gcd_condition_monoid) asc_cong_gcd_split [simp] =
```
```  2364     assoc_split[OF _ asc_cong_gcd_l] assoc_split[OF _ asc_cong_gcd_r]
```
```  2365 *)
```
```  2366
```
```  2367 lemma (in gcd_condition_monoid) gcdI:
```
```  2368   assumes dvd: "a divides b"  "a divides c"
```
```  2369     and others: "\<And>y. \<lbrakk>y\<in>carrier G; y divides b; y divides c\<rbrakk> \<Longrightarrow> y divides a"
```
```  2370     and acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G" and ccarr: "c \<in> carrier G"
```
```  2371   shows "a \<sim> somegcd G b c"
```
```  2372 proof -
```
```  2373   have "\<exists>a. a \<in> carrier G \<and> a gcdof b c"
```
```  2374     by (simp add: bcarr ccarr gcdof_exists)
```
```  2375   moreover have "\<And>x. x \<in> carrier G \<and> x gcdof b c \<Longrightarrow> a \<sim> x"
```
```  2376     by (simp add: acarr associated_def dvd isgcd_def others)
```
```  2377   ultimately show ?thesis
```
```  2378     unfolding somegcd_def by (blast intro: someI2_ex)
```
```  2379 qed
```
```  2380
```
```  2381 lemma (in gcd_condition_monoid) gcdI2:
```
```  2382   assumes "a gcdof b c" and "a \<in> carrier G" and "b \<in> carrier G" and "c \<in> carrier G"
```
```  2383   shows "a \<sim> somegcd G b c"
```
```  2384   using assms unfolding isgcd_def
```
```  2385   by (simp add: gcdI)
```
```  2386
```
```  2387 lemma (in gcd_condition_monoid) SomeGcd_ex:
```
```  2388   assumes "finite A"  "A \<subseteq> carrier G"  "A \<noteq> {}"
```
```  2389   shows "\<exists>x\<in> carrier G. x = SomeGcd G A"
```
```  2390 proof -
```
```  2391   interpret weak_lower_semilattice "division_rel G"
```
```  2392     by simp
```
```  2393   show ?thesis
```
```  2394     apply (simp add: SomeGcd_def)
```
```  2395     apply (rule finite_inf_closed[simplified], fact+)
```
```  2396     done
```
```  2397 qed
```
```  2398
```
```  2399 lemma (in gcd_condition_monoid) gcd_assoc:
```
```  2400   assumes carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
```
```  2401   shows "somegcd G (somegcd G a b) c \<sim> somegcd G a (somegcd G b c)"
```
```  2402 proof -
```
```  2403   interpret weak_lower_semilattice "division_rel G"
```
```  2404     by simp
```
```  2405   show ?thesis
```
```  2406     unfolding associated_def
```
```  2407     by (meson carr divides_trans gcd_divides gcd_divides_l gcd_divides_r gcd_exists)
```
```  2408 qed
```
```  2409
```
```  2410 lemma (in gcd_condition_monoid) gcd_mult:
```
```  2411   assumes acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G" and ccarr: "c \<in> carrier G"
```
```  2412   shows "c \<otimes> somegcd G a b \<sim> somegcd G (c \<otimes> a) (c \<otimes> b)"
```
```  2413 proof - (* following Jacobson, Basic Algebra, p.140 *)
```
```  2414   let ?d = "somegcd G a b"
```
```  2415   let ?e = "somegcd G (c \<otimes> a) (c \<otimes> b)"
```
```  2416   note carr[simp] = acarr bcarr ccarr
```
```  2417   have dcarr: "?d \<in> carrier G" by simp
```
```  2418   have ecarr: "?e \<in> carrier G" by simp
```
```  2419   note carr = carr dcarr ecarr
```
```  2420
```
```  2421   have "?d divides a" by (simp add: gcd_divides_l)
```
```  2422   then have cd'ca: "c \<otimes> ?d divides (c \<otimes> a)" by (simp add: divides_mult_lI)
```
```  2423
```
```  2424   have "?d divides b" by (simp add: gcd_divides_r)
```
```  2425   then have cd'cb: "c \<otimes> ?d divides (c \<otimes> b)" by (simp add: divides_mult_lI)
```
```  2426
```
```  2427   from cd'ca cd'cb have cd'e: "c \<otimes> ?d divides ?e"
```
```  2428     by (rule gcd_divides) simp_all
```
```  2429   then obtain u where ucarr[simp]: "u \<in> carrier G" and e_cdu: "?e = c \<otimes> ?d \<otimes> u"
```
```  2430     by blast
```
```  2431
```
```  2432   note carr = carr ucarr
```
```  2433
```
```  2434   have "?e divides c \<otimes> a" by (rule gcd_divides_l) simp_all
```
```  2435   then obtain x where xcarr: "x \<in> carrier G" and ca_ex: "c \<otimes> a = ?e \<otimes> x"
```
```  2436     by blast
```
```  2437   with e_cdu have ca_cdux: "c \<otimes> a = c \<otimes> ?d \<otimes> u \<otimes> x"
```
```  2438     by simp
```
```  2439
```
```  2440   from ca_cdux xcarr have "c \<otimes> a = c \<otimes> (?d \<otimes> u \<otimes> x)"
```
```  2441     by (simp add: m_assoc)
```
```  2442   then have "a = ?d \<otimes> u \<otimes> x"
```
```  2443     by (rule l_cancel[of c a]) (simp add: xcarr)+
```
```  2444   then have du'a: "?d \<otimes> u divides a"
```
```  2445     by (rule dividesI[OF xcarr])
```
```  2446
```
```  2447   have "?e divides c \<otimes> b" by (intro gcd_divides_r) simp_all
```
```  2448   then obtain x where xcarr: "x \<in> carrier G" and cb_ex: "c \<otimes> b = ?e \<otimes> x"
```
```  2449     by blast
```
```  2450   with e_cdu have cb_cdux: "c \<otimes> b = c \<otimes> ?d \<otimes> u \<otimes> x"
```
```  2451     by simp
```
```  2452
```
```  2453   from cb_cdux xcarr have "c \<otimes> b = c \<otimes> (?d \<otimes> u \<otimes> x)"
```
```  2454     by (simp add: m_assoc)
```
```  2455   with xcarr have "b = ?d \<otimes> u \<otimes> x"
```
```  2456     by (intro l_cancel[of c b]) simp_all
```
```  2457   then have du'b: "?d \<otimes> u divides b"
```
```  2458     by (intro dividesI[OF xcarr])
```
```  2459
```
```  2460   from du'a du'b carr have du'd: "?d \<otimes> u divides ?d"
```
```  2461     by (intro gcd_divides) simp_all
```
```  2462   then have uunit: "u \<in> Units G"
```
```  2463   proof (elim dividesE)
```
```  2464     fix v
```
```  2465     assume vcarr[simp]: "v \<in> carrier G"
```
```  2466     assume d: "?d = ?d \<otimes> u \<otimes> v"
```
```  2467     have "?d \<otimes> \<one> = ?d \<otimes> u \<otimes> v" by simp fact
```
```  2468     also have "?d \<otimes> u \<otimes> v = ?d \<otimes> (u \<otimes> v)" by (simp add: m_assoc)
```
```  2469     finally have "?d \<otimes> \<one> = ?d \<otimes> (u \<otimes> v)" .
```
```  2470     then have i2: "\<one> = u \<otimes> v" by (rule l_cancel) simp_all
```
```  2471     then have i1: "\<one> = v \<otimes> u" by (simp add: m_comm)
```
```  2472     from vcarr i1[symmetric] i2[symmetric] show "u \<in> Units G"
```
```  2473       by (auto simp: Units_def)
```
```  2474   qed
```
```  2475
```
```  2476   from e_cdu uunit have "somegcd G (c \<otimes> a) (c \<otimes> b) \<sim> c \<otimes> somegcd G a b"
```
```  2477     by (intro associatedI2[of u]) simp_all
```
```  2478   from this[symmetric] show "c \<otimes> somegcd G a b \<sim> somegcd G (c \<otimes> a) (c \<otimes> b)"
```
```  2479     by simp
```
```  2480 qed
```
```  2481
```
```  2482 lemma (in monoid) assoc_subst:
```
```  2483   assumes ab: "a \<sim> b"
```
```  2484     and cP: "\<forall>a b. a \<in> carrier G \<and> b \<in> carrier G \<and> a \<sim> b
```
```  2485       \<longrightarrow> f a \<in> carrier G \<and> f b \<in> carrier G \<and> f a \<sim> f b"
```
```  2486     and carr: "a \<in> carrier G"  "b \<in> carrier G"
```
```  2487   shows "f a \<sim> f b"
```
```  2488   using assms by auto
```
```  2489
```
```  2490 lemma (in gcd_condition_monoid) relprime_mult:
```
```  2491   assumes abrelprime: "somegcd G a b \<sim> \<one>"
```
```  2492     and acrelprime: "somegcd G a c \<sim> \<one>"
```
```  2493     and carr[simp]: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
```
```  2494   shows "somegcd G a (b \<otimes> c) \<sim> \<one>"
```
```  2495 proof -
```
```  2496   have "c = c \<otimes> \<one>" by simp
```
```  2497   also from abrelprime[symmetric]
```
```  2498   have "\<dots> \<sim> c \<otimes> somegcd G a b"
```
```  2499     by (rule assoc_subst) (simp add: mult_cong_r)+
```
```  2500   also have "\<dots> \<sim> somegcd G (c \<otimes> a) (c \<otimes> b)"
```
```  2501     by (rule gcd_mult) fact+
```
```  2502   finally have c: "c \<sim> somegcd G (c \<otimes> a) (c \<otimes> b)"
```
```  2503     by simp
```
```  2504
```
```  2505   from carr have a: "a \<sim> somegcd G a (c \<otimes> a)"
```
```  2506     by (fast intro: gcdI divides_prod_l)
```
```  2507
```
```  2508   have "somegcd G a (b \<otimes> c) \<sim> somegcd G a (c \<otimes> b)"
```
```  2509     by (simp add: m_comm)
```
```  2510   also from a have "\<dots> \<sim> somegcd G (somegcd G a (c \<otimes> a)) (c \<otimes> b)"
```
```  2511     by (rule assoc_subst) (simp add: gcd_cong_l)+
```
```  2512   also from gcd_assoc have "\<dots> \<sim> somegcd G a (somegcd G (c \<otimes> a) (c \<otimes> b))"
```
```  2513     by (rule assoc_subst) simp+
```
```  2514   also from c[symmetric] have "\<dots> \<sim> somegcd G a c"
```
```  2515     by (rule assoc_subst) (simp add: gcd_cong_r)+
```
```  2516   also note acrelprime
```
```  2517   finally show "somegcd G a (b \<otimes> c) \<sim> \<one>"
```
```  2518     by simp
```
```  2519 qed
```
```  2520
```
```  2521 lemma (in gcd_condition_monoid) primeness_condition: "primeness_condition_monoid G"
```
```  2522 proof -
```
```  2523   have *: "p divides a \<or> p divides b"
```
```  2524     if pcarr[simp]: "p \<in> carrier G" and acarr[simp]: "a \<in> carrier G" and bcarr[simp]: "b \<in> carrier G"
```
```  2525       and pirr: "irreducible G p" and pdvdab: "p divides a \<otimes> b"
```
```  2526     for p a b
```
```  2527   proof -
```
```  2528     from pirr have pnunit: "p \<notin> Units G"
```
```  2529       and r: "\<And>b. \<lbrakk>b \<in> carrier G; properfactor G b p\<rbrakk> \<Longrightarrow> b \<in> Units G"
```
```  2530       by (fast elim: irreducibleE)+
```
```  2531     show "p divides a \<or> p divides b"
```
```  2532     proof (rule ccontr, clarsimp)
```
```  2533       assume npdvda: "\<not> p divides a" and npdvdb: "\<not> p divides b"
```
```  2534       have "\<one> \<sim> somegcd G p a"
```
```  2535       proof (intro gcdI unit_divides)
```
```  2536         show "\<And>y. \<lbrakk>y \<in> carrier G; y divides p; y divides a\<rbrakk> \<Longrightarrow> y \<in> Units G"
```
```  2537           by (meson divides_trans npdvda pcarr properfactorI r)
```
```  2538       qed auto
```
```  2539       with pcarr acarr have pa: "somegcd G p a \<sim> \<one>"
```
```  2540         by (fast intro: associated_sym[of "\<one>"] gcd_closed)
```
```  2541       have "\<one> \<sim> somegcd G p b"
```
```  2542       proof (intro gcdI unit_divides)
```
```  2543         show "\<And>y. \<lbrakk>y \<in> carrier G; y divides p; y divides b\<rbrakk> \<Longrightarrow> y \<in> Units G"
```
```  2544           by (meson divides_trans npdvdb pcarr properfactorI r)
```
```  2545       qed auto
```
```  2546       with pcarr bcarr have pb: "somegcd G p b \<sim> \<one>"
```
```  2547         by (fast intro: associated_sym[of "\<one>"] gcd_closed)
```
```  2548       have "p \<sim> somegcd G p (a \<otimes> b)"
```
```  2549         using pdvdab by (simp add: gcdI2 isgcd_divides_l)
```
```  2550       also from pa pb pcarr acarr bcarr have "somegcd G p (a \<otimes> b) \<sim> \<one>"
```
```  2551         by (rule relprime_mult)
```
```  2552       finally have "p \<sim> \<one>"
```
```  2553         by simp
```
```  2554       with pcarr have "p \<in> Units G"
```
```  2555         by (fast intro: assoc_unit_l)
```
```  2556       with pnunit show False ..
```
```  2557     qed
```
```  2558   qed
```
```  2559   show ?thesis
```
```  2560     by unfold_locales (metis * primeI irreducibleE)
```
```  2561 qed
```
```  2562
```
```  2563
```
```  2564 sublocale gcd_condition_monoid \<subseteq> primeness_condition_monoid
```
```  2565   by (rule primeness_condition)
```
```  2566
```
```  2567
```
```  2568 subsubsection \<open>Divisor chain condition\<close>
```
```  2569
```
```  2570 lemma (in divisor_chain_condition_monoid) wfactors_exist:
```
```  2571   assumes acarr: "a \<in> carrier G"
```
```  2572   shows "\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as a"
```
```  2573 proof -
```
```  2574   have r: "a \<in> carrier G \<Longrightarrow> (\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as a)"
```
```  2575     using division_wellfounded
```
```  2576   proof (induction rule: wf_induct_rule)
```
```  2577     case (less x)
```
```  2578     then have xcarr: "x \<in> carrier G"
```
```  2579       by auto
```
```  2580     show ?case
```
```  2581     proof (cases "x \<in> Units G")
```
```  2582       case True
```
```  2583       then show ?thesis
```
```  2584         by (metis bot.extremum list.set(1) unit_wfactors)
```
```  2585     next
```
```  2586       case xnunit: False
```
```  2587       show ?thesis
```
```  2588       proof (cases "irreducible G x")
```
```  2589         case True
```
```  2590         then show ?thesis
```
```  2591           by (rule_tac x="[x]" in exI) (simp add: wfactors_def xcarr)
```
```  2592       next
```
```  2593         case False
```
```  2594         then obtain y where ycarr: "y \<in> carrier G" and ynunit: "y \<notin> Units G" and pfyx: "properfactor G y x"
```
```  2595           by (meson irreducible_def xnunit)
```
```  2596         obtain ys where yscarr: "set ys \<subseteq> carrier G" and yfs: "wfactors G ys y"
```
```  2597           using less ycarr pfyx by blast
```
```  2598         then obtain z where zcarr: "z \<in> carrier G" and x: "x = y \<otimes> z"
```
```  2599           by (meson dividesE pfyx properfactorE2)
```
```  2600         from zcarr ycarr have "properfactor G z x"
```
```  2601           using m_comm properfactorI3 x ynunit by blast
```
```  2602         with less zcarr obtain zs where zscarr: "set zs \<subseteq> carrier G" and zfs: "wfactors G zs z"
```
```  2603           by blast
```
```  2604         from yscarr zscarr have xscarr: "set (ys@zs) \<subseteq> carrier G"
```
```  2605           by simp
```
```  2606         have "wfactors G (ys@zs) (y\<otimes>z)"
```
```  2607           using xscarr ycarr yfs zcarr zfs by auto
```
```  2608         then have "wfactors G (ys@zs) x"
```
```  2609           by (simp add: x)
```
```  2610         with xscarr show "\<exists>xs. set xs \<subseteq> carrier G \<and> wfactors G xs x"
```
```  2611           by fast
```
```  2612       qed
```
```  2613     qed
```
```  2614   qed
```
```  2615   from acarr show ?thesis by (rule r)
```
```  2616 qed
```
```  2617
```
```  2618
```
```  2619 subsubsection \<open>Primeness condition\<close>
```
```  2620
```
```  2621 lemma (in comm_monoid_cancel) multlist_prime_pos:
```
```  2622   assumes aprime: "prime G a" and carr: "a \<in> carrier G"
```
```  2623      and as: "set as \<subseteq> carrier G" "a divides (foldr (\<otimes>) as \<one>)"
```
```  2624    shows "\<exists>i<length as. a divides (as!i)"
```
```  2625   using as
```
```  2626 proof (induction as)
```
```  2627   case Nil
```
```  2628   then show ?case
```
```  2629     by simp (meson Units_one_closed aprime carr divides_unit primeE)
```
```  2630 next
```
```  2631   case (Cons x as)
```
```  2632   then have "x \<in> carrier G"  "set as \<subseteq> carrier G" and "a divides x \<otimes> foldr (\<otimes>) as \<one>"
```
```  2633     by (auto simp: )
```
```  2634   with carr aprime have "a divides x \<or> a divides foldr (\<otimes>) as \<one>"
```
```  2635     by (intro prime_divides) simp+
```
```  2636   then show ?case
```
```  2637     using Cons.IH Cons.prems(1) by force
```
```  2638 qed
```
```  2639
```
```  2640
```
```  2641 lemma (in primeness_condition_monoid) wfactors_unique__hlp_induct:
```
```  2642   "\<forall>a as'. a \<in> carrier G \<and> set as \<subseteq> carrier G \<and> set as' \<subseteq> carrier G \<and>
```
```  2643            wfactors G as a \<and> wfactors G as' a \<longrightarrow> essentially_equal G as as'"
```
```  2644 proof (induct as)
```
```  2645   case Nil
```
```  2646   show ?case
```
```  2647     apply (clarsimp simp: wfactors_def)
```
```  2648     by (metis Units_one_closed assoc_unit_r list_update_nonempty unit_wfactors_empty unitfactor_ee wfactorsI)
```
```  2649 next
```
```  2650   case (Cons ah as)
```
```  2651   then show ?case
```
```  2652   proof clarsimp
```
```  2653     fix a as'
```
```  2654     assume ih [rule_format]:
```
```  2655       "\<forall>a as'. a \<in> carrier G \<and> set as' \<subseteq> carrier G \<and> wfactors G as a \<and>
```
```  2656         wfactors G as' a \<longrightarrow> essentially_equal G as as'"
```
```  2657       and acarr: "a \<in> carrier G" and ahcarr: "ah \<in> carrier G"
```
```  2658       and ascarr: "set as \<subseteq> carrier G" and as'carr: "set as' \<subseteq> carrier G"
```
```  2659       and afs: "wfactors G (ah # as) a"
```
```  2660       and afs': "wfactors G as' a"
```
```  2661     then have ahdvda: "ah divides a"
```
```  2662       by (intro wfactors_dividesI[of "ah#as" "a"]) simp_all
```
```  2663     then obtain a' where a'carr: "a' \<in> carrier G" and a: "a = ah \<otimes> a'"
```
```  2664       by blast
```
```  2665     have a'fs: "wfactors G as a'"
```
```  2666       apply (rule wfactorsE[OF afs], rule wfactorsI, simp)
```
```  2667       by (metis a a'carr ahcarr ascarr assoc_l_cancel factorsI factors_def factors_mult_single list.set_intros(1) list.set_intros(2) multlist_closed)
```
```  2668     from afs have ahirr: "irreducible G ah"
```
```  2669       by (elim wfactorsE) simp
```
```  2670     with ascarr have ahprime: "prime G ah"
```
```  2671       by (intro irreducible_prime ahcarr)
```
```  2672
```
```  2673     note carr [simp] = acarr ahcarr ascarr as'carr a'carr
```
```  2674
```
```  2675     note ahdvda
```
```  2676     also from afs' have "a divides (foldr (\<otimes>) as' \<one>)"
```
```  2677       by (elim wfactorsE associatedE, simp)
```
```  2678     finally have "ah divides (foldr (\<otimes>) as' \<one>)"
```
```  2679       by simp
```
```  2680     with ahprime have "\<exists>i<length as'. ah divides as'!i"
```
```  2681       by (intro multlist_prime_pos) simp_all
```
```  2682     then obtain i where len: "i<length as'" and ahdvd: "ah divides as'!i"
```
```  2683       by blast
```
```  2684     from afs' carr have irrasi: "irreducible G (as'!i)"
```
```  2685       by (fast intro: nth_mem[OF len] elim: wfactorsE)
```
```  2686     from len carr have asicarr[simp]: "as'!i \<in> carrier G"
```
```  2687       unfolding set_conv_nth by force
```
```  2688     note carr = carr asicarr
```
```  2689
```
```  2690     from ahdvd obtain x where "x \<in> carrier G" and asi: "as'!i = ah \<otimes> x"
```
```  2691       by blast
```
```  2692     with carr irrasi[simplified asi] have asiah: "as'!i \<sim> ah"
```
```  2693       by (metis ahprime associatedI2 irreducible_prodE primeE)
```
```  2694     note setparts = set_take_subset[of i as'] set_drop_subset[of "Suc i" as']
```
```  2695     note partscarr [simp] = setparts[THEN subset_trans[OF _ as'carr]]
```
```  2696     note carr = carr partscarr
```
```  2697
```
```  2698     have "\<exists>aa_1. aa_1 \<in> carrier G \<and> wfactors G (take i as') aa_1"
```
```  2699       by (meson afs' in_set_takeD partscarr(1) wfactorsE wfactors_prod_exists)
```
```  2700     then obtain aa_1 where aa1carr: "aa_1 \<in> carrier G" and aa1fs: "wfactors G (take i as') aa_1"
```
```  2701       by auto
```
```  2702
```
```  2703     have "\<exists>aa_2. aa_2 \<in> carrier G \<and> wfactors G (drop (Suc i) as') aa_2"
```
```  2704       by (meson afs' in_set_dropD partscarr(2) wfactors_def wfactors_prod_exists)
```
```  2705     then obtain aa_2 where aa2carr: "aa_2 \<in> carrier G"
```
```  2706       and aa2fs: "wfactors G (drop (Suc i) as') aa_2"
```
```  2707       by auto
```
```  2708
```
```  2709     note carr = carr aa1carr[simp] aa2carr[simp]
```
```  2710
```
```  2711     from aa1fs aa2fs
```
```  2712     have v1: "wfactors G (take i as' @ drop (Suc i) as') (aa_1 \<otimes> aa_2)"
```
```  2713       by (intro wfactors_mult, simp+)
```
```  2714     then have v1': "wfactors G (as'!i # take i as' @ drop (Suc i) as') (as'!i \<otimes> (aa_1 \<otimes> aa_2))"
```
```  2715       using irrasi wfactors_mult_single by auto
```
```  2716     from aa2carr carr aa1fs aa2fs have "wfactors G (as'!i # drop (Suc i) as') (as'!i \<otimes> aa_2)"
```
```  2717       by (metis irrasi wfactors_mult_single)
```
```  2718     with len carr aa1carr aa2carr aa1fs
```
```  2719     have v2: "wfactors G (take i as' @ as'!i # drop (Suc i) as') (aa_1 \<otimes> (as'!i \<otimes> aa_2))"
```
```  2720       using wfactors_mult by auto
```
```  2721     from len have as': "as' = (take i as' @ as'!i # drop (Suc i) as')"
```
```  2722       by (simp add: Cons_nth_drop_Suc)
```
```  2723     with carr have eer: "essentially_equal G (take i as' @ as'!i # drop (Suc i) as') as'"
```
```  2724       by simp
```
```  2725     with v2 afs' carr aa1carr aa2carr nth_mem[OF len] have "aa_1 \<otimes> (as'!i \<otimes> aa_2) \<sim> a"
```
```  2726       by (metis as' ee_wfactorsD m_closed)
```
```  2727     then have t1: "as'!i \<otimes> (aa_1 \<otimes> aa_2) \<sim> a"
```
```  2728       by (metis aa1carr aa2carr asicarr m_lcomm)
```
```  2729     from carr asiah have "ah \<otimes> (aa_1 \<otimes> aa_2) \<sim> as'!i \<otimes> (aa_1 \<otimes> aa_2)"
```
```  2730       by (metis associated_sym m_closed mult_cong_l)
```
```  2731     also note t1
```
```  2732     finally have "ah \<otimes> (aa_1 \<otimes> aa_2) \<sim> a" by simp
```
```  2733
```
```  2734     with carr aa1carr aa2carr a'carr nth_mem[OF len] have a': "aa_1 \<otimes> aa_2 \<sim> a'"
```
```  2735       by (simp add: a, fast intro: assoc_l_cancel[of ah _ a'])
```
```  2736
```
```  2737     note v1
```
```  2738     also note a'
```
```  2739     finally have "wfactors G (take i as' @ drop (Suc i) as') a'"
```
```  2740       by simp
```
```  2741
```
```  2742     from a'fs this carr have "essentially_equal G as (take i as' @ drop (Suc i) as')"
```
```  2743       by (intro ih[of a']) simp
```
```  2744     then have ee1: "essentially_equal G (ah # as) (ah # take i as' @ drop (Suc i) as')"
```
```  2745       by (elim essentially_equalE) (fastforce intro: essentially_equalI)
```
```  2746
```
```  2747     from carr have ee2: "essentially_equal G (ah # take i as' @ drop (Suc i) as')
```
```  2748       (as' ! i # take i as' @ drop (Suc i) as')"
```
```  2749     proof (intro essentially_equalI)
```
```  2750       show "ah # take i as' @ drop (Suc i) as' <~~> ah # take i as' @ drop (Suc i) as'"
```
```  2751         by simp
```
```  2752     next
```
```  2753       show "ah # take i as' @ drop (Suc i) as' [\<sim>] as' ! i # take i as' @ drop (Suc i) as'"
```
```  2754         by (simp add: list_all2_append) (simp add: asiah[symmetric])
```
```  2755     qed
```
```  2756
```
```  2757     note ee1
```
```  2758     also note ee2
```
```  2759     also have "essentially_equal G (as' ! i # take i as' @ drop (Suc i) as')
```
```  2760                                    (take i as' @ as' ! i # drop (Suc i) as')"
```
```  2761       by (metis as' as'carr listassoc_refl essentially_equalI perm_append_Cons)
```
```  2762     finally have "essentially_equal G (ah # as) (take i as' @ as' ! i # drop (Suc i) as')"
```
```  2763       by simp
```
```  2764     then show "essentially_equal G (ah # as) as'"
```
```  2765       by (subst as')
```
```  2766   qed
```
```  2767 qed
```
```  2768
```
```  2769 lemma (in primeness_condition_monoid) wfactors_unique:
```
```  2770   assumes "wfactors G as a"  "wfactors G as' a"
```
```  2771     and "a \<in> carrier G"  "set as \<subseteq> carrier G"  "set as' \<subseteq> carrier G"
```
```  2772   shows "essentially_equal G as as'"
```
```  2773   by (rule wfactors_unique__hlp_induct[rule_format, of a]) (simp add: assms)
```
```  2774
```
```  2775
```
```  2776 subsubsection \<open>Application to factorial monoids\<close>
```
```  2777
```
```  2778 text \<open>Number of factors for wellfoundedness\<close>
```
```  2779
```
```  2780 definition factorcount :: "_ \<Rightarrow> 'a \<Rightarrow> nat"
```
```  2781   where "factorcount G a =
```
```  2782     (THE c. \<forall>as. set as \<subseteq> carrier G \<and> wfactors G as a \<longrightarrow> c = length as)"
```
```  2783
```
```  2784 lemma (in monoid) ee_length:
```
```  2785   assumes ee: "essentially_equal G as bs"
```
```  2786   shows "length as = length bs"
```
```  2787   by (rule essentially_equalE[OF ee]) (metis list_all2_conv_all_nth perm_length)
```
```  2788
```
```  2789 lemma (in factorial_monoid) factorcount_exists:
```
```  2790   assumes carr[simp]: "a \<in> carrier G"
```
```  2791   shows "\<exists>c. \<forall>as. set as \<subseteq> carrier G \<and> wfactors G as a \<longrightarrow> c = length as"
```
```  2792 proof -
```
```  2793   have "\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as a"
```
```  2794     by (intro wfactors_exist) simp
```
```  2795   then obtain as where ascarr[simp]: "set as \<subseteq> carrier G" and afs: "wfactors G as a"
```
```  2796     by (auto simp del: carr)
```
```  2797   have "\<forall>as'. set as' \<subseteq> carrier G \<and> wfactors G as' a \<longrightarrow> length as = length as'"
```
```  2798     by (metis afs ascarr assms ee_length wfactors_unique)
```
```  2799   then show "\<exists>c. \<forall>as'. set as' \<subseteq> carrier G \<and> wfactors G as' a \<longrightarrow> c = length as'" ..
```
```  2800 qed
```
```  2801
```
```  2802 lemma (in factorial_monoid) factorcount_unique:
```
```  2803   assumes afs: "wfactors G as a"
```
```  2804     and acarr[simp]: "a \<in> carrier G" and ascarr: "set as \<subseteq> carrier G"
```
```  2805   shows "factorcount G a = length as"
```
```  2806 proof -
```
```  2807   have "\<exists>ac. \<forall>as. set as \<subseteq> carrier G \<and> wfactors G as a \<longrightarrow> ac = length as"
```
```  2808     by (rule factorcount_exists) simp
```
```  2809   then obtain ac where alen: "\<forall>as. set as \<subseteq> carrier G \<and> wfactors G as a \<longrightarrow> ac = length as"
```
```  2810     by auto
```
```  2811   then have ac: "ac = factorcount G a"
```
```  2812     unfolding factorcount_def using ascarr by (blast intro: theI2 afs)
```
```  2813   from ascarr afs have "ac = length as"
```
```  2814     by (simp add: alen)
```
```  2815   with ac show ?thesis
```
```  2816     by simp
```
```  2817 qed
```
```  2818
```
```  2819 lemma (in factorial_monoid) divides_fcount:
```
```  2820   assumes dvd: "a divides b"
```
```  2821     and acarr: "a \<in> carrier G"
```
```  2822     and bcarr:"b \<in> carrier G"
```
```  2823   shows "factorcount G a \<le> factorcount G b"
```
```  2824 proof (rule dividesE[OF dvd])
```
```  2825   fix c
```
```  2826   from assms have "\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as a"
```
```  2827     by blast
```
```  2828   then obtain as where ascarr: "set as \<subseteq> carrier G" and afs: "wfactors G as a"
```
```  2829     by blast
```
```  2830   with acarr have fca: "factorcount G a = length as"
```
```  2831     by (intro factorcount_unique)
```
```  2832
```
```  2833   assume ccarr: "c \<in> carrier G"
```
```  2834   then have "\<exists>cs. set cs \<subseteq> carrier G \<and> wfactors G cs c"
```
```  2835     by blast
```
```  2836   then obtain cs where cscarr: "set cs \<subseteq> carrier G" and cfs: "wfactors G cs c"
```
```  2837     by blast
```
```  2838
```
```  2839   note [simp] = acarr bcarr ccarr ascarr cscarr
```
```  2840
```
```  2841   assume b: "b = a \<otimes> c"
```
```  2842   from afs cfs have "wfactors G (as@cs) (a \<otimes> c)"
```
```  2843     by (intro wfactors_mult) simp_all
```
```  2844   with b have "wfactors G (as@cs) b"
```
```  2845     by simp
```
```  2846   then have "factorcount G b = length (as@cs)"
```
```  2847     by (intro factorcount_unique) simp_all
```
```  2848   then have "factorcount G b = length as + length cs"
```
```  2849     by simp
```
```  2850   with fca show ?thesis
```
```  2851     by simp
```
```  2852 qed
```
```  2853
```
```  2854 lemma (in factorial_monoid) associated_fcount:
```
```  2855   assumes acarr: "a \<in> carrier G"
```
```  2856     and bcarr: "b \<in> carrier G"
```
```  2857     and asc: "a \<sim> b"
```
```  2858   shows "factorcount G a = factorcount G b"
```
```  2859   using assms
```
```  2860   by (auto simp: associated_def factorial_monoid.divides_fcount factorial_monoid_axioms le_antisym)
```
```  2861
```
```  2862 lemma (in factorial_monoid) properfactor_fcount:
```
```  2863   assumes acarr: "a \<in> carrier G" and bcarr:"b \<in> carrier G"
```
```  2864     and pf: "properfactor G a b"
```
```  2865   shows "factorcount G a < factorcount G b"
```
```  2866 proof (rule properfactorE[OF pf], elim dividesE)
```
```  2867   fix c
```
```  2868   from assms have "\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as a"
```
```  2869     by blast
```
```  2870   then obtain as where ascarr: "set as \<subseteq> carrier G" and afs: "wfactors G as a"
```
```  2871     by blast
```
```  2872   with acarr have fca: "factorcount G a = length as"
```
```  2873     by (intro factorcount_unique)
```
```  2874
```
```  2875   assume ccarr: "c \<in> carrier G"
```
```  2876   then have "\<exists>cs. set cs \<subseteq> carrier G \<and> wfactors G cs c"
```
```  2877     by blast
```
```  2878   then obtain cs where cscarr: "set cs \<subseteq> carrier G" and cfs: "wfactors G cs c"
```
```  2879     by blast
```
```  2880
```
```  2881   assume b: "b = a \<otimes> c"
```
```  2882
```
```  2883   have "wfactors G (as@cs) (a \<otimes> c)"
```
```  2884     by (rule wfactors_mult) fact+
```
```  2885   with b have "wfactors G (as@cs) b"
```
```  2886     by simp
```
```  2887   with ascarr cscarr bcarr have "factorcount G b = length (as@cs)"
```
```  2888     by (simp add: factorcount_unique)
```
```  2889   then have fcb: "factorcount G b = length as + length cs"
```
```  2890     by simp
```
```  2891
```
```  2892   assume nbdvda: "\<not> b divides a"
```
```  2893   have "c \<notin> Units G"
```
```  2894   proof
```
```  2895     assume cunit:"c \<in> Units G"
```
```  2896     have "b \<otimes> inv c = a \<otimes> c \<otimes> inv c"
```
```  2897       by (simp add: b)
```
```  2898     also from ccarr acarr cunit have "\<dots> = a \<otimes> (c \<otimes> inv c)"
```
```  2899       by (fast intro: m_assoc)
```
```  2900     also from ccarr cunit have "\<dots> = a \<otimes> \<one>" by simp
```
```  2901     also from acarr have "\<dots> = a" by simp
```
```  2902     finally have "a = b \<otimes> inv c" by simp
```
```  2903     with ccarr cunit have "b divides a"
```
```  2904       by (fast intro: dividesI[of "inv c"])
```
```  2905     with nbdvda show False by simp
```
```  2906   qed
```
```  2907   with cfs have "length cs > 0"
```
```  2908     by (metis Units_one_closed assoc_unit_r ccarr foldr.simps(1) id_apply length_greater_0_conv wfactors_def)
```
```  2909   with fca fcb show ?thesis
```
```  2910     by simp
```
```  2911 qed
```
```  2912
```
```  2913 sublocale factorial_monoid \<subseteq> divisor_chain_condition_monoid
```
```  2914   apply unfold_locales
```
```  2915   apply (rule wfUNIVI)
```
```  2916   apply (rule measure_induct[of "factorcount G"])
```
```  2917   apply simp
```
```  2918   apply (metis properfactor_fcount)
```
```  2919   done
```
```  2920
```
```  2921 sublocale factorial_monoid \<subseteq> primeness_condition_monoid
```
```  2922   by standard (rule irreducible_prime)
```
```  2923
```
```  2924
```
```  2925 lemma (in factorial_monoid) primeness_condition: "primeness_condition_monoid G" ..
```
```  2926
```
```  2927 lemma (in factorial_monoid) gcd_condition [simp]: "gcd_condition_monoid G"
```
```  2928   by standard (rule gcdof_exists)
```
```  2929
```
```  2930 sublocale factorial_monoid \<subseteq> gcd_condition_monoid
```
```  2931   by standard (rule gcdof_exists)
```
```  2932
```
```  2933 lemma (in factorial_monoid) division_weak_lattice [simp]: "weak_lattice (division_rel G)"
```
```  2934 proof -
```
```  2935   interpret weak_lower_semilattice "division_rel G"
```
```  2936     by simp
```
```  2937   show "weak_lattice (division_rel G)"
```
```  2938   proof (unfold_locales, simp_all)
```
```  2939     fix x y
```
```  2940     assume carr: "x \<in> carrier G"  "y \<in> carrier G"
```
```  2941     from lcmof_exists [OF this] obtain z where zcarr: "z \<in> carrier G" and isgcd: "z lcmof x y"
```
```  2942       by blast
```
```  2943     with carr have "least (division_rel G) z (Upper (division_rel G) {x, y})"
```
```  2944       by (simp add: lcmof_leastUpper[symmetric])
```
```  2945     then show "\<exists>z. least (division_rel G) z (Upper (division_rel G) {x, y})"
```
```  2946       by blast
```
```  2947   qed
```
```  2948 qed
```
```  2949
```
```  2950
```
```  2951 subsection \<open>Factoriality Theorems\<close>
```
```  2952
```
```  2953 theorem factorial_condition_one: (* Jacobson theorem 2.21 *)
```
```  2954   "divisor_chain_condition_monoid G \<and> primeness_condition_monoid G \<longleftrightarrow> factorial_monoid G"
```
```  2955 proof (rule iffI, clarify)
```
```  2956   assume dcc: "divisor_chain_condition_monoid G"
```
```  2957     and pc: "primeness_condition_monoid G"
```
```  2958   interpret divisor_chain_condition_monoid "G" by (rule dcc)
```
```  2959   interpret primeness_condition_monoid "G" by (rule pc)
```
```  2960   show "factorial_monoid G"
```
```  2961     by (fast intro: factorial_monoidI wfactors_exist wfactors_unique)
```
```  2962 next
```
```  2963   assume "factorial_monoid G"
```
```  2964   then interpret factorial_monoid "G" .
```
```  2965   show "divisor_chain_condition_monoid G \<and> primeness_condition_monoid G"
```
```  2966     by rule unfold_locales
```
```  2967 qed
```
```  2968
```
```  2969 theorem factorial_condition_two: (* Jacobson theorem 2.22 *)
```
```  2970   "divisor_chain_condition_monoid G \<and> gcd_condition_monoid G \<longleftrightarrow> factorial_monoid G"
```
```  2971 proof (rule iffI, clarify)
```
```  2972   assume dcc: "divisor_chain_condition_monoid G"
```
```  2973     and gc: "gcd_condition_monoid G"
```
```  2974   interpret divisor_chain_condition_monoid "G" by (rule dcc)
```
```  2975   interpret gcd_condition_monoid "G" by (rule gc)
```
```  2976   show "factorial_monoid G"
```
```  2977     by (simp add: factorial_condition_one[symmetric], rule, unfold_locales)
```
```  2978 next
```
```  2979   assume "factorial_monoid G"
```
```  2980   then interpret factorial_monoid "G" .
```
```  2981   show "divisor_chain_condition_monoid G \<and> gcd_condition_monoid G"
```
```  2982     by rule unfold_locales
```
```  2983 qed
```
```  2984
```
```  2985 end
```