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