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