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