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