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