# Theory Coset

Up to index of Isabelle/HOL/HOL-Algebra

theory Coset
imports Group Exponent
begin

    (*  Title:      HOL/Algebra/Coset.thy
        ID:         $Id: Coset.thy,v 1.16 2005/06/17 14:13:05 haftmann Exp $
        Author:     Florian Kammueller, with new proofs by L C Paulson
    *)

    header{*Cosets and Quotient Groups*}

    theory Coset imports Group Exponent begin

    constdefs (structure G)
      r_coset    :: "[_, 'a set, 'a] => 'a set"    (infixl "#>\<index>" 60)
      "H #> a ≡ \<Union>h∈H. {h ⊗ a}"

      l_coset    :: "[_, 'a, 'a set] => 'a set"    (infixl "<#\<index>" 60)
      "a <# H ≡ \<Union>h∈H. {a ⊗ h}"

      RCOSETS  :: "[_, 'a set] => ('a set)set"   ("rcosets\<index> _" [81] 80)
      "rcosets H ≡ \<Union>a∈carrier G. {H #> a}"

      set_mult  :: "[_, 'a set ,'a set] => 'a set" (infixl "<#>\<index>" 60)
      "H <#> K ≡ \<Union>h∈H. \<Union>k∈K. {h ⊗ k}"

      SET_INV :: "[_,'a set] => 'a set"  ("set'_inv\<index> _" [81] 80)
      "set_inv H ≡ \<Union>h∈H. {inv h}"

    locale normal = subgroup + group +
      assumes coset_eq: "(∀x ∈ carrier G. H #> x = x <# H)"

    syntax
      "@normal" :: "['a set, ('a, 'b) monoid_scheme] => bool"  (infixl "\<lhd>" 60)

    translations
      "H \<lhd> G" == "normal H G"

    subsection {*Basic Properties of Cosets*}

    lemma (in group) coset_mult_assoc:
         "[| M ⊆ carrier G; g ∈ carrier G; h ∈ carrier G |]
          ==> (M #> g) #> h = M #> (g ⊗ h)"
    by (force simp add: r_coset_def m_assoc)

    lemma (in group) coset_mult_one [simp]: "M ⊆ carrier G ==> M #> \<one> = M"
    by (force simp add: r_coset_def)

    lemma (in group) coset_mult_inv1:
         "[| M #> (x ⊗ (inv y)) = M;  x ∈ carrier G ; y ∈ carrier G;
             M ⊆ carrier G |] ==> M #> x = M #> y"
    apply (erule subst [of concl: "%z. M #> x = z #> y"])
    apply (simp add: coset_mult_assoc m_assoc)
    done

    lemma (in group) coset_mult_inv2:
         "[| M #> x = M #> y;  x ∈ carrier G;  y ∈ carrier G;  M ⊆ carrier G |]
          ==> M #> (x ⊗ (inv y)) = M "
    apply (simp add: coset_mult_assoc [symmetric])
    apply (simp add: coset_mult_assoc)
    done

    lemma (in group) coset_join1:
         "[| H #> x = H;  x ∈ carrier G;  subgroup H G |] ==> x ∈ H"
    apply (erule subst)
    apply (simp add: r_coset_def)
    apply (blast intro: l_one subgroup.one_closed sym)
    done

    lemma (in group) solve_equation:
        "[|subgroup H G; x ∈ H; y ∈ H|] ==> ∃h∈H. y = h ⊗ x"
    apply (rule bexI [of _ "y ⊗ (inv x)"])
    apply (auto simp add: subgroup.m_closed subgroup.m_inv_closed m_assoc
                          subgroup.subset [THEN subsetD])
    done

    lemma (in group) repr_independence:
         "[|y ∈ H #> x;  x ∈ carrier G; subgroup H G|] ==> H #> x = H #> y"
    by (auto simp add: r_coset_def m_assoc [symmetric]
                       subgroup.subset [THEN subsetD]
                       subgroup.m_closed solve_equation)

    lemma (in group) coset_join2:
         "[|x ∈ carrier G;  subgroup H G;  x∈H|] ==> H #> x = H"
      --{*Alternative proof is to put @{term "x=\<one>"} in @{text repr_independence}.*}
    by (force simp add: subgroup.m_closed r_coset_def solve_equation)

    lemma (in group) r_coset_subset_G:
         "[| H ⊆ carrier G; x ∈ carrier G |] ==> H #> x ⊆ carrier G"
    by (auto simp add: r_coset_def)

    lemma (in group) rcosI:
         "[| h ∈ H; H ⊆ carrier G; x ∈ carrier G|] ==> h ⊗ x ∈ H #> x"
    by (auto simp add: r_coset_def)

    lemma (in group) rcosetsI:
         "[|H ⊆ carrier G; x ∈ carrier G|] ==> H #> x ∈ rcosets H"
    by (auto simp add: RCOSETS_def)

    text{*Really needed?*}
    lemma (in group) transpose_inv:
         "[| x ⊗ y = z;  x ∈ carrier G;  y ∈ carrier G;  z ∈ carrier G |]
          ==> (inv x) ⊗ z = y"
    by (force simp add: m_assoc [symmetric])

    lemma (in group) rcos_self: "[| x ∈ carrier G; subgroup H G |] ==> x ∈ H #> x"
    apply (simp add: r_coset_def)
    apply (blast intro: sym l_one subgroup.subset [THEN subsetD]
                        subgroup.one_closed)
    done

    subsection {* Normal subgroups *}

    lemma normal_imp_subgroup: "H \<lhd> G ==> subgroup H G"
      by (simp add: normal_def subgroup_def)

    lemma (in group) normalI:
      "subgroup H G ==> (∀x ∈ carrier G. H #> x = x <# H) ==> H \<lhd> G";
      by (simp add: normal_def normal_axioms_def prems)

    lemma (in normal) inv_op_closed1:
         "[|x ∈ carrier G; h ∈ H|] ==> (inv x) ⊗ h ⊗ x ∈ H"
    apply (insert coset_eq)
    apply (auto simp add: l_coset_def r_coset_def)
    apply (drule bspec, assumption)
    apply (drule equalityD1 [THEN subsetD], blast, clarify)
    apply (simp add: m_assoc)
    apply (simp add: m_assoc [symmetric])
    done

    lemma (in normal) inv_op_closed2:
         "[|x ∈ carrier G; h ∈ H|] ==> x ⊗ h ⊗ (inv x) ∈ H"
    apply (subgoal_tac "inv (inv x) ⊗ h ⊗ (inv x) ∈ H")
    apply (simp add: );
    apply (blast intro: inv_op_closed1)
    done

    text{*Alternative characterization of normal subgroups*}
    lemma (in group) normal_inv_iff:
         "(N \<lhd> G) =
          (subgroup N G & (∀x ∈ carrier G. ∀h ∈ N. x ⊗ h ⊗ (inv x) ∈ N))"
          (is "_ = ?rhs")
    proof
      assume N: "N \<lhd> G"
      show ?rhs
        by (blast intro: N normal.inv_op_closed2 normal_imp_subgroup)
    next
      assume ?rhs
      hence sg: "subgroup N G"
        and closed: "!!x. x∈carrier G ==> ∀h∈N. x ⊗ h ⊗ inv x ∈ N" by auto
      hence sb: "N ⊆ carrier G" by (simp add: subgroup.subset)
      show "N \<lhd> G"
      proof (intro normalI [OF sg], simp add: l_coset_def r_coset_def, clarify)
        fix x
        assume x: "x ∈ carrier G"
        show "(\<Union>h∈N. {h ⊗ x}) = (\<Union>h∈N. {x ⊗ h})"
        proof
          show "(\<Union>h∈N. {h ⊗ x}) ⊆ (\<Union>h∈N. {x ⊗ h})"
          proof clarify
            fix n
            assume n: "n ∈ N"
            show "n ⊗ x ∈ (\<Union>h∈N. {x ⊗ h})"
            proof
              from closed [of "inv x"]
              show "inv x ⊗ n ⊗ x ∈ N" by (simp add: x n)
              show "n ⊗ x ∈ {x ⊗ (inv x ⊗ n ⊗ x)}"
                by (simp add: x n m_assoc [symmetric] sb [THEN subsetD])
            qed
          qed
        next
          show "(\<Union>h∈N. {x ⊗ h}) ⊆ (\<Union>h∈N. {h ⊗ x})"
          proof clarify
            fix n
            assume n: "n ∈ N"
            show "x ⊗ n ∈ (\<Union>h∈N. {h ⊗ x})"
            proof
              show "x ⊗ n ⊗ inv x ∈ N" by (simp add: x n closed)
              show "x ⊗ n ∈ {x ⊗ n ⊗ inv x ⊗ x}"
                by (simp add: x n m_assoc sb [THEN subsetD])
            qed
          qed
        qed
      qed
    qed

    subsection{*More Properties of Cosets*}

    lemma (in group) lcos_m_assoc:
         "[| M ⊆ carrier G; g ∈ carrier G; h ∈ carrier G |]
          ==> g <# (h <# M) = (g ⊗ h) <# M"
    by (force simp add: l_coset_def m_assoc)

    lemma (in group) lcos_mult_one: "M ⊆ carrier G ==> \<one> <# M = M"
    by (force simp add: l_coset_def)

    lemma (in group) l_coset_subset_G:
         "[| H ⊆ carrier G; x ∈ carrier G |] ==> x <# H ⊆ carrier G"
    by (auto simp add: l_coset_def subsetD)

    lemma (in group) l_coset_swap:
         "[|y ∈ x <# H;  x ∈ carrier G;  subgroup H G|] ==> x ∈ y <# H"
    proof (simp add: l_coset_def)
      assume "∃h∈H. y = x ⊗ h"
        and x: "x ∈ carrier G"
        and sb: "subgroup H G"
      then obtain h' where h': "h' ∈ H & x ⊗ h' = y" by blast
      show "∃h∈H. x = y ⊗ h"
      proof
        show "x = y ⊗ inv h'" using h' x sb
          by (auto simp add: m_assoc subgroup.subset [THEN subsetD])
        show "inv h' ∈ H" using h' sb
          by (auto simp add: subgroup.subset [THEN subsetD] subgroup.m_inv_closed)
      qed
    qed

    lemma (in group) l_coset_carrier:
         "[| y ∈ x <# H;  x ∈ carrier G;  subgroup H G |] ==> y ∈ carrier G"
    by (auto simp add: l_coset_def m_assoc
                       subgroup.subset [THEN subsetD] subgroup.m_closed)

    lemma (in group) l_repr_imp_subset:
      assumes y: "y ∈ x <# H" and x: "x ∈ carrier G" and sb: "subgroup H G"
      shows "y <# H ⊆ x <# H"
    proof -
      from y
      obtain h' where "h' ∈ H" "x ⊗ h' = y" by (auto simp add: l_coset_def)
      thus ?thesis using x sb
        by (auto simp add: l_coset_def m_assoc
                           subgroup.subset [THEN subsetD] subgroup.m_closed)
    qed

    lemma (in group) l_repr_independence:
      assumes y: "y ∈ x <# H" and x: "x ∈ carrier G" and sb: "subgroup H G"
      shows "x <# H = y <# H"
    proof
      show "x <# H ⊆ y <# H"
        by (rule l_repr_imp_subset,
            (blast intro: l_coset_swap l_coset_carrier y x sb)+)
      show "y <# H ⊆ x <# H" by (rule l_repr_imp_subset [OF y x sb])
    qed

    lemma (in group) setmult_subset_G:
         "[|H ⊆ carrier G; K ⊆ carrier G|] ==> H <#> K ⊆ carrier G"
    by (auto simp add: set_mult_def subsetD)

    lemma (in group) subgroup_mult_id: "subgroup H G ==> H <#> H = H"
    apply (auto simp add: subgroup.m_closed set_mult_def Sigma_def image_def)
    apply (rule_tac x = x in bexI)
    apply (rule bexI [of _ "\<one>"])
    apply (auto simp add: subgroup.m_closed subgroup.one_closed
                          r_one subgroup.subset [THEN subsetD])
    done

    subsubsection {* Set of inverses of an @{text r_coset}. *}

    lemma (in normal) rcos_inv:
      assumes x:     "x ∈ carrier G"
      shows "set_inv (H #> x) = H #> (inv x)"
    proof (simp add: r_coset_def SET_INV_def x inv_mult_group, safe)
      fix h
      assume "h ∈ H"
      show "inv x ⊗ inv h ∈ (\<Union>j∈H. {j ⊗ inv x})"
      proof
        show "inv x ⊗ inv h ⊗ x ∈ H"
          by (simp add: inv_op_closed1 prems)
        show "inv x ⊗ inv h ∈ {inv x ⊗ inv h ⊗ x ⊗ inv x}"
          by (simp add: prems m_assoc)
      qed
    next
      fix h
      assume "h ∈ H"
      show "h ⊗ inv x ∈ (\<Union>j∈H. {inv x ⊗ inv j})"
      proof
        show "x ⊗ inv h ⊗ inv x ∈ H"
          by (simp add: inv_op_closed2 prems)
        show "h ⊗ inv x ∈ {inv x ⊗ inv (x ⊗ inv h ⊗ inv x)}"
          by (simp add: prems m_assoc [symmetric] inv_mult_group)
      qed
    qed

    subsubsection {*Theorems for @{text "<#>"} with @{text "#>"} or @{text "<#"}.*}

    lemma (in group) setmult_rcos_assoc:
         "[|H ⊆ carrier G; K ⊆ carrier G; x ∈ carrier G|]
          ==> H <#> (K #> x) = (H <#> K) #> x"
    by (force simp add: r_coset_def set_mult_def m_assoc)

    lemma (in group) rcos_assoc_lcos:
         "[|H ⊆ carrier G; K ⊆ carrier G; x ∈ carrier G|]
          ==> (H #> x) <#> K = H <#> (x <# K)"
    by (force simp add: r_coset_def l_coset_def set_mult_def m_assoc)

    lemma (in normal) rcos_mult_step1:
         "[|x ∈ carrier G; y ∈ carrier G|]
          ==> (H #> x) <#> (H #> y) = (H <#> (x <# H)) #> y"
    by (simp add: setmult_rcos_assoc subset
                  r_coset_subset_G l_coset_subset_G rcos_assoc_lcos)

    lemma (in normal) rcos_mult_step2:
         "[|x ∈ carrier G; y ∈ carrier G|]
          ==> (H <#> (x <# H)) #> y = (H <#> (H #> x)) #> y"
    by (insert coset_eq, simp add: normal_def)

    lemma (in normal) rcos_mult_step3:
         "[|x ∈ carrier G; y ∈ carrier G|]
          ==> (H <#> (H #> x)) #> y = H #> (x ⊗ y)"
    by (simp add: setmult_rcos_assoc coset_mult_assoc
                  subgroup_mult_id subset prems)

    lemma (in normal) rcos_sum:
         "[|x ∈ carrier G; y ∈ carrier G|]
          ==> (H #> x) <#> (H #> y) = H #> (x ⊗ y)"
    by (simp add: rcos_mult_step1 rcos_mult_step2 rcos_mult_step3)

    lemma (in normal) rcosets_mult_eq: "M ∈ rcosets H ==> H <#> M = M"
      -- {* generalizes @{text subgroup_mult_id} *}
      by (auto simp add: RCOSETS_def subset
            setmult_rcos_assoc subgroup_mult_id prems)

    subsubsection{*An Equivalence Relation*}

    constdefs (structure G)
      r_congruent :: "[('a,'b)monoid_scheme, 'a set] => ('a*'a)set"
                      ("rcong\<index> _")
       "rcong H ≡ {(x,y). x ∈ carrier G & y ∈ carrier G & inv x ⊗ y ∈ H}"

    lemma (in subgroup) equiv_rcong:
       includes group G
       shows "equiv (carrier G) (rcong H)"
    proof (intro equiv.intro)
      show "refl (carrier G) (rcong H)"
        by (auto simp add: r_congruent_def refl_def)
    next
      show "sym (rcong H)"
      proof (simp add: r_congruent_def sym_def, clarify)
        fix x y
        assume [simp]: "x ∈ carrier G" "y ∈ carrier G"
           and "inv x ⊗ y ∈ H"
        hence "inv (inv x ⊗ y) ∈ H" by (simp add: m_inv_closed)
        thus "inv y ⊗ x ∈ H" by (simp add: inv_mult_group)
      qed
    next
      show "trans (rcong H)"
      proof (simp add: r_congruent_def trans_def, clarify)
        fix x y z
        assume [simp]: "x ∈ carrier G" "y ∈ carrier G" "z ∈ carrier G"
           and "inv x ⊗ y ∈ H" and "inv y ⊗ z ∈ H"
        hence "(inv x ⊗ y) ⊗ (inv y ⊗ z) ∈ H" by simp
        hence "inv x ⊗ (y ⊗ inv y) ⊗ z ∈ H" by (simp add: m_assoc del: r_inv)
        thus "inv x ⊗ z ∈ H" by simp
      qed
    qed

    text{*Equivalence classes of @{text rcong} correspond to left cosets.
      Was there a mistake in the definitions? I'd have expected them to
      correspond to right cosets.*}

    (* CB: This is correct, but subtle.
       We call H #> a the right coset of a relative to H.  According to
       Jacobson, this is what the majority of group theory literature does.
       He then defines the notion of congruence relation ~ over monoids as
       equivalence relation with a ~ a' & b ~ b' ==> a*b ~ a'*b'.
       Our notion of right congruence induced by K: rcong K appears only in
       the context where K is a normal subgroup.  Jacobson doesn't name it.
       But in this context left and right cosets are identical.
    *)

    lemma (in subgroup) l_coset_eq_rcong:
      includes group G
      assumes a: "a ∈ carrier G"
      shows "a <# H = rcong H `` {a}"
    by (force simp add: r_congruent_def l_coset_def m_assoc [symmetric] a )

    subsubsection{*Two distinct right cosets are disjoint*}

    lemma (in group) rcos_equation:
      includes subgroup H G
      shows
         "[|ha ⊗ a = h ⊗ b; a ∈ carrier G;  b ∈ carrier G;
            h ∈ H;  ha ∈ H;  hb ∈ H|]
          ==> hb ⊗ a ∈ (\<Union>h∈H. {h ⊗ b})"
    apply (rule UN_I [of "hb ⊗ ((inv ha) ⊗ h)"])
    apply (simp add: );
    apply (simp add: m_assoc transpose_inv)
    done

    lemma (in group) rcos_disjoint:
      includes subgroup H G
      shows "[|a ∈ rcosets H; b ∈ rcosets H; a≠b|] ==> a ∩ b = {}"
    apply (simp add: RCOSETS_def r_coset_def)
    apply (blast intro: rcos_equation prems sym)
    done

    subsection {*Order of a Group and Lagrange's Theorem*}

    constdefs
      order :: "('a, 'b) monoid_scheme => nat"
      "order S ≡ card (carrier S)"

    lemma (in group) rcos_self:
      includes subgroup
      shows "x ∈ carrier G ==> x ∈ H #> x"
    apply (simp add: r_coset_def)
    apply (rule_tac x="\<one>" in bexI)
    apply (auto simp add: );
    done

    lemma (in group) rcosets_part_G:
      includes subgroup
      shows "\<Union>(rcosets H) = carrier G"
    apply (rule equalityI)
     apply (force simp add: RCOSETS_def r_coset_def)
    apply (auto simp add: RCOSETS_def intro: rcos_self prems)
    done

    lemma (in group) cosets_finite:
         "[|c ∈ rcosets H;  H ⊆ carrier G;  finite (carrier G)|] ==> finite c"
    apply (auto simp add: RCOSETS_def)
    apply (simp add: r_coset_subset_G [THEN finite_subset])
    done

    text{*The next two lemmas support the proof of @{text card_cosets_equal}.*}
    lemma (in group) inj_on_f:
        "[|H ⊆ carrier G;  a ∈ carrier G|] ==> inj_on (λy. y ⊗ inv a) (H #> a)"
    apply (rule inj_onI)
    apply (subgoal_tac "x ∈ carrier G & y ∈ carrier G")
     prefer 2 apply (blast intro: r_coset_subset_G [THEN subsetD])
    apply (simp add: subsetD)
    done

    lemma (in group) inj_on_g:
        "[|H ⊆ carrier G;  a ∈ carrier G|] ==> inj_on (λy. y ⊗ a) H"
    by (force simp add: inj_on_def subsetD)

    lemma (in group) card_cosets_equal:
         "[|c ∈ rcosets H;  H ⊆ carrier G; finite(carrier G)|]
          ==> card c = card H"
    apply (auto simp add: RCOSETS_def)
    apply (rule card_bij_eq)
         apply (rule inj_on_f, assumption+)
        apply (force simp add: m_assoc subsetD r_coset_def)
       apply (rule inj_on_g, assumption+)
      apply (force simp add: m_assoc subsetD r_coset_def)
     txt{*The sets @{term "H #> a"} and @{term "H"} are finite.*}
     apply (simp add: r_coset_subset_G [THEN finite_subset])
    apply (blast intro: finite_subset)
    done

    lemma (in group) rcosets_subset_PowG:
         "subgroup H G  ==> rcosets H ⊆ Pow(carrier G)"
    apply (simp add: RCOSETS_def)
    apply (blast dest: r_coset_subset_G subgroup.subset)
    done

    theorem (in group) lagrange:
         "[|finite(carrier G); subgroup H G|]
          ==> card(rcosets H) * card(H) = order(G)"
    apply (simp (no_asm_simp) add: order_def rcosets_part_G [symmetric])
    apply (subst mult_commute)
    apply (rule card_partition)
       apply (simp add: rcosets_subset_PowG [THEN finite_subset])
      apply (simp add: rcosets_part_G)
     apply (simp add: card_cosets_equal subgroup.subset)
    apply (simp add: rcos_disjoint)
    done

    subsection {*Quotient Groups: Factorization of a Group*}

    constdefs
      FactGroup :: "[('a,'b) monoid_scheme, 'a set] => ('a set) monoid"
         (infixl "Mod" 65)
        --{*Actually defined for groups rather than monoids*}
      "FactGroup G H ≡
        (|carrier = rcosetsG H, mult = set_mult G, one = H|)),"

    lemma (in normal) setmult_closed:
         "[|K1 ∈ rcosets H; K2 ∈ rcosets H|] ==> K1 <#> K2 ∈ rcosets H"
    by (auto simp add: rcos_sum RCOSETS_def)

    lemma (in normal) setinv_closed:
         "K ∈ rcosets H ==> set_inv K ∈ rcosets H"
    by (auto simp add: rcos_inv RCOSETS_def)

    lemma (in normal) rcosets_assoc:
         "[|M1 ∈ rcosets H; M2 ∈ rcosets H; M3 ∈ rcosets H|]
          ==> M1 <#> M2 <#> M3 = M1 <#> (M2 <#> M3)"
    by (auto simp add: RCOSETS_def rcos_sum m_assoc)

    lemma (in subgroup) subgroup_in_rcosets:
      includes group G
      shows "H ∈ rcosets H"
    proof -
      have "H #> \<one> = H"
        by (rule coset_join2, auto)
      then show ?thesis
        by (auto simp add: RCOSETS_def)
    qed

    lemma (in normal) rcosets_inv_mult_group_eq:
         "M ∈ rcosets H ==> set_inv M <#> M = H"
    by (auto simp add: RCOSETS_def rcos_inv rcos_sum subgroup.subset prems)

    theorem (in normal) factorgroup_is_group:
      "group (G Mod H)"
    apply (simp add: FactGroup_def)
    apply (rule groupI)
        apply (simp add: setmult_closed)
       apply (simp add: normal_imp_subgroup subgroup_in_rcosets [OF is_group])
      apply (simp add: restrictI setmult_closed rcosets_assoc)
     apply (simp add: normal_imp_subgroup
                      subgroup_in_rcosets rcosets_mult_eq)
    apply (auto dest: rcosets_inv_mult_group_eq simp add: setinv_closed)
    done

    lemma mult_FactGroup [simp]: "X ⊗(G Mod H) X' = X <#>G X'"
      by (simp add: FactGroup_def)

    lemma (in normal) inv_FactGroup:
         "X ∈ carrier (G Mod H) ==> invG Mod H X = set_inv X"
    apply (rule group.inv_equality [OF factorgroup_is_group])
    apply (simp_all add: FactGroup_def setinv_closed rcosets_inv_mult_group_eq)
    done

    text{*The coset map is a homomorphism from @{term G} to the quotient group
      @{term "G Mod H"}*}
    lemma (in normal) r_coset_hom_Mod:
      "(λa. H #> a) ∈ hom G (G Mod H)"
      by (auto simp add: FactGroup_def RCOSETS_def Pi_def hom_def rcos_sum)

    subsection{*The First Isomorphism Theorem*}

    text{*The quotient by the kernel of a homomorphism is isomorphic to the
      range of that homomorphism.*}

    constdefs
      kernel :: "('a, 'm) monoid_scheme => ('b, 'n) monoid_scheme =>
                 ('a => 'b) => 'a set"
        --{*the kernel of a homomorphism*}
      "kernel G H h ≡ {x. x ∈ carrier G & h x = \<one>H}";

    lemma (in group_hom) subgroup_kernel: "subgroup (kernel G H h) G"
    apply (rule subgroup.intro)
    apply (auto simp add: kernel_def group.intro prems)
    done

    text{*The kernel of a homomorphism is a normal subgroup*}
    lemma (in group_hom) normal_kernel: "(kernel G H h) \<lhd> G"
    apply (simp add: group.normal_inv_iff subgroup_kernel group.intro prems)
    apply (simp add: kernel_def)
    done

    lemma (in group_hom) FactGroup_nonempty:
      assumes X: "X ∈ carrier (G Mod kernel G H h)"
      shows "X ≠ {}"
    proof -
      from X
      obtain g where "g ∈ carrier G"
                 and "X = kernel G H h #> g"
        by (auto simp add: FactGroup_def RCOSETS_def)
      thus ?thesis
       by (auto simp add: kernel_def r_coset_def image_def intro: hom_one)
    qed

    lemma (in group_hom) FactGroup_contents_mem:
      assumes X: "X ∈ carrier (G Mod (kernel G H h))"
      shows "contents (h`X) ∈ carrier H"
    proof -
      from X
      obtain g where g: "g ∈ carrier G"
                 and "X = kernel G H h #> g"
        by (auto simp add: FactGroup_def RCOSETS_def)
      hence "h ` X = {h g}" by (auto simp add: kernel_def r_coset_def image_def g)
      thus ?thesis by (auto simp add: g)
    qed

    lemma (in group_hom) FactGroup_hom:
         "(λX. contents (h`X)) ∈ hom (G Mod (kernel G H h)) H"
    apply (simp add: hom_def FactGroup_contents_mem  normal.factorgroup_is_group [OF normal_kernel] group.axioms monoid.m_closed)
    proof (simp add: hom_def funcsetI FactGroup_contents_mem, intro ballI)
      fix X and X'
      assume X:  "X  ∈ carrier (G Mod kernel G H h)"
         and X': "X' ∈ carrier (G Mod kernel G H h)"
      then
      obtain g and g'
               where "g ∈ carrier G" and "g' ∈ carrier G"
                 and "X = kernel G H h #> g" and "X' = kernel G H h #> g'"
        by (auto simp add: FactGroup_def RCOSETS_def)
      hence all: "∀x∈X. h x = h g" "∀x∈X'. h x = h g'"
        and Xsub: "X ⊆ carrier G" and X'sub: "X' ⊆ carrier G"
        by (force simp add: kernel_def r_coset_def image_def)+
      hence "h ` (X <#> X') = {h g ⊗H h g'}" using X X'
        by (auto dest!: FactGroup_nonempty
                 simp add: set_mult_def image_eq_UN
                           subsetD [OF Xsub] subsetD [OF X'sub])
      thus "contents (h ` (X <#> X')) = contents (h ` X) ⊗H contents (h ` X')"
        by (simp add: all image_eq_UN FactGroup_nonempty X X')
    qed

    text{*Lemma for the following injectivity result*}
    lemma (in group_hom) FactGroup_subset:
         "[|g ∈ carrier G; g' ∈ carrier G; h g = h g'|]
          ==>  kernel G H h #> g ⊆ kernel G H h #> g'"
    apply (clarsimp simp add: kernel_def r_coset_def image_def);
    apply (rename_tac y)
    apply (rule_tac x="y ⊗ g ⊗ inv g'" in exI)
    apply (simp add: G.m_assoc);
    done

    lemma (in group_hom) FactGroup_inj_on:
         "inj_on (λX. contents (h ` X)) (carrier (G Mod kernel G H h))"
    proof (simp add: inj_on_def, clarify)
      fix X and X'
      assume X:  "X  ∈ carrier (G Mod kernel G H h)"
         and X': "X' ∈ carrier (G Mod kernel G H h)"
      then
      obtain g and g'
               where gX: "g ∈ carrier G"  "g' ∈ carrier G"
                  "X = kernel G H h #> g" "X' = kernel G H h #> g'"
        by (auto simp add: FactGroup_def RCOSETS_def)
      hence all: "∀x∈X. h x = h g" "∀x∈X'. h x = h g'"
        by (force simp add: kernel_def r_coset_def image_def)+
      assume "contents (h ` X) = contents (h ` X')"
      hence h: "h g = h g'"
        by (simp add: image_eq_UN all FactGroup_nonempty X X')
      show "X=X'" by (rule equalityI) (simp_all add: FactGroup_subset h gX)
    qed

    text{*If the homomorphism @{term h} is onto @{term H}, then so is the
    homomorphism from the quotient group*}
    lemma (in group_hom) FactGroup_onto:
      assumes h: "h ` carrier G = carrier H"
      shows "(λX. contents (h ` X)) ` carrier (G Mod kernel G H h) = carrier H"
    proof
      show "(λX. contents (h ` X)) ` carrier (G Mod kernel G H h) ⊆ carrier H"
        by (auto simp add: FactGroup_contents_mem)
      show "carrier H ⊆ (λX. contents (h ` X)) ` carrier (G Mod kernel G H h)"
      proof
        fix y
        assume y: "y ∈ carrier H"
        with h obtain g where g: "g ∈ carrier G" "h g = y"
          by (blast elim: equalityE);
        hence "(\<Union>x∈kernel G H h #> g. {h x}) = {y}"
          by (auto simp add: y kernel_def r_coset_def)
        with g show "y ∈ (λX. contents (h ` X)) ` carrier (G Mod kernel G H h)"
          by (auto intro!: bexI simp add: FactGroup_def RCOSETS_def image_eq_UN)
      qed
    qed

    text{*If @{term h} is a homomorphism from @{term G} onto @{term H}, then the
     quotient group @{term "G Mod (kernel G H h)"} is isomorphic to @{term H}.*}
    theorem (in group_hom) FactGroup_iso:
      "h ` carrier G = carrier H
       ==> (λX. contents (h`X)) ∈ (G Mod (kernel G H h)) ≅ H"
    by (simp add: iso_def FactGroup_hom FactGroup_inj_on bij_betw_def
                  FactGroup_onto)

    end

### Basic Properties of Cosets

lemma coset_mult_assoc:

      [| group G; M ⊆ carrier G; g ∈ carrier G; h ∈ carrier G |]
      ==> M #>G g #>G h = M #>G g ⊗G h

lemma coset_mult_one:

      [| group G; M ⊆ carrier G |] ==> M #>G \<one>G = M

lemma coset_mult_inv1:

      [| group G; M #>G x ⊗G invG y = M; x ∈ carrier G; y ∈ carrier G;
         M ⊆ carrier G |]
      ==> M #>G x = M #>G y

lemma coset_mult_inv2:

      [| group G; M #>G x = M #>G y; x ∈ carrier G; y ∈ carrier G; M ⊆ carrier G |]
      ==> M #>G x ⊗G invG y = M

lemma coset_join1:

      [| group G; H #>G x = H; x ∈ carrier G; subgroup H G |] ==> x ∈ H

lemma solve_equation:

      [| group G; subgroup H G; x ∈ H; y ∈ H |] ==> ∃h∈H. y = h ⊗G x

lemma repr_independence:

      [| group G; y ∈ H #>G x; x ∈ carrier G; subgroup H G |] ==> H #>G x = H #>G y

lemma coset_join2:

      [| group G; x ∈ carrier G; subgroup H G; x ∈ H |] ==> H #>G x = H

lemma r_coset_subset_G:

      [| group G; H ⊆ carrier G; x ∈ carrier G |] ==> H #>G x ⊆ carrier G

lemma rcosI:

      [| group G; h ∈ H; H ⊆ carrier G; x ∈ carrier G |] ==> h ⊗G x ∈ H #>G x

lemma rcosetsI:

      [| group G; H ⊆ carrier G; x ∈ carrier G |] ==> H #>G x ∈ rcosetsG H

lemma transpose_inv:

      [| group G; x ⊗G y = z; x ∈ carrier G; y ∈ carrier G; z ∈ carrier G |]
      ==> invG x ⊗G z = y

lemma rcos_self:

      [| group G; x ∈ carrier G; subgroup H G |] ==> x ∈ H #>G x

### Normal subgroups

lemma normal_imp_subgroup:

      H \<lhd> G ==> subgroup H G

lemma normalI:

      [| group G; subgroup H G; ∀x∈carrier G. H #>G x = x <#G H |] ==> H \<lhd> G

lemma inv_op_closed1:

      [| H \<lhd> G; x ∈ carrier G; h ∈ H |] ==> invG x ⊗G h ⊗G x ∈ H

lemma inv_op_closed2:

      [| H \<lhd> G; x ∈ carrier G; h ∈ H |] ==> x ⊗G h ⊗G invG x ∈ H

lemma normal_inv_iff:

      group G
      ==> N \<lhd> G = (subgroup N G ∧ (∀x∈carrier G. ∀h∈N. x ⊗G h ⊗G invG x ∈ N))

### More Properties of Cosets

lemma lcos_m_assoc:

      [| group G; M ⊆ carrier G; g ∈ carrier G; h ∈ carrier G |]
      ==> g <#G (h <#G M) = g ⊗G h <#G M

lemma lcos_mult_one:

      [| group G; M ⊆ carrier G |] ==> \<one>G <#G M = M

lemma l_coset_subset_G:

      [| group G; H ⊆ carrier G; x ∈ carrier G |] ==> x <#G H ⊆ carrier G

lemma l_coset_swap:

      [| group G; y ∈ x <#G H; x ∈ carrier G; subgroup H G |] ==> x ∈ y <#G H

lemma l_coset_carrier:

      [| group G; y ∈ x <#G H; x ∈ carrier G; subgroup H G |] ==> y ∈ carrier G

lemma l_repr_imp_subset:

      [| group G; y ∈ x <#G H; x ∈ carrier G; subgroup H G |] ==> y <#G H ⊆ x <#G H

lemma l_repr_independence:

      [| group G; y ∈ x <#G H; x ∈ carrier G; subgroup H G |] ==> x <#G H = y <#G H

lemma setmult_subset_G:

      [| group G; H ⊆ carrier G; K ⊆ carrier G |] ==> H <#>G K ⊆ carrier G

lemma subgroup_mult_id:

      [| group G; subgroup H G |] ==> H <#>G H = H

#### Set of inverses of an @{text r_coset}.

lemma rcos_inv:

      [| H \<lhd> G; x ∈ carrier G |] ==> set_invG (H #>G x) = H #>G invG x

#### Theorems for @{text "<#>"} with @{text "#>"} or @{text "<#"}.

lemma setmult_rcos_assoc:

      [| group G; H ⊆ carrier G; K ⊆ carrier G; x ∈ carrier G |]
      ==> H <#>G (K #>G x) = H <#>G K #>G x

lemma rcos_assoc_lcos:

      [| group G; H ⊆ carrier G; K ⊆ carrier G; x ∈ carrier G |]
      ==> H #>G x <#>G K = H <#>G (x <#G K)

lemma rcos_mult_step1:

      [| H \<lhd> G; x ∈ carrier G; y ∈ carrier G |]
      ==> H #>G x <#>G (H #>G y) = H <#>G (x <#G H) #>G y

lemma rcos_mult_step2:

      [| H \<lhd> G; x ∈ carrier G; y ∈ carrier G |]
      ==> H <#>G (x <#G H) #>G y = H <#>G (H #>G x) #>G y

lemma rcos_mult_step3:

      [| H \<lhd> G; x ∈ carrier G; y ∈ carrier G |]
      ==> H <#>G (H #>G x) #>G y = H #>G x ⊗G y

lemma rcos_sum:

      [| H \<lhd> G; x ∈ carrier G; y ∈ carrier G |]
      ==> H #>G x <#>G (H #>G y) = H #>G x ⊗G y

lemma rcosets_mult_eq:

      [| H \<lhd> G; M ∈ rcosetsG H |] ==> H <#>G M = M

#### An Equivalence Relation

lemma equiv_rcong:

      [| subgroup H G; group G |] ==> equiv (carrier G) rcongG H

lemma l_coset_eq_rcong:

      [| subgroup H G; group G; a ∈ carrier G |] ==> a <#G H = rcongG H `` {a}

#### Two distinct right cosets are disjoint

lemma rcos_equation:

      [| group G; subgroup H G; ha ⊗G a = h ⊗G b; a ∈ carrier G; b ∈ carrier G; h ∈ H;
         ha ∈ H; hb ∈ H |]
      ==> hb ⊗G a ∈ (UN h:H. {h ⊗G b})

lemma rcos_disjoint:

      [| group G; subgroup H G; a ∈ rcosetsG H; b ∈ rcosetsG H; a ≠ b |]
      ==> a ∩ b = {}

### Order of a Group and Lagrange's Theorem

lemma rcos_self:

      [| group G; subgroup H G; x ∈ carrier G |] ==> x ∈ H #>G x

lemma rcosets_part_G:

      [| group G; subgroup H G |] ==> Union (rcosetsG H) = carrier G

lemma cosets_finite:

      [| group G; c ∈ rcosetsG H; H ⊆ carrier G; finite (carrier G) |] ==> finite c

lemma inj_on_f:

      [| group G; H ⊆ carrier G; a ∈ carrier G |]
      ==> inj_on (%y. y ⊗G invG a) (H #>G a)

lemma inj_on_g:

      [| group G; H ⊆ carrier G; a ∈ carrier G |] ==> inj_on (%y. y ⊗G a) H

lemma card_cosets_equal:

      [| group G; c ∈ rcosetsG H; H ⊆ carrier G; finite (carrier G) |]
      ==> card c = card H

lemma rcosets_subset_PowG:

      [| group G; subgroup H G |] ==> rcosetsG H ⊆ Pow (carrier G)

theorem lagrange:

      [| group G; finite (carrier G); subgroup H G |]
      ==> card (rcosetsG H) * card H = order G

### Quotient Groups: Factorization of a Group

lemma setmult_closed:

      [| H \<lhd> G; K1.0 ∈ rcosetsG H; K2.0 ∈ rcosetsG H |]
      ==> K1.0 <#>G K2.0 ∈ rcosetsG H

lemma setinv_closed:

      [| H \<lhd> G; K ∈ rcosetsG H |] ==> set_invG K ∈ rcosetsG H

lemma rcosets_assoc:

      [| H \<lhd> G; M1.0 ∈ rcosetsG H; M2.0 ∈ rcosetsG H; M3.0 ∈ rcosetsG H |]
      ==> M1.0 <#>G M2.0 <#>G M3.0 = M1.0 <#>G (M2.0 <#>G M3.0)

lemma subgroup_in_rcosets:

      [| subgroup H G; group G |] ==> H ∈ rcosetsG H

lemma rcosets_inv_mult_group_eq:

      [| H \<lhd> G; M ∈ rcosetsG H |] ==> set_invG M <#>G M = H

theorem factorgroup_is_group:

      H \<lhd> G ==> group (G Mod H)

lemma mult_FactGroup:

      X ⊗G Mod H X' = X <#>G X'

lemma inv_FactGroup:

      [| H \<lhd> G; X ∈ carrier (G Mod H) |] ==> invG Mod H X = set_invG X

lemma r_coset_hom_Mod:

      H \<lhd> G ==> op #>G H ∈ hom G (G Mod H)

### The First Isomorphism Theorem

lemma subgroup_kernel:

      group_hom G H h ==> subgroup (kernel G H h) G

lemma normal_kernel:

      group_hom G H h ==> kernel G H h \<lhd> G

lemma FactGroup_nonempty:

      [| group_hom G H h; X ∈ carrier (G Mod kernel G H h) |] ==> X ≠ {}

lemma FactGroup_contents_mem:

      [| group_hom G H h; X ∈ carrier (G Mod kernel G H h) |]
      ==> contents (h ` X) ∈ carrier H

lemma FactGroup_hom:

      group_hom G H h ==> (%X. contents (h ` X)) ∈ hom (G Mod kernel G H h) H

lemma FactGroup_subset:

      [| group_hom G H h; g ∈ carrier G; g' ∈ carrier G; h g = h g' |]
      ==> kernel G H h #>G g ⊆ kernel G H h #>G g'

lemma FactGroup_inj_on:

      group_hom G H h ==> inj_on (%X. contents (h ` X)) (carrier (G Mod kernel G H h))

lemma FactGroup_onto:

      [| group_hom G H h; h ` carrier G = carrier H |]
      ==> (%X. contents (h ` X)) ` carrier (G Mod kernel G H h) = carrier H

theorem FactGroup_iso:

      [| group_hom G H h; h ` carrier G = carrier H |]
      ==> (%X. contents (h ` X)) ∈ G Mod kernel G H h ≅ H