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