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