src/HOL/Algebra/Coset.thy
author haftmann
Fri Apr 20 11:21:42 2007 +0200 (2007-04-20)
changeset 22744 5cbe966d67a2
parent 21404 eb85850d3eb7
child 23350 50c5b0912a0c
permissions -rw-r--r--
Isar definitions are now added explicitly to code theorem table
     1 (*  Title:      HOL/Algebra/Coset.thy
     2     ID:         $Id$
     3     Author:     Florian Kammueller, with new proofs by L C Paulson, and
     4                 Stephan Hohe
     5 *)
     6 
     7 theory Coset imports Group Exponent begin
     8 
     9 
    10 section {*Cosets and Quotient Groups*}
    11 
    12 constdefs (structure G)
    13   r_coset    :: "[_, 'a set, 'a] \<Rightarrow> 'a set"    (infixl "#>\<index>" 60)
    14   "H #> a \<equiv> \<Union>h\<in>H. {h \<otimes> a}"
    15 
    16   l_coset    :: "[_, 'a, 'a set] \<Rightarrow> 'a set"    (infixl "<#\<index>" 60)
    17   "a <# H \<equiv> \<Union>h\<in>H. {a \<otimes> h}"
    18 
    19   RCOSETS  :: "[_, 'a set] \<Rightarrow> ('a set)set"   ("rcosets\<index> _" [81] 80)
    20   "rcosets H \<equiv> \<Union>a\<in>carrier G. {H #> a}"
    21 
    22   set_mult  :: "[_, 'a set ,'a set] \<Rightarrow> 'a set" (infixl "<#>\<index>" 60)
    23   "H <#> K \<equiv> \<Union>h\<in>H. \<Union>k\<in>K. {h \<otimes> k}"
    24 
    25   SET_INV :: "[_,'a set] \<Rightarrow> 'a set"  ("set'_inv\<index> _" [81] 80)
    26   "set_inv H \<equiv> \<Union>h\<in>H. {inv h}"
    27 
    28 
    29 locale normal = subgroup + group +
    30   assumes coset_eq: "(\<forall>x \<in> carrier G. H #> x = x <# H)"
    31 
    32 abbreviation
    33   normal_rel :: "['a set, ('a, 'b) monoid_scheme] \<Rightarrow> bool"  (infixl "\<lhd>" 60) where
    34   "H \<lhd> G \<equiv> normal H G"
    35 
    36 
    37 subsection {*Basic Properties of Cosets*}
    38 
    39 lemma (in group) coset_mult_assoc:
    40      "[| M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G |]
    41       ==> (M #> g) #> h = M #> (g \<otimes> h)"
    42 by (force simp add: r_coset_def m_assoc)
    43 
    44 lemma (in group) coset_mult_one [simp]: "M \<subseteq> carrier G ==> M #> \<one> = M"
    45 by (force simp add: r_coset_def)
    46 
    47 lemma (in group) coset_mult_inv1:
    48      "[| M #> (x \<otimes> (inv y)) = M;  x \<in> carrier G ; y \<in> carrier G;
    49          M \<subseteq> carrier G |] ==> M #> x = M #> y"
    50 apply (erule subst [of concl: "%z. M #> x = z #> y"])
    51 apply (simp add: coset_mult_assoc m_assoc)
    52 done
    53 
    54 lemma (in group) coset_mult_inv2:
    55      "[| M #> x = M #> y;  x \<in> carrier G;  y \<in> carrier G;  M \<subseteq> carrier G |]
    56       ==> M #> (x \<otimes> (inv y)) = M "
    57 apply (simp add: coset_mult_assoc [symmetric])
    58 apply (simp add: coset_mult_assoc)
    59 done
    60 
    61 lemma (in group) coset_join1:
    62      "[| H #> x = H;  x \<in> carrier G;  subgroup H G |] ==> x \<in> H"
    63 apply (erule subst)
    64 apply (simp add: r_coset_def)
    65 apply (blast intro: l_one subgroup.one_closed sym)
    66 done
    67 
    68 lemma (in group) solve_equation:
    69     "\<lbrakk>subgroup H G; x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> \<exists>h\<in>H. y = h \<otimes> x"
    70 apply (rule bexI [of _ "y \<otimes> (inv x)"])
    71 apply (auto simp add: subgroup.m_closed subgroup.m_inv_closed m_assoc
    72                       subgroup.subset [THEN subsetD])
    73 done
    74 
    75 lemma (in group) repr_independence:
    76      "\<lbrakk>y \<in> H #> x;  x \<in> carrier G; subgroup H G\<rbrakk> \<Longrightarrow> H #> x = H #> y"
    77 by (auto simp add: r_coset_def m_assoc [symmetric]
    78                    subgroup.subset [THEN subsetD]
    79                    subgroup.m_closed solve_equation)
    80 
    81 lemma (in group) coset_join2:
    82      "\<lbrakk>x \<in> carrier G;  subgroup H G;  x\<in>H\<rbrakk> \<Longrightarrow> H #> x = H"
    83   --{*Alternative proof is to put @{term "x=\<one>"} in @{text repr_independence}.*}
    84 by (force simp add: subgroup.m_closed r_coset_def solve_equation)
    85 
    86 lemma (in monoid) r_coset_subset_G:
    87      "[| H \<subseteq> carrier G; x \<in> carrier G |] ==> H #> x \<subseteq> carrier G"
    88 by (auto simp add: r_coset_def)
    89 
    90 lemma (in group) rcosI:
    91      "[| h \<in> H; H \<subseteq> carrier G; x \<in> carrier G|] ==> h \<otimes> x \<in> H #> x"
    92 by (auto simp add: r_coset_def)
    93 
    94 lemma (in group) rcosetsI:
    95      "\<lbrakk>H \<subseteq> carrier G; x \<in> carrier G\<rbrakk> \<Longrightarrow> H #> x \<in> rcosets H"
    96 by (auto simp add: RCOSETS_def)
    97 
    98 text{*Really needed?*}
    99 lemma (in group) transpose_inv:
   100      "[| x \<otimes> y = z;  x \<in> carrier G;  y \<in> carrier G;  z \<in> carrier G |]
   101       ==> (inv x) \<otimes> z = y"
   102 by (force simp add: m_assoc [symmetric])
   103 
   104 lemma (in group) rcos_self: "[| x \<in> carrier G; subgroup H G |] ==> x \<in> H #> x"
   105 apply (simp add: r_coset_def)
   106 apply (blast intro: sym l_one subgroup.subset [THEN subsetD]
   107                     subgroup.one_closed)
   108 done
   109 
   110 text {* Opposite of @{thm [locale=group,source] "repr_independence"} *}
   111 lemma (in group) repr_independenceD:
   112   includes subgroup H G
   113   assumes ycarr: "y \<in> carrier G"
   114       and repr:  "H #> x = H #> y"
   115   shows "y \<in> H #> x"
   116   by (subst repr, intro rcos_self)
   117 
   118 text {* Elements of a right coset are in the carrier *}
   119 lemma (in subgroup) elemrcos_carrier:
   120   includes group
   121   assumes acarr: "a \<in> carrier G"
   122     and a': "a' \<in> H #> a"
   123   shows "a' \<in> carrier G"
   124 proof -
   125   from subset and acarr
   126   have "H #> a \<subseteq> carrier G" by (rule r_coset_subset_G)
   127   from this and a'
   128   show "a' \<in> carrier G"
   129     by fast
   130 qed
   131 
   132 lemma (in subgroup) rcos_const:
   133   includes group
   134   assumes hH: "h \<in> H"
   135   shows "H #> h = H"
   136   apply (unfold r_coset_def)
   137   apply rule apply rule
   138   apply clarsimp
   139   apply (intro subgroup.m_closed)
   140   apply assumption+
   141   apply rule
   142   apply simp
   143 proof -
   144   fix h'
   145   assume h'H: "h' \<in> H"
   146   note carr = hH[THEN mem_carrier] h'H[THEN mem_carrier]
   147   from carr
   148   have a: "h' = (h' \<otimes> inv h) \<otimes> h" by (simp add: m_assoc)
   149   from h'H hH
   150   have "h' \<otimes> inv h \<in> H" by simp
   151   from this and a
   152   show "\<exists>x\<in>H. h' = x \<otimes> h" by fast
   153 qed
   154 
   155 text {* Step one for lemma @{text "rcos_module"} *}
   156 lemma (in subgroup) rcos_module_imp:
   157   includes group
   158   assumes xcarr: "x \<in> carrier G"
   159       and x'cos: "x' \<in> H #> x"
   160   shows "(x' \<otimes> inv x) \<in> H"
   161 proof -
   162   from xcarr x'cos
   163       have x'carr: "x' \<in> carrier G"
   164       by (rule elemrcos_carrier[OF is_group])
   165   from xcarr
   166       have ixcarr: "inv x \<in> carrier G"
   167       by simp
   168   from x'cos
   169       have "\<exists>h\<in>H. x' = h \<otimes> x"
   170       unfolding r_coset_def
   171       by fast
   172   from this
   173       obtain h
   174         where hH: "h \<in> H"
   175         and x': "x' = h \<otimes> x"
   176       by auto
   177   from hH and subset
   178       have hcarr: "h \<in> carrier G" by fast
   179   note carr = xcarr x'carr hcarr
   180   from x' and carr
   181       have "x' \<otimes> (inv x) = (h \<otimes> x) \<otimes> (inv x)" by fast
   182   also from carr
   183       have "\<dots> = h \<otimes> (x \<otimes> inv x)" by (simp add: m_assoc)
   184   also from carr
   185       have "\<dots> = h \<otimes> \<one>" by simp
   186   also from carr
   187       have "\<dots> = h" by simp
   188   finally
   189       have "x' \<otimes> (inv x) = h" by simp
   190   from hH this
   191       show "x' \<otimes> (inv x) \<in> H" by simp
   192 qed
   193 
   194 text {* Step two for lemma @{text "rcos_module"} *}
   195 lemma (in subgroup) rcos_module_rev:
   196   includes group
   197   assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
   198       and xixH: "(x' \<otimes> inv x) \<in> H"
   199   shows "x' \<in> H #> x"
   200 proof -
   201   from xixH
   202       have "\<exists>h\<in>H. x' \<otimes> (inv x) = h" by fast
   203   from this
   204       obtain h
   205         where hH: "h \<in> H"
   206         and hsym: "x' \<otimes> (inv x) = h"
   207       by fast
   208   from hH subset have hcarr: "h \<in> carrier G" by simp
   209   note carr = carr hcarr
   210   from hsym[symmetric] have "h \<otimes> x = x' \<otimes> (inv x) \<otimes> x" by fast
   211   also from carr
   212       have "\<dots> = x' \<otimes> ((inv x) \<otimes> x)" by (simp add: m_assoc)
   213   also from carr
   214       have "\<dots> = x' \<otimes> \<one>" by (simp add: l_inv)
   215   also from carr
   216       have "\<dots> = x'" by simp
   217   finally
   218       have "h \<otimes> x = x'" by simp
   219   from this[symmetric] and hH
   220       show "x' \<in> H #> x"
   221       unfolding r_coset_def
   222       by fast
   223 qed
   224 
   225 text {* Module property of right cosets *}
   226 lemma (in subgroup) rcos_module:
   227   includes group
   228   assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
   229   shows "(x' \<in> H #> x) = (x' \<otimes> inv x \<in> H)"
   230 proof
   231   assume "x' \<in> H #> x"
   232   from this and carr
   233       show "x' \<otimes> inv x \<in> H"
   234       by (intro rcos_module_imp[OF is_group])
   235 next
   236   assume "x' \<otimes> inv x \<in> H"
   237   from this and carr
   238       show "x' \<in> H #> x"
   239       by (intro rcos_module_rev[OF is_group])
   240 qed
   241 
   242 text {* Right cosets are subsets of the carrier. *} 
   243 lemma (in subgroup) rcosets_carrier:
   244   includes group
   245   assumes XH: "X \<in> rcosets H"
   246   shows "X \<subseteq> carrier G"
   247 proof -
   248   from XH have "\<exists>x\<in> carrier G. X = H #> x"
   249       unfolding RCOSETS_def
   250       by fast
   251   from this
   252       obtain x
   253         where xcarr: "x\<in> carrier G"
   254         and X: "X = H #> x"
   255       by fast
   256   from subset and xcarr
   257       show "X \<subseteq> carrier G"
   258       unfolding X
   259       by (rule r_coset_subset_G)
   260 qed
   261 
   262 text {* Multiplication of general subsets *}
   263 lemma (in monoid) set_mult_closed:
   264   assumes Acarr: "A \<subseteq> carrier G"
   265       and Bcarr: "B \<subseteq> carrier G"
   266   shows "A <#> B \<subseteq> carrier G"
   267 apply rule apply (simp add: set_mult_def, clarsimp)
   268 proof -
   269   fix a b
   270   assume "a \<in> A"
   271   from this and Acarr
   272       have acarr: "a \<in> carrier G" by fast
   273 
   274   assume "b \<in> B"
   275   from this and Bcarr
   276       have bcarr: "b \<in> carrier G" by fast
   277 
   278   from acarr bcarr
   279       show "a \<otimes> b \<in> carrier G" by (rule m_closed)
   280 qed
   281 
   282 lemma (in comm_group) mult_subgroups:
   283   assumes subH: "subgroup H G"
   284       and subK: "subgroup K G"
   285   shows "subgroup (H <#> K) G"
   286 apply (rule subgroup.intro)
   287    apply (intro set_mult_closed subgroup.subset[OF subH] subgroup.subset[OF subK])
   288   apply (simp add: set_mult_def) apply clarsimp defer 1
   289   apply (simp add: set_mult_def) defer 1
   290   apply (simp add: set_mult_def, clarsimp) defer 1
   291 proof -
   292   fix ha hb ka kb
   293   assume haH: "ha \<in> H" and hbH: "hb \<in> H" and kaK: "ka \<in> K" and kbK: "kb \<in> K"
   294   note carr = haH[THEN subgroup.mem_carrier[OF subH]] hbH[THEN subgroup.mem_carrier[OF subH]]
   295               kaK[THEN subgroup.mem_carrier[OF subK]] kbK[THEN subgroup.mem_carrier[OF subK]]
   296   from carr
   297       have "(ha \<otimes> ka) \<otimes> (hb \<otimes> kb) = ha \<otimes> (ka \<otimes> hb) \<otimes> kb" by (simp add: m_assoc)
   298   also from carr
   299       have "\<dots> = ha \<otimes> (hb \<otimes> ka) \<otimes> kb" by (simp add: m_comm)
   300   also from carr
   301       have "\<dots> = (ha \<otimes> hb) \<otimes> (ka \<otimes> kb)" by (simp add: m_assoc)
   302   finally
   303       have eq: "(ha \<otimes> ka) \<otimes> (hb \<otimes> kb) = (ha \<otimes> hb) \<otimes> (ka \<otimes> kb)" .
   304 
   305   from haH hbH have hH: "ha \<otimes> hb \<in> H" by (simp add: subgroup.m_closed[OF subH])
   306   from kaK kbK have kK: "ka \<otimes> kb \<in> K" by (simp add: subgroup.m_closed[OF subK])
   307   
   308   from hH and kK and eq
   309       show "\<exists>h'\<in>H. \<exists>k'\<in>K. (ha \<otimes> ka) \<otimes> (hb \<otimes> kb) = h' \<otimes> k'" by fast
   310 next
   311   have "\<one> = \<one> \<otimes> \<one>" by simp
   312   from subgroup.one_closed[OF subH] subgroup.one_closed[OF subK] this
   313       show "\<exists>h\<in>H. \<exists>k\<in>K. \<one> = h \<otimes> k" by fast
   314 next
   315   fix h k
   316   assume hH: "h \<in> H"
   317      and kK: "k \<in> K"
   318 
   319   from hH[THEN subgroup.mem_carrier[OF subH]] kK[THEN subgroup.mem_carrier[OF subK]]
   320       have "inv (h \<otimes> k) = inv h \<otimes> inv k" by (simp add: inv_mult_group m_comm)
   321 
   322   from subgroup.m_inv_closed[OF subH hH] and subgroup.m_inv_closed[OF subK kK] and this
   323       show "\<exists>ha\<in>H. \<exists>ka\<in>K. inv (h \<otimes> k) = ha \<otimes> ka" by fast
   324 qed
   325 
   326 lemma (in subgroup) lcos_module_rev:
   327   includes group
   328   assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
   329       and xixH: "(inv x \<otimes> x') \<in> H"
   330   shows "x' \<in> x <# H"
   331 proof -
   332   from xixH
   333       have "\<exists>h\<in>H. (inv x) \<otimes> x' = h" by fast
   334   from this
   335       obtain h
   336         where hH: "h \<in> H"
   337         and hsym: "(inv x) \<otimes> x' = h"
   338       by fast
   339 
   340   from hH subset have hcarr: "h \<in> carrier G" by simp
   341   note carr = carr hcarr
   342   from hsym[symmetric] have "x \<otimes> h = x \<otimes> ((inv x) \<otimes> x')" by fast
   343   also from carr
   344       have "\<dots> = (x \<otimes> (inv x)) \<otimes> x'" by (simp add: m_assoc[symmetric])
   345   also from carr
   346       have "\<dots> = \<one> \<otimes> x'" by simp
   347   also from carr
   348       have "\<dots> = x'" by simp
   349   finally
   350       have "x \<otimes> h = x'" by simp
   351 
   352   from this[symmetric] and hH
   353       show "x' \<in> x <# H"
   354       unfolding l_coset_def
   355       by fast
   356 qed
   357 
   358 
   359 subsection {* Normal subgroups *}
   360 
   361 lemma normal_imp_subgroup: "H \<lhd> G \<Longrightarrow> subgroup H G"
   362   by (simp add: normal_def subgroup_def)
   363 
   364 lemma (in group) normalI: 
   365   "subgroup H G \<Longrightarrow> (\<forall>x \<in> carrier G. H #> x = x <# H) \<Longrightarrow> H \<lhd> G";
   366   by (simp add: normal_def normal_axioms_def prems) 
   367 
   368 lemma (in normal) inv_op_closed1:
   369      "\<lbrakk>x \<in> carrier G; h \<in> H\<rbrakk> \<Longrightarrow> (inv x) \<otimes> h \<otimes> x \<in> H"
   370 apply (insert coset_eq) 
   371 apply (auto simp add: l_coset_def r_coset_def)
   372 apply (drule bspec, assumption)
   373 apply (drule equalityD1 [THEN subsetD], blast, clarify)
   374 apply (simp add: m_assoc)
   375 apply (simp add: m_assoc [symmetric])
   376 done
   377 
   378 lemma (in normal) inv_op_closed2:
   379      "\<lbrakk>x \<in> carrier G; h \<in> H\<rbrakk> \<Longrightarrow> x \<otimes> h \<otimes> (inv x) \<in> H"
   380 apply (subgoal_tac "inv (inv x) \<otimes> h \<otimes> (inv x) \<in> H") 
   381 apply (simp add: ); 
   382 apply (blast intro: inv_op_closed1) 
   383 done
   384 
   385 text{*Alternative characterization of normal subgroups*}
   386 lemma (in group) normal_inv_iff:
   387      "(N \<lhd> G) = 
   388       (subgroup N G & (\<forall>x \<in> carrier G. \<forall>h \<in> N. x \<otimes> h \<otimes> (inv x) \<in> N))"
   389       (is "_ = ?rhs")
   390 proof
   391   assume N: "N \<lhd> G"
   392   show ?rhs
   393     by (blast intro: N normal.inv_op_closed2 normal_imp_subgroup) 
   394 next
   395   assume ?rhs
   396   hence sg: "subgroup N G" 
   397     and closed: "\<And>x. x\<in>carrier G \<Longrightarrow> \<forall>h\<in>N. x \<otimes> h \<otimes> inv x \<in> N" by auto
   398   hence sb: "N \<subseteq> carrier G" by (simp add: subgroup.subset) 
   399   show "N \<lhd> G"
   400   proof (intro normalI [OF sg], simp add: l_coset_def r_coset_def, clarify)
   401     fix x
   402     assume x: "x \<in> carrier G"
   403     show "(\<Union>h\<in>N. {h \<otimes> x}) = (\<Union>h\<in>N. {x \<otimes> h})"
   404     proof
   405       show "(\<Union>h\<in>N. {h \<otimes> x}) \<subseteq> (\<Union>h\<in>N. {x \<otimes> h})"
   406       proof clarify
   407         fix n
   408         assume n: "n \<in> N" 
   409         show "n \<otimes> x \<in> (\<Union>h\<in>N. {x \<otimes> h})"
   410         proof 
   411           from closed [of "inv x"]
   412           show "inv x \<otimes> n \<otimes> x \<in> N" by (simp add: x n)
   413           show "n \<otimes> x \<in> {x \<otimes> (inv x \<otimes> n \<otimes> x)}"
   414             by (simp add: x n m_assoc [symmetric] sb [THEN subsetD])
   415         qed
   416       qed
   417     next
   418       show "(\<Union>h\<in>N. {x \<otimes> h}) \<subseteq> (\<Union>h\<in>N. {h \<otimes> x})"
   419       proof clarify
   420         fix n
   421         assume n: "n \<in> N" 
   422         show "x \<otimes> n \<in> (\<Union>h\<in>N. {h \<otimes> x})"
   423         proof 
   424           show "x \<otimes> n \<otimes> inv x \<in> N" by (simp add: x n closed)
   425           show "x \<otimes> n \<in> {x \<otimes> n \<otimes> inv x \<otimes> x}"
   426             by (simp add: x n m_assoc sb [THEN subsetD])
   427         qed
   428       qed
   429     qed
   430   qed
   431 qed
   432 
   433 
   434 subsection{*More Properties of Cosets*}
   435 
   436 lemma (in group) lcos_m_assoc:
   437      "[| M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G |]
   438       ==> g <# (h <# M) = (g \<otimes> h) <# M"
   439 by (force simp add: l_coset_def m_assoc)
   440 
   441 lemma (in group) lcos_mult_one: "M \<subseteq> carrier G ==> \<one> <# M = M"
   442 by (force simp add: l_coset_def)
   443 
   444 lemma (in group) l_coset_subset_G:
   445      "[| H \<subseteq> carrier G; x \<in> carrier G |] ==> x <# H \<subseteq> carrier G"
   446 by (auto simp add: l_coset_def subsetD)
   447 
   448 lemma (in group) l_coset_swap:
   449      "\<lbrakk>y \<in> x <# H;  x \<in> carrier G;  subgroup H G\<rbrakk> \<Longrightarrow> x \<in> y <# H"
   450 proof (simp add: l_coset_def)
   451   assume "\<exists>h\<in>H. y = x \<otimes> h"
   452     and x: "x \<in> carrier G"
   453     and sb: "subgroup H G"
   454   then obtain h' where h': "h' \<in> H & x \<otimes> h' = y" by blast
   455   show "\<exists>h\<in>H. x = y \<otimes> h"
   456   proof
   457     show "x = y \<otimes> inv h'" using h' x sb
   458       by (auto simp add: m_assoc subgroup.subset [THEN subsetD])
   459     show "inv h' \<in> H" using h' sb
   460       by (auto simp add: subgroup.subset [THEN subsetD] subgroup.m_inv_closed)
   461   qed
   462 qed
   463 
   464 lemma (in group) l_coset_carrier:
   465      "[| y \<in> x <# H;  x \<in> carrier G;  subgroup H G |] ==> y \<in> carrier G"
   466 by (auto simp add: l_coset_def m_assoc
   467                    subgroup.subset [THEN subsetD] subgroup.m_closed)
   468 
   469 lemma (in group) l_repr_imp_subset:
   470   assumes y: "y \<in> x <# H" and x: "x \<in> carrier G" and sb: "subgroup H G"
   471   shows "y <# H \<subseteq> x <# H"
   472 proof -
   473   from y
   474   obtain h' where "h' \<in> H" "x \<otimes> h' = y" by (auto simp add: l_coset_def)
   475   thus ?thesis using x sb
   476     by (auto simp add: l_coset_def m_assoc
   477                        subgroup.subset [THEN subsetD] subgroup.m_closed)
   478 qed
   479 
   480 lemma (in group) l_repr_independence:
   481   assumes y: "y \<in> x <# H" and x: "x \<in> carrier G" and sb: "subgroup H G"
   482   shows "x <# H = y <# H"
   483 proof
   484   show "x <# H \<subseteq> y <# H"
   485     by (rule l_repr_imp_subset,
   486         (blast intro: l_coset_swap l_coset_carrier y x sb)+)
   487   show "y <# H \<subseteq> x <# H" by (rule l_repr_imp_subset [OF y x sb])
   488 qed
   489 
   490 lemma (in group) setmult_subset_G:
   491      "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G\<rbrakk> \<Longrightarrow> H <#> K \<subseteq> carrier G"
   492 by (auto simp add: set_mult_def subsetD)
   493 
   494 lemma (in group) subgroup_mult_id: "subgroup H G \<Longrightarrow> H <#> H = H"
   495 apply (auto simp add: subgroup.m_closed set_mult_def Sigma_def image_def)
   496 apply (rule_tac x = x in bexI)
   497 apply (rule bexI [of _ "\<one>"])
   498 apply (auto simp add: subgroup.m_closed subgroup.one_closed
   499                       r_one subgroup.subset [THEN subsetD])
   500 done
   501 
   502 
   503 subsubsection {* Set of Inverses of an @{text r_coset}. *}
   504 
   505 lemma (in normal) rcos_inv:
   506   assumes x:     "x \<in> carrier G"
   507   shows "set_inv (H #> x) = H #> (inv x)" 
   508 proof (simp add: r_coset_def SET_INV_def x inv_mult_group, safe)
   509   fix h
   510   assume "h \<in> H"
   511   show "inv x \<otimes> inv h \<in> (\<Union>j\<in>H. {j \<otimes> inv x})"
   512   proof
   513     show "inv x \<otimes> inv h \<otimes> x \<in> H"
   514       by (simp add: inv_op_closed1 prems)
   515     show "inv x \<otimes> inv h \<in> {inv x \<otimes> inv h \<otimes> x \<otimes> inv x}"
   516       by (simp add: prems m_assoc)
   517   qed
   518 next
   519   fix h
   520   assume "h \<in> H"
   521   show "h \<otimes> inv x \<in> (\<Union>j\<in>H. {inv x \<otimes> inv j})"
   522   proof
   523     show "x \<otimes> inv h \<otimes> inv x \<in> H"
   524       by (simp add: inv_op_closed2 prems)
   525     show "h \<otimes> inv x \<in> {inv x \<otimes> inv (x \<otimes> inv h \<otimes> inv x)}"
   526       by (simp add: prems m_assoc [symmetric] inv_mult_group)
   527   qed
   528 qed
   529 
   530 
   531 subsubsection {*Theorems for @{text "<#>"} with @{text "#>"} or @{text "<#"}.*}
   532 
   533 lemma (in group) setmult_rcos_assoc:
   534      "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G\<rbrakk>
   535       \<Longrightarrow> H <#> (K #> x) = (H <#> K) #> x"
   536 by (force simp add: r_coset_def set_mult_def m_assoc)
   537 
   538 lemma (in group) rcos_assoc_lcos:
   539      "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G\<rbrakk>
   540       \<Longrightarrow> (H #> x) <#> K = H <#> (x <# K)"
   541 by (force simp add: r_coset_def l_coset_def set_mult_def m_assoc)
   542 
   543 lemma (in normal) rcos_mult_step1:
   544      "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
   545       \<Longrightarrow> (H #> x) <#> (H #> y) = (H <#> (x <# H)) #> y"
   546 by (simp add: setmult_rcos_assoc subset
   547               r_coset_subset_G l_coset_subset_G rcos_assoc_lcos)
   548 
   549 lemma (in normal) rcos_mult_step2:
   550      "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
   551       \<Longrightarrow> (H <#> (x <# H)) #> y = (H <#> (H #> x)) #> y"
   552 by (insert coset_eq, simp add: normal_def)
   553 
   554 lemma (in normal) rcos_mult_step3:
   555      "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
   556       \<Longrightarrow> (H <#> (H #> x)) #> y = H #> (x \<otimes> y)"
   557 by (simp add: setmult_rcos_assoc coset_mult_assoc
   558               subgroup_mult_id normal.axioms subset prems)
   559 
   560 lemma (in normal) rcos_sum:
   561      "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
   562       \<Longrightarrow> (H #> x) <#> (H #> y) = H #> (x \<otimes> y)"
   563 by (simp add: rcos_mult_step1 rcos_mult_step2 rcos_mult_step3)
   564 
   565 lemma (in normal) rcosets_mult_eq: "M \<in> rcosets H \<Longrightarrow> H <#> M = M"
   566   -- {* generalizes @{text subgroup_mult_id} *}
   567   by (auto simp add: RCOSETS_def subset
   568         setmult_rcos_assoc subgroup_mult_id normal.axioms prems)
   569 
   570 
   571 subsubsection{*An Equivalence Relation*}
   572 
   573 constdefs (structure G)
   574   r_congruent :: "[('a,'b)monoid_scheme, 'a set] \<Rightarrow> ('a*'a)set"
   575                   ("rcong\<index> _")
   576    "rcong H \<equiv> {(x,y). x \<in> carrier G & y \<in> carrier G & inv x \<otimes> y \<in> H}"
   577 
   578 
   579 lemma (in subgroup) equiv_rcong:
   580    includes group G
   581    shows "equiv (carrier G) (rcong H)"
   582 proof (intro equiv.intro)
   583   show "refl (carrier G) (rcong H)"
   584     by (auto simp add: r_congruent_def refl_def) 
   585 next
   586   show "sym (rcong H)"
   587   proof (simp add: r_congruent_def sym_def, clarify)
   588     fix x y
   589     assume [simp]: "x \<in> carrier G" "y \<in> carrier G" 
   590        and "inv x \<otimes> y \<in> H"
   591     hence "inv (inv x \<otimes> y) \<in> H" by (simp add: m_inv_closed) 
   592     thus "inv y \<otimes> x \<in> H" by (simp add: inv_mult_group)
   593   qed
   594 next
   595   show "trans (rcong H)"
   596   proof (simp add: r_congruent_def trans_def, clarify)
   597     fix x y z
   598     assume [simp]: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
   599        and "inv x \<otimes> y \<in> H" and "inv y \<otimes> z \<in> H"
   600     hence "(inv x \<otimes> y) \<otimes> (inv y \<otimes> z) \<in> H" by simp
   601     hence "inv x \<otimes> (y \<otimes> inv y) \<otimes> z \<in> H" by (simp add: m_assoc del: r_inv) 
   602     thus "inv x \<otimes> z \<in> H" by simp
   603   qed
   604 qed
   605 
   606 text{*Equivalence classes of @{text rcong} correspond to left cosets.
   607   Was there a mistake in the definitions? I'd have expected them to
   608   correspond to right cosets.*}
   609 
   610 (* CB: This is correct, but subtle.
   611    We call H #> a the right coset of a relative to H.  According to
   612    Jacobson, this is what the majority of group theory literature does.
   613    He then defines the notion of congruence relation ~ over monoids as
   614    equivalence relation with a ~ a' & b ~ b' \<Longrightarrow> a*b ~ a'*b'.
   615    Our notion of right congruence induced by K: rcong K appears only in
   616    the context where K is a normal subgroup.  Jacobson doesn't name it.
   617    But in this context left and right cosets are identical.
   618 *)
   619 
   620 lemma (in subgroup) l_coset_eq_rcong:
   621   includes group G
   622   assumes a: "a \<in> carrier G"
   623   shows "a <# H = rcong H `` {a}"
   624 by (force simp add: r_congruent_def l_coset_def m_assoc [symmetric] a ) 
   625 
   626 
   627 subsubsection{*Two Distinct Right Cosets are Disjoint*}
   628 
   629 lemma (in group) rcos_equation:
   630   includes subgroup H G
   631   shows
   632      "\<lbrakk>ha \<otimes> a = h \<otimes> b; a \<in> carrier G;  b \<in> carrier G;  
   633         h \<in> H;  ha \<in> H;  hb \<in> H\<rbrakk>
   634       \<Longrightarrow> hb \<otimes> a \<in> (\<Union>h\<in>H. {h \<otimes> b})"
   635 apply (rule UN_I [of "hb \<otimes> ((inv ha) \<otimes> h)"])
   636 apply (simp add: ); 
   637 apply (simp add: m_assoc transpose_inv)
   638 done
   639 
   640 lemma (in group) rcos_disjoint:
   641   includes subgroup H G
   642   shows "\<lbrakk>a \<in> rcosets H; b \<in> rcosets H; a\<noteq>b\<rbrakk> \<Longrightarrow> a \<inter> b = {}"
   643 apply (simp add: RCOSETS_def r_coset_def)
   644 apply (blast intro: rcos_equation prems sym)
   645 done
   646 
   647 subsection {* Further lemmas for @{text "r_congruent"} *}
   648 
   649 text {* The relation is a congruence *}
   650 
   651 lemma (in normal) congruent_rcong:
   652   shows "congruent2 (rcong H) (rcong H) (\<lambda>a b. a \<otimes> b <# H)"
   653 proof (intro congruent2I[of "carrier G" _ "carrier G" _] equiv_rcong is_group)
   654   fix a b c
   655   assume abrcong: "(a, b) \<in> rcong H"
   656     and ccarr: "c \<in> carrier G"
   657 
   658   from abrcong
   659       have acarr: "a \<in> carrier G"
   660         and bcarr: "b \<in> carrier G"
   661         and abH: "inv a \<otimes> b \<in> H"
   662       unfolding r_congruent_def
   663       by fast+
   664 
   665   note carr = acarr bcarr ccarr
   666 
   667   from ccarr and abH
   668       have "inv c \<otimes> (inv a \<otimes> b) \<otimes> c \<in> H" by (rule inv_op_closed1)
   669   moreover
   670       from carr and inv_closed
   671       have "inv c \<otimes> (inv a \<otimes> b) \<otimes> c = (inv c \<otimes> inv a) \<otimes> (b \<otimes> c)" 
   672       by (force cong: m_assoc)
   673   moreover 
   674       from carr and inv_closed
   675       have "\<dots> = (inv (a \<otimes> c)) \<otimes> (b \<otimes> c)"
   676       by (simp add: inv_mult_group)
   677   ultimately
   678       have "(inv (a \<otimes> c)) \<otimes> (b \<otimes> c) \<in> H" by simp
   679   from carr and this
   680      have "(b \<otimes> c) \<in> (a \<otimes> c) <# H"
   681      by (simp add: lcos_module_rev[OF is_group])
   682   from carr and this and is_subgroup
   683      show "(a \<otimes> c) <# H = (b \<otimes> c) <# H" by (intro l_repr_independence, simp+)
   684 next
   685   fix a b c
   686   assume abrcong: "(a, b) \<in> rcong H"
   687     and ccarr: "c \<in> carrier G"
   688 
   689   from ccarr have "c \<in> Units G" by (simp add: Units_eq)
   690   hence cinvc_one: "inv c \<otimes> c = \<one>" by (rule Units_l_inv)
   691 
   692   from abrcong
   693       have acarr: "a \<in> carrier G"
   694        and bcarr: "b \<in> carrier G"
   695        and abH: "inv a \<otimes> b \<in> H"
   696       by (unfold r_congruent_def, fast+)
   697 
   698   note carr = acarr bcarr ccarr
   699 
   700   from carr and inv_closed
   701      have "inv a \<otimes> b = inv a \<otimes> (\<one> \<otimes> b)" by simp
   702   also from carr and inv_closed
   703       have "\<dots> = inv a \<otimes> (inv c \<otimes> c) \<otimes> b" by simp
   704   also from carr and inv_closed
   705       have "\<dots> = (inv a \<otimes> inv c) \<otimes> (c \<otimes> b)" by (force cong: m_assoc)
   706   also from carr and inv_closed
   707       have "\<dots> = inv (c \<otimes> a) \<otimes> (c \<otimes> b)" by (simp add: inv_mult_group)
   708   finally
   709       have "inv a \<otimes> b = inv (c \<otimes> a) \<otimes> (c \<otimes> b)" .
   710   from abH and this
   711       have "inv (c \<otimes> a) \<otimes> (c \<otimes> b) \<in> H" by simp
   712 
   713   from carr and this
   714      have "(c \<otimes> b) \<in> (c \<otimes> a) <# H"
   715      by (simp add: lcos_module_rev[OF is_group])
   716   from carr and this and is_subgroup
   717      show "(c \<otimes> a) <# H = (c \<otimes> b) <# H" by (intro l_repr_independence, simp+)
   718 qed
   719 
   720 
   721 subsection {*Order of a Group and Lagrange's Theorem*}
   722 
   723 constdefs
   724   order :: "('a, 'b) monoid_scheme \<Rightarrow> nat"
   725   "order S \<equiv> card (carrier S)"
   726 
   727 lemma (in group) rcos_self:
   728   includes subgroup
   729   shows "x \<in> carrier G \<Longrightarrow> x \<in> H #> x"
   730 apply (simp add: r_coset_def)
   731 apply (rule_tac x="\<one>" in bexI) 
   732 apply (auto simp add: ); 
   733 done
   734 
   735 lemma (in group) rcosets_part_G:
   736   includes subgroup
   737   shows "\<Union>(rcosets H) = carrier G"
   738 apply (rule equalityI)
   739  apply (force simp add: RCOSETS_def r_coset_def)
   740 apply (auto simp add: RCOSETS_def intro: rcos_self prems)
   741 done
   742 
   743 lemma (in group) cosets_finite:
   744      "\<lbrakk>c \<in> rcosets H;  H \<subseteq> carrier G;  finite (carrier G)\<rbrakk> \<Longrightarrow> finite c"
   745 apply (auto simp add: RCOSETS_def)
   746 apply (simp add: r_coset_subset_G [THEN finite_subset])
   747 done
   748 
   749 text{*The next two lemmas support the proof of @{text card_cosets_equal}.*}
   750 lemma (in group) inj_on_f:
   751     "\<lbrakk>H \<subseteq> carrier G;  a \<in> carrier G\<rbrakk> \<Longrightarrow> inj_on (\<lambda>y. y \<otimes> inv a) (H #> a)"
   752 apply (rule inj_onI)
   753 apply (subgoal_tac "x \<in> carrier G & y \<in> carrier G")
   754  prefer 2 apply (blast intro: r_coset_subset_G [THEN subsetD])
   755 apply (simp add: subsetD)
   756 done
   757 
   758 lemma (in group) inj_on_g:
   759     "\<lbrakk>H \<subseteq> carrier G;  a \<in> carrier G\<rbrakk> \<Longrightarrow> inj_on (\<lambda>y. y \<otimes> a) H"
   760 by (force simp add: inj_on_def subsetD)
   761 
   762 lemma (in group) card_cosets_equal:
   763      "\<lbrakk>c \<in> rcosets H;  H \<subseteq> carrier G; finite(carrier G)\<rbrakk>
   764       \<Longrightarrow> card c = card H"
   765 apply (auto simp add: RCOSETS_def)
   766 apply (rule card_bij_eq)
   767      apply (rule inj_on_f, assumption+)
   768     apply (force simp add: m_assoc subsetD r_coset_def)
   769    apply (rule inj_on_g, assumption+)
   770   apply (force simp add: m_assoc subsetD r_coset_def)
   771  txt{*The sets @{term "H #> a"} and @{term "H"} are finite.*}
   772  apply (simp add: r_coset_subset_G [THEN finite_subset])
   773 apply (blast intro: finite_subset)
   774 done
   775 
   776 lemma (in group) rcosets_subset_PowG:
   777      "subgroup H G  \<Longrightarrow> rcosets H \<subseteq> Pow(carrier G)"
   778 apply (simp add: RCOSETS_def)
   779 apply (blast dest: r_coset_subset_G subgroup.subset)
   780 done
   781 
   782 
   783 theorem (in group) lagrange:
   784      "\<lbrakk>finite(carrier G); subgroup H G\<rbrakk>
   785       \<Longrightarrow> card(rcosets H) * card(H) = order(G)"
   786 apply (simp (no_asm_simp) add: order_def rcosets_part_G [symmetric])
   787 apply (subst mult_commute)
   788 apply (rule card_partition)
   789    apply (simp add: rcosets_subset_PowG [THEN finite_subset])
   790   apply (simp add: rcosets_part_G)
   791  apply (simp add: card_cosets_equal subgroup.subset)
   792 apply (simp add: rcos_disjoint)
   793 done
   794 
   795 
   796 subsection {*Quotient Groups: Factorization of a Group*}
   797 
   798 constdefs
   799   FactGroup :: "[('a,'b) monoid_scheme, 'a set] \<Rightarrow> ('a set) monoid"
   800      (infixl "Mod" 65)
   801     --{*Actually defined for groups rather than monoids*}
   802   "FactGroup G H \<equiv>
   803     \<lparr>carrier = rcosets\<^bsub>G\<^esub> H, mult = set_mult G, one = H\<rparr>"
   804 
   805 lemma (in normal) setmult_closed:
   806      "\<lbrakk>K1 \<in> rcosets H; K2 \<in> rcosets H\<rbrakk> \<Longrightarrow> K1 <#> K2 \<in> rcosets H"
   807 by (auto simp add: rcos_sum RCOSETS_def)
   808 
   809 lemma (in normal) setinv_closed:
   810      "K \<in> rcosets H \<Longrightarrow> set_inv K \<in> rcosets H"
   811 by (auto simp add: rcos_inv RCOSETS_def)
   812 
   813 lemma (in normal) rcosets_assoc:
   814      "\<lbrakk>M1 \<in> rcosets H; M2 \<in> rcosets H; M3 \<in> rcosets H\<rbrakk>
   815       \<Longrightarrow> M1 <#> M2 <#> M3 = M1 <#> (M2 <#> M3)"
   816 by (auto simp add: RCOSETS_def rcos_sum m_assoc)
   817 
   818 lemma (in subgroup) subgroup_in_rcosets:
   819   includes group G
   820   shows "H \<in> rcosets H"
   821 proof -
   822   have "H #> \<one> = H"
   823     by (rule coset_join2, auto)
   824   then show ?thesis
   825     by (auto simp add: RCOSETS_def)
   826 qed
   827 
   828 lemma (in normal) rcosets_inv_mult_group_eq:
   829      "M \<in> rcosets H \<Longrightarrow> set_inv M <#> M = H"
   830 by (auto simp add: RCOSETS_def rcos_inv rcos_sum subgroup.subset normal.axioms prems)
   831 
   832 theorem (in normal) factorgroup_is_group:
   833   "group (G Mod H)"
   834 apply (simp add: FactGroup_def)
   835 apply (rule groupI)
   836     apply (simp add: setmult_closed)
   837    apply (simp add: normal_imp_subgroup subgroup_in_rcosets [OF is_group])
   838   apply (simp add: restrictI setmult_closed rcosets_assoc)
   839  apply (simp add: normal_imp_subgroup
   840                   subgroup_in_rcosets rcosets_mult_eq)
   841 apply (auto dest: rcosets_inv_mult_group_eq simp add: setinv_closed)
   842 done
   843 
   844 lemma mult_FactGroup [simp]: "X \<otimes>\<^bsub>(G Mod H)\<^esub> X' = X <#>\<^bsub>G\<^esub> X'"
   845   by (simp add: FactGroup_def) 
   846 
   847 lemma (in normal) inv_FactGroup:
   848      "X \<in> carrier (G Mod H) \<Longrightarrow> inv\<^bsub>G Mod H\<^esub> X = set_inv X"
   849 apply (rule group.inv_equality [OF factorgroup_is_group]) 
   850 apply (simp_all add: FactGroup_def setinv_closed rcosets_inv_mult_group_eq)
   851 done
   852 
   853 text{*The coset map is a homomorphism from @{term G} to the quotient group
   854   @{term "G Mod H"}*}
   855 lemma (in normal) r_coset_hom_Mod:
   856   "(\<lambda>a. H #> a) \<in> hom G (G Mod H)"
   857   by (auto simp add: FactGroup_def RCOSETS_def Pi_def hom_def rcos_sum)
   858 
   859  
   860 subsection{*The First Isomorphism Theorem*}
   861 
   862 text{*The quotient by the kernel of a homomorphism is isomorphic to the 
   863   range of that homomorphism.*}
   864 
   865 constdefs
   866   kernel :: "('a, 'm) monoid_scheme \<Rightarrow> ('b, 'n) monoid_scheme \<Rightarrow> 
   867              ('a \<Rightarrow> 'b) \<Rightarrow> 'a set" 
   868     --{*the kernel of a homomorphism*}
   869   "kernel G H h \<equiv> {x. x \<in> carrier G & h x = \<one>\<^bsub>H\<^esub>}";
   870 
   871 lemma (in group_hom) subgroup_kernel: "subgroup (kernel G H h) G"
   872 apply (rule subgroup.intro) 
   873 apply (auto simp add: kernel_def group.intro prems) 
   874 done
   875 
   876 text{*The kernel of a homomorphism is a normal subgroup*}
   877 lemma (in group_hom) normal_kernel: "(kernel G H h) \<lhd> G"
   878 apply (simp add: G.normal_inv_iff subgroup_kernel)
   879 apply (simp add: kernel_def)
   880 done
   881 
   882 lemma (in group_hom) FactGroup_nonempty:
   883   assumes X: "X \<in> carrier (G Mod kernel G H h)"
   884   shows "X \<noteq> {}"
   885 proof -
   886   from X
   887   obtain g where "g \<in> carrier G" 
   888              and "X = kernel G H h #> g"
   889     by (auto simp add: FactGroup_def RCOSETS_def)
   890   thus ?thesis 
   891    by (auto simp add: kernel_def r_coset_def image_def intro: hom_one)
   892 qed
   893 
   894 
   895 lemma (in group_hom) FactGroup_contents_mem:
   896   assumes X: "X \<in> carrier (G Mod (kernel G H h))"
   897   shows "contents (h`X) \<in> carrier H"
   898 proof -
   899   from X
   900   obtain g where g: "g \<in> carrier G" 
   901              and "X = kernel G H h #> g"
   902     by (auto simp add: FactGroup_def RCOSETS_def)
   903   hence "h ` X = {h g}" by (auto simp add: kernel_def r_coset_def image_def g)
   904   thus ?thesis by (auto simp add: g)
   905 qed
   906 
   907 lemma (in group_hom) FactGroup_hom:
   908      "(\<lambda>X. contents (h`X)) \<in> hom (G Mod (kernel G H h)) H"
   909 apply (simp add: hom_def FactGroup_contents_mem  normal.factorgroup_is_group [OF normal_kernel] group.axioms monoid.m_closed)  
   910 proof (simp add: hom_def funcsetI FactGroup_contents_mem, intro ballI) 
   911   fix X and X'
   912   assume X:  "X  \<in> carrier (G Mod kernel G H h)"
   913      and X': "X' \<in> carrier (G Mod kernel G H h)"
   914   then
   915   obtain g and g'
   916            where "g \<in> carrier G" and "g' \<in> carrier G" 
   917              and "X = kernel G H h #> g" and "X' = kernel G H h #> g'"
   918     by (auto simp add: FactGroup_def RCOSETS_def)
   919   hence all: "\<forall>x\<in>X. h x = h g" "\<forall>x\<in>X'. h x = h g'" 
   920     and Xsub: "X \<subseteq> carrier G" and X'sub: "X' \<subseteq> carrier G"
   921     by (force simp add: kernel_def r_coset_def image_def)+
   922   hence "h ` (X <#> X') = {h g \<otimes>\<^bsub>H\<^esub> h g'}" using X X'
   923     by (auto dest!: FactGroup_nonempty
   924              simp add: set_mult_def image_eq_UN 
   925                        subsetD [OF Xsub] subsetD [OF X'sub]) 
   926   thus "contents (h ` (X <#> X')) = contents (h ` X) \<otimes>\<^bsub>H\<^esub> contents (h ` X')"
   927     by (simp add: all image_eq_UN FactGroup_nonempty X X')  
   928 qed
   929 
   930 
   931 text{*Lemma for the following injectivity result*}
   932 lemma (in group_hom) FactGroup_subset:
   933      "\<lbrakk>g \<in> carrier G; g' \<in> carrier G; h g = h g'\<rbrakk>
   934       \<Longrightarrow>  kernel G H h #> g \<subseteq> kernel G H h #> g'"
   935 apply (clarsimp simp add: kernel_def r_coset_def image_def);
   936 apply (rename_tac y)  
   937 apply (rule_tac x="y \<otimes> g \<otimes> inv g'" in exI) 
   938 apply (simp add: G.m_assoc); 
   939 done
   940 
   941 lemma (in group_hom) FactGroup_inj_on:
   942      "inj_on (\<lambda>X. contents (h ` X)) (carrier (G Mod kernel G H h))"
   943 proof (simp add: inj_on_def, clarify) 
   944   fix X and X'
   945   assume X:  "X  \<in> carrier (G Mod kernel G H h)"
   946      and X': "X' \<in> carrier (G Mod kernel G H h)"
   947   then
   948   obtain g and g'
   949            where gX: "g \<in> carrier G"  "g' \<in> carrier G" 
   950               "X = kernel G H h #> g" "X' = kernel G H h #> g'"
   951     by (auto simp add: FactGroup_def RCOSETS_def)
   952   hence all: "\<forall>x\<in>X. h x = h g" "\<forall>x\<in>X'. h x = h g'" 
   953     by (force simp add: kernel_def r_coset_def image_def)+
   954   assume "contents (h ` X) = contents (h ` X')"
   955   hence h: "h g = h g'"
   956     by (simp add: image_eq_UN all FactGroup_nonempty X X') 
   957   show "X=X'" by (rule equalityI) (simp_all add: FactGroup_subset h gX) 
   958 qed
   959 
   960 text{*If the homomorphism @{term h} is onto @{term H}, then so is the
   961 homomorphism from the quotient group*}
   962 lemma (in group_hom) FactGroup_onto:
   963   assumes h: "h ` carrier G = carrier H"
   964   shows "(\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h) = carrier H"
   965 proof
   966   show "(\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h) \<subseteq> carrier H"
   967     by (auto simp add: FactGroup_contents_mem)
   968   show "carrier H \<subseteq> (\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h)"
   969   proof
   970     fix y
   971     assume y: "y \<in> carrier H"
   972     with h obtain g where g: "g \<in> carrier G" "h g = y"
   973       by (blast elim: equalityE); 
   974     hence "(\<Union>x\<in>kernel G H h #> g. {h x}) = {y}" 
   975       by (auto simp add: y kernel_def r_coset_def) 
   976     with g show "y \<in> (\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h)" 
   977       by (auto intro!: bexI simp add: FactGroup_def RCOSETS_def image_eq_UN)
   978   qed
   979 qed
   980 
   981 
   982 text{*If @{term h} is a homomorphism from @{term G} onto @{term H}, then the
   983  quotient group @{term "G Mod (kernel G H h)"} is isomorphic to @{term H}.*}
   984 theorem (in group_hom) FactGroup_iso:
   985   "h ` carrier G = carrier H
   986    \<Longrightarrow> (\<lambda>X. contents (h`X)) \<in> (G Mod (kernel G H h)) \<cong> H"
   987 by (simp add: iso_def FactGroup_hom FactGroup_inj_on bij_betw_def 
   988               FactGroup_onto) 
   989 
   990 
   991 end