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