src/ZF/ex/Group.thy
author ballarin
Thu Dec 11 18:30:26 2008 +0100 (2008-12-11)
changeset 29223 e09c53289830
parent 27618 72fe9939a2ab
child 32960 69916a850301
permissions -rw-r--r--
Conversion of HOL-Main and ZF to new locales.
paulson@14884
     1
(* Title:  ZF/ex/Group.thy
paulson@14884
     2
paulson@14884
     3
*)
paulson@14884
     4
paulson@14884
     5
header {* Groups *}
paulson@14884
     6
haftmann@16417
     7
theory Group imports Main begin
paulson@14884
     8
paulson@14884
     9
text{*Based on work by Clemens Ballarin, Florian Kammueller, L C Paulson and
paulson@14884
    10
Markus Wenzel.*}
paulson@14884
    11
paulson@14884
    12
paulson@14884
    13
subsection {* Monoids *}
paulson@14884
    14
paulson@14884
    15
(*First, we must simulate a record declaration:
paulson@14884
    16
record monoid = 
paulson@14884
    17
  carrier :: i
paulson@14891
    18
  mult :: "[i,i] => i" (infixl "\<cdot>\<index>" 70)
paulson@14884
    19
  one :: i ("\<one>\<index>")
paulson@14884
    20
*)
paulson@14884
    21
wenzelm@21233
    22
definition
wenzelm@21404
    23
  carrier :: "i => i" where
wenzelm@21233
    24
  "carrier(M) == fst(M)"
paulson@14884
    25
wenzelm@21404
    26
definition
wenzelm@21404
    27
  mmult :: "[i, i, i] => i" (infixl "\<cdot>\<index>" 70) where
wenzelm@21233
    28
  "mmult(M,x,y) == fst(snd(M)) ` <x,y>"
paulson@14884
    29
wenzelm@21404
    30
definition
wenzelm@21404
    31
  one :: "i => i" ("\<one>\<index>") where
wenzelm@21233
    32
  "one(M) == fst(snd(snd(M)))"
paulson@14884
    33
wenzelm@21404
    34
definition
wenzelm@21404
    35
  update_carrier :: "[i,i] => i" where
wenzelm@21233
    36
  "update_carrier(M,A) == <A,snd(M)>"
paulson@14884
    37
wenzelm@21233
    38
definition
wenzelm@21404
    39
  m_inv :: "i => i => i" ("inv\<index> _" [81] 80) where
wenzelm@21233
    40
  "inv\<^bsub>G\<^esub> x == (THE y. y \<in> carrier(G) & y \<cdot>\<^bsub>G\<^esub> x = \<one>\<^bsub>G\<^esub> & x \<cdot>\<^bsub>G\<^esub> y = \<one>\<^bsub>G\<^esub>)"
paulson@14884
    41
ballarin@29223
    42
locale monoid = fixes G (structure)
paulson@14884
    43
  assumes m_closed [intro, simp]:
paulson@14884
    44
         "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk> \<Longrightarrow> x \<cdot> y \<in> carrier(G)"
paulson@14884
    45
      and m_assoc:
paulson@14884
    46
         "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk> 
paulson@14884
    47
          \<Longrightarrow> (x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
paulson@14884
    48
      and one_closed [intro, simp]: "\<one> \<in> carrier(G)"
paulson@14884
    49
      and l_one [simp]: "x \<in> carrier(G) \<Longrightarrow> \<one> \<cdot> x = x"
paulson@14884
    50
      and r_one [simp]: "x \<in> carrier(G) \<Longrightarrow> x \<cdot> \<one> = x"
paulson@14884
    51
paulson@14884
    52
text{*Simulating the record*}
paulson@14884
    53
lemma carrier_eq [simp]: "carrier(<A,Z>) = A"
paulson@14884
    54
  by (simp add: carrier_def)
paulson@14884
    55
paulson@14884
    56
lemma mult_eq [simp]: "mmult(<A,M,Z>, x, y) = M ` <x,y>"
paulson@14884
    57
  by (simp add: mmult_def)
paulson@14884
    58
paulson@14884
    59
lemma one_eq [simp]: "one(<A,M,I,Z>) = I"
paulson@14884
    60
  by (simp add: one_def)
paulson@14884
    61
paulson@14884
    62
lemma update_carrier_eq [simp]: "update_carrier(<A,Z>,B) = <B,Z>"
paulson@14884
    63
  by (simp add: update_carrier_def)
paulson@14884
    64
paulson@14884
    65
lemma carrier_update_carrier [simp]: "carrier(update_carrier(M,B)) = B"
wenzelm@22931
    66
  by (simp add: update_carrier_def) 
paulson@14884
    67
paulson@14884
    68
lemma mult_update_carrier [simp]: "mmult(update_carrier(M,B),x,y) = mmult(M,x,y)"
wenzelm@22931
    69
  by (simp add: update_carrier_def mmult_def) 
paulson@14884
    70
paulson@14884
    71
lemma one_update_carrier [simp]: "one(update_carrier(M,B)) = one(M)"
wenzelm@22931
    72
  by (simp add: update_carrier_def one_def) 
paulson@14884
    73
paulson@14884
    74
paulson@14884
    75
lemma (in monoid) inv_unique:
paulson@14884
    76
  assumes eq: "y \<cdot> x = \<one>"  "x \<cdot> y' = \<one>"
paulson@14884
    77
    and G: "x \<in> carrier(G)"  "y \<in> carrier(G)"  "y' \<in> carrier(G)"
paulson@14884
    78
  shows "y = y'"
paulson@14884
    79
proof -
paulson@14884
    80
  from G eq have "y = y \<cdot> (x \<cdot> y')" by simp
paulson@14884
    81
  also from G have "... = (y \<cdot> x) \<cdot> y'" by (simp add: m_assoc)
paulson@14884
    82
  also from G eq have "... = y'" by simp
paulson@14884
    83
  finally show ?thesis .
paulson@14884
    84
qed
paulson@14884
    85
paulson@14884
    86
text {*
paulson@14884
    87
  A group is a monoid all of whose elements are invertible.
paulson@14884
    88
*}
paulson@14884
    89
paulson@14884
    90
locale group = monoid +
paulson@14884
    91
  assumes inv_ex:
paulson@14884
    92
     "\<And>x. x \<in> carrier(G) \<Longrightarrow> \<exists>y \<in> carrier(G). y \<cdot> x = \<one> & x \<cdot> y = \<one>"
paulson@14884
    93
wenzelm@26199
    94
lemma (in group) is_group [simp]: "group(G)" by (rule group_axioms)
paulson@14884
    95
paulson@14884
    96
theorem groupI:
ballarin@27618
    97
  fixes G (structure)
paulson@14884
    98
  assumes m_closed [simp]:
paulson@14884
    99
      "\<And>x y. \<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk> \<Longrightarrow> x \<cdot> y \<in> carrier(G)"
paulson@14884
   100
    and one_closed [simp]: "\<one> \<in> carrier(G)"
paulson@14884
   101
    and m_assoc:
paulson@14884
   102
      "\<And>x y z. \<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk> \<Longrightarrow>
paulson@14884
   103
      (x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
paulson@14884
   104
    and l_one [simp]: "\<And>x. x \<in> carrier(G) \<Longrightarrow> \<one> \<cdot> x = x"
paulson@14884
   105
    and l_inv_ex: "\<And>x. x \<in> carrier(G) \<Longrightarrow> \<exists>y \<in> carrier(G). y \<cdot> x = \<one>"
paulson@14884
   106
  shows "group(G)"
paulson@14884
   107
proof -
paulson@14884
   108
  have l_cancel [simp]:
paulson@14884
   109
    "\<And>x y z. \<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk> \<Longrightarrow>
paulson@14884
   110
    (x \<cdot> y = x \<cdot> z) <-> (y = z)"
paulson@14884
   111
  proof
paulson@14884
   112
    fix x y z
paulson@14884
   113
    assume G: "x \<in> carrier(G)"  "y \<in> carrier(G)"  "z \<in> carrier(G)"
paulson@14884
   114
    { 
paulson@14884
   115
      assume eq: "x \<cdot> y = x \<cdot> z"
paulson@14884
   116
      with G l_inv_ex obtain x_inv where xG: "x_inv \<in> carrier(G)"
paulson@14884
   117
	and l_inv: "x_inv \<cdot> x = \<one>" by fast
paulson@14884
   118
      from G eq xG have "(x_inv \<cdot> x) \<cdot> y = (x_inv \<cdot> x) \<cdot> z"
paulson@14884
   119
	by (simp add: m_assoc)
paulson@14884
   120
      with G show "y = z" by (simp add: l_inv)
paulson@14884
   121
    next
paulson@14884
   122
      assume eq: "y = z"
paulson@14884
   123
      with G show "x \<cdot> y = x \<cdot> z" by simp
paulson@14884
   124
    }
paulson@14884
   125
  qed
paulson@14884
   126
  have r_one:
paulson@14884
   127
    "\<And>x. x \<in> carrier(G) \<Longrightarrow> x \<cdot> \<one> = x"
paulson@14884
   128
  proof -
paulson@14884
   129
    fix x
paulson@14884
   130
    assume x: "x \<in> carrier(G)"
paulson@14884
   131
    with l_inv_ex obtain x_inv where xG: "x_inv \<in> carrier(G)"
paulson@14884
   132
      and l_inv: "x_inv \<cdot> x = \<one>" by fast
paulson@14884
   133
    from x xG have "x_inv \<cdot> (x \<cdot> \<one>) = x_inv \<cdot> x"
paulson@14884
   134
      by (simp add: m_assoc [symmetric] l_inv)
paulson@14884
   135
    with x xG show "x \<cdot> \<one> = x" by simp
paulson@14884
   136
  qed
paulson@14884
   137
  have inv_ex:
paulson@14884
   138
    "!!x. x \<in> carrier(G) ==> \<exists>y \<in> carrier(G). y \<cdot> x = \<one> & x \<cdot> y = \<one>"
paulson@14884
   139
  proof -
paulson@14884
   140
    fix x
paulson@14884
   141
    assume x: "x \<in> carrier(G)"
paulson@14884
   142
    with l_inv_ex obtain y where y: "y \<in> carrier(G)"
paulson@14884
   143
      and l_inv: "y \<cdot> x = \<one>" by fast
paulson@14884
   144
    from x y have "y \<cdot> (x \<cdot> y) = y \<cdot> \<one>"
paulson@14884
   145
      by (simp add: m_assoc [symmetric] l_inv r_one)
paulson@14884
   146
    with x y have r_inv: "x \<cdot> y = \<one>"
paulson@14884
   147
      by simp
paulson@14884
   148
    from x y show "\<exists>y \<in> carrier(G). y \<cdot> x = \<one> & x \<cdot> y = \<one>"
paulson@14884
   149
      by (fast intro: l_inv r_inv)
paulson@14884
   150
  qed
paulson@14884
   151
  show ?thesis
paulson@14884
   152
    by (blast intro: group.intro monoid.intro group_axioms.intro 
paulson@14884
   153
                     prems r_one inv_ex)
paulson@14884
   154
qed
paulson@14884
   155
paulson@14884
   156
lemma (in group) inv [simp]:
paulson@14884
   157
  "x \<in> carrier(G) \<Longrightarrow> inv x \<in> carrier(G) & inv x \<cdot> x = \<one> & x \<cdot> inv x = \<one>"
paulson@14884
   158
  apply (frule inv_ex) 
paulson@14884
   159
  apply (unfold Bex_def m_inv_def)
paulson@14884
   160
  apply (erule exE) 
paulson@14884
   161
  apply (rule theI)
paulson@14884
   162
  apply (rule ex1I, assumption)
paulson@14884
   163
   apply (blast intro: inv_unique)
paulson@14884
   164
  done
paulson@14884
   165
paulson@14884
   166
lemma (in group) inv_closed [intro!]:
paulson@14884
   167
  "x \<in> carrier(G) \<Longrightarrow> inv x \<in> carrier(G)"
paulson@14884
   168
  by simp
paulson@14884
   169
paulson@14884
   170
lemma (in group) l_inv:
paulson@14884
   171
  "x \<in> carrier(G) \<Longrightarrow> inv x \<cdot> x = \<one>"
paulson@14884
   172
  by simp
paulson@14884
   173
paulson@14884
   174
lemma (in group) r_inv:
paulson@14884
   175
  "x \<in> carrier(G) \<Longrightarrow> x \<cdot> inv x = \<one>"
paulson@14884
   176
  by simp
paulson@14884
   177
paulson@14884
   178
paulson@14884
   179
subsection {* Cancellation Laws and Basic Properties *}
paulson@14884
   180
paulson@14884
   181
lemma (in group) l_cancel [simp]:
paulson@14884
   182
  assumes [simp]: "x \<in> carrier(G)" "y \<in> carrier(G)" "z \<in> carrier(G)"
paulson@14884
   183
  shows "(x \<cdot> y = x \<cdot> z) <-> (y = z)"
paulson@14884
   184
proof
paulson@14884
   185
  assume eq: "x \<cdot> y = x \<cdot> z"
paulson@14884
   186
  hence  "(inv x \<cdot> x) \<cdot> y = (inv x \<cdot> x) \<cdot> z"
paulson@14884
   187
    by (simp only: m_assoc inv_closed prems)
paulson@14884
   188
  thus "y = z" by simp
paulson@14884
   189
next
paulson@14884
   190
  assume eq: "y = z"
paulson@14884
   191
  then show "x \<cdot> y = x \<cdot> z" by simp
paulson@14884
   192
qed
paulson@14884
   193
paulson@14884
   194
lemma (in group) r_cancel [simp]:
paulson@14884
   195
  assumes [simp]: "x \<in> carrier(G)" "y \<in> carrier(G)" "z \<in> carrier(G)"
paulson@14884
   196
  shows "(y \<cdot> x = z \<cdot> x) <-> (y = z)"
paulson@14884
   197
proof
paulson@14884
   198
  assume eq: "y \<cdot> x = z \<cdot> x"
paulson@14884
   199
  then have "y \<cdot> (x \<cdot> inv x) = z \<cdot> (x \<cdot> inv x)"
paulson@14884
   200
    by (simp only: m_assoc [symmetric] inv_closed prems)
paulson@14884
   201
  thus "y = z" by simp
paulson@14884
   202
next
paulson@14884
   203
  assume eq: "y = z"
paulson@14884
   204
  thus  "y \<cdot> x = z \<cdot> x" by simp
paulson@14884
   205
qed
paulson@14884
   206
paulson@14884
   207
lemma (in group) inv_comm:
paulson@14884
   208
  assumes inv: "x \<cdot> y = \<one>"
paulson@14884
   209
      and G: "x \<in> carrier(G)"  "y \<in> carrier(G)"
paulson@14884
   210
  shows "y \<cdot> x = \<one>"
paulson@14884
   211
proof -
paulson@14884
   212
  from G have "x \<cdot> y \<cdot> x = x \<cdot> \<one>" by (auto simp add: inv)
paulson@14884
   213
  with G show ?thesis by (simp del: r_one add: m_assoc)
paulson@14884
   214
qed
paulson@14884
   215
paulson@14884
   216
lemma (in group) inv_equality:
paulson@14884
   217
     "\<lbrakk>y \<cdot> x = \<one>; x \<in> carrier(G); y \<in> carrier(G)\<rbrakk> \<Longrightarrow> inv x = y"
paulson@14884
   218
apply (simp add: m_inv_def)
paulson@14884
   219
apply (rule the_equality)
paulson@14884
   220
 apply (simp add: inv_comm [of y x])
paulson@14884
   221
apply (rule r_cancel [THEN iffD1], auto)
paulson@14884
   222
done
paulson@14884
   223
paulson@14884
   224
lemma (in group) inv_one [simp]:
paulson@14884
   225
  "inv \<one> = \<one>"
paulson@14884
   226
  by (auto intro: inv_equality) 
paulson@14884
   227
paulson@14884
   228
lemma (in group) inv_inv [simp]: "x \<in> carrier(G) \<Longrightarrow> inv (inv x) = x"
paulson@14884
   229
  by (auto intro: inv_equality) 
paulson@14884
   230
paulson@14884
   231
text{*This proof is by cancellation*}
paulson@14884
   232
lemma (in group) inv_mult_group:
paulson@14884
   233
  "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk> \<Longrightarrow> inv (x \<cdot> y) = inv y \<cdot> inv x"
paulson@14884
   234
proof -
paulson@14884
   235
  assume G: "x \<in> carrier(G)"  "y \<in> carrier(G)"
paulson@14884
   236
  then have "inv (x \<cdot> y) \<cdot> (x \<cdot> y) = (inv y \<cdot> inv x) \<cdot> (x \<cdot> y)"
paulson@14884
   237
    by (simp add: m_assoc l_inv) (simp add: m_assoc [symmetric] l_inv)
paulson@14884
   238
  with G show ?thesis by (simp_all del: inv add: inv_closed)
paulson@14884
   239
qed
paulson@14884
   240
paulson@14884
   241
paulson@14884
   242
subsection {* Substructures *}
paulson@14884
   243
ballarin@29223
   244
locale subgroup = fixes H and G (structure)
paulson@14884
   245
  assumes subset: "H \<subseteq> carrier(G)"
paulson@14884
   246
    and m_closed [intro, simp]: "\<lbrakk>x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> x \<cdot> y \<in> H"
paulson@14884
   247
    and  one_closed [simp]: "\<one> \<in> H"
paulson@14884
   248
    and m_inv_closed [intro,simp]: "x \<in> H \<Longrightarrow> inv x \<in> H"
paulson@14884
   249
paulson@14884
   250
paulson@14884
   251
lemma (in subgroup) mem_carrier [simp]:
paulson@14884
   252
  "x \<in> H \<Longrightarrow> x \<in> carrier(G)"
paulson@14884
   253
  using subset by blast
paulson@14884
   254
paulson@14884
   255
paulson@14884
   256
lemma subgroup_imp_subset:
paulson@14884
   257
  "subgroup(H,G) \<Longrightarrow> H \<subseteq> carrier(G)"
paulson@14884
   258
  by (rule subgroup.subset)
paulson@14884
   259
paulson@14884
   260
lemma (in subgroup) group_axiomsI [intro]:
ballarin@27618
   261
  assumes "group(G)"
paulson@14884
   262
  shows "group_axioms (update_carrier(G,H))"
ballarin@27618
   263
proof -
ballarin@29223
   264
  interpret group G by fact
ballarin@27618
   265
  show ?thesis by (force intro: group_axioms.intro l_inv r_inv)
ballarin@27618
   266
qed
paulson@14884
   267
paulson@14891
   268
lemma (in subgroup) is_group [intro]:
ballarin@27618
   269
  assumes "group(G)"
paulson@14891
   270
  shows "group (update_carrier(G,H))"
ballarin@27618
   271
proof -
ballarin@29223
   272
  interpret group G by fact
ballarin@27618
   273
  show ?thesis
paulson@14884
   274
  by (rule groupI) (auto intro: m_assoc l_inv mem_carrier)
ballarin@27618
   275
qed
paulson@14884
   276
paulson@14884
   277
text {*
paulson@14884
   278
  Since @{term H} is nonempty, it contains some element @{term x}.  Since
paulson@14884
   279
  it is closed under inverse, it contains @{text "inv x"}.  Since
paulson@14884
   280
  it is closed under product, it contains @{text "x \<cdot> inv x = \<one>"}.
paulson@14884
   281
*}
paulson@14884
   282
paulson@14884
   283
text {*
paulson@14884
   284
  Since @{term H} is nonempty, it contains some element @{term x}.  Since
paulson@14884
   285
  it is closed under inverse, it contains @{text "inv x"}.  Since
paulson@14884
   286
  it is closed under product, it contains @{text "x \<cdot> inv x = \<one>"}.
paulson@14884
   287
*}
paulson@14884
   288
paulson@14884
   289
lemma (in group) one_in_subset:
paulson@14884
   290
  "\<lbrakk>H \<subseteq> carrier(G); H \<noteq> 0; \<forall>a \<in> H. inv a \<in> H; \<forall>a\<in>H. \<forall>b\<in>H. a \<cdot> b \<in> H\<rbrakk>
paulson@14884
   291
   \<Longrightarrow> \<one> \<in> H"
paulson@14884
   292
by (force simp add: l_inv)
paulson@14884
   293
paulson@14884
   294
text {* A characterization of subgroups: closed, non-empty subset. *}
paulson@14884
   295
paulson@14884
   296
declare monoid.one_closed [simp] group.inv_closed [simp]
paulson@14884
   297
  monoid.l_one [simp] monoid.r_one [simp] group.inv_inv [simp]
paulson@14884
   298
paulson@14884
   299
lemma subgroup_nonempty:
paulson@14884
   300
  "~ subgroup(0,G)"
paulson@14884
   301
  by (blast dest: subgroup.one_closed)
paulson@14884
   302
paulson@14884
   303
paulson@14884
   304
subsection {* Direct Products *}
paulson@14884
   305
wenzelm@21233
   306
definition
wenzelm@21404
   307
  DirProdGroup :: "[i,i] => i"  (infixr "\<Otimes>" 80) where
paulson@14884
   308
  "G \<Otimes> H == <carrier(G) \<times> carrier(H),
paulson@14884
   309
              (\<lambda><<g,h>, <g', h'>>
paulson@14884
   310
                   \<in> (carrier(G) \<times> carrier(H)) \<times> (carrier(G) \<times> carrier(H)).
paulson@14884
   311
                <g \<cdot>\<^bsub>G\<^esub> g', h \<cdot>\<^bsub>H\<^esub> h'>),
paulson@14884
   312
              <\<one>\<^bsub>G\<^esub>, \<one>\<^bsub>H\<^esub>>, 0>"
paulson@14884
   313
paulson@14884
   314
lemma DirProdGroup_group:
ballarin@27618
   315
  assumes "group(G)" and "group(H)"
paulson@14884
   316
  shows "group (G \<Otimes> H)"
ballarin@27618
   317
proof -
ballarin@29223
   318
  interpret G: group G by fact
ballarin@29223
   319
  interpret H: group H by fact
ballarin@27618
   320
  show ?thesis by (force intro!: groupI G.m_assoc H.m_assoc G.l_inv H.l_inv
paulson@14884
   321
          simp add: DirProdGroup_def)
ballarin@27618
   322
qed
paulson@14884
   323
paulson@14884
   324
lemma carrier_DirProdGroup [simp]:
paulson@14884
   325
     "carrier (G \<Otimes> H) = carrier(G) \<times> carrier(H)"
paulson@14884
   326
  by (simp add: DirProdGroup_def)
paulson@14884
   327
paulson@14884
   328
lemma one_DirProdGroup [simp]:
paulson@14884
   329
     "\<one>\<^bsub>G \<Otimes> H\<^esub> = <\<one>\<^bsub>G\<^esub>, \<one>\<^bsub>H\<^esub>>"
paulson@14884
   330
  by (simp add: DirProdGroup_def)
paulson@14884
   331
paulson@14884
   332
lemma mult_DirProdGroup [simp]:
paulson@14884
   333
     "[|g \<in> carrier(G); h \<in> carrier(H); g' \<in> carrier(G); h' \<in> carrier(H)|]
paulson@14884
   334
      ==> <g, h> \<cdot>\<^bsub>G \<Otimes> H\<^esub> <g', h'> = <g \<cdot>\<^bsub>G\<^esub> g', h \<cdot>\<^bsub>H\<^esub> h'>"
wenzelm@22931
   335
  by (simp add: DirProdGroup_def)
paulson@14884
   336
paulson@14884
   337
lemma inv_DirProdGroup [simp]:
ballarin@27618
   338
  assumes "group(G)" and "group(H)"
paulson@14884
   339
  assumes g: "g \<in> carrier(G)"
paulson@14884
   340
      and h: "h \<in> carrier(H)"
paulson@14884
   341
  shows "inv \<^bsub>G \<Otimes> H\<^esub> <g, h> = <inv\<^bsub>G\<^esub> g, inv\<^bsub>H\<^esub> h>"
paulson@14884
   342
  apply (rule group.inv_equality [OF DirProdGroup_group])
ballarin@19931
   343
  apply (simp_all add: prems group.l_inv)
paulson@14884
   344
  done
paulson@14884
   345
paulson@14884
   346
subsection {* Isomorphisms *}
paulson@14884
   347
wenzelm@21233
   348
definition
wenzelm@21404
   349
  hom :: "[i,i] => i" where
paulson@14884
   350
  "hom(G,H) ==
paulson@14884
   351
    {h \<in> carrier(G) -> carrier(H).
paulson@14884
   352
      (\<forall>x \<in> carrier(G). \<forall>y \<in> carrier(G). h ` (x \<cdot>\<^bsub>G\<^esub> y) = (h ` x) \<cdot>\<^bsub>H\<^esub> (h ` y))}"
paulson@14884
   353
paulson@14884
   354
lemma hom_mult:
paulson@14884
   355
  "\<lbrakk>h \<in> hom(G,H); x \<in> carrier(G); y \<in> carrier(G)\<rbrakk>
paulson@14884
   356
   \<Longrightarrow> h ` (x \<cdot>\<^bsub>G\<^esub> y) = h ` x \<cdot>\<^bsub>H\<^esub> h ` y"
paulson@14884
   357
  by (simp add: hom_def)
paulson@14884
   358
paulson@14884
   359
lemma hom_closed:
paulson@14884
   360
  "\<lbrakk>h \<in> hom(G,H); x \<in> carrier(G)\<rbrakk> \<Longrightarrow> h ` x \<in> carrier(H)"
paulson@14884
   361
  by (auto simp add: hom_def)
paulson@14884
   362
paulson@14884
   363
lemma (in group) hom_compose:
paulson@14884
   364
     "\<lbrakk>h \<in> hom(G,H); i \<in> hom(H,I)\<rbrakk> \<Longrightarrow> i O h \<in> hom(G,I)"
paulson@14884
   365
by (force simp add: hom_def comp_fun) 
paulson@14884
   366
paulson@14884
   367
lemma hom_is_fun:
paulson@14884
   368
  "h \<in> hom(G,H) \<Longrightarrow> h \<in> carrier(G) -> carrier(H)"
paulson@14884
   369
  by (simp add: hom_def)
paulson@14884
   370
paulson@14884
   371
paulson@14884
   372
subsection {* Isomorphisms *}
paulson@14884
   373
wenzelm@21233
   374
definition
wenzelm@21404
   375
  iso :: "[i,i] => i"  (infixr "\<cong>" 60) where
paulson@14884
   376
  "G \<cong> H == hom(G,H) \<inter> bij(carrier(G), carrier(H))"
paulson@14884
   377
paulson@14884
   378
lemma (in group) iso_refl: "id(carrier(G)) \<in> G \<cong> G"
wenzelm@22931
   379
  by (simp add: iso_def hom_def id_type id_bij) 
paulson@14884
   380
paulson@14884
   381
paulson@14884
   382
lemma (in group) iso_sym:
paulson@14884
   383
     "h \<in> G \<cong> H \<Longrightarrow> converse(h) \<in> H \<cong> G"
paulson@14884
   384
apply (simp add: iso_def bij_converse_bij, clarify) 
paulson@14884
   385
apply (subgoal_tac "converse(h) \<in> carrier(H) \<rightarrow> carrier(G)") 
paulson@14884
   386
 prefer 2 apply (simp add: bij_converse_bij bij_is_fun) 
paulson@14884
   387
apply (auto intro: left_inverse_eq [of _ "carrier(G)" "carrier(H)"] 
paulson@14884
   388
            simp add: hom_def bij_is_inj right_inverse_bij); 
paulson@14884
   389
done
paulson@14884
   390
paulson@14884
   391
lemma (in group) iso_trans: 
paulson@14884
   392
     "\<lbrakk>h \<in> G \<cong> H; i \<in> H \<cong> I\<rbrakk> \<Longrightarrow> i O h \<in> G \<cong> I"
wenzelm@22931
   393
  by (auto simp add: iso_def hom_compose comp_bij)
paulson@14884
   394
paulson@14884
   395
lemma DirProdGroup_commute_iso:
ballarin@27618
   396
  assumes "group(G)" and "group(H)"
paulson@14884
   397
  shows "(\<lambda><x,y> \<in> carrier(G \<Otimes> H). <y,x>) \<in> (G \<Otimes> H) \<cong> (H \<Otimes> G)"
ballarin@27618
   398
proof -
ballarin@29223
   399
  interpret group G by fact
ballarin@29223
   400
  interpret group H by fact
ballarin@27618
   401
  show ?thesis by (auto simp add: iso_def hom_def inj_def surj_def bij_def)
ballarin@27618
   402
qed
paulson@14884
   403
paulson@14884
   404
lemma DirProdGroup_assoc_iso:
ballarin@27618
   405
  assumes "group(G)" and "group(H)" and "group(I)"
paulson@14884
   406
  shows "(\<lambda><<x,y>,z> \<in> carrier((G \<Otimes> H) \<Otimes> I). <x,<y,z>>)
paulson@14884
   407
          \<in> ((G \<Otimes> H) \<Otimes> I) \<cong> (G \<Otimes> (H \<Otimes> I))"
ballarin@27618
   408
proof -
ballarin@29223
   409
  interpret group G by fact
ballarin@29223
   410
  interpret group H by fact
ballarin@29223
   411
  interpret group I by fact
ballarin@27618
   412
  show ?thesis
ballarin@27618
   413
    by (auto intro: lam_type simp add: iso_def hom_def inj_def surj_def bij_def) 
ballarin@27618
   414
qed
paulson@14884
   415
paulson@14884
   416
text{*Basis for homomorphism proofs: we assume two groups @{term G} and
paulson@14884
   417
  @term{H}, with a homomorphism @{term h} between them*}
ballarin@29223
   418
locale group_hom = G: group G + H: group H
ballarin@29223
   419
  for G (structure) and H (structure) and h +
paulson@14884
   420
  assumes homh: "h \<in> hom(G,H)"
paulson@14884
   421
  notes hom_mult [simp] = hom_mult [OF homh]
paulson@14884
   422
    and hom_closed [simp] = hom_closed [OF homh]
paulson@14884
   423
    and hom_is_fun [simp] = hom_is_fun [OF homh]
paulson@14884
   424
paulson@14884
   425
lemma (in group_hom) one_closed [simp]:
paulson@14884
   426
  "h ` \<one> \<in> carrier(H)"
paulson@14884
   427
  by simp
paulson@14884
   428
paulson@14884
   429
lemma (in group_hom) hom_one [simp]:
paulson@14884
   430
  "h ` \<one> = \<one>\<^bsub>H\<^esub>"
paulson@14884
   431
proof -
paulson@14884
   432
  have "h ` \<one> \<cdot>\<^bsub>H\<^esub> \<one>\<^bsub>H\<^esub> = (h ` \<one>) \<cdot>\<^bsub>H\<^esub> (h ` \<one>)"
paulson@14884
   433
    by (simp add: hom_mult [symmetric] del: hom_mult)
paulson@14884
   434
  then show ?thesis by (simp del: r_one)
paulson@14884
   435
qed
paulson@14884
   436
paulson@14884
   437
lemma (in group_hom) inv_closed [simp]:
paulson@14884
   438
  "x \<in> carrier(G) \<Longrightarrow> h ` (inv x) \<in> carrier(H)"
paulson@14884
   439
  by simp
paulson@14884
   440
paulson@14884
   441
lemma (in group_hom) hom_inv [simp]:
paulson@14884
   442
  "x \<in> carrier(G) \<Longrightarrow> h ` (inv x) = inv\<^bsub>H\<^esub> (h ` x)"
paulson@14884
   443
proof -
paulson@14884
   444
  assume x: "x \<in> carrier(G)"
paulson@14884
   445
  then have "h ` x \<cdot>\<^bsub>H\<^esub> h ` (inv x) = \<one>\<^bsub>H\<^esub>"
paulson@14884
   446
    by (simp add: hom_mult [symmetric] G.r_inv del: hom_mult)
paulson@14884
   447
  also from x have "... = h ` x \<cdot>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h ` x)"
paulson@14884
   448
    by (simp add: hom_mult [symmetric] H.r_inv del: hom_mult)
paulson@14884
   449
  finally have "h ` x \<cdot>\<^bsub>H\<^esub> h ` (inv x) = h ` x \<cdot>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h ` x)" .
paulson@14884
   450
  with x show ?thesis by (simp del: inv add: is_group)
paulson@14884
   451
qed
paulson@14884
   452
paulson@14884
   453
subsection {* Commutative Structures *}
paulson@14884
   454
paulson@14884
   455
text {*
paulson@14884
   456
  Naming convention: multiplicative structures that are commutative
paulson@14884
   457
  are called \emph{commutative}, additive structures are called
paulson@14884
   458
  \emph{Abelian}.
paulson@14884
   459
*}
paulson@14884
   460
paulson@14884
   461
subsection {* Definition *}
paulson@14884
   462
paulson@14884
   463
locale comm_monoid = monoid +
paulson@14884
   464
  assumes m_comm: "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk> \<Longrightarrow> x \<cdot> y = y \<cdot> x"
paulson@14884
   465
paulson@14884
   466
lemma (in comm_monoid) m_lcomm:
paulson@14884
   467
  "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk> \<Longrightarrow>
paulson@14884
   468
   x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
paulson@14884
   469
proof -
paulson@14884
   470
  assume xyz: "x \<in> carrier(G)"  "y \<in> carrier(G)"  "z \<in> carrier(G)"
paulson@14884
   471
  from xyz have "x \<cdot> (y \<cdot> z) = (x \<cdot> y) \<cdot> z" by (simp add: m_assoc)
paulson@14884
   472
  also from xyz have "... = (y \<cdot> x) \<cdot> z" by (simp add: m_comm)
paulson@14884
   473
  also from xyz have "... = y \<cdot> (x \<cdot> z)" by (simp add: m_assoc)
paulson@14884
   474
  finally show ?thesis .
paulson@14884
   475
qed
paulson@14884
   476
paulson@14884
   477
lemmas (in comm_monoid) m_ac = m_assoc m_comm m_lcomm
paulson@14884
   478
paulson@14884
   479
locale comm_group = comm_monoid + group
paulson@14884
   480
paulson@14884
   481
lemma (in comm_group) inv_mult:
paulson@14884
   482
  "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk> \<Longrightarrow> inv (x \<cdot> y) = inv x \<cdot> inv y"
paulson@14884
   483
  by (simp add: m_ac inv_mult_group)
paulson@14884
   484
paulson@14884
   485
paulson@14884
   486
lemma (in group) subgroup_self: "subgroup (carrier(G),G)"
paulson@14884
   487
by (simp add: subgroup_def prems) 
paulson@14884
   488
paulson@14884
   489
lemma (in group) subgroup_imp_group:
paulson@14884
   490
  "subgroup(H,G) \<Longrightarrow> group (update_carrier(G,H))"
paulson@14891
   491
by (simp add: subgroup.is_group)
paulson@14884
   492
paulson@14884
   493
lemma (in group) subgroupI:
paulson@14884
   494
  assumes subset: "H \<subseteq> carrier(G)" and non_empty: "H \<noteq> 0"
paulson@14884
   495
    and inv: "!!a. a \<in> H ==> inv a \<in> H"
paulson@14884
   496
    and mult: "!!a b. [|a \<in> H; b \<in> H|] ==> a \<cdot> b \<in> H"
paulson@14884
   497
  shows "subgroup(H,G)"
paulson@14884
   498
proof (simp add: subgroup_def prems)
paulson@14884
   499
  show "\<one> \<in> H" by (rule one_in_subset) (auto simp only: prems)
paulson@14884
   500
qed
paulson@14884
   501
paulson@14884
   502
paulson@14884
   503
subsection {* Bijections of a Set, Permutation Groups, Automorphism Groups *}
paulson@14884
   504
wenzelm@21233
   505
definition
wenzelm@21404
   506
  BijGroup :: "i=>i" where
paulson@14884
   507
  "BijGroup(S) ==
paulson@14884
   508
    <bij(S,S),
paulson@14884
   509
     \<lambda><g,f> \<in> bij(S,S) \<times> bij(S,S). g O f,
paulson@14884
   510
     id(S), 0>"
paulson@14884
   511
paulson@14884
   512
paulson@14884
   513
subsection {*Bijections Form a Group *}
paulson@14884
   514
paulson@14884
   515
theorem group_BijGroup: "group(BijGroup(S))"
paulson@14884
   516
apply (simp add: BijGroup_def)
paulson@14884
   517
apply (rule groupI) 
paulson@14884
   518
    apply (simp_all add: id_bij comp_bij comp_assoc) 
paulson@14884
   519
 apply (simp add: id_bij bij_is_fun left_comp_id [of _ S S] fun_is_rel)
paulson@14884
   520
apply (blast intro: left_comp_inverse bij_is_inj bij_converse_bij)
paulson@14884
   521
done
paulson@14884
   522
paulson@14884
   523
paulson@14884
   524
subsection{*Automorphisms Form a Group*}
paulson@14884
   525
paulson@14884
   526
lemma Bij_Inv_mem: "\<lbrakk>f \<in> bij(S,S);  x \<in> S\<rbrakk> \<Longrightarrow> converse(f) ` x \<in> S" 
paulson@14884
   527
by (blast intro: apply_funtype bij_is_fun bij_converse_bij)
paulson@14884
   528
paulson@14884
   529
lemma inv_BijGroup: "f \<in> bij(S,S) \<Longrightarrow> m_inv (BijGroup(S), f) = converse(f)"
paulson@14884
   530
apply (rule group.inv_equality)
paulson@14884
   531
apply (rule group_BijGroup)
paulson@14884
   532
apply (simp_all add: BijGroup_def bij_converse_bij 
paulson@14884
   533
          left_comp_inverse [OF bij_is_inj]) 
paulson@14884
   534
done
paulson@14884
   535
paulson@14884
   536
lemma iso_is_bij: "h \<in> G \<cong> H ==> h \<in> bij(carrier(G), carrier(H))"
paulson@14884
   537
by (simp add: iso_def)
paulson@14884
   538
paulson@14884
   539
wenzelm@21233
   540
definition
wenzelm@21404
   541
  auto :: "i=>i" where
paulson@14884
   542
  "auto(G) == iso(G,G)"
paulson@14884
   543
wenzelm@21404
   544
definition
wenzelm@21404
   545
  AutoGroup :: "i=>i" where
paulson@14884
   546
  "AutoGroup(G) == update_carrier(BijGroup(carrier(G)), auto(G))"
paulson@14884
   547
paulson@14884
   548
paulson@14884
   549
lemma (in group) id_in_auto: "id(carrier(G)) \<in> auto(G)"
paulson@14884
   550
  by (simp add: iso_refl auto_def)
paulson@14884
   551
paulson@14884
   552
lemma (in group) subgroup_auto:
paulson@14884
   553
      "subgroup (auto(G)) (BijGroup (carrier(G)))"
paulson@14884
   554
proof (rule subgroup.intro)
paulson@14884
   555
  show "auto(G) \<subseteq> carrier (BijGroup (carrier(G)))"
paulson@14884
   556
    by (auto simp add: auto_def BijGroup_def iso_def)
paulson@14884
   557
next
paulson@14884
   558
  fix x y
paulson@14884
   559
  assume "x \<in> auto(G)" "y \<in> auto(G)" 
paulson@14884
   560
  thus "x \<cdot>\<^bsub>BijGroup (carrier(G))\<^esub> y \<in> auto(G)"
paulson@14884
   561
    by (auto simp add: BijGroup_def auto_def iso_def bij_is_fun 
paulson@14884
   562
                       group.hom_compose comp_bij)
paulson@14884
   563
next
paulson@14884
   564
  show "\<one>\<^bsub>BijGroup (carrier(G))\<^esub> \<in> auto(G)" by (simp add:  BijGroup_def id_in_auto)
paulson@14884
   565
next
paulson@14884
   566
  fix x 
paulson@14884
   567
  assume "x \<in> auto(G)" 
paulson@14884
   568
  thus "inv\<^bsub>BijGroup (carrier(G))\<^esub> x \<in> auto(G)"
paulson@14884
   569
    by (simp add: auto_def inv_BijGroup iso_is_bij iso_sym) 
paulson@14884
   570
qed
paulson@14884
   571
paulson@14884
   572
theorem (in group) AutoGroup: "group (AutoGroup(G))"
paulson@14891
   573
by (simp add: AutoGroup_def subgroup.is_group subgroup_auto group_BijGroup)
paulson@14884
   574
paulson@14884
   575
paulson@14884
   576
paulson@14884
   577
subsection{*Cosets and Quotient Groups*}
paulson@14884
   578
wenzelm@21233
   579
definition
wenzelm@21404
   580
  r_coset  :: "[i,i,i] => i"  (infixl "#>\<index>" 60) where
wenzelm@21233
   581
  "H #>\<^bsub>G\<^esub> a == \<Union>h\<in>H. {h \<cdot>\<^bsub>G\<^esub> a}"
paulson@14884
   582
wenzelm@21404
   583
definition
wenzelm@21404
   584
  l_coset  :: "[i,i,i] => i"  (infixl "<#\<index>" 60) where
wenzelm@21233
   585
  "a <#\<^bsub>G\<^esub> H == \<Union>h\<in>H. {a \<cdot>\<^bsub>G\<^esub> h}"
paulson@14884
   586
wenzelm@21404
   587
definition
wenzelm@21404
   588
  RCOSETS  :: "[i,i] => i"  ("rcosets\<index> _" [81] 80) where
wenzelm@21233
   589
  "rcosets\<^bsub>G\<^esub> H == \<Union>a\<in>carrier(G). {H #>\<^bsub>G\<^esub> a}"
paulson@14884
   590
wenzelm@21404
   591
definition
wenzelm@21404
   592
  set_mult :: "[i,i,i] => i"  (infixl "<#>\<index>" 60) where
wenzelm@21233
   593
  "H <#>\<^bsub>G\<^esub> K == \<Union>h\<in>H. \<Union>k\<in>K. {h \<cdot>\<^bsub>G\<^esub> k}"
paulson@14884
   594
wenzelm@21404
   595
definition
wenzelm@21404
   596
  SET_INV  :: "[i,i] => i"  ("set'_inv\<index> _" [81] 80) where
wenzelm@21233
   597
  "set_inv\<^bsub>G\<^esub> H == \<Union>h\<in>H. {inv\<^bsub>G\<^esub> h}"
paulson@14884
   598
paulson@14884
   599
paulson@14884
   600
locale normal = subgroup + group +
paulson@14884
   601
  assumes coset_eq: "(\<forall>x \<in> carrier(G). H #> x = x <# H)"
paulson@14884
   602
wenzelm@21233
   603
notation
wenzelm@21233
   604
  normal  (infixl "\<lhd>" 60)
paulson@14884
   605
paulson@14884
   606
paulson@14884
   607
subsection {*Basic Properties of Cosets*}
paulson@14884
   608
paulson@14884
   609
lemma (in group) coset_mult_assoc:
paulson@14884
   610
     "\<lbrakk>M \<subseteq> carrier(G); g \<in> carrier(G); h \<in> carrier(G)\<rbrakk>
paulson@14884
   611
      \<Longrightarrow> (M #> g) #> h = M #> (g \<cdot> h)"
paulson@14884
   612
by (force simp add: r_coset_def m_assoc)
paulson@14884
   613
paulson@14884
   614
lemma (in group) coset_mult_one [simp]: "M \<subseteq> carrier(G) \<Longrightarrow> M #> \<one> = M"
paulson@14884
   615
by (force simp add: r_coset_def)
paulson@14884
   616
paulson@14884
   617
lemma (in group) solve_equation:
paulson@14884
   618
    "\<lbrakk>subgroup(H,G); x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> \<exists>h\<in>H. y = h \<cdot> x"
paulson@14884
   619
apply (rule bexI [of _ "y \<cdot> (inv x)"])
paulson@14884
   620
apply (auto simp add: subgroup.m_closed subgroup.m_inv_closed m_assoc
paulson@14884
   621
                      subgroup.subset [THEN subsetD])
paulson@14884
   622
done
paulson@14884
   623
paulson@14884
   624
lemma (in group) repr_independence:
paulson@14884
   625
     "\<lbrakk>y \<in> H #> x;  x \<in> carrier(G); subgroup(H,G)\<rbrakk> \<Longrightarrow> H #> x = H #> y"
paulson@14884
   626
by (auto simp add: r_coset_def m_assoc [symmetric]
paulson@14884
   627
                   subgroup.subset [THEN subsetD]
paulson@14884
   628
                   subgroup.m_closed solve_equation)
paulson@14884
   629
paulson@14884
   630
lemma (in group) coset_join2:
paulson@14884
   631
     "\<lbrakk>x \<in> carrier(G);  subgroup(H,G);  x\<in>H\<rbrakk> \<Longrightarrow> H #> x = H"
paulson@14884
   632
  --{*Alternative proof is to put @{term "x=\<one>"} in @{text repr_independence}.*}
paulson@14884
   633
by (force simp add: subgroup.m_closed r_coset_def solve_equation)
paulson@14884
   634
paulson@14884
   635
lemma (in group) r_coset_subset_G:
paulson@14884
   636
     "\<lbrakk>H \<subseteq> carrier(G); x \<in> carrier(G)\<rbrakk> \<Longrightarrow> H #> x \<subseteq> carrier(G)"
paulson@14884
   637
by (auto simp add: r_coset_def)
paulson@14884
   638
paulson@14884
   639
lemma (in group) rcosI:
paulson@14884
   640
     "\<lbrakk>h \<in> H; H \<subseteq> carrier(G); x \<in> carrier(G)\<rbrakk> \<Longrightarrow> h \<cdot> x \<in> H #> x"
paulson@14884
   641
by (auto simp add: r_coset_def)
paulson@14884
   642
paulson@14884
   643
lemma (in group) rcosetsI:
paulson@14884
   644
     "\<lbrakk>H \<subseteq> carrier(G); x \<in> carrier(G)\<rbrakk> \<Longrightarrow> H #> x \<in> rcosets H"
paulson@14884
   645
by (auto simp add: RCOSETS_def)
paulson@14884
   646
paulson@14884
   647
paulson@14884
   648
text{*Really needed?*}
paulson@14884
   649
lemma (in group) transpose_inv:
paulson@14884
   650
     "\<lbrakk>x \<cdot> y = z;  x \<in> carrier(G);  y \<in> carrier(G);  z \<in> carrier(G)\<rbrakk>
paulson@14884
   651
      \<Longrightarrow> (inv x) \<cdot> z = y"
paulson@14884
   652
by (force simp add: m_assoc [symmetric])
paulson@14884
   653
paulson@14884
   654
paulson@14884
   655
paulson@14884
   656
subsection {* Normal subgroups *}
paulson@14884
   657
paulson@14884
   658
lemma normal_imp_subgroup: "H \<lhd> G ==> subgroup(H,G)"
paulson@14884
   659
  by (simp add: normal_def subgroup_def)
paulson@14884
   660
paulson@14884
   661
lemma (in group) normalI: 
paulson@14884
   662
  "subgroup(H,G) \<Longrightarrow> (\<forall>x \<in> carrier(G). H #> x = x <# H) \<Longrightarrow> H \<lhd> G";
ballarin@19931
   663
  by (simp add: normal_def normal_axioms_def)
paulson@14884
   664
paulson@14884
   665
lemma (in normal) inv_op_closed1:
paulson@14884
   666
     "\<lbrakk>x \<in> carrier(G); h \<in> H\<rbrakk> \<Longrightarrow> (inv x) \<cdot> h \<cdot> x \<in> H"
paulson@14884
   667
apply (insert coset_eq) 
paulson@14884
   668
apply (auto simp add: l_coset_def r_coset_def)
paulson@14884
   669
apply (drule bspec, assumption)
paulson@14884
   670
apply (drule equalityD1 [THEN subsetD], blast, clarify)
paulson@14884
   671
apply (simp add: m_assoc)
paulson@14884
   672
apply (simp add: m_assoc [symmetric])
paulson@14884
   673
done
paulson@14884
   674
paulson@14884
   675
lemma (in normal) inv_op_closed2:
paulson@14884
   676
     "\<lbrakk>x \<in> carrier(G); h \<in> H\<rbrakk> \<Longrightarrow> x \<cdot> h \<cdot> (inv x) \<in> H"
paulson@14884
   677
apply (subgoal_tac "inv (inv x) \<cdot> h \<cdot> (inv x) \<in> H") 
paulson@14884
   678
apply simp 
paulson@14884
   679
apply (blast intro: inv_op_closed1) 
paulson@14884
   680
done
paulson@14884
   681
paulson@14884
   682
text{*Alternative characterization of normal subgroups*}
paulson@14884
   683
lemma (in group) normal_inv_iff:
paulson@14884
   684
     "(N \<lhd> G) <->
paulson@14884
   685
      (subgroup(N,G) & (\<forall>x \<in> carrier(G). \<forall>h \<in> N. x \<cdot> h \<cdot> (inv x) \<in> N))"
paulson@14884
   686
      (is "_ <-> ?rhs")
paulson@14884
   687
proof
paulson@14884
   688
  assume N: "N \<lhd> G"
paulson@14884
   689
  show ?rhs
paulson@14884
   690
    by (blast intro: N normal.inv_op_closed2 normal_imp_subgroup) 
paulson@14884
   691
next
paulson@14884
   692
  assume ?rhs
paulson@14884
   693
  hence sg: "subgroup(N,G)" 
paulson@14884
   694
    and closed: "\<And>x. x\<in>carrier(G) \<Longrightarrow> \<forall>h\<in>N. x \<cdot> h \<cdot> inv x \<in> N" by auto
paulson@14884
   695
  hence sb: "N \<subseteq> carrier(G)" by (simp add: subgroup.subset) 
paulson@14884
   696
  show "N \<lhd> G"
paulson@14884
   697
  proof (intro normalI [OF sg], simp add: l_coset_def r_coset_def, clarify)
paulson@14884
   698
    fix x
paulson@14884
   699
    assume x: "x \<in> carrier(G)"
paulson@14884
   700
    show "(\<Union>h\<in>N. {h \<cdot> x}) = (\<Union>h\<in>N. {x \<cdot> h})"
paulson@14884
   701
    proof
paulson@14884
   702
      show "(\<Union>h\<in>N. {h \<cdot> x}) \<subseteq> (\<Union>h\<in>N. {x \<cdot> h})"
paulson@14884
   703
      proof clarify
paulson@14884
   704
        fix n
paulson@14884
   705
        assume n: "n \<in> N" 
paulson@14884
   706
        show "n \<cdot> x \<in> (\<Union>h\<in>N. {x \<cdot> h})"
paulson@14884
   707
        proof (rule UN_I) 
paulson@14884
   708
          from closed [of "inv x"]
paulson@14884
   709
          show "inv x \<cdot> n \<cdot> x \<in> N" by (simp add: x n)
paulson@14884
   710
          show "n \<cdot> x \<in> {x \<cdot> (inv x \<cdot> n \<cdot> x)}"
paulson@14884
   711
            by (simp add: x n m_assoc [symmetric] sb [THEN subsetD])
paulson@14884
   712
        qed
paulson@14884
   713
      qed
paulson@14884
   714
    next
paulson@14884
   715
      show "(\<Union>h\<in>N. {x \<cdot> h}) \<subseteq> (\<Union>h\<in>N. {h \<cdot> x})"
paulson@14884
   716
      proof clarify
paulson@14884
   717
        fix n
paulson@14884
   718
        assume n: "n \<in> N" 
paulson@14884
   719
        show "x \<cdot> n \<in> (\<Union>h\<in>N. {h \<cdot> x})"
paulson@14884
   720
        proof (rule UN_I) 
paulson@14884
   721
          show "x \<cdot> n \<cdot> inv x \<in> N" by (simp add: x n closed)
paulson@14884
   722
          show "x \<cdot> n \<in> {x \<cdot> n \<cdot> inv x \<cdot> x}"
paulson@14884
   723
            by (simp add: x n m_assoc sb [THEN subsetD])
paulson@14884
   724
        qed
paulson@14884
   725
      qed
paulson@14884
   726
    qed
paulson@14884
   727
  qed
paulson@14884
   728
qed
paulson@14884
   729
paulson@14884
   730
paulson@14884
   731
subsection{*More Properties of Cosets*}
paulson@14884
   732
paulson@14884
   733
lemma (in group) l_coset_subset_G:
paulson@14884
   734
     "\<lbrakk>H \<subseteq> carrier(G); x \<in> carrier(G)\<rbrakk> \<Longrightarrow> x <# H \<subseteq> carrier(G)"
paulson@14884
   735
by (auto simp add: l_coset_def subsetD)
paulson@14884
   736
paulson@14884
   737
lemma (in group) l_coset_swap:
paulson@14884
   738
     "\<lbrakk>y \<in> x <# H;  x \<in> carrier(G);  subgroup(H,G)\<rbrakk> \<Longrightarrow> x \<in> y <# H"
paulson@14884
   739
proof (simp add: l_coset_def)
paulson@14884
   740
  assume "\<exists>h\<in>H. y = x \<cdot> h"
paulson@14884
   741
    and x: "x \<in> carrier(G)"
paulson@14884
   742
    and sb: "subgroup(H,G)"
paulson@14884
   743
  then obtain h' where h': "h' \<in> H & x \<cdot> h' = y" by blast
paulson@14884
   744
  show "\<exists>h\<in>H. x = y \<cdot> h"
paulson@14884
   745
  proof
paulson@14884
   746
    show "x = y \<cdot> inv h'" using h' x sb
paulson@14884
   747
      by (auto simp add: m_assoc subgroup.subset [THEN subsetD])
paulson@14884
   748
    show "inv h' \<in> H" using h' sb
paulson@14884
   749
      by (auto simp add: subgroup.subset [THEN subsetD] subgroup.m_inv_closed)
paulson@14884
   750
  qed
paulson@14884
   751
qed
paulson@14884
   752
paulson@14884
   753
lemma (in group) l_coset_carrier:
paulson@14884
   754
     "\<lbrakk>y \<in> x <# H;  x \<in> carrier(G);  subgroup(H,G)\<rbrakk> \<Longrightarrow> y \<in> carrier(G)"
paulson@14884
   755
by (auto simp add: l_coset_def m_assoc
paulson@14884
   756
                   subgroup.subset [THEN subsetD] subgroup.m_closed)
paulson@14884
   757
paulson@14884
   758
lemma (in group) l_repr_imp_subset:
paulson@14884
   759
  assumes y: "y \<in> x <# H" and x: "x \<in> carrier(G)" and sb: "subgroup(H,G)"
paulson@14884
   760
  shows "y <# H \<subseteq> x <# H"
paulson@14884
   761
proof -
paulson@14884
   762
  from y
paulson@14884
   763
  obtain h' where "h' \<in> H" "x \<cdot> h' = y" by (auto simp add: l_coset_def)
paulson@14884
   764
  thus ?thesis using x sb
paulson@14884
   765
    by (auto simp add: l_coset_def m_assoc
paulson@14884
   766
                       subgroup.subset [THEN subsetD] subgroup.m_closed)
paulson@14884
   767
qed
paulson@14884
   768
paulson@14884
   769
lemma (in group) l_repr_independence:
paulson@14884
   770
  assumes y: "y \<in> x <# H" and x: "x \<in> carrier(G)" and sb: "subgroup(H,G)"
paulson@14884
   771
  shows "x <# H = y <# H"
paulson@14884
   772
proof
paulson@14884
   773
  show "x <# H \<subseteq> y <# H"
paulson@14884
   774
    by (rule l_repr_imp_subset,
paulson@14884
   775
        (blast intro: l_coset_swap l_coset_carrier y x sb)+)
paulson@14884
   776
  show "y <# H \<subseteq> x <# H" by (rule l_repr_imp_subset [OF y x sb])
paulson@14884
   777
qed
paulson@14884
   778
paulson@14884
   779
lemma (in group) setmult_subset_G:
paulson@14884
   780
     "\<lbrakk>H \<subseteq> carrier(G); K \<subseteq> carrier(G)\<rbrakk> \<Longrightarrow> H <#> K \<subseteq> carrier(G)"
paulson@14884
   781
by (auto simp add: set_mult_def subsetD)
paulson@14884
   782
paulson@14884
   783
lemma (in group) subgroup_mult_id: "subgroup(H,G) \<Longrightarrow> H <#> H = H"
paulson@14884
   784
apply (rule equalityI) 
paulson@14884
   785
apply (auto simp add: subgroup.m_closed set_mult_def Sigma_def image_def)
paulson@14884
   786
apply (rule_tac x = x in bexI)
paulson@14884
   787
apply (rule bexI [of _ "\<one>"])
paulson@14884
   788
apply (auto simp add: subgroup.m_closed subgroup.one_closed
paulson@14884
   789
                      r_one subgroup.subset [THEN subsetD])
paulson@14884
   790
done
paulson@14884
   791
paulson@14884
   792
paulson@14884
   793
subsubsection {* Set of inverses of an @{text r_coset}. *}
paulson@14884
   794
paulson@14884
   795
lemma (in normal) rcos_inv:
paulson@14884
   796
  assumes x:     "x \<in> carrier(G)"
paulson@14884
   797
  shows "set_inv (H #> x) = H #> (inv x)" 
paulson@14884
   798
proof (simp add: r_coset_def SET_INV_def x inv_mult_group, safe intro!: equalityI)
paulson@14884
   799
  fix h
paulson@14884
   800
  assume "h \<in> H"
paulson@14884
   801
  show "inv x \<cdot> inv h \<in> (\<Union>j\<in>H. {j \<cdot> inv x})"
paulson@14884
   802
  proof (rule UN_I)
paulson@14884
   803
    show "inv x \<cdot> inv h \<cdot> x \<in> H"
paulson@14884
   804
      by (simp add: inv_op_closed1 prems)
paulson@14884
   805
    show "inv x \<cdot> inv h \<in> {inv x \<cdot> inv h \<cdot> x \<cdot> inv x}"
paulson@14884
   806
      by (simp add: prems m_assoc)
paulson@14884
   807
  qed
paulson@14884
   808
next
paulson@14884
   809
  fix h
paulson@14884
   810
  assume "h \<in> H"
paulson@14884
   811
  show "h \<cdot> inv x \<in> (\<Union>j\<in>H. {inv x \<cdot> inv j})"
paulson@14884
   812
  proof (rule UN_I)
paulson@14884
   813
    show "x \<cdot> inv h \<cdot> inv x \<in> H"
paulson@14884
   814
      by (simp add: inv_op_closed2 prems)
paulson@14884
   815
    show "h \<cdot> inv x \<in> {inv x \<cdot> inv (x \<cdot> inv h \<cdot> inv x)}"
paulson@14884
   816
      by (simp add: prems m_assoc [symmetric] inv_mult_group)
paulson@14884
   817
  qed
paulson@14884
   818
qed
paulson@14884
   819
paulson@14884
   820
paulson@14884
   821
paulson@14884
   822
subsubsection {*Theorems for @{text "<#>"} with @{text "#>"} or @{text "<#"}.*}
paulson@14884
   823
paulson@14884
   824
lemma (in group) setmult_rcos_assoc:
paulson@14884
   825
     "\<lbrakk>H \<subseteq> carrier(G); K \<subseteq> carrier(G); x \<in> carrier(G)\<rbrakk>
paulson@14884
   826
      \<Longrightarrow> H <#> (K #> x) = (H <#> K) #> x"
paulson@14884
   827
by (force simp add: r_coset_def set_mult_def m_assoc)
paulson@14884
   828
paulson@14884
   829
lemma (in group) rcos_assoc_lcos:
paulson@14884
   830
     "\<lbrakk>H \<subseteq> carrier(G); K \<subseteq> carrier(G); x \<in> carrier(G)\<rbrakk>
paulson@14884
   831
      \<Longrightarrow> (H #> x) <#> K = H <#> (x <# K)"
paulson@14884
   832
by (force simp add: r_coset_def l_coset_def set_mult_def m_assoc)
paulson@14884
   833
paulson@14884
   834
lemma (in normal) rcos_mult_step1:
paulson@14884
   835
     "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk>
paulson@14884
   836
      \<Longrightarrow> (H #> x) <#> (H #> y) = (H <#> (x <# H)) #> y"
paulson@14884
   837
by (simp add: setmult_rcos_assoc subset
paulson@14884
   838
              r_coset_subset_G l_coset_subset_G rcos_assoc_lcos)
paulson@14884
   839
paulson@14884
   840
lemma (in normal) rcos_mult_step2:
paulson@14884
   841
     "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk>
paulson@14884
   842
      \<Longrightarrow> (H <#> (x <# H)) #> y = (H <#> (H #> x)) #> y"
paulson@14884
   843
by (insert coset_eq, simp add: normal_def)
paulson@14884
   844
paulson@14884
   845
lemma (in normal) rcos_mult_step3:
paulson@14884
   846
     "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk>
paulson@14884
   847
      \<Longrightarrow> (H <#> (H #> x)) #> y = H #> (x \<cdot> y)"
ballarin@19931
   848
  by (simp add: setmult_rcos_assoc coset_mult_assoc
ballarin@19931
   849
              subgroup_mult_id subset prems normal.axioms)
paulson@14884
   850
paulson@14884
   851
lemma (in normal) rcos_sum:
paulson@14884
   852
     "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk>
paulson@14884
   853
      \<Longrightarrow> (H #> x) <#> (H #> y) = H #> (x \<cdot> y)"
paulson@14884
   854
by (simp add: rcos_mult_step1 rcos_mult_step2 rcos_mult_step3)
paulson@14884
   855
paulson@14884
   856
lemma (in normal) rcosets_mult_eq: "M \<in> rcosets H \<Longrightarrow> H <#> M = M"
paulson@14884
   857
  -- {* generalizes @{text subgroup_mult_id} *}
paulson@14884
   858
  by (auto simp add: RCOSETS_def subset
ballarin@19931
   859
        setmult_rcos_assoc subgroup_mult_id prems normal.axioms)
paulson@14884
   860
paulson@14884
   861
paulson@14884
   862
subsubsection{*Two distinct right cosets are disjoint*}
paulson@14884
   863
wenzelm@21233
   864
definition
wenzelm@21404
   865
  r_congruent :: "[i,i] => i" ("rcong\<index> _" [60] 60) where
wenzelm@21233
   866
  "rcong\<^bsub>G\<^esub> H == {<x,y> \<in> carrier(G) * carrier(G). inv\<^bsub>G\<^esub> x \<cdot>\<^bsub>G\<^esub> y \<in> H}"
paulson@14884
   867
paulson@14884
   868
paulson@14884
   869
lemma (in subgroup) equiv_rcong:
ballarin@27618
   870
   assumes "group(G)"
paulson@14884
   871
   shows "equiv (carrier(G), rcong H)"
ballarin@27618
   872
proof -
ballarin@29223
   873
  interpret group G by fact
ballarin@27618
   874
  show ?thesis proof (simp add: equiv_def, intro conjI)
ballarin@27618
   875
    show "rcong H \<subseteq> carrier(G) \<times> carrier(G)"
ballarin@27618
   876
      by (auto simp add: r_congruent_def) 
ballarin@27618
   877
  next
ballarin@27618
   878
    show "refl (carrier(G), rcong H)"
ballarin@27618
   879
      by (auto simp add: r_congruent_def refl_def) 
ballarin@27618
   880
  next
ballarin@27618
   881
    show "sym (rcong H)"
ballarin@27618
   882
    proof (simp add: r_congruent_def sym_def, clarify)
ballarin@27618
   883
      fix x y
ballarin@27618
   884
      assume [simp]: "x \<in> carrier(G)" "y \<in> carrier(G)" 
ballarin@27618
   885
	and "inv x \<cdot> y \<in> H"
ballarin@27618
   886
      hence "inv (inv x \<cdot> y) \<in> H" by (simp add: m_inv_closed) 
ballarin@27618
   887
      thus "inv y \<cdot> x \<in> H" by (simp add: inv_mult_group)
ballarin@27618
   888
    qed
ballarin@27618
   889
  next
ballarin@27618
   890
    show "trans (rcong H)"
ballarin@27618
   891
    proof (simp add: r_congruent_def trans_def, clarify)
ballarin@27618
   892
      fix x y z
ballarin@27618
   893
      assume [simp]: "x \<in> carrier(G)" "y \<in> carrier(G)" "z \<in> carrier(G)"
ballarin@27618
   894
	and "inv x \<cdot> y \<in> H" and "inv y \<cdot> z \<in> H"
ballarin@27618
   895
      hence "(inv x \<cdot> y) \<cdot> (inv y \<cdot> z) \<in> H" by simp
ballarin@27618
   896
      hence "inv x \<cdot> (y \<cdot> inv y) \<cdot> z \<in> H" by (simp add: m_assoc del: inv) 
ballarin@27618
   897
      thus "inv x \<cdot> z \<in> H" by simp
ballarin@27618
   898
    qed
paulson@14884
   899
  qed
paulson@14884
   900
qed
paulson@14884
   901
paulson@14884
   902
text{*Equivalence classes of @{text rcong} correspond to left cosets.
paulson@14884
   903
  Was there a mistake in the definitions? I'd have expected them to
paulson@14884
   904
  correspond to right cosets.*}
paulson@14884
   905
lemma (in subgroup) l_coset_eq_rcong:
ballarin@27618
   906
  assumes "group(G)"
paulson@14884
   907
  assumes a: "a \<in> carrier(G)"
paulson@14884
   908
  shows "a <# H = (rcong H) `` {a}" 
ballarin@27618
   909
proof -
ballarin@29223
   910
  interpret group G by fact
ballarin@27618
   911
  show ?thesis
ballarin@27618
   912
    by (force simp add: r_congruent_def l_coset_def m_assoc [symmetric] a
ballarin@27618
   913
      Collect_image_eq) 
ballarin@27618
   914
qed
paulson@14884
   915
paulson@14884
   916
lemma (in group) rcos_equation:
ballarin@27618
   917
  assumes "subgroup(H, G)"
paulson@14884
   918
  shows
paulson@14884
   919
     "\<lbrakk>ha \<cdot> a = h \<cdot> b; a \<in> carrier(G);  b \<in> carrier(G);  
paulson@14884
   920
        h \<in> H;  ha \<in> H;  hb \<in> H\<rbrakk>
ballarin@27618
   921
      \<Longrightarrow> hb \<cdot> a \<in> (\<Union>h\<in>H. {h \<cdot> b})" (is "PROP ?P")
ballarin@27618
   922
proof -
ballarin@29223
   923
  interpret subgroup H G by fact
ballarin@27618
   924
  show "PROP ?P"
ballarin@27618
   925
    apply (rule UN_I [of "hb \<cdot> ((inv ha) \<cdot> h)"], simp)
ballarin@27618
   926
    apply (simp add: m_assoc transpose_inv)
ballarin@27618
   927
    done
ballarin@27618
   928
qed
paulson@14884
   929
paulson@14884
   930
lemma (in group) rcos_disjoint:
ballarin@27618
   931
  assumes "subgroup(H, G)"
ballarin@27618
   932
  shows "\<lbrakk>a \<in> rcosets H; b \<in> rcosets H; a\<noteq>b\<rbrakk> \<Longrightarrow> a \<inter> b = 0" (is "PROP ?P")
ballarin@27618
   933
proof -
ballarin@29223
   934
  interpret subgroup H G by fact
ballarin@27618
   935
  show "PROP ?P"
ballarin@27618
   936
    apply (simp add: RCOSETS_def r_coset_def)
ballarin@27618
   937
    apply (blast intro: rcos_equation prems sym)
ballarin@27618
   938
    done
ballarin@27618
   939
qed
paulson@14884
   940
paulson@14884
   941
paulson@14884
   942
subsection {*Order of a Group and Lagrange's Theorem*}
paulson@14884
   943
wenzelm@21233
   944
definition
wenzelm@21404
   945
  order :: "i => i" where
paulson@14884
   946
  "order(S) == |carrier(S)|"
paulson@14884
   947
paulson@14884
   948
lemma (in group) rcos_self:
ballarin@27618
   949
  assumes "subgroup(H, G)"
ballarin@27618
   950
  shows "x \<in> carrier(G) \<Longrightarrow> x \<in> H #> x" (is "PROP ?P")
ballarin@27618
   951
proof -
ballarin@29223
   952
  interpret subgroup H G by fact
ballarin@27618
   953
  show "PROP ?P"
ballarin@27618
   954
    apply (simp add: r_coset_def)
ballarin@27618
   955
    apply (rule_tac x="\<one>" in bexI) apply (auto)
ballarin@27618
   956
    done
ballarin@27618
   957
qed
paulson@14884
   958
paulson@14884
   959
lemma (in group) rcosets_part_G:
ballarin@27618
   960
  assumes "subgroup(H, G)"
paulson@14884
   961
  shows "\<Union>(rcosets H) = carrier(G)"
ballarin@27618
   962
proof -
ballarin@29223
   963
  interpret subgroup H G by fact
ballarin@27618
   964
  show ?thesis
ballarin@27618
   965
    apply (rule equalityI)
ballarin@27618
   966
    apply (force simp add: RCOSETS_def r_coset_def)
ballarin@27618
   967
    apply (auto simp add: RCOSETS_def intro: rcos_self prems)
ballarin@27618
   968
    done
ballarin@27618
   969
qed
paulson@14884
   970
paulson@14884
   971
lemma (in group) cosets_finite:
paulson@14884
   972
     "\<lbrakk>c \<in> rcosets H;  H \<subseteq> carrier(G);  Finite (carrier(G))\<rbrakk> \<Longrightarrow> Finite(c)"
paulson@14884
   973
apply (auto simp add: RCOSETS_def)
paulson@14884
   974
apply (simp add: r_coset_subset_G [THEN subset_Finite])
paulson@14884
   975
done
paulson@14884
   976
paulson@14884
   977
text{*More general than the HOL version, which also requires @{term G} to
paulson@14884
   978
      be finite.*}
paulson@14884
   979
lemma (in group) card_cosets_equal:
paulson@14884
   980
  assumes H:   "H \<subseteq> carrier(G)"
paulson@14884
   981
  shows "c \<in> rcosets H \<Longrightarrow> |c| = |H|"
paulson@14884
   982
proof (simp add: RCOSETS_def, clarify)
paulson@14884
   983
  fix a
paulson@14884
   984
  assume a: "a \<in> carrier(G)"
paulson@14884
   985
  show "|H #> a| = |H|"
paulson@14884
   986
  proof (rule eqpollI [THEN cardinal_cong])
paulson@14884
   987
    show "H #> a \<lesssim> H"
paulson@14884
   988
    proof (simp add: lepoll_def, intro exI) 
paulson@14884
   989
      show "(\<lambda>y \<in> H#>a. y \<cdot> inv a) \<in> inj(H #> a, H)"
paulson@14884
   990
        by (auto intro: lam_type 
paulson@14884
   991
                 simp add: inj_def r_coset_def m_assoc subsetD [OF H] a)
paulson@14884
   992
    qed
paulson@14884
   993
    show "H \<lesssim> H #> a"
paulson@14884
   994
    proof (simp add: lepoll_def, intro exI) 
paulson@14884
   995
      show "(\<lambda>y\<in> H. y \<cdot> a) \<in> inj(H, H #> a)"
paulson@14884
   996
        by (auto intro: lam_type 
paulson@14884
   997
                 simp add: inj_def r_coset_def  subsetD [OF H] a)
paulson@14884
   998
    qed
paulson@14884
   999
  qed
paulson@14884
  1000
qed
paulson@14884
  1001
paulson@14884
  1002
paulson@14884
  1003
lemma (in group) rcosets_subset_PowG:
paulson@14884
  1004
     "subgroup(H,G) \<Longrightarrow> rcosets H \<subseteq> Pow(carrier(G))"
paulson@14884
  1005
apply (simp add: RCOSETS_def)
paulson@14884
  1006
apply (blast dest: r_coset_subset_G subgroup.subset)
paulson@14884
  1007
done
paulson@14884
  1008
paulson@14884
  1009
theorem (in group) lagrange:
paulson@14884
  1010
     "\<lbrakk>Finite(carrier(G)); subgroup(H,G)\<rbrakk>
paulson@14884
  1011
      \<Longrightarrow> |rcosets H| #* |H| = order(G)"
paulson@14884
  1012
apply (simp (no_asm_simp) add: order_def rcosets_part_G [symmetric])
paulson@14884
  1013
apply (subst mult_commute)
paulson@14884
  1014
apply (rule card_partition)
paulson@14884
  1015
   apply (simp add: rcosets_subset_PowG [THEN subset_Finite])
paulson@14884
  1016
  apply (simp add: rcosets_part_G)
paulson@14884
  1017
 apply (simp add: card_cosets_equal [OF subgroup.subset])
paulson@14884
  1018
apply (simp add: rcos_disjoint)
paulson@14884
  1019
done
paulson@14884
  1020
paulson@14884
  1021
paulson@14884
  1022
subsection {*Quotient Groups: Factorization of a Group*}
paulson@14884
  1023
wenzelm@21233
  1024
definition
wenzelm@21404
  1025
  FactGroup :: "[i,i] => i" (infixl "Mod" 65) where
paulson@14884
  1026
    --{*Actually defined for groups rather than monoids*}
paulson@14884
  1027
  "G Mod H == 
wenzelm@21233
  1028
     <rcosets\<^bsub>G\<^esub> H, \<lambda><K1,K2> \<in> (rcosets\<^bsub>G\<^esub> H) \<times> (rcosets\<^bsub>G\<^esub> H). K1 <#>\<^bsub>G\<^esub> K2, H, 0>"
paulson@14884
  1029
paulson@14884
  1030
lemma (in normal) setmult_closed:
paulson@14884
  1031
     "\<lbrakk>K1 \<in> rcosets H; K2 \<in> rcosets H\<rbrakk> \<Longrightarrow> K1 <#> K2 \<in> rcosets H"
paulson@14884
  1032
by (auto simp add: rcos_sum RCOSETS_def)
paulson@14884
  1033
paulson@14884
  1034
lemma (in normal) setinv_closed:
paulson@14884
  1035
     "K \<in> rcosets H \<Longrightarrow> set_inv K \<in> rcosets H"
paulson@14884
  1036
by (auto simp add: rcos_inv RCOSETS_def)
paulson@14884
  1037
paulson@14884
  1038
lemma (in normal) rcosets_assoc:
paulson@14884
  1039
     "\<lbrakk>M1 \<in> rcosets H; M2 \<in> rcosets H; M3 \<in> rcosets H\<rbrakk>
paulson@14884
  1040
      \<Longrightarrow> M1 <#> M2 <#> M3 = M1 <#> (M2 <#> M3)"
paulson@14884
  1041
by (auto simp add: RCOSETS_def rcos_sum m_assoc)
paulson@14884
  1042
paulson@14884
  1043
lemma (in subgroup) subgroup_in_rcosets:
ballarin@27618
  1044
  assumes "group(G)"
paulson@14884
  1045
  shows "H \<in> rcosets H"
paulson@14884
  1046
proof -
ballarin@29223
  1047
  interpret group G by fact
paulson@14884
  1048
  have "H #> \<one> = H"
wenzelm@26199
  1049
    using _ subgroup_axioms by (rule coset_join2) simp_all
paulson@14884
  1050
  then show ?thesis
paulson@14884
  1051
    by (auto simp add: RCOSETS_def intro: sym)
paulson@14884
  1052
qed
paulson@14884
  1053
paulson@14884
  1054
lemma (in normal) rcosets_inv_mult_group_eq:
paulson@14884
  1055
     "M \<in> rcosets H \<Longrightarrow> set_inv M <#> M = H"
ballarin@19931
  1056
by (auto simp add: RCOSETS_def rcos_inv rcos_sum subgroup.subset prems normal.axioms)
paulson@14884
  1057
paulson@14884
  1058
theorem (in normal) factorgroup_is_group:
paulson@14884
  1059
  "group (G Mod H)"
paulson@14884
  1060
apply (simp add: FactGroup_def)
paulson@14891
  1061
apply (rule groupI)
paulson@14884
  1062
    apply (simp add: setmult_closed)
paulson@14884
  1063
   apply (simp add: normal_imp_subgroup subgroup_in_rcosets)
paulson@14884
  1064
  apply (simp add: setmult_closed rcosets_assoc)
paulson@14884
  1065
 apply (simp add: normal_imp_subgroup
paulson@14884
  1066
                  subgroup_in_rcosets rcosets_mult_eq)
paulson@14884
  1067
apply (auto dest: rcosets_inv_mult_group_eq simp add: setinv_closed)
paulson@14884
  1068
done
paulson@14884
  1069
paulson@14884
  1070
lemma (in normal) inv_FactGroup:
paulson@14884
  1071
     "X \<in> carrier (G Mod H) \<Longrightarrow> inv\<^bsub>G Mod H\<^esub> X = set_inv X"
paulson@14884
  1072
apply (rule group.inv_equality [OF factorgroup_is_group]) 
paulson@14884
  1073
apply (simp_all add: FactGroup_def setinv_closed rcosets_inv_mult_group_eq)
paulson@14884
  1074
done
paulson@14884
  1075
paulson@14884
  1076
text{*The coset map is a homomorphism from @{term G} to the quotient group
paulson@14884
  1077
  @{term "G Mod H"}*}
paulson@14884
  1078
lemma (in normal) r_coset_hom_Mod:
paulson@14884
  1079
  "(\<lambda>a \<in> carrier(G). H #> a) \<in> hom(G, G Mod H)"
paulson@14884
  1080
by (auto simp add: FactGroup_def RCOSETS_def hom_def rcos_sum intro: lam_type) 
paulson@14884
  1081
paulson@14884
  1082
paulson@14891
  1083
subsection{*The First Isomorphism Theorem*}
paulson@14891
  1084
paulson@14891
  1085
text{*The quotient by the kernel of a homomorphism is isomorphic to the 
paulson@14891
  1086
  range of that homomorphism.*}
paulson@14884
  1087
wenzelm@21233
  1088
definition
wenzelm@21404
  1089
  kernel :: "[i,i,i] => i" where
paulson@14884
  1090
    --{*the kernel of a homomorphism*}
paulson@14884
  1091
  "kernel(G,H,h) == {x \<in> carrier(G). h ` x = \<one>\<^bsub>H\<^esub>}";
paulson@14884
  1092
paulson@14884
  1093
lemma (in group_hom) subgroup_kernel: "subgroup (kernel(G,H,h), G)"
paulson@14884
  1094
apply (rule subgroup.intro) 
paulson@14884
  1095
apply (auto simp add: kernel_def group.intro prems) 
paulson@14884
  1096
done
paulson@14884
  1097
paulson@14884
  1098
text{*The kernel of a homomorphism is a normal subgroup*}
paulson@14884
  1099
lemma (in group_hom) normal_kernel: "(kernel(G,H,h)) \<lhd> G"
paulson@14884
  1100
apply (simp add: group.normal_inv_iff subgroup_kernel group.intro prems)
paulson@14884
  1101
apply (simp add: kernel_def)  
paulson@14884
  1102
done
paulson@14884
  1103
paulson@14884
  1104
lemma (in group_hom) FactGroup_nonempty:
paulson@14884
  1105
  assumes X: "X \<in> carrier (G Mod kernel(G,H,h))"
paulson@14884
  1106
  shows "X \<noteq> 0"
paulson@14884
  1107
proof -
paulson@14884
  1108
  from X
paulson@14884
  1109
  obtain g where "g \<in> carrier(G)" 
paulson@14884
  1110
             and "X = kernel(G,H,h) #> g"
paulson@14884
  1111
    by (auto simp add: FactGroup_def RCOSETS_def)
paulson@14884
  1112
  thus ?thesis 
paulson@14884
  1113
   by (auto simp add: kernel_def r_coset_def image_def intro: hom_one)
paulson@14884
  1114
qed
paulson@14884
  1115
paulson@14884
  1116
paulson@14884
  1117
lemma (in group_hom) FactGroup_contents_mem:
paulson@14884
  1118
  assumes X: "X \<in> carrier (G Mod (kernel(G,H,h)))"
paulson@14884
  1119
  shows "contents (h``X) \<in> carrier(H)"
paulson@14884
  1120
proof -
paulson@14884
  1121
  from X
paulson@14884
  1122
  obtain g where g: "g \<in> carrier(G)" 
paulson@14884
  1123
             and "X = kernel(G,H,h) #> g"
paulson@14884
  1124
    by (auto simp add: FactGroup_def RCOSETS_def)
paulson@14884
  1125
  hence "h `` X = {h ` g}"
paulson@14884
  1126
    by (auto simp add: kernel_def r_coset_def image_UN 
paulson@14884
  1127
                       image_eq_UN [OF hom_is_fun] g)
paulson@14884
  1128
  thus ?thesis by (auto simp add: g)
paulson@14884
  1129
qed
paulson@14884
  1130
paulson@14884
  1131
lemma mult_FactGroup:
paulson@14884
  1132
     "[|X \<in> carrier(G Mod H); X' \<in> carrier(G Mod H)|] 
paulson@14884
  1133
      ==> X \<cdot>\<^bsub>(G Mod H)\<^esub> X' = X <#>\<^bsub>G\<^esub> X'"
paulson@14884
  1134
by (simp add: FactGroup_def) 
paulson@14884
  1135
paulson@14884
  1136
lemma (in normal) FactGroup_m_closed:
paulson@14884
  1137
     "[|X \<in> carrier(G Mod H); X' \<in> carrier(G Mod H)|] 
paulson@14884
  1138
      ==> X <#>\<^bsub>G\<^esub> X' \<in> carrier(G Mod H)"
paulson@14884
  1139
by (simp add: FactGroup_def setmult_closed) 
paulson@14884
  1140
paulson@14884
  1141
lemma (in group_hom) FactGroup_hom:
paulson@14884
  1142
     "(\<lambda>X \<in> carrier(G Mod (kernel(G,H,h))). contents (h``X))
paulson@14884
  1143
      \<in> hom (G Mod (kernel(G,H,h)), H)" 
paulson@14884
  1144
proof (simp add: hom_def FactGroup_contents_mem lam_type mult_FactGroup normal.FactGroup_m_closed [OF normal_kernel], intro ballI)  
paulson@14884
  1145
  fix X and X'
paulson@14884
  1146
  assume X:  "X  \<in> carrier (G Mod kernel(G,H,h))"
paulson@14884
  1147
     and X': "X' \<in> carrier (G Mod kernel(G,H,h))"
paulson@14884
  1148
  then
paulson@14884
  1149
  obtain g and g'
paulson@14884
  1150
           where "g \<in> carrier(G)" and "g' \<in> carrier(G)" 
paulson@14884
  1151
             and "X = kernel(G,H,h) #> g" and "X' = kernel(G,H,h) #> g'"
paulson@14884
  1152
    by (auto simp add: FactGroup_def RCOSETS_def)
paulson@14884
  1153
  hence all: "\<forall>x\<in>X. h ` x = h ` g" "\<forall>x\<in>X'. h ` x = h ` g'" 
paulson@14884
  1154
    and Xsub: "X \<subseteq> carrier(G)" and X'sub: "X' \<subseteq> carrier(G)"
paulson@14884
  1155
    by (force simp add: kernel_def r_coset_def image_def)+
paulson@14884
  1156
  hence "h `` (X <#> X') = {h ` g \<cdot>\<^bsub>H\<^esub> h ` g'}" using X X'
paulson@14884
  1157
    by (auto dest!: FactGroup_nonempty
paulson@14884
  1158
             simp add: set_mult_def image_eq_UN [OF hom_is_fun] image_UN
paulson@14884
  1159
                       subsetD [OF Xsub] subsetD [OF X'sub]) 
paulson@14884
  1160
  thus "contents (h `` (X <#> X')) = contents (h `` X) \<cdot>\<^bsub>H\<^esub> contents (h `` X')"
paulson@14884
  1161
    by (simp add: all image_eq_UN [OF hom_is_fun] FactGroup_nonempty 
paulson@14884
  1162
                  X X' Xsub X'sub)
paulson@14884
  1163
qed
paulson@14884
  1164
paulson@14884
  1165
paulson@14884
  1166
text{*Lemma for the following injectivity result*}
paulson@14884
  1167
lemma (in group_hom) FactGroup_subset:
paulson@14884
  1168
     "\<lbrakk>g \<in> carrier(G); g' \<in> carrier(G); h ` g = h ` g'\<rbrakk>
paulson@14884
  1169
      \<Longrightarrow>  kernel(G,H,h) #> g \<subseteq> kernel(G,H,h) #> g'"
paulson@14884
  1170
apply (clarsimp simp add: kernel_def r_coset_def image_def)
paulson@14884
  1171
apply (rename_tac y)  
paulson@14884
  1172
apply (rule_tac x="y \<cdot> g \<cdot> inv g'" in bexI) 
paulson@14884
  1173
apply (simp_all add: G.m_assoc) 
paulson@14884
  1174
done
paulson@14884
  1175
paulson@14884
  1176
lemma (in group_hom) FactGroup_inj:
paulson@14884
  1177
     "(\<lambda>X\<in>carrier (G Mod kernel(G,H,h)). contents (h `` X))
paulson@14884
  1178
      \<in> inj(carrier (G Mod kernel(G,H,h)), carrier(H))"
paulson@14884
  1179
proof (simp add: inj_def FactGroup_contents_mem lam_type, clarify) 
paulson@14884
  1180
  fix X and X'
paulson@14884
  1181
  assume X:  "X  \<in> carrier (G Mod kernel(G,H,h))"
paulson@14884
  1182
     and X': "X' \<in> carrier (G Mod kernel(G,H,h))"
paulson@14884
  1183
  then
paulson@14884
  1184
  obtain g and g'
paulson@14884
  1185
           where gX: "g \<in> carrier(G)"  "g' \<in> carrier(G)" 
paulson@14884
  1186
              "X = kernel(G,H,h) #> g" "X' = kernel(G,H,h) #> g'"
paulson@14884
  1187
    by (auto simp add: FactGroup_def RCOSETS_def)
paulson@14884
  1188
  hence all: "\<forall>x\<in>X. h ` x = h ` g" "\<forall>x\<in>X'. h ` x = h ` g'"
paulson@14884
  1189
    and Xsub: "X \<subseteq> carrier(G)" and X'sub: "X' \<subseteq> carrier(G)"
paulson@14884
  1190
    by (force simp add: kernel_def r_coset_def image_def)+
paulson@14884
  1191
  assume "contents (h `` X) = contents (h `` X')"
paulson@14884
  1192
  hence h: "h ` g = h ` g'"
paulson@14884
  1193
    by (simp add: all image_eq_UN [OF hom_is_fun] FactGroup_nonempty 
paulson@14884
  1194
                  X X' Xsub X'sub)
paulson@14884
  1195
  show "X=X'" by (rule equalityI) (simp_all add: FactGroup_subset h gX) 
paulson@14884
  1196
qed
paulson@14884
  1197
paulson@14884
  1198
paulson@14884
  1199
lemma (in group_hom) kernel_rcoset_subset:
paulson@14884
  1200
  assumes g: "g \<in> carrier(G)"
paulson@14884
  1201
  shows "kernel(G,H,h) #> g \<subseteq> carrier (G)"
paulson@14884
  1202
    by (auto simp add: g kernel_def r_coset_def) 
paulson@14884
  1203
paulson@14884
  1204
paulson@14884
  1205
paulson@14884
  1206
text{*If the homomorphism @{term h} is onto @{term H}, then so is the
paulson@14884
  1207
homomorphism from the quotient group*}
paulson@14884
  1208
lemma (in group_hom) FactGroup_surj:
paulson@14884
  1209
  assumes h: "h \<in> surj(carrier(G), carrier(H))"
paulson@14884
  1210
  shows "(\<lambda>X\<in>carrier (G Mod kernel(G,H,h)). contents (h `` X))
paulson@14884
  1211
         \<in> surj(carrier (G Mod kernel(G,H,h)), carrier(H))"
paulson@14884
  1212
proof (simp add: surj_def FactGroup_contents_mem lam_type, clarify)
paulson@14884
  1213
  fix y
paulson@14884
  1214
  assume y: "y \<in> carrier(H)"
paulson@14884
  1215
  with h obtain g where g: "g \<in> carrier(G)" "h ` g = y"
paulson@14884
  1216
    by (auto simp add: surj_def) 
paulson@14884
  1217
  hence "(\<Union>x\<in>kernel(G,H,h) #> g. {h ` x}) = {y}" 
paulson@14884
  1218
    by (auto simp add: y kernel_def r_coset_def) 
paulson@14884
  1219
  with g show "\<exists>x\<in>carrier(G Mod kernel(G, H, h)). contents(h `` x) = y"
paulson@14884
  1220
        --{*The witness is @{term "kernel(G,H,h) #> g"}*}
paulson@14884
  1221
    by (force simp add: FactGroup_def RCOSETS_def 
paulson@14884
  1222
           image_eq_UN [OF hom_is_fun] kernel_rcoset_subset)
paulson@14884
  1223
qed
paulson@14884
  1224
paulson@14884
  1225
paulson@14884
  1226
text{*If @{term h} is a homomorphism from @{term G} onto @{term H}, then the
paulson@14884
  1227
 quotient group @{term "G Mod (kernel(G,H,h))"} is isomorphic to @{term H}.*}
paulson@14884
  1228
theorem (in group_hom) FactGroup_iso:
paulson@14884
  1229
  "h \<in> surj(carrier(G), carrier(H))
paulson@14884
  1230
   \<Longrightarrow> (\<lambda>X\<in>carrier (G Mod kernel(G,H,h)). contents (h``X)) \<in> (G Mod (kernel(G,H,h))) \<cong> H"
paulson@14884
  1231
by (simp add: iso_def FactGroup_hom FactGroup_inj bij_def FactGroup_surj)
paulson@14884
  1232
 
paulson@14884
  1233
end