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