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