src/HOL/Algebra/Coset.thy
author paulson
Tue Mar 18 18:07:06 2003 +0100 (2003-03-18)
changeset 13870 cf947d1ec5ff
child 13889 6676ac2527fa
permissions -rw-r--r--
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
to the new Group setup.

Deleted Ring, Module from GroupTheory

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