src/HOL/Algebra/Coset.thy
author wenzelm
Thu Apr 22 11:01:34 2004 +0200 (2004-04-22)
changeset 14651 02b8f3bcf7fe
parent 14530 e94fd774ecf5
child 14666 65f8680c3f16
permissions -rw-r--r--
improved notation;
paulson@13870
     1
(*  Title:      HOL/GroupTheory/Coset
paulson@13870
     2
    ID:         $Id$
paulson@13870
     3
    Author:     Florian Kammueller, with new proofs by L C Paulson
paulson@13870
     4
*)
paulson@13870
     5
paulson@13870
     6
header{*Theory of Cosets*}
paulson@13870
     7
paulson@13870
     8
theory Coset = Group + Exponent:
paulson@13870
     9
paulson@13870
    10
declare (in group) l_inv [simp]  r_inv [simp] 
paulson@13870
    11
wenzelm@14651
    12
constdefs (structure G)
wenzelm@14651
    13
  r_coset    :: "[_,'a set, 'a] => 'a set"    
wenzelm@14651
    14
   "r_coset G H a == (% x. x \<otimes> a) ` H"
paulson@13870
    15
wenzelm@14651
    16
  l_coset    :: "[_, 'a, 'a set] => 'a set"
wenzelm@14651
    17
   "l_coset G a H == (% x. a \<otimes> x) ` H"
paulson@13870
    18
wenzelm@14651
    19
  rcosets  :: "[_, 'a set] => ('a set)set"
paulson@13870
    20
   "rcosets G H == r_coset G H ` (carrier G)"
paulson@13870
    21
wenzelm@14651
    22
  set_mult  :: "[_, 'a set ,'a set] => 'a set"
wenzelm@14651
    23
   "set_mult G H K == (%(x,y). x \<otimes> y) ` (H \<times> K)"
paulson@13870
    24
wenzelm@14651
    25
  set_inv   :: "[_,'a set] => 'a set"
wenzelm@14651
    26
   "set_inv G H == m_inv G ` H"
paulson@13870
    27
wenzelm@14651
    28
  normal     :: "['a set, _] => bool"       (infixl "<|" 60)
paulson@13870
    29
   "normal H G == subgroup H G & 
paulson@13870
    30
                  (\<forall>x \<in> carrier G. r_coset G H x = l_coset G x H)"
paulson@13870
    31
paulson@13870
    32
syntax (xsymbols)
ballarin@13936
    33
  normal  :: "['a set, ('a,'b) monoid_scheme] => bool" (infixl "\<lhd>" 60)
paulson@13870
    34
paulson@13870
    35
locale coset = group G +
paulson@13870
    36
  fixes rcos      :: "['a set, 'a] => 'a set"     (infixl "#>" 60)
paulson@13870
    37
    and lcos      :: "['a, 'a set] => 'a set"     (infixl "<#" 60)
paulson@13870
    38
    and setmult   :: "['a set, 'a set] => 'a set" (infixl "<#>" 60)
paulson@13870
    39
  defines rcos_def: "H #> x == r_coset G H x"
paulson@13870
    40
      and lcos_def: "x <# H == l_coset G x H"
paulson@13870
    41
      and setmult_def: "H <#> K == set_mult G H K"
paulson@13870
    42
ballarin@13889
    43
text {*
ballarin@13889
    44
  Locale @{term coset} provides only syntax.
ballarin@13889
    45
  Logically, groups are cosets.
ballarin@13889
    46
*}
ballarin@13889
    47
lemma (in group) is_coset:
ballarin@13889
    48
  "coset G"
ballarin@14254
    49
  by (rule coset.intro)
paulson@13870
    50
paulson@13870
    51
text{*Lemmas useful for Sylow's Theorem*}
paulson@13870
    52
paulson@13870
    53
lemma card_inj:
paulson@13870
    54
     "[|f \<in> A\<rightarrow>B; inj_on f A; finite A; finite B|] ==> card(A) <= card(B)"
paulson@13870
    55
apply (rule card_inj_on_le)
paulson@13870
    56
apply (auto simp add: Pi_def)
paulson@13870
    57
done
paulson@13870
    58
paulson@13870
    59
lemma card_bij: 
paulson@13870
    60
     "[|f \<in> A\<rightarrow>B; inj_on f A; 
paulson@13870
    61
        g \<in> B\<rightarrow>A; inj_on g B; finite A; finite B|] ==> card(A) = card(B)"
paulson@13870
    62
by (blast intro: card_inj order_antisym) 
paulson@13870
    63
paulson@13870
    64
paulson@13870
    65
subsection{*Lemmas Using Locale Constants*}
paulson@13870
    66
paulson@13870
    67
lemma (in coset) r_coset_eq: "H #> a = {b . \<exists>h\<in>H. h \<otimes> a = b}"
paulson@13870
    68
by (auto simp add: rcos_def r_coset_def)
paulson@13870
    69
paulson@13870
    70
lemma (in coset) l_coset_eq: "a <# H = {b . \<exists>h\<in>H. a \<otimes> h = b}"
paulson@13870
    71
by (auto simp add: lcos_def l_coset_def)
paulson@13870
    72
paulson@13870
    73
lemma (in coset) setrcos_eq: "rcosets G H = {C . \<exists>a\<in>carrier G. C = H #> a}"
paulson@13870
    74
by (auto simp add: rcosets_def rcos_def)
paulson@13870
    75
paulson@13870
    76
lemma (in coset) set_mult_eq: "H <#> K = {c . \<exists>h\<in>H. \<exists>k\<in>K. c = h \<otimes> k}"
paulson@13870
    77
by (simp add: setmult_def set_mult_def image_def)
paulson@13870
    78
paulson@13870
    79
lemma (in coset) coset_mult_assoc:
paulson@13870
    80
     "[| M <= carrier G; g \<in> carrier G; h \<in> carrier G |]  
paulson@13870
    81
      ==> (M #> g) #> h = M #> (g \<otimes> h)"
paulson@13870
    82
by (force simp add: r_coset_eq m_assoc)
paulson@13870
    83
paulson@13870
    84
lemma (in coset) coset_mult_one [simp]: "M <= carrier G ==> M #> \<one> = M"
paulson@13870
    85
by (force simp add: r_coset_eq)
paulson@13870
    86
paulson@13870
    87
lemma (in coset) coset_mult_inv1:
paulson@13870
    88
     "[| M #> (x \<otimes> (inv y)) = M;  x \<in> carrier G ; y \<in> carrier G; 
paulson@13870
    89
         M <= carrier G |] ==> M #> x = M #> y"
paulson@13870
    90
apply (erule subst [of concl: "%z. M #> x = z #> y"])
paulson@13870
    91
apply (simp add: coset_mult_assoc m_assoc)
paulson@13870
    92
done
paulson@13870
    93
paulson@13870
    94
lemma (in coset) coset_mult_inv2:
paulson@13870
    95
     "[| M #> x = M #> y;  x \<in> carrier G;  y \<in> carrier G;  M <= carrier G |]  
paulson@13870
    96
      ==> M #> (x \<otimes> (inv y)) = M "
paulson@13870
    97
apply (simp add: coset_mult_assoc [symmetric])
paulson@13870
    98
apply (simp add: coset_mult_assoc)
paulson@13870
    99
done
paulson@13870
   100
paulson@13870
   101
lemma (in coset) coset_join1:
paulson@13870
   102
     "[| H #> x = H;  x \<in> carrier G;  subgroup H G |] ==> x\<in>H"
paulson@13870
   103
apply (erule subst)
paulson@13870
   104
apply (simp add: r_coset_eq)
paulson@13870
   105
apply (blast intro: l_one subgroup.one_closed)
paulson@13870
   106
done
paulson@13870
   107
paulson@13870
   108
text{*Locales don't currently work with @{text rule_tac}, so we
paulson@13870
   109
must prove this lemma separately.*}
paulson@13870
   110
lemma (in coset) solve_equation:
paulson@13870
   111
    "\<lbrakk>subgroup H G; x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> \<exists>h\<in>H. h \<otimes> x = y"
paulson@13870
   112
apply (rule bexI [of _ "y \<otimes> (inv x)"])
paulson@13870
   113
apply (auto simp add: subgroup.m_closed subgroup.m_inv_closed m_assoc 
paulson@13870
   114
                      subgroup.subset [THEN subsetD])
paulson@13870
   115
done
paulson@13870
   116
paulson@13870
   117
lemma (in coset) coset_join2:
paulson@13870
   118
     "[| x \<in> carrier G;  subgroup H G;  x\<in>H |] ==> H #> x = H"
paulson@13870
   119
by (force simp add: subgroup.m_closed r_coset_eq solve_equation)
paulson@13870
   120
paulson@13870
   121
lemma (in coset) r_coset_subset_G:
paulson@13870
   122
     "[| H <= carrier G; x \<in> carrier G |] ==> H #> x <= carrier G"
paulson@13870
   123
by (auto simp add: r_coset_eq)
paulson@13870
   124
paulson@13870
   125
lemma (in coset) rcosI:
paulson@13870
   126
     "[| h \<in> H; H <= carrier G; x \<in> carrier G|] ==> h \<otimes> x \<in> H #> x"
paulson@13870
   127
by (auto simp add: r_coset_eq)
paulson@13870
   128
paulson@13870
   129
lemma (in coset) setrcosI:
paulson@13870
   130
     "[| H <= carrier G; x \<in> carrier G |] ==> H #> x \<in> rcosets G H"
paulson@13870
   131
by (auto simp add: setrcos_eq)
paulson@13870
   132
paulson@13870
   133
paulson@13870
   134
text{*Really needed?*}
paulson@13870
   135
lemma (in coset) transpose_inv:
paulson@13870
   136
     "[| x \<otimes> y = z;  x \<in> carrier G;  y \<in> carrier G;  z \<in> carrier G |]  
paulson@13870
   137
      ==> (inv x) \<otimes> z = y"
paulson@13870
   138
by (force simp add: m_assoc [symmetric])
paulson@13870
   139
paulson@13870
   140
lemma (in coset) repr_independence:
paulson@13870
   141
     "[| y \<in> H #> x;  x \<in> carrier G; subgroup H G |] ==> H #> x = H #> y"
paulson@13870
   142
by (auto simp add: r_coset_eq m_assoc [symmetric] 
paulson@13870
   143
                   subgroup.subset [THEN subsetD]
paulson@13870
   144
                   subgroup.m_closed solve_equation)
paulson@13870
   145
paulson@13870
   146
lemma (in coset) rcos_self: "[| x \<in> carrier G; subgroup H G |] ==> x \<in> H #> x"
paulson@13870
   147
apply (simp add: r_coset_eq)
paulson@13870
   148
apply (blast intro: l_one subgroup.subset [THEN subsetD] 
paulson@13870
   149
                    subgroup.one_closed)
paulson@13870
   150
done
paulson@13870
   151
paulson@13870
   152
paulson@13870
   153
subsection{*normal subgroups*}
paulson@13870
   154
paulson@13870
   155
(*????????????????
ballarin@13936
   156
text "Allows use of theorems proved in the locale coset"
paulson@13870
   157
lemma subgroup_imp_coset: "subgroup H G ==> coset G"
paulson@13870
   158
apply (drule subgroup_imp_group)
paulson@13870
   159
apply (simp add: group_def coset_def)  
paulson@13870
   160
done
paulson@13870
   161
*)
paulson@13870
   162
paulson@13870
   163
lemma normal_imp_subgroup: "H <| G ==> subgroup H G"
paulson@13870
   164
by (simp add: normal_def)
paulson@13870
   165
paulson@13870
   166
paulson@13870
   167
(*????????????????
paulson@13870
   168
lemmas normal_imp_group = normal_imp_subgroup [THEN subgroup_imp_group]
paulson@13870
   169
lemmas normal_imp_coset = normal_imp_subgroup [THEN subgroup_imp_coset]
paulson@13870
   170
*)
paulson@13870
   171
paulson@13870
   172
lemma (in coset) normal_iff:
paulson@13870
   173
     "(H <| G) = (subgroup H G & (\<forall>x \<in> carrier G. H #> x = x <# H))"
paulson@13870
   174
by (simp add: lcos_def rcos_def normal_def)
paulson@13870
   175
paulson@13870
   176
lemma (in coset) normal_imp_rcos_eq_lcos:
paulson@13870
   177
     "[| H <| G; x \<in> carrier G |] ==> H #> x = x <# H"
paulson@13870
   178
by (simp add: lcos_def rcos_def normal_def)
paulson@13870
   179
paulson@13870
   180
lemma (in coset) normal_inv_op_closed1:
paulson@13870
   181
     "\<lbrakk>H \<lhd> G; x \<in> carrier G; h \<in> H\<rbrakk> \<Longrightarrow> (inv x) \<otimes> h \<otimes> x \<in> H"
paulson@13870
   182
apply (auto simp add: l_coset_eq r_coset_eq normal_iff)
paulson@13870
   183
apply (drule bspec, assumption) 
paulson@13870
   184
apply (drule equalityD1 [THEN subsetD], blast, clarify)
paulson@13870
   185
apply (simp add: m_assoc subgroup.subset [THEN subsetD])
paulson@13870
   186
apply (erule subst)
paulson@13870
   187
apply (simp add: m_assoc [symmetric] subgroup.subset [THEN subsetD])
paulson@13870
   188
done
paulson@13870
   189
paulson@13870
   190
lemma (in coset) normal_inv_op_closed2:
paulson@13870
   191
     "\<lbrakk>H \<lhd> G; x \<in> carrier G; h \<in> H\<rbrakk> \<Longrightarrow> x \<otimes> h \<otimes> (inv x) \<in> H"
paulson@13870
   192
apply (drule normal_inv_op_closed1 [of H "(inv x)"]) 
paulson@13870
   193
apply auto
paulson@13870
   194
done
paulson@13870
   195
paulson@13870
   196
lemma (in coset) lcos_m_assoc:
paulson@13870
   197
     "[| M <= carrier G; g \<in> carrier G; h \<in> carrier G |]  
paulson@13870
   198
      ==> g <# (h <# M) = (g \<otimes> h) <# M"
paulson@13870
   199
by (force simp add: l_coset_eq m_assoc)
paulson@13870
   200
paulson@13870
   201
lemma (in coset) lcos_mult_one: "M <= carrier G ==> \<one> <# M = M"
paulson@13870
   202
by (force simp add: l_coset_eq)
paulson@13870
   203
paulson@13870
   204
lemma (in coset) l_coset_subset_G:
paulson@13870
   205
     "[| H <= carrier G; x \<in> carrier G |] ==> x <# H <= carrier G"
paulson@13870
   206
by (auto simp add: l_coset_eq subsetD)
paulson@13870
   207
paulson@14530
   208
lemma (in coset) l_coset_swap:
paulson@14530
   209
     "[| y \<in> x <# H;  x \<in> carrier G;  subgroup H G |] ==> x \<in> y <# H"
paulson@14530
   210
proof (simp add: l_coset_eq)
paulson@14530
   211
  assume "\<exists>h\<in>H. x \<otimes> h = y" 
paulson@14530
   212
    and x: "x \<in> carrier G" 
paulson@14530
   213
    and sb: "subgroup H G"
paulson@14530
   214
  then obtain h' where h': "h' \<in> H & x \<otimes> h' = y" by blast
paulson@14530
   215
  show "\<exists>h\<in>H. y \<otimes> h = x"
paulson@14530
   216
  proof
paulson@14530
   217
    show "y \<otimes> inv h' = x" using h' x sb
paulson@14530
   218
      by (auto simp add: m_assoc subgroup.subset [THEN subsetD])
paulson@14530
   219
    show "inv h' \<in> H" using h' sb
paulson@14530
   220
      by (auto simp add: subgroup.subset [THEN subsetD] subgroup.m_inv_closed)
paulson@14530
   221
  qed
paulson@14530
   222
qed
paulson@14530
   223
paulson@14530
   224
lemma (in coset) l_coset_carrier:
paulson@14530
   225
     "[| y \<in> x <# H;  x \<in> carrier G;  subgroup H G |] ==> y \<in> carrier G"
paulson@14530
   226
by (auto simp add: l_coset_eq m_assoc 
paulson@14530
   227
                   subgroup.subset [THEN subsetD] subgroup.m_closed)
paulson@14530
   228
paulson@14530
   229
lemma (in coset) l_repr_imp_subset:
paulson@14530
   230
  assumes y: "y \<in> x <# H" and x: "x \<in> carrier G" and sb: "subgroup H G" 
paulson@14530
   231
  shows "y <# H \<subseteq> x <# H"
paulson@14530
   232
proof -
paulson@14530
   233
  from y
paulson@14530
   234
  obtain h' where "h' \<in> H" "x \<otimes> h' = y" by (auto simp add: l_coset_eq)
paulson@14530
   235
  thus ?thesis using x sb
paulson@14530
   236
    by (auto simp add: l_coset_eq m_assoc 
paulson@14530
   237
                       subgroup.subset [THEN subsetD] subgroup.m_closed)
paulson@14530
   238
qed
paulson@14530
   239
paulson@13870
   240
lemma (in coset) l_repr_independence:
paulson@14530
   241
  assumes y: "y \<in> x <# H" and x: "x \<in> carrier G" and sb: "subgroup H G" 
paulson@14530
   242
  shows "x <# H = y <# H"
paulson@14530
   243
proof 
paulson@14530
   244
  show "x <# H \<subseteq> y <# H"
paulson@14530
   245
    by (rule l_repr_imp_subset, 
paulson@14530
   246
        (blast intro: l_coset_swap l_coset_carrier y x sb)+)
paulson@14530
   247
  show "y <# H \<subseteq> x <# H" by (rule l_repr_imp_subset [OF y x sb]) 
paulson@14530
   248
qed
paulson@13870
   249
paulson@13870
   250
lemma (in coset) setmult_subset_G:
paulson@13870
   251
     "[| H <= carrier G; K <= carrier G |] ==> H <#> K <= carrier G"
paulson@13870
   252
by (auto simp add: set_mult_eq subsetD)
paulson@13870
   253
paulson@13870
   254
lemma (in coset) subgroup_mult_id: "subgroup H G ==> H <#> H = H"
paulson@13870
   255
apply (auto simp add: subgroup.m_closed set_mult_eq Sigma_def image_def)
paulson@13870
   256
apply (rule_tac x = x in bexI)
paulson@13870
   257
apply (rule bexI [of _ "\<one>"])
paulson@13870
   258
apply (auto simp add: subgroup.m_closed subgroup.one_closed 
paulson@13870
   259
                      r_one subgroup.subset [THEN subsetD])
paulson@13870
   260
done
paulson@13870
   261
paulson@13870
   262
paulson@13870
   263
(* set of inverses of an r_coset *)
paulson@13870
   264
lemma (in coset) rcos_inv:
paulson@13870
   265
  assumes normalHG: "H <| G"
paulson@13870
   266
      and xinG:     "x \<in> carrier G"
paulson@13870
   267
  shows "set_inv G (H #> x) = H #> (inv x)"
paulson@13870
   268
proof -
paulson@13870
   269
  have H_subset: "H <= carrier G" 
paulson@13870
   270
    by (rule subgroup.subset [OF normal_imp_subgroup, OF normalHG])
paulson@13870
   271
  show ?thesis
paulson@13870
   272
  proof (auto simp add: r_coset_eq image_def set_inv_def)
paulson@13870
   273
    fix h
paulson@13870
   274
    assume "h \<in> H"
paulson@13870
   275
      hence "((inv x) \<otimes> (inv h) \<otimes> x) \<otimes> inv x = inv (h \<otimes> x)"
paulson@13870
   276
	by (simp add: xinG m_assoc inv_mult_group H_subset [THEN subsetD])
paulson@13870
   277
      thus "\<exists>j\<in>H. j \<otimes> inv x = inv (h \<otimes> x)" 
paulson@13870
   278
       using prems
paulson@13870
   279
	by (blast intro: normal_inv_op_closed1 normal_imp_subgroup 
paulson@13870
   280
			 subgroup.m_inv_closed)
paulson@13870
   281
  next
paulson@13870
   282
    fix h
paulson@13870
   283
    assume "h \<in> H"
paulson@13870
   284
      hence eq: "(x \<otimes> (inv h) \<otimes> (inv x)) \<otimes> x = x \<otimes> inv h"
paulson@13870
   285
        by (simp add: xinG m_assoc H_subset [THEN subsetD])
paulson@13870
   286
      hence "(\<exists>j\<in>H. j \<otimes> x = inv  (h \<otimes> (inv x))) \<and> h \<otimes> inv x = inv (inv (h \<otimes> (inv x)))"
paulson@13870
   287
       using prems
paulson@13870
   288
	by (simp add: m_assoc inv_mult_group H_subset [THEN subsetD],
paulson@13870
   289
            blast intro: eq normal_inv_op_closed2 normal_imp_subgroup 
paulson@13870
   290
			 subgroup.m_inv_closed)
paulson@13870
   291
      thus "\<exists>y. (\<exists>h\<in>H. h \<otimes> x = y) \<and> h \<otimes> inv x = inv y" ..
paulson@13870
   292
  qed
paulson@13870
   293
qed
paulson@13870
   294
paulson@13870
   295
(*The old proof is something like this, but the rule_tac calls make
paulson@13870
   296
illegal references to implicit structures.
paulson@13870
   297
lemma (in coset) rcos_inv:
paulson@13870
   298
     "[| H <| G; x \<in> carrier G |] ==> set_inv G (H #> x) = H #> (inv x)"
paulson@13870
   299
apply (frule normal_imp_subgroup)
paulson@13870
   300
apply (auto simp add: r_coset_eq image_def set_inv_def)
paulson@13870
   301
apply (rule_tac x = "(inv x) \<otimes> (inv h) \<otimes> x" in bexI)
paulson@13870
   302
apply (simp add: m_assoc inv_mult_group subgroup.subset [THEN subsetD])
paulson@13870
   303
apply (simp add: subgroup.m_inv_closed, assumption+)
paulson@13870
   304
apply (rule_tac x = "inv  (h \<otimes> (inv x)) " in exI)
paulson@13870
   305
apply (simp add: inv_mult_group subgroup.subset [THEN subsetD])
paulson@13870
   306
apply (rule_tac x = "x \<otimes> (inv h) \<otimes> (inv x)" in bexI)
paulson@13870
   307
apply (simp add: m_assoc subgroup.subset [THEN subsetD])
paulson@13870
   308
apply (simp add: normal_inv_op_closed2 subgroup.m_inv_closed)
paulson@13870
   309
done
paulson@13870
   310
*)
paulson@13870
   311
paulson@13870
   312
lemma (in coset) rcos_inv2:
paulson@13870
   313
     "[| H <| G; K \<in> rcosets G H; x \<in> K |] ==> set_inv G K = H #> (inv x)"
paulson@13870
   314
apply (simp add: setrcos_eq, clarify)
paulson@13870
   315
apply (subgoal_tac "x : carrier G")
paulson@13870
   316
 prefer 2
paulson@13870
   317
 apply (blast dest: r_coset_subset_G subgroup.subset normal_imp_subgroup) 
paulson@13870
   318
apply (drule repr_independence)
paulson@13870
   319
  apply assumption
paulson@13870
   320
 apply (erule normal_imp_subgroup)
paulson@13870
   321
apply (simp add: rcos_inv)
paulson@13870
   322
done
paulson@13870
   323
paulson@13870
   324
paulson@13870
   325
(* some rules for <#> with #> or <# *)
paulson@13870
   326
lemma (in coset) setmult_rcos_assoc:
paulson@13870
   327
     "[| H <= carrier G; K <= carrier G; x \<in> carrier G |] 
paulson@13870
   328
      ==> H <#> (K #> x) = (H <#> K) #> x"
paulson@13870
   329
apply (auto simp add: rcos_def r_coset_def setmult_def set_mult_def)
paulson@13870
   330
apply (force simp add: m_assoc)+
paulson@13870
   331
done
paulson@13870
   332
paulson@13870
   333
lemma (in coset) rcos_assoc_lcos:
paulson@13870
   334
     "[| H <= carrier G; K <= carrier G; x \<in> carrier G |] 
paulson@13870
   335
      ==> (H #> x) <#> K = H <#> (x <# K)"
paulson@13870
   336
apply (auto simp add: rcos_def r_coset_def lcos_def l_coset_def 
paulson@13870
   337
                      setmult_def set_mult_def Sigma_def image_def)
paulson@13870
   338
apply (force intro!: exI bexI simp add: m_assoc)+
paulson@13870
   339
done
paulson@13870
   340
paulson@13870
   341
lemma (in coset) rcos_mult_step1:
paulson@13870
   342
     "[| H <| G; x \<in> carrier G; y \<in> carrier G |] 
paulson@13870
   343
      ==> (H #> x) <#> (H #> y) = (H <#> (x <# H)) #> y"
paulson@13870
   344
by (simp add: setmult_rcos_assoc normal_imp_subgroup [THEN subgroup.subset]
paulson@13870
   345
              r_coset_subset_G l_coset_subset_G rcos_assoc_lcos)
paulson@13870
   346
paulson@13870
   347
lemma (in coset) rcos_mult_step2:
paulson@13870
   348
     "[| H <| G; x \<in> carrier G; y \<in> carrier G |] 
paulson@13870
   349
      ==> (H <#> (x <# H)) #> y = (H <#> (H #> x)) #> y"
paulson@13870
   350
by (simp add: normal_imp_rcos_eq_lcos)
paulson@13870
   351
paulson@13870
   352
lemma (in coset) rcos_mult_step3:
paulson@13870
   353
     "[| H <| G; x \<in> carrier G; y \<in> carrier G |] 
paulson@13870
   354
      ==> (H <#> (H #> x)) #> y = H #> (x \<otimes> y)"
paulson@13870
   355
by (simp add: setmult_rcos_assoc r_coset_subset_G coset_mult_assoc
paulson@13870
   356
              setmult_subset_G  subgroup_mult_id
paulson@13870
   357
              subgroup.subset normal_imp_subgroup)
paulson@13870
   358
paulson@13870
   359
lemma (in coset) rcos_sum:
paulson@13870
   360
     "[| H <| G; x \<in> carrier G; y \<in> carrier G |] 
paulson@13870
   361
      ==> (H #> x) <#> (H #> y) = H #> (x \<otimes> y)"
paulson@13870
   362
by (simp add: rcos_mult_step1 rcos_mult_step2 rcos_mult_step3)
paulson@13870
   363
paulson@13870
   364
(*generalizes subgroup_mult_id*)
paulson@13870
   365
lemma (in coset) setrcos_mult_eq: "[|H <| G; M \<in> rcosets G H|] ==> H <#> M = M"
paulson@13870
   366
by (auto simp add: setrcos_eq normal_imp_subgroup subgroup.subset
paulson@13870
   367
                   setmult_rcos_assoc subgroup_mult_id)
paulson@13870
   368
paulson@13870
   369
paulson@13870
   370
subsection{*Lemmas Leading to Lagrange's Theorem*}
paulson@13870
   371
paulson@13870
   372
lemma (in coset) setrcos_part_G: "subgroup H G ==> \<Union> rcosets G H = carrier G"
paulson@13870
   373
apply (rule equalityI)
paulson@13870
   374
apply (force simp add: subgroup.subset [THEN subsetD] 
paulson@13870
   375
                       setrcos_eq r_coset_eq)
paulson@13870
   376
apply (auto simp add: setrcos_eq subgroup.subset rcos_self)
paulson@13870
   377
done
paulson@13870
   378
paulson@13870
   379
lemma (in coset) cosets_finite:
paulson@13870
   380
     "[| c \<in> rcosets G H;  H <= carrier G;  finite (carrier G) |] ==> finite c"
paulson@13870
   381
apply (auto simp add: setrcos_eq)
paulson@13870
   382
apply (simp (no_asm_simp) add: r_coset_subset_G [THEN finite_subset])
paulson@13870
   383
done
paulson@13870
   384
paulson@13870
   385
text{*The next two lemmas support the proof of @{text card_cosets_equal},
paulson@13870
   386
since we can't use @{text rule_tac} with explicit terms for @{term f} and
paulson@13870
   387
@{term g}.*}
paulson@13870
   388
lemma (in coset) inj_on_f:
paulson@13870
   389
    "[|H \<subseteq> carrier G;  a \<in> carrier G|] ==> inj_on (\<lambda>y. y \<otimes> inv a) (H #> a)"
paulson@13870
   390
apply (rule inj_onI)
paulson@13870
   391
apply (subgoal_tac "x \<in> carrier G & y \<in> carrier G")
paulson@13870
   392
 prefer 2 apply (blast intro: r_coset_subset_G [THEN subsetD])
paulson@13870
   393
apply (simp add: subsetD)
paulson@13870
   394
done
paulson@13870
   395
paulson@13870
   396
lemma (in coset) inj_on_g:
paulson@13870
   397
    "[|H \<subseteq> carrier G;  a \<in> carrier G|] ==> inj_on (\<lambda>y. y \<otimes> a) H"
paulson@13870
   398
by (force simp add: inj_on_def subsetD)
paulson@13870
   399
paulson@13870
   400
lemma (in coset) card_cosets_equal:
paulson@13870
   401
     "[| c \<in> rcosets G H;  H <= carrier G; finite(carrier G) |] 
paulson@13870
   402
      ==> card c = card H"
paulson@13870
   403
apply (auto simp add: setrcos_eq)
paulson@13870
   404
apply (rule card_bij_eq)
paulson@13870
   405
     apply (rule inj_on_f, assumption+) 
paulson@13870
   406
    apply (force simp add: m_assoc subsetD r_coset_eq)
paulson@13870
   407
   apply (rule inj_on_g, assumption+) 
paulson@13870
   408
  apply (force simp add: m_assoc subsetD r_coset_eq)
paulson@13870
   409
 txt{*The sets @{term "H #> a"} and @{term "H"} are finite.*}
paulson@13870
   410
 apply (simp add: r_coset_subset_G [THEN finite_subset])
paulson@13870
   411
apply (blast intro: finite_subset)
paulson@13870
   412
done
paulson@13870
   413
paulson@13870
   414
subsection{*Two distinct right cosets are disjoint*}
paulson@13870
   415
paulson@13870
   416
lemma (in coset) rcos_equation:
paulson@13870
   417
     "[|subgroup H G;  a \<in> carrier G;  b \<in> carrier G;  ha \<otimes> a = h \<otimes> b;   
paulson@13870
   418
        h \<in> H;  ha \<in> H;  hb \<in> H|]  
paulson@13870
   419
      ==> \<exists>h\<in>H. h \<otimes> b = hb \<otimes> a"
paulson@13870
   420
apply (rule bexI [of _"hb \<otimes> ((inv ha) \<otimes> h)"])
paulson@13870
   421
apply (simp  add: m_assoc transpose_inv subgroup.subset [THEN subsetD])
paulson@13870
   422
apply (simp add: subgroup.m_closed subgroup.m_inv_closed)
paulson@13870
   423
done
paulson@13870
   424
paulson@13870
   425
lemma (in coset) rcos_disjoint:
paulson@13870
   426
     "[|subgroup H G; a \<in> rcosets G H; b \<in> rcosets G H; a\<noteq>b|] ==> a \<inter> b = {}"
paulson@13870
   427
apply (simp add: setrcos_eq r_coset_eq)
paulson@13870
   428
apply (blast intro: rcos_equation sym)
paulson@13870
   429
done
paulson@13870
   430
paulson@13870
   431
lemma (in coset) setrcos_subset_PowG:
paulson@13870
   432
     "subgroup H G  ==> rcosets G H <= Pow(carrier G)"
paulson@13870
   433
apply (simp add: setrcos_eq)
paulson@13870
   434
apply (blast dest: r_coset_subset_G subgroup.subset)
paulson@13870
   435
done
paulson@13870
   436
paulson@13870
   437
subsection {*Factorization of a Group*}
paulson@13870
   438
paulson@13870
   439
constdefs
ballarin@13936
   440
  FactGroup :: "[('a,'b) monoid_scheme, 'a set] => ('a set) monoid"
paulson@13870
   441
     (infixl "Mod" 60)
paulson@13870
   442
   "FactGroup G H ==
paulson@13870
   443
      (| carrier = rcosets G H,
paulson@13870
   444
	 mult = (%X: rcosets G H. %Y: rcosets G H. set_mult G X Y),
ballarin@13936
   445
	 one = H (*,
ballarin@13936
   446
	 m_inv = (%X: rcosets G H. set_inv G X) *) |)"
paulson@13870
   447
paulson@13870
   448
lemma (in coset) setmult_closed:
paulson@13870
   449
     "[| H <| G; K1 \<in> rcosets G H; K2 \<in> rcosets G H |] 
paulson@13870
   450
      ==> K1 <#> K2 \<in> rcosets G H"
paulson@13870
   451
by (auto simp add: normal_imp_subgroup [THEN subgroup.subset] 
paulson@13870
   452
                   rcos_sum setrcos_eq)
paulson@13870
   453
ballarin@13889
   454
lemma (in group) setinv_closed:
ballarin@13889
   455
     "[| H <| G; K \<in> rcosets G H |] ==> set_inv G K \<in> rcosets G H"
ballarin@13889
   456
by (auto simp add:  normal_imp_subgroup
ballarin@13889
   457
                 subgroup.subset coset.rcos_inv [OF is_coset]
ballarin@13889
   458
                 coset.setrcos_eq [OF is_coset])
ballarin@13889
   459
paulson@13870
   460
(*
ballarin@13889
   461
The old version is no longer valid: "group G" has to be an explicit premise.
ballarin@13889
   462
paulson@13870
   463
lemma setinv_closed:
paulson@13870
   464
     "[| H <| G; K \<in> rcosets G H |] ==> set_inv G K \<in> rcosets G H"
paulson@13870
   465
by (auto simp add:  normal_imp_subgroup
paulson@13870
   466
                   subgroup.subset coset.rcos_inv coset.setrcos_eq)
paulson@13870
   467
*)
paulson@13870
   468
paulson@13870
   469
lemma (in coset) setrcos_assoc:
paulson@13870
   470
     "[|H <| G; M1 \<in> rcosets G H; M2 \<in> rcosets G H; M3 \<in> rcosets G H|]   
paulson@13870
   471
      ==> M1 <#> M2 <#> M3 = M1 <#> (M2 <#> M3)"
paulson@13870
   472
by (auto simp add: setrcos_eq rcos_sum normal_imp_subgroup 
paulson@13870
   473
                   subgroup.subset m_assoc)
paulson@13870
   474
ballarin@13889
   475
lemma (in group) subgroup_in_rcosets:
ballarin@13889
   476
  "subgroup H G ==> H \<in> rcosets G H"
ballarin@13889
   477
proof -
ballarin@13889
   478
  assume sub: "subgroup H G"
ballarin@13889
   479
  have "r_coset G H \<one> = H"
ballarin@13889
   480
    by (rule coset.coset_join2)
ballarin@13889
   481
      (auto intro: sub subgroup.one_closed is_coset)
ballarin@13889
   482
  then show ?thesis
ballarin@13889
   483
    by (auto simp add: coset.setrcos_eq [OF is_coset])
ballarin@13889
   484
qed
ballarin@13889
   485
ballarin@13889
   486
(*
ballarin@13889
   487
lemma subgroup_in_rcosets:
ballarin@13889
   488
  "subgroup H G ==> H \<in> rcosets G H"
paulson@13870
   489
apply (frule subgroup_imp_coset) 
paulson@13870
   490
apply (frule subgroup_imp_group) 
paulson@13870
   491
apply (simp add: coset.setrcos_eq)
paulson@13870
   492
apply (blast del: equalityI 
paulson@13870
   493
             intro!: group.subgroup.one_closed group.one_closed
paulson@13870
   494
                     coset.coset_join2 [symmetric])
paulson@13870
   495
done
paulson@13870
   496
*)
paulson@13870
   497
paulson@13870
   498
lemma (in coset) setrcos_inv_mult_group_eq:
paulson@13870
   499
     "[|H <| G; M \<in> rcosets G H|] ==> set_inv G M <#> M = H"
paulson@13870
   500
by (auto simp add: setrcos_eq rcos_inv rcos_sum normal_imp_subgroup 
paulson@13870
   501
                   subgroup.subset)
ballarin@13940
   502
(*
ballarin@13889
   503
lemma (in group) factorgroup_is_magma:
ballarin@13889
   504
  "H <| G ==> magma (G Mod H)"
ballarin@13889
   505
  by rule (simp add: FactGroup_def coset.setmult_closed [OF is_coset])
ballarin@13889
   506
ballarin@13889
   507
lemma (in group) factorgroup_semigroup_axioms:
ballarin@13889
   508
  "H <| G ==> semigroup_axioms (G Mod H)"
ballarin@13889
   509
  by rule (simp add: FactGroup_def coset.setrcos_assoc [OF is_coset]
ballarin@13889
   510
    coset.setmult_closed [OF is_coset])
ballarin@13940
   511
*)
ballarin@13889
   512
theorem (in group) factorgroup_is_group:
ballarin@13889
   513
  "H <| G ==> group (G Mod H)"
ballarin@13889
   514
apply (insert is_coset) 
ballarin@13889
   515
apply (simp add: FactGroup_def) 
ballarin@13936
   516
apply (rule groupI)
ballarin@13936
   517
    apply (simp add: coset.setmult_closed)
ballarin@13936
   518
   apply (simp add: normal_imp_subgroup subgroup_in_rcosets)
ballarin@13889
   519
  apply (simp add: restrictI coset.setmult_closed coset.setrcos_assoc)
ballarin@13889
   520
 apply (simp add: normal_imp_subgroup
ballarin@13889
   521
   subgroup_in_rcosets coset.setrcos_mult_eq)
ballarin@13936
   522
apply (auto dest: coset.setrcos_inv_mult_group_eq simp add: setinv_closed)
ballarin@13889
   523
done
ballarin@13889
   524
paulson@13870
   525
end