src/HOL/Algebra/Coset.thy
author ballarin
Thu Nov 06 14:18:05 2003 +0100 (2003-11-06)
changeset 14254 342634f38451
parent 13943 83d842ccd4aa
child 14530 e94fd774ecf5
permissions -rw-r--r--
Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by
default.
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
ballarin@13936
    13
  r_coset    :: "[('a,'b) monoid_scheme,'a set, 'a] => 'a set"    
paulson@13870
    14
   "r_coset G H a == (% x. (mult G) x a) ` H"
paulson@13870
    15
ballarin@13936
    16
  l_coset    :: "[('a,'b) monoid_scheme, 'a, 'a set] => 'a set"
paulson@13870
    17
   "l_coset G a H == (% x. (mult G) a x) ` H"
paulson@13870
    18
ballarin@13936
    19
  rcosets  :: "[('a,'b) monoid_scheme,'a set] => ('a set)set"
paulson@13870
    20
   "rcosets G H == r_coset G H ` (carrier G)"
paulson@13870
    21
ballarin@13936
    22
  set_mult  :: "[('a,'b) monoid_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
ballarin@13936
    25
  set_inv   :: "[('a,'b) monoid_scheme,'a set] => 'a set"
paulson@13870
    26
   "set_inv G H == (m_inv G) ` H"
paulson@13870
    27
ballarin@13936
    28
  normal     :: "['a set, ('a,'b) monoid_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)
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@13870
   208
lemma (in coset) l_repr_independence:
paulson@13870
   209
     "[| y \<in> x <# H;  x \<in> carrier G;  subgroup H G |] ==> x <# H = y <# H"
paulson@13870
   210
apply (auto simp add: l_coset_eq m_assoc 
paulson@13870
   211
                      subgroup.subset [THEN subsetD] subgroup.m_closed)
paulson@13870
   212
apply (rule_tac x = "mult G (m_inv G h) ha" in bexI)
paulson@13870
   213
  --{*FIXME: locales don't currently work with @{text rule_tac},
paulson@13870
   214
      want @{term "(inv h) \<otimes> ha"}*}
paulson@13870
   215
apply (auto simp add: m_assoc [symmetric] subgroup.subset [THEN subsetD] 
paulson@13870
   216
                      subgroup.m_inv_closed subgroup.m_closed)
paulson@13870
   217
done
paulson@13870
   218
paulson@13870
   219
lemma (in coset) setmult_subset_G:
paulson@13870
   220
     "[| H <= carrier G; K <= carrier G |] ==> H <#> K <= carrier G"
paulson@13870
   221
by (auto simp add: set_mult_eq subsetD)
paulson@13870
   222
paulson@13870
   223
lemma (in coset) subgroup_mult_id: "subgroup H G ==> H <#> H = H"
paulson@13870
   224
apply (auto simp add: subgroup.m_closed set_mult_eq Sigma_def image_def)
paulson@13870
   225
apply (rule_tac x = x in bexI)
paulson@13870
   226
apply (rule bexI [of _ "\<one>"])
paulson@13870
   227
apply (auto simp add: subgroup.m_closed subgroup.one_closed 
paulson@13870
   228
                      r_one subgroup.subset [THEN subsetD])
paulson@13870
   229
done
paulson@13870
   230
paulson@13870
   231
paulson@13870
   232
(* set of inverses of an r_coset *)
paulson@13870
   233
lemma (in coset) rcos_inv:
paulson@13870
   234
  assumes normalHG: "H <| G"
paulson@13870
   235
      and xinG:     "x \<in> carrier G"
paulson@13870
   236
  shows "set_inv G (H #> x) = H #> (inv x)"
paulson@13870
   237
proof -
paulson@13870
   238
  have H_subset: "H <= carrier G" 
paulson@13870
   239
    by (rule subgroup.subset [OF normal_imp_subgroup, OF normalHG])
paulson@13870
   240
  show ?thesis
paulson@13870
   241
  proof (auto simp add: r_coset_eq image_def set_inv_def)
paulson@13870
   242
    fix h
paulson@13870
   243
    assume "h \<in> H"
paulson@13870
   244
      hence "((inv x) \<otimes> (inv h) \<otimes> x) \<otimes> inv x = inv (h \<otimes> x)"
paulson@13870
   245
	by (simp add: xinG m_assoc inv_mult_group H_subset [THEN subsetD])
paulson@13870
   246
      thus "\<exists>j\<in>H. j \<otimes> inv x = inv (h \<otimes> x)" 
paulson@13870
   247
       using prems
paulson@13870
   248
	by (blast intro: normal_inv_op_closed1 normal_imp_subgroup 
paulson@13870
   249
			 subgroup.m_inv_closed)
paulson@13870
   250
  next
paulson@13870
   251
    fix h
paulson@13870
   252
    assume "h \<in> H"
paulson@13870
   253
      hence eq: "(x \<otimes> (inv h) \<otimes> (inv x)) \<otimes> x = x \<otimes> inv h"
paulson@13870
   254
        by (simp add: xinG m_assoc H_subset [THEN subsetD])
paulson@13870
   255
      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
   256
       using prems
paulson@13870
   257
	by (simp add: m_assoc inv_mult_group H_subset [THEN subsetD],
paulson@13870
   258
            blast intro: eq normal_inv_op_closed2 normal_imp_subgroup 
paulson@13870
   259
			 subgroup.m_inv_closed)
paulson@13870
   260
      thus "\<exists>y. (\<exists>h\<in>H. h \<otimes> x = y) \<and> h \<otimes> inv x = inv y" ..
paulson@13870
   261
  qed
paulson@13870
   262
qed
paulson@13870
   263
paulson@13870
   264
(*The old proof is something like this, but the rule_tac calls make
paulson@13870
   265
illegal references to implicit structures.
paulson@13870
   266
lemma (in coset) rcos_inv:
paulson@13870
   267
     "[| H <| G; x \<in> carrier G |] ==> set_inv G (H #> x) = H #> (inv x)"
paulson@13870
   268
apply (frule normal_imp_subgroup)
paulson@13870
   269
apply (auto simp add: r_coset_eq image_def set_inv_def)
paulson@13870
   270
apply (rule_tac x = "(inv x) \<otimes> (inv h) \<otimes> x" in bexI)
paulson@13870
   271
apply (simp add: m_assoc inv_mult_group subgroup.subset [THEN subsetD])
paulson@13870
   272
apply (simp add: subgroup.m_inv_closed, assumption+)
paulson@13870
   273
apply (rule_tac x = "inv  (h \<otimes> (inv x)) " in exI)
paulson@13870
   274
apply (simp add: inv_mult_group subgroup.subset [THEN subsetD])
paulson@13870
   275
apply (rule_tac x = "x \<otimes> (inv h) \<otimes> (inv x)" in bexI)
paulson@13870
   276
apply (simp add: m_assoc subgroup.subset [THEN subsetD])
paulson@13870
   277
apply (simp add: normal_inv_op_closed2 subgroup.m_inv_closed)
paulson@13870
   278
done
paulson@13870
   279
*)
paulson@13870
   280
paulson@13870
   281
lemma (in coset) rcos_inv2:
paulson@13870
   282
     "[| H <| G; K \<in> rcosets G H; x \<in> K |] ==> set_inv G K = H #> (inv x)"
paulson@13870
   283
apply (simp add: setrcos_eq, clarify)
paulson@13870
   284
apply (subgoal_tac "x : carrier G")
paulson@13870
   285
 prefer 2
paulson@13870
   286
 apply (blast dest: r_coset_subset_G subgroup.subset normal_imp_subgroup) 
paulson@13870
   287
apply (drule repr_independence)
paulson@13870
   288
  apply assumption
paulson@13870
   289
 apply (erule normal_imp_subgroup)
paulson@13870
   290
apply (simp add: rcos_inv)
paulson@13870
   291
done
paulson@13870
   292
paulson@13870
   293
paulson@13870
   294
(* some rules for <#> with #> or <# *)
paulson@13870
   295
lemma (in coset) setmult_rcos_assoc:
paulson@13870
   296
     "[| H <= carrier G; K <= carrier G; x \<in> carrier G |] 
paulson@13870
   297
      ==> H <#> (K #> x) = (H <#> K) #> x"
paulson@13870
   298
apply (auto simp add: rcos_def r_coset_def setmult_def set_mult_def)
paulson@13870
   299
apply (force simp add: m_assoc)+
paulson@13870
   300
done
paulson@13870
   301
paulson@13870
   302
lemma (in coset) rcos_assoc_lcos:
paulson@13870
   303
     "[| H <= carrier G; K <= carrier G; x \<in> carrier G |] 
paulson@13870
   304
      ==> (H #> x) <#> K = H <#> (x <# K)"
paulson@13870
   305
apply (auto simp add: rcos_def r_coset_def lcos_def l_coset_def 
paulson@13870
   306
                      setmult_def set_mult_def Sigma_def image_def)
paulson@13870
   307
apply (force intro!: exI bexI simp add: m_assoc)+
paulson@13870
   308
done
paulson@13870
   309
paulson@13870
   310
lemma (in coset) rcos_mult_step1:
paulson@13870
   311
     "[| H <| G; x \<in> carrier G; y \<in> carrier G |] 
paulson@13870
   312
      ==> (H #> x) <#> (H #> y) = (H <#> (x <# H)) #> y"
paulson@13870
   313
by (simp add: setmult_rcos_assoc normal_imp_subgroup [THEN subgroup.subset]
paulson@13870
   314
              r_coset_subset_G l_coset_subset_G rcos_assoc_lcos)
paulson@13870
   315
paulson@13870
   316
lemma (in coset) rcos_mult_step2:
paulson@13870
   317
     "[| H <| G; x \<in> carrier G; y \<in> carrier G |] 
paulson@13870
   318
      ==> (H <#> (x <# H)) #> y = (H <#> (H #> x)) #> y"
paulson@13870
   319
by (simp add: normal_imp_rcos_eq_lcos)
paulson@13870
   320
paulson@13870
   321
lemma (in coset) rcos_mult_step3:
paulson@13870
   322
     "[| H <| G; x \<in> carrier G; y \<in> carrier G |] 
paulson@13870
   323
      ==> (H <#> (H #> x)) #> y = H #> (x \<otimes> y)"
paulson@13870
   324
by (simp add: setmult_rcos_assoc r_coset_subset_G coset_mult_assoc
paulson@13870
   325
              setmult_subset_G  subgroup_mult_id
paulson@13870
   326
              subgroup.subset normal_imp_subgroup)
paulson@13870
   327
paulson@13870
   328
lemma (in coset) rcos_sum:
paulson@13870
   329
     "[| H <| G; x \<in> carrier G; y \<in> carrier G |] 
paulson@13870
   330
      ==> (H #> x) <#> (H #> y) = H #> (x \<otimes> y)"
paulson@13870
   331
by (simp add: rcos_mult_step1 rcos_mult_step2 rcos_mult_step3)
paulson@13870
   332
paulson@13870
   333
(*generalizes subgroup_mult_id*)
paulson@13870
   334
lemma (in coset) setrcos_mult_eq: "[|H <| G; M \<in> rcosets G H|] ==> H <#> M = M"
paulson@13870
   335
by (auto simp add: setrcos_eq normal_imp_subgroup subgroup.subset
paulson@13870
   336
                   setmult_rcos_assoc subgroup_mult_id)
paulson@13870
   337
paulson@13870
   338
paulson@13870
   339
subsection{*Lemmas Leading to Lagrange's Theorem*}
paulson@13870
   340
paulson@13870
   341
lemma (in coset) setrcos_part_G: "subgroup H G ==> \<Union> rcosets G H = carrier G"
paulson@13870
   342
apply (rule equalityI)
paulson@13870
   343
apply (force simp add: subgroup.subset [THEN subsetD] 
paulson@13870
   344
                       setrcos_eq r_coset_eq)
paulson@13870
   345
apply (auto simp add: setrcos_eq subgroup.subset rcos_self)
paulson@13870
   346
done
paulson@13870
   347
paulson@13870
   348
lemma (in coset) cosets_finite:
paulson@13870
   349
     "[| c \<in> rcosets G H;  H <= carrier G;  finite (carrier G) |] ==> finite c"
paulson@13870
   350
apply (auto simp add: setrcos_eq)
paulson@13870
   351
apply (simp (no_asm_simp) add: r_coset_subset_G [THEN finite_subset])
paulson@13870
   352
done
paulson@13870
   353
paulson@13870
   354
text{*The next two lemmas support the proof of @{text card_cosets_equal},
paulson@13870
   355
since we can't use @{text rule_tac} with explicit terms for @{term f} and
paulson@13870
   356
@{term g}.*}
paulson@13870
   357
lemma (in coset) inj_on_f:
paulson@13870
   358
    "[|H \<subseteq> carrier G;  a \<in> carrier G|] ==> inj_on (\<lambda>y. y \<otimes> inv a) (H #> a)"
paulson@13870
   359
apply (rule inj_onI)
paulson@13870
   360
apply (subgoal_tac "x \<in> carrier G & y \<in> carrier G")
paulson@13870
   361
 prefer 2 apply (blast intro: r_coset_subset_G [THEN subsetD])
paulson@13870
   362
apply (simp add: subsetD)
paulson@13870
   363
done
paulson@13870
   364
paulson@13870
   365
lemma (in coset) inj_on_g:
paulson@13870
   366
    "[|H \<subseteq> carrier G;  a \<in> carrier G|] ==> inj_on (\<lambda>y. y \<otimes> a) H"
paulson@13870
   367
by (force simp add: inj_on_def subsetD)
paulson@13870
   368
paulson@13870
   369
lemma (in coset) card_cosets_equal:
paulson@13870
   370
     "[| c \<in> rcosets G H;  H <= carrier G; finite(carrier G) |] 
paulson@13870
   371
      ==> card c = card H"
paulson@13870
   372
apply (auto simp add: setrcos_eq)
paulson@13870
   373
apply (rule card_bij_eq)
paulson@13870
   374
     apply (rule inj_on_f, assumption+) 
paulson@13870
   375
    apply (force simp add: m_assoc subsetD r_coset_eq)
paulson@13870
   376
   apply (rule inj_on_g, assumption+) 
paulson@13870
   377
  apply (force simp add: m_assoc subsetD r_coset_eq)
paulson@13870
   378
 txt{*The sets @{term "H #> a"} and @{term "H"} are finite.*}
paulson@13870
   379
 apply (simp add: r_coset_subset_G [THEN finite_subset])
paulson@13870
   380
apply (blast intro: finite_subset)
paulson@13870
   381
done
paulson@13870
   382
paulson@13870
   383
subsection{*Two distinct right cosets are disjoint*}
paulson@13870
   384
paulson@13870
   385
lemma (in coset) rcos_equation:
paulson@13870
   386
     "[|subgroup H G;  a \<in> carrier G;  b \<in> carrier G;  ha \<otimes> a = h \<otimes> b;   
paulson@13870
   387
        h \<in> H;  ha \<in> H;  hb \<in> H|]  
paulson@13870
   388
      ==> \<exists>h\<in>H. h \<otimes> b = hb \<otimes> a"
paulson@13870
   389
apply (rule bexI [of _"hb \<otimes> ((inv ha) \<otimes> h)"])
paulson@13870
   390
apply (simp  add: m_assoc transpose_inv subgroup.subset [THEN subsetD])
paulson@13870
   391
apply (simp add: subgroup.m_closed subgroup.m_inv_closed)
paulson@13870
   392
done
paulson@13870
   393
paulson@13870
   394
lemma (in coset) rcos_disjoint:
paulson@13870
   395
     "[|subgroup H G; a \<in> rcosets G H; b \<in> rcosets G H; a\<noteq>b|] ==> a \<inter> b = {}"
paulson@13870
   396
apply (simp add: setrcos_eq r_coset_eq)
paulson@13870
   397
apply (blast intro: rcos_equation sym)
paulson@13870
   398
done
paulson@13870
   399
paulson@13870
   400
lemma (in coset) setrcos_subset_PowG:
paulson@13870
   401
     "subgroup H G  ==> rcosets G H <= Pow(carrier G)"
paulson@13870
   402
apply (simp add: setrcos_eq)
paulson@13870
   403
apply (blast dest: r_coset_subset_G subgroup.subset)
paulson@13870
   404
done
paulson@13870
   405
paulson@13870
   406
subsection {*Factorization of a Group*}
paulson@13870
   407
paulson@13870
   408
constdefs
ballarin@13936
   409
  FactGroup :: "[('a,'b) monoid_scheme, 'a set] => ('a set) monoid"
paulson@13870
   410
     (infixl "Mod" 60)
paulson@13870
   411
   "FactGroup G H ==
paulson@13870
   412
      (| carrier = rcosets G H,
paulson@13870
   413
	 mult = (%X: rcosets G H. %Y: rcosets G H. set_mult G X Y),
ballarin@13936
   414
	 one = H (*,
ballarin@13936
   415
	 m_inv = (%X: rcosets G H. set_inv G X) *) |)"
paulson@13870
   416
paulson@13870
   417
lemma (in coset) setmult_closed:
paulson@13870
   418
     "[| H <| G; K1 \<in> rcosets G H; K2 \<in> rcosets G H |] 
paulson@13870
   419
      ==> K1 <#> K2 \<in> rcosets G H"
paulson@13870
   420
by (auto simp add: normal_imp_subgroup [THEN subgroup.subset] 
paulson@13870
   421
                   rcos_sum setrcos_eq)
paulson@13870
   422
ballarin@13889
   423
lemma (in group) setinv_closed:
ballarin@13889
   424
     "[| H <| G; K \<in> rcosets G H |] ==> set_inv G K \<in> rcosets G H"
ballarin@13889
   425
by (auto simp add:  normal_imp_subgroup
ballarin@13889
   426
                 subgroup.subset coset.rcos_inv [OF is_coset]
ballarin@13889
   427
                 coset.setrcos_eq [OF is_coset])
ballarin@13889
   428
paulson@13870
   429
(*
ballarin@13889
   430
The old version is no longer valid: "group G" has to be an explicit premise.
ballarin@13889
   431
paulson@13870
   432
lemma setinv_closed:
paulson@13870
   433
     "[| H <| G; K \<in> rcosets G H |] ==> set_inv G K \<in> rcosets G H"
paulson@13870
   434
by (auto simp add:  normal_imp_subgroup
paulson@13870
   435
                   subgroup.subset coset.rcos_inv coset.setrcos_eq)
paulson@13870
   436
*)
paulson@13870
   437
paulson@13870
   438
lemma (in coset) setrcos_assoc:
paulson@13870
   439
     "[|H <| G; M1 \<in> rcosets G H; M2 \<in> rcosets G H; M3 \<in> rcosets G H|]   
paulson@13870
   440
      ==> M1 <#> M2 <#> M3 = M1 <#> (M2 <#> M3)"
paulson@13870
   441
by (auto simp add: setrcos_eq rcos_sum normal_imp_subgroup 
paulson@13870
   442
                   subgroup.subset m_assoc)
paulson@13870
   443
ballarin@13889
   444
lemma (in group) subgroup_in_rcosets:
ballarin@13889
   445
  "subgroup H G ==> H \<in> rcosets G H"
ballarin@13889
   446
proof -
ballarin@13889
   447
  assume sub: "subgroup H G"
ballarin@13889
   448
  have "r_coset G H \<one> = H"
ballarin@13889
   449
    by (rule coset.coset_join2)
ballarin@13889
   450
      (auto intro: sub subgroup.one_closed is_coset)
ballarin@13889
   451
  then show ?thesis
ballarin@13889
   452
    by (auto simp add: coset.setrcos_eq [OF is_coset])
ballarin@13889
   453
qed
ballarin@13889
   454
ballarin@13889
   455
(*
ballarin@13889
   456
lemma subgroup_in_rcosets:
ballarin@13889
   457
  "subgroup H G ==> H \<in> rcosets G H"
paulson@13870
   458
apply (frule subgroup_imp_coset) 
paulson@13870
   459
apply (frule subgroup_imp_group) 
paulson@13870
   460
apply (simp add: coset.setrcos_eq)
paulson@13870
   461
apply (blast del: equalityI 
paulson@13870
   462
             intro!: group.subgroup.one_closed group.one_closed
paulson@13870
   463
                     coset.coset_join2 [symmetric])
paulson@13870
   464
done
paulson@13870
   465
*)
paulson@13870
   466
paulson@13870
   467
lemma (in coset) setrcos_inv_mult_group_eq:
paulson@13870
   468
     "[|H <| G; M \<in> rcosets G H|] ==> set_inv G M <#> M = H"
paulson@13870
   469
by (auto simp add: setrcos_eq rcos_inv rcos_sum normal_imp_subgroup 
paulson@13870
   470
                   subgroup.subset)
ballarin@13940
   471
(*
ballarin@13889
   472
lemma (in group) factorgroup_is_magma:
ballarin@13889
   473
  "H <| G ==> magma (G Mod H)"
ballarin@13889
   474
  by rule (simp add: FactGroup_def coset.setmult_closed [OF is_coset])
ballarin@13889
   475
ballarin@13889
   476
lemma (in group) factorgroup_semigroup_axioms:
ballarin@13889
   477
  "H <| G ==> semigroup_axioms (G Mod H)"
ballarin@13889
   478
  by rule (simp add: FactGroup_def coset.setrcos_assoc [OF is_coset]
ballarin@13889
   479
    coset.setmult_closed [OF is_coset])
ballarin@13940
   480
*)
ballarin@13889
   481
theorem (in group) factorgroup_is_group:
ballarin@13889
   482
  "H <| G ==> group (G Mod H)"
ballarin@13889
   483
apply (insert is_coset) 
ballarin@13889
   484
apply (simp add: FactGroup_def) 
ballarin@13936
   485
apply (rule groupI)
ballarin@13936
   486
    apply (simp add: coset.setmult_closed)
ballarin@13936
   487
   apply (simp add: normal_imp_subgroup subgroup_in_rcosets)
ballarin@13889
   488
  apply (simp add: restrictI coset.setmult_closed coset.setrcos_assoc)
ballarin@13889
   489
 apply (simp add: normal_imp_subgroup
ballarin@13889
   490
   subgroup_in_rcosets coset.setrcos_mult_eq)
ballarin@13936
   491
apply (auto dest: coset.setrcos_inv_mult_group_eq simp add: setinv_closed)
ballarin@13889
   492
done
ballarin@13889
   493
paulson@13870
   494
end