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