# HG changeset patch
# User paulson
# Date 1530459988 -3600
# Node ID fcffdcb8f5067c3e75a909f4840c0e61b9375fc8
# Parent  5273df52ad830cadbf2c48d768d5ad7761144c1a# Parent  22d51874f37d88d21908dc663fbff18cc4fa3057
merged

diff -r 5273df52ad83 -r fcffdcb8f506 src/HOL/Algebra/Coset.thy
--- a/src/HOL/Algebra/Coset.thy	Sun Jul 01 17:38:08 2018 +0200
+++ b/src/HOL/Algebra/Coset.thy	Sun Jul 01 16:46:28 2018 +0100
@@ -37,13 +37,12 @@
   normal_rel :: "['a set, ('a, 'b) monoid_scheme] \<Rightarrow> bool"  (infixl "\<lhd>" 60) where
   "H \<lhd> G \<equiv> normal H G"
 
-(* ************************************************************************** *)
-(* Next two lemmas contributed by Martin Baillon.                                  *)
+(*Next two lemmas contributed by Martin Baillon.*)
 
 lemma l_coset_eq_set_mult:
   fixes G (structure)
   shows "x <# H = {x} <#> H"
-  unfolding l_coset_def set_mult_def by simp 
+  unfolding l_coset_def set_mult_def by simp
 
 lemma r_coset_eq_set_mult:
   fixes G (structure)
@@ -74,7 +73,7 @@
                       and h2: "h2 \<in> H" "r2 = h2 \<otimes> g"
     using r1 r2 unfolding r_coset_def by blast
   hence "r1 \<otimes> (inv r2) = (h1 \<otimes> g) \<otimes> ((inv g) \<otimes> (inv h2))"
-    using inv_mult_group is_group assms(1) g(1) subgroup.mem_carrier by fastforce 
+    using inv_mult_group is_group assms(1) g(1) subgroup.mem_carrier by fastforce
   also have " ... =  (h1 \<otimes> (g \<otimes> inv g) \<otimes> inv h2)"
     using h1 h2 assms(1) g(1) inv_closed m_closed monoid.m_assoc
           monoid_axioms subgroup.mem_carrier by smt
@@ -89,21 +88,6 @@
 
 subsection \<open>Stable Operations for Subgroups\<close>
 
-lemma (in group) subgroup_set_mult_equality[simp]:
-  assumes "subgroup H G" "I \<subseteq> H" "J \<subseteq> H"
-  shows "I <#>\<^bsub>G \<lparr> carrier := H \<rparr>\<^esub> J = I <#> J"
-  unfolding set_mult_def subgroup_mult_equality[OF assms(1)] by auto
-
-lemma (in group) subgroup_rcos_equality[simp]:
-  assumes "subgroup H G" "I \<subseteq> H" "h \<in> H"
-  shows "I #>\<^bsub>G \<lparr> carrier := H \<rparr>\<^esub> h = I #> h"
-  using subgroup_set_mult_equality by (simp add: r_coset_eq_set_mult assms)
-
-lemma (in group) subgroup_lcos_equality[simp]:
-  assumes "subgroup H G" "I \<subseteq> H" "h \<in> H"
-  shows "h <#\<^bsub>G \<lparr> carrier := H \<rparr>\<^esub> I = h <# I"
-  using subgroup_set_mult_equality by (simp add: l_coset_eq_set_mult assms)
-
 lemma set_mult_consistent [simp]:
   "N <#>\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> K = N <#>\<^bsub>G\<^esub> K"
   unfolding set_mult_def by simp
@@ -184,7 +168,7 @@
   assumes "M #> x = M #> y"
     and "x \<in> carrier G"  "y \<in> carrier G" "M \<subseteq> carrier G"
   shows "M #> (x \<otimes> (inv y)) = M " using assms
-  by (metis group.coset_mult_assoc group.coset_mult_one inv_closed is_group r_inv) 
+  by (metis group.coset_mult_assoc group.coset_mult_one inv_closed is_group r_inv)
 
 lemma (in group) coset_join1:
   assumes "H #> x = H"
@@ -297,12 +281,12 @@
   shows "(x' \<in> H #> x) = (x' \<otimes> inv x \<in> H)"
   using rcos_module_rev rcos_module_imp assms by blast
 
-text \<open>Right cosets are subsets of the carrier.\<close> 
+text \<open>Right cosets are subsets of the carrier.\<close>
 lemma (in subgroup) rcosets_carrier:
   assumes "group G" "X \<in> rcosets H"
   shows "X \<subseteq> carrier G"
   using assms elemrcos_carrier singletonD
-  subset_eq unfolding RCOSETS_def by force 
+  subset_eq unfolding RCOSETS_def by force
 
 
 text \<open>Multiplication of general subsets\<close>
@@ -369,7 +353,7 @@
 lemma normal_imp_subgroup: "H \<lhd> G \<Longrightarrow> 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 is_group)
 
@@ -378,32 +362,32 @@
   shows "(inv x) \<otimes> h \<otimes> x \<in> H"
 proof -
   have "h \<otimes> x \<in> x <# H"
-    using assms coset_eq assms(1) unfolding r_coset_def by blast 
+    using assms coset_eq assms(1) unfolding r_coset_def by blast
   then obtain h' where "h' \<in> H" "h \<otimes> x = x \<otimes> h'"
     unfolding l_coset_def by blast
-  thus ?thesis by (metis assms inv_closed l_inv l_one m_assoc mem_carrier) 
+  thus ?thesis by (metis assms inv_closed l_inv l_one m_assoc mem_carrier)
 qed
 
 lemma (in normal) inv_op_closed2:
   assumes "x \<in> carrier G" and "h \<in> H"
   shows "x \<otimes> h \<otimes> (inv x) \<in> H"
-  using assms inv_op_closed1 by (metis inv_closed inv_inv) 
+  using assms inv_op_closed1 by (metis inv_closed inv_inv)
 
 
 text\<open>Alternative characterization of normal subgroups\<close>
 lemma (in group) normal_inv_iff:
-     "(N \<lhd> G) = 
+     "(N \<lhd> G) =
       (subgroup N G \<and> (\<forall>x \<in> carrier G. \<forall>h \<in> N. x \<otimes> h \<otimes> (inv x) \<in> N))"
       (is "_ = ?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 \<otimes> h \<otimes> 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
@@ -413,9 +397,9 @@
       show "(\<Union>h\<in>N. {h \<otimes> x}) \<subseteq> (\<Union>h\<in>N. {x \<otimes> h})"
       proof clarify
         fix n
-        assume n: "n \<in> N" 
+        assume n: "n \<in> N"
         show "n \<otimes> x \<in> (\<Union>h\<in>N. {x \<otimes> h})"
-        proof 
+        proof
           from closed [of "inv x"]
           show "inv x \<otimes> n \<otimes> x \<in> N" by (simp add: x n)
           show "n \<otimes> x \<in> {x \<otimes> (inv x \<otimes> n \<otimes> x)}"
@@ -426,9 +410,9 @@
       show "(\<Union>h\<in>N. {x \<otimes> h}) \<subseteq> (\<Union>h\<in>N. {h \<otimes> x})"
       proof clarify
         fix n
-        assume n: "n \<in> N" 
+        assume n: "n \<in> N"
         show "x \<otimes> n \<in> (\<Union>h\<in>N. {h \<otimes> x})"
-        proof 
+        proof
           show "x \<otimes> n \<otimes> inv x \<in> N" by (simp add: x n closed)
           show "x \<otimes> n \<in> {x \<otimes> n \<otimes> inv x \<otimes> x}"
             by (simp add: x n m_assoc sb [THEN subsetD])
@@ -444,14 +428,14 @@
   using assms normal_inv_iff by blast
 
 corollary (in group) normal_invE:
-  assumes "N \<lhd> G" 
+  assumes "N \<lhd> G"
   shows "subgroup N G" and "\<And>x h. \<lbrakk> x \<in> carrier G; h \<in> N \<rbrakk> \<Longrightarrow> x \<otimes> h \<otimes> inv x \<in> N"
   using assms normal_inv_iff apply blast
-  by (simp add: assms normal.inv_op_closed2) 
+  by (simp add: assms normal.inv_op_closed2)
 
 
 lemma (in group) one_is_normal :
-   "{\<one>} \<lhd> G" 
+   "{\<one>} \<lhd> G"
 proof(intro normal_invI )
   show "subgroup {\<one>} G"
     by (simp add: subgroup_def)
@@ -470,7 +454,7 @@
   hence "\<And> h. h \<in> H \<Longrightarrow> x \<otimes> h = y \<otimes> ((inv h') \<otimes> h)"
     by (smt assms(2-3) inv_closed inv_solve_right m_assoc m_closed subgroup.mem_carrier)
   hence "\<And> xh. xh \<in> x <# H \<Longrightarrow> xh \<in> y <# H"
-    unfolding l_coset_def by (metis (no_types, lifting) UN_iff assms(3) h'(1) subgroup_def) 
+    unfolding l_coset_def by (metis (no_types, lifting) UN_iff assms(3) h'(1) subgroup_def)
   moreover have "\<And> h. h \<in> H \<Longrightarrow> y \<otimes> h = x \<otimes> (h' \<otimes> h)"
     using h' by (meson assms(2) assms(3) m_assoc subgroup.mem_carrier)
   hence "\<And> yh. yh \<in> y <# H \<Longrightarrow> yh \<in> x <# H"
@@ -494,7 +478,7 @@
   by (auto simp add: l_coset_def m_assoc  subgroup.subset [THEN subsetD] subgroup.m_closed)
 
 lemma (in group) l_coset_swap:
-  assumes "y \<in> x <# H" "x \<in> carrier G" "subgroup H G" 
+  assumes "y \<in> x <# H" "x \<in> carrier G" "subgroup H G"
   shows "x \<in> y <# H"
   using assms(2) l_repr_independence[OF assms] subgroup.one_closed[OF assms(3)]
   unfolding l_coset_def by fastforce
@@ -518,7 +502,7 @@
 
 lemma (in normal) rcos_inv:
   assumes x:     "x \<in> carrier G"
-  shows "set_inv (H #> x) = H #> (inv x)" 
+  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 \<in> H"
@@ -595,12 +579,12 @@
   show ?thesis
   proof (intro equivI)
     show "refl_on (carrier G) (rcong H)"
-      by (auto simp add: r_congruent_def refl_on_def) 
+      by (auto simp add: r_congruent_def refl_on_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 \<otimes> y \<in> H"
       hence "inv (inv x \<otimes> y) \<in> H" by simp
       thus "inv y \<otimes> x \<in> H" by (simp add: inv_mult_group)
@@ -613,7 +597,7 @@
          and "inv x \<otimes> y \<in> H" and "inv y \<otimes> z \<in> H"
       hence "(inv x \<otimes> y) \<otimes> (inv y \<otimes> z) \<in> H" by simp
       hence "inv x \<otimes> (y \<otimes> inv y) \<otimes> z \<in> H"
-        by (simp add: m_assoc del: r_inv Units_r_inv) 
+        by (simp add: m_assoc del: r_inv Units_r_inv)
       thus "inv x \<otimes> z \<in> H" by simp
     qed
   qed
@@ -639,7 +623,7 @@
   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 ) 
+  show ?thesis by (force simp add: r_congruent_def l_coset_def m_assoc [symmetric] a )
 qed
 
 
@@ -692,9 +676,9 @@
       have "inv c \<otimes> (inv a \<otimes> b) \<otimes> c \<in> H" by (rule inv_op_closed1)
   moreover
       from carr and inv_closed
-      have "inv c \<otimes> (inv a \<otimes> b) \<otimes> c = (inv c \<otimes> inv a) \<otimes> (b \<otimes> c)" 
+      have "inv c \<otimes> (inv a \<otimes> b) \<otimes> c = (inv c \<otimes> inv a) \<otimes> (b \<otimes> c)"
       by (force cong: m_assoc)
-  moreover 
+  moreover
       from carr and inv_closed
       have "\<dots> = (inv (a \<otimes> c)) \<otimes> (b \<otimes> c)"
       by (simp add: inv_mult_group)
@@ -803,7 +787,7 @@
   moreover have "?f ` H \<subseteq> R"
     using g unfolding r_coset_def by blast
   ultimately show ?thesis using inj_on_g unfolding bij_betw_def
-    using assms(2) g(1) by auto 
+    using assms(2) g(1) by auto
 qed
 
 corollary (in group) card_rcosets_equal:
@@ -843,7 +827,7 @@
   case False note inf_G = this
   thus ?thesis
   proof (cases "finite H")
-    case False thus ?thesis using inf_G  by (simp add: order_def)  
+    case False thus ?thesis using inf_G  by (simp add: order_def)
   next
     case True note finite_H = this
     have "infinite (rcosets H)"
@@ -860,7 +844,7 @@
       hence "order G = (card H) * (card (rcosets H))" by simp
       hence "order G \<noteq> 0" using finite_rcos finite_H assms ex_in_conv
                                 rcosets_part_G subgroup.one_closed by fastforce
-      thus False using inf_G order_gt_0_iff_finite by blast 
+      thus False using inf_G order_gt_0_iff_finite by blast
     qed
     thus ?thesis using inf_G by (simp add: order_def)
   qed
@@ -915,11 +899,11 @@
 done
 
 lemma mult_FactGroup [simp]: "X \<otimes>\<^bsub>(G Mod H)\<^esub> X' = X <#>\<^bsub>G\<^esub> X'"
-  by (simp add: FactGroup_def) 
+  by (simp add: FactGroup_def)
 
 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
 
@@ -929,10 +913,10 @@
   "(\<lambda>a. H #> a) \<in> hom G (G Mod H)"
   by (auto simp add: FactGroup_def RCOSETS_def Pi_def hom_def rcos_sum)
 
- 
+
 subsection\<open>The First Isomorphism Theorem\<close>
 
-text\<open>The quotient by the kernel of a homomorphism is isomorphic to the 
+text\<open>The quotient by the kernel of a homomorphism is isomorphic to the
   range of that homomorphism.\<close>
 
 definition
@@ -941,8 +925,8 @@
   where "kernel G H h = {x. x \<in> carrier G \<and> h x = \<one>\<^bsub>H\<^esub>}"
 
 lemma (in group_hom) subgroup_kernel: "subgroup (kernel G H h) G"
-apply (rule subgroup.intro) 
-apply (auto simp add: kernel_def group.intro is_group) 
+apply (rule subgroup.intro)
+apply (auto simp add: kernel_def group.intro is_group)
 done
 
 text\<open>The kernel of a homomorphism is a normal subgroup\<close>
@@ -956,10 +940,10 @@
   shows "X \<noteq> {}"
 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
 
@@ -969,7 +953,7 @@
   shows "the_elem (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 g intro!: imageI)
@@ -985,16 +969,16 @@
      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 \<otimes>\<^bsub>H\<^esub> h g'}" using X X'
     by (auto dest!: FactGroup_nonempty intro!: image_eqI
-             simp add: set_mult_def 
-                       subsetD [OF Xsub] subsetD [OF X'sub]) 
+             simp add: set_mult_def
+                       subsetD [OF Xsub] subsetD [OF X'sub])
   then show "the_elem (h ` (X <#> X')) = the_elem (h ` X) \<otimes>\<^bsub>H\<^esub> the_elem (h ` X')"
     by (auto simp add: all FactGroup_nonempty X X' the_elem_image_unique)
 qed
@@ -1005,28 +989,28 @@
      "\<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)
-apply (rename_tac y)  
-apply (rule_tac x="y \<otimes> g \<otimes> inv g'" in exI) 
-apply (simp add: G.m_assoc) 
+apply (rename_tac y)
+apply (rule_tac x="y \<otimes> g \<otimes> inv g'" in exI)
+apply (simp add: G.m_assoc)
 done
 
 lemma (in group_hom) FactGroup_inj_on:
      "inj_on (\<lambda>X. the_elem (h ` X)) (carrier (G Mod kernel G H h))"
-proof (simp add: inj_on_def, clarify) 
+proof (simp add: inj_on_def, 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'" 
+  hence all: "\<forall>x\<in>X. h x = h g" "\<forall>x\<in>X'. h x = h g'"
     by (force simp add: kernel_def r_coset_def image_def)+
   assume "the_elem (h ` X) = the_elem (h ` X')"
   hence h: "h g = h g'"
-    by (simp add: all FactGroup_nonempty X X' the_elem_image_unique) 
-  show "X=X'" by (rule equalityI) (simp_all add: FactGroup_subset h gX) 
+    by (simp add: all FactGroup_nonempty X X' the_elem_image_unique)
+  show "X=X'" by (rule equalityI) (simp_all add: FactGroup_subset h gX)
 qed
 
 text\<open>If the homomorphism @{term h} is onto @{term H}, then so is the
@@ -1042,10 +1026,10 @@
     fix y
     assume y: "y \<in> carrier H"
     with h obtain g where g: "g \<in> carrier G" "h g = y"
-      by (blast elim: equalityE) 
-    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 "y \<in> (\<lambda>X. the_elem (h ` X)) ` carrier (G Mod kernel G H h)" 
+      by (blast elim: equalityE)
+    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 "y \<in> (\<lambda>X. the_elem (h ` X)) ` carrier (G Mod kernel G H h)"
       apply (auto intro!: bexI image_eqI simp add: FactGroup_def RCOSETS_def)
       apply (subst the_elem_image_unique)
       apply auto
@@ -1059,8 +1043,8 @@
 theorem (in group_hom) FactGroup_iso_set:
   "h ` carrier G = carrier H
    \<Longrightarrow> (\<lambda>X. the_elem (h`X)) \<in> iso (G Mod (kernel G H h)) H"
-by (simp add: iso_def FactGroup_hom FactGroup_inj_on bij_betw_def 
-              FactGroup_onto) 
+by (simp add: iso_def FactGroup_hom FactGroup_inj_on bij_betw_def
+              FactGroup_onto)
 
 corollary (in group_hom) FactGroup_iso :
   "h ` carrier G = carrier H
@@ -1137,7 +1121,7 @@
                  \<forall>ya\<in>carrier (K Mod N).  x \<times> y = xa \<times> ya \<longrightarrow> x = xa \<and> y = ya)"
     unfolding  FactGroup_def using times_eq_iff subgroup.rcosets_non_empty
     by (metis assms(2) assms(3) normal_def partial_object.select_convs(1))
-  moreover have "(\<lambda>(X, Y). X \<times> Y) ` (carrier (G Mod H) \<times> carrier (K Mod N)) = 
+  moreover have "(\<lambda>(X, Y). X \<times> Y) ` (carrier (G Mod H) \<times> carrier (K Mod N)) =
                                      carrier (G \<times>\<times> K Mod H \<times> N)"
     unfolding image_def  apply auto using R apply force
     unfolding DirProd_def FactGroup_def RCOSETS_def r_coset_def by force
@@ -1168,7 +1152,7 @@
   assumes "subgroup H G"
   shows "(carrier G) <#> H = carrier G"
 proof
-  show "(carrier G)<#>H \<subseteq> carrier G" 
+  show "(carrier G)<#>H \<subseteq> carrier G"
     unfolding set_mult_def using subgroup.subset assms by blast
 next
   have " (carrier G) #>  \<one> = carrier G" unfolding set_mult_def r_coset_def group_axioms by simp
@@ -1179,18 +1163,14 @@
 
 (*Same lemma as above, but everything is included in a subgroup*)
 lemma (in group) set_mult_subgroup_idem:
-  assumes "subgroup H G"
-    and "subgroup N (G\<lparr>carrier:=H\<rparr>)"
-  shows "H<#>N = H"
-  using group.set_mult_carrier_idem[OF subgroup_imp_group] subgroup.subset assms
-  by (metis monoid.cases_scheme order_refl partial_object.simps(1)
-      partial_object.update_convs(1) subgroup_set_mult_equality)
+  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*)
 lemma (in group) commut_normal:
-  assumes "subgroup H G"
-    and "N\<lhd>G"
-  shows "H<#>N = N<#>H" 
+  assumes "subgroup H G" and "N\<lhd>G"
+  shows "H<#>N = N<#>H"
 proof-
   have aux1: "{H <#> N} = {\<Union>h\<in>H. h <# N }" unfolding set_mult_def l_coset_def by auto
   also have "... = {\<Union>h\<in>H. N #> h }" using assms normal.coset_eq subgroup.mem_carrier by fastforce
@@ -1200,23 +1180,10 @@
 
 (*Same lemma as above, but everything is included in a subgroup*)
 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"
-proof-
-  have "N \<subseteq> carrier (G\<lparr>carrier := H\<rparr>)" using assms normal_imp_subgroup subgroup.subset by blast
-  hence NH : "N \<subseteq> H" by simp
-  have "K \<subseteq> carrier(G\<lparr>carrier := H\<rparr>)" using subgroup.subset assms by blast
-  hence KH : "K \<subseteq> H" by simp
-  have Egal : "K <#>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N = N <#>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> K"
-  using group.commut_normal[where ?G = "G\<lparr>carrier :=H\<rparr>", of K N,OF subgroup_imp_group[OF assms(1)]
-               assms(3) assms(2)] by auto
-  also have "... = N <#> K" using subgroup_set_mult_equality[of H N K, OF assms(1) NH KH] by auto
-  moreover have "K <#>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N = K <#> N"
-    using subgroup_set_mult_equality[of H K N, OF assms(1) KH NH] by auto
-  ultimately show "K<#>N = N<#>K" by auto
-qed
+  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
 
 
 
@@ -1226,7 +1193,7 @@
   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>)"
@@ -1243,10 +1210,10 @@
     next
       show "subgroup (H\<inter>K) G" using HK_def subgroups_Inter_pair assms by auto
     next
-      have "H1 \<subseteq> (carrier (G\<lparr>carrier:=H\<rparr>))" 
+      have "H1 \<subseteq> (carrier (G\<lparr>carrier:=H\<rparr>))"
         using  assms(3) normal_imp_subgroup subgroup.subset by blast
       also have "... \<subseteq> H" by simp
-      thus "H1K \<subseteq>H\<inter>K" 
+      thus "H1K \<subseteq>H\<inter>K"
         using H1K_def calculation by auto
     qed
     thus "subgroup H1K GHK" using GHK_def by simp
@@ -1254,7 +1221,7 @@
     show "\<And> x h. x\<in>carrier GHK \<Longrightarrow> h\<in>H1K \<Longrightarrow> x \<otimes>\<^bsub>GHK\<^esub> h \<otimes>\<^bsub>GHK\<^esub> inv\<^bsub>GHK\<^esub> x\<in> H1K"
     proof-
       have invHK: "\<lbrakk>y\<in>HK\<rbrakk> \<Longrightarrow> inv\<^bsub>GHK\<^esub> y = inv\<^bsub>GH\<^esub> y"
-        using subgroup_inv_equality assms HK_def GH_def GHK_def subgroups_Inter_pair by simp
+        using m_inv_consistent assms HK_def GH_def GHK_def subgroups_Inter_pair by simp
       have multHK : "\<lbrakk>x\<in>HK;y\<in>HK\<rbrakk> \<Longrightarrow>  x \<otimes>\<^bsub>(G\<lparr>carrier:=HK\<rparr>)\<^esub> y =  x \<otimes> y"
         using HK_def by simp
       fix x assume p: "x\<in>carrier GHK"
@@ -1263,17 +1230,17 @@
         using GHK_def HK_def by simp
       hence xHK:"x\<in>HK" using p by auto
       hence invx:"inv\<^bsub>GHK\<^esub> x = inv\<^bsub>GH\<^esub> x"
-        using invHK assms GHK_def HK_def GH_def subgroup_inv_equality subgroups_Inter_pair by simp
+        using invHK assms GHK_def HK_def GH_def m_inv_consistent subgroups_Inter_pair by simp
       have "H1\<subseteq>carrier(GH)"
         using assms GH_def normal_imp_subgroup subgroup.subset by blast
-      hence hHK:"h\<in>HK" 
+      hence hHK:"h\<in>HK"
         using p2 H1K_def HK_def GH_def by auto
       hence xhx_egal : "x \<otimes>\<^bsub>GHK\<^esub> h \<otimes>\<^bsub>GHK\<^esub> inv\<^bsub>GHK\<^esub>x =  x \<otimes>\<^bsub>GH\<^esub> h \<otimes>\<^bsub>GH\<^esub> inv\<^bsub>GH\<^esub> x"
         using invx invHK multHK GHK_def GH_def by auto
-      have xH:"x\<in>carrier(GH)" 
-        using xHK HK_def GH_def by auto 
+      have xH:"x\<in>carrier(GH)"
+        using xHK HK_def GH_def by auto
       have hH:"h\<in>carrier(GH)"
-        using hHK HK_def GH_def by auto 
+        using hHK HK_def GH_def by auto
       have  "(\<forall>x\<in>carrier (GH). \<forall>h\<in>H1.  x \<otimes>\<^bsub>GH\<^esub> h \<otimes>\<^bsub>GH\<^esub> inv\<^bsub>GH\<^esub> x \<in> H1)"
         using assms normal_invE GH_def normal.inv_op_closed2 by fastforce
       hence INCL_1 : "x \<otimes>\<^bsub>GH\<^esub> h \<otimes>\<^bsub>GH\<^esub> inv\<^bsub>GH\<^esub> x \<in> H1"
diff -r 5273df52ad83 -r fcffdcb8f506 src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Sun Jul 01 17:38:08 2018 +0200
+++ b/src/HOL/Algebra/Group.thy	Sun Jul 01 16:46:28 2018 +0100
@@ -590,12 +590,18 @@
     by (rule monoid.group_l_invI) (auto intro: l_inv mem_carrier)
 qed
 
-lemma (in group) subgroup_inv_equality:
+lemma subgroup_is_submonoid:
+  assumes "subgroup H G" shows "submonoid H G"
+  using assms by (auto intro: submonoid.intro simp add: subgroup_def)
+
+lemma (in group) subgroup_Units:
+  assumes "subgroup H G" shows "H \<subseteq> Units (G \<lparr> carrier := H \<rparr>)"
+  using group.Units[OF subgroup.subgroup_is_group[OF assms group_axioms]] by simp
+
+lemma (in group) m_inv_consistent:
   assumes "subgroup H G" "x \<in> H"
-  shows "m_inv (G \<lparr>carrier := H\<rparr>) x = inv x"
-  unfolding m_inv_def apply auto
-  using subgroup.m_inv_closed[OF assms] inv_equality
-  by (metis (no_types, hide_lams) assms subgroup.mem_carrier)
+  shows "inv\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> x = inv x"
+  using assms m_inv_monoid_consistent[OF _ subgroup_is_submonoid] subgroup_Units[of H] by auto
 
 lemma (in group) int_pow_consistent: (* by Paulo *)
   assumes "subgroup H G" "x \<in> H"
@@ -616,7 +622,7 @@
   also have " ... = (inv x) [^] (nat (- n))"
     by (metis assms nat_pow_inv subgroup.mem_carrier)
   also have " ... = (inv\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> x) [^]\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> (nat (- n))"
-    using subgroup_inv_equality[OF assms] nat_pow_consistent by auto
+    using m_inv_consistent[OF assms] nat_pow_consistent by auto
   also have " ... = inv\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> (x [^]\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> (nat (- n)))"
     using group.nat_pow_inv[OF subgroup.subgroup_is_group[OF assms(1) is_group]] assms(2) by auto
   also have " ... = x [^]\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> n"
@@ -1290,18 +1296,16 @@
   thus  "I \<subseteq> carrier G \<and> (\<forall>x y. x \<in> I \<longrightarrow> y \<in> I \<longrightarrow> x \<otimes> y \<in> I)"  using H by blast
   have K: "\<one> \<in> I" using assms(2) by (auto simp add: subgroup_def)
   have "(\<And>x. x \<in> I \<Longrightarrow> inv x \<in> I)" using assms  subgroup.m_inv_closed H
-    by (metis H1 H2  subgroup_inv_equality subsetCE)
+    by (metis H1 H2 m_inv_consistent subsetCE)
   thus "\<one> \<in> I \<and> (\<forall>x. x \<in> I \<longrightarrow> inv x \<in> I)" using K by blast
 qed
 
 (*A subgroup included in another subgroup is a subgroup of the subgroup*)
 lemma (in group) subgroup_incl:
-  assumes "subgroup I G"
-    and "subgroup J G"
-    and "I\<subseteq>J"
-  shows "subgroup I (G\<lparr>carrier:=J\<rparr>)"using assms subgroup_inv_equality
-  by (auto simp add: subgroup_def)
-
+  assumes "subgroup I G" and "subgroup J G" and "I \<subseteq> J"
+  shows "subgroup I (G \<lparr> carrier := J \<rparr>)"
+  using group.group_incl_imp_subgroup[of "G \<lparr> carrier := J \<rparr>" I]
+        assms(1-2)[THEN subgroup.subgroup_is_group[OF _ group_axioms]] assms(3) by auto
 
 
 subsection \<open>The Lattice of Subgroups of a Group\<close>
@@ -1433,7 +1437,7 @@
 lemma units_of_one: "one (units_of G) = one G"
   by (auto simp: units_of_def)
 
-lemma (in monoid) units_of_inv: 
+lemma (in monoid) units_of_inv:
   assumes "x \<in> Units G"
   shows "m_inv (units_of G) x = m_inv G x"
   by (simp add: assms group.inv_equality units_group units_of_carrier units_of_mult units_of_one)
diff -r 5273df52ad83 -r fcffdcb8f506 src/HOL/Algebra/Zassenhaus.thy
--- a/src/HOL/Algebra/Zassenhaus.thy	Sun Jul 01 17:38:08 2018 +0200
+++ b/src/HOL/Algebra/Zassenhaus.thy	Sun Jul 01 16:46:28 2018 +0100
@@ -43,7 +43,7 @@
     ultimately have "x \<otimes>\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> h = x \<otimes> h" by simp
     moreover have " inv\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> x =  inv x"
       using xnormalizer
-      by (simp add: assms normalizer_imp_subgroup subgroup.subset subgroup_inv_equality)
+      by (simp add: assms normalizer_imp_subgroup subgroup.subset m_inv_consistent)
     ultimately  have xhxegal: "x \<otimes>\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> h
                 \<otimes>\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> inv\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> x
                   = x \<otimes>h \<otimes> inv x"
@@ -172,7 +172,7 @@
   also have "... \<subseteq> K" by simp
   finally have Incl2:"N \<subseteq> K" by simp
   have "(N <#>\<^bsub>G\<lparr>carrier := K\<rparr>\<^esub> H) = (N <#> H)"
-    using subgroup_set_mult_equality[of K] assms Incl1 Incl2 by simp
+    using set_mult_consistent by simp
   thus "subgroup (N<#>H) (G\<lparr>carrier:=K\<rparr>)" using Hyp by auto
 qed
 
@@ -332,8 +332,7 @@
          G\<lparr>carrier := normalizer G N, carrier := H\<rparr> Mod N \<inter> H =
           (G\<lparr>carrier:= N<#>H\<rparr> Mod N)  \<cong>
          G\<lparr>carrier := normalizer G N, carrier := H\<rparr> Mod N \<inter> H"
-    using subgroup_set_mult_equality[OF  normalizer_imp_subgroup[OF subgroup.subset[OF assms(2)]], of N H]
-          subgroup.subset[OF assms(3)]
+    using subgroup.subset[OF assms(3)]
           subgroup.subset[OF normal_imp_subgroup[OF subgroup_in_normalizer[OF assms(2)]]]
     by simp
   ultimately have "G\<lparr>carrier := normalizer G N,
@@ -493,7 +492,7 @@
     hence allG : "h1 \<in> carrier G" "hk \<in> carrier G" "x \<in> carrier G"
       using assms subgroup.subset h1hk_def normal_imp_subgroup incl_subgroup apply blast+.
     hence "x <#\<^bsub>G\<lparr>carrier := H1 <#> H\<inter>K\<rparr>\<^esub> (H1 <#> H\<inter>K1) =h1 \<otimes> hk <# (H1 <#> H\<inter>K1)"
-      using subgroup_set_mult_equality subgroup.subset xH h1hk_def by (simp add: l_coset_def)
+      using subgroup.subset xH h1hk_def by (simp add: l_coset_def)
     also have "... = h1 <# (hk <# (H1 <#> H\<inter>K1))"
       using lcos_m_assoc[OF subgroup.subset[OF incl_subgroup[OF assms(1) subH1]]allG(1)allG(2)]
       by (metis allG(1) allG(2) assms(1) incl_subgroup lcos_m_assoc subH2 subgroup.subset)
@@ -535,7 +534,7 @@
     finally have eq1 : "x <#\<^bsub>G\<lparr>carrier := H1 <#> H \<inter> K\<rparr>\<^esub> (H1 <#> H \<inter> K1) = H1 <#> (H \<inter> K1) #> hk"
       by (simp add: allG(2) all_inclG inf.coboundedI2 setmult_rcos_assoc)
     have "H1 <#> H \<inter> K1 #>\<^bsub>G\<lparr>carrier := H1 <#> H \<inter> K\<rparr>\<^esub> x = H1 <#> H \<inter> K1 #> (h1 \<otimes> hk)"
-      using subgroup_set_mult_equality subgroup.subset xH h1hk_def by (simp add: r_coset_def)
+      using subgroup.subset xH h1hk_def by (simp add: r_coset_def)
     also have "... = H1 <#> H \<inter> K1 #> h1 #> hk"
       using coset_mult_assoc by (simp add: allG all_inclG inf.coboundedI2 setmult_subset_G)
     also have"... =  H \<inter> K1 <#> H1 #> h1 #> hk"