src/ZF/ex/Group.thy

 
 
 subsection {* Monoids *}
 
 (*First, we must simulate a record declaration:
-record monoid = 
+record monoid =
   carrier :: i
   mult :: "[i,i] => i" (infixl "\<cdot>\<index>" 70)
   one :: i ("\<one>\<index>")
 *)
 

 
 locale monoid = fixes G (structure)
   assumes m_closed [intro, simp]:
          "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk> \<Longrightarrow> x \<cdot> y \<in> carrier(G)"
       and m_assoc:
-         "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk> 
+         "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk>
           \<Longrightarrow> (x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
       and one_closed [intro, simp]: "\<one> \<in> carrier(G)"
       and l_one [simp]: "x \<in> carrier(G) \<Longrightarrow> \<one> \<cdot> x = x"
       and r_one [simp]: "x \<in> carrier(G) \<Longrightarrow> x \<cdot> \<one> = x"
 

 
 lemma update_carrier_eq [simp]: "update_carrier(<A,Z>,B) = <B,Z>"
   by (simp add: update_carrier_def)
 
 lemma carrier_update_carrier [simp]: "carrier(update_carrier(M,B)) = B"
-  by (simp add: update_carrier_def) 
+  by (simp add: update_carrier_def)
 
 lemma mult_update_carrier [simp]: "mmult(update_carrier(M,B),x,y) = mmult(M,x,y)"
-  by (simp add: update_carrier_def mmult_def) 
+  by (simp add: update_carrier_def mmult_def)
 
 lemma one_update_carrier [simp]: "one(update_carrier(M,B)) = one(M)"
-  by (simp add: update_carrier_def one_def) 
+  by (simp add: update_carrier_def one_def)
 
 
 lemma (in monoid) inv_unique:
   assumes eq: "y \<cdot> x = \<one>"  "x \<cdot> y' = \<one>"
     and G: "x \<in> carrier(G)"  "y \<in> carrier(G)"  "y' \<in> carrier(G)"

     "\<And>x y z. \<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk> \<Longrightarrow>
     (x \<cdot> y = x \<cdot> z) \<longleftrightarrow> (y = z)"
   proof
     fix x y z
     assume G: "x \<in> carrier(G)"  "y \<in> carrier(G)"  "z \<in> carrier(G)"
-    { 
+    {
       assume eq: "x \<cdot> y = x \<cdot> z"
       with G l_inv_ex obtain x_inv where xG: "x_inv \<in> carrier(G)"
         and l_inv: "x_inv \<cdot> x = \<one>" by fast
       from G eq xG have "(x_inv \<cdot> x) \<cdot> y = (x_inv \<cdot> x) \<cdot> z"
         by (simp add: m_assoc)

       by simp
     from x y show "\<exists>y \<in> carrier(G). y \<cdot> x = \<one> & x \<cdot> y = \<one>"
       by (fast intro: l_inv r_inv)
   qed
   show ?thesis
-    by (blast intro: group.intro monoid.intro group_axioms.intro 
+    by (blast intro: group.intro monoid.intro group_axioms.intro
                      assms r_one inv_ex)
 qed
 
 lemma (in group) inv [simp]:
   "x \<in> carrier(G) \<Longrightarrow> inv x \<in> carrier(G) & inv x \<cdot> x = \<one> & x \<cdot> inv x = \<one>"
-  apply (frule inv_ex) 
+  apply (frule inv_ex)
   apply (unfold Bex_def m_inv_def)
-  apply (erule exE) 
+  apply (erule exE)
   apply (rule theI)
   apply (rule ex1I, assumption)
    apply (blast intro: inv_unique)
   done
 

 apply (rule r_cancel [THEN iffD1], auto)
 done
 
 lemma (in group) inv_one [simp]:
   "inv \<one> = \<one>"
-  by (auto intro: inv_equality) 
+  by (auto intro: inv_equality)
 
 lemma (in group) inv_inv [simp]: "x \<in> carrier(G) \<Longrightarrow> inv (inv x) = x"
-  by (auto intro: inv_equality) 
+  by (auto intro: inv_equality)
 
 text{*This proof is by cancellation*}
 lemma (in group) inv_mult_group:
   "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk> \<Longrightarrow> inv (x \<cdot> y) = inv y \<cdot> inv x"
 proof -

   "\<lbrakk>h \<in> hom(G,H); x \<in> carrier(G)\<rbrakk> \<Longrightarrow> h ` x \<in> carrier(H)"
   by (auto simp add: hom_def)
 
 lemma (in group) hom_compose:
      "\<lbrakk>h \<in> hom(G,H); i \<in> hom(H,I)\<rbrakk> \<Longrightarrow> i O h \<in> hom(G,I)"
-by (force simp add: hom_def comp_fun) 
+by (force simp add: hom_def comp_fun)
 
 lemma hom_is_fun:
   "h \<in> hom(G,H) \<Longrightarrow> h \<in> carrier(G) -> carrier(H)"
   by (simp add: hom_def)
 

 definition
   iso :: "[i,i] => i"  (infixr "\<cong>" 60) where
   "G \<cong> H == hom(G,H) \<inter> bij(carrier(G), carrier(H))"
 
 lemma (in group) iso_refl: "id(carrier(G)) \<in> G \<cong> G"
-  by (simp add: iso_def hom_def id_type id_bij) 
+  by (simp add: iso_def hom_def id_type id_bij)
 
 
 lemma (in group) iso_sym:
      "h \<in> G \<cong> H \<Longrightarrow> converse(h) \<in> H \<cong> G"
-apply (simp add: iso_def bij_converse_bij, clarify) 
-apply (subgoal_tac "converse(h) \<in> carrier(H) \<rightarrow> carrier(G)") 
- prefer 2 apply (simp add: bij_converse_bij bij_is_fun) 
-apply (auto intro: left_inverse_eq [of _ "carrier(G)" "carrier(H)"] 
-            simp add: hom_def bij_is_inj right_inverse_bij); 
-done
-
-lemma (in group) iso_trans: 
+apply (simp add: iso_def bij_converse_bij, clarify)
+apply (subgoal_tac "converse(h) \<in> carrier(H) \<rightarrow> carrier(G)")
+ prefer 2 apply (simp add: bij_converse_bij bij_is_fun)
+apply (auto intro: left_inverse_eq [of _ "carrier(G)" "carrier(H)"]
+            simp add: hom_def bij_is_inj right_inverse_bij);
+done
+
+lemma (in group) iso_trans:
      "\<lbrakk>h \<in> G \<cong> H; i \<in> H \<cong> I\<rbrakk> \<Longrightarrow> i O h \<in> G \<cong> I"
   by (auto simp add: iso_def hom_compose comp_bij)
 
 lemma DirProdGroup_commute_iso:
   assumes "group(G)" and "group(H)"

 proof -
   interpret group G by fact
   interpret group H by fact
   interpret group I by fact
   show ?thesis
-    by (auto intro: lam_type simp add: iso_def hom_def inj_def surj_def bij_def) 
+    by (auto intro: lam_type simp add: iso_def hom_def inj_def surj_def bij_def)
 qed
 
 text{*Basis for homomorphism proofs: we assume two groups @{term G} and
   @{term H}, with a homomorphism @{term h} between them*}
 locale group_hom = G: group G + H: group H

   "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk> \<Longrightarrow> inv (x \<cdot> y) = inv x \<cdot> inv y"
   by (simp add: m_ac inv_mult_group)
 
 
 lemma (in group) subgroup_self: "subgroup (carrier(G),G)"
-by (simp add: subgroup_def) 
+by (simp add: subgroup_def)
 
 lemma (in group) subgroup_imp_group:
   "subgroup(H,G) \<Longrightarrow> group (update_carrier(G,H))"
 by (simp add: subgroup.is_group)
 

 
 subsection {*Bijections Form a Group *}
 
 theorem group_BijGroup: "group(BijGroup(S))"
 apply (simp add: BijGroup_def)
-apply (rule groupI) 
-    apply (simp_all add: id_bij comp_bij comp_assoc) 
+apply (rule groupI)
+    apply (simp_all add: id_bij comp_bij comp_assoc)
  apply (simp add: id_bij bij_is_fun left_comp_id [of _ S S] fun_is_rel)
 apply (blast intro: left_comp_inverse bij_is_inj bij_converse_bij)
 done
 
 
 subsection{*Automorphisms Form a Group*}
 
-lemma Bij_Inv_mem: "\<lbrakk>f \<in> bij(S,S);  x \<in> S\<rbrakk> \<Longrightarrow> converse(f) ` x \<in> S" 
+lemma Bij_Inv_mem: "\<lbrakk>f \<in> bij(S,S);  x \<in> S\<rbrakk> \<Longrightarrow> converse(f) ` x \<in> S"
 by (blast intro: apply_funtype bij_is_fun bij_converse_bij)
 
 lemma inv_BijGroup: "f \<in> bij(S,S) \<Longrightarrow> m_inv (BijGroup(S), f) = converse(f)"
 apply (rule group.inv_equality)
 apply (rule group_BijGroup)
-apply (simp_all add: BijGroup_def bij_converse_bij 
-          left_comp_inverse [OF bij_is_inj]) 
+apply (simp_all add: BijGroup_def bij_converse_bij
+          left_comp_inverse [OF bij_is_inj])
 done
 
 lemma iso_is_bij: "h \<in> G \<cong> H ==> h \<in> bij(carrier(G), carrier(H))"
 by (simp add: iso_def)
 

 proof (rule subgroup.intro)
   show "auto(G) \<subseteq> carrier (BijGroup (carrier(G)))"
     by (auto simp add: auto_def BijGroup_def iso_def)
 next
   fix x y
-  assume "x \<in> auto(G)" "y \<in> auto(G)" 
+  assume "x \<in> auto(G)" "y \<in> auto(G)"
   thus "x \<cdot>\<^bsub>BijGroup (carrier(G))\<^esub> y \<in> auto(G)"
-    by (auto simp add: BijGroup_def auto_def iso_def bij_is_fun 
+    by (auto simp add: BijGroup_def auto_def iso_def bij_is_fun
                        group.hom_compose comp_bij)
 next
   show "\<one>\<^bsub>BijGroup (carrier(G))\<^esub> \<in> auto(G)" by (simp add:  BijGroup_def id_in_auto)
 next
-  fix x 
-  assume "x \<in> auto(G)" 
+  fix x
+  assume "x \<in> auto(G)"
   thus "inv\<^bsub>BijGroup (carrier(G))\<^esub> x \<in> auto(G)"
-    by (simp add: auto_def inv_BijGroup iso_is_bij iso_sym) 
+    by (simp add: auto_def inv_BijGroup iso_is_bij iso_sym)
 qed
 
 theorem (in group) AutoGroup: "group (AutoGroup(G))"
 by (simp add: AutoGroup_def subgroup.is_group subgroup_auto group_BijGroup)
 

 subsection {* Normal subgroups *}
 
 lemma normal_imp_subgroup: "H \<lhd> G ==> subgroup(H,G)"
   by (simp add: normal_def subgroup_def)
 
-lemma (in group) normalI: 
+lemma (in group) normalI:
   "subgroup(H,G) \<Longrightarrow> (\<forall>x \<in> carrier(G). H #> x = x <# H) \<Longrightarrow> H \<lhd> G";
   by (simp add: normal_def normal_axioms_def)
 
 lemma (in normal) inv_op_closed1:
      "\<lbrakk>x \<in> carrier(G); h \<in> H\<rbrakk> \<Longrightarrow> (inv x) \<cdot> h \<cdot> x \<in> H"
-apply (insert coset_eq) 
+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:
      "\<lbrakk>x \<in> carrier(G); h \<in> H\<rbrakk> \<Longrightarrow> x \<cdot> h \<cdot> (inv x) \<in> H"
-apply (subgoal_tac "inv (inv x) \<cdot> h \<cdot> (inv x) \<in> H") 
-apply simp 
-apply (blast intro: inv_op_closed1) 
+apply (subgoal_tac "inv (inv x) \<cdot> h \<cdot> (inv x) \<in> H")
+apply simp
+apply (blast intro: inv_op_closed1)
 done
 
 text{*Alternative characterization of normal subgroups*}
 lemma (in group) normal_inv_iff:
      "(N \<lhd> G) \<longleftrightarrow>
       (subgroup(N,G) & (\<forall>x \<in> carrier(G). \<forall>h \<in> N. x \<cdot> h \<cdot> (inv x) \<in> N))"
       (is "_ \<longleftrightarrow> ?rhs")
 proof
   assume N: "N \<lhd> G"
   show ?rhs
-    by (blast intro: N normal.inv_op_closed2 normal_imp_subgroup) 
+    by (blast intro: N normal.inv_op_closed2 normal_imp_subgroup)
 next
   assume ?rhs
-  hence sg: "subgroup(N,G)" 
+  hence sg: "subgroup(N,G)"
     and closed: "\<And>x. x\<in>carrier(G) \<Longrightarrow> \<forall>h\<in>N. x \<cdot> h \<cdot> inv x \<in> N" by auto
-  hence sb: "N \<subseteq> carrier(G)" by (simp add: subgroup.subset) 
+  hence sb: "N \<subseteq> 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 \<in> carrier(G)"
     show "(\<Union>h\<in>N. {h \<cdot> x}) = (\<Union>h\<in>N. {x \<cdot> h})"
     proof
       show "(\<Union>h\<in>N. {h \<cdot> x}) \<subseteq> (\<Union>h\<in>N. {x \<cdot> h})"
       proof clarify
         fix n
-        assume n: "n \<in> N" 
+        assume n: "n \<in> N"
         show "n \<cdot> x \<in> (\<Union>h\<in>N. {x \<cdot> h})"
-        proof (rule UN_I) 
+        proof (rule UN_I)
           from closed [of "inv x"]
           show "inv x \<cdot> n \<cdot> x \<in> N" by (simp add: x n)
           show "n \<cdot> x \<in> {x \<cdot> (inv x \<cdot> n \<cdot> x)}"
             by (simp add: x n m_assoc [symmetric] sb [THEN subsetD])
         qed
       qed
     next
       show "(\<Union>h\<in>N. {x \<cdot> h}) \<subseteq> (\<Union>h\<in>N. {h \<cdot> x})"
       proof clarify
         fix n
-        assume n: "n \<in> N" 
+        assume n: "n \<in> N"
         show "x \<cdot> n \<in> (\<Union>h\<in>N. {h \<cdot> x})"
-        proof (rule UN_I) 
+        proof (rule UN_I)
           show "x \<cdot> n \<cdot> inv x \<in> N" by (simp add: x n closed)
           show "x \<cdot> n \<in> {x \<cdot> n \<cdot> inv x \<cdot> x}"
             by (simp add: x n m_assoc sb [THEN subsetD])
         qed
       qed

 lemma (in group) setmult_subset_G:
      "\<lbrakk>H \<subseteq> carrier(G); K \<subseteq> carrier(G)\<rbrakk> \<Longrightarrow> H <#> K \<subseteq> carrier(G)"
 by (auto simp add: set_mult_def subsetD)
 
 lemma (in group) subgroup_mult_id: "subgroup(H,G) \<Longrightarrow> H <#> H = H"
-apply (rule equalityI) 
+apply (rule equalityI)
 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.one_closed subgroup.subset [THEN subsetD])
 done

    shows "equiv (carrier(G), rcong H)"
 proof -
   interpret group G by fact
   show ?thesis proof (simp add: equiv_def, intro conjI)
     show "rcong H \<subseteq> carrier(G) \<times> carrier(G)"
-      by (auto simp add: r_congruent_def) 
+      by (auto simp add: r_congruent_def)
   next
     show "refl (carrier(G), rcong H)"
-      by (auto simp add: r_congruent_def refl_def) 
+      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 \<in> carrier(G)" "y \<in> carrier(G)" 
+      assume [simp]: "x \<in> carrier(G)" "y \<in> carrier(G)"
         and "inv x \<cdot> y \<in> H"
       hence "inv (inv x \<cdot> y) \<in> H" by simp
       thus "inv y \<cdot> x \<in> H" by (simp add: inv_mult_group)
     qed
   next

     proof (simp add: r_congruent_def trans_def, clarify)
       fix x y z
       assume [simp]: "x \<in> carrier(G)" "y \<in> carrier(G)" "z \<in> carrier(G)"
         and "inv x \<cdot> y \<in> H" and "inv y \<cdot> z \<in> H"
       hence "(inv x \<cdot> y) \<cdot> (inv y \<cdot> z) \<in> H" by simp
-      hence "inv x \<cdot> (y \<cdot> inv y) \<cdot> z \<in> H" by (simp add: m_assoc del: inv) 
+      hence "inv x \<cdot> (y \<cdot> inv y) \<cdot> z \<in> H" by (simp add: m_assoc del: inv)
       thus "inv x \<cdot> z \<in> H" by simp
     qed
   qed
 qed
 

   Was there a mistake in the definitions? I'd have expected them to
   correspond to right cosets.*}
 lemma (in subgroup) l_coset_eq_rcong:
   assumes "group(G)"
   assumes a: "a \<in> carrier(G)"
-  shows "a <# H = (rcong H) `` {a}" 
+  shows "a <# H = (rcong H) `` {a}"
 proof -
   interpret group G by fact
   show ?thesis
     by (force simp add: r_congruent_def l_coset_def m_assoc [symmetric] a
-      Collect_image_eq) 
+      Collect_image_eq)
 qed
 
 lemma (in group) rcos_equation:
   assumes "subgroup(H, G)"
   shows
-     "\<lbrakk>ha \<cdot> a = h \<cdot> b; a \<in> carrier(G);  b \<in> carrier(G);  
+     "\<lbrakk>ha \<cdot> a = h \<cdot> b; a \<in> carrier(G);  b \<in> carrier(G);
         h \<in> H;  ha \<in> H;  hb \<in> H\<rbrakk>
       \<Longrightarrow> hb \<cdot> a \<in> (\<Union>h\<in>H. {h \<cdot> b})" (is "PROP ?P")
 proof -
   interpret subgroup H G by fact
   show "PROP ?P"

   fix a
   assume a: "a \<in> carrier(G)"
   show "|H #> a| = |H|"
   proof (rule eqpollI [THEN cardinal_cong])
     show "H #> a \<lesssim> H"
-    proof (simp add: lepoll_def, intro exI) 
+    proof (simp add: lepoll_def, intro exI)
       show "(\<lambda>y \<in> H#>a. y \<cdot> inv a) \<in> inj(H #> a, H)"
-        by (auto intro: lam_type 
+        by (auto intro: lam_type
                  simp add: inj_def r_coset_def m_assoc subsetD [OF H] a)
     qed
     show "H \<lesssim> H #> a"
-    proof (simp add: lepoll_def, intro exI) 
+    proof (simp add: lepoll_def, intro exI)
       show "(\<lambda>y\<in> H. y \<cdot> a) \<in> inj(H, H #> a)"
-        by (auto intro: lam_type 
+        by (auto intro: lam_type
                  simp add: inj_def r_coset_def  subsetD [OF H] a)
     qed
   qed
 qed
 

 subsection {*Quotient Groups: Factorization of a Group*}
 
 definition
   FactGroup :: "[i,i] => i" (infixl "Mod" 65) where
     --{*Actually defined for groups rather than monoids*}
-  "G Mod H == 
+  "G Mod H ==
      <rcosets\<^bsub>G\<^esub> H, \<lambda><K1,K2> \<in> (rcosets\<^bsub>G\<^esub> H) \<times> (rcosets\<^bsub>G\<^esub> H). K1 <#>\<^bsub>G\<^esub> K2, H, 0>"
 
 lemma (in normal) setmult_closed:
      "\<lbrakk>K1 \<in> rcosets H; K2 \<in> rcosets H\<rbrakk> \<Longrightarrow> K1 <#> K2 \<in> rcosets H"
 by (auto simp add: rcos_sum RCOSETS_def)

 apply (auto dest: rcosets_inv_mult_group_eq simp add: setinv_closed)
 done
 
 lemma (in normal) inv_FactGroup:
      "X \<in> carrier (G Mod H) \<Longrightarrow> inv\<^bsub>G Mod H\<^esub> X = set_inv X"
-apply (rule group.inv_equality [OF factorgroup_is_group]) 
+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:
   "(\<lambda>a \<in> carrier(G). H #> a) \<in> hom(G, G Mod H)"
-by (auto simp add: FactGroup_def RCOSETS_def hom_def rcos_sum intro: lam_type) 
+by (auto simp add: FactGroup_def RCOSETS_def hom_def rcos_sum intro: lam_type)
 
 
 subsection{*The First Isomorphism Theorem*}
 
-text{*The quotient by the kernel of a homomorphism is isomorphic to the 
+text{*The quotient by the kernel of a homomorphism is isomorphic to the
   range of that homomorphism.*}
 
 definition
   kernel :: "[i,i,i] => i" where
     --{*the kernel of a homomorphism*}
   "kernel(G,H,h) == {x \<in> carrier(G). h ` x = \<one>\<^bsub>H\<^esub>}";
 
 lemma (in group_hom) subgroup_kernel: "subgroup (kernel(G,H,h), G)"
-apply (rule subgroup.intro) 
+apply (rule subgroup.intro)
 apply (auto simp add: kernel_def group.intro)
 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)
-apply (simp add: kernel_def)  
+apply (simp add: kernel_def)
 done
 
 lemma (in group_hom) FactGroup_nonempty:
   assumes X: "X \<in> carrier (G Mod kernel(G,H,h))"
   shows "X \<noteq> 0"
 proof -
   from X
-  obtain g where "g \<in> carrier(G)" 
+  obtain g where "g \<in> carrier(G)"
              and "X = kernel(G,H,h) #> g"
     by (auto simp add: FactGroup_def RCOSETS_def)
-  thus ?thesis 
+  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 \<in> carrier (G Mod (kernel(G,H,h)))"
   shows "contents (h``X) \<in> carrier(H)"
 proof -
   from X
-  obtain g where g: "g \<in> carrier(G)" 
+  obtain g where g: "g \<in> 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_UN 
+    by (auto simp add: kernel_def r_coset_def image_UN
                        image_eq_UN [OF hom_is_fun] g)
   thus ?thesis by (auto simp add: g)
 qed
 
 lemma mult_FactGroup:
-     "[|X \<in> carrier(G Mod H); X' \<in> carrier(G Mod H)|] 
+     "[|X \<in> carrier(G Mod H); X' \<in> carrier(G Mod H)|]
       ==> X \<cdot>\<^bsub>(G Mod H)\<^esub> X' = X <#>\<^bsub>G\<^esub> X'"
-by (simp add: FactGroup_def) 
+by (simp add: FactGroup_def)
 
 lemma (in normal) FactGroup_m_closed:
-     "[|X \<in> carrier(G Mod H); X' \<in> carrier(G Mod H)|] 
+     "[|X \<in> carrier(G Mod H); X' \<in> carrier(G Mod H)|]
       ==> X <#>\<^bsub>G\<^esub> X' \<in> carrier(G Mod H)"
-by (simp add: FactGroup_def setmult_closed) 
+by (simp add: FactGroup_def setmult_closed)
 
 lemma (in group_hom) FactGroup_hom:
      "(\<lambda>X \<in> carrier(G Mod (kernel(G,H,h))). contents (h``X))
-      \<in> hom (G Mod (kernel(G,H,h)), H)" 
-proof (simp add: hom_def FactGroup_contents_mem lam_type mult_FactGroup normal.FactGroup_m_closed [OF normal_kernel], intro ballI)  
+      \<in> hom (G Mod (kernel(G,H,h)), H)"
+proof (simp add: hom_def FactGroup_contents_mem lam_type mult_FactGroup normal.FactGroup_m_closed [OF normal_kernel], intro ballI)
   fix X and X'
   assume X:  "X  \<in> carrier (G Mod kernel(G,H,h))"
      and X': "X' \<in> carrier (G Mod kernel(G,H,h))"
   then
   obtain g and g'
-           where "g \<in> carrier(G)" and "g' \<in> carrier(G)" 
+           where "g \<in> carrier(G)" and "g' \<in> 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: "\<forall>x\<in>X. h ` x = h ` g" "\<forall>x\<in>X'. h ` x = h ` g'" 
+  hence all: "\<forall>x\<in>X. h ` x = h ` g" "\<forall>x\<in>X'. h ` x = h ` g'"
     and Xsub: "X \<subseteq> carrier(G)" and X'sub: "X' \<subseteq> carrier(G)"
     by (force simp add: kernel_def r_coset_def image_def)+
   hence "h `` (X <#> X') = {h ` g \<cdot>\<^bsub>H\<^esub> h ` g'}" using X X'
     by (auto dest!: FactGroup_nonempty
              simp add: set_mult_def image_eq_UN [OF hom_is_fun] image_UN
-                       subsetD [OF Xsub] subsetD [OF X'sub]) 
+                       subsetD [OF Xsub] subsetD [OF X'sub])
   thus "contents (h `` (X <#> X')) = contents (h `` X) \<cdot>\<^bsub>H\<^esub> contents (h `` X')"
-    by (simp add: all image_eq_UN [OF hom_is_fun] FactGroup_nonempty 
+    by (simp add: all image_eq_UN [OF hom_is_fun] FactGroup_nonempty
                   X X' Xsub X'sub)
 qed
 
 
 text{*Lemma for the following injectivity result*}
 lemma (in group_hom) FactGroup_subset:
      "\<lbrakk>g \<in> carrier(G); g' \<in> carrier(G); h ` g = h ` g'\<rbrakk>
       \<Longrightarrow>  kernel(G,H,h) #> g \<subseteq> 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 \<cdot> g \<cdot> inv g'" in bexI) 
-apply (simp_all add: G.m_assoc) 
+apply (rename_tac y)
+apply (rule_tac x="y \<cdot> g \<cdot> inv g'" in bexI)
+apply (simp_all add: G.m_assoc)
 done
 
 lemma (in group_hom) FactGroup_inj:
      "(\<lambda>X\<in>carrier (G Mod kernel(G,H,h)). contents (h `` X))
       \<in> inj(carrier (G Mod kernel(G,H,h)), carrier(H))"
-proof (simp add: inj_def FactGroup_contents_mem lam_type, clarify) 
+proof (simp add: inj_def FactGroup_contents_mem lam_type, clarify)
   fix X and X'
   assume X:  "X  \<in> carrier (G Mod kernel(G,H,h))"
      and X': "X' \<in> carrier (G Mod kernel(G,H,h))"
   then
   obtain g and g'
-           where gX: "g \<in> carrier(G)"  "g' \<in> carrier(G)" 
+           where gX: "g \<in> carrier(G)"  "g' \<in> carrier(G)"
               "X = kernel(G,H,h) #> g" "X' = kernel(G,H,h) #> g'"
     by (auto simp add: FactGroup_def RCOSETS_def)
   hence all: "\<forall>x\<in>X. h ` x = h ` g" "\<forall>x\<in>X'. h ` x = h ` g'"
     and Xsub: "X \<subseteq> carrier(G)" and X'sub: "X' \<subseteq> carrier(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: all image_eq_UN [OF hom_is_fun] FactGroup_nonempty 
+    by (simp add: all image_eq_UN [OF hom_is_fun] FactGroup_nonempty
                   X X' Xsub X'sub)
-  show "X=X'" by (rule equalityI) (simp_all add: FactGroup_subset h gX) 
+  show "X=X'" by (rule equalityI) (simp_all add: FactGroup_subset h gX)
 qed
 
 
 lemma (in group_hom) kernel_rcoset_subset:
   assumes g: "g \<in> carrier(G)"
   shows "kernel(G,H,h) #> g \<subseteq> carrier (G)"
-    by (auto simp add: g kernel_def r_coset_def) 
+    by (auto simp add: g kernel_def r_coset_def)
 
 
 
 text{*If the homomorphism @{term h} is onto @{term H}, then so is the
 homomorphism from the quotient group*}

          \<in> surj(carrier (G Mod kernel(G,H,h)), carrier(H))"
 proof (simp add: surj_def FactGroup_contents_mem lam_type, clarify)
   fix y
   assume y: "y \<in> carrier(H)"
   with h obtain g where g: "g \<in> carrier(G)" "h ` g = y"
-    by (auto simp add: surj_def) 
-  hence "(\<Union>x\<in>kernel(G,H,h) #> g. {h ` x}) = {y}" 
-    by (auto simp add: y kernel_def r_coset_def) 
+    by (auto simp add: surj_def)
+  hence "(\<Union>x\<in>kernel(G,H,h) #> g. {h ` x}) = {y}"
+    by (auto simp add: y kernel_def r_coset_def)
   with g show "\<exists>x\<in>carrier(G Mod kernel(G, H, h)). contents(h `` x) = y"
         --{*The witness is @{term "kernel(G,H,h) #> g"}*}
-    by (force simp add: FactGroup_def RCOSETS_def 
+    by (force simp add: FactGroup_def RCOSETS_def
            image_eq_UN [OF hom_is_fun] kernel_rcoset_subset)
 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 \<in> surj(carrier(G), carrier(H))
    \<Longrightarrow> (\<lambda>X\<in>carrier (G Mod kernel(G,H,h)). contents (h``X)) \<in> (G Mod (kernel(G,H,h))) \<cong> H"
 by (simp add: iso_def FactGroup_hom FactGroup_inj bij_def FactGroup_surj)
- 
+
 end