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