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