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