# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1677517799 0
# Node ID c2013f617a7081d1aa9f213a7fb0ebd9a925583c
# Parent  aac23f2e7f3c4207bf6d5810aa163a17f385867a
Importation of basic group theory results, due to Jakob von Raumer from his AFP entry Jordan-Hölder Theorem

diff -r aac23f2e7f3c -r c2013f617a70 src/HOL/Algebra/Algebra.thy
--- a/src/HOL/Algebra/Algebra.thy	Sun Feb 26 21:17:53 2023 +0000
+++ b/src/HOL/Algebra/Algebra.thy	Mon Feb 27 17:09:59 2023 +0000
@@ -3,6 +3,6 @@
 theory Algebra
   imports Sylow Chinese_Remainder Zassenhaus Galois_Connection Generated_Fields Free_Abelian_Groups
      Divisibility Embedded_Algebras IntRing Sym_Groups Exact_Sequence Polynomials Algebraic_Closure
-     Left_Coset
+     Left_Coset SimpleGroups SndIsomorphismGrp
 begin
 end
diff -r aac23f2e7f3c -r c2013f617a70 src/HOL/Algebra/Coset.thy
--- a/src/HOL/Algebra/Coset.thy	Sun Feb 26 21:17:53 2023 +0000
+++ b/src/HOL/Algebra/Coset.thy	Mon Feb 27 17:09:59 2023 +0000
@@ -39,7 +39,7 @@
   "H \<lhd> G \<equiv> normal H G"
 
 lemma (in comm_group) subgroup_imp_normal: "subgroup A G \<Longrightarrow> A \<lhd> G"
-  by (simp add: normal_def normal_axioms_def is_group l_coset_def r_coset_def m_comm subgroup.mem_carrier)
+  by (simp add: normal_def normal_axioms_def l_coset_def r_coset_def m_comm subgroup.mem_carrier)
 
 lemma l_coset_eq_set_mult: \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close>
   fixes G (structure)
@@ -468,13 +468,65 @@
   using assms normal_inv_iff apply blast
   by (simp add: assms normal.inv_op_closed2)
 
+lemma (in group) one_is_normal: "{\<one>} \<lhd> G"
+  using normal_invI triv_subgroup by force
 
-lemma (in group) one_is_normal: "{\<one>} \<lhd> G"
-proof(intro normal_invI)
-  show "subgroup {\<one>} G"
-    by (simp add: subgroup_def)
-qed simp
+text \<open>The intersection of two normal subgroups is, again, a normal subgroup.\<close>
+lemma (in group) normal_subgroup_intersect:
+  assumes "M \<lhd> G" and "N \<lhd> G" shows "M \<inter> N \<lhd> G"
+  using  assms normal_inv_iff subgroups_Inter_pair by force
+
+
+text \<open>Being a normal subgroup is preserved by surjective homomorphisms.\<close>
 
+lemma (in normal) surj_hom_normal_subgroup:
+  assumes \<phi>: "group_hom G F \<phi>"
+  assumes \<phi>surj: "\<phi> ` (carrier G) = carrier F"
+  shows "(\<phi> ` H) \<lhd> F"
+proof (rule group.normalI)
+  show "group F"
+    using \<phi> group_hom.axioms(2) by blast
+next
+  show "subgroup (\<phi> ` H) F"
+    using \<phi> group_hom.subgroup_img_is_subgroup subgroup_axioms by blast
+next
+  show "\<forall>x\<in>carrier F. \<phi> ` H #>\<^bsub>F\<^esub> x = x <#\<^bsub>F\<^esub> \<phi> ` H"
+  proof
+    fix f
+    assume f: "f \<in> carrier F"
+    with \<phi>surj obtain g where g: "g \<in> carrier G" "f = \<phi> g" by auto
+    hence "\<phi> ` H #>\<^bsub>F\<^esub> f = \<phi> ` H #>\<^bsub>F\<^esub> \<phi> g" by simp
+    also have "... = (\<lambda>x. (\<phi> x) \<otimes>\<^bsub>F\<^esub> (\<phi> g)) ` H" 
+      unfolding r_coset_def image_def by auto
+    also have "... = (\<lambda>x. \<phi> (x \<otimes> g)) ` H" 
+      using subset g \<phi> group_hom.hom_mult unfolding image_def by fastforce
+    also have "... = \<phi> ` (H #> g)" 
+      using \<phi> unfolding r_coset_def by auto
+    also have "... = \<phi> ` (g <# H)" 
+      by (metis coset_eq g(1))
+    also have "... = (\<lambda>x. \<phi> (g \<otimes> x)) ` H" 
+      using \<phi> unfolding l_coset_def by auto
+    also have "... = (\<lambda>x. (\<phi> g) \<otimes>\<^bsub>F\<^esub> (\<phi> x)) ` H" 
+      using subset g \<phi> group_hom.hom_mult by fastforce
+    also have "... = \<phi> g <#\<^bsub>F\<^esub> \<phi> ` H" 
+      unfolding l_coset_def image_def by auto
+    also have "... = f <#\<^bsub>F\<^esub> \<phi> ` H" 
+      using g by simp
+    finally show "\<phi> ` H #>\<^bsub>F\<^esub> f = f <#\<^bsub>F\<^esub> \<phi> ` H".
+  qed
+qed
+
+text \<open>Being a normal subgroup is preserved by group isomorphisms.\<close>
+lemma iso_normal_subgroup:
+  assumes \<phi>: "\<phi> \<in> iso G F" "group G" "group F" "H \<lhd> G"
+  shows "(\<phi> ` H) \<lhd> F"
+  by (meson assms Group.iso_iff group_hom_axioms_def group_hom_def normal.surj_hom_normal_subgroup)
+
+text \<open>The set product of two normal subgroups is a normal subgroup.\<close>
+lemma (in group) setmult_lcos_assoc:
+  "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G\<rbrakk>
+      \<Longrightarrow> (x <# H) <#> K = x <# (H <#> K)"
+  by (force simp add: l_coset_def set_mult_def m_assoc)
 
 subsection\<open>More Properties of Left Cosets\<close>
 
@@ -770,8 +822,17 @@
   order :: "('a, 'b) monoid_scheme \<Rightarrow> nat"
   where "order S = card (carrier S)"
 
+lemma iso_same_order:
+  assumes "\<phi> \<in> iso G H"
+  shows "order G = order H"
+  by (metis assms is_isoI iso_same_card order_def order_def)
+
 lemma (in monoid) order_gt_0_iff_finite: "0 < order G \<longleftrightarrow> finite (carrier G)"
-by(auto simp add: order_def card_gt_0_iff)
+  by(auto simp add: order_def card_gt_0_iff)
+
+lemma (in group) order_one_triv_iff:
+  shows "(order G = 1) = (carrier G = {\<one>})"
+  by (metis One_nat_def card.empty card_Suc_eq empty_iff one_closed order_def singleton_iff)
 
 lemma (in group) rcosets_part_G:
   assumes "subgroup H G"
@@ -889,6 +950,11 @@
   qed
 qed
 
+text \<open>The cardinality of the right cosets of the trivial subgroup is the cardinality of the group itself:\<close>
+corollary (in group) card_rcosets_triv:
+  assumes "finite (carrier G)"
+  shows "card (rcosets {\<one>}) = order G"
+  using lagrange triv_subgroup by fastforce
 
 subsection \<open>Quotient Groups: Factorization of a Group\<close>
 
@@ -1523,7 +1589,7 @@
 
 subsubsection "More Lemmas about set multiplication"
 
-(*A group multiplied by a subgroup stays the same*)
+text \<open>A group multiplied by a subgroup stays the same\<close>
 lemma (in group) set_mult_carrier_idem:
   assumes "subgroup H G"
   shows "(carrier G) <#> H = carrier G"
@@ -1537,13 +1603,13 @@
   ultimately show "carrier G \<subseteq> (carrier G) <#> H" by simp
 qed
 
-(*Same lemma as above, but everything is included in a subgroup*)
+text \<open>Same lemma as above, but everything is included in a subgroup\<close>
 lemma (in group) set_mult_subgroup_idem:
   assumes HG: "subgroup H G" and NG: "subgroup N (G \<lparr> carrier := H \<rparr>)"
   shows "H <#> N = H"
   using group.set_mult_carrier_idem[OF subgroup.subgroup_is_group[OF HG group_axioms] NG] by simp
 
-(*A normal subgroup is commutative with set_mult*)
+text \<open>A normal subgroup is commutative with set_mult\<close>
 lemma (in group) commut_normal:
   assumes "subgroup H G" and "N\<lhd>G"
   shows "H<#>N = N<#>H"
@@ -1554,22 +1620,22 @@
   ultimately show "H<#>N = N<#>H" by simp
 qed
 
-(*Same lemma as above, but everything is included in a subgroup*)
+text \<open>Same lemma as above, but everything is included in a subgroup\<close>
 lemma (in group) commut_normal_subgroup:
   assumes "subgroup H G" and "N \<lhd> (G\<lparr> carrier := H \<rparr>)"
     and "subgroup K (G \<lparr> carrier := H \<rparr>)"
   shows "K <#> N = N <#> K"
-  using group.commut_normal[OF subgroup.subgroup_is_group[OF assms(1) group_axioms] assms(3,2)] by simp
-
+  by (metis assms(2) assms(3) group.commut_normal normal.axioms(2) set_mult_consistent)
 
 
 subsubsection "Lemmas about intersection and normal subgroups"
+text \<open>Mostly by Jakob von Raumer\<close>
 
 lemma (in group) normal_inter:
   assumes "subgroup H G"
     and "subgroup K G"
     and "H1\<lhd>G\<lparr>carrier := H\<rparr>"
-  shows " (H1\<inter>K)\<lhd>(G\<lparr>carrier:= (H\<inter>K)\<rparr>)"
+  shows "(H1\<inter>K)\<lhd>(G\<lparr>carrier:= (H\<inter>K)\<rparr>)"
 proof-
   define HK and H1K and GH and GHK
     where "HK = H\<inter>K" and "H1K=H1\<inter>K" and "GH =G\<lparr>carrier := H\<rparr>" and "GHK = (G\<lparr>carrier:= (H\<inter>K)\<rparr>)"
@@ -1647,4 +1713,337 @@
  by auto
 qed
 
+lemma (in group) normal_restrict_supergroup:
+  assumes "subgroup S G" "N \<lhd> G" "N \<subseteq> S"
+  shows "N \<lhd> (G\<lparr>carrier := S\<rparr>)"
+  by (metis assms inf.absorb_iff1 normal_Int_subgroup)
+
+text \<open>A subgroup relation survives factoring by a normal subgroup.\<close>
+lemma (in group) normal_subgroup_factorize:
+  assumes "N \<lhd> G" and "N \<subseteq> H" and "subgroup H G"
+  shows "subgroup (rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N) (G Mod N)"
+proof -
+  interpret GModN: group "G Mod N" 
+    using assms(1) by (rule normal.factorgroup_is_group)
+  have "N \<lhd> G\<lparr>carrier := H\<rparr>" 
+    using assms by (metis normal_restrict_supergroup)
+  hence grpHN: "group (G\<lparr>carrier := H\<rparr> Mod N)" 
+    by (rule normal.factorgroup_is_group)
+  have "(<#>\<^bsub>G\<lparr>carrier:=H\<rparr>\<^esub>) = (\<lambda>U K. (\<Union>h\<in>U. \<Union>k\<in>K. {h \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> k}))" 
+    using set_mult_def by metis
+  moreover have "\<dots> = (\<lambda>U K. (\<Union>h\<in>U. \<Union>k\<in>K. {h \<otimes>\<^bsub>G\<^esub> k}))" 
+    by auto
+  moreover have "(<#>) = (\<lambda>U K. (\<Union>h\<in>U. \<Union>k\<in>K. {h \<otimes> k}))" 
+    using set_mult_def by metis
+  ultimately have "(<#>\<^bsub>G\<lparr>carrier:=H\<rparr>\<^esub>) = (<#>\<^bsub>G\<^esub>)" 
+    by simp
+  with grpHN have "group ((G Mod N)\<lparr>carrier := (rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N)\<rparr>)" 
+    unfolding FactGroup_def by auto
+  moreover have "rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N \<subseteq> carrier (G Mod N)" 
+    unfolding FactGroup_def RCOSETS_def r_coset_def using assms(3) subgroup.subset 
+    by fastforce
+  ultimately show ?thesis
+    using GModN.group_incl_imp_subgroup by blast
+qed
+
+text \<open>A normality relation survives factoring by a normal subgroup.\<close>
+lemma (in group) normality_factorization:
+  assumes NG: "N \<lhd> G" and NH: "N \<subseteq> H" and HG: "H \<lhd> G"
+  shows "(rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N) \<lhd> (G Mod N)"
+proof -
+  from assms(1) interpret GModN: group "G Mod N" by (metis normal.factorgroup_is_group)
+  show ?thesis
+    unfolding GModN.normal_inv_iff
+  proof (intro conjI strip)
+    show "subgroup (rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N) (G Mod N)" 
+      using assms normal_imp_subgroup normal_subgroup_factorize by force
+  next
+    fix U V
+    assume U: "U \<in> carrier (G Mod N)" and V: "V \<in> rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N"
+    then obtain g where g: "g \<in> carrier G" "U = N #> g"
+      unfolding FactGroup_def RCOSETS_def by auto
+    from V obtain h where h: "h \<in> H" "V = N #> h" 
+      unfolding FactGroup_def RCOSETS_def r_coset_def by auto
+    hence hG: "h \<in> carrier G" 
+      using HG normal_imp_subgroup subgroup.mem_carrier by force
+    hence ghG: "g \<otimes> h \<in> carrier G" 
+      using g m_closed by auto
+    from g h have "g \<otimes> h \<otimes> inv g \<in> H" 
+      using HG normal_inv_iff by auto
+    moreover have "U <#> V <#> inv\<^bsub>G Mod N\<^esub> U = N #> (g \<otimes> h \<otimes> inv g)"
+    proof -
+      from g U have "inv\<^bsub>G Mod N\<^esub> U = N #> inv g" 
+        using NG normal.inv_FactGroup normal.rcos_inv by fastforce
+      hence "U <#> V <#> inv\<^bsub>G Mod N\<^esub> U = (N #> g) <#> (N #> h) <#> (N #> inv g)" 
+        using g h by simp
+      also have "\<dots> = N #> (g \<otimes> h \<otimes> inv g)" 
+        using g hG NG inv_closed ghG normal.rcos_sum by force
+      finally show ?thesis .
+    qed
+    ultimately show "U \<otimes>\<^bsub>G Mod N\<^esub> V \<otimes>\<^bsub>G Mod N\<^esub> inv\<^bsub>G Mod N\<^esub> U \<in> rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N" 
+      unfolding RCOSETS_def r_coset_def by auto
+  qed
+qed
+
+text \<open>Factorizing by the trivial subgroup is an isomorphism.\<close>
+lemma (in group) trivial_factor_iso:
+  shows "the_elem \<in> iso (G Mod {\<one>}) G"
+proof -
+  have "group_hom G G (\<lambda>x. x)" 
+    unfolding group_hom_def group_hom_axioms_def hom_def using is_group by simp
+  moreover have "(\<lambda>x. x) ` carrier G = carrier G" 
+    by simp
+  moreover have "kernel G G (\<lambda>x. x) = {\<one>}" 
+    unfolding kernel_def by auto
+  ultimately show ?thesis using group_hom.FactGroup_iso_set 
+    by force
+qed
+
+text \<open>And the dual theorem to the previous one: Factorizing by the group itself gives the trivial group\<close>
+
+lemma (in group) self_factor_iso:
+  shows "(\<lambda>X. the_elem ((\<lambda>x. \<one>) ` X)) \<in> iso (G Mod (carrier G)) (G\<lparr> carrier := {\<one>} \<rparr>)"
+proof -
+  have "group (G\<lparr>carrier := {\<one>}\<rparr>)" 
+    by (metis subgroup_imp_group triv_subgroup)
+  hence "group_hom G (G\<lparr>carrier := {\<one>}\<rparr>) (\<lambda>x. \<one>)" 
+    unfolding group_hom_def group_hom_axioms_def hom_def using is_group by auto
+  moreover have "(\<lambda>x. \<one>) ` carrier G = carrier (G\<lparr>carrier := {\<one>}\<rparr>)" 
+    by auto
+  moreover have "kernel G (G\<lparr>carrier := {\<one>}\<rparr>) (\<lambda>x. \<one>) = carrier G" 
+    unfolding kernel_def by auto
+  ultimately show ?thesis using group_hom.FactGroup_iso_set 
+    by force
+qed
+
+text \<open>Factoring by a normal subgroups yields the trivial group iff the subgroup is the whole group.\<close>
+lemma (in normal) fact_group_trivial_iff:
+  assumes "finite (carrier G)"
+  shows "(carrier (G Mod H) = {\<one>\<^bsub>G Mod H\<^esub>}) \<longleftrightarrow> (H = carrier G)"
+proof
+  assume "carrier (G Mod H) = {\<one>\<^bsub>G Mod H\<^esub>}" 
+  moreover have "order (G Mod H) * card H = order G"
+    by (simp add: FactGroup_def lagrange order_def subgroup_axioms)
+  ultimately have "card H = order G" unfolding order_def by auto
+  thus "H = carrier G"
+    by (simp add: assms card_subset_eq order_def subset)
+next
+  assume "H = carrier G"
+  with assms is_subgroup lagrange 
+  have "card (rcosets H) * order G = order G"
+    by (simp add: order_def)
+  then have "card (rcosets H) = 1" 
+    using assms order_gt_0_iff_finite by auto
+  hence "order (G Mod H) = 1" 
+    unfolding order_def FactGroup_def by auto
+  thus "carrier (G Mod H) = {\<one>\<^bsub>G Mod H\<^esub>}" 
+    using factorgroup_is_group by (metis group.order_one_triv_iff)
+qed
+
+text \<open>The union of all the cosets contained in a subgroup of a quotient group acts as a represenation for that subgroup.\<close>
+
+lemma (in normal) factgroup_subgroup_union_char:
+  assumes "subgroup A (G Mod H)"
+  shows "(\<Union>A) = {x \<in> carrier G. H #> x \<in> A}"
+proof
+  show "\<Union>A \<subseteq> {x \<in> carrier G. H #> x \<in> A}"
+  proof
+    fix x
+    assume x: "x \<in> \<Union>A"
+    then obtain a where a: "a \<in> A" "x \<in> a" and xx: "x \<in> carrier G"
+      using subgroup.subset assms by (force simp add: FactGroup_def RCOSETS_def r_coset_def)
+    from assms a obtain y where y: "y \<in> carrier G" "a = H #> y" 
+      using subgroup.subset unfolding FactGroup_def RCOSETS_def by force
+    with a have "x \<in> H #> y" by simp
+    hence "H #> y = H #> x" using y is_subgroup repr_independence by auto
+    with y(2) a(1) have "H #> x \<in> A" 
+      by auto
+    with xx show "x \<in> {x \<in> carrier G. H #> x \<in> A}" by simp
+  qed
+next
+  show "{x \<in> carrier G. H #> x \<in> A} \<subseteq> \<Union>A"
+    using rcos_self subgroup_axioms by auto
+qed
+
+lemma (in normal) factgroup_subgroup_union_subgroup:
+  assumes "subgroup A (G Mod H)"
+  shows "subgroup (\<Union>A) G"
+proof -
+  have "subgroup {x \<in> carrier G. H #> x \<in> A} G"
+  proof
+    show "{x \<in> carrier G. H #> x \<in> A} \<subseteq> carrier G" by auto
+  next
+    fix x y
+    assume xy: "x \<in> {x \<in> carrier G. H #> x \<in> A}" "y \<in> {x \<in> carrier G. H #> x \<in> A}"
+    then have "(H #> x) <#> (H #> y) \<in> A" 
+      using subgroup.m_closed assms unfolding FactGroup_def  by fastforce
+    hence "H #> (x \<otimes> y) \<in> A"
+      using xy rcos_sum by force
+    with xy show "x \<otimes> y \<in> {x \<in> carrier G. H #> x \<in> A}" by blast 
+  next
+    have "H #> \<one> \<in> A"
+      using assms subgroup.one_closed subset by fastforce
+    with assms one_closed show "\<one> \<in> {x \<in> carrier G. H #> x \<in> A}" by simp
+  next
+    fix x
+    assume x: "x \<in> {x \<in> carrier G. H #> x \<in> A}"
+    hence invx: "inv x \<in> carrier G" using inv_closed by simp
+    from assms x have "set_inv (H #> x) \<in> A" using subgroup.m_inv_closed
+      using inv_FactGroup subgroup.mem_carrier by fastforce
+    with invx show "inv x \<in> {x \<in> carrier G. H #> x \<in> A}"
+      using rcos_inv x by force
+  qed
+  with assms factgroup_subgroup_union_char show ?thesis by auto
+qed
+
+lemma (in normal) factgroup_subgroup_union_normal:
+  assumes "A \<lhd> (G Mod H)"
+  shows "\<Union>A \<lhd> G"
+proof - 
+  have "{x \<in> carrier G. H #> x \<in> A} \<lhd> G"
+    unfolding normal_def normal_axioms_def
+  proof (intro conjI strip)
+    from assms show "subgroup {x \<in> carrier G. H #> x \<in> A} G"
+      by (metis (full_types) factgroup_subgroup_union_char factgroup_subgroup_union_subgroup normal_imp_subgroup)
+  next
+    interpret Anormal: normal A "(G Mod H)" using assms by simp
+    show "{x \<in> carrier G. H #> x \<in> A} #> x = x <# {x \<in> carrier G. H #> x \<in> A}" if x: "x \<in> carrier G" for x
+    proof -
+      { fix y
+        assume y: "y \<in> {x \<in> carrier G. H #> x \<in> A} #> x"
+        then obtain x' where x': "x' \<in> carrier G" "H #> x' \<in> A" "y = x' \<otimes> x" 
+          unfolding r_coset_def by auto
+        from x(1) have Hx: "H #> x \<in> carrier (G Mod H)" 
+          unfolding FactGroup_def RCOSETS_def by force
+        with x' have "(inv\<^bsub>G Mod H\<^esub> (H #> x)) \<otimes>\<^bsub>G Mod H\<^esub> (H #> x') \<otimes>\<^bsub>G Mod H\<^esub> (H #> x) \<in> A" 
+          using Anormal.inv_op_closed1 by auto
+        hence "(set_inv (H #> x)) <#> (H #> x') <#> (H #> x) \<in> A" 
+          using inv_FactGroup Hx unfolding FactGroup_def by auto
+        hence "(H #> (inv x)) <#> (H #> x') <#> (H #> x) \<in> A" 
+          using x(1) by (metis rcos_inv)
+        hence "H #> (inv x \<otimes> x' \<otimes> x) \<in> A" 
+          by (metis inv_closed m_closed rcos_sum x'(1) x(1))
+        moreover have "inv x \<otimes> x' \<otimes> x \<in> carrier G" 
+          using x x' by (metis inv_closed m_closed)
+        ultimately have xcoset: "x \<otimes> (inv x \<otimes> x' \<otimes> x) \<in> x <# {x \<in> carrier G. H #> x \<in> A}" 
+          unfolding l_coset_def using x(1) by auto
+        have "x \<otimes> (inv x \<otimes> x' \<otimes> x) = (x \<otimes> inv x) \<otimes> x' \<otimes> x" 
+          by (metis Units_eq Units_inv_Units m_assoc m_closed x'(1) x(1))
+        also have "\<dots> = y"
+          by (simp add: x x')
+        finally have "x \<otimes> (inv x \<otimes> x' \<otimes> x) = y" .
+        with xcoset have "y \<in> x <# {x \<in> carrier G. H #> x \<in> A}" by auto}
+      moreover
+      { fix y
+        assume y: "y \<in> x <# {x \<in> carrier G. H #> x \<in> A}"
+        then obtain x' where x': "x' \<in> carrier G" "H #> x' \<in> A" "y = x \<otimes> x'" unfolding l_coset_def by auto
+        from x(1) have invx: "inv x \<in> carrier G" 
+          by (rule inv_closed)
+        hence Hinvx: "H #> (inv x) \<in> carrier (G Mod H)" 
+          unfolding FactGroup_def RCOSETS_def by force
+        with x' have "(inv\<^bsub>G Mod H\<^esub> (H #> inv x)) \<otimes>\<^bsub>G Mod H\<^esub> (H #> x') \<otimes>\<^bsub>G Mod H\<^esub> (H #> inv x) \<in> A" 
+          using invx Anormal.inv_op_closed1 by auto
+        hence "(set_inv (H #> inv x)) <#> (H #> x') <#> (H #> inv x) \<in> A" 
+          using inv_FactGroup Hinvx unfolding FactGroup_def by auto
+        hence "H #> (x \<otimes> x' \<otimes> inv x) \<in> A"
+          by (simp add: rcos_inv rcos_sum x x'(1))
+        moreover have "x \<otimes> x' \<otimes> inv x \<in> carrier G" using x x' by (metis inv_closed m_closed)
+        ultimately have xcoset: "(x \<otimes> x' \<otimes> inv x) \<otimes> x \<in> {x \<in> carrier G. H #> x \<in> A} #> x" 
+          unfolding r_coset_def using invx by auto
+        have "(x \<otimes> x' \<otimes> inv x) \<otimes> x = (x \<otimes> x') \<otimes> (inv x \<otimes> x)" 
+          by (metis Units_eq Units_inv_Units m_assoc m_closed x'(1) x(1))
+        also have "\<dots> = y"
+          by (simp add: x x')
+        finally have "x \<otimes> x' \<otimes> inv x \<otimes> x = y".
+        with xcoset have "y \<in> {x \<in> carrier G. H #> x \<in> A} #> x" by auto }
+      ultimately show ?thesis
+        by auto
+    qed
+  qed auto
+  with assms show ?thesis 
+    by (metis (full_types) factgroup_subgroup_union_char normal_imp_subgroup)
+qed
+
+lemma (in normal) factgroup_subgroup_union_factor:
+  assumes "subgroup A (G Mod H)"
+  shows "A = rcosets\<^bsub>G\<lparr>carrier := \<Union>A\<rparr>\<^esub> H"
+  using assms subgroup.mem_carrier factgroup_subgroup_union_char by (fastforce simp: RCOSETS_def FactGroup_def)
+
+
+section  \<open>Flattening the type of group carriers\<close>
+
+text \<open>Flattening here means to convert the type of group elements from 'a set to 'a.
+This is possible whenever the empty set is not an element of the group. By Jakob von Raumer\<close>
+
+
+definition flatten where
+  "flatten (G::('a set, 'b) monoid_scheme) rep = \<lparr>carrier=(rep ` (carrier G)),
+      monoid.mult=(\<lambda> x y. rep ((the_inv_into (carrier G) rep x) \<otimes>\<^bsub>G\<^esub> (the_inv_into (carrier G) rep y))), 
+      one=rep \<one>\<^bsub>G\<^esub> \<rparr>"
+
+lemma flatten_set_group_hom:
+  assumes group: "group G"
+  assumes inj: "inj_on rep (carrier G)"
+  shows "rep \<in> hom G (flatten G rep)"
+  by (force simp add: hom_def flatten_def inj the_inv_into_f_f)
+
+lemma flatten_set_group:
+  assumes "group G" "inj_on rep (carrier G)"
+  shows "group (flatten G rep)"
+proof (rule groupI)
+  fix x y
+  assume "x \<in> carrier (flatten G rep)" and "y \<in> carrier (flatten G rep)"
+  then show "x \<otimes>\<^bsub>flatten G rep\<^esub> y \<in> carrier (flatten G rep)" 
+    using assms group.surj_const_mult the_inv_into_f_f by (fastforce simp: flatten_def)
+next
+  show "\<one>\<^bsub>flatten G rep\<^esub> \<in> carrier (flatten G rep)" 
+    unfolding flatten_def by (simp add: assms group.is_monoid)
+next
+  fix x y z
+  assume "x \<in> carrier (flatten G rep)" "y \<in> carrier (flatten G rep)" "z \<in> carrier (flatten G rep)"
+  then show "x \<otimes>\<^bsub>flatten G rep\<^esub> y \<otimes>\<^bsub>flatten G rep\<^esub> z = x \<otimes>\<^bsub>flatten G rep\<^esub> (y \<otimes>\<^bsub>flatten G rep\<^esub> z)"
+    by (auto simp: assms flatten_def group.is_monoid monoid.m_assoc monoid.m_closed the_inv_into_f_f)
+next
+  fix x
+  assume x: "x \<in> carrier (flatten G rep)"
+  then show "\<one>\<^bsub>flatten G rep\<^esub> \<otimes>\<^bsub>flatten G rep\<^esub> x = x"
+    by (auto simp: assms group.is_monoid the_inv_into_f_f flatten_def)
+  then have "\<exists>y\<in>carrier G. rep (y \<otimes>\<^bsub>G\<^esub> z) = rep \<one>\<^bsub>G\<^esub>" if "z \<in> carrier G" for z
+    by (metis \<open>group G\<close> group.l_inv_ex that)
+  with assms x show "\<exists>y\<in>carrier (flatten G rep). y \<otimes>\<^bsub>flatten G rep\<^esub> x = \<one>\<^bsub>flatten G rep\<^esub>"
+    by (auto simp: flatten_def the_inv_into_f_f)
+qed
+
+lemma (in normal) flatten_set_group_mod_inj:
+  shows "inj_on (\<lambda>U. SOME g. g \<in> U) (carrier (G Mod H))"
+proof (rule inj_onI)
+  fix U V
+  assume U: "U \<in> carrier (G Mod H)" and V: "V \<in> carrier (G Mod H)"
+  then obtain g h where g: "U = H #> g" "g \<in> carrier G" and h: "V = H #> h" "h \<in> carrier G"
+    unfolding FactGroup_def RCOSETS_def by auto
+  hence notempty: "U \<noteq> {}" "V \<noteq> {}" 
+    by (metis empty_iff is_subgroup rcos_self)+
+  assume "(SOME g. g \<in> U) = (SOME g. g \<in> V)"
+  with notempty have "(SOME g. g \<in> U) \<in> U \<inter> V" 
+    by (metis IntI ex_in_conv someI)
+  thus "U = V" 
+    by (metis Int_iff g h is_subgroup repr_independence)
+qed
+
+lemma (in normal) flatten_set_group_mod:
+  shows "group (flatten (G Mod H) (\<lambda>U. SOME g. g \<in> U))"
+  by (simp add: factorgroup_is_group flatten_set_group flatten_set_group_mod_inj)
+
+lemma (in normal) flatten_set_group_mod_iso:
+  shows "(\<lambda>U. SOME g. g \<in> U) \<in> iso (G Mod H) (flatten (G Mod H) (\<lambda>U. SOME g. g \<in> U))"
+proof -
+  have "(\<lambda>U. SOME g. g \<in> U) \<in> hom (G Mod H) (flatten (G Mod H) (\<lambda>U. SOME g. g \<in> U))"
+    using factorgroup_is_group flatten_set_group_hom flatten_set_group_mod_inj by blast
+  moreover
+  have "inj_on (\<lambda>U. SOME g. g \<in> U) (carrier (G Mod H))"
+    using flatten_set_group_mod_inj by blast
+  ultimately show ?thesis
+    by (simp add: iso_def bij_betw_def flatten_def)
+qed
+
 end
diff -r aac23f2e7f3c -r c2013f617a70 src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Sun Feb 26 21:17:53 2023 +0000
+++ b/src/HOL/Algebra/Group.thy	Mon Feb 27 17:09:59 2023 +0000
@@ -674,6 +674,9 @@
     by (rule monoid.group_l_invI) (auto intro: l_inv mem_carrier)
 qed
 
+lemma (in group) triv_subgroup: "subgroup {\<one>} G"
+  by (auto simp: subgroup_def)
+
 lemma subgroup_is_submonoid:
   assumes "subgroup H G" shows "submonoid H G"
   using assms by (auto intro: submonoid.intro simp add: subgroup_def)
@@ -1362,6 +1365,12 @@
     using group_hom.img_is_subgroup[of "G \<lparr> carrier := I \<rparr>" H h] by simp
 qed
 
+lemma (in subgroup) iso_subgroup: \<^marker>\<open>contributor \<open>Jakob von Raumer\<close>\<close>
+  assumes "group G" "group F"
+  assumes "\<phi> \<in> iso G F"
+  shows "subgroup (\<phi> ` H) F"
+  by (metis assms Group.iso_iff group_hom.intro group_hom_axioms_def group_hom.subgroup_img_is_subgroup subgroup_axioms)
+
 lemma (in group_hom) induced_group_hom: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   assumes "subgroup I G"
   shows "group_hom (G \<lparr> carrier := I \<rparr>) (H \<lparr> carrier := h ` I \<rparr>) h"
@@ -1374,6 +1383,24 @@
           subgroup.subgroup_is_group[OF subgroup_img_is_subgroup[OF assms] is_group] by simp
 qed
 
+text \<open>An isomorphism restricts to an isomorphism of subgroups.\<close>
+
+lemma iso_restrict:
+  assumes "\<phi> \<in> iso G F"
+  assumes groups: "group G" "group F"
+  assumes HG: "subgroup H G"
+  shows "(restrict \<phi> H) \<in> iso (G\<lparr>carrier := H\<rparr>) (F\<lparr>carrier := \<phi> ` H\<rparr>)"
+proof -
+  have "\<And>x y. \<lbrakk>x \<in> H; y \<in> H; x \<otimes>\<^bsub>G\<^esub> y \<in> H\<rbrakk> \<Longrightarrow> \<phi> (x \<otimes>\<^bsub>G\<^esub> y) = \<phi> x \<otimes>\<^bsub>F\<^esub> \<phi> y"
+    by (meson assms hom_mult iso_imp_homomorphism subgroup.mem_carrier)
+  moreover have "\<And>x y. \<lbrakk>x \<in> H; y \<in> H; x \<otimes>\<^bsub>G\<^esub> y \<notin> H\<rbrakk> \<Longrightarrow> \<phi> x \<otimes>\<^bsub>F\<^esub> \<phi> y = undefined"
+    by (simp add: HG subgroup.m_closed)
+  moreover have "\<And>x y. \<lbrakk>x \<in> H; y \<in> H; \<phi> x = \<phi> y\<rbrakk> \<Longrightarrow> x = y"
+    by (smt (verit, ccfv_SIG) assms group.iso_iff_group_isomorphisms group_isomorphisms_def subgroup.mem_carrier)
+  ultimately show ?thesis
+    by (auto simp: iso_def hom_def bij_betw_def inj_on_def)
+qed
+
 lemma (in group) canonical_inj_is_hom: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
   assumes "subgroup H G"
   shows "group_hom (G \<lparr> carrier := H \<rparr>) G id"
@@ -1636,9 +1663,8 @@
 qed
 
 lemma (in group) subgroups_Inter_pair :
-  assumes  "subgroup I G"
-    and  "subgroup J G"
-  shows "subgroup (I\<inter>J) G" using subgroups_Inter[ where ?A = "{I,J}"] assms by auto
+  assumes "subgroup I G" "subgroup J G" shows "subgroup (I\<inter>J) G" 
+  using subgroups_Inter[ where ?A = "{I,J}"] assms by auto
 
 theorem (in group) subgroups_complete_lattice:
   "complete_lattice \<lparr>carrier = {H. subgroup H G}, eq = (=), le = (\<subseteq>)\<rparr>"
diff -r aac23f2e7f3c -r c2013f617a70 src/HOL/Algebra/SimpleGroups.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/SimpleGroups.thy	Mon Feb 27 17:09:59 2023 +0000
@@ -0,0 +1,95 @@
+(*  Title:      Simple Groups
+    Author:     Jakob von Raumer, Karlsruhe Institute of Technology
+    Maintainer: Jakob von Raumer <jakob.raumer@student.kit.edu>
+*)
+
+theory SimpleGroups
+imports Coset "HOL-Computational_Algebra.Primes"
+begin
+
+section \<open>Simple Groups\<close>
+
+locale simple_group = group +
+  assumes order_gt_one: "order G > 1"
+  assumes no_real_normal_subgroup: "\<And>H. H \<lhd> G \<Longrightarrow> (H = carrier G \<or> H = {\<one>})"
+
+lemma (in simple_group) is_simple_group: "simple_group G" 
+  by (rule simple_group_axioms)
+
+text \<open>Simple groups are non-trivial.\<close>
+
+lemma (in simple_group) simple_not_triv: "carrier G \<noteq> {\<one>}" 
+  using order_gt_one unfolding order_def by auto
+
+text \<open>Every group of prime order is simple\<close>
+
+lemma (in group) prime_order_simple:
+  assumes prime: "prime (order G)"
+  shows "simple_group G"
+proof
+  from prime show "1 < order G" 
+    unfolding prime_nat_iff by auto
+next
+  fix H
+  assume "H \<lhd> G"
+  hence HG: "subgroup H G" unfolding normal_def by simp
+  hence "card H dvd order G"
+    by (metis dvd_triv_right lagrange)
+  with prime have "card H = 1 \<or> card H = order G" 
+    unfolding prime_nat_iff by simp
+  thus "H = carrier G \<or> H = {\<one>}"
+  proof
+    assume "card H = 1"
+    moreover from HG have "\<one> \<in> H" by (metis subgroup.one_closed)
+    ultimately show ?thesis by (auto simp: card_Suc_eq)
+  next
+    assume "card H = order G"
+    moreover from HG have "H \<subseteq> carrier G" unfolding subgroup_def by simp
+    moreover from prime have "finite (carrier G)"
+      using order_gt_0_iff_finite by force
+    ultimately show ?thesis 
+      unfolding order_def by (metis card_subset_eq)
+  qed
+qed
+
+text \<open>Being simple is a property that is preserved by isomorphisms.\<close>
+
+lemma (in simple_group) iso_simple:
+  assumes H: "group H"
+  assumes iso: "\<phi> \<in> iso G H"
+  shows "simple_group H"
+unfolding simple_group_def simple_group_axioms_def 
+proof (intro conjI strip H)
+  from iso have "order G = order H" unfolding iso_def order_def using bij_betw_same_card by auto
+  with order_gt_one show "1 < order H" by simp
+next
+  have inv_iso: "(inv_into (carrier G) \<phi>) \<in> iso H G" using iso
+    by (simp add: iso_set_sym)    
+  fix N
+  assume NH: "N \<lhd> H" 
+  then interpret Nnormal: normal N H by simp
+  define M where "M = (inv_into (carrier G) \<phi>) ` N"
+  hence MG: "M \<lhd> G" 
+    using inv_iso NH H by (metis is_group iso_normal_subgroup)
+  have surj: "\<phi> ` carrier G = carrier H" 
+    using iso unfolding iso_def bij_betw_def by simp
+  hence MN: "\<phi> ` M = N" 
+    unfolding M_def using Nnormal.subset image_inv_into_cancel by metis
+  then have "N = {\<one>\<^bsub>H\<^esub>}" if "M = {\<one>}"
+    using Nnormal.subgroup_axioms subgroup.one_closed that by force
+  then show "N = carrier H \<or> N = {\<one>\<^bsub>H\<^esub>}"
+    by (metis MG MN no_real_normal_subgroup surj)
+qed
+
+text \<open>As a corollary of this: Factorizing a group by itself does not result in a simple group!\<close>
+
+lemma (in group) self_factor_not_simple: "\<not> simple_group (G Mod (carrier G))"
+proof
+  assume assm: "simple_group (G Mod (carrier G))"
+  with self_factor_iso simple_group.iso_simple have "simple_group (G\<lparr>carrier := {\<one>}\<rparr>)"
+    using subgroup_imp_group triv_subgroup by blast
+  thus False 
+    using simple_group.simple_not_triv by force
+qed
+
+end
diff -r aac23f2e7f3c -r c2013f617a70 src/HOL/Algebra/SndIsomorphismGrp.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/SndIsomorphismGrp.thy	Mon Feb 27 17:09:59 2023 +0000
@@ -0,0 +1,207 @@
+(*  Title:      The Second Isomorphism Theorem for Groups
+    Author:     Jakob von Raumer, Karlsruhe Institute of Technology
+    Maintainer: Jakob von Raumer <jakob.raumer@student.kit.edu>
+*)
+
+theory SndIsomorphismGrp
+imports Coset
+begin
+
+section \<open>The Second Isomorphism Theorem for Groups\<close>
+
+text \<open>This theory provides a proof of the second isomorphism theorems for groups. 
+The theorems consist of several facts about normal subgroups.\<close>
+
+text \<open>The first lemma states that whenever we have a subgroup @{term S} and
+a normal subgroup @{term H} of a group @{term G}, their intersection is normal
+in @{term G}\<close>
+
+locale second_isomorphism_grp = normal +
+  fixes S:: "'a set"
+  assumes subgrpS: "subgroup S G"
+
+context second_isomorphism_grp
+begin
+
+interpretation groupS: group "G\<lparr>carrier := S\<rparr>"
+  using subgrpS 
+  by (metis subgroup_imp_group)
+
+lemma normal_subgrp_intersection_normal:
+  shows "S \<inter> H \<lhd> (G\<lparr>carrier := S\<rparr>)"
+proof(auto simp: groupS.normal_inv_iff)
+  from subgrpS is_subgroup have "\<And>x. x \<in> {S, H} \<Longrightarrow> subgroup x G" by auto
+  hence "subgroup (\<Inter> {S, H}) G" using subgroups_Inter by blast
+  hence "subgroup (S \<inter> H) G" by auto
+  moreover have "S \<inter> H \<subseteq> S" by simp
+  ultimately show "subgroup (S \<inter> H) (G\<lparr>carrier := S\<rparr>)"
+    by (simp add: subgroup_incl subgrpS)
+next
+  fix g h
+  assume g: "g \<in> S" and hH: "h \<in> H" and hS: "h \<in> S" 
+  from g hH subgrpS show "g \<otimes> h \<otimes> inv\<^bsub>G\<lparr>carrier := S\<rparr>\<^esub> g \<in> H" 
+    by (metis inv_op_closed2 subgroup.mem_carrier m_inv_consistent)
+  from g hS subgrpS show "g \<otimes> h \<otimes> inv\<^bsub>G\<lparr>carrier := S\<rparr>\<^esub> g \<in> S" 
+    by (metis subgroup.m_closed subgroup.m_inv_closed m_inv_consistent)
+qed
+
+lemma normal_set_mult_subgroup:
+  shows "subgroup (H <#> S) G"
+proof(rule subgroupI)
+  show "H <#> S \<subseteq> carrier G" 
+    by (metis setmult_subset_G subgroup.subset subgrpS subset)
+next
+  have "\<one> \<in> H" "\<one> \<in> S" 
+    using is_subgroup subgrpS subgroup.one_closed by auto
+  hence "\<one> \<otimes> \<one> \<in> H <#> S" 
+    unfolding set_mult_def by blast
+  thus "H <#> S \<noteq> {}" by auto
+next
+  fix g
+  assume g: "g \<in> H <#> S"
+  then obtain h s where h: "h \<in> H" and s: "s \<in> S" and ghs: "g = h \<otimes> s" unfolding set_mult_def 
+    by auto
+  hence "s \<in> carrier G" by (metis subgroup.mem_carrier subgrpS)
+  with h ghs obtain h' where h': "h' \<in> H" and "g = s \<otimes> h'" 
+    using coset_eq unfolding r_coset_def l_coset_def by auto
+  with s have "inv g = (inv h') \<otimes> (inv s)" 
+    by (metis inv_mult_group mem_carrier subgroup.mem_carrier subgrpS)
+  moreover from h' s subgrpS have "inv h' \<in> H" "inv s \<in> S" 
+    using subgroup.m_inv_closed m_inv_closed by auto
+  ultimately show "inv g \<in> H <#> S" 
+    unfolding set_mult_def by auto
+next
+  fix g g'
+  assume g: "g \<in> H <#> S" and h: "g' \<in> H <#> S"
+  then obtain h h' s s' where hh'ss': "h \<in> H" "h' \<in> H" "s \<in> S" "s' \<in> S" and "g = h \<otimes> s" and "g' = h' \<otimes> s'" 
+    unfolding set_mult_def by auto
+  hence "g \<otimes> g' = (h \<otimes> s) \<otimes> (h' \<otimes> s')" by metis
+  also from hh'ss' have inG: "h \<in> carrier G" "h' \<in> carrier G" "s \<in> carrier G" "s' \<in> carrier G" 
+    using subgrpS mem_carrier subgroup.mem_carrier by force+
+  hence "(h \<otimes> s) \<otimes> (h' \<otimes> s') = h \<otimes> (s \<otimes> h') \<otimes> s'" 
+    using m_assoc by auto
+  also from hh'ss' inG obtain h'' where h'': "h'' \<in> H" and "s \<otimes> h' = h'' \<otimes> s"
+    using coset_eq unfolding r_coset_def l_coset_def 
+    by fastforce
+  hence "h \<otimes> (s \<otimes> h') \<otimes> s' = h \<otimes> (h'' \<otimes> s) \<otimes> s'" 
+    by simp
+  also from h'' inG have "... = (h \<otimes> h'') \<otimes> (s \<otimes> s')" 
+    using m_assoc mem_carrier by auto
+  finally have "g \<otimes> g' = h \<otimes> h'' \<otimes> (s \<otimes> s')".
+  moreover have "... \<in> H <#> S" 
+    unfolding set_mult_def using h'' hh'ss' subgrpS subgroup.m_closed by fastforce
+  ultimately show "g \<otimes> g' \<in> H <#> S" 
+    by simp
+qed
+
+lemma H_contained_in_set_mult:
+  shows "H \<subseteq> H <#> S"
+proof 
+  fix x
+  assume x: "x \<in> H"
+  have "x \<otimes> \<one> \<in> H <#> S" unfolding set_mult_def
+    using second_isomorphism_grp.subgrpS second_isomorphism_grp_axioms subgroup.one_closed x by force
+  with x show "x \<in> H <#> S" by (metis mem_carrier r_one)
+qed
+
+lemma S_contained_in_set_mult:
+  shows "S \<subseteq> H <#> S"
+proof
+  fix s
+  assume s: "s \<in> S"
+  then have "\<one> \<otimes> s \<in> H <#> S" unfolding set_mult_def by force
+  with s show "s \<in> H <#> S" using subgrpS subgroup.mem_carrier l_one by force
+qed
+
+lemma normal_intersection_hom:
+  shows "group_hom (G\<lparr>carrier := S\<rparr>) ((G\<lparr>carrier := H <#> S\<rparr>) Mod H) (\<lambda>g. H #> g)"
+proof -
+  have "group ((G\<lparr>carrier := H <#> S\<rparr>) Mod H)"
+    by (simp add: H_contained_in_set_mult normal.factorgroup_is_group normal_axioms 
+        normal_restrict_supergroup normal_set_mult_subgroup)
+  moreover
+  { fix g
+    assume g: "g \<in> S"
+    with g have "g \<in> H <#> S"
+      using S_contained_in_set_mult by blast
+    hence "H #> g \<in> carrier ((G\<lparr>carrier := H <#> S\<rparr>) Mod H)" 
+      unfolding FactGroup_def RCOSETS_def r_coset_def by auto }
+  moreover
+  have "\<And>x y. \<lbrakk>x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> H #> x \<otimes> y = H #> x <#> (H #> y)"
+    using normal.rcos_sum normal_axioms subgroup.mem_carrier subgrpS by fastforce
+  ultimately show ?thesis
+    by (auto simp: group_hom_def group_hom_axioms_def hom_def)
+qed
+
+lemma normal_intersection_hom_kernel:
+  shows "kernel (G\<lparr>carrier := S\<rparr>) ((G\<lparr>carrier := H <#> S\<rparr>) Mod H) (\<lambda>g. H #> g) = H \<inter> S"
+proof -
+  have "kernel (G\<lparr>carrier := S\<rparr>) ((G\<lparr>carrier := H <#> S\<rparr>) Mod H) (\<lambda>g. H #> g)
+      = {g \<in> S. H #> g = \<one>\<^bsub>(G\<lparr>carrier := H <#> S\<rparr>) Mod H\<^esub>}" 
+    unfolding kernel_def by auto
+  also have "... = {g \<in> S. H #> g = H}" 
+    unfolding FactGroup_def by auto
+  also have "... = {g \<in> S. g \<in> H}"
+    by (meson coset_join1 is_group rcos_const subgroupE(1) subgroup_axioms subgrpS subset_eq)
+  also have "... = H \<inter> S" by auto
+  finally show ?thesis.
+qed
+
+lemma normal_intersection_hom_surj:
+  shows "(\<lambda>g. H #> g) ` carrier (G\<lparr>carrier := S\<rparr>) = carrier ((G\<lparr>carrier := H <#> S\<rparr>) Mod H)"
+proof auto
+  fix g
+  assume "g \<in> S"
+  hence "g \<in> H <#> S" 
+    using S_contained_in_set_mult by auto
+  thus "H #> g \<in> carrier ((G\<lparr>carrier := H <#> S\<rparr>) Mod H)" 
+    unfolding FactGroup_def RCOSETS_def r_coset_def by auto
+next
+  fix x
+  assume "x \<in> carrier (G\<lparr>carrier := H <#> S\<rparr> Mod H)"
+  then obtain h s where h: "h \<in> H" and s: "s \<in> S" and "x = H #> (h \<otimes> s)"
+    unfolding FactGroup_def RCOSETS_def r_coset_def set_mult_def by auto
+  hence "x = (H #> h) #> s" 
+    by (metis h s coset_mult_assoc mem_carrier subgroup.mem_carrier subgrpS subset)
+  also have "... = H #> s" 
+    by (metis h is_group rcos_const)
+  finally have "x = H #> s".
+  with s show "x \<in> (#>) H ` S" 
+    by simp
+qed
+
+text \<open>Finally we can prove the actual isomorphism theorem:\<close>
+
+theorem normal_intersection_quotient_isom:
+  shows "(\<lambda>X. the_elem ((\<lambda>g. H #> g) ` X)) \<in> iso ((G\<lparr>carrier := S\<rparr>) Mod (H \<inter> S)) (((G\<lparr>carrier := H <#> S\<rparr>)) Mod H)"
+using normal_intersection_hom_kernel[symmetric] normal_intersection_hom normal_intersection_hom_surj
+by (metis group_hom.FactGroup_iso_set)
+
+end
+
+
+corollary (in group) normal_subgroup_set_mult_closed:
+  assumes "M \<lhd> G" and "N \<lhd> G"
+  shows "M <#> N \<lhd> G"
+proof (rule normalI)
+  from assms show "subgroup (M <#> N) G"
+    using second_isomorphism_grp.normal_set_mult_subgroup normal_imp_subgroup
+    unfolding second_isomorphism_grp_def second_isomorphism_grp_axioms_def by force
+next
+  show "\<forall>x\<in>carrier G. M <#> N #> x = x <# (M <#> N)"
+  proof
+    fix x
+    assume x: "x \<in> carrier G"
+    have "M <#> N #> x = M <#> (N #> x)" 
+      by (metis assms normal_inv_iff setmult_rcos_assoc subgroup.subset x)
+    also have "\<dots> = M <#> (x <# N)" 
+      by (metis assms(2) normal.coset_eq x)
+    also have "\<dots> = (M #> x) <#> N" 
+      by (metis assms normal_imp_subgroup rcos_assoc_lcos subgroup.subset x)
+    also have "\<dots> = x <# (M <#> N)"
+      by (simp add: assms normal.coset_eq normal_imp_subgroup setmult_lcos_assoc subgroup.subset x)
+    finally show "M <#> N #> x = x <# (M <#> N)" .
+  qed
+qed
+
+end