# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1528982618 -3600
# Node ID c183a6a69f2d0a69ff907b3d64478d661e820991
# Parent  ff61cbfb3f2d185b0de85a5629d222f9ab547085
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories

diff -r ff61cbfb3f2d -r c183a6a69f2d src/HOL/Algebra/Coset.thy
--- a/src/HOL/Algebra/Coset.thy	Tue Jun 12 16:09:12 2018 +0100
+++ b/src/HOL/Algebra/Coset.thy	Thu Jun 14 14:23:38 2018 +0100
@@ -1,7 +1,6 @@
 (*  Title:      HOL/Algebra/Coset.thy
-    Author:     Florian Kammueller
-    Author:     L C Paulson
-    Author:     Stephan Hohe
+    Authors:     Florian Kammueller, L C Paulson, Stephan Hohe
+With additional contributions from Martin Baillon and Paulo Emílio de Vilhena.
 *)
 
 theory Coset
@@ -106,10 +105,9 @@
   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)
 
-(* ************************************************************************** *)
                                  
 
-subsection \<open>Basic Properties of set_mult\<close>
+subsection \<open>Basic Properties of set multiplication\<close>
 
 lemma (in group) setmult_subset_G:
   assumes "H \<subseteq> carrier G" "K \<subseteq> carrier G"
@@ -121,9 +119,7 @@
   shows "H <#> K \<subseteq> carrier G"
   using assms by (auto simp add: set_mult_def subsetD)
 
-(* ************************************************************************** *)
-(* Next lemma contributed by Martin Baillon.                                  *)
-
+(* Next lemma contributed by Martin Baillon.*)
 lemma (in group) set_mult_assoc:
   assumes "M \<subseteq> carrier G" "H \<subseteq> carrier G" "K \<subseteq> carrier G"
   shows "(M <#> H) <#> K = M <#> (H <#> K)"
@@ -151,7 +147,6 @@
   qed
 qed
 
-(* ************************************************************************** *)
 
 
 subsection \<open>Basic Properties of Cosets\<close>
@@ -1087,7 +1082,6 @@
 
 subsection \<open>Theorems about Factor Groups and Direct product\<close>
 
-
 lemma (in group) DirProd_normal :
   assumes "group K"
     and "H \<lhd> G"
@@ -1158,5 +1152,148 @@
         DirProd_group[OF normal.factorgroup_is_group normal.factorgroup_is_group]
   by blast
 
+subsubsection "More Lemmas about set multiplication"
+
+(*A group multiplied by a subgroup stays the same*)
+lemma (in group) set_mult_carrier_idem:
+  assumes "subgroup H G"
+  shows "(carrier G) <#> H = carrier G"
+proof
+  show "(carrier G)<#>H \<subseteq> carrier G" 
+    unfolding set_mult_def using subgroup_imp_subset assms by blast
+next
+  have " (carrier G) #>  \<one> = carrier G" unfolding set_mult_def r_coset_def group_axioms by simp
+  moreover have "(carrier G) #>  \<one> \<subseteq> (carrier G) <#> H" unfolding set_mult_def r_coset_def
+    using assms subgroup.one_closed[OF assms] by blast
+  ultimately show "carrier G \<subseteq> (carrier G) <#> H" by simp
+qed
+
+(*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_imp_subset assms
+  by (metis monoid.cases_scheme order_refl partial_object.simps(1)
+      partial_object.update_convs(1) subgroup_set_mult_equality)
+
+(*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" 
+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
+  moreover have aux2: "{N <#> H} = {\<Union>h\<in>H. N #> h }"unfolding set_mult_def r_coset_def by auto
+  ultimately show "H<#>N = N<#>H" by simp
+qed
+
+(*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_imp_subset by blast
+  hence NH : "N \<subseteq> H" by simp
+  have "K \<subseteq> carrier(G\<lparr>carrier := H\<rparr>)" using subgroup_imp_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
+
+
+
+subsubsection "Lemmas about intersection and normal subgroups"
+
+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>)" 
+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>)"
+  show "H1K\<lhd>GHK"
+  proof (intro group.normal_invI[of GHK H1K])
+    show "Group.group GHK"
+      using GHK_def subgroups_Inter_pair subgroup_imp_group assms by blast
+
+  next
+    have  H1K_incl:"subgroup H1K (G\<lparr>carrier:= (H\<inter>K)\<rparr>)"
+    proof(intro subgroup_incl)
+      show "subgroup H1K G"
+        using assms normal_imp_subgroup subgroups_Inter_pair incl_subgroup H1K_def by blast
+    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>))" 
+        using  assms(3) normal_imp_subgroup subgroup_imp_subset by blast
+      also have "... \<subseteq> H" by simp
+      thus "H1K \<subseteq>H\<inter>K" 
+        using H1K_def calculation by auto
+    qed
+    thus "subgroup H1K GHK" using GHK_def by simp
+  next
+    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
+      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"
+      fix h assume p2 : "h:H1K"
+      have "carrier(GHK)\<subseteq>HK"
+        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
+      have "H1\<subseteq>carrier(GH)"
+        using assms GH_def normal_imp_subgroup subgroup_imp_subset by blast
+      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 hH:"h\<in>carrier(GH)"
+        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"
+        using  xH H1K_def p2 by blast
+      have " x \<otimes>\<^bsub>GH\<^esub> h \<otimes>\<^bsub>GH\<^esub> inv\<^bsub>GH\<^esub> x \<in> HK"
+        using assms HK_def subgroups_Inter_pair hHK xHK
+        by (metis GH_def inf.cobounded1 subgroup_def subgroup_incl)
+      hence " x \<otimes>\<^bsub>GH\<^esub> h \<otimes>\<^bsub>GH\<^esub> inv\<^bsub>GH\<^esub> x \<in> K" using HK_def by simp
+      hence " x \<otimes>\<^bsub>GH\<^esub> h \<otimes>\<^bsub>GH\<^esub> inv\<^bsub>GH\<^esub> x \<in> H1K" using INCL_1 H1K_def by auto
+      thus  "x \<otimes>\<^bsub>GHK\<^esub> h \<otimes>\<^bsub>GHK\<^esub> inv\<^bsub>GHK\<^esub> x \<in> H1K" using xhx_egal by simp
+    qed
+  qed
+qed
+
+
+lemma (in group) normal_inter_subgroup:
+  assumes "subgroup H G"
+    and "N \<lhd> G"
+  shows "(N\<inter>H) \<lhd> (G\<lparr>carrier := H\<rparr>)"
+proof -
+  define K where "K = carrier G"
+  have "G\<lparr>carrier := K\<rparr> =  G" using K_def by auto
+  moreover have "subgroup K G" using K_def subgroup_self by blast
+  moreover have "normal N (G \<lparr>carrier :=K\<rparr>)" using assms K_def by simp
+  ultimately have "N \<inter> H \<lhd> G\<lparr>carrier := K \<inter> H\<rparr>"
+    using normal_inter[of K H N] assms(1) by blast
+  moreover have "K \<inter> H = H" using K_def assms subgroup_imp_subset by blast
+  ultimately show "normal (N\<inter>H) (G\<lparr>carrier := H\<rparr>)" by auto
+qed
+
 
 end
diff -r ff61cbfb3f2d -r c183a6a69f2d src/HOL/Algebra/FiniteProduct.thy
--- a/src/HOL/Algebra/FiniteProduct.thy	Tue Jun 12 16:09:12 2018 +0100
+++ b/src/HOL/Algebra/FiniteProduct.thy	Thu Jun 14 14:23:38 2018 +0100
@@ -524,4 +524,49 @@
 
 end
 
+(* Jeremy Avigad. This should be generalized to arbitrary groups, not just commutative
+   ones, using Lagrange's theorem. *)
+
+lemma (in comm_group) power_order_eq_one:
+  assumes fin [simp]: "finite (carrier G)"
+    and a [simp]: "a \<in> carrier G"
+  shows "a [^] card(carrier G) = one G"
+proof -
+  have "(\<Otimes>x\<in>carrier G. x) = (\<Otimes>x\<in>carrier G. a \<otimes> x)"
+    by (subst (2) finprod_reindex [symmetric],
+      auto simp add: Pi_def inj_on_const_mult surj_const_mult)
+  also have "\<dots> = (\<Otimes>x\<in>carrier G. a) \<otimes> (\<Otimes>x\<in>carrier G. x)"
+    by (auto simp add: finprod_multf Pi_def)
+  also have "(\<Otimes>x\<in>carrier G. a) = a [^] card(carrier G)"
+    by (auto simp add: finprod_const)
+  finally show ?thesis
+(* uses the preceeding lemma *)
+    by auto
+qed
+
+
+lemma (in comm_monoid) finprod_UN_disjoint:
+  "finite I \<Longrightarrow> (\<forall>i\<in>I. finite (A i)) \<longrightarrow> (\<forall>i\<in>I. \<forall>j\<in>I. i \<noteq> j \<longrightarrow> A i \<inter> A j = {}) \<longrightarrow>
+    (\<forall>i\<in>I. \<forall>x \<in> A i. g x \<in> carrier G) \<longrightarrow>
+    finprod G g (UNION I A) = finprod G (\<lambda>i. finprod G g (A i)) I"
+  apply (induct set: finite)
+   apply force
+  apply clarsimp
+  apply (subst finprod_Un_disjoint)
+       apply blast
+      apply (erule finite_UN_I)
+      apply blast
+     apply (fastforce)
+    apply (auto intro!: funcsetI finprod_closed)
+  done
+
+lemma (in comm_monoid) finprod_Union_disjoint:
+  "finite C \<Longrightarrow>
+    \<forall>A\<in>C. finite A \<and> (\<forall>x\<in>A. f x \<in> carrier G) \<Longrightarrow>
+    \<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A \<inter> B = {} \<Longrightarrow>
+    finprod G f (\<Union>C) = finprod G (finprod G f) C"
+  apply (frule finprod_UN_disjoint [of C id f])
+  apply auto
+  done
+
 end
diff -r ff61cbfb3f2d -r c183a6a69f2d src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Tue Jun 12 16:09:12 2018 +0100
+++ b/src/HOL/Algebra/Group.thy	Thu Jun 14 14:23:38 2018 +0100
@@ -2,6 +2,7 @@
     Author:     Clemens Ballarin, started 4 February 2003
 
 Based on work by Florian Kammueller, L C Paulson and Markus Wenzel.
+With additional contributions from Martin Baillon and Paulo Emílio de Vilhena.
 *)
 
 theory Group
@@ -52,7 +53,7 @@
   assumes m_closed [intro, simp]:
          "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk> \<Longrightarrow> x \<otimes> 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 \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
       and one_closed [intro, simp]: "\<one> \<in> carrier G"
       and l_one [simp]: "x \<in> carrier G \<Longrightarrow> \<one> \<otimes> x = x"
@@ -104,13 +105,7 @@
   moreover from x y xinv yinv have "x \<otimes> (y \<otimes> y') \<otimes> x' = \<one>" by simp
   moreover note x y
   ultimately show ?thesis unfolding Units_def
-    \<comment> \<open>Must avoid premature use of \<open>hyp_subst_tac\<close>.\<close>
-    apply (rule_tac CollectI)
-    apply (rule)
-    apply (fast)
-    apply (rule bexI [where x = "y' \<otimes> x'"])
-    apply (auto simp: m_assoc)
-    done
+    by simp (metis m_assoc m_closed)
 qed
 
 lemma (in monoid) Units_one_closed [intro, simp]:
@@ -146,6 +141,10 @@
    apply (fast intro: inv_unique, fast)
   done
 
+lemma (in monoid) inv_one [simp]:
+  "inv \<one> = \<one>"
+  by (metis Units_one_closed Units_r_inv l_one monoid.Units_inv_closed monoid_axioms)
+
 lemma (in monoid) Units_inv_Units [intro, simp]:
   "x \<in> Units G ==> inv x \<in> Units G"
 proof -
@@ -223,12 +222,12 @@
 
 lemma (in monoid) nat_pow_comm:
   "x \<in> carrier G \<Longrightarrow> (x [^] (n::nat)) \<otimes> (x [^] (m :: nat)) = (x [^] m) \<otimes> (x [^] n)"
-  using nat_pow_mult[of x n m] nat_pow_mult[of x m n] by (simp add: add.commute) 
+  using nat_pow_mult[of x n m] nat_pow_mult[of x m n] by (simp add: add.commute)
 
 lemma (in monoid) nat_pow_Suc2:
   "x \<in> carrier G \<Longrightarrow> x [^] (Suc n) = x \<otimes> (x [^] n)"
   using nat_pow_mult[of x 1 n] Suc_eq_plus1[of n]
-  by (metis One_nat_def Suc_eq_plus1_left l_one nat.rec(1) nat_pow_Suc nat_pow_def) 
+  by (metis One_nat_def Suc_eq_plus1_left l_one nat.rec(1) nat_pow_Suc nat_pow_def)
 
 lemma (in monoid) nat_pow_pow:
   "x \<in> carrier G ==> (x [^] n) [^] m = x [^] (n * m::nat)"
@@ -237,7 +236,7 @@
 lemma (in monoid) nat_pow_consistent:
   "x [^] (n :: nat) = x [^]\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> n"
   unfolding nat_pow_def by simp
-  
+
 
 (* Jacobson defines submonoid here. *)
 (* Jacobson defines the order of a monoid here. *)
@@ -357,14 +356,6 @@
    (y \<otimes> x = z \<otimes> x) = (y = z)"
   by (metis inv_closed m_assoc r_inv r_one)
 
-lemma (in group) inv_one [simp]:
-  "inv \<one> = \<one>"
-proof -
-  have "inv \<one> = \<one> \<otimes> (inv \<one>)" by (simp del: r_inv Units_r_inv)
-  moreover have "... = \<one>" by simp
-  finally show ?thesis .
-qed
-
 lemma (in group) inv_inv [simp]:
   "x \<in> carrier G ==> inv (inv x) = x"
   using Units_inv_inv by simp
@@ -449,7 +440,7 @@
     using inv_mult_group[OF Suc.prems nat_pow_closed[OF Suc.prems, of i]] by simp
   also have " ... = inv (x [^] (Suc i))"
     using Suc.prems nat_pow_Suc2 by auto
-  finally show ?case . 
+  finally show ?case .
 qed
 
 lemma (in group) int_pow_inv:
@@ -578,6 +569,7 @@
   "x \<in> H \<Longrightarrow> x \<in> carrier G"
   using subset by blast
 
+(*DELETE*)
 lemma subgroup_imp_subset:
   "subgroup H G \<Longrightarrow> H \<subseteq> carrier G"
   by (rule subgroup.subset)
@@ -594,9 +586,9 @@
     done
 qed
 
-lemma (in group) m_inv_consistent:
+lemma (in group) subgroup_inv_equality:
   assumes "subgroup H G" "x \<in> H"
-  shows "inv x = inv\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> x"
+  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)
@@ -613,14 +605,14 @@
   also have " ... = x [^]\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> n"
     using group.int_pow_def2[OF subgroup.subgroup_is_group[OF assms(1) is_group]] ge by auto
   finally show ?thesis .
-next 
+next
   assume "\<not> n \<ge> 0" hence lt: "n < 0" by simp
   hence "x [^] n = inv (x [^] (nat (- n)))"
     using int_pow_def2 by auto
   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 m_inv_consistent[OF assms] nat_pow_consistent by auto
+    using subgroup_inv_equality[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"
@@ -657,7 +649,7 @@
     and "H \<noteq> {}"
     and "\<And>a. a \<in> H \<Longrightarrow> inv a \<in> H"
     and "\<And>a b. \<lbrakk>a \<in> H; b \<in> H\<rbrakk> \<Longrightarrow> a \<otimes> b \<in> H"
-  using assms subgroup_imp_subset apply blast
+  using assms subgroup.subset apply blast
   using assms subgroup_def apply auto[1]
   by (simp add: assms subgroup.m_closed subgroup.m_inv_closed)+
 
@@ -691,12 +683,12 @@
 
 lemma (in group) group_incl_imp_subgroup:
   assumes "H \<subseteq> carrier G"
-and "group (G\<lparr>carrier := H\<rparr>)"
-shows "subgroup H G"
+    and "group (G\<lparr>carrier := H\<rparr>)"
+  shows "subgroup H G"
 proof (intro submonoid_subgroupI[OF monoid_incl_imp_submonoid[OF assms(1)]])
   show "monoid (G\<lparr>carrier := H\<rparr>)" using group_def assms by blast
   have ab_eq : "\<And> a b. a \<in> H \<Longrightarrow> b \<in> H \<Longrightarrow> a \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> b = a \<otimes> b" using assms by simp
-  fix a  assume aH : "a \<in> H" 
+  fix a  assume aH : "a \<in> H"
   have " inv\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> a \<in> carrier G"
     using assms aH group.inv_closed[OF assms(2)] by auto
   moreover have "\<one>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> = \<one>" using assms monoid.one_closed ab_eq one_def by simp
@@ -710,10 +702,6 @@
   ultimately show "inv a \<in> H" by auto
 qed
 
-(*
-lemma (in monoid) Units_subgroup:
-  "subgroup (Units G) G"
-*)
 
 subsection \<open>Direct Products\<close>
 
@@ -731,7 +719,7 @@
   interpret G: monoid G by fact
   interpret H: monoid H by fact
   from assms
-  show ?thesis by (unfold monoid_def DirProd_def, auto) 
+  show ?thesis by (unfold monoid_def DirProd_def, auto)
 qed
 
 
@@ -778,16 +766,16 @@
 
 lemma DirProd_subgroups :
   assumes "group G"
-and "subgroup H G"
-and "group K"
-and "subgroup I K"
-shows "subgroup (H \<times> I) (G \<times>\<times> K)"
+    and "subgroup H G"
+    and "group K"
+    and "subgroup I K"
+  shows "subgroup (H \<times> I) (G \<times>\<times> K)"
 proof (intro group.group_incl_imp_subgroup[OF DirProd_group[OF assms(1)assms(3)]])
-  have "H \<subseteq> carrier G" "I \<subseteq> carrier K" using subgroup_imp_subset assms apply blast+.
+  have "H \<subseteq> carrier G" "I \<subseteq> carrier K" using subgroup.subset assms apply blast+.
   thus "(H \<times> I) \<subseteq> carrier (G \<times>\<times> K)" unfolding DirProd_def by auto
   have "Group.group ((G\<lparr>carrier := H\<rparr>) \<times>\<times> (K\<lparr>carrier := I\<rparr>))"
     using DirProd_group[OF subgroup.subgroup_is_group[OF assms(2)assms(1)]
-                           subgroup.subgroup_is_group[OF assms(4)assms(3)]].
+        subgroup.subgroup_is_group[OF assms(4)assms(3)]].
   moreover have "((G\<lparr>carrier := H\<rparr>) \<times>\<times> (K\<lparr>carrier := I\<rparr>)) = ((G \<times>\<times> K)\<lparr>carrier := H \<times> I\<rparr>)"
     unfolding DirProd_def using assms apply simp.
   ultimately show "Group.group ((G \<times>\<times> K)\<lparr>carrier := H \<times> I\<rparr>)" by simp
@@ -806,12 +794,12 @@
 by (fastforce simp add: hom_def compose_def)
 
 definition
-  iso :: "_ => _ => ('a => 'b) set" 
+  iso :: "_ => _ => ('a => 'b) set"
   where "iso G H = {h. h \<in> hom G H \<and> bij_betw h (carrier G) (carrier H)}"
 
 definition
   is_iso :: "_ \<Rightarrow> _ \<Rightarrow> bool" (infixr "\<cong>" 60)
-  where "G \<cong> H = (iso G H  \<noteq> {})" 
+  where "G \<cong> H = (iso G H  \<noteq> {})"
 
 lemma iso_set_refl: "(\<lambda>x. x) \<in> iso G G"
   by (simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def)
@@ -821,9 +809,9 @@
 
 lemma (in group) iso_set_sym:
      "h \<in> iso G H \<Longrightarrow> inv_into (carrier G) h \<in> (iso H G)"
-apply (simp add: iso_def bij_betw_inv_into) 
-apply (subgoal_tac "inv_into (carrier G) h \<in> carrier H \<rightarrow> carrier G") 
- prefer 2 apply (simp add: bij_betw_imp_funcset [OF bij_betw_inv_into]) 
+apply (simp add: iso_def bij_betw_inv_into)
+apply (subgoal_tac "inv_into (carrier G) h \<in> carrier H \<rightarrow> carrier G")
+ prefer 2 apply (simp add: bij_betw_imp_funcset [OF bij_betw_inv_into])
 apply (simp add: hom_def bij_betw_def inv_into_f_eq f_inv_into_f Pi_def)
 done
 
@@ -831,7 +819,7 @@
 "G \<cong> H \<Longrightarrow> H \<cong> G"
   using iso_set_sym unfolding is_iso_def by auto
 
-lemma (in group) iso_set_trans: 
+lemma (in group) iso_set_trans:
      "[|h \<in> iso G H; i \<in> iso H I|] ==> (compose (carrier G) i h) \<in> iso G I"
 by (auto simp add: iso_def hom_compose bij_betw_compose)
 
@@ -839,7 +827,7 @@
 "\<lbrakk>G \<cong> H ; H \<cong> I\<rbrakk> \<Longrightarrow> G \<cong> I"
   using iso_set_trans unfolding is_iso_def by blast
 
-(* Next four lemmas contributed by Paulo Emílio de Vilhena. *)
+(* Next four lemmas contributed by Paulo. *)
 
 lemma (in monoid) hom_imp_img_monoid:
   assumes "h \<in> hom G H"
@@ -909,7 +897,7 @@
   obtain \<phi> where phi: "\<phi> \<in> iso G H" "inv_into (carrier G) \<phi> \<in> iso H G"
     using iso_set_sym assms unfolding is_iso_def by blast
   define \<psi> where psi_def: "\<psi> = inv_into (carrier G) \<phi>"
-  
+
   from phi
   have surj: "\<phi> ` (carrier G) = (carrier H)" "\<psi> ` (carrier H) = (carrier G)"
    and inj: "inj_on \<phi> (carrier G)" "inj_on \<psi> (carrier H)"
@@ -983,7 +971,7 @@
   shows "(\<lambda>(x,y,z). (x,(y,z))) \<in> iso (G \<times>\<times> H \<times>\<times> I) (G \<times>\<times> (H \<times>\<times> I))"
 by (auto simp add: iso_def hom_def inj_on_def bij_betw_def)
 
-lemma (in group) DirProd_iso_set_trans: 
+lemma (in group) DirProd_iso_set_trans:
   assumes "g \<in> iso G G2"
     and "h \<in> iso H I"
   shows "(\<lambda>(x,y). (g x, h y)) \<in> iso (G \<times>\<times> H) (G2 \<times>\<times> I)"
@@ -1058,7 +1046,7 @@
   "x \<in> carrier G \<Longrightarrow> (([^]) x) \<in> hom \<lparr> carrier = UNIV, mult = (+), one = 0::int \<rparr> G "
   unfolding hom_def by (simp add: int_pow_mult)
 
-(* Next six lemmas contributed by Paulo Emílio de Vilhena. *)
+(* Next six lemmas contributed by Paulo. *)
 
 lemma (in group_hom) img_is_subgroup: "subgroup (h ` (carrier G)) H"
   apply (rule subgroupI)
@@ -1098,7 +1086,7 @@
   shows "group_hom (G \<lparr> carrier := H \<rparr>) G id"
   unfolding group_hom_def group_hom_axioms_def hom_def
   using subgroup.subgroup_is_group[OF assms is_group]
-        is_group subgroup_imp_subset[OF assms] by auto
+        is_group subgroup.subset[OF assms] by auto
 
 lemma (in group_hom) nat_pow_hom:
   "x \<in> carrier G \<Longrightarrow> h (x [^] (n :: nat)) = (h x) [^]\<^bsub>H\<^esub> n"
@@ -1146,7 +1134,7 @@
       "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y = y \<otimes> x"
   shows "comm_monoid G"
   using l_one
-    by (auto intro!: comm_monoid.intro comm_monoid_axioms.intro monoid.intro 
+    by (auto intro!: comm_monoid.intro comm_monoid_axioms.intro monoid.intro
              intro: assms simp: m_closed one_closed m_comm)
 
 lemma (in monoid) monoid_comm_monoidI:
@@ -1220,7 +1208,7 @@
   "[| x \<in> carrier G; y \<in> carrier G |] ==> inv (x \<otimes> y) = inv x \<otimes> inv y"
   by (simp add: m_ac inv_mult_group)
 
-(* Next three lemmas contributed by Paulo Emílio de Vilhena. *)
+(* Next three lemmas contributed by Paulo. *)
 
 lemma (in comm_monoid) hom_imp_img_comm_monoid:
   assumes "h \<in> hom G H"
@@ -1280,6 +1268,32 @@
     using comm_gr by simp
 qed
 
+(*A subgroup of a subgroup is a subgroup of the group*)
+lemma (in group) incl_subgroup:
+  assumes "subgroup J G"
+    and "subgroup I (G\<lparr>carrier:=J\<rparr>)"
+  shows "subgroup I G" unfolding subgroup_def
+proof
+  have H1: "I \<subseteq> carrier (G\<lparr>carrier:=J\<rparr>)" using assms(2) subgroup_imp_subset by blast
+  also have H2: "...\<subseteq>J" by simp
+  also  have "...\<subseteq>(carrier G)"  by (simp add: assms(1) subgroup_imp_subset)
+  finally have H: "I \<subseteq> carrier G" by simp
+  have "(\<And>x y. \<lbrakk>x \<in> I ; y \<in> I\<rbrakk> \<Longrightarrow> x \<otimes> y \<in> I)" using assms(2) by (auto simp add: subgroup_def)
+  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)
+  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)
+
 
 
 subsection \<open>The Lattice of Subgroups of a Group\<close>
@@ -1300,16 +1314,7 @@
 
 lemma (in group) is_monoid [intro, simp]:
   "monoid G"
-  by (auto intro: monoid.intro m_assoc) 
-
-lemma (in group) subgroup_inv_equality:
-  "[| subgroup H G; x \<in> H |] ==> m_inv (G \<lparr>carrier := H\<rparr>) x = inv x"
-apply (rule_tac inv_equality [THEN sym])
-  apply (rule group.l_inv [OF subgroup_imp_group, simplified], assumption+)
- apply (rule subsetD [OF subgroup.subset], assumption+)
-apply (rule subsetD [OF subgroup.subset], assumption)
-apply (rule_tac group.inv_closed [OF subgroup_imp_group, simplified], assumption+)
-done
+  by (auto intro: monoid.intro m_assoc)
 
 lemma (in group) subgroup_mult_equality:
   "\<lbrakk> subgroup H G; h1 \<in> H; h2 \<in> H \<rbrakk> \<Longrightarrow>  h1 \<otimes>\<^bsub>G \<lparr> carrier := H \<rparr>\<^esub> h2 = h1 \<otimes> h2"
@@ -1336,7 +1341,7 @@
 qed
 
 lemma (in group) subgroups_Inter_pair :
-  assumes  "subgroup I G" 
+  assumes  "subgroup I G"
     and  "subgroup J G"
   shows "subgroup (I\<inter>J) G" using subgroups_Inter[ where ?A = "{I,J}"] assms by auto
 
@@ -1378,4 +1383,90 @@
   then show "\<exists>I. greatest ?L I (Lower ?L A)" ..
 qed
 
+subsection\<open>Jeremy Avigad's @{text"More_Group"} material\<close>
+
+text \<open>
+  Show that the units in any monoid give rise to a group.
+
+  The file Residues.thy provides some infrastructure to use
+  facts about the unit group within the ring locale.
+\<close>
+
+definition units_of :: "('a, 'b) monoid_scheme \<Rightarrow> 'a monoid"
+  where "units_of G =
+    \<lparr>carrier = Units G, Group.monoid.mult = Group.monoid.mult G, one  = one G\<rparr>"
+
+lemma (in monoid) units_group: "group (units_of G)"
+  apply (unfold units_of_def)
+  apply (rule groupI)
+      apply auto
+   apply (subst m_assoc)
+      apply auto
+  apply (rule_tac x = "inv x" in bexI)
+   apply auto
+  done
+
+lemma (in comm_monoid) units_comm_group: "comm_group (units_of G)"
+  apply (rule group.group_comm_groupI)
+   apply (rule units_group)
+  apply (insert comm_monoid_axioms)
+  apply (unfold units_of_def Units_def comm_monoid_def comm_monoid_axioms_def)
+  apply auto
+  done
+
+lemma units_of_carrier: "carrier (units_of G) = Units G"
+  by (auto simp: units_of_def)
+
+lemma units_of_mult: "mult (units_of G) = mult G"
+  by (auto simp: units_of_def)
+
+lemma units_of_one: "one (units_of G) = one G"
+  by (auto simp: units_of_def)
+
+lemma (in monoid) units_of_inv: "x \<in> Units G \<Longrightarrow> m_inv (units_of G) x = m_inv G x"
+  apply (rule sym)
+  apply (subst m_inv_def)
+  apply (rule the1_equality)
+   apply (rule ex_ex1I)
+    apply (subst (asm) Units_def)
+    apply auto
+     apply (erule inv_unique)
+        apply auto
+    apply (rule Units_closed)
+    apply (simp_all only: units_of_carrier [symmetric])
+    apply (insert units_group)
+    apply auto
+   apply (subst units_of_mult [symmetric])
+   apply (subst units_of_one [symmetric])
+   apply (erule group.r_inv, assumption)
+  apply (subst units_of_mult [symmetric])
+  apply (subst units_of_one [symmetric])
+  apply (erule group.l_inv, assumption)
+  done
+
+lemma (in group) inj_on_const_mult: "a \<in> carrier G \<Longrightarrow> inj_on (\<lambda>x. a \<otimes> x) (carrier G)"
+  unfolding inj_on_def by auto
+
+lemma (in group) surj_const_mult: "a \<in> carrier G \<Longrightarrow> (\<lambda>x. a \<otimes> x) ` carrier G = carrier G"
+  apply (auto simp add: image_def)
+  apply (rule_tac x = "(m_inv G a) \<otimes> x" in bexI)
+  apply auto
+(* auto should get this. I suppose we need "comm_monoid_simprules"
+   for ac_simps rewriting. *)
+  apply (subst m_assoc [symmetric])
+  apply auto
+  done
+
+lemma (in group) l_cancel_one [simp]: "x \<in> carrier G \<Longrightarrow> a \<in> carrier G \<Longrightarrow> x \<otimes> a = x \<longleftrightarrow> a = one G"
+  by (metis Units_eq Units_l_cancel monoid.r_one monoid_axioms one_closed)
+
+lemma (in group) r_cancel_one [simp]: "x \<in> carrier G \<Longrightarrow> a \<in> carrier G \<Longrightarrow> a \<otimes> x = x \<longleftrightarrow> a = one G"
+  by (metis monoid.l_one monoid_axioms one_closed right_cancel)
+
+lemma (in group) l_cancel_one' [simp]: "x \<in> carrier G \<Longrightarrow> a \<in> carrier G \<Longrightarrow> x = x \<otimes> a \<longleftrightarrow> a = one G"
+  using l_cancel_one by fastforce
+
+lemma (in group) r_cancel_one' [simp]: "x \<in> carrier G \<Longrightarrow> a \<in> carrier G \<Longrightarrow> x = a \<otimes> x \<longleftrightarrow> a = one G"
+  using r_cancel_one by fastforce
+
 end
diff -r ff61cbfb3f2d -r c183a6a69f2d src/HOL/Algebra/Group_Action.thy
--- a/src/HOL/Algebra/Group_Action.thy	Tue Jun 12 16:09:12 2018 +0100
+++ b/src/HOL/Algebra/Group_Action.thy	Thu Jun 14 14:23:38 2018 +0100
@@ -1,7 +1,5 @@
-(* ************************************************************************** *)
 (* Title:      Group_Action.thy                                               *)
 (* Author:     Paulo Emílio de Vilhena                                        *)
-(* ************************************************************************** *)
 
 theory Group_Action
 imports Bij Coset Congruence
@@ -313,7 +311,7 @@
 
 text \<open>In this subsection, we prove the Orbit-Stabilizer theorem.
       Our approach is to show the existence of a bijection between
-      "rcosets (stabilizer G \<phi> x)" and "orbit G \<phi> x". Then we use
+      "rcosets (stabilizer G phi x)" and "orbit G phi x". Then we use
       Lagrange's theorem to find the cardinal of the first set.\<close>
 
 subsubsection \<open>Rcosets - Supporting Lemmas\<close>
@@ -766,11 +764,11 @@
   unfolding bij_betw_def
 proof
   show "inj_on ?\<phi> {H. subgroup H G}"
-    using subgroup_conjugation_is_inj assms inj_on_def subgroup_imp_subset
+    using subgroup_conjugation_is_inj assms inj_on_def subgroup.subset
     by (metis (mono_tags, lifting) inj_on_restrict_eq mem_Collect_eq)
 next
   have "\<And>H. H \<in> {H. subgroup H G} \<Longrightarrow> ?\<phi> ((inv g) <# H #> g) = H"
-    by (simp add: assms subgroup_imp_subset subgroup_conjugation_is_surj0
+    by (simp add: assms subgroup.subset subgroup_conjugation_is_surj0
                   subgroup_conjugation_is_surj1 is_group)
   hence "\<And>H. H \<in> {H. subgroup H G} \<Longrightarrow> \<exists>H' \<in> {H. subgroup H G}. ?\<phi> H' = H"
     using assms subgroup_conjugation_is_surj1 by fastforce
@@ -800,11 +798,11 @@
       by (simp add: H g2 subgroup_conjugation_is_surj2)
     also have " ... = g1 <# (g2 <# H) #> ((inv g2) \<otimes> (inv g1))"
       by (simp add: H coset_mult_assoc g1 g2 group.coset_assoc
-                    is_group l_coset_subset_G subgroup_imp_subset)
+                    is_group l_coset_subset_G subgroup.subset)
     also have " ... = g1 <# (g2 <# H) #> inv (g1 \<otimes> g2)"
       using g1 g2 by (simp add: inv_mult_group)
     finally have "(?\<phi> g1) ((?\<phi> g2) H) = ?\<psi> (g1 \<otimes> g2) H"
-      by (simp add: H g1 g2 lcos_m_assoc subgroup_imp_subset)
+      by (simp add: H g1 g2 lcos_m_assoc subgroup.subset)
     thus "?\<psi> (g1 \<otimes> g2) H = (?\<phi> g1) ((?\<phi> g2) H)" by auto
   qed
   hence "\<And> g1 g2. \<lbrakk> g1 \<in> carrier G; g2 \<in> carrier G \<rbrakk> \<Longrightarrow>
diff -r ff61cbfb3f2d -r c183a6a69f2d src/HOL/Algebra/Ideal.thy
--- a/src/HOL/Algebra/Ideal.thy	Tue Jun 12 16:09:12 2018 +0100
+++ b/src/HOL/Algebra/Ideal.thy	Thu Jun 14 14:23:38 2018 +0100
@@ -14,7 +14,7 @@
 
 locale ideal = additive_subgroup I R + ring R for I and R (structure) +
   assumes I_l_closed: "\<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> x \<otimes> a \<in> I"
-    and I_r_closed: "\<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> a \<otimes> x \<in> I"
+      and I_r_closed: "\<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> a \<otimes> x \<in> I"
 
 sublocale ideal \<subseteq> abelian_subgroup I R
   apply (intro abelian_subgroupI3 abelian_group.intro)
@@ -74,7 +74,7 @@
 
 locale maximalideal = ideal +
   assumes I_notcarr: "carrier R \<noteq> I"
-    and I_maximal: "\<lbrakk>ideal J R; I \<subseteq> J; J \<subseteq> carrier R\<rbrakk> \<Longrightarrow> J = I \<or> J = carrier R"
+    and I_maximal: "\<lbrakk>ideal J R; I \<subseteq> J; J \<subseteq> carrier R\<rbrakk> \<Longrightarrow> (J = I) \<or> (J = carrier R)"
 
 lemma (in maximalideal) is_maximalideal: "maximalideal I R"
   by (rule maximalideal_axioms)
@@ -83,7 +83,7 @@
   fixes R
   assumes "ideal I R"
     and I_notcarr: "carrier R \<noteq> I"
-    and I_maximal: "\<And>J. \<lbrakk>ideal J R; I \<subseteq> J; J \<subseteq> carrier R\<rbrakk> \<Longrightarrow> J = I \<or> J = carrier R"
+    and I_maximal: "\<And>J. \<lbrakk>ideal J R; I \<subseteq> J; J \<subseteq> carrier R\<rbrakk> \<Longrightarrow> (J = I) \<or> (J = carrier R)"
   shows "maximalideal I R"
 proof -
   interpret ideal I R by fact
@@ -143,26 +143,17 @@
 subsection \<open>Special Ideals\<close>
 
 lemma (in ring) zeroideal: "ideal {\<zero>} R"
-  apply (intro idealI subgroup.intro)
-        apply (rule is_ring)
-       apply simp+
-    apply (fold a_inv_def, simp)
-   apply simp+
-  done
+  by (intro idealI subgroup.intro) (simp_all add: is_ring)
 
 lemma (in ring) oneideal: "ideal (carrier R) R"
   by (rule idealI) (auto intro: is_ring add.subgroupI)
 
 lemma (in "domain") zeroprimeideal: "primeideal {\<zero>} R"
-  apply (intro primeidealI)
-     apply (rule zeroideal)
-    apply (rule domain.axioms, rule domain_axioms)
-   defer 1
-   apply (simp add: integral)
-proof (rule ccontr, simp)
-  assume "carrier R = {\<zero>}"
-  then have "\<one> = \<zero>" by (rule one_zeroI)
-  with one_not_zero show False by simp
+proof -
+  have "carrier R \<noteq> {\<zero>}"
+    by (simp add: carrier_one_not_zero)
+  then show ?thesis
+    by (metis (no_types, lifting) domain_axioms domain_def integral primeidealI singleton_iff zeroideal)
 qed
 
 
@@ -651,6 +642,46 @@
 qed
 
 
+(* Next lemma contributed by Paulo Emílio de Vilhena. *)
+
+text \<open>This next lemma would be trivial if placed in a theory that imports QuotRing,
+      but it makes more sense to have it here (easier to find and coherent with the
+      previous developments).\<close>
+
+lemma (in cring) cgenideal_prod:
+  assumes "a \<in> carrier R" "b \<in> carrier R"
+  shows "(PIdl a) <#> (PIdl b) = PIdl (a \<otimes> b)"
+proof -
+  have "(carrier R #> a) <#> (carrier R #> b) = carrier R #> (a \<otimes> b)"
+  proof
+    show "(carrier R #> a) <#> (carrier R #> b) \<subseteq> carrier R #> a \<otimes> b"
+    proof
+      fix x assume "x \<in> (carrier R #> a) <#> (carrier R #> b)"
+      then obtain r1 r2 where r1: "r1 \<in> carrier R" and r2: "r2 \<in> carrier R"
+                          and "x = (r1 \<otimes> a) \<otimes> (r2 \<otimes> b)"
+        unfolding set_mult_def r_coset_def by blast
+      hence "x = (r1 \<otimes> r2) \<otimes> (a \<otimes> b)"
+        by (simp add: assms local.ring_axioms m_lcomm ring.ring_simprules(11))
+      thus "x \<in> carrier R #> a \<otimes> b"
+        unfolding r_coset_def using r1 r2 assms by blast 
+    qed
+  next
+    show "carrier R #> a \<otimes> b \<subseteq> (carrier R #> a) <#> (carrier R #> b)"
+    proof
+      fix x assume "x \<in> carrier R #> a \<otimes> b"
+      then obtain r where r: "r \<in> carrier R" "x = r \<otimes> (a \<otimes> b)"
+        unfolding r_coset_def by blast
+      hence "x = (r \<otimes> a) \<otimes> (\<one> \<otimes> b)"
+        using assms by (simp add: m_assoc)
+      thus "x \<in> (carrier R #> a) <#> (carrier R #> b)"
+        unfolding set_mult_def r_coset_def using assms r by blast
+    qed
+  qed
+  thus ?thesis
+    using cgenideal_eq_rcos[of a] cgenideal_eq_rcos[of b] cgenideal_eq_rcos[of "a \<otimes> b"] by simp
+qed
+
+
 subsection \<open>Prime Ideals\<close>
 
 lemma (in ideal) primeidealCD:
@@ -918,7 +949,7 @@
   qed
 qed (simp add: zeroideal oneideal)
 
-\<comment> \<open>Jacobson Theorem 2.2\<close>
+\<comment>\<open>"Jacobson Theorem 2.2"\<close>
 lemma (in cring) trivialideals_eq_field:
   assumes carrnzero: "carrier R \<noteq> {\<zero>}"
   shows "({I. ideal I R} = {{\<zero>}, carrier R}) = field R"
diff -r ff61cbfb3f2d -r c183a6a69f2d src/HOL/Algebra/More_Finite_Product.thy
--- a/src/HOL/Algebra/More_Finite_Product.thy	Tue Jun 12 16:09:12 2018 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,102 +0,0 @@
-(*  Title:      HOL/Algebra/More_Finite_Product.thy
-    Author:     Jeremy Avigad
-*)
-
-section \<open>More on finite products\<close>
-
-theory More_Finite_Product
-  imports More_Group
-begin
-
-lemma (in comm_monoid) finprod_UN_disjoint:
-  "finite I \<Longrightarrow> (\<forall>i\<in>I. finite (A i)) \<longrightarrow> (\<forall>i\<in>I. \<forall>j\<in>I. i \<noteq> j \<longrightarrow> A i \<inter> A j = {}) \<longrightarrow>
-    (\<forall>i\<in>I. \<forall>x \<in> A i. g x \<in> carrier G) \<longrightarrow>
-    finprod G g (UNION I A) = finprod G (\<lambda>i. finprod G g (A i)) I"
-  apply (induct set: finite)
-   apply force
-  apply clarsimp
-  apply (subst finprod_Un_disjoint)
-       apply blast
-      apply (erule finite_UN_I)
-      apply blast
-     apply (fastforce)
-    apply (auto intro!: funcsetI finprod_closed)
-  done
-
-lemma (in comm_monoid) finprod_Union_disjoint:
-  "finite C \<Longrightarrow>
-    \<forall>A\<in>C. finite A \<and> (\<forall>x\<in>A. f x \<in> carrier G) \<Longrightarrow>
-    \<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A \<inter> B = {} \<Longrightarrow>
-    finprod G f (\<Union>C) = finprod G (finprod G f) C"
-  apply (frule finprod_UN_disjoint [of C id f])
-  apply auto
-  done
-
-lemma (in comm_monoid) finprod_one: "finite A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x = \<one>) \<Longrightarrow> finprod G f A = \<one>"
-  by (induct set: finite) auto
-
-
-(* need better simplification rules for rings *)
-(* the next one holds more generally for abelian groups *)
-
-lemma (in cring) sum_zero_eq_neg: "x \<in> carrier R \<Longrightarrow> y \<in> carrier R \<Longrightarrow> x \<oplus> y = \<zero> \<Longrightarrow> x = \<ominus> y"
-  by (metis minus_equality)
-
-lemma (in domain) square_eq_one:
-  fixes x
-  assumes [simp]: "x \<in> carrier R"
-    and "x \<otimes> x = \<one>"
-  shows "x = \<one> \<or> x = \<ominus>\<one>"
-proof -
-  have "(x \<oplus> \<one>) \<otimes> (x \<oplus> \<ominus> \<one>) = x \<otimes> x \<oplus> \<ominus> \<one>"
-    by (simp add: ring_simprules)
-  also from \<open>x \<otimes> x = \<one>\<close> have "\<dots> = \<zero>"
-    by (simp add: ring_simprules)
-  finally have "(x \<oplus> \<one>) \<otimes> (x \<oplus> \<ominus> \<one>) = \<zero>" .
-  then have "(x \<oplus> \<one>) = \<zero> \<or> (x \<oplus> \<ominus> \<one>) = \<zero>"
-    by (intro integral) auto
-  then show ?thesis
-    apply auto
-     apply (erule notE)
-     apply (rule sum_zero_eq_neg)
-       apply auto
-    apply (subgoal_tac "x = \<ominus> (\<ominus> \<one>)")
-     apply (simp add: ring_simprules)
-    apply (rule sum_zero_eq_neg)
-      apply auto
-    done
-qed
-
-lemma (in domain) inv_eq_self: "x \<in> Units R \<Longrightarrow> x = inv x \<Longrightarrow> x = \<one> \<or> x = \<ominus>\<one>"
-  by (metis Units_closed Units_l_inv square_eq_one)
-
-
-text \<open>
-  The following translates theorems about groups to the facts about
-  the units of a ring. (The list should be expanded as more things are
-  needed.)
-\<close>
-
-lemma (in ring) finite_ring_finite_units [intro]: "finite (carrier R) \<Longrightarrow> finite (Units R)"
-  by (rule finite_subset) auto
-
-lemma (in monoid) units_of_pow:
-  fixes n :: nat
-  shows "x \<in> Units G \<Longrightarrow> x [^]\<^bsub>units_of G\<^esub> n = x [^]\<^bsub>G\<^esub> n"
-  apply (induct n)
-  apply (auto simp add: units_group group.is_monoid
-    monoid.nat_pow_0 monoid.nat_pow_Suc units_of_one units_of_mult)
-  done
-
-lemma (in cring) units_power_order_eq_one:
-  "finite (Units R) \<Longrightarrow> a \<in> Units R \<Longrightarrow> a [^] card(Units R) = \<one>"
-  apply (subst units_of_carrier [symmetric])
-  apply (subst units_of_one [symmetric])
-  apply (subst units_of_pow [symmetric])
-   apply assumption
-  apply (rule comm_group.power_order_eq_one)
-    apply (rule units_comm_group)
-   apply (unfold units_of_def, auto)
-  done
-
-end
diff -r ff61cbfb3f2d -r c183a6a69f2d src/HOL/Algebra/More_Group.thy
--- a/src/HOL/Algebra/More_Group.thy	Tue Jun 12 16:09:12 2018 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,115 +0,0 @@
-(*  Title:      HOL/Algebra/More_Group.thy
-    Author:     Jeremy Avigad
-*)
-
-section \<open>More on groups\<close>
-
-theory More_Group
-  imports Ring
-begin
-
-text \<open>
-  Show that the units in any monoid give rise to a group.
-
-  The file Residues.thy provides some infrastructure to use
-  facts about the unit group within the ring locale.
-\<close>
-
-definition units_of :: "('a, 'b) monoid_scheme \<Rightarrow> 'a monoid"
-  where "units_of G =
-    \<lparr>carrier = Units G, Group.monoid.mult = Group.monoid.mult G, one  = one G\<rparr>"
-
-lemma (in monoid) units_group: "group (units_of G)"
-  apply (unfold units_of_def)
-  apply (rule groupI)
-      apply auto
-   apply (subst m_assoc)
-      apply auto
-  apply (rule_tac x = "inv x" in bexI)
-   apply auto
-  done
-
-lemma (in comm_monoid) units_comm_group: "comm_group (units_of G)"
-  apply (rule group.group_comm_groupI)
-   apply (rule units_group)
-  apply (insert comm_monoid_axioms)
-  apply (unfold units_of_def Units_def comm_monoid_def comm_monoid_axioms_def)
-  apply auto
-  done
-
-lemma units_of_carrier: "carrier (units_of G) = Units G"
-  by (auto simp: units_of_def)
-
-lemma units_of_mult: "mult (units_of G) = mult G"
-  by (auto simp: units_of_def)
-
-lemma units_of_one: "one (units_of G) = one G"
-  by (auto simp: units_of_def)
-
-lemma (in monoid) units_of_inv: "x \<in> Units G \<Longrightarrow> m_inv (units_of G) x = m_inv G x"
-  apply (rule sym)
-  apply (subst m_inv_def)
-  apply (rule the1_equality)
-   apply (rule ex_ex1I)
-    apply (subst (asm) Units_def)
-    apply auto
-     apply (erule inv_unique)
-        apply auto
-    apply (rule Units_closed)
-    apply (simp_all only: units_of_carrier [symmetric])
-    apply (insert units_group)
-    apply auto
-   apply (subst units_of_mult [symmetric])
-   apply (subst units_of_one [symmetric])
-   apply (erule group.r_inv, assumption)
-  apply (subst units_of_mult [symmetric])
-  apply (subst units_of_one [symmetric])
-  apply (erule group.l_inv, assumption)
-  done
-
-lemma (in group) inj_on_const_mult: "a \<in> carrier G \<Longrightarrow> inj_on (\<lambda>x. a \<otimes> x) (carrier G)"
-  unfolding inj_on_def by auto
-
-lemma (in group) surj_const_mult: "a \<in> carrier G \<Longrightarrow> (\<lambda>x. a \<otimes> x) ` carrier G = carrier G"
-  apply (auto simp add: image_def)
-  apply (rule_tac x = "(m_inv G a) \<otimes> x" in bexI)
-  apply auto
-(* auto should get this. I suppose we need "comm_monoid_simprules"
-   for ac_simps rewriting. *)
-  apply (subst m_assoc [symmetric])
-  apply auto
-  done
-
-lemma (in group) l_cancel_one [simp]: "x \<in> carrier G \<Longrightarrow> a \<in> carrier G \<Longrightarrow> x \<otimes> a = x \<longleftrightarrow> a = one G"
-  by (metis Units_eq Units_l_cancel monoid.r_one monoid_axioms one_closed)
-
-lemma (in group) r_cancel_one [simp]: "x \<in> carrier G \<Longrightarrow> a \<in> carrier G \<Longrightarrow> a \<otimes> x = x \<longleftrightarrow> a = one G"
-  by (metis monoid.l_one monoid_axioms one_closed right_cancel)
-
-lemma (in group) l_cancel_one' [simp]: "x \<in> carrier G \<Longrightarrow> a \<in> carrier G \<Longrightarrow> x = x \<otimes> a \<longleftrightarrow> a = one G"
-  using l_cancel_one by fastforce
-
-lemma (in group) r_cancel_one' [simp]: "x \<in> carrier G \<Longrightarrow> a \<in> carrier G \<Longrightarrow> x = a \<otimes> x \<longleftrightarrow> a = one G"
-  using r_cancel_one by fastforce
-
-(* This should be generalized to arbitrary groups, not just commutative
-   ones, using Lagrange's theorem. *)
-
-lemma (in comm_group) power_order_eq_one:
-  assumes fin [simp]: "finite (carrier G)"
-    and a [simp]: "a \<in> carrier G"
-  shows "a [^] card(carrier G) = one G"
-proof -
-  have "(\<Otimes>x\<in>carrier G. x) = (\<Otimes>x\<in>carrier G. a \<otimes> x)"
-    by (subst (2) finprod_reindex [symmetric],
-      auto simp add: Pi_def inj_on_const_mult surj_const_mult)
-  also have "\<dots> = (\<Otimes>x\<in>carrier G. a) \<otimes> (\<Otimes>x\<in>carrier G. x)"
-    by (auto simp add: finprod_multf Pi_def)
-  also have "(\<Otimes>x\<in>carrier G. a) = a [^] card(carrier G)"
-    by (auto simp add: finprod_const)
-  finally show ?thesis
-(* uses the preceeding lemma *)
-    by auto
-qed
-
-end
diff -r ff61cbfb3f2d -r c183a6a69f2d src/HOL/Algebra/More_Ring.thy
--- a/src/HOL/Algebra/More_Ring.thy	Tue Jun 12 16:09:12 2018 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,74 +0,0 @@
-(*  Title:      HOL/Algebra/More_Ring.thy
-    Author:     Jeremy Avigad
-*)
-
-section \<open>More on rings etc.\<close>
-
-theory More_Ring
-  imports Ring
-begin
-
-lemma (in cring) field_intro2: "\<zero>\<^bsub>R\<^esub> \<noteq> \<one>\<^bsub>R\<^esub> \<Longrightarrow> \<forall>x \<in> carrier R - {\<zero>\<^bsub>R\<^esub>}. x \<in> Units R \<Longrightarrow> field R"
-  apply (unfold_locales)
-    apply (use cring_axioms in auto)
-   apply (rule trans)
-    apply (subgoal_tac "a = (a \<otimes> b) \<otimes> inv b")
-     apply assumption
-    apply (subst m_assoc)
-       apply auto
-  apply (unfold Units_def)
-  apply auto
-  done
-
-lemma (in monoid) inv_char:
-  "x \<in> carrier G \<Longrightarrow> y \<in> carrier G \<Longrightarrow> x \<otimes> y = \<one> \<Longrightarrow> y \<otimes> x = \<one> \<Longrightarrow> inv x = y"
-  apply (subgoal_tac "x \<in> Units G")
-   apply (subgoal_tac "y = inv x \<otimes> \<one>")
-    apply simp
-   apply (erule subst)
-   apply (subst m_assoc [symmetric])
-      apply auto
-  apply (unfold Units_def)
-  apply auto
-  done
-
-lemma (in comm_monoid) comm_inv_char: "x \<in> carrier G \<Longrightarrow> y \<in> carrier G \<Longrightarrow> x \<otimes> y = \<one> \<Longrightarrow> inv x = y"
-  apply (rule inv_char)
-     apply auto
-  apply (subst m_comm, auto)
-  done
-
-lemma (in ring) inv_neg_one [simp]: "inv (\<ominus> \<one>) = \<ominus> \<one>"
-  apply (rule inv_char)
-     apply (auto simp add: l_minus r_minus)
-  done
-
-lemma (in monoid) inv_eq_imp_eq: "x \<in> Units G \<Longrightarrow> y \<in> Units G \<Longrightarrow> inv x = inv y \<Longrightarrow> x = y"
-  apply (subgoal_tac "inv (inv x) = inv (inv y)")
-   apply (subst (asm) Units_inv_inv)+
-    apply auto
-  done
-
-lemma (in ring) Units_minus_one_closed [intro]: "\<ominus> \<one> \<in> Units R"
-  apply (unfold Units_def)
-  apply auto
-  apply (rule_tac x = "\<ominus> \<one>" in bexI)
-   apply auto
-  apply (simp add: l_minus r_minus)
-  done
-
-lemma (in monoid) inv_one [simp]: "inv \<one> = \<one>"
-  apply (rule inv_char)
-     apply auto
-  done
-
-lemma (in ring) inv_eq_neg_one_eq: "x \<in> Units R \<Longrightarrow> inv x = \<ominus> \<one> \<longleftrightarrow> x = \<ominus> \<one>"
-  apply auto
-  apply (subst Units_inv_inv [symmetric])
-   apply auto
-  done
-
-lemma (in monoid) inv_eq_one_eq: "x \<in> Units G \<Longrightarrow> inv x = \<one> \<longleftrightarrow> x = \<one>"
-  by (metis Units_inv_inv inv_one)
-
-end
diff -r ff61cbfb3f2d -r c183a6a69f2d src/HOL/Algebra/Multiplicative_Group.thy
--- a/src/HOL/Algebra/Multiplicative_Group.thy	Tue Jun 12 16:09:12 2018 +0100
+++ b/src/HOL/Algebra/Multiplicative_Group.thy	Thu Jun 14 14:23:38 2018 +0100
@@ -7,8 +7,6 @@
 imports
   Complex_Main
   Group
-  More_Group
-  More_Finite_Product
   Coset
   UnivPoly
 begin
diff -r ff61cbfb3f2d -r c183a6a69f2d src/HOL/Algebra/Ring.thy
--- a/src/HOL/Algebra/Ring.thy	Tue Jun 12 16:09:12 2018 +0100
+++ b/src/HOL/Algebra/Ring.thy	Thu Jun 14 14:23:38 2018 +0100
@@ -25,10 +25,9 @@
   a_inv :: "[('a, 'm) ring_scheme, 'a ] \<Rightarrow> 'a" ("\<ominus>\<index> _" [81] 80)
   where "a_inv R = m_inv (add_monoid R)"
 
-
 definition
   a_minus :: "[('a, 'm) ring_scheme, 'a, 'a] => 'a" ("(_ \<ominus>\<index> _)" [65,66] 65)
-  where "\<lbrakk> x \<in> carrier R; y \<in> carrier R \<rbrakk> \<Longrightarrow> x \<ominus>\<^bsub>R\<^esub> y = x \<oplus>\<^bsub>R\<^esub> (\<ominus>\<^bsub>R\<^esub> y)"
+  where "x \<ominus>\<^bsub>R\<^esub> y = x \<oplus>\<^bsub>R\<^esub> (\<ominus>\<^bsub>R\<^esub> y)"
 
 definition
   add_pow :: "[_, ('b :: semiring_1), 'a] \<Rightarrow> 'a" ("[_] \<cdot>\<index> _" [81, 81] 80)
@@ -212,7 +211,6 @@
 
 lemmas l_neg = add.l_inv [simp del]
 lemmas r_neg = add.r_inv [simp del]
-lemmas minus_zero = add.inv_one
 lemmas minus_minus = add.inv_inv
 lemmas a_inv_inj = add.inv_inj
 lemmas minus_equality = add.inv_equality
@@ -344,6 +342,8 @@
 lemma (in cring) is_cring:
   "cring R" by (rule cring_axioms)
 
+lemma (in ring) minus_zero [simp]: "\<ominus> \<zero> = \<zero>"
+  by (simp add: a_inv_def)
 
 subsubsection \<open>Normaliser for Rings\<close>
 
@@ -416,9 +416,8 @@
 
 end
 
-lemma (in abelian_group) minus_eq:
-  "\<lbrakk> x \<in> carrier G; y \<in> carrier G \<rbrakk> \<Longrightarrow> x \<ominus> y = x \<oplus> (\<ominus> y)"
-  by (simp only: a_minus_def)
+lemma (in abelian_group) minus_eq: "x \<ominus> y = x \<oplus> (\<ominus> y)"
+  by (rule a_minus_def)
 
 text \<open>Setup algebra method:
   compute distributive normal form in locale contexts\<close>
@@ -602,7 +601,6 @@
     using add_pow_int_lt[of k R b] add_pow_int_lt[of k R "a \<otimes> b"]
           add_pow_rdistr[OF assms, of "nat (- k)"] assms r_minus by auto 
 qed
-(* ************************************************************************** *)
 
 
 subsection \<open>Integral Domains\<close>
@@ -631,7 +629,7 @@
   with R have "a \<otimes> (b \<ominus> c) = \<zero>" by algebra
   with R have "a = \<zero> \<or> (b \<ominus> c) = \<zero>" by (simp add: integral_iff)
   with prem and R have "b \<ominus> c = \<zero>" by auto 
-  with R have "b = b \<ominus> (b \<ominus> c)" by algebra 
+  with R have "b = b \<ominus> (b \<ominus> c)" by algebra
   also from R have "b \<ominus> (b \<ominus> c) = c" by algebra
   finally show "b = c" .
 next
@@ -805,4 +803,111 @@
   "\<lbrakk> f \<in> ring_hom R S; g \<in> ring_hom S T \<rbrakk> \<Longrightarrow> g \<circ> f \<in> ring_hom R T"
   by (rule ring_hom_memI) (auto simp add: ring_hom_closed ring_hom_mult ring_hom_add ring_hom_one)
 
+subsection\<open>Jeremy Avigad's @{text"More_Finite_Product"} material\<close>
+
+(* need better simplification rules for rings *)
+(* the next one holds more generally for abelian groups *)
+
+lemma (in cring) sum_zero_eq_neg: "x \<in> carrier R \<Longrightarrow> y \<in> carrier R \<Longrightarrow> x \<oplus> y = \<zero> \<Longrightarrow> x = \<ominus> y"
+  by (metis minus_equality)
+
+lemma (in domain) square_eq_one:
+  fixes x
+  assumes [simp]: "x \<in> carrier R"
+    and "x \<otimes> x = \<one>"
+  shows "x = \<one> \<or> x = \<ominus>\<one>"
+proof -
+  have "(x \<oplus> \<one>) \<otimes> (x \<oplus> \<ominus> \<one>) = x \<otimes> x \<oplus> \<ominus> \<one>"
+    by (simp add: ring_simprules)
+  also from \<open>x \<otimes> x = \<one>\<close> have "\<dots> = \<zero>"
+    by (simp add: ring_simprules)
+  finally have "(x \<oplus> \<one>) \<otimes> (x \<oplus> \<ominus> \<one>) = \<zero>" .
+  then have "(x \<oplus> \<one>) = \<zero> \<or> (x \<oplus> \<ominus> \<one>) = \<zero>"
+    by (intro integral) auto
+  then show ?thesis
+    by (metis add.inv_closed add.inv_solve_right assms(1) l_zero one_closed zero_closed)
+qed
+
+lemma (in domain) inv_eq_self: "x \<in> Units R \<Longrightarrow> x = inv x \<Longrightarrow> x = \<one> \<or> x = \<ominus>\<one>"
+  by (metis Units_closed Units_l_inv square_eq_one)
+
+
+text \<open>
+  The following translates theorems about groups to the facts about
+  the units of a ring. (The list should be expanded as more things are
+  needed.)
+\<close>
+
+lemma (in ring) finite_ring_finite_units [intro]: "finite (carrier R) \<Longrightarrow> finite (Units R)"
+  by (rule finite_subset) auto
+
+lemma (in monoid) units_of_pow:
+  fixes n :: nat
+  shows "x \<in> Units G \<Longrightarrow> x [^]\<^bsub>units_of G\<^esub> n = x [^]\<^bsub>G\<^esub> n"
+  apply (induct n)
+  apply (auto simp add: units_group group.is_monoid
+    monoid.nat_pow_0 monoid.nat_pow_Suc units_of_one units_of_mult)
+  done
+
+lemma (in cring) units_power_order_eq_one:
+  "finite (Units R) \<Longrightarrow> a \<in> Units R \<Longrightarrow> a [^] card(Units R) = \<one>"
+  by (metis comm_group.power_order_eq_one units_comm_group units_of_carrier units_of_one units_of_pow)
+
+subsection\<open>Jeremy Avigad's @{text"More_Ring"} material\<close>
+
+lemma (in cring) field_intro2: "\<zero>\<^bsub>R\<^esub> \<noteq> \<one>\<^bsub>R\<^esub> \<Longrightarrow> \<forall>x \<in> carrier R - {\<zero>\<^bsub>R\<^esub>}. x \<in> Units R \<Longrightarrow> field R"
+  apply (unfold_locales)
+    apply (use cring_axioms in auto)
+   apply (rule trans)
+    apply (subgoal_tac "a = (a \<otimes> b) \<otimes> inv b")
+     apply assumption
+    apply (subst m_assoc)
+       apply auto
+  apply (unfold Units_def)
+  apply auto
+  done
+
+lemma (in monoid) inv_char:
+  "x \<in> carrier G \<Longrightarrow> y \<in> carrier G \<Longrightarrow> x \<otimes> y = \<one> \<Longrightarrow> y \<otimes> x = \<one> \<Longrightarrow> inv x = y"
+  apply (subgoal_tac "x \<in> Units G")
+   apply (subgoal_tac "y = inv x \<otimes> \<one>")
+    apply simp
+   apply (erule subst)
+   apply (subst m_assoc [symmetric])
+      apply auto
+  apply (unfold Units_def)
+  apply auto
+  done
+
+lemma (in comm_monoid) comm_inv_char: "x \<in> carrier G \<Longrightarrow> y \<in> carrier G \<Longrightarrow> x \<otimes> y = \<one> \<Longrightarrow> inv x = y"
+  by (simp add: inv_char m_comm)
+
+lemma (in ring) inv_neg_one [simp]: "inv (\<ominus> \<one>) = \<ominus> \<one>"
+  apply (rule inv_char)
+     apply (auto simp add: l_minus r_minus)
+  done
+
+lemma (in monoid) inv_eq_imp_eq: "x \<in> Units G \<Longrightarrow> y \<in> Units G \<Longrightarrow> inv x = inv y \<Longrightarrow> x = y"
+  apply (subgoal_tac "inv (inv x) = inv (inv y)")
+   apply (subst (asm) Units_inv_inv)+
+    apply auto
+  done
+
+lemma (in ring) Units_minus_one_closed [intro]: "\<ominus> \<one> \<in> Units R"
+  apply (unfold Units_def)
+  apply auto
+  apply (rule_tac x = "\<ominus> \<one>" in bexI)
+   apply auto
+  apply (simp add: l_minus r_minus)
+  done
+
+lemma (in ring) inv_eq_neg_one_eq: "x \<in> Units R \<Longrightarrow> inv x = \<ominus> \<one> \<longleftrightarrow> x = \<ominus> \<one>"
+  apply auto
+  apply (subst Units_inv_inv [symmetric])
+   apply auto
+  done
+
+lemma (in monoid) inv_eq_one_eq: "x \<in> Units G \<Longrightarrow> inv x = \<one> \<longleftrightarrow> x = \<one>"
+  by (metis Units_inv_inv inv_one)
+
 end
diff -r ff61cbfb3f2d -r c183a6a69f2d src/HOL/Algebra/Sylow.thy
--- a/src/HOL/Algebra/Sylow.thy	Tue Jun 12 16:09:12 2018 +0100
+++ b/src/HOL/Algebra/Sylow.thy	Thu Jun 14 14:23:38 2018 +0100
@@ -223,7 +223,7 @@
 
 lemma M_funcset_rcosets_H:
   "(\<lambda>x\<in>M. H #> (SOME g. g \<in> carrier G \<and> M1 #> g = x)) \<in> M \<rightarrow> rcosets H"
-  by (metis (lifting) H_is_subgroup M_elem_map_carrier rcosetsI restrictI subgroup_imp_subset)
+  by (metis (lifting) H_is_subgroup M_elem_map_carrier rcosetsI restrictI subgroup.subset)
 
 lemma inj_M_GmodH: "\<exists>f \<in> M \<rightarrow> rcosets H. inj_on f M"
   apply (rule bexI)
diff -r ff61cbfb3f2d -r c183a6a69f2d src/HOL/Algebra/UnivPoly.thy
--- a/src/HOL/Algebra/UnivPoly.thy	Tue Jun 12 16:09:12 2018 +0100
+++ b/src/HOL/Algebra/UnivPoly.thy	Thu Jun 14 14:23:38 2018 +0100
@@ -116,14 +116,15 @@
 proof
   assume R: "p \<in> up R"
   then obtain n where "bound \<zero> n p" by auto
-  then have "bound \<zero> n (\<lambda>i. \<ominus> p i)" by auto
+  then have "bound \<zero> n (\<lambda>i. \<ominus> p i)"
+    by (simp add: bound_def minus_equality)
   then show "\<exists>n. bound \<zero> n (\<lambda>i. \<ominus> p i)" by auto
 qed auto
 
 lemma up_minus_closed:
   "[| p \<in> up R; q \<in> up R |] ==> (\<lambda>i. p i \<ominus> q i) \<in> up R"
-  using mem_upD [of p R] mem_upD [of q R] up_add_closed up_a_inv_closed a_minus_def [of _ R]
-  by auto
+  unfolding a_minus_def
+  using mem_upD [of p R] mem_upD [of q R] up_add_closed up_a_inv_closed  by auto
 
 lemma up_mult_closed:
   "[| p \<in> up R; q \<in> up R |] ==>
@@ -695,7 +696,7 @@
 
 lemma monom_a_inv [simp]:
   "a \<in> carrier R ==> monom P (\<ominus> a) n = \<ominus>\<^bsub>P\<^esub> monom P a n"
-  by (rule up_eqI) simp_all
+  by (rule up_eqI) auto
 
 lemma monom_inj:
   "inj_on (\<lambda>a. monom P a n) (carrier R)"
@@ -1462,9 +1463,9 @@
 subsection\<open>The long division algorithm: some previous facts.\<close>
 
 lemma coeff_minus [simp]:
-  assumes p: "p \<in> carrier P" and q: "q \<in> carrier P" shows "coeff P (p \<ominus>\<^bsub>P\<^esub> q) n = coeff P p n \<ominus> coeff P q n"
-  unfolding a_minus_def [OF p q] unfolding coeff_add [OF p a_inv_closed [OF q]] unfolding coeff_a_inv [OF q]
-  using coeff_closed [OF p, of n] using coeff_closed [OF q, of n] by algebra
+  assumes p: "p \<in> carrier P" and q: "q \<in> carrier P" 
+  shows "coeff P (p \<ominus>\<^bsub>P\<^esub> q) n = coeff P p n \<ominus> coeff P q n"
+  by (simp add: a_minus_def p q)
 
 lemma lcoeff_closed [simp]: assumes p: "p \<in> carrier P" shows "lcoeff p \<in> carrier R"
   using coeff_closed [OF p, of "deg R p"] by simp
@@ -1719,10 +1720,7 @@
     and min_mon0_closed: "\<ominus>\<^bsub>P\<^esub> monom P a 0 \<in> carrier P"
     using a R.a_inv_closed by auto
   have "eval R R id a ?g = eval R R id a (monom P \<one> 1) \<ominus> eval R R id a (monom P a 0)"
-    unfolding P.minus_eq [OF mon1_closed mon0_closed]
-    unfolding hom_add [OF mon1_closed min_mon0_closed]
-    unfolding hom_a_inv [OF mon0_closed]
-    using R.minus_eq [symmetric] mon1_closed mon0_closed by auto
+    by (simp add: a_minus_def mon0_closed)
   also have "\<dots> = a \<ominus> a"
     using eval_monom [OF R.one_closed a, of 1] using eval_monom [OF a a, of 0] using a by simp
   also have "\<dots> = \<zero>"
diff -r ff61cbfb3f2d -r c183a6a69f2d src/HOL/Algebra/Zassenhaus.thy
--- a/src/HOL/Algebra/Zassenhaus.thy	Tue Jun 12 16:09:12 2018 +0100
+++ b/src/HOL/Algebra/Zassenhaus.thy	Thu Jun 14 14:23:38 2018 +0100
@@ -2,220 +2,8 @@
   imports Coset Group_Action
 begin
 
-subsection "fundamental lemmas"
 
-
-text "Lemmas about subgroups"
-
-
-(*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)
-
-(*A subgroup of a subgroup is a subgroup of the group*)
-lemma (in group) incl_subgroup :
-  assumes "subgroup J G"
-    and "subgroup I (G\<lparr>carrier:=J\<rparr>)"
-  shows "subgroup I G" unfolding subgroup_def
-proof
-  have H1: "I \<subseteq> carrier (G\<lparr>carrier:=J\<rparr>)" using assms(2) subgroup_imp_subset by blast
-  also have H2: "...\<subseteq>J" by simp
-  also  have "...\<subseteq>(carrier G)"  by (simp add: assms(1) subgroup_imp_subset)
-  finally have H: "I \<subseteq> carrier G" by simp
-  have "(\<And>x y. \<lbrakk>x \<in> I ; y \<in> I\<rbrakk> \<Longrightarrow> x \<otimes> y \<in> I)" using assms(2) by (auto simp add: subgroup_def)
-  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)
-  thus "\<one> \<in> I \<and> (\<forall>x. x \<in> I \<longrightarrow> inv x \<in> I)" using K by blast
-qed
-
-
-text "Lemmas about set_mult"
-
-
-lemma (in group) set_mult_same_law :
-  assumes "subgroup H G"
-and "K1 \<subseteq> H"
-and "K2 \<subseteq> H"
-shows "K1<#>\<^bsub>(G\<lparr>carrier:=H\<rparr>)\<^esub>K2 = K1<#>K2"
-proof 
-  show "K1 <#>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> K2 \<subseteq> K1 <#> K2"
-  proof
-    fix h assume Hyph : "h\<in>K1<#>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub>K2"
-    then obtain k1 k2 where Hyp : "k1\<in>K1 \<and> k2\<in>K2 \<and> k1\<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub>k2 = h"
-      unfolding set_mult_def by blast
-    hence "k1\<in>H" using assms by blast
-    moreover have  "k2\<in>H" using Hyp assms by blast
-    ultimately have EGAL : "k1 \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> k2 = k1 \<otimes>\<^bsub>G\<^esub> k2" by simp
-    have "k1 \<otimes>\<^bsub>G\<^esub> k2 \<in> K1<#>K2" unfolding  set_mult_def using Hyp by blast
-    hence "k1 \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> k2 \<in> K1<#>K2" using EGAL by auto
-    thus "h \<in> K1<#>K2 " using Hyp by blast
-  qed
-  show "K1 <#> K2 \<subseteq> K1 <#>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> K2"
-  proof
-    fix h assume Hyph : "h\<in>K1<#>K2"
-    then obtain k1 k2 where Hyp : "k1\<in>K1 \<and> k2\<in>K2 \<and> k1\<otimes>k2 = h" unfolding set_mult_def by blast
-    hence k1H: "k1\<in>H" using assms by blast
-    have  k2H: "k2\<in>H" using Hyp assms by blast
-    have EGAL : "k1 \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> k2 = k1 \<otimes>\<^bsub>G\<^esub> k2" using k1H k2H by simp
-    have "k1 \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> k2 \<in> K1<#>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub>K2" unfolding  set_mult_def using Hyp by blast
-    hence "k1 \<otimes> k2 \<in> K1<#>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub>K2" using EGAL by auto
-    thus "h \<in> K1<#>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub>K2 " using Hyp by blast
-  qed
-qed
-
-
-(*A group multiplied by a subgroup stays the same*)
-lemma (in group) set_mult_carrier_idem :
-  assumes "subgroup H G"
-  shows "(carrier G)<#>H = carrier G"
-proof
-  show "(carrier G)<#>H \<subseteq> carrier G" unfolding set_mult_def using subgroup_imp_subset assms by blast
-next
-  have " (carrier G) #>  \<one> = carrier G" unfolding set_mult_def r_coset_def group_axioms by simp
-  moreover have "(carrier G) #>  \<one> \<subseteq> (carrier G) <#> H" unfolding set_mult_def r_coset_def
-    using assms subgroup.one_closed[OF assms] by blast
-  ultimately show "carrier G \<subseteq> (carrier G) <#> H" by simp
-qed
-
-(*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_imp_subset assms
-  by (metis monoid.cases_scheme order_refl partial_object.simps(1)
-      partial_object.update_convs(1) set_mult_same_law)
-
-(*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" 
-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
-  moreover have aux2 : "{N <#> H} = {\<Union>h\<in>H. N #> h }"unfolding set_mult_def r_coset_def by auto
-  ultimately show "H<#>N = N<#>H" by simp
-qed
-
-(*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_imp_subset by blast
-  hence NH : "N \<subseteq> H" by simp
-  have "K \<subseteq> carrier(G\<lparr>carrier := H\<rparr>)" using subgroup_imp_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 set_mult_same_law[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 set_mult_same_law[of H K N, OF assms(1) KH NH] by auto
-  ultimately show "K<#>N = N<#>K" by auto
-qed
-
-
-
-text "Lemmas about intersection and normal subgroups"
-
-
-
-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>)" 
-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>)"
-  show "H1K\<lhd>GHK"
-  proof (intro group.normal_invI[of GHK H1K])
-    show "Group.group GHK"
-      using GHK_def subgroups_Inter_pair subgroup_imp_group assms by blast
-
-  next
-    have  H1K_incl:"subgroup H1K (G\<lparr>carrier:= (H\<inter>K)\<rparr>)"
-    proof(intro subgroup_incl)
-          show "subgroup H1K G"
-            using assms normal_imp_subgroup subgroups_Inter_pair incl_subgroup H1K_def by blast
-        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>))" 
-            using  assms(3) normal_imp_subgroup subgroup_imp_subset by blast
-          also have "... \<subseteq> H" by simp
-          thus "H1K \<subseteq>H\<inter>K" 
-            using H1K_def calculation by auto
-        qed
-        thus "subgroup H1K GHK" using GHK_def by simp
-
-  next
-    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
-          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"
-            fix h assume p2 : "h:H1K"
-            have "carrier(GHK)\<subseteq>HK"
-              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
-            have "H1\<subseteq>carrier(GH)"
-              using assms GH_def normal_imp_subgroup subgroup_imp_subset by blast
-            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 hH:"h\<in>carrier(GH)"
-              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"
-              using  xH H1K_def p2 by blast
-            have " x \<otimes>\<^bsub>GH\<^esub> h \<otimes>\<^bsub>GH\<^esub> inv\<^bsub>GH\<^esub> x \<in> HK"
-              using assms HK_def subgroups_Inter_pair hHK xHK
-              by (metis GH_def inf.cobounded1 subgroup_def subgroup_incl)
-            hence " x \<otimes>\<^bsub>GH\<^esub> h \<otimes>\<^bsub>GH\<^esub> inv\<^bsub>GH\<^esub> x \<in> K" using HK_def by simp
-            hence " x \<otimes>\<^bsub>GH\<^esub> h \<otimes>\<^bsub>GH\<^esub> inv\<^bsub>GH\<^esub> x \<in> H1K" using INCL_1 H1K_def by auto
-            thus  "x \<otimes>\<^bsub>GHK\<^esub> h \<otimes>\<^bsub>GHK\<^esub> inv\<^bsub>GHK\<^esub> x \<in> H1K" using xhx_egal by simp
-          qed
-    qed
-qed
-
-
-lemma (in group) normal_inter_subgroup :
-  assumes "subgroup H G"
-    and "N \<lhd> G"
-  shows "(N\<inter>H) \<lhd> (G\<lparr>carrier := H\<rparr>)"
-proof -
-  define K where "K = carrier G"
-  have "G\<lparr>carrier := K\<rparr> =  G" using K_def by auto
-  moreover have "subgroup K G" using K_def subgroup_self by blast
-  moreover have "normal N (G \<lparr>carrier :=K\<rparr>)" using assms K_def by simp
-  ultimately have "N \<inter> H \<lhd> G\<lparr>carrier := K \<inter> H\<rparr>"
-    using normal_inter[of K H N] assms(1) by blast
-  moreover have "K \<inter> H = H" using K_def assms subgroup_imp_subset by blast
-  ultimately show "normal (N\<inter>H) (G\<lparr>carrier := H\<rparr>)" by auto
-qed
-
-
-
-text \<open>Lemmas about normalizer\<close>
+subsubsection \<open>Lemmas about normalizer\<close>
 
 
 lemma (in group) subgroup_in_normalizer: 
@@ -267,39 +55,38 @@
 qed
 
 
-lemma (in group) normal_imp_subgroup_normalizer :
+lemma (in group) normal_imp_subgroup_normalizer:
   assumes "subgroup H G"
-and "N \<lhd> (G\<lparr>carrier := H\<rparr>)"
-shows "subgroup H (G\<lparr>carrier := normalizer G N\<rparr>)" 
+    and "N \<lhd> (G\<lparr>carrier := H\<rparr>)"
+  shows "subgroup H (G\<lparr>carrier := normalizer G N\<rparr>)" 
 proof-
   have N_carrierG : "N \<subseteq> carrier(G)"
     using assms normal_imp_subgroup subgroup_imp_subset
     by (smt monoid.cases_scheme order_trans partial_object.simps(1) partial_object.update_convs(1))
   {have "H \<subseteq> normalizer G N" unfolding normalizer_def stabilizer_def
     proof
-    fix x assume xH : "x \<in> H"
-    hence xcarrierG : "x \<in> carrier(G)" using assms subgroup_imp_subset  by auto
-    have "   N #> x = x <# N" using assms xH
-      unfolding r_coset_def l_coset_def normal_def normal_axioms_def subgroup_imp_group by auto
-    hence "x <# N #> inv x =(N #> x) #> inv x"
-      by simp
-    also have "... = N #> \<one>"
-      using  assms r_inv xcarrierG coset_mult_assoc[OF N_carrierG] by simp  
-    finally have "x <# N #> inv x = N" by (simp add: N_carrierG)
-    thus "x \<in> {g \<in> carrier G. (\<lambda>H\<in>{H. H \<subseteq> carrier G}. g <# H #> inv g) N = N}"
-      using xcarrierG by (simp add : N_carrierG)
-  qed}
+      fix x assume xH : "x \<in> H"
+      hence xcarrierG : "x \<in> carrier(G)" using assms subgroup_imp_subset  by auto
+      have "   N #> x = x <# N" using assms xH
+        unfolding r_coset_def l_coset_def normal_def normal_axioms_def subgroup_imp_group by auto
+      hence "x <# N #> inv x =(N #> x) #> inv x"
+        by simp
+      also have "... = N #> \<one>"
+        using  assms r_inv xcarrierG coset_mult_assoc[OF N_carrierG] by simp  
+      finally have "x <# N #> inv x = N" by (simp add: N_carrierG)
+      thus "x \<in> {g \<in> carrier G. (\<lambda>H\<in>{H. H \<subseteq> carrier G}. g <# H #> inv g) N = N}"
+        using xcarrierG by (simp add : N_carrierG)
+    qed}
   thus "subgroup H (G\<lparr>carrier := normalizer G N\<rparr>)"
     using subgroup_incl[OF assms(1) normalizer_imp_subgroup]
-         assms normal_imp_subgroup subgroup_imp_subset
+      assms normal_imp_subgroup subgroup_imp_subset
     by (metis  group.incl_subgroup is_group)
 qed
 
 
 subsection \<open>Second Isomorphism Theorem\<close>
 
-
-lemma (in group) mult_norm_subgroup :
+lemma (in group) mult_norm_subgroup:
   assumes "normal N G"
     and "subgroup H G"
   shows "subgroup (N<#>H) G" unfolding subgroup_def
@@ -364,7 +151,7 @@
 qed
     
 
-lemma (in group) mult_norm_sub_in_sub :
+lemma (in group) mult_norm_sub_in_sub:
   assumes "normal N (G\<lparr>carrier:=K\<rparr>)"
   assumes "subgroup H (G\<lparr>carrier:=K\<rparr>)"
   assumes "subgroup K G"
@@ -379,12 +166,12 @@
   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 set_mult_same_law[of K] assms Incl1 Incl2 by simp
+    using subgroup_set_mult_equality[of K] assms Incl1 Incl2 by simp
   thus "subgroup (N<#>H) (G\<lparr>carrier:=K\<rparr>)" using Hyp by auto
 qed
 
 
-lemma (in group) subgroup_of_normal_set_mult :
+lemma (in group) subgroup_of_normal_set_mult:
   assumes "normal N G"
 and "subgroup H G"
 shows "subgroup H (G\<lparr>carrier := N <#> H\<rparr>)"
@@ -398,7 +185,7 @@
 qed
 
 
-lemma (in group) normal_in_normal_set_mult :
+lemma (in group) normal_in_normal_set_mult:
   assumes "normal N G"
 and "subgroup H G"
 shows "normal N (G\<lparr>carrier := N <#> H\<rparr>)"
@@ -413,7 +200,7 @@
 qed
 
 
-proposition (in group) weak_snd_iso_thme :
+proposition (in group) weak_snd_iso_thme:
   assumes "subgroup  H G" 
     and "N\<lhd>G"
   shows "(G\<lparr>carrier := N<#>H\<rparr> Mod N \<cong> G\<lparr>carrier:=H\<rparr> Mod (N\<inter>H))"
@@ -518,7 +305,7 @@
 qed
 
 
-theorem (in group) snd_iso_thme :
+theorem (in group) snd_iso_thme:
   assumes "subgroup H G"
     and "subgroup N G"
     and "subgroup H (G\<lparr>carrier:= (normalizer G N)\<rparr>)"
@@ -539,7 +326,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 set_mult_same_law[OF  normalizer_imp_subgroup[OF subgroup_imp_subset[OF assms(2)]], of N H] 
+    using subgroup_set_mult_equality[OF  normalizer_imp_subgroup[OF subgroup_imp_subset[OF assms(2)]], of N H] 
           subgroup_imp_subset[OF assms(3)]
           subgroup_imp_subset[OF normal_imp_subgroup[OF subgroup_in_normalizer[OF assms(2)]]]
     by simp
@@ -570,7 +357,7 @@
 subsection\<open>The Zassenhaus Lemma\<close>
 
 
-lemma (in group) distinc :
+lemma (in group) distinc:
   assumes "subgroup  H G" 
     and "H1\<lhd>G\<lparr>carrier := H\<rparr>" 
     and  "subgroup K G" 
@@ -623,7 +410,7 @@
   qed
 qed
 
-lemma (in group) preliminary1 :
+lemma (in group) preliminary1:
   assumes "subgroup  H G" 
     and "H1\<lhd>G\<lparr>carrier := H\<rparr>" 
     and  "subgroup K G" 
@@ -664,7 +451,7 @@
   qed
 qed
 
-lemma (in group) preliminary2 :
+lemma (in group) preliminary2:
   assumes "subgroup  H G" 
     and "H1\<lhd>G\<lparr>carrier := H\<rparr>"
     and  "subgroup K G" 
@@ -700,7 +487,7 @@
     hence allG : "h1 \<in> carrier G" "hk \<in> carrier G" "x \<in> carrier G"
       using assms subgroup_imp_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 set_mult_same_law subgroup_imp_subset xH h1hk_def by (simp add: l_coset_def)
+      using subgroup_set_mult_equality subgroup_imp_subset xH h1hk_def by (simp add: l_coset_def)
     also have "... = h1 <# (hk <# (H1 <#> H\<inter>K1))"
       using lcos_m_assoc[OF subgroup_imp_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_imp_subset)
@@ -742,7 +529,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 set_mult_same_law subgroup_imp_subset xH h1hk_def by (simp add: r_coset_def)
+      using subgroup_set_mult_equality subgroup_imp_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"
@@ -762,7 +549,7 @@
 qed
 
 
-proposition (in group)  Zassenhaus_1 :
+proposition (in group)  Zassenhaus_1:
   assumes "subgroup  H G" 
     and "H1\<lhd>G\<lparr>carrier := H\<rparr>" 
     and  "subgroup K G" 
@@ -811,7 +598,7 @@
 qed
 
 
-theorem (in group) Zassenhaus :
+theorem (in group) Zassenhaus:
   assumes "subgroup  H G" 
     and "H1\<lhd>G\<lparr>carrier := H\<rparr>" 
     and  "subgroup K G" 
diff -r ff61cbfb3f2d -r c183a6a69f2d src/HOL/ROOT
--- a/src/HOL/ROOT	Tue Jun 12 16:09:12 2018 +0100
+++ b/src/HOL/ROOT	Thu Jun 14 14:23:38 2018 +0100
@@ -294,22 +294,16 @@
   theories
     (* Orders and Lattices *)
     Galois_Connection    (* Knaster-Tarski theorem and Galois connections *)
-
     (* Groups *)
     FiniteProduct        (* Product operator for commutative groups *)
     Sylow                (* Sylow's theorem *)
     Bij                  (* Automorphism Groups *)
-    More_Group
-    More_Finite_Product
     Multiplicative_Group
     Zassenhaus            (* The Zassenhaus lemma *)
-
-
     (* Rings *)
     Divisibility         (* Rings *)
     IntRing              (* Ideals and residue classes *)
     UnivPoly             (* Polynomials *)
-    More_Ring
   document_files "root.bib" "root.tex"
 
 session "HOL-Auth" (timing) in Auth = "HOL-Library" +