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