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