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