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