src/HOL/Algebra/Coset.thy
author wenzelm
Sat Oct 10 16:26:23 2015 +0200 (2015-10-10)
changeset 61382 efac889fccbc
parent 57512 cc97b347b301
child 61628 8dd2bd4fe30b
permissions -rw-r--r--
isabelle update_cartouches;
wenzelm@14706
     1
(*  Title:      HOL/Algebra/Coset.thy
wenzelm@35849
     2
    Author:     Florian Kammueller
wenzelm@35849
     3
    Author:     L C Paulson
wenzelm@35849
     4
    Author:     Stephan Hohe
paulson@13870
     5
*)
paulson@13870
     6
wenzelm@35849
     7
theory Coset
wenzelm@35849
     8
imports Group
wenzelm@35849
     9
begin
ballarin@20318
    10
wenzelm@61382
    11
section \<open>Cosets and Quotient Groups\<close>
paulson@13870
    12
wenzelm@35847
    13
definition
paulson@14963
    14
  r_coset    :: "[_, 'a set, 'a] \<Rightarrow> 'a set"    (infixl "#>\<index>" 60)
wenzelm@35848
    15
  where "H #>\<^bsub>G\<^esub> a = (\<Union>h\<in>H. {h \<otimes>\<^bsub>G\<^esub> a})"
paulson@13870
    16
wenzelm@35847
    17
definition
paulson@14963
    18
  l_coset    :: "[_, 'a, 'a set] \<Rightarrow> 'a set"    (infixl "<#\<index>" 60)
wenzelm@35848
    19
  where "a <#\<^bsub>G\<^esub> H = (\<Union>h\<in>H. {a \<otimes>\<^bsub>G\<^esub> h})"
paulson@13870
    20
wenzelm@35847
    21
definition
paulson@14963
    22
  RCOSETS  :: "[_, 'a set] \<Rightarrow> ('a set)set"   ("rcosets\<index> _" [81] 80)
wenzelm@35848
    23
  where "rcosets\<^bsub>G\<^esub> H = (\<Union>a\<in>carrier G. {H #>\<^bsub>G\<^esub> a})"
paulson@14963
    24
wenzelm@35847
    25
definition
paulson@14963
    26
  set_mult  :: "[_, 'a set ,'a set] \<Rightarrow> 'a set" (infixl "<#>\<index>" 60)
wenzelm@35848
    27
  where "H <#>\<^bsub>G\<^esub> K = (\<Union>h\<in>H. \<Union>k\<in>K. {h \<otimes>\<^bsub>G\<^esub> k})"
paulson@13870
    28
wenzelm@35847
    29
definition
paulson@14963
    30
  SET_INV :: "[_,'a set] \<Rightarrow> 'a set"  ("set'_inv\<index> _" [81] 80)
wenzelm@35848
    31
  where "set_inv\<^bsub>G\<^esub> H = (\<Union>h\<in>H. {inv\<^bsub>G\<^esub> h})"
paulson@13870
    32
paulson@14963
    33
paulson@14963
    34
locale normal = subgroup + group +
paulson@14963
    35
  assumes coset_eq: "(\<forall>x \<in> carrier G. H #> x = x <# H)"
paulson@13870
    36
wenzelm@19380
    37
abbreviation
wenzelm@21404
    38
  normal_rel :: "['a set, ('a, 'b) monoid_scheme] \<Rightarrow> bool"  (infixl "\<lhd>" 60) where
wenzelm@19380
    39
  "H \<lhd> G \<equiv> normal H G"
paulson@13870
    40
paulson@13870
    41
wenzelm@61382
    42
subsection \<open>Basic Properties of Cosets\<close>
paulson@13870
    43
paulson@14747
    44
lemma (in group) coset_mult_assoc:
paulson@14747
    45
     "[| M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G |]
paulson@13870
    46
      ==> (M #> g) #> h = M #> (g \<otimes> h)"
paulson@14747
    47
by (force simp add: r_coset_def m_assoc)
paulson@13870
    48
paulson@14747
    49
lemma (in group) coset_mult_one [simp]: "M \<subseteq> carrier G ==> M #> \<one> = M"
paulson@14747
    50
by (force simp add: r_coset_def)
paulson@13870
    51
paulson@14747
    52
lemma (in group) coset_mult_inv1:
wenzelm@14666
    53
     "[| M #> (x \<otimes> (inv y)) = M;  x \<in> carrier G ; y \<in> carrier G;
paulson@14747
    54
         M \<subseteq> carrier G |] ==> M #> x = M #> y"
paulson@13870
    55
apply (erule subst [of concl: "%z. M #> x = z #> y"])
paulson@13870
    56
apply (simp add: coset_mult_assoc m_assoc)
paulson@13870
    57
done
paulson@13870
    58
paulson@14747
    59
lemma (in group) coset_mult_inv2:
paulson@14747
    60
     "[| M #> x = M #> y;  x \<in> carrier G;  y \<in> carrier G;  M \<subseteq> carrier G |]
paulson@13870
    61
      ==> M #> (x \<otimes> (inv y)) = M "
paulson@13870
    62
apply (simp add: coset_mult_assoc [symmetric])
paulson@13870
    63
apply (simp add: coset_mult_assoc)
paulson@13870
    64
done
paulson@13870
    65
paulson@14747
    66
lemma (in group) coset_join1:
paulson@14747
    67
     "[| H #> x = H;  x \<in> carrier G;  subgroup H G |] ==> x \<in> H"
paulson@13870
    68
apply (erule subst)
paulson@14963
    69
apply (simp add: r_coset_def)
paulson@14963
    70
apply (blast intro: l_one subgroup.one_closed sym)
paulson@13870
    71
done
paulson@13870
    72
paulson@14747
    73
lemma (in group) solve_equation:
paulson@14963
    74
    "\<lbrakk>subgroup H G; x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> \<exists>h\<in>H. y = h \<otimes> x"
paulson@13870
    75
apply (rule bexI [of _ "y \<otimes> (inv x)"])
wenzelm@14666
    76
apply (auto simp add: subgroup.m_closed subgroup.m_inv_closed m_assoc
paulson@13870
    77
                      subgroup.subset [THEN subsetD])
paulson@13870
    78
done
paulson@13870
    79
paulson@14963
    80
lemma (in group) repr_independence:
paulson@14963
    81
     "\<lbrakk>y \<in> H #> x;  x \<in> carrier G; subgroup H G\<rbrakk> \<Longrightarrow> H #> x = H #> y"
paulson@14963
    82
by (auto simp add: r_coset_def m_assoc [symmetric]
paulson@14963
    83
                   subgroup.subset [THEN subsetD]
paulson@14963
    84
                   subgroup.m_closed solve_equation)
paulson@14963
    85
paulson@14747
    86
lemma (in group) coset_join2:
paulson@14963
    87
     "\<lbrakk>x \<in> carrier G;  subgroup H G;  x\<in>H\<rbrakk> \<Longrightarrow> H #> x = H"
wenzelm@61382
    88
  --\<open>Alternative proof is to put @{term "x=\<one>"} in @{text repr_independence}.\<close>
paulson@14963
    89
by (force simp add: subgroup.m_closed r_coset_def solve_equation)
paulson@13870
    90
ballarin@20318
    91
lemma (in monoid) r_coset_subset_G:
paulson@14747
    92
     "[| H \<subseteq> carrier G; x \<in> carrier G |] ==> H #> x \<subseteq> carrier G"
paulson@14747
    93
by (auto simp add: r_coset_def)
paulson@13870
    94
paulson@14747
    95
lemma (in group) rcosI:
paulson@14747
    96
     "[| h \<in> H; H \<subseteq> carrier G; x \<in> carrier G|] ==> h \<otimes> x \<in> H #> x"
paulson@14747
    97
by (auto simp add: r_coset_def)
paulson@13870
    98
paulson@14963
    99
lemma (in group) rcosetsI:
paulson@14963
   100
     "\<lbrakk>H \<subseteq> carrier G; x \<in> carrier G\<rbrakk> \<Longrightarrow> H #> x \<in> rcosets H"
paulson@14963
   101
by (auto simp add: RCOSETS_def)
paulson@13870
   102
wenzelm@61382
   103
text\<open>Really needed?\<close>
paulson@14747
   104
lemma (in group) transpose_inv:
wenzelm@14666
   105
     "[| x \<otimes> y = z;  x \<in> carrier G;  y \<in> carrier G;  z \<in> carrier G |]
paulson@13870
   106
      ==> (inv x) \<otimes> z = y"
paulson@13870
   107
by (force simp add: m_assoc [symmetric])
paulson@13870
   108
paulson@14747
   109
lemma (in group) rcos_self: "[| x \<in> carrier G; subgroup H G |] ==> x \<in> H #> x"
paulson@14963
   110
apply (simp add: r_coset_def)
paulson@14963
   111
apply (blast intro: sym l_one subgroup.subset [THEN subsetD]
paulson@13870
   112
                    subgroup.one_closed)
paulson@13870
   113
done
paulson@13870
   114
wenzelm@61382
   115
text (in group) \<open>Opposite of @{thm [source] "repr_independence"}\<close>
ballarin@20318
   116
lemma (in group) repr_independenceD:
ballarin@27611
   117
  assumes "subgroup H G"
ballarin@20318
   118
  assumes ycarr: "y \<in> carrier G"
ballarin@20318
   119
      and repr:  "H #> x = H #> y"
ballarin@20318
   120
  shows "y \<in> H #> x"
ballarin@27611
   121
proof -
ballarin@29237
   122
  interpret subgroup H G by fact
ballarin@27611
   123
  show ?thesis  apply (subst repr)
wenzelm@23350
   124
  apply (intro rcos_self)
wenzelm@23350
   125
   apply (rule ycarr)
wenzelm@23350
   126
   apply (rule is_subgroup)
wenzelm@23350
   127
  done
ballarin@27611
   128
qed
ballarin@20318
   129
wenzelm@61382
   130
text \<open>Elements of a right coset are in the carrier\<close>
ballarin@20318
   131
lemma (in subgroup) elemrcos_carrier:
ballarin@27611
   132
  assumes "group G"
ballarin@20318
   133
  assumes acarr: "a \<in> carrier G"
ballarin@20318
   134
    and a': "a' \<in> H #> a"
ballarin@20318
   135
  shows "a' \<in> carrier G"
ballarin@20318
   136
proof -
ballarin@29237
   137
  interpret group G by fact
ballarin@20318
   138
  from subset and acarr
ballarin@20318
   139
  have "H #> a \<subseteq> carrier G" by (rule r_coset_subset_G)
ballarin@20318
   140
  from this and a'
ballarin@20318
   141
  show "a' \<in> carrier G"
ballarin@20318
   142
    by fast
ballarin@20318
   143
qed
ballarin@20318
   144
ballarin@20318
   145
lemma (in subgroup) rcos_const:
ballarin@27611
   146
  assumes "group G"
ballarin@20318
   147
  assumes hH: "h \<in> H"
ballarin@20318
   148
  shows "H #> h = H"
ballarin@27611
   149
proof -
ballarin@29237
   150
  interpret group G by fact
ballarin@27611
   151
  show ?thesis apply (unfold r_coset_def)
ballarin@27611
   152
    apply rule
ballarin@27611
   153
    apply rule
ballarin@27611
   154
    apply clarsimp
ballarin@27611
   155
    apply (intro subgroup.m_closed)
ballarin@27611
   156
    apply (rule is_subgroup)
wenzelm@23463
   157
    apply assumption
ballarin@27611
   158
    apply (rule hH)
ballarin@27611
   159
    apply rule
ballarin@27611
   160
    apply simp
ballarin@27611
   161
  proof -
ballarin@27611
   162
    fix h'
ballarin@27611
   163
    assume h'H: "h' \<in> H"
ballarin@27611
   164
    note carr = hH[THEN mem_carrier] h'H[THEN mem_carrier]
ballarin@27611
   165
    from carr
ballarin@27611
   166
    have a: "h' = (h' \<otimes> inv h) \<otimes> h" by (simp add: m_assoc)
ballarin@27611
   167
    from h'H hH
ballarin@27611
   168
    have "h' \<otimes> inv h \<in> H" by simp
ballarin@27611
   169
    from this and a
ballarin@27611
   170
    show "\<exists>x\<in>H. h' = x \<otimes> h" by fast
ballarin@27611
   171
  qed
ballarin@20318
   172
qed
ballarin@20318
   173
wenzelm@61382
   174
text \<open>Step one for lemma @{text "rcos_module"}\<close>
ballarin@20318
   175
lemma (in subgroup) rcos_module_imp:
ballarin@27611
   176
  assumes "group G"
ballarin@20318
   177
  assumes xcarr: "x \<in> carrier G"
ballarin@20318
   178
      and x'cos: "x' \<in> H #> x"
ballarin@20318
   179
  shows "(x' \<otimes> inv x) \<in> H"
ballarin@20318
   180
proof -
ballarin@29237
   181
  interpret group G by fact
ballarin@20318
   182
  from xcarr x'cos
ballarin@20318
   183
      have x'carr: "x' \<in> carrier G"
ballarin@20318
   184
      by (rule elemrcos_carrier[OF is_group])
ballarin@20318
   185
  from xcarr
ballarin@20318
   186
      have ixcarr: "inv x \<in> carrier G"
ballarin@20318
   187
      by simp
ballarin@20318
   188
  from x'cos
ballarin@20318
   189
      have "\<exists>h\<in>H. x' = h \<otimes> x"
ballarin@20318
   190
      unfolding r_coset_def
ballarin@20318
   191
      by fast
ballarin@20318
   192
  from this
ballarin@20318
   193
      obtain h
ballarin@20318
   194
        where hH: "h \<in> H"
ballarin@20318
   195
        and x': "x' = h \<otimes> x"
ballarin@20318
   196
      by auto
ballarin@20318
   197
  from hH and subset
ballarin@20318
   198
      have hcarr: "h \<in> carrier G" by fast
ballarin@20318
   199
  note carr = xcarr x'carr hcarr
ballarin@20318
   200
  from x' and carr
ballarin@20318
   201
      have "x' \<otimes> (inv x) = (h \<otimes> x) \<otimes> (inv x)" by fast
ballarin@20318
   202
  also from carr
ballarin@20318
   203
      have "\<dots> = h \<otimes> (x \<otimes> inv x)" by (simp add: m_assoc)
ballarin@20318
   204
  also from carr
ballarin@20318
   205
      have "\<dots> = h \<otimes> \<one>" by simp
ballarin@20318
   206
  also from carr
ballarin@20318
   207
      have "\<dots> = h" by simp
ballarin@20318
   208
  finally
ballarin@20318
   209
      have "x' \<otimes> (inv x) = h" by simp
ballarin@20318
   210
  from hH this
ballarin@20318
   211
      show "x' \<otimes> (inv x) \<in> H" by simp
ballarin@20318
   212
qed
ballarin@20318
   213
wenzelm@61382
   214
text \<open>Step two for lemma @{text "rcos_module"}\<close>
ballarin@20318
   215
lemma (in subgroup) rcos_module_rev:
ballarin@27611
   216
  assumes "group G"
ballarin@20318
   217
  assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
ballarin@20318
   218
      and xixH: "(x' \<otimes> inv x) \<in> H"
ballarin@20318
   219
  shows "x' \<in> H #> x"
ballarin@20318
   220
proof -
ballarin@29237
   221
  interpret group G by fact
ballarin@20318
   222
  from xixH
ballarin@20318
   223
      have "\<exists>h\<in>H. x' \<otimes> (inv x) = h" by fast
ballarin@20318
   224
  from this
ballarin@20318
   225
      obtain h
ballarin@20318
   226
        where hH: "h \<in> H"
ballarin@20318
   227
        and hsym: "x' \<otimes> (inv x) = h"
ballarin@20318
   228
      by fast
ballarin@20318
   229
  from hH subset have hcarr: "h \<in> carrier G" by simp
ballarin@20318
   230
  note carr = carr hcarr
ballarin@20318
   231
  from hsym[symmetric] have "h \<otimes> x = x' \<otimes> (inv x) \<otimes> x" by fast
ballarin@20318
   232
  also from carr
ballarin@20318
   233
      have "\<dots> = x' \<otimes> ((inv x) \<otimes> x)" by (simp add: m_assoc)
ballarin@20318
   234
  also from carr
wenzelm@46721
   235
      have "\<dots> = x' \<otimes> \<one>" by simp
ballarin@20318
   236
  also from carr
ballarin@20318
   237
      have "\<dots> = x'" by simp
ballarin@20318
   238
  finally
ballarin@20318
   239
      have "h \<otimes> x = x'" by simp
ballarin@20318
   240
  from this[symmetric] and hH
ballarin@20318
   241
      show "x' \<in> H #> x"
ballarin@20318
   242
      unfolding r_coset_def
ballarin@20318
   243
      by fast
ballarin@20318
   244
qed
ballarin@20318
   245
wenzelm@61382
   246
text \<open>Module property of right cosets\<close>
ballarin@20318
   247
lemma (in subgroup) rcos_module:
ballarin@27611
   248
  assumes "group G"
ballarin@20318
   249
  assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
ballarin@20318
   250
  shows "(x' \<in> H #> x) = (x' \<otimes> inv x \<in> H)"
ballarin@27611
   251
proof -
ballarin@29237
   252
  interpret group G by fact
ballarin@27611
   253
  show ?thesis proof  assume "x' \<in> H #> x"
ballarin@27611
   254
    from this and carr
ballarin@27611
   255
    show "x' \<otimes> inv x \<in> H"
ballarin@20318
   256
      by (intro rcos_module_imp[OF is_group])
ballarin@27611
   257
  next
ballarin@27611
   258
    assume "x' \<otimes> inv x \<in> H"
ballarin@27611
   259
    from this and carr
ballarin@27611
   260
    show "x' \<in> H #> x"
ballarin@20318
   261
      by (intro rcos_module_rev[OF is_group])
ballarin@27611
   262
  qed
ballarin@20318
   263
qed
ballarin@20318
   264
wenzelm@61382
   265
text \<open>Right cosets are subsets of the carrier.\<close> 
ballarin@20318
   266
lemma (in subgroup) rcosets_carrier:
ballarin@27611
   267
  assumes "group G"
ballarin@20318
   268
  assumes XH: "X \<in> rcosets H"
ballarin@20318
   269
  shows "X \<subseteq> carrier G"
ballarin@20318
   270
proof -
ballarin@29237
   271
  interpret group G by fact
ballarin@20318
   272
  from XH have "\<exists>x\<in> carrier G. X = H #> x"
ballarin@20318
   273
      unfolding RCOSETS_def
ballarin@20318
   274
      by fast
ballarin@20318
   275
  from this
ballarin@20318
   276
      obtain x
ballarin@20318
   277
        where xcarr: "x\<in> carrier G"
ballarin@20318
   278
        and X: "X = H #> x"
ballarin@20318
   279
      by fast
ballarin@20318
   280
  from subset and xcarr
ballarin@20318
   281
      show "X \<subseteq> carrier G"
ballarin@20318
   282
      unfolding X
ballarin@20318
   283
      by (rule r_coset_subset_G)
ballarin@20318
   284
qed
ballarin@20318
   285
wenzelm@61382
   286
text \<open>Multiplication of general subsets\<close>
ballarin@20318
   287
lemma (in monoid) set_mult_closed:
ballarin@20318
   288
  assumes Acarr: "A \<subseteq> carrier G"
ballarin@20318
   289
      and Bcarr: "B \<subseteq> carrier G"
ballarin@20318
   290
  shows "A <#> B \<subseteq> carrier G"
ballarin@20318
   291
apply rule apply (simp add: set_mult_def, clarsimp)
ballarin@20318
   292
proof -
ballarin@20318
   293
  fix a b
ballarin@20318
   294
  assume "a \<in> A"
ballarin@20318
   295
  from this and Acarr
ballarin@20318
   296
      have acarr: "a \<in> carrier G" by fast
ballarin@20318
   297
ballarin@20318
   298
  assume "b \<in> B"
ballarin@20318
   299
  from this and Bcarr
ballarin@20318
   300
      have bcarr: "b \<in> carrier G" by fast
ballarin@20318
   301
ballarin@20318
   302
  from acarr bcarr
ballarin@20318
   303
      show "a \<otimes> b \<in> carrier G" by (rule m_closed)
ballarin@20318
   304
qed
ballarin@20318
   305
ballarin@20318
   306
lemma (in comm_group) mult_subgroups:
ballarin@20318
   307
  assumes subH: "subgroup H G"
ballarin@20318
   308
      and subK: "subgroup K G"
ballarin@20318
   309
  shows "subgroup (H <#> K) G"
ballarin@20318
   310
apply (rule subgroup.intro)
ballarin@20318
   311
   apply (intro set_mult_closed subgroup.subset[OF subH] subgroup.subset[OF subK])
ballarin@20318
   312
  apply (simp add: set_mult_def) apply clarsimp defer 1
ballarin@20318
   313
  apply (simp add: set_mult_def) defer 1
ballarin@20318
   314
  apply (simp add: set_mult_def, clarsimp) defer 1
ballarin@20318
   315
proof -
ballarin@20318
   316
  fix ha hb ka kb
ballarin@20318
   317
  assume haH: "ha \<in> H" and hbH: "hb \<in> H" and kaK: "ka \<in> K" and kbK: "kb \<in> K"
ballarin@20318
   318
  note carr = haH[THEN subgroup.mem_carrier[OF subH]] hbH[THEN subgroup.mem_carrier[OF subH]]
ballarin@20318
   319
              kaK[THEN subgroup.mem_carrier[OF subK]] kbK[THEN subgroup.mem_carrier[OF subK]]
ballarin@20318
   320
  from carr
ballarin@20318
   321
      have "(ha \<otimes> ka) \<otimes> (hb \<otimes> kb) = ha \<otimes> (ka \<otimes> hb) \<otimes> kb" by (simp add: m_assoc)
ballarin@20318
   322
  also from carr
ballarin@20318
   323
      have "\<dots> = ha \<otimes> (hb \<otimes> ka) \<otimes> kb" by (simp add: m_comm)
ballarin@20318
   324
  also from carr
ballarin@20318
   325
      have "\<dots> = (ha \<otimes> hb) \<otimes> (ka \<otimes> kb)" by (simp add: m_assoc)
ballarin@20318
   326
  finally
ballarin@20318
   327
      have eq: "(ha \<otimes> ka) \<otimes> (hb \<otimes> kb) = (ha \<otimes> hb) \<otimes> (ka \<otimes> kb)" .
ballarin@20318
   328
ballarin@20318
   329
  from haH hbH have hH: "ha \<otimes> hb \<in> H" by (simp add: subgroup.m_closed[OF subH])
ballarin@20318
   330
  from kaK kbK have kK: "ka \<otimes> kb \<in> K" by (simp add: subgroup.m_closed[OF subK])
ballarin@20318
   331
  
ballarin@20318
   332
  from hH and kK and eq
ballarin@20318
   333
      show "\<exists>h'\<in>H. \<exists>k'\<in>K. (ha \<otimes> ka) \<otimes> (hb \<otimes> kb) = h' \<otimes> k'" by fast
ballarin@20318
   334
next
ballarin@20318
   335
  have "\<one> = \<one> \<otimes> \<one>" by simp
ballarin@20318
   336
  from subgroup.one_closed[OF subH] subgroup.one_closed[OF subK] this
ballarin@20318
   337
      show "\<exists>h\<in>H. \<exists>k\<in>K. \<one> = h \<otimes> k" by fast
ballarin@20318
   338
next
ballarin@20318
   339
  fix h k
ballarin@20318
   340
  assume hH: "h \<in> H"
ballarin@20318
   341
     and kK: "k \<in> K"
ballarin@20318
   342
ballarin@20318
   343
  from hH[THEN subgroup.mem_carrier[OF subH]] kK[THEN subgroup.mem_carrier[OF subK]]
ballarin@20318
   344
      have "inv (h \<otimes> k) = inv h \<otimes> inv k" by (simp add: inv_mult_group m_comm)
ballarin@20318
   345
ballarin@20318
   346
  from subgroup.m_inv_closed[OF subH hH] and subgroup.m_inv_closed[OF subK kK] and this
ballarin@20318
   347
      show "\<exists>ha\<in>H. \<exists>ka\<in>K. inv (h \<otimes> k) = ha \<otimes> ka" by fast
ballarin@20318
   348
qed
ballarin@20318
   349
ballarin@20318
   350
lemma (in subgroup) lcos_module_rev:
ballarin@27611
   351
  assumes "group G"
ballarin@20318
   352
  assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
ballarin@20318
   353
      and xixH: "(inv x \<otimes> x') \<in> H"
ballarin@20318
   354
  shows "x' \<in> x <# H"
ballarin@20318
   355
proof -
ballarin@29237
   356
  interpret group G by fact
ballarin@20318
   357
  from xixH
ballarin@20318
   358
      have "\<exists>h\<in>H. (inv x) \<otimes> x' = h" by fast
ballarin@20318
   359
  from this
ballarin@20318
   360
      obtain h
ballarin@20318
   361
        where hH: "h \<in> H"
ballarin@20318
   362
        and hsym: "(inv x) \<otimes> x' = h"
ballarin@20318
   363
      by fast
ballarin@20318
   364
ballarin@20318
   365
  from hH subset have hcarr: "h \<in> carrier G" by simp
ballarin@20318
   366
  note carr = carr hcarr
ballarin@20318
   367
  from hsym[symmetric] have "x \<otimes> h = x \<otimes> ((inv x) \<otimes> x')" by fast
ballarin@20318
   368
  also from carr
ballarin@20318
   369
      have "\<dots> = (x \<otimes> (inv x)) \<otimes> x'" by (simp add: m_assoc[symmetric])
ballarin@20318
   370
  also from carr
ballarin@20318
   371
      have "\<dots> = \<one> \<otimes> x'" by simp
ballarin@20318
   372
  also from carr
ballarin@20318
   373
      have "\<dots> = x'" by simp
ballarin@20318
   374
  finally
ballarin@20318
   375
      have "x \<otimes> h = x'" by simp
ballarin@20318
   376
ballarin@20318
   377
  from this[symmetric] and hH
ballarin@20318
   378
      show "x' \<in> x <# H"
ballarin@20318
   379
      unfolding l_coset_def
ballarin@20318
   380
      by fast
ballarin@20318
   381
qed
ballarin@20318
   382
paulson@13870
   383
wenzelm@61382
   384
subsection \<open>Normal subgroups\<close>
paulson@13870
   385
paulson@14963
   386
lemma normal_imp_subgroup: "H \<lhd> G \<Longrightarrow> subgroup H G"
paulson@14963
   387
  by (simp add: normal_def subgroup_def)
paulson@13870
   388
paulson@14963
   389
lemma (in group) normalI: 
wenzelm@26310
   390
  "subgroup H G \<Longrightarrow> (\<forall>x \<in> carrier G. H #> x = x <# H) \<Longrightarrow> H \<lhd> G"
wenzelm@41528
   391
  by (simp add: normal_def normal_axioms_def is_group)
paulson@14963
   392
paulson@14963
   393
lemma (in normal) inv_op_closed1:
paulson@14963
   394
     "\<lbrakk>x \<in> carrier G; h \<in> H\<rbrakk> \<Longrightarrow> (inv x) \<otimes> h \<otimes> x \<in> H"
paulson@14963
   395
apply (insert coset_eq) 
paulson@14963
   396
apply (auto simp add: l_coset_def r_coset_def)
wenzelm@14666
   397
apply (drule bspec, assumption)
paulson@13870
   398
apply (drule equalityD1 [THEN subsetD], blast, clarify)
paulson@14963
   399
apply (simp add: m_assoc)
paulson@14963
   400
apply (simp add: m_assoc [symmetric])
paulson@13870
   401
done
paulson@13870
   402
paulson@14963
   403
lemma (in normal) inv_op_closed2:
paulson@14963
   404
     "\<lbrakk>x \<in> carrier G; h \<in> H\<rbrakk> \<Longrightarrow> x \<otimes> h \<otimes> (inv x) \<in> H"
paulson@14963
   405
apply (subgoal_tac "inv (inv x) \<otimes> h \<otimes> (inv x) \<in> H") 
wenzelm@26310
   406
apply (simp add: ) 
paulson@14963
   407
apply (blast intro: inv_op_closed1) 
paulson@13870
   408
done
paulson@13870
   409
wenzelm@61382
   410
text\<open>Alternative characterization of normal subgroups\<close>
paulson@14747
   411
lemma (in group) normal_inv_iff:
paulson@14747
   412
     "(N \<lhd> G) = 
paulson@14747
   413
      (subgroup N G & (\<forall>x \<in> carrier G. \<forall>h \<in> N. x \<otimes> h \<otimes> (inv x) \<in> N))"
paulson@14747
   414
      (is "_ = ?rhs")
paulson@14747
   415
proof
paulson@14747
   416
  assume N: "N \<lhd> G"
paulson@14747
   417
  show ?rhs
paulson@14963
   418
    by (blast intro: N normal.inv_op_closed2 normal_imp_subgroup) 
paulson@14747
   419
next
paulson@14747
   420
  assume ?rhs
paulson@14747
   421
  hence sg: "subgroup N G" 
paulson@14963
   422
    and closed: "\<And>x. x\<in>carrier G \<Longrightarrow> \<forall>h\<in>N. x \<otimes> h \<otimes> inv x \<in> N" by auto
paulson@14747
   423
  hence sb: "N \<subseteq> carrier G" by (simp add: subgroup.subset) 
paulson@14747
   424
  show "N \<lhd> G"
paulson@14963
   425
  proof (intro normalI [OF sg], simp add: l_coset_def r_coset_def, clarify)
paulson@14747
   426
    fix x
paulson@14747
   427
    assume x: "x \<in> carrier G"
nipkow@15120
   428
    show "(\<Union>h\<in>N. {h \<otimes> x}) = (\<Union>h\<in>N. {x \<otimes> h})"
paulson@14747
   429
    proof
nipkow@15120
   430
      show "(\<Union>h\<in>N. {h \<otimes> x}) \<subseteq> (\<Union>h\<in>N. {x \<otimes> h})"
paulson@14747
   431
      proof clarify
paulson@14747
   432
        fix n
paulson@14747
   433
        assume n: "n \<in> N" 
nipkow@15120
   434
        show "n \<otimes> x \<in> (\<Union>h\<in>N. {x \<otimes> h})"
paulson@14747
   435
        proof 
paulson@14963
   436
          from closed [of "inv x"]
paulson@14963
   437
          show "inv x \<otimes> n \<otimes> x \<in> N" by (simp add: x n)
paulson@14963
   438
          show "n \<otimes> x \<in> {x \<otimes> (inv x \<otimes> n \<otimes> x)}"
paulson@14747
   439
            by (simp add: x n m_assoc [symmetric] sb [THEN subsetD])
paulson@14747
   440
        qed
paulson@14747
   441
      qed
paulson@14747
   442
    next
nipkow@15120
   443
      show "(\<Union>h\<in>N. {x \<otimes> h}) \<subseteq> (\<Union>h\<in>N. {h \<otimes> x})"
paulson@14747
   444
      proof clarify
paulson@14747
   445
        fix n
paulson@14747
   446
        assume n: "n \<in> N" 
nipkow@15120
   447
        show "x \<otimes> n \<in> (\<Union>h\<in>N. {h \<otimes> x})"
paulson@14747
   448
        proof 
paulson@14963
   449
          show "x \<otimes> n \<otimes> inv x \<in> N" by (simp add: x n closed)
paulson@14963
   450
          show "x \<otimes> n \<in> {x \<otimes> n \<otimes> inv x \<otimes> x}"
paulson@14747
   451
            by (simp add: x n m_assoc sb [THEN subsetD])
paulson@14747
   452
        qed
paulson@14747
   453
      qed
paulson@14747
   454
    qed
paulson@14747
   455
  qed
paulson@14747
   456
qed
paulson@13870
   457
paulson@14963
   458
wenzelm@61382
   459
subsection\<open>More Properties of Cosets\<close>
paulson@14803
   460
paulson@14747
   461
lemma (in group) lcos_m_assoc:
paulson@14747
   462
     "[| M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G |]
paulson@14747
   463
      ==> g <# (h <# M) = (g \<otimes> h) <# M"
paulson@14747
   464
by (force simp add: l_coset_def m_assoc)
paulson@13870
   465
paulson@14747
   466
lemma (in group) lcos_mult_one: "M \<subseteq> carrier G ==> \<one> <# M = M"
paulson@14747
   467
by (force simp add: l_coset_def)
paulson@13870
   468
paulson@14747
   469
lemma (in group) l_coset_subset_G:
paulson@14747
   470
     "[| H \<subseteq> carrier G; x \<in> carrier G |] ==> x <# H \<subseteq> carrier G"
paulson@14747
   471
by (auto simp add: l_coset_def subsetD)
paulson@14747
   472
paulson@14747
   473
lemma (in group) l_coset_swap:
paulson@14963
   474
     "\<lbrakk>y \<in> x <# H;  x \<in> carrier G;  subgroup H G\<rbrakk> \<Longrightarrow> x \<in> y <# H"
paulson@14963
   475
proof (simp add: l_coset_def)
paulson@14963
   476
  assume "\<exists>h\<in>H. y = x \<otimes> h"
wenzelm@14666
   477
    and x: "x \<in> carrier G"
paulson@14530
   478
    and sb: "subgroup H G"
paulson@14530
   479
  then obtain h' where h': "h' \<in> H & x \<otimes> h' = y" by blast
paulson@14963
   480
  show "\<exists>h\<in>H. x = y \<otimes> h"
paulson@14530
   481
  proof
paulson@14963
   482
    show "x = y \<otimes> inv h'" using h' x sb
paulson@14530
   483
      by (auto simp add: m_assoc subgroup.subset [THEN subsetD])
paulson@14530
   484
    show "inv h' \<in> H" using h' sb
paulson@14530
   485
      by (auto simp add: subgroup.subset [THEN subsetD] subgroup.m_inv_closed)
paulson@14530
   486
  qed
paulson@14530
   487
qed
paulson@14530
   488
paulson@14747
   489
lemma (in group) l_coset_carrier:
paulson@14530
   490
     "[| y \<in> x <# H;  x \<in> carrier G;  subgroup H G |] ==> y \<in> carrier G"
paulson@14747
   491
by (auto simp add: l_coset_def m_assoc
paulson@14530
   492
                   subgroup.subset [THEN subsetD] subgroup.m_closed)
paulson@14530
   493
paulson@14747
   494
lemma (in group) l_repr_imp_subset:
wenzelm@14666
   495
  assumes y: "y \<in> x <# H" and x: "x \<in> carrier G" and sb: "subgroup H G"
paulson@14530
   496
  shows "y <# H \<subseteq> x <# H"
paulson@14530
   497
proof -
paulson@14530
   498
  from y
paulson@14747
   499
  obtain h' where "h' \<in> H" "x \<otimes> h' = y" by (auto simp add: l_coset_def)
paulson@14530
   500
  thus ?thesis using x sb
paulson@14747
   501
    by (auto simp add: l_coset_def m_assoc
paulson@14530
   502
                       subgroup.subset [THEN subsetD] subgroup.m_closed)
paulson@14530
   503
qed
paulson@14530
   504
paulson@14747
   505
lemma (in group) l_repr_independence:
wenzelm@14666
   506
  assumes y: "y \<in> x <# H" and x: "x \<in> carrier G" and sb: "subgroup H G"
paulson@14530
   507
  shows "x <# H = y <# H"
wenzelm@14666
   508
proof
paulson@14530
   509
  show "x <# H \<subseteq> y <# H"
wenzelm@14666
   510
    by (rule l_repr_imp_subset,
paulson@14530
   511
        (blast intro: l_coset_swap l_coset_carrier y x sb)+)
wenzelm@14666
   512
  show "y <# H \<subseteq> x <# H" by (rule l_repr_imp_subset [OF y x sb])
paulson@14530
   513
qed
paulson@13870
   514
paulson@14747
   515
lemma (in group) setmult_subset_G:
paulson@14963
   516
     "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G\<rbrakk> \<Longrightarrow> H <#> K \<subseteq> carrier G"
paulson@14963
   517
by (auto simp add: set_mult_def subsetD)
paulson@13870
   518
paulson@14963
   519
lemma (in group) subgroup_mult_id: "subgroup H G \<Longrightarrow> H <#> H = H"
paulson@14963
   520
apply (auto simp add: subgroup.m_closed set_mult_def Sigma_def image_def)
paulson@13870
   521
apply (rule_tac x = x in bexI)
paulson@13870
   522
apply (rule bexI [of _ "\<one>"])
wenzelm@46721
   523
apply (auto simp add: subgroup.one_closed subgroup.subset [THEN subsetD])
paulson@13870
   524
done
paulson@13870
   525
paulson@13870
   526
wenzelm@61382
   527
subsubsection \<open>Set of Inverses of an @{text r_coset}.\<close>
wenzelm@14666
   528
paulson@14963
   529
lemma (in normal) rcos_inv:
paulson@14963
   530
  assumes x:     "x \<in> carrier G"
paulson@14963
   531
  shows "set_inv (H #> x) = H #> (inv x)" 
paulson@14963
   532
proof (simp add: r_coset_def SET_INV_def x inv_mult_group, safe)
paulson@14963
   533
  fix h
wenzelm@41528
   534
  assume h: "h \<in> H"
nipkow@15120
   535
  show "inv x \<otimes> inv h \<in> (\<Union>j\<in>H. {j \<otimes> inv x})"
paulson@14963
   536
  proof
paulson@14963
   537
    show "inv x \<otimes> inv h \<otimes> x \<in> H"
wenzelm@41528
   538
      by (simp add: inv_op_closed1 h x)
paulson@14963
   539
    show "inv x \<otimes> inv h \<in> {inv x \<otimes> inv h \<otimes> x \<otimes> inv x}"
wenzelm@41528
   540
      by (simp add: h x m_assoc)
paulson@14963
   541
  qed
nipkow@15120
   542
  show "h \<otimes> inv x \<in> (\<Union>j\<in>H. {inv x \<otimes> inv j})"
paulson@14963
   543
  proof
paulson@14963
   544
    show "x \<otimes> inv h \<otimes> inv x \<in> H"
wenzelm@41528
   545
      by (simp add: inv_op_closed2 h x)
paulson@14963
   546
    show "h \<otimes> inv x \<in> {inv x \<otimes> inv (x \<otimes> inv h \<otimes> inv x)}"
wenzelm@41528
   547
      by (simp add: h x m_assoc [symmetric] inv_mult_group)
paulson@13870
   548
  qed
paulson@13870
   549
qed
paulson@13870
   550
paulson@13870
   551
wenzelm@61382
   552
subsubsection \<open>Theorems for @{text "<#>"} with @{text "#>"} or @{text "<#"}.\<close>
wenzelm@14666
   553
paulson@14747
   554
lemma (in group) setmult_rcos_assoc:
paulson@14963
   555
     "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G\<rbrakk>
paulson@14963
   556
      \<Longrightarrow> H <#> (K #> x) = (H <#> K) #> x"
paulson@14963
   557
by (force simp add: r_coset_def set_mult_def m_assoc)
paulson@13870
   558
paulson@14747
   559
lemma (in group) rcos_assoc_lcos:
paulson@14963
   560
     "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G\<rbrakk>
paulson@14963
   561
      \<Longrightarrow> (H #> x) <#> K = H <#> (x <# K)"
paulson@14963
   562
by (force simp add: r_coset_def l_coset_def set_mult_def m_assoc)
paulson@13870
   563
paulson@14963
   564
lemma (in normal) rcos_mult_step1:
paulson@14963
   565
     "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
paulson@14963
   566
      \<Longrightarrow> (H #> x) <#> (H #> y) = (H <#> (x <# H)) #> y"
paulson@14963
   567
by (simp add: setmult_rcos_assoc subset
paulson@13870
   568
              r_coset_subset_G l_coset_subset_G rcos_assoc_lcos)
paulson@13870
   569
paulson@14963
   570
lemma (in normal) rcos_mult_step2:
paulson@14963
   571
     "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
paulson@14963
   572
      \<Longrightarrow> (H <#> (x <# H)) #> y = (H <#> (H #> x)) #> y"
paulson@14963
   573
by (insert coset_eq, simp add: normal_def)
paulson@13870
   574
paulson@14963
   575
lemma (in normal) rcos_mult_step3:
paulson@14963
   576
     "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
paulson@14963
   577
      \<Longrightarrow> (H <#> (H #> x)) #> y = H #> (x \<otimes> y)"
paulson@14963
   578
by (simp add: setmult_rcos_assoc coset_mult_assoc
wenzelm@41528
   579
              subgroup_mult_id normal.axioms subset normal_axioms)
paulson@13870
   580
paulson@14963
   581
lemma (in normal) rcos_sum:
paulson@14963
   582
     "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
paulson@14963
   583
      \<Longrightarrow> (H #> x) <#> (H #> y) = H #> (x \<otimes> y)"
paulson@13870
   584
by (simp add: rcos_mult_step1 rcos_mult_step2 rcos_mult_step3)
paulson@13870
   585
paulson@14963
   586
lemma (in normal) rcosets_mult_eq: "M \<in> rcosets H \<Longrightarrow> H <#> M = M"
wenzelm@61382
   587
  -- \<open>generalizes @{text subgroup_mult_id}\<close>
paulson@14963
   588
  by (auto simp add: RCOSETS_def subset
wenzelm@41528
   589
        setmult_rcos_assoc subgroup_mult_id normal.axioms normal_axioms)
paulson@14963
   590
paulson@14963
   591
wenzelm@61382
   592
subsubsection\<open>An Equivalence Relation\<close>
paulson@14963
   593
wenzelm@35847
   594
definition
wenzelm@35847
   595
  r_congruent :: "[('a,'b)monoid_scheme, 'a set] \<Rightarrow> ('a*'a)set"  ("rcong\<index> _")
wenzelm@35848
   596
  where "rcong\<^bsub>G\<^esub> H = {(x,y). x \<in> carrier G & y \<in> carrier G & inv\<^bsub>G\<^esub> x \<otimes>\<^bsub>G\<^esub> y \<in> H}"
paulson@14963
   597
paulson@14963
   598
paulson@14963
   599
lemma (in subgroup) equiv_rcong:
ballarin@27611
   600
   assumes "group G"
paulson@14963
   601
   shows "equiv (carrier G) (rcong H)"
ballarin@27611
   602
proof -
ballarin@29237
   603
  interpret group G by fact
ballarin@27611
   604
  show ?thesis
haftmann@40815
   605
  proof (intro equivI)
nipkow@30198
   606
    show "refl_on (carrier G) (rcong H)"
nipkow@30198
   607
      by (auto simp add: r_congruent_def refl_on_def) 
ballarin@27611
   608
  next
ballarin@27611
   609
    show "sym (rcong H)"
ballarin@27611
   610
    proof (simp add: r_congruent_def sym_def, clarify)
ballarin@27611
   611
      fix x y
ballarin@27611
   612
      assume [simp]: "x \<in> carrier G" "y \<in> carrier G" 
wenzelm@32960
   613
         and "inv x \<otimes> y \<in> H"
wenzelm@46721
   614
      hence "inv (inv x \<otimes> y) \<in> H" by simp
ballarin@27611
   615
      thus "inv y \<otimes> x \<in> H" by (simp add: inv_mult_group)
ballarin@27611
   616
    qed
ballarin@27611
   617
  next
ballarin@27611
   618
    show "trans (rcong H)"
ballarin@27611
   619
    proof (simp add: r_congruent_def trans_def, clarify)
ballarin@27611
   620
      fix x y z
ballarin@27611
   621
      assume [simp]: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
wenzelm@32960
   622
         and "inv x \<otimes> y \<in> H" and "inv y \<otimes> z \<in> H"
ballarin@27611
   623
      hence "(inv x \<otimes> y) \<otimes> (inv y \<otimes> z) \<in> H" by simp
ballarin@27698
   624
      hence "inv x \<otimes> (y \<otimes> inv y) \<otimes> z \<in> H"
wenzelm@32960
   625
        by (simp add: m_assoc del: r_inv Units_r_inv) 
ballarin@27611
   626
      thus "inv x \<otimes> z \<in> H" by simp
ballarin@27611
   627
    qed
paulson@14963
   628
  qed
paulson@14963
   629
qed
paulson@14963
   630
wenzelm@61382
   631
text\<open>Equivalence classes of @{text rcong} correspond to left cosets.
paulson@14963
   632
  Was there a mistake in the definitions? I'd have expected them to
wenzelm@61382
   633
  correspond to right cosets.\<close>
paulson@14963
   634
paulson@14963
   635
(* CB: This is correct, but subtle.
paulson@14963
   636
   We call H #> a the right coset of a relative to H.  According to
paulson@14963
   637
   Jacobson, this is what the majority of group theory literature does.
paulson@14963
   638
   He then defines the notion of congruence relation ~ over monoids as
paulson@14963
   639
   equivalence relation with a ~ a' & b ~ b' \<Longrightarrow> a*b ~ a'*b'.
paulson@14963
   640
   Our notion of right congruence induced by K: rcong K appears only in
paulson@14963
   641
   the context where K is a normal subgroup.  Jacobson doesn't name it.
paulson@14963
   642
   But in this context left and right cosets are identical.
paulson@14963
   643
*)
paulson@14963
   644
paulson@14963
   645
lemma (in subgroup) l_coset_eq_rcong:
ballarin@27611
   646
  assumes "group G"
paulson@14963
   647
  assumes a: "a \<in> carrier G"
paulson@14963
   648
  shows "a <# H = rcong H `` {a}"
ballarin@27611
   649
proof -
ballarin@29237
   650
  interpret group G by fact
ballarin@27611
   651
  show ?thesis by (force simp add: r_congruent_def l_coset_def m_assoc [symmetric] a ) 
ballarin@27611
   652
qed
paulson@13870
   653
wenzelm@35849
   654
wenzelm@61382
   655
subsubsection\<open>Two Distinct Right Cosets are Disjoint\<close>
paulson@14803
   656
paulson@14803
   657
lemma (in group) rcos_equation:
ballarin@27611
   658
  assumes "subgroup H G"
ballarin@27611
   659
  assumes p: "ha \<otimes> a = h \<otimes> b" "a \<in> carrier G" "b \<in> carrier G" "h \<in> H" "ha \<in> H" "hb \<in> H"
ballarin@27611
   660
  shows "hb \<otimes> a \<in> (\<Union>h\<in>H. {h \<otimes> b})"
ballarin@27611
   661
proof -
ballarin@29237
   662
  interpret subgroup H G by fact
ballarin@27611
   663
  from p show ?thesis apply (rule_tac UN_I [of "hb \<otimes> ((inv ha) \<otimes> h)"])
ballarin@27611
   664
    apply (simp add: )
ballarin@27611
   665
    apply (simp add: m_assoc transpose_inv)
ballarin@27611
   666
    done
ballarin@27611
   667
qed
paulson@14803
   668
paulson@14803
   669
lemma (in group) rcos_disjoint:
ballarin@27611
   670
  assumes "subgroup H G"
ballarin@27611
   671
  assumes p: "a \<in> rcosets H" "b \<in> rcosets H" "a\<noteq>b"
ballarin@27611
   672
  shows "a \<inter> b = {}"
ballarin@27611
   673
proof -
ballarin@29237
   674
  interpret subgroup H G by fact
wenzelm@41528
   675
  from p show ?thesis
wenzelm@41528
   676
    apply (simp add: RCOSETS_def r_coset_def)
wenzelm@41528
   677
    apply (blast intro: rcos_equation assms sym)
ballarin@27611
   678
    done
ballarin@27611
   679
qed
paulson@14803
   680
wenzelm@35849
   681
wenzelm@61382
   682
subsection \<open>Further lemmas for @{text "r_congruent"}\<close>
ballarin@20318
   683
wenzelm@61382
   684
text \<open>The relation is a congruence\<close>
ballarin@20318
   685
ballarin@20318
   686
lemma (in normal) congruent_rcong:
ballarin@20318
   687
  shows "congruent2 (rcong H) (rcong H) (\<lambda>a b. a \<otimes> b <# H)"
ballarin@20318
   688
proof (intro congruent2I[of "carrier G" _ "carrier G" _] equiv_rcong is_group)
ballarin@20318
   689
  fix a b c
ballarin@20318
   690
  assume abrcong: "(a, b) \<in> rcong H"
ballarin@20318
   691
    and ccarr: "c \<in> carrier G"
ballarin@20318
   692
ballarin@20318
   693
  from abrcong
ballarin@20318
   694
      have acarr: "a \<in> carrier G"
ballarin@20318
   695
        and bcarr: "b \<in> carrier G"
ballarin@20318
   696
        and abH: "inv a \<otimes> b \<in> H"
ballarin@20318
   697
      unfolding r_congruent_def
ballarin@20318
   698
      by fast+
ballarin@20318
   699
ballarin@20318
   700
  note carr = acarr bcarr ccarr
ballarin@20318
   701
ballarin@20318
   702
  from ccarr and abH
ballarin@20318
   703
      have "inv c \<otimes> (inv a \<otimes> b) \<otimes> c \<in> H" by (rule inv_op_closed1)
ballarin@20318
   704
  moreover
ballarin@20318
   705
      from carr and inv_closed
ballarin@20318
   706
      have "inv c \<otimes> (inv a \<otimes> b) \<otimes> c = (inv c \<otimes> inv a) \<otimes> (b \<otimes> c)" 
ballarin@20318
   707
      by (force cong: m_assoc)
ballarin@20318
   708
  moreover 
ballarin@20318
   709
      from carr and inv_closed
ballarin@20318
   710
      have "\<dots> = (inv (a \<otimes> c)) \<otimes> (b \<otimes> c)"
ballarin@20318
   711
      by (simp add: inv_mult_group)
ballarin@20318
   712
  ultimately
ballarin@20318
   713
      have "(inv (a \<otimes> c)) \<otimes> (b \<otimes> c) \<in> H" by simp
ballarin@20318
   714
  from carr and this
ballarin@20318
   715
     have "(b \<otimes> c) \<in> (a \<otimes> c) <# H"
ballarin@20318
   716
     by (simp add: lcos_module_rev[OF is_group])
ballarin@20318
   717
  from carr and this and is_subgroup
ballarin@20318
   718
     show "(a \<otimes> c) <# H = (b \<otimes> c) <# H" by (intro l_repr_independence, simp+)
ballarin@20318
   719
next
ballarin@20318
   720
  fix a b c
ballarin@20318
   721
  assume abrcong: "(a, b) \<in> rcong H"
ballarin@20318
   722
    and ccarr: "c \<in> carrier G"
ballarin@20318
   723
wenzelm@46721
   724
  from ccarr have "c \<in> Units G" by simp
ballarin@20318
   725
  hence cinvc_one: "inv c \<otimes> c = \<one>" by (rule Units_l_inv)
ballarin@20318
   726
ballarin@20318
   727
  from abrcong
ballarin@20318
   728
      have acarr: "a \<in> carrier G"
ballarin@20318
   729
       and bcarr: "b \<in> carrier G"
ballarin@20318
   730
       and abH: "inv a \<otimes> b \<in> H"
ballarin@20318
   731
      by (unfold r_congruent_def, fast+)
ballarin@20318
   732
ballarin@20318
   733
  note carr = acarr bcarr ccarr
ballarin@20318
   734
ballarin@20318
   735
  from carr and inv_closed
ballarin@20318
   736
     have "inv a \<otimes> b = inv a \<otimes> (\<one> \<otimes> b)" by simp
ballarin@20318
   737
  also from carr and inv_closed
ballarin@20318
   738
      have "\<dots> = inv a \<otimes> (inv c \<otimes> c) \<otimes> b" by simp
ballarin@20318
   739
  also from carr and inv_closed
ballarin@20318
   740
      have "\<dots> = (inv a \<otimes> inv c) \<otimes> (c \<otimes> b)" by (force cong: m_assoc)
ballarin@20318
   741
  also from carr and inv_closed
ballarin@20318
   742
      have "\<dots> = inv (c \<otimes> a) \<otimes> (c \<otimes> b)" by (simp add: inv_mult_group)
ballarin@20318
   743
  finally
ballarin@20318
   744
      have "inv a \<otimes> b = inv (c \<otimes> a) \<otimes> (c \<otimes> b)" .
ballarin@20318
   745
  from abH and this
ballarin@20318
   746
      have "inv (c \<otimes> a) \<otimes> (c \<otimes> b) \<in> H" by simp
ballarin@20318
   747
ballarin@20318
   748
  from carr and this
ballarin@20318
   749
     have "(c \<otimes> b) \<in> (c \<otimes> a) <# H"
ballarin@20318
   750
     by (simp add: lcos_module_rev[OF is_group])
ballarin@20318
   751
  from carr and this and is_subgroup
ballarin@20318
   752
     show "(c \<otimes> a) <# H = (c \<otimes> b) <# H" by (intro l_repr_independence, simp+)
ballarin@20318
   753
qed
ballarin@20318
   754
paulson@14803
   755
wenzelm@61382
   756
subsection \<open>Order of a Group and Lagrange's Theorem\<close>
paulson@14803
   757
wenzelm@35848
   758
definition
wenzelm@35848
   759
  order :: "('a, 'b) monoid_scheme \<Rightarrow> nat"
wenzelm@35848
   760
  where "order S = card (carrier S)"
paulson@13870
   761
paulson@14963
   762
lemma (in group) rcosets_part_G:
ballarin@27611
   763
  assumes "subgroup H G"
paulson@14963
   764
  shows "\<Union>(rcosets H) = carrier G"
ballarin@27611
   765
proof -
ballarin@29237
   766
  interpret subgroup H G by fact
ballarin@27611
   767
  show ?thesis
ballarin@27611
   768
    apply (rule equalityI)
ballarin@27611
   769
    apply (force simp add: RCOSETS_def r_coset_def)
wenzelm@41528
   770
    apply (auto simp add: RCOSETS_def intro: rcos_self assms)
ballarin@27611
   771
    done
ballarin@27611
   772
qed
paulson@13870
   773
paulson@14747
   774
lemma (in group) cosets_finite:
paulson@14963
   775
     "\<lbrakk>c \<in> rcosets H;  H \<subseteq> carrier G;  finite (carrier G)\<rbrakk> \<Longrightarrow> finite c"
paulson@14963
   776
apply (auto simp add: RCOSETS_def)
paulson@14963
   777
apply (simp add: r_coset_subset_G [THEN finite_subset])
paulson@13870
   778
done
paulson@13870
   779
wenzelm@61382
   780
text\<open>The next two lemmas support the proof of @{text card_cosets_equal}.\<close>
paulson@14747
   781
lemma (in group) inj_on_f:
paulson@14963
   782
    "\<lbrakk>H \<subseteq> carrier G;  a \<in> carrier G\<rbrakk> \<Longrightarrow> inj_on (\<lambda>y. y \<otimes> inv a) (H #> a)"
paulson@13870
   783
apply (rule inj_onI)
paulson@13870
   784
apply (subgoal_tac "x \<in> carrier G & y \<in> carrier G")
paulson@13870
   785
 prefer 2 apply (blast intro: r_coset_subset_G [THEN subsetD])
paulson@13870
   786
apply (simp add: subsetD)
paulson@13870
   787
done
paulson@13870
   788
paulson@14747
   789
lemma (in group) inj_on_g:
paulson@14963
   790
    "\<lbrakk>H \<subseteq> carrier G;  a \<in> carrier G\<rbrakk> \<Longrightarrow> inj_on (\<lambda>y. y \<otimes> a) H"
paulson@13870
   791
by (force simp add: inj_on_def subsetD)
paulson@13870
   792
paulson@14747
   793
lemma (in group) card_cosets_equal:
paulson@14963
   794
     "\<lbrakk>c \<in> rcosets H;  H \<subseteq> carrier G; finite(carrier G)\<rbrakk>
paulson@14963
   795
      \<Longrightarrow> card c = card H"
paulson@14963
   796
apply (auto simp add: RCOSETS_def)
paulson@13870
   797
apply (rule card_bij_eq)
wenzelm@14666
   798
     apply (rule inj_on_f, assumption+)
paulson@14747
   799
    apply (force simp add: m_assoc subsetD r_coset_def)
wenzelm@14666
   800
   apply (rule inj_on_g, assumption+)
paulson@14747
   801
  apply (force simp add: m_assoc subsetD r_coset_def)
wenzelm@61382
   802
 txt\<open>The sets @{term "H #> a"} and @{term "H"} are finite.\<close>
paulson@13870
   803
 apply (simp add: r_coset_subset_G [THEN finite_subset])
paulson@13870
   804
apply (blast intro: finite_subset)
paulson@13870
   805
done
paulson@13870
   806
paulson@14963
   807
lemma (in group) rcosets_subset_PowG:
paulson@14963
   808
     "subgroup H G  \<Longrightarrow> rcosets H \<subseteq> Pow(carrier G)"
paulson@14963
   809
apply (simp add: RCOSETS_def)
paulson@13870
   810
apply (blast dest: r_coset_subset_G subgroup.subset)
paulson@13870
   811
done
paulson@13870
   812
paulson@14803
   813
paulson@14803
   814
theorem (in group) lagrange:
paulson@14963
   815
     "\<lbrakk>finite(carrier G); subgroup H G\<rbrakk>
paulson@14963
   816
      \<Longrightarrow> card(rcosets H) * card(H) = order(G)"
paulson@14963
   817
apply (simp (no_asm_simp) add: order_def rcosets_part_G [symmetric])
haftmann@57512
   818
apply (subst mult.commute)
paulson@14803
   819
apply (rule card_partition)
paulson@14963
   820
   apply (simp add: rcosets_subset_PowG [THEN finite_subset])
paulson@14963
   821
  apply (simp add: rcosets_part_G)
paulson@14803
   822
 apply (simp add: card_cosets_equal subgroup.subset)
paulson@14803
   823
apply (simp add: rcos_disjoint)
paulson@14803
   824
done
paulson@14803
   825
paulson@14803
   826
wenzelm@61382
   827
subsection \<open>Quotient Groups: Factorization of a Group\<close>
paulson@13870
   828
wenzelm@35848
   829
definition
wenzelm@35848
   830
  FactGroup :: "[('a,'b) monoid_scheme, 'a set] \<Rightarrow> ('a set) monoid" (infixl "Mod" 65)
wenzelm@61382
   831
    --\<open>Actually defined for groups rather than monoids\<close>
wenzelm@35848
   832
   where "FactGroup G H = \<lparr>carrier = rcosets\<^bsub>G\<^esub> H, mult = set_mult G, one = H\<rparr>"
paulson@14747
   833
paulson@14963
   834
lemma (in normal) setmult_closed:
paulson@14963
   835
     "\<lbrakk>K1 \<in> rcosets H; K2 \<in> rcosets H\<rbrakk> \<Longrightarrow> K1 <#> K2 \<in> rcosets H"
paulson@14963
   836
by (auto simp add: rcos_sum RCOSETS_def)
paulson@13870
   837
paulson@14963
   838
lemma (in normal) setinv_closed:
paulson@14963
   839
     "K \<in> rcosets H \<Longrightarrow> set_inv K \<in> rcosets H"
paulson@14963
   840
by (auto simp add: rcos_inv RCOSETS_def)
ballarin@13889
   841
paulson@14963
   842
lemma (in normal) rcosets_assoc:
paulson@14963
   843
     "\<lbrakk>M1 \<in> rcosets H; M2 \<in> rcosets H; M3 \<in> rcosets H\<rbrakk>
paulson@14963
   844
      \<Longrightarrow> M1 <#> M2 <#> M3 = M1 <#> (M2 <#> M3)"
paulson@14963
   845
by (auto simp add: RCOSETS_def rcos_sum m_assoc)
paulson@13870
   846
paulson@14963
   847
lemma (in subgroup) subgroup_in_rcosets:
ballarin@27611
   848
  assumes "group G"
paulson@14963
   849
  shows "H \<in> rcosets H"
ballarin@13889
   850
proof -
ballarin@29237
   851
  interpret group G by fact
wenzelm@26203
   852
  from _ subgroup_axioms have "H #> \<one> = H"
wenzelm@23350
   853
    by (rule coset_join2) auto
ballarin@13889
   854
  then show ?thesis
paulson@14963
   855
    by (auto simp add: RCOSETS_def)
ballarin@13889
   856
qed
ballarin@13889
   857
paulson@14963
   858
lemma (in normal) rcosets_inv_mult_group_eq:
paulson@14963
   859
     "M \<in> rcosets H \<Longrightarrow> set_inv M <#> M = H"
wenzelm@41528
   860
by (auto simp add: RCOSETS_def rcos_inv rcos_sum subgroup.subset normal.axioms normal_axioms)
ballarin@13889
   861
paulson@14963
   862
theorem (in normal) factorgroup_is_group:
paulson@14963
   863
  "group (G Mod H)"
wenzelm@14666
   864
apply (simp add: FactGroup_def)
ballarin@13936
   865
apply (rule groupI)
paulson@14747
   866
    apply (simp add: setmult_closed)
paulson@14963
   867
   apply (simp add: normal_imp_subgroup subgroup_in_rcosets [OF is_group])
paulson@14963
   868
  apply (simp add: restrictI setmult_closed rcosets_assoc)
ballarin@13889
   869
 apply (simp add: normal_imp_subgroup
paulson@14963
   870
                  subgroup_in_rcosets rcosets_mult_eq)
paulson@14963
   871
apply (auto dest: rcosets_inv_mult_group_eq simp add: setinv_closed)
ballarin@13889
   872
done
ballarin@13889
   873
paulson@14803
   874
lemma mult_FactGroup [simp]: "X \<otimes>\<^bsub>(G Mod H)\<^esub> X' = X <#>\<^bsub>G\<^esub> X'"
paulson@14803
   875
  by (simp add: FactGroup_def) 
paulson@14803
   876
paulson@14963
   877
lemma (in normal) inv_FactGroup:
paulson@14963
   878
     "X \<in> carrier (G Mod H) \<Longrightarrow> inv\<^bsub>G Mod H\<^esub> X = set_inv X"
paulson@14747
   879
apply (rule group.inv_equality [OF factorgroup_is_group]) 
paulson@14963
   880
apply (simp_all add: FactGroup_def setinv_closed rcosets_inv_mult_group_eq)
paulson@14747
   881
done
paulson@14747
   882
wenzelm@61382
   883
text\<open>The coset map is a homomorphism from @{term G} to the quotient group
wenzelm@61382
   884
  @{term "G Mod H"}\<close>
paulson@14963
   885
lemma (in normal) r_coset_hom_Mod:
paulson@14963
   886
  "(\<lambda>a. H #> a) \<in> hom G (G Mod H)"
paulson@14963
   887
  by (auto simp add: FactGroup_def RCOSETS_def Pi_def hom_def rcos_sum)
paulson@14747
   888
paulson@14963
   889
 
wenzelm@61382
   890
subsection\<open>The First Isomorphism Theorem\<close>
paulson@14803
   891
wenzelm@61382
   892
text\<open>The quotient by the kernel of a homomorphism is isomorphic to the 
wenzelm@61382
   893
  range of that homomorphism.\<close>
paulson@14803
   894
wenzelm@35848
   895
definition
wenzelm@35848
   896
  kernel :: "('a, 'm) monoid_scheme \<Rightarrow> ('b, 'n) monoid_scheme \<Rightarrow>  ('a \<Rightarrow> 'b) \<Rightarrow> 'a set"
wenzelm@61382
   897
    --\<open>the kernel of a homomorphism\<close>
wenzelm@35848
   898
  where "kernel G H h = {x. x \<in> carrier G & h x = \<one>\<^bsub>H\<^esub>}"
paulson@14803
   899
paulson@14803
   900
lemma (in group_hom) subgroup_kernel: "subgroup (kernel G H h) G"
paulson@14963
   901
apply (rule subgroup.intro) 
wenzelm@41528
   902
apply (auto simp add: kernel_def group.intro is_group) 
paulson@14803
   903
done
paulson@14803
   904
wenzelm@61382
   905
text\<open>The kernel of a homomorphism is a normal subgroup\<close>
paulson@14963
   906
lemma (in group_hom) normal_kernel: "(kernel G H h) \<lhd> G"
ballarin@19931
   907
apply (simp add: G.normal_inv_iff subgroup_kernel)
ballarin@19931
   908
apply (simp add: kernel_def)
paulson@14803
   909
done
paulson@14803
   910
paulson@14803
   911
lemma (in group_hom) FactGroup_nonempty:
paulson@14803
   912
  assumes X: "X \<in> carrier (G Mod kernel G H h)"
paulson@14803
   913
  shows "X \<noteq> {}"
paulson@14803
   914
proof -
paulson@14803
   915
  from X
paulson@14803
   916
  obtain g where "g \<in> carrier G" 
paulson@14803
   917
             and "X = kernel G H h #> g"
paulson@14963
   918
    by (auto simp add: FactGroup_def RCOSETS_def)
paulson@14803
   919
  thus ?thesis 
paulson@14963
   920
   by (auto simp add: kernel_def r_coset_def image_def intro: hom_one)
paulson@14803
   921
qed
paulson@14803
   922
paulson@14803
   923
haftmann@39910
   924
lemma (in group_hom) FactGroup_the_elem_mem:
paulson@14803
   925
  assumes X: "X \<in> carrier (G Mod (kernel G H h))"
haftmann@39910
   926
  shows "the_elem (h`X) \<in> carrier H"
paulson@14803
   927
proof -
paulson@14803
   928
  from X
paulson@14803
   929
  obtain g where g: "g \<in> carrier G" 
paulson@14803
   930
             and "X = kernel G H h #> g"
paulson@14963
   931
    by (auto simp add: FactGroup_def RCOSETS_def)
paulson@14963
   932
  hence "h ` X = {h g}" by (auto simp add: kernel_def r_coset_def image_def g)
paulson@14803
   933
  thus ?thesis by (auto simp add: g)
paulson@14803
   934
qed
paulson@14803
   935
paulson@14803
   936
lemma (in group_hom) FactGroup_hom:
haftmann@39910
   937
     "(\<lambda>X. the_elem (h`X)) \<in> hom (G Mod (kernel G H h)) H"
haftmann@39910
   938
apply (simp add: hom_def FactGroup_the_elem_mem normal.factorgroup_is_group [OF normal_kernel] group.axioms monoid.m_closed)
nipkow@31727
   939
proof (intro ballI)
paulson@14803
   940
  fix X and X'
paulson@14803
   941
  assume X:  "X  \<in> carrier (G Mod kernel G H h)"
paulson@14803
   942
     and X': "X' \<in> carrier (G Mod kernel G H h)"
paulson@14803
   943
  then
paulson@14803
   944
  obtain g and g'
paulson@14803
   945
           where "g \<in> carrier G" and "g' \<in> carrier G" 
paulson@14803
   946
             and "X = kernel G H h #> g" and "X' = kernel G H h #> g'"
paulson@14963
   947
    by (auto simp add: FactGroup_def RCOSETS_def)
paulson@14803
   948
  hence all: "\<forall>x\<in>X. h x = h g" "\<forall>x\<in>X'. h x = h g'" 
paulson@14803
   949
    and Xsub: "X \<subseteq> carrier G" and X'sub: "X' \<subseteq> carrier G"
paulson@14803
   950
    by (force simp add: kernel_def r_coset_def image_def)+
paulson@14803
   951
  hence "h ` (X <#> X') = {h g \<otimes>\<^bsub>H\<^esub> h g'}" using X X'
paulson@14803
   952
    by (auto dest!: FactGroup_nonempty
paulson@14803
   953
             simp add: set_mult_def image_eq_UN 
paulson@14803
   954
                       subsetD [OF Xsub] subsetD [OF X'sub]) 
haftmann@39910
   955
  thus "the_elem (h ` (X <#> X')) = the_elem (h ` X) \<otimes>\<^bsub>H\<^esub> the_elem (h ` X')"
nipkow@31727
   956
    by (simp add: all image_eq_UN FactGroup_nonempty X X')
paulson@14803
   957
qed
paulson@14803
   958
paulson@14963
   959
wenzelm@61382
   960
text\<open>Lemma for the following injectivity result\<close>
paulson@14803
   961
lemma (in group_hom) FactGroup_subset:
paulson@14963
   962
     "\<lbrakk>g \<in> carrier G; g' \<in> carrier G; h g = h g'\<rbrakk>
paulson@14963
   963
      \<Longrightarrow>  kernel G H h #> g \<subseteq> kernel G H h #> g'"
wenzelm@26310
   964
apply (clarsimp simp add: kernel_def r_coset_def image_def)
paulson@14803
   965
apply (rename_tac y)  
paulson@14803
   966
apply (rule_tac x="y \<otimes> g \<otimes> inv g'" in exI) 
wenzelm@26310
   967
apply (simp add: G.m_assoc) 
paulson@14803
   968
done
paulson@14803
   969
paulson@14803
   970
lemma (in group_hom) FactGroup_inj_on:
haftmann@39910
   971
     "inj_on (\<lambda>X. the_elem (h ` X)) (carrier (G Mod kernel G H h))"
paulson@14803
   972
proof (simp add: inj_on_def, clarify) 
paulson@14803
   973
  fix X and X'
paulson@14803
   974
  assume X:  "X  \<in> carrier (G Mod kernel G H h)"
paulson@14803
   975
     and X': "X' \<in> carrier (G Mod kernel G H h)"
paulson@14803
   976
  then
paulson@14803
   977
  obtain g and g'
paulson@14803
   978
           where gX: "g \<in> carrier G"  "g' \<in> carrier G" 
paulson@14803
   979
              "X = kernel G H h #> g" "X' = kernel G H h #> g'"
paulson@14963
   980
    by (auto simp add: FactGroup_def RCOSETS_def)
paulson@14803
   981
  hence all: "\<forall>x\<in>X. h x = h g" "\<forall>x\<in>X'. h x = h g'" 
paulson@14803
   982
    by (force simp add: kernel_def r_coset_def image_def)+
haftmann@39910
   983
  assume "the_elem (h ` X) = the_elem (h ` X')"
paulson@14803
   984
  hence h: "h g = h g'"
paulson@14803
   985
    by (simp add: image_eq_UN all FactGroup_nonempty X X') 
paulson@14803
   986
  show "X=X'" by (rule equalityI) (simp_all add: FactGroup_subset h gX) 
paulson@14803
   987
qed
paulson@14803
   988
wenzelm@61382
   989
text\<open>If the homomorphism @{term h} is onto @{term H}, then so is the
wenzelm@61382
   990
homomorphism from the quotient group\<close>
paulson@14803
   991
lemma (in group_hom) FactGroup_onto:
paulson@14803
   992
  assumes h: "h ` carrier G = carrier H"
haftmann@39910
   993
  shows "(\<lambda>X. the_elem (h ` X)) ` carrier (G Mod kernel G H h) = carrier H"
paulson@14803
   994
proof
haftmann@39910
   995
  show "(\<lambda>X. the_elem (h ` X)) ` carrier (G Mod kernel G H h) \<subseteq> carrier H"
haftmann@39910
   996
    by (auto simp add: FactGroup_the_elem_mem)
haftmann@39910
   997
  show "carrier H \<subseteq> (\<lambda>X. the_elem (h ` X)) ` carrier (G Mod kernel G H h)"
paulson@14803
   998
  proof
paulson@14803
   999
    fix y
paulson@14803
  1000
    assume y: "y \<in> carrier H"
paulson@14803
  1001
    with h obtain g where g: "g \<in> carrier G" "h g = y"
wenzelm@26310
  1002
      by (blast elim: equalityE) 
nipkow@15120
  1003
    hence "(\<Union>x\<in>kernel G H h #> g. {h x}) = {y}" 
paulson@14803
  1004
      by (auto simp add: y kernel_def r_coset_def) 
haftmann@39910
  1005
    with g show "y \<in> (\<lambda>X. the_elem (h ` X)) ` carrier (G Mod kernel G H h)" 
paulson@14963
  1006
      by (auto intro!: bexI simp add: FactGroup_def RCOSETS_def image_eq_UN)
paulson@14803
  1007
  qed
paulson@14803
  1008
qed
paulson@14803
  1009
paulson@14803
  1010
wenzelm@61382
  1011
text\<open>If @{term h} is a homomorphism from @{term G} onto @{term H}, then the
wenzelm@61382
  1012
 quotient group @{term "G Mod (kernel G H h)"} is isomorphic to @{term H}.\<close>
paulson@14803
  1013
theorem (in group_hom) FactGroup_iso:
paulson@14803
  1014
  "h ` carrier G = carrier H
haftmann@39910
  1015
   \<Longrightarrow> (\<lambda>X. the_elem (h`X)) \<in> (G Mod (kernel G H h)) \<cong> H"
paulson@14803
  1016
by (simp add: iso_def FactGroup_hom FactGroup_inj_on bij_betw_def 
paulson@14803
  1017
              FactGroup_onto) 
paulson@14803
  1018
paulson@14963
  1019
paulson@13870
  1020
end