src/HOL/Algebra/Coset.thy
author paulson
Tue Jun 28 15:27:45 2005 +0200 (2005-06-28)
changeset 16587 b34c8aa657a5
parent 16417 9bc16273c2d4
child 19380 b808efaa5828
permissions -rw-r--r--
Constant "If" is now local
     1 (*  Title:      HOL/Algebra/Coset.thy
     2     ID:         $Id$
     3     Author:     Florian Kammueller, with new proofs by L C Paulson
     4 *)
     5 
     6 header{*Cosets and Quotient Groups*}
     7 
     8 theory Coset imports Group Exponent begin
     9 
    10 constdefs (structure G)
    11   r_coset    :: "[_, 'a set, 'a] \<Rightarrow> 'a set"    (infixl "#>\<index>" 60)
    12   "H #> a \<equiv> \<Union>h\<in>H. {h \<otimes> a}"
    13 
    14   l_coset    :: "[_, 'a, 'a set] \<Rightarrow> 'a set"    (infixl "<#\<index>" 60)
    15   "a <# H \<equiv> \<Union>h\<in>H. {a \<otimes> h}"
    16 
    17   RCOSETS  :: "[_, 'a set] \<Rightarrow> ('a set)set"   ("rcosets\<index> _" [81] 80)
    18   "rcosets H \<equiv> \<Union>a\<in>carrier G. {H #> a}"
    19 
    20   set_mult  :: "[_, 'a set ,'a set] \<Rightarrow> 'a set" (infixl "<#>\<index>" 60)
    21   "H <#> K \<equiv> \<Union>h\<in>H. \<Union>k\<in>K. {h \<otimes> k}"
    22 
    23   SET_INV :: "[_,'a set] \<Rightarrow> 'a set"  ("set'_inv\<index> _" [81] 80)
    24   "set_inv H \<equiv> \<Union>h\<in>H. {inv h}"
    25 
    26 
    27 locale normal = subgroup + group +
    28   assumes coset_eq: "(\<forall>x \<in> carrier G. H #> x = x <# H)"
    29 
    30 
    31 syntax
    32   "@normal" :: "['a set, ('a, 'b) monoid_scheme] \<Rightarrow> bool"  (infixl "\<lhd>" 60)
    33 
    34 translations
    35   "H \<lhd> G" == "normal H G"
    36 
    37 
    38 subsection {*Basic Properties of Cosets*}
    39 
    40 lemma (in group) coset_mult_assoc:
    41      "[| M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G |]
    42       ==> (M #> g) #> h = M #> (g \<otimes> h)"
    43 by (force simp add: r_coset_def m_assoc)
    44 
    45 lemma (in group) coset_mult_one [simp]: "M \<subseteq> carrier G ==> M #> \<one> = M"
    46 by (force simp add: r_coset_def)
    47 
    48 lemma (in group) coset_mult_inv1:
    49      "[| M #> (x \<otimes> (inv y)) = M;  x \<in> carrier G ; y \<in> carrier G;
    50          M \<subseteq> carrier G |] ==> M #> x = M #> y"
    51 apply (erule subst [of concl: "%z. M #> x = z #> y"])
    52 apply (simp add: coset_mult_assoc m_assoc)
    53 done
    54 
    55 lemma (in group) coset_mult_inv2:
    56      "[| M #> x = M #> y;  x \<in> carrier G;  y \<in> carrier G;  M \<subseteq> carrier G |]
    57       ==> M #> (x \<otimes> (inv y)) = M "
    58 apply (simp add: coset_mult_assoc [symmetric])
    59 apply (simp add: coset_mult_assoc)
    60 done
    61 
    62 lemma (in group) coset_join1:
    63      "[| H #> x = H;  x \<in> carrier G;  subgroup H G |] ==> x \<in> H"
    64 apply (erule subst)
    65 apply (simp add: r_coset_def)
    66 apply (blast intro: l_one subgroup.one_closed sym)
    67 done
    68 
    69 lemma (in group) solve_equation:
    70     "\<lbrakk>subgroup H G; x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> \<exists>h\<in>H. y = h \<otimes> x"
    71 apply (rule bexI [of _ "y \<otimes> (inv x)"])
    72 apply (auto simp add: subgroup.m_closed subgroup.m_inv_closed m_assoc
    73                       subgroup.subset [THEN subsetD])
    74 done
    75 
    76 lemma (in group) repr_independence:
    77      "\<lbrakk>y \<in> H #> x;  x \<in> carrier G; subgroup H G\<rbrakk> \<Longrightarrow> H #> x = H #> y"
    78 by (auto simp add: r_coset_def m_assoc [symmetric]
    79                    subgroup.subset [THEN subsetD]
    80                    subgroup.m_closed solve_equation)
    81 
    82 lemma (in group) coset_join2:
    83      "\<lbrakk>x \<in> carrier G;  subgroup H G;  x\<in>H\<rbrakk> \<Longrightarrow> H #> x = H"
    84   --{*Alternative proof is to put @{term "x=\<one>"} in @{text repr_independence}.*}
    85 by (force simp add: subgroup.m_closed r_coset_def solve_equation)
    86 
    87 lemma (in group) r_coset_subset_G:
    88      "[| H \<subseteq> carrier G; x \<in> carrier G |] ==> H #> x \<subseteq> carrier G"
    89 by (auto simp add: r_coset_def)
    90 
    91 lemma (in group) rcosI:
    92      "[| h \<in> H; H \<subseteq> carrier G; x \<in> carrier G|] ==> h \<otimes> x \<in> H #> x"
    93 by (auto simp add: r_coset_def)
    94 
    95 lemma (in group) rcosetsI:
    96      "\<lbrakk>H \<subseteq> carrier G; x \<in> carrier G\<rbrakk> \<Longrightarrow> H #> x \<in> rcosets H"
    97 by (auto simp add: RCOSETS_def)
    98 
    99 text{*Really needed?*}
   100 lemma (in group) transpose_inv:
   101      "[| x \<otimes> y = z;  x \<in> carrier G;  y \<in> carrier G;  z \<in> carrier G |]
   102       ==> (inv x) \<otimes> z = y"
   103 by (force simp add: m_assoc [symmetric])
   104 
   105 lemma (in group) rcos_self: "[| x \<in> carrier G; subgroup H G |] ==> x \<in> H #> x"
   106 apply (simp add: r_coset_def)
   107 apply (blast intro: sym l_one subgroup.subset [THEN subsetD]
   108                     subgroup.one_closed)
   109 done
   110 
   111 
   112 subsection {* Normal subgroups *}
   113 
   114 lemma normal_imp_subgroup: "H \<lhd> G \<Longrightarrow> subgroup H G"
   115   by (simp add: normal_def subgroup_def)
   116 
   117 lemma (in group) normalI: 
   118   "subgroup H G \<Longrightarrow> (\<forall>x \<in> carrier G. H #> x = x <# H) \<Longrightarrow> H \<lhd> G";
   119   by (simp add: normal_def normal_axioms_def prems) 
   120 
   121 lemma (in normal) inv_op_closed1:
   122      "\<lbrakk>x \<in> carrier G; h \<in> H\<rbrakk> \<Longrightarrow> (inv x) \<otimes> h \<otimes> x \<in> H"
   123 apply (insert coset_eq) 
   124 apply (auto simp add: l_coset_def r_coset_def)
   125 apply (drule bspec, assumption)
   126 apply (drule equalityD1 [THEN subsetD], blast, clarify)
   127 apply (simp add: m_assoc)
   128 apply (simp add: m_assoc [symmetric])
   129 done
   130 
   131 lemma (in normal) inv_op_closed2:
   132      "\<lbrakk>x \<in> carrier G; h \<in> H\<rbrakk> \<Longrightarrow> x \<otimes> h \<otimes> (inv x) \<in> H"
   133 apply (subgoal_tac "inv (inv x) \<otimes> h \<otimes> (inv x) \<in> H") 
   134 apply (simp add: ); 
   135 apply (blast intro: inv_op_closed1) 
   136 done
   137 
   138 text{*Alternative characterization of normal subgroups*}
   139 lemma (in group) normal_inv_iff:
   140      "(N \<lhd> G) = 
   141       (subgroup N G & (\<forall>x \<in> carrier G. \<forall>h \<in> N. x \<otimes> h \<otimes> (inv x) \<in> N))"
   142       (is "_ = ?rhs")
   143 proof
   144   assume N: "N \<lhd> G"
   145   show ?rhs
   146     by (blast intro: N normal.inv_op_closed2 normal_imp_subgroup) 
   147 next
   148   assume ?rhs
   149   hence sg: "subgroup N G" 
   150     and closed: "\<And>x. x\<in>carrier G \<Longrightarrow> \<forall>h\<in>N. x \<otimes> h \<otimes> inv x \<in> N" by auto
   151   hence sb: "N \<subseteq> carrier G" by (simp add: subgroup.subset) 
   152   show "N \<lhd> G"
   153   proof (intro normalI [OF sg], simp add: l_coset_def r_coset_def, clarify)
   154     fix x
   155     assume x: "x \<in> carrier G"
   156     show "(\<Union>h\<in>N. {h \<otimes> x}) = (\<Union>h\<in>N. {x \<otimes> h})"
   157     proof
   158       show "(\<Union>h\<in>N. {h \<otimes> x}) \<subseteq> (\<Union>h\<in>N. {x \<otimes> h})"
   159       proof clarify
   160         fix n
   161         assume n: "n \<in> N" 
   162         show "n \<otimes> x \<in> (\<Union>h\<in>N. {x \<otimes> h})"
   163         proof 
   164           from closed [of "inv x"]
   165           show "inv x \<otimes> n \<otimes> x \<in> N" by (simp add: x n)
   166           show "n \<otimes> x \<in> {x \<otimes> (inv x \<otimes> n \<otimes> x)}"
   167             by (simp add: x n m_assoc [symmetric] sb [THEN subsetD])
   168         qed
   169       qed
   170     next
   171       show "(\<Union>h\<in>N. {x \<otimes> h}) \<subseteq> (\<Union>h\<in>N. {h \<otimes> x})"
   172       proof clarify
   173         fix n
   174         assume n: "n \<in> N" 
   175         show "x \<otimes> n \<in> (\<Union>h\<in>N. {h \<otimes> x})"
   176         proof 
   177           show "x \<otimes> n \<otimes> inv x \<in> N" by (simp add: x n closed)
   178           show "x \<otimes> n \<in> {x \<otimes> n \<otimes> inv x \<otimes> x}"
   179             by (simp add: x n m_assoc sb [THEN subsetD])
   180         qed
   181       qed
   182     qed
   183   qed
   184 qed
   185 
   186 
   187 subsection{*More Properties of Cosets*}
   188 
   189 lemma (in group) lcos_m_assoc:
   190      "[| M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G |]
   191       ==> g <# (h <# M) = (g \<otimes> h) <# M"
   192 by (force simp add: l_coset_def m_assoc)
   193 
   194 lemma (in group) lcos_mult_one: "M \<subseteq> carrier G ==> \<one> <# M = M"
   195 by (force simp add: l_coset_def)
   196 
   197 lemma (in group) l_coset_subset_G:
   198      "[| H \<subseteq> carrier G; x \<in> carrier G |] ==> x <# H \<subseteq> carrier G"
   199 by (auto simp add: l_coset_def subsetD)
   200 
   201 lemma (in group) l_coset_swap:
   202      "\<lbrakk>y \<in> x <# H;  x \<in> carrier G;  subgroup H G\<rbrakk> \<Longrightarrow> x \<in> y <# H"
   203 proof (simp add: l_coset_def)
   204   assume "\<exists>h\<in>H. y = x \<otimes> h"
   205     and x: "x \<in> carrier G"
   206     and sb: "subgroup H G"
   207   then obtain h' where h': "h' \<in> H & x \<otimes> h' = y" by blast
   208   show "\<exists>h\<in>H. x = y \<otimes> h"
   209   proof
   210     show "x = y \<otimes> inv h'" using h' x sb
   211       by (auto simp add: m_assoc subgroup.subset [THEN subsetD])
   212     show "inv h' \<in> H" using h' sb
   213       by (auto simp add: subgroup.subset [THEN subsetD] subgroup.m_inv_closed)
   214   qed
   215 qed
   216 
   217 lemma (in group) l_coset_carrier:
   218      "[| y \<in> x <# H;  x \<in> carrier G;  subgroup H G |] ==> y \<in> carrier G"
   219 by (auto simp add: l_coset_def m_assoc
   220                    subgroup.subset [THEN subsetD] subgroup.m_closed)
   221 
   222 lemma (in group) l_repr_imp_subset:
   223   assumes y: "y \<in> x <# H" and x: "x \<in> carrier G" and sb: "subgroup H G"
   224   shows "y <# H \<subseteq> x <# H"
   225 proof -
   226   from y
   227   obtain h' where "h' \<in> H" "x \<otimes> h' = y" by (auto simp add: l_coset_def)
   228   thus ?thesis using x sb
   229     by (auto simp add: l_coset_def m_assoc
   230                        subgroup.subset [THEN subsetD] subgroup.m_closed)
   231 qed
   232 
   233 lemma (in group) l_repr_independence:
   234   assumes y: "y \<in> x <# H" and x: "x \<in> carrier G" and sb: "subgroup H G"
   235   shows "x <# H = y <# H"
   236 proof
   237   show "x <# H \<subseteq> y <# H"
   238     by (rule l_repr_imp_subset,
   239         (blast intro: l_coset_swap l_coset_carrier y x sb)+)
   240   show "y <# H \<subseteq> x <# H" by (rule l_repr_imp_subset [OF y x sb])
   241 qed
   242 
   243 lemma (in group) setmult_subset_G:
   244      "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G\<rbrakk> \<Longrightarrow> H <#> K \<subseteq> carrier G"
   245 by (auto simp add: set_mult_def subsetD)
   246 
   247 lemma (in group) subgroup_mult_id: "subgroup H G \<Longrightarrow> H <#> H = H"
   248 apply (auto simp add: subgroup.m_closed set_mult_def Sigma_def image_def)
   249 apply (rule_tac x = x in bexI)
   250 apply (rule bexI [of _ "\<one>"])
   251 apply (auto simp add: subgroup.m_closed subgroup.one_closed
   252                       r_one subgroup.subset [THEN subsetD])
   253 done
   254 
   255 
   256 subsubsection {* Set of inverses of an @{text r_coset}. *}
   257 
   258 lemma (in normal) rcos_inv:
   259   assumes x:     "x \<in> carrier G"
   260   shows "set_inv (H #> x) = H #> (inv x)" 
   261 proof (simp add: r_coset_def SET_INV_def x inv_mult_group, safe)
   262   fix h
   263   assume "h \<in> H"
   264   show "inv x \<otimes> inv h \<in> (\<Union>j\<in>H. {j \<otimes> inv x})"
   265   proof
   266     show "inv x \<otimes> inv h \<otimes> x \<in> H"
   267       by (simp add: inv_op_closed1 prems)
   268     show "inv x \<otimes> inv h \<in> {inv x \<otimes> inv h \<otimes> x \<otimes> inv x}"
   269       by (simp add: prems m_assoc)
   270   qed
   271 next
   272   fix h
   273   assume "h \<in> H"
   274   show "h \<otimes> inv x \<in> (\<Union>j\<in>H. {inv x \<otimes> inv j})"
   275   proof
   276     show "x \<otimes> inv h \<otimes> inv x \<in> H"
   277       by (simp add: inv_op_closed2 prems)
   278     show "h \<otimes> inv x \<in> {inv x \<otimes> inv (x \<otimes> inv h \<otimes> inv x)}"
   279       by (simp add: prems m_assoc [symmetric] inv_mult_group)
   280   qed
   281 qed
   282 
   283 
   284 subsubsection {*Theorems for @{text "<#>"} with @{text "#>"} or @{text "<#"}.*}
   285 
   286 lemma (in group) setmult_rcos_assoc:
   287      "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G\<rbrakk>
   288       \<Longrightarrow> H <#> (K #> x) = (H <#> K) #> x"
   289 by (force simp add: r_coset_def set_mult_def m_assoc)
   290 
   291 lemma (in group) rcos_assoc_lcos:
   292      "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G\<rbrakk>
   293       \<Longrightarrow> (H #> x) <#> K = H <#> (x <# K)"
   294 by (force simp add: r_coset_def l_coset_def set_mult_def m_assoc)
   295 
   296 lemma (in normal) rcos_mult_step1:
   297      "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
   298       \<Longrightarrow> (H #> x) <#> (H #> y) = (H <#> (x <# H)) #> y"
   299 by (simp add: setmult_rcos_assoc subset
   300               r_coset_subset_G l_coset_subset_G rcos_assoc_lcos)
   301 
   302 lemma (in normal) rcos_mult_step2:
   303      "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
   304       \<Longrightarrow> (H <#> (x <# H)) #> y = (H <#> (H #> x)) #> y"
   305 by (insert coset_eq, simp add: normal_def)
   306 
   307 lemma (in normal) rcos_mult_step3:
   308      "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
   309       \<Longrightarrow> (H <#> (H #> x)) #> y = H #> (x \<otimes> y)"
   310 by (simp add: setmult_rcos_assoc coset_mult_assoc
   311               subgroup_mult_id subset prems)
   312 
   313 lemma (in normal) rcos_sum:
   314      "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
   315       \<Longrightarrow> (H #> x) <#> (H #> y) = H #> (x \<otimes> y)"
   316 by (simp add: rcos_mult_step1 rcos_mult_step2 rcos_mult_step3)
   317 
   318 lemma (in normal) rcosets_mult_eq: "M \<in> rcosets H \<Longrightarrow> H <#> M = M"
   319   -- {* generalizes @{text subgroup_mult_id} *}
   320   by (auto simp add: RCOSETS_def subset
   321         setmult_rcos_assoc subgroup_mult_id prems)
   322 
   323 
   324 subsubsection{*An Equivalence Relation*}
   325 
   326 constdefs (structure G)
   327   r_congruent :: "[('a,'b)monoid_scheme, 'a set] \<Rightarrow> ('a*'a)set"
   328                   ("rcong\<index> _")
   329    "rcong H \<equiv> {(x,y). x \<in> carrier G & y \<in> carrier G & inv x \<otimes> y \<in> H}"
   330 
   331 
   332 lemma (in subgroup) equiv_rcong:
   333    includes group G
   334    shows "equiv (carrier G) (rcong H)"
   335 proof (intro equiv.intro)
   336   show "refl (carrier G) (rcong H)"
   337     by (auto simp add: r_congruent_def refl_def) 
   338 next
   339   show "sym (rcong H)"
   340   proof (simp add: r_congruent_def sym_def, clarify)
   341     fix x y
   342     assume [simp]: "x \<in> carrier G" "y \<in> carrier G" 
   343        and "inv x \<otimes> y \<in> H"
   344     hence "inv (inv x \<otimes> y) \<in> H" by (simp add: m_inv_closed) 
   345     thus "inv y \<otimes> x \<in> H" by (simp add: inv_mult_group)
   346   qed
   347 next
   348   show "trans (rcong H)"
   349   proof (simp add: r_congruent_def trans_def, clarify)
   350     fix x y z
   351     assume [simp]: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
   352        and "inv x \<otimes> y \<in> H" and "inv y \<otimes> z \<in> H"
   353     hence "(inv x \<otimes> y) \<otimes> (inv y \<otimes> z) \<in> H" by simp
   354     hence "inv x \<otimes> (y \<otimes> inv y) \<otimes> z \<in> H" by (simp add: m_assoc del: r_inv) 
   355     thus "inv x \<otimes> z \<in> H" by simp
   356   qed
   357 qed
   358 
   359 text{*Equivalence classes of @{text rcong} correspond to left cosets.
   360   Was there a mistake in the definitions? I'd have expected them to
   361   correspond to right cosets.*}
   362 
   363 (* CB: This is correct, but subtle.
   364    We call H #> a the right coset of a relative to H.  According to
   365    Jacobson, this is what the majority of group theory literature does.
   366    He then defines the notion of congruence relation ~ over monoids as
   367    equivalence relation with a ~ a' & b ~ b' \<Longrightarrow> a*b ~ a'*b'.
   368    Our notion of right congruence induced by K: rcong K appears only in
   369    the context where K is a normal subgroup.  Jacobson doesn't name it.
   370    But in this context left and right cosets are identical.
   371 *)
   372 
   373 lemma (in subgroup) l_coset_eq_rcong:
   374   includes group G
   375   assumes a: "a \<in> carrier G"
   376   shows "a <# H = rcong H `` {a}"
   377 by (force simp add: r_congruent_def l_coset_def m_assoc [symmetric] a ) 
   378 
   379 
   380 subsubsection{*Two distinct right cosets are disjoint*}
   381 
   382 lemma (in group) rcos_equation:
   383   includes subgroup H G
   384   shows
   385      "\<lbrakk>ha \<otimes> a = h \<otimes> b; a \<in> carrier G;  b \<in> carrier G;  
   386         h \<in> H;  ha \<in> H;  hb \<in> H\<rbrakk>
   387       \<Longrightarrow> hb \<otimes> a \<in> (\<Union>h\<in>H. {h \<otimes> b})"
   388 apply (rule UN_I [of "hb \<otimes> ((inv ha) \<otimes> h)"])
   389 apply (simp add: ); 
   390 apply (simp add: m_assoc transpose_inv)
   391 done
   392 
   393 lemma (in group) rcos_disjoint:
   394   includes subgroup H G
   395   shows "\<lbrakk>a \<in> rcosets H; b \<in> rcosets H; a\<noteq>b\<rbrakk> \<Longrightarrow> a \<inter> b = {}"
   396 apply (simp add: RCOSETS_def r_coset_def)
   397 apply (blast intro: rcos_equation prems sym)
   398 done
   399 
   400 
   401 subsection {*Order of a Group and Lagrange's Theorem*}
   402 
   403 constdefs
   404   order :: "('a, 'b) monoid_scheme \<Rightarrow> nat"
   405   "order S \<equiv> card (carrier S)"
   406 
   407 lemma (in group) rcos_self:
   408   includes subgroup
   409   shows "x \<in> carrier G \<Longrightarrow> x \<in> H #> x"
   410 apply (simp add: r_coset_def)
   411 apply (rule_tac x="\<one>" in bexI) 
   412 apply (auto simp add: ); 
   413 done
   414 
   415 lemma (in group) rcosets_part_G:
   416   includes subgroup
   417   shows "\<Union>(rcosets H) = carrier G"
   418 apply (rule equalityI)
   419  apply (force simp add: RCOSETS_def r_coset_def)
   420 apply (auto simp add: RCOSETS_def intro: rcos_self prems)
   421 done
   422 
   423 lemma (in group) cosets_finite:
   424      "\<lbrakk>c \<in> rcosets H;  H \<subseteq> carrier G;  finite (carrier G)\<rbrakk> \<Longrightarrow> finite c"
   425 apply (auto simp add: RCOSETS_def)
   426 apply (simp add: r_coset_subset_G [THEN finite_subset])
   427 done
   428 
   429 text{*The next two lemmas support the proof of @{text card_cosets_equal}.*}
   430 lemma (in group) inj_on_f:
   431     "\<lbrakk>H \<subseteq> carrier G;  a \<in> carrier G\<rbrakk> \<Longrightarrow> inj_on (\<lambda>y. y \<otimes> inv a) (H #> a)"
   432 apply (rule inj_onI)
   433 apply (subgoal_tac "x \<in> carrier G & y \<in> carrier G")
   434  prefer 2 apply (blast intro: r_coset_subset_G [THEN subsetD])
   435 apply (simp add: subsetD)
   436 done
   437 
   438 lemma (in group) inj_on_g:
   439     "\<lbrakk>H \<subseteq> carrier G;  a \<in> carrier G\<rbrakk> \<Longrightarrow> inj_on (\<lambda>y. y \<otimes> a) H"
   440 by (force simp add: inj_on_def subsetD)
   441 
   442 lemma (in group) card_cosets_equal:
   443      "\<lbrakk>c \<in> rcosets H;  H \<subseteq> carrier G; finite(carrier G)\<rbrakk>
   444       \<Longrightarrow> card c = card H"
   445 apply (auto simp add: RCOSETS_def)
   446 apply (rule card_bij_eq)
   447      apply (rule inj_on_f, assumption+)
   448     apply (force simp add: m_assoc subsetD r_coset_def)
   449    apply (rule inj_on_g, assumption+)
   450   apply (force simp add: m_assoc subsetD r_coset_def)
   451  txt{*The sets @{term "H #> a"} and @{term "H"} are finite.*}
   452  apply (simp add: r_coset_subset_G [THEN finite_subset])
   453 apply (blast intro: finite_subset)
   454 done
   455 
   456 lemma (in group) rcosets_subset_PowG:
   457      "subgroup H G  \<Longrightarrow> rcosets H \<subseteq> Pow(carrier G)"
   458 apply (simp add: RCOSETS_def)
   459 apply (blast dest: r_coset_subset_G subgroup.subset)
   460 done
   461 
   462 
   463 theorem (in group) lagrange:
   464      "\<lbrakk>finite(carrier G); subgroup H G\<rbrakk>
   465       \<Longrightarrow> card(rcosets H) * card(H) = order(G)"
   466 apply (simp (no_asm_simp) add: order_def rcosets_part_G [symmetric])
   467 apply (subst mult_commute)
   468 apply (rule card_partition)
   469    apply (simp add: rcosets_subset_PowG [THEN finite_subset])
   470   apply (simp add: rcosets_part_G)
   471  apply (simp add: card_cosets_equal subgroup.subset)
   472 apply (simp add: rcos_disjoint)
   473 done
   474 
   475 
   476 subsection {*Quotient Groups: Factorization of a Group*}
   477 
   478 constdefs
   479   FactGroup :: "[('a,'b) monoid_scheme, 'a set] \<Rightarrow> ('a set) monoid"
   480      (infixl "Mod" 65)
   481     --{*Actually defined for groups rather than monoids*}
   482   "FactGroup G H \<equiv>
   483     \<lparr>carrier = rcosets\<^bsub>G\<^esub> H, mult = set_mult G, one = H\<rparr>"
   484 
   485 lemma (in normal) setmult_closed:
   486      "\<lbrakk>K1 \<in> rcosets H; K2 \<in> rcosets H\<rbrakk> \<Longrightarrow> K1 <#> K2 \<in> rcosets H"
   487 by (auto simp add: rcos_sum RCOSETS_def)
   488 
   489 lemma (in normal) setinv_closed:
   490      "K \<in> rcosets H \<Longrightarrow> set_inv K \<in> rcosets H"
   491 by (auto simp add: rcos_inv RCOSETS_def)
   492 
   493 lemma (in normal) rcosets_assoc:
   494      "\<lbrakk>M1 \<in> rcosets H; M2 \<in> rcosets H; M3 \<in> rcosets H\<rbrakk>
   495       \<Longrightarrow> M1 <#> M2 <#> M3 = M1 <#> (M2 <#> M3)"
   496 by (auto simp add: RCOSETS_def rcos_sum m_assoc)
   497 
   498 lemma (in subgroup) subgroup_in_rcosets:
   499   includes group G
   500   shows "H \<in> rcosets H"
   501 proof -
   502   have "H #> \<one> = H"
   503     by (rule coset_join2, auto)
   504   then show ?thesis
   505     by (auto simp add: RCOSETS_def)
   506 qed
   507 
   508 lemma (in normal) rcosets_inv_mult_group_eq:
   509      "M \<in> rcosets H \<Longrightarrow> set_inv M <#> M = H"
   510 by (auto simp add: RCOSETS_def rcos_inv rcos_sum subgroup.subset prems)
   511 
   512 theorem (in normal) factorgroup_is_group:
   513   "group (G Mod H)"
   514 apply (simp add: FactGroup_def)
   515 apply (rule groupI)
   516     apply (simp add: setmult_closed)
   517    apply (simp add: normal_imp_subgroup subgroup_in_rcosets [OF is_group])
   518   apply (simp add: restrictI setmult_closed rcosets_assoc)
   519  apply (simp add: normal_imp_subgroup
   520                   subgroup_in_rcosets rcosets_mult_eq)
   521 apply (auto dest: rcosets_inv_mult_group_eq simp add: setinv_closed)
   522 done
   523 
   524 lemma mult_FactGroup [simp]: "X \<otimes>\<^bsub>(G Mod H)\<^esub> X' = X <#>\<^bsub>G\<^esub> X'"
   525   by (simp add: FactGroup_def) 
   526 
   527 lemma (in normal) inv_FactGroup:
   528      "X \<in> carrier (G Mod H) \<Longrightarrow> inv\<^bsub>G Mod H\<^esub> X = set_inv X"
   529 apply (rule group.inv_equality [OF factorgroup_is_group]) 
   530 apply (simp_all add: FactGroup_def setinv_closed rcosets_inv_mult_group_eq)
   531 done
   532 
   533 text{*The coset map is a homomorphism from @{term G} to the quotient group
   534   @{term "G Mod H"}*}
   535 lemma (in normal) r_coset_hom_Mod:
   536   "(\<lambda>a. H #> a) \<in> hom G (G Mod H)"
   537   by (auto simp add: FactGroup_def RCOSETS_def Pi_def hom_def rcos_sum)
   538 
   539  
   540 subsection{*The First Isomorphism Theorem*}
   541 
   542 text{*The quotient by the kernel of a homomorphism is isomorphic to the 
   543   range of that homomorphism.*}
   544 
   545 constdefs
   546   kernel :: "('a, 'm) monoid_scheme \<Rightarrow> ('b, 'n) monoid_scheme \<Rightarrow> 
   547              ('a \<Rightarrow> 'b) \<Rightarrow> 'a set" 
   548     --{*the kernel of a homomorphism*}
   549   "kernel G H h \<equiv> {x. x \<in> carrier G & h x = \<one>\<^bsub>H\<^esub>}";
   550 
   551 lemma (in group_hom) subgroup_kernel: "subgroup (kernel G H h) G"
   552 apply (rule subgroup.intro) 
   553 apply (auto simp add: kernel_def group.intro prems) 
   554 done
   555 
   556 text{*The kernel of a homomorphism is a normal subgroup*}
   557 lemma (in group_hom) normal_kernel: "(kernel G H h) \<lhd> G"
   558 apply (simp add: group.normal_inv_iff subgroup_kernel group.intro prems)
   559 apply (simp add: kernel_def)  
   560 done
   561 
   562 lemma (in group_hom) FactGroup_nonempty:
   563   assumes X: "X \<in> carrier (G Mod kernel G H h)"
   564   shows "X \<noteq> {}"
   565 proof -
   566   from X
   567   obtain g where "g \<in> carrier G" 
   568              and "X = kernel G H h #> g"
   569     by (auto simp add: FactGroup_def RCOSETS_def)
   570   thus ?thesis 
   571    by (auto simp add: kernel_def r_coset_def image_def intro: hom_one)
   572 qed
   573 
   574 
   575 lemma (in group_hom) FactGroup_contents_mem:
   576   assumes X: "X \<in> carrier (G Mod (kernel G H h))"
   577   shows "contents (h`X) \<in> carrier H"
   578 proof -
   579   from X
   580   obtain g where g: "g \<in> carrier G" 
   581              and "X = kernel G H h #> g"
   582     by (auto simp add: FactGroup_def RCOSETS_def)
   583   hence "h ` X = {h g}" by (auto simp add: kernel_def r_coset_def image_def g)
   584   thus ?thesis by (auto simp add: g)
   585 qed
   586 
   587 lemma (in group_hom) FactGroup_hom:
   588      "(\<lambda>X. contents (h`X)) \<in> hom (G Mod (kernel G H h)) H"
   589 apply (simp add: hom_def FactGroup_contents_mem  normal.factorgroup_is_group [OF normal_kernel] group.axioms monoid.m_closed)  
   590 proof (simp add: hom_def funcsetI FactGroup_contents_mem, intro ballI) 
   591   fix X and X'
   592   assume X:  "X  \<in> carrier (G Mod kernel G H h)"
   593      and X': "X' \<in> carrier (G Mod kernel G H h)"
   594   then
   595   obtain g and g'
   596            where "g \<in> carrier G" and "g' \<in> carrier G" 
   597              and "X = kernel G H h #> g" and "X' = kernel G H h #> g'"
   598     by (auto simp add: FactGroup_def RCOSETS_def)
   599   hence all: "\<forall>x\<in>X. h x = h g" "\<forall>x\<in>X'. h x = h g'" 
   600     and Xsub: "X \<subseteq> carrier G" and X'sub: "X' \<subseteq> carrier G"
   601     by (force simp add: kernel_def r_coset_def image_def)+
   602   hence "h ` (X <#> X') = {h g \<otimes>\<^bsub>H\<^esub> h g'}" using X X'
   603     by (auto dest!: FactGroup_nonempty
   604              simp add: set_mult_def image_eq_UN 
   605                        subsetD [OF Xsub] subsetD [OF X'sub]) 
   606   thus "contents (h ` (X <#> X')) = contents (h ` X) \<otimes>\<^bsub>H\<^esub> contents (h ` X')"
   607     by (simp add: all image_eq_UN FactGroup_nonempty X X')  
   608 qed
   609 
   610 
   611 text{*Lemma for the following injectivity result*}
   612 lemma (in group_hom) FactGroup_subset:
   613      "\<lbrakk>g \<in> carrier G; g' \<in> carrier G; h g = h g'\<rbrakk>
   614       \<Longrightarrow>  kernel G H h #> g \<subseteq> kernel G H h #> g'"
   615 apply (clarsimp simp add: kernel_def r_coset_def image_def);
   616 apply (rename_tac y)  
   617 apply (rule_tac x="y \<otimes> g \<otimes> inv g'" in exI) 
   618 apply (simp add: G.m_assoc); 
   619 done
   620 
   621 lemma (in group_hom) FactGroup_inj_on:
   622      "inj_on (\<lambda>X. contents (h ` X)) (carrier (G Mod kernel G H h))"
   623 proof (simp add: inj_on_def, clarify) 
   624   fix X and X'
   625   assume X:  "X  \<in> carrier (G Mod kernel G H h)"
   626      and X': "X' \<in> carrier (G Mod kernel G H h)"
   627   then
   628   obtain g and g'
   629            where gX: "g \<in> carrier G"  "g' \<in> carrier G" 
   630               "X = kernel G H h #> g" "X' = kernel G H h #> g'"
   631     by (auto simp add: FactGroup_def RCOSETS_def)
   632   hence all: "\<forall>x\<in>X. h x = h g" "\<forall>x\<in>X'. h x = h g'" 
   633     by (force simp add: kernel_def r_coset_def image_def)+
   634   assume "contents (h ` X) = contents (h ` X')"
   635   hence h: "h g = h g'"
   636     by (simp add: image_eq_UN all FactGroup_nonempty X X') 
   637   show "X=X'" by (rule equalityI) (simp_all add: FactGroup_subset h gX) 
   638 qed
   639 
   640 text{*If the homomorphism @{term h} is onto @{term H}, then so is the
   641 homomorphism from the quotient group*}
   642 lemma (in group_hom) FactGroup_onto:
   643   assumes h: "h ` carrier G = carrier H"
   644   shows "(\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h) = carrier H"
   645 proof
   646   show "(\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h) \<subseteq> carrier H"
   647     by (auto simp add: FactGroup_contents_mem)
   648   show "carrier H \<subseteq> (\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h)"
   649   proof
   650     fix y
   651     assume y: "y \<in> carrier H"
   652     with h obtain g where g: "g \<in> carrier G" "h g = y"
   653       by (blast elim: equalityE); 
   654     hence "(\<Union>x\<in>kernel G H h #> g. {h x}) = {y}" 
   655       by (auto simp add: y kernel_def r_coset_def) 
   656     with g show "y \<in> (\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h)" 
   657       by (auto intro!: bexI simp add: FactGroup_def RCOSETS_def image_eq_UN)
   658   qed
   659 qed
   660 
   661 
   662 text{*If @{term h} is a homomorphism from @{term G} onto @{term H}, then the
   663  quotient group @{term "G Mod (kernel G H h)"} is isomorphic to @{term H}.*}
   664 theorem (in group_hom) FactGroup_iso:
   665   "h ` carrier G = carrier H
   666    \<Longrightarrow> (\<lambda>X. contents (h`X)) \<in> (G Mod (kernel G H h)) \<cong> H"
   667 by (simp add: iso_def FactGroup_hom FactGroup_inj_on bij_betw_def 
   668               FactGroup_onto) 
   669 
   670 
   671 end