reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
authorpaulson <lp15@cam.ac.uk>
Thu Jun 14 14:23:38 2018 +0100 (3 months ago)
changeset 68445c183a6a69f2d
parent 68444 ff61cbfb3f2d
child 68446 92ddca1edc43
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
src/HOL/Algebra/Coset.thy
src/HOL/Algebra/FiniteProduct.thy
src/HOL/Algebra/Group.thy
src/HOL/Algebra/Group_Action.thy
src/HOL/Algebra/Ideal.thy
src/HOL/Algebra/More_Finite_Product.thy
src/HOL/Algebra/More_Group.thy
src/HOL/Algebra/More_Ring.thy
src/HOL/Algebra/Multiplicative_Group.thy
src/HOL/Algebra/Ring.thy
src/HOL/Algebra/Sylow.thy
src/HOL/Algebra/UnivPoly.thy
src/HOL/Algebra/Zassenhaus.thy
src/HOL/ROOT
     1.1 --- a/src/HOL/Algebra/Coset.thy	Tue Jun 12 16:09:12 2018 +0100
     1.2 +++ b/src/HOL/Algebra/Coset.thy	Thu Jun 14 14:23:38 2018 +0100
     1.3 @@ -1,7 +1,6 @@
     1.4  (*  Title:      HOL/Algebra/Coset.thy
     1.5 -    Author:     Florian Kammueller
     1.6 -    Author:     L C Paulson
     1.7 -    Author:     Stephan Hohe
     1.8 +    Authors:     Florian Kammueller, L C Paulson, Stephan Hohe
     1.9 +With additional contributions from Martin Baillon and Paulo Emílio de Vilhena.
    1.10  *)
    1.11  
    1.12  theory Coset
    1.13 @@ -106,10 +105,9 @@
    1.14    shows "h <#\<^bsub>G \<lparr> carrier := H \<rparr>\<^esub> I = h <# I"
    1.15    using subgroup_set_mult_equality by (simp add: l_coset_eq_set_mult assms)
    1.16  
    1.17 -(* ************************************************************************** *)
    1.18                                   
    1.19  
    1.20 -subsection \<open>Basic Properties of set_mult\<close>
    1.21 +subsection \<open>Basic Properties of set multiplication\<close>
    1.22  
    1.23  lemma (in group) setmult_subset_G:
    1.24    assumes "H \<subseteq> carrier G" "K \<subseteq> carrier G"
    1.25 @@ -121,9 +119,7 @@
    1.26    shows "H <#> K \<subseteq> carrier G"
    1.27    using assms by (auto simp add: set_mult_def subsetD)
    1.28  
    1.29 -(* ************************************************************************** *)
    1.30 -(* Next lemma contributed by Martin Baillon.                                  *)
    1.31 -
    1.32 +(* Next lemma contributed by Martin Baillon.*)
    1.33  lemma (in group) set_mult_assoc:
    1.34    assumes "M \<subseteq> carrier G" "H \<subseteq> carrier G" "K \<subseteq> carrier G"
    1.35    shows "(M <#> H) <#> K = M <#> (H <#> K)"
    1.36 @@ -151,7 +147,6 @@
    1.37    qed
    1.38  qed
    1.39  
    1.40 -(* ************************************************************************** *)
    1.41  
    1.42  
    1.43  subsection \<open>Basic Properties of Cosets\<close>
    1.44 @@ -1087,7 +1082,6 @@
    1.45  
    1.46  subsection \<open>Theorems about Factor Groups and Direct product\<close>
    1.47  
    1.48 -
    1.49  lemma (in group) DirProd_normal :
    1.50    assumes "group K"
    1.51      and "H \<lhd> G"
    1.52 @@ -1158,5 +1152,148 @@
    1.53          DirProd_group[OF normal.factorgroup_is_group normal.factorgroup_is_group]
    1.54    by blast
    1.55  
    1.56 +subsubsection "More Lemmas about set multiplication"
    1.57 +
    1.58 +(*A group multiplied by a subgroup stays the same*)
    1.59 +lemma (in group) set_mult_carrier_idem:
    1.60 +  assumes "subgroup H G"
    1.61 +  shows "(carrier G) <#> H = carrier G"
    1.62 +proof
    1.63 +  show "(carrier G)<#>H \<subseteq> carrier G" 
    1.64 +    unfolding set_mult_def using subgroup_imp_subset assms by blast
    1.65 +next
    1.66 +  have " (carrier G) #>  \<one> = carrier G" unfolding set_mult_def r_coset_def group_axioms by simp
    1.67 +  moreover have "(carrier G) #>  \<one> \<subseteq> (carrier G) <#> H" unfolding set_mult_def r_coset_def
    1.68 +    using assms subgroup.one_closed[OF assms] by blast
    1.69 +  ultimately show "carrier G \<subseteq> (carrier G) <#> H" by simp
    1.70 +qed
    1.71 +
    1.72 +(*Same lemma as above, but everything is included in a subgroup*)
    1.73 +lemma (in group) set_mult_subgroup_idem:
    1.74 +  assumes "subgroup H G"
    1.75 +    and "subgroup N (G\<lparr>carrier:=H\<rparr>)"
    1.76 +  shows "H<#>N = H"
    1.77 +  using group.set_mult_carrier_idem[OF subgroup_imp_group] subgroup_imp_subset assms
    1.78 +  by (metis monoid.cases_scheme order_refl partial_object.simps(1)
    1.79 +      partial_object.update_convs(1) subgroup_set_mult_equality)
    1.80 +
    1.81 +(*A normal subgroup is commutative with set_mult*)
    1.82 +lemma (in group) commut_normal:
    1.83 +  assumes "subgroup H G"
    1.84 +    and "N\<lhd>G"
    1.85 +  shows "H<#>N = N<#>H" 
    1.86 +proof-
    1.87 +  have aux1: "{H <#> N} = {\<Union>h\<in>H. h <# N }" unfolding set_mult_def l_coset_def by auto
    1.88 +  also have "... = {\<Union>h\<in>H. N #> h }" using assms normal.coset_eq subgroup.mem_carrier by fastforce
    1.89 +  moreover have aux2: "{N <#> H} = {\<Union>h\<in>H. N #> h }"unfolding set_mult_def r_coset_def by auto
    1.90 +  ultimately show "H<#>N = N<#>H" by simp
    1.91 +qed
    1.92 +
    1.93 +(*Same lemma as above, but everything is included in a subgroup*)
    1.94 +lemma (in group) commut_normal_subgroup:
    1.95 +  assumes "subgroup H G"
    1.96 +    and "N\<lhd>(G\<lparr>carrier:=H\<rparr>)"
    1.97 +    and "subgroup K (G\<lparr>carrier:=H\<rparr>)"
    1.98 +  shows "K<#>N = N<#>K"
    1.99 +proof-
   1.100 +  have "N \<subseteq> carrier (G\<lparr>carrier := H\<rparr>)" using assms normal_imp_subgroup subgroup_imp_subset by blast
   1.101 +  hence NH : "N \<subseteq> H" by simp
   1.102 +  have "K \<subseteq> carrier(G\<lparr>carrier := H\<rparr>)" using subgroup_imp_subset assms by blast
   1.103 +  hence KH : "K \<subseteq> H" by simp
   1.104 +  have Egal : "K <#>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N = N <#>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> K"
   1.105 +  using group.commut_normal[where ?G = "G\<lparr>carrier :=H\<rparr>", of K N,OF subgroup_imp_group[OF assms(1)]
   1.106 +               assms(3) assms(2)] by auto
   1.107 +  also have "... = N <#> K" using subgroup_set_mult_equality[of H N K, OF assms(1) NH KH] by auto
   1.108 +  moreover have "K <#>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N = K <#> N"
   1.109 +    using subgroup_set_mult_equality[of H K N, OF assms(1) KH NH] by auto
   1.110 +  ultimately show "K<#>N = N<#>K" by auto
   1.111 +qed
   1.112 +
   1.113 +
   1.114 +
   1.115 +subsubsection "Lemmas about intersection and normal subgroups"
   1.116 +
   1.117 +lemma (in group) normal_inter:
   1.118 +  assumes "subgroup H G"
   1.119 +    and "subgroup K G"
   1.120 +    and "H1\<lhd>G\<lparr>carrier := H\<rparr>"
   1.121 +  shows " (H1\<inter>K)\<lhd>(G\<lparr>carrier:= (H\<inter>K)\<rparr>)" 
   1.122 +proof-
   1.123 +  define HK and H1K and GH and GHK
   1.124 +    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>)"
   1.125 +  show "H1K\<lhd>GHK"
   1.126 +  proof (intro group.normal_invI[of GHK H1K])
   1.127 +    show "Group.group GHK"
   1.128 +      using GHK_def subgroups_Inter_pair subgroup_imp_group assms by blast
   1.129 +
   1.130 +  next
   1.131 +    have  H1K_incl:"subgroup H1K (G\<lparr>carrier:= (H\<inter>K)\<rparr>)"
   1.132 +    proof(intro subgroup_incl)
   1.133 +      show "subgroup H1K G"
   1.134 +        using assms normal_imp_subgroup subgroups_Inter_pair incl_subgroup H1K_def by blast
   1.135 +    next
   1.136 +      show "subgroup (H\<inter>K) G" using HK_def subgroups_Inter_pair assms by auto
   1.137 +    next
   1.138 +      have "H1 \<subseteq> (carrier (G\<lparr>carrier:=H\<rparr>))" 
   1.139 +        using  assms(3) normal_imp_subgroup subgroup_imp_subset by blast
   1.140 +      also have "... \<subseteq> H" by simp
   1.141 +      thus "H1K \<subseteq>H\<inter>K" 
   1.142 +        using H1K_def calculation by auto
   1.143 +    qed
   1.144 +    thus "subgroup H1K GHK" using GHK_def by simp
   1.145 +  next
   1.146 +    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"
   1.147 +    proof-
   1.148 +      have invHK: "\<lbrakk>y\<in>HK\<rbrakk> \<Longrightarrow> inv\<^bsub>GHK\<^esub> y = inv\<^bsub>GH\<^esub> y"
   1.149 +        using subgroup_inv_equality assms HK_def GH_def GHK_def subgroups_Inter_pair by simp
   1.150 +      have multHK : "\<lbrakk>x\<in>HK;y\<in>HK\<rbrakk> \<Longrightarrow>  x \<otimes>\<^bsub>(G\<lparr>carrier:=HK\<rparr>)\<^esub> y =  x \<otimes> y"
   1.151 +        using HK_def by simp
   1.152 +      fix x assume p: "x\<in>carrier GHK"
   1.153 +      fix h assume p2 : "h:H1K"
   1.154 +      have "carrier(GHK)\<subseteq>HK"
   1.155 +        using GHK_def HK_def by simp
   1.156 +      hence xHK:"x\<in>HK" using p by auto
   1.157 +      hence invx:"inv\<^bsub>GHK\<^esub> x = inv\<^bsub>GH\<^esub> x"
   1.158 +        using invHK assms GHK_def HK_def GH_def subgroup_inv_equality subgroups_Inter_pair by simp
   1.159 +      have "H1\<subseteq>carrier(GH)"
   1.160 +        using assms GH_def normal_imp_subgroup subgroup_imp_subset by blast
   1.161 +      hence hHK:"h\<in>HK" 
   1.162 +        using p2 H1K_def HK_def GH_def by auto
   1.163 +      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"
   1.164 +        using invx invHK multHK GHK_def GH_def by auto
   1.165 +      have xH:"x\<in>carrier(GH)" 
   1.166 +        using xHK HK_def GH_def by auto 
   1.167 +      have hH:"h\<in>carrier(GH)"
   1.168 +        using hHK HK_def GH_def by auto 
   1.169 +      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)"
   1.170 +        using assms normal_invE GH_def normal.inv_op_closed2 by fastforce
   1.171 +      hence INCL_1 : "x \<otimes>\<^bsub>GH\<^esub> h \<otimes>\<^bsub>GH\<^esub> inv\<^bsub>GH\<^esub> x \<in> H1"
   1.172 +        using  xH H1K_def p2 by blast
   1.173 +      have " x \<otimes>\<^bsub>GH\<^esub> h \<otimes>\<^bsub>GH\<^esub> inv\<^bsub>GH\<^esub> x \<in> HK"
   1.174 +        using assms HK_def subgroups_Inter_pair hHK xHK
   1.175 +        by (metis GH_def inf.cobounded1 subgroup_def subgroup_incl)
   1.176 +      hence " x \<otimes>\<^bsub>GH\<^esub> h \<otimes>\<^bsub>GH\<^esub> inv\<^bsub>GH\<^esub> x \<in> K" using HK_def by simp
   1.177 +      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
   1.178 +      thus  "x \<otimes>\<^bsub>GHK\<^esub> h \<otimes>\<^bsub>GHK\<^esub> inv\<^bsub>GHK\<^esub> x \<in> H1K" using xhx_egal by simp
   1.179 +    qed
   1.180 +  qed
   1.181 +qed
   1.182 +
   1.183 +
   1.184 +lemma (in group) normal_inter_subgroup:
   1.185 +  assumes "subgroup H G"
   1.186 +    and "N \<lhd> G"
   1.187 +  shows "(N\<inter>H) \<lhd> (G\<lparr>carrier := H\<rparr>)"
   1.188 +proof -
   1.189 +  define K where "K = carrier G"
   1.190 +  have "G\<lparr>carrier := K\<rparr> =  G" using K_def by auto
   1.191 +  moreover have "subgroup K G" using K_def subgroup_self by blast
   1.192 +  moreover have "normal N (G \<lparr>carrier :=K\<rparr>)" using assms K_def by simp
   1.193 +  ultimately have "N \<inter> H \<lhd> G\<lparr>carrier := K \<inter> H\<rparr>"
   1.194 +    using normal_inter[of K H N] assms(1) by blast
   1.195 +  moreover have "K \<inter> H = H" using K_def assms subgroup_imp_subset by blast
   1.196 +  ultimately show "normal (N\<inter>H) (G\<lparr>carrier := H\<rparr>)" by auto
   1.197 +qed
   1.198 +
   1.199  
   1.200  end
     2.1 --- a/src/HOL/Algebra/FiniteProduct.thy	Tue Jun 12 16:09:12 2018 +0100
     2.2 +++ b/src/HOL/Algebra/FiniteProduct.thy	Thu Jun 14 14:23:38 2018 +0100
     2.3 @@ -524,4 +524,49 @@
     2.4  
     2.5  end
     2.6  
     2.7 +(* Jeremy Avigad. This should be generalized to arbitrary groups, not just commutative
     2.8 +   ones, using Lagrange's theorem. *)
     2.9 +
    2.10 +lemma (in comm_group) power_order_eq_one:
    2.11 +  assumes fin [simp]: "finite (carrier G)"
    2.12 +    and a [simp]: "a \<in> carrier G"
    2.13 +  shows "a [^] card(carrier G) = one G"
    2.14 +proof -
    2.15 +  have "(\<Otimes>x\<in>carrier G. x) = (\<Otimes>x\<in>carrier G. a \<otimes> x)"
    2.16 +    by (subst (2) finprod_reindex [symmetric],
    2.17 +      auto simp add: Pi_def inj_on_const_mult surj_const_mult)
    2.18 +  also have "\<dots> = (\<Otimes>x\<in>carrier G. a) \<otimes> (\<Otimes>x\<in>carrier G. x)"
    2.19 +    by (auto simp add: finprod_multf Pi_def)
    2.20 +  also have "(\<Otimes>x\<in>carrier G. a) = a [^] card(carrier G)"
    2.21 +    by (auto simp add: finprod_const)
    2.22 +  finally show ?thesis
    2.23 +(* uses the preceeding lemma *)
    2.24 +    by auto
    2.25 +qed
    2.26 +
    2.27 +
    2.28 +lemma (in comm_monoid) finprod_UN_disjoint:
    2.29 +  "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>
    2.30 +    (\<forall>i\<in>I. \<forall>x \<in> A i. g x \<in> carrier G) \<longrightarrow>
    2.31 +    finprod G g (UNION I A) = finprod G (\<lambda>i. finprod G g (A i)) I"
    2.32 +  apply (induct set: finite)
    2.33 +   apply force
    2.34 +  apply clarsimp
    2.35 +  apply (subst finprod_Un_disjoint)
    2.36 +       apply blast
    2.37 +      apply (erule finite_UN_I)
    2.38 +      apply blast
    2.39 +     apply (fastforce)
    2.40 +    apply (auto intro!: funcsetI finprod_closed)
    2.41 +  done
    2.42 +
    2.43 +lemma (in comm_monoid) finprod_Union_disjoint:
    2.44 +  "finite C \<Longrightarrow>
    2.45 +    \<forall>A\<in>C. finite A \<and> (\<forall>x\<in>A. f x \<in> carrier G) \<Longrightarrow>
    2.46 +    \<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A \<inter> B = {} \<Longrightarrow>
    2.47 +    finprod G f (\<Union>C) = finprod G (finprod G f) C"
    2.48 +  apply (frule finprod_UN_disjoint [of C id f])
    2.49 +  apply auto
    2.50 +  done
    2.51 +
    2.52  end
     3.1 --- a/src/HOL/Algebra/Group.thy	Tue Jun 12 16:09:12 2018 +0100
     3.2 +++ b/src/HOL/Algebra/Group.thy	Thu Jun 14 14:23:38 2018 +0100
     3.3 @@ -2,6 +2,7 @@
     3.4      Author:     Clemens Ballarin, started 4 February 2003
     3.5  
     3.6  Based on work by Florian Kammueller, L C Paulson and Markus Wenzel.
     3.7 +With additional contributions from Martin Baillon and Paulo Emílio de Vilhena.
     3.8  *)
     3.9  
    3.10  theory Group
    3.11 @@ -52,7 +53,7 @@
    3.12    assumes m_closed [intro, simp]:
    3.13           "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk> \<Longrightarrow> x \<otimes> y \<in> carrier G"
    3.14        and m_assoc:
    3.15 -         "\<lbrakk>x \<in> carrier G; y \<in> carrier G; z \<in> carrier G\<rbrakk> 
    3.16 +         "\<lbrakk>x \<in> carrier G; y \<in> carrier G; z \<in> carrier G\<rbrakk>
    3.17            \<Longrightarrow> (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
    3.18        and one_closed [intro, simp]: "\<one> \<in> carrier G"
    3.19        and l_one [simp]: "x \<in> carrier G \<Longrightarrow> \<one> \<otimes> x = x"
    3.20 @@ -104,13 +105,7 @@
    3.21    moreover from x y xinv yinv have "x \<otimes> (y \<otimes> y') \<otimes> x' = \<one>" by simp
    3.22    moreover note x y
    3.23    ultimately show ?thesis unfolding Units_def
    3.24 -    \<comment> \<open>Must avoid premature use of \<open>hyp_subst_tac\<close>.\<close>
    3.25 -    apply (rule_tac CollectI)
    3.26 -    apply (rule)
    3.27 -    apply (fast)
    3.28 -    apply (rule bexI [where x = "y' \<otimes> x'"])
    3.29 -    apply (auto simp: m_assoc)
    3.30 -    done
    3.31 +    by simp (metis m_assoc m_closed)
    3.32  qed
    3.33  
    3.34  lemma (in monoid) Units_one_closed [intro, simp]:
    3.35 @@ -146,6 +141,10 @@
    3.36     apply (fast intro: inv_unique, fast)
    3.37    done
    3.38  
    3.39 +lemma (in monoid) inv_one [simp]:
    3.40 +  "inv \<one> = \<one>"
    3.41 +  by (metis Units_one_closed Units_r_inv l_one monoid.Units_inv_closed monoid_axioms)
    3.42 +
    3.43  lemma (in monoid) Units_inv_Units [intro, simp]:
    3.44    "x \<in> Units G ==> inv x \<in> Units G"
    3.45  proof -
    3.46 @@ -223,12 +222,12 @@
    3.47  
    3.48  lemma (in monoid) nat_pow_comm:
    3.49    "x \<in> carrier G \<Longrightarrow> (x [^] (n::nat)) \<otimes> (x [^] (m :: nat)) = (x [^] m) \<otimes> (x [^] n)"
    3.50 -  using nat_pow_mult[of x n m] nat_pow_mult[of x m n] by (simp add: add.commute) 
    3.51 +  using nat_pow_mult[of x n m] nat_pow_mult[of x m n] by (simp add: add.commute)
    3.52  
    3.53  lemma (in monoid) nat_pow_Suc2:
    3.54    "x \<in> carrier G \<Longrightarrow> x [^] (Suc n) = x \<otimes> (x [^] n)"
    3.55    using nat_pow_mult[of x 1 n] Suc_eq_plus1[of n]
    3.56 -  by (metis One_nat_def Suc_eq_plus1_left l_one nat.rec(1) nat_pow_Suc nat_pow_def) 
    3.57 +  by (metis One_nat_def Suc_eq_plus1_left l_one nat.rec(1) nat_pow_Suc nat_pow_def)
    3.58  
    3.59  lemma (in monoid) nat_pow_pow:
    3.60    "x \<in> carrier G ==> (x [^] n) [^] m = x [^] (n * m::nat)"
    3.61 @@ -237,7 +236,7 @@
    3.62  lemma (in monoid) nat_pow_consistent:
    3.63    "x [^] (n :: nat) = x [^]\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> n"
    3.64    unfolding nat_pow_def by simp
    3.65 -  
    3.66 +
    3.67  
    3.68  (* Jacobson defines submonoid here. *)
    3.69  (* Jacobson defines the order of a monoid here. *)
    3.70 @@ -357,14 +356,6 @@
    3.71     (y \<otimes> x = z \<otimes> x) = (y = z)"
    3.72    by (metis inv_closed m_assoc r_inv r_one)
    3.73  
    3.74 -lemma (in group) inv_one [simp]:
    3.75 -  "inv \<one> = \<one>"
    3.76 -proof -
    3.77 -  have "inv \<one> = \<one> \<otimes> (inv \<one>)" by (simp del: r_inv Units_r_inv)
    3.78 -  moreover have "... = \<one>" by simp
    3.79 -  finally show ?thesis .
    3.80 -qed
    3.81 -
    3.82  lemma (in group) inv_inv [simp]:
    3.83    "x \<in> carrier G ==> inv (inv x) = x"
    3.84    using Units_inv_inv by simp
    3.85 @@ -449,7 +440,7 @@
    3.86      using inv_mult_group[OF Suc.prems nat_pow_closed[OF Suc.prems, of i]] by simp
    3.87    also have " ... = inv (x [^] (Suc i))"
    3.88      using Suc.prems nat_pow_Suc2 by auto
    3.89 -  finally show ?case . 
    3.90 +  finally show ?case .
    3.91  qed
    3.92  
    3.93  lemma (in group) int_pow_inv:
    3.94 @@ -578,6 +569,7 @@
    3.95    "x \<in> H \<Longrightarrow> x \<in> carrier G"
    3.96    using subset by blast
    3.97  
    3.98 +(*DELETE*)
    3.99  lemma subgroup_imp_subset:
   3.100    "subgroup H G \<Longrightarrow> H \<subseteq> carrier G"
   3.101    by (rule subgroup.subset)
   3.102 @@ -594,9 +586,9 @@
   3.103      done
   3.104  qed
   3.105  
   3.106 -lemma (in group) m_inv_consistent:
   3.107 +lemma (in group) subgroup_inv_equality:
   3.108    assumes "subgroup H G" "x \<in> H"
   3.109 -  shows "inv x = inv\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> x"
   3.110 +  shows "m_inv (G \<lparr>carrier := H\<rparr>) x = inv x"
   3.111    unfolding m_inv_def apply auto
   3.112    using subgroup.m_inv_closed[OF assms] inv_equality
   3.113    by (metis (no_types, hide_lams) assms subgroup.mem_carrier)
   3.114 @@ -613,14 +605,14 @@
   3.115    also have " ... = x [^]\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> n"
   3.116      using group.int_pow_def2[OF subgroup.subgroup_is_group[OF assms(1) is_group]] ge by auto
   3.117    finally show ?thesis .
   3.118 -next 
   3.119 +next
   3.120    assume "\<not> n \<ge> 0" hence lt: "n < 0" by simp
   3.121    hence "x [^] n = inv (x [^] (nat (- n)))"
   3.122      using int_pow_def2 by auto
   3.123    also have " ... = (inv x) [^] (nat (- n))"
   3.124      by (metis assms nat_pow_inv subgroup.mem_carrier)
   3.125    also have " ... = (inv\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> x) [^]\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> (nat (- n))"
   3.126 -    using m_inv_consistent[OF assms] nat_pow_consistent by auto
   3.127 +    using subgroup_inv_equality[OF assms] nat_pow_consistent by auto
   3.128    also have " ... = inv\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> (x [^]\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> (nat (- n)))"
   3.129      using group.nat_pow_inv[OF subgroup.subgroup_is_group[OF assms(1) is_group]] assms(2) by auto
   3.130    also have " ... = x [^]\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> n"
   3.131 @@ -657,7 +649,7 @@
   3.132      and "H \<noteq> {}"
   3.133      and "\<And>a. a \<in> H \<Longrightarrow> inv a \<in> H"
   3.134      and "\<And>a b. \<lbrakk>a \<in> H; b \<in> H\<rbrakk> \<Longrightarrow> a \<otimes> b \<in> H"
   3.135 -  using assms subgroup_imp_subset apply blast
   3.136 +  using assms subgroup.subset apply blast
   3.137    using assms subgroup_def apply auto[1]
   3.138    by (simp add: assms subgroup.m_closed subgroup.m_inv_closed)+
   3.139  
   3.140 @@ -691,12 +683,12 @@
   3.141  
   3.142  lemma (in group) group_incl_imp_subgroup:
   3.143    assumes "H \<subseteq> carrier G"
   3.144 -and "group (G\<lparr>carrier := H\<rparr>)"
   3.145 -shows "subgroup H G"
   3.146 +    and "group (G\<lparr>carrier := H\<rparr>)"
   3.147 +  shows "subgroup H G"
   3.148  proof (intro submonoid_subgroupI[OF monoid_incl_imp_submonoid[OF assms(1)]])
   3.149    show "monoid (G\<lparr>carrier := H\<rparr>)" using group_def assms by blast
   3.150    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
   3.151 -  fix a  assume aH : "a \<in> H" 
   3.152 +  fix a  assume aH : "a \<in> H"
   3.153    have " inv\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> a \<in> carrier G"
   3.154      using assms aH group.inv_closed[OF assms(2)] by auto
   3.155    moreover have "\<one>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> = \<one>" using assms monoid.one_closed ab_eq one_def by simp
   3.156 @@ -710,10 +702,6 @@
   3.157    ultimately show "inv a \<in> H" by auto
   3.158  qed
   3.159  
   3.160 -(*
   3.161 -lemma (in monoid) Units_subgroup:
   3.162 -  "subgroup (Units G) G"
   3.163 -*)
   3.164  
   3.165  subsection \<open>Direct Products\<close>
   3.166  
   3.167 @@ -731,7 +719,7 @@
   3.168    interpret G: monoid G by fact
   3.169    interpret H: monoid H by fact
   3.170    from assms
   3.171 -  show ?thesis by (unfold monoid_def DirProd_def, auto) 
   3.172 +  show ?thesis by (unfold monoid_def DirProd_def, auto)
   3.173  qed
   3.174  
   3.175  
   3.176 @@ -778,16 +766,16 @@
   3.177  
   3.178  lemma DirProd_subgroups :
   3.179    assumes "group G"
   3.180 -and "subgroup H G"
   3.181 -and "group K"
   3.182 -and "subgroup I K"
   3.183 -shows "subgroup (H \<times> I) (G \<times>\<times> K)"
   3.184 +    and "subgroup H G"
   3.185 +    and "group K"
   3.186 +    and "subgroup I K"
   3.187 +  shows "subgroup (H \<times> I) (G \<times>\<times> K)"
   3.188  proof (intro group.group_incl_imp_subgroup[OF DirProd_group[OF assms(1)assms(3)]])
   3.189 -  have "H \<subseteq> carrier G" "I \<subseteq> carrier K" using subgroup_imp_subset assms apply blast+.
   3.190 +  have "H \<subseteq> carrier G" "I \<subseteq> carrier K" using subgroup.subset assms apply blast+.
   3.191    thus "(H \<times> I) \<subseteq> carrier (G \<times>\<times> K)" unfolding DirProd_def by auto
   3.192    have "Group.group ((G\<lparr>carrier := H\<rparr>) \<times>\<times> (K\<lparr>carrier := I\<rparr>))"
   3.193      using DirProd_group[OF subgroup.subgroup_is_group[OF assms(2)assms(1)]
   3.194 -                           subgroup.subgroup_is_group[OF assms(4)assms(3)]].
   3.195 +        subgroup.subgroup_is_group[OF assms(4)assms(3)]].
   3.196    moreover have "((G\<lparr>carrier := H\<rparr>) \<times>\<times> (K\<lparr>carrier := I\<rparr>)) = ((G \<times>\<times> K)\<lparr>carrier := H \<times> I\<rparr>)"
   3.197      unfolding DirProd_def using assms apply simp.
   3.198    ultimately show "Group.group ((G \<times>\<times> K)\<lparr>carrier := H \<times> I\<rparr>)" by simp
   3.199 @@ -806,12 +794,12 @@
   3.200  by (fastforce simp add: hom_def compose_def)
   3.201  
   3.202  definition
   3.203 -  iso :: "_ => _ => ('a => 'b) set" 
   3.204 +  iso :: "_ => _ => ('a => 'b) set"
   3.205    where "iso G H = {h. h \<in> hom G H \<and> bij_betw h (carrier G) (carrier H)}"
   3.206  
   3.207  definition
   3.208    is_iso :: "_ \<Rightarrow> _ \<Rightarrow> bool" (infixr "\<cong>" 60)
   3.209 -  where "G \<cong> H = (iso G H  \<noteq> {})" 
   3.210 +  where "G \<cong> H = (iso G H  \<noteq> {})"
   3.211  
   3.212  lemma iso_set_refl: "(\<lambda>x. x) \<in> iso G G"
   3.213    by (simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def)
   3.214 @@ -821,9 +809,9 @@
   3.215  
   3.216  lemma (in group) iso_set_sym:
   3.217       "h \<in> iso G H \<Longrightarrow> inv_into (carrier G) h \<in> (iso H G)"
   3.218 -apply (simp add: iso_def bij_betw_inv_into) 
   3.219 -apply (subgoal_tac "inv_into (carrier G) h \<in> carrier H \<rightarrow> carrier G") 
   3.220 - prefer 2 apply (simp add: bij_betw_imp_funcset [OF bij_betw_inv_into]) 
   3.221 +apply (simp add: iso_def bij_betw_inv_into)
   3.222 +apply (subgoal_tac "inv_into (carrier G) h \<in> carrier H \<rightarrow> carrier G")
   3.223 + prefer 2 apply (simp add: bij_betw_imp_funcset [OF bij_betw_inv_into])
   3.224  apply (simp add: hom_def bij_betw_def inv_into_f_eq f_inv_into_f Pi_def)
   3.225  done
   3.226  
   3.227 @@ -831,7 +819,7 @@
   3.228  "G \<cong> H \<Longrightarrow> H \<cong> G"
   3.229    using iso_set_sym unfolding is_iso_def by auto
   3.230  
   3.231 -lemma (in group) iso_set_trans: 
   3.232 +lemma (in group) iso_set_trans:
   3.233       "[|h \<in> iso G H; i \<in> iso H I|] ==> (compose (carrier G) i h) \<in> iso G I"
   3.234  by (auto simp add: iso_def hom_compose bij_betw_compose)
   3.235  
   3.236 @@ -839,7 +827,7 @@
   3.237  "\<lbrakk>G \<cong> H ; H \<cong> I\<rbrakk> \<Longrightarrow> G \<cong> I"
   3.238    using iso_set_trans unfolding is_iso_def by blast
   3.239  
   3.240 -(* Next four lemmas contributed by Paulo Emílio de Vilhena. *)
   3.241 +(* Next four lemmas contributed by Paulo. *)
   3.242  
   3.243  lemma (in monoid) hom_imp_img_monoid:
   3.244    assumes "h \<in> hom G H"
   3.245 @@ -909,7 +897,7 @@
   3.246    obtain \<phi> where phi: "\<phi> \<in> iso G H" "inv_into (carrier G) \<phi> \<in> iso H G"
   3.247      using iso_set_sym assms unfolding is_iso_def by blast
   3.248    define \<psi> where psi_def: "\<psi> = inv_into (carrier G) \<phi>"
   3.249 -  
   3.250 +
   3.251    from phi
   3.252    have surj: "\<phi> ` (carrier G) = (carrier H)" "\<psi> ` (carrier H) = (carrier G)"
   3.253     and inj: "inj_on \<phi> (carrier G)" "inj_on \<psi> (carrier H)"
   3.254 @@ -983,7 +971,7 @@
   3.255    shows "(\<lambda>(x,y,z). (x,(y,z))) \<in> iso (G \<times>\<times> H \<times>\<times> I) (G \<times>\<times> (H \<times>\<times> I))"
   3.256  by (auto simp add: iso_def hom_def inj_on_def bij_betw_def)
   3.257  
   3.258 -lemma (in group) DirProd_iso_set_trans: 
   3.259 +lemma (in group) DirProd_iso_set_trans:
   3.260    assumes "g \<in> iso G G2"
   3.261      and "h \<in> iso H I"
   3.262    shows "(\<lambda>(x,y). (g x, h y)) \<in> iso (G \<times>\<times> H) (G2 \<times>\<times> I)"
   3.263 @@ -1058,7 +1046,7 @@
   3.264    "x \<in> carrier G \<Longrightarrow> (([^]) x) \<in> hom \<lparr> carrier = UNIV, mult = (+), one = 0::int \<rparr> G "
   3.265    unfolding hom_def by (simp add: int_pow_mult)
   3.266  
   3.267 -(* Next six lemmas contributed by Paulo Emílio de Vilhena. *)
   3.268 +(* Next six lemmas contributed by Paulo. *)
   3.269  
   3.270  lemma (in group_hom) img_is_subgroup: "subgroup (h ` (carrier G)) H"
   3.271    apply (rule subgroupI)
   3.272 @@ -1098,7 +1086,7 @@
   3.273    shows "group_hom (G \<lparr> carrier := H \<rparr>) G id"
   3.274    unfolding group_hom_def group_hom_axioms_def hom_def
   3.275    using subgroup.subgroup_is_group[OF assms is_group]
   3.276 -        is_group subgroup_imp_subset[OF assms] by auto
   3.277 +        is_group subgroup.subset[OF assms] by auto
   3.278  
   3.279  lemma (in group_hom) nat_pow_hom:
   3.280    "x \<in> carrier G \<Longrightarrow> h (x [^] (n :: nat)) = (h x) [^]\<^bsub>H\<^esub> n"
   3.281 @@ -1146,7 +1134,7 @@
   3.282        "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y = y \<otimes> x"
   3.283    shows "comm_monoid G"
   3.284    using l_one
   3.285 -    by (auto intro!: comm_monoid.intro comm_monoid_axioms.intro monoid.intro 
   3.286 +    by (auto intro!: comm_monoid.intro comm_monoid_axioms.intro monoid.intro
   3.287               intro: assms simp: m_closed one_closed m_comm)
   3.288  
   3.289  lemma (in monoid) monoid_comm_monoidI:
   3.290 @@ -1220,7 +1208,7 @@
   3.291    "[| x \<in> carrier G; y \<in> carrier G |] ==> inv (x \<otimes> y) = inv x \<otimes> inv y"
   3.292    by (simp add: m_ac inv_mult_group)
   3.293  
   3.294 -(* Next three lemmas contributed by Paulo Emílio de Vilhena. *)
   3.295 +(* Next three lemmas contributed by Paulo. *)
   3.296  
   3.297  lemma (in comm_monoid) hom_imp_img_comm_monoid:
   3.298    assumes "h \<in> hom G H"
   3.299 @@ -1280,6 +1268,32 @@
   3.300      using comm_gr by simp
   3.301  qed
   3.302  
   3.303 +(*A subgroup of a subgroup is a subgroup of the group*)
   3.304 +lemma (in group) incl_subgroup:
   3.305 +  assumes "subgroup J G"
   3.306 +    and "subgroup I (G\<lparr>carrier:=J\<rparr>)"
   3.307 +  shows "subgroup I G" unfolding subgroup_def
   3.308 +proof
   3.309 +  have H1: "I \<subseteq> carrier (G\<lparr>carrier:=J\<rparr>)" using assms(2) subgroup_imp_subset by blast
   3.310 +  also have H2: "...\<subseteq>J" by simp
   3.311 +  also  have "...\<subseteq>(carrier G)"  by (simp add: assms(1) subgroup_imp_subset)
   3.312 +  finally have H: "I \<subseteq> carrier G" by simp
   3.313 +  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)
   3.314 +  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
   3.315 +  have K: "\<one> \<in> I" using assms(2) by (auto simp add: subgroup_def)
   3.316 +  have "(\<And>x. x \<in> I \<Longrightarrow> inv x \<in> I)" using assms  subgroup.m_inv_closed H
   3.317 +    by (metis H1 H2  subgroup_inv_equality subsetCE)
   3.318 +  thus "\<one> \<in> I \<and> (\<forall>x. x \<in> I \<longrightarrow> inv x \<in> I)" using K by blast
   3.319 +qed
   3.320 +
   3.321 +(*A subgroup included in another subgroup is a subgroup of the subgroup*)
   3.322 +lemma (in group) subgroup_incl:
   3.323 +  assumes "subgroup I G"
   3.324 +    and "subgroup J G"
   3.325 +    and "I\<subseteq>J"
   3.326 +  shows "subgroup I (G\<lparr>carrier:=J\<rparr>)"using assms subgroup_inv_equality
   3.327 +  by (auto simp add: subgroup_def)
   3.328 +
   3.329  
   3.330  
   3.331  subsection \<open>The Lattice of Subgroups of a Group\<close>
   3.332 @@ -1300,16 +1314,7 @@
   3.333  
   3.334  lemma (in group) is_monoid [intro, simp]:
   3.335    "monoid G"
   3.336 -  by (auto intro: monoid.intro m_assoc) 
   3.337 -
   3.338 -lemma (in group) subgroup_inv_equality:
   3.339 -  "[| subgroup H G; x \<in> H |] ==> m_inv (G \<lparr>carrier := H\<rparr>) x = inv x"
   3.340 -apply (rule_tac inv_equality [THEN sym])
   3.341 -  apply (rule group.l_inv [OF subgroup_imp_group, simplified], assumption+)
   3.342 - apply (rule subsetD [OF subgroup.subset], assumption+)
   3.343 -apply (rule subsetD [OF subgroup.subset], assumption)
   3.344 -apply (rule_tac group.inv_closed [OF subgroup_imp_group, simplified], assumption+)
   3.345 -done
   3.346 +  by (auto intro: monoid.intro m_assoc)
   3.347  
   3.348  lemma (in group) subgroup_mult_equality:
   3.349    "\<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"
   3.350 @@ -1336,7 +1341,7 @@
   3.351  qed
   3.352  
   3.353  lemma (in group) subgroups_Inter_pair :
   3.354 -  assumes  "subgroup I G" 
   3.355 +  assumes  "subgroup I G"
   3.356      and  "subgroup J G"
   3.357    shows "subgroup (I\<inter>J) G" using subgroups_Inter[ where ?A = "{I,J}"] assms by auto
   3.358  
   3.359 @@ -1378,4 +1383,90 @@
   3.360    then show "\<exists>I. greatest ?L I (Lower ?L A)" ..
   3.361  qed
   3.362  
   3.363 +subsection\<open>Jeremy Avigad's @{text"More_Group"} material\<close>
   3.364 +
   3.365 +text \<open>
   3.366 +  Show that the units in any monoid give rise to a group.
   3.367 +
   3.368 +  The file Residues.thy provides some infrastructure to use
   3.369 +  facts about the unit group within the ring locale.
   3.370 +\<close>
   3.371 +
   3.372 +definition units_of :: "('a, 'b) monoid_scheme \<Rightarrow> 'a monoid"
   3.373 +  where "units_of G =
   3.374 +    \<lparr>carrier = Units G, Group.monoid.mult = Group.monoid.mult G, one  = one G\<rparr>"
   3.375 +
   3.376 +lemma (in monoid) units_group: "group (units_of G)"
   3.377 +  apply (unfold units_of_def)
   3.378 +  apply (rule groupI)
   3.379 +      apply auto
   3.380 +   apply (subst m_assoc)
   3.381 +      apply auto
   3.382 +  apply (rule_tac x = "inv x" in bexI)
   3.383 +   apply auto
   3.384 +  done
   3.385 +
   3.386 +lemma (in comm_monoid) units_comm_group: "comm_group (units_of G)"
   3.387 +  apply (rule group.group_comm_groupI)
   3.388 +   apply (rule units_group)
   3.389 +  apply (insert comm_monoid_axioms)
   3.390 +  apply (unfold units_of_def Units_def comm_monoid_def comm_monoid_axioms_def)
   3.391 +  apply auto
   3.392 +  done
   3.393 +
   3.394 +lemma units_of_carrier: "carrier (units_of G) = Units G"
   3.395 +  by (auto simp: units_of_def)
   3.396 +
   3.397 +lemma units_of_mult: "mult (units_of G) = mult G"
   3.398 +  by (auto simp: units_of_def)
   3.399 +
   3.400 +lemma units_of_one: "one (units_of G) = one G"
   3.401 +  by (auto simp: units_of_def)
   3.402 +
   3.403 +lemma (in monoid) units_of_inv: "x \<in> Units G \<Longrightarrow> m_inv (units_of G) x = m_inv G x"
   3.404 +  apply (rule sym)
   3.405 +  apply (subst m_inv_def)
   3.406 +  apply (rule the1_equality)
   3.407 +   apply (rule ex_ex1I)
   3.408 +    apply (subst (asm) Units_def)
   3.409 +    apply auto
   3.410 +     apply (erule inv_unique)
   3.411 +        apply auto
   3.412 +    apply (rule Units_closed)
   3.413 +    apply (simp_all only: units_of_carrier [symmetric])
   3.414 +    apply (insert units_group)
   3.415 +    apply auto
   3.416 +   apply (subst units_of_mult [symmetric])
   3.417 +   apply (subst units_of_one [symmetric])
   3.418 +   apply (erule group.r_inv, assumption)
   3.419 +  apply (subst units_of_mult [symmetric])
   3.420 +  apply (subst units_of_one [symmetric])
   3.421 +  apply (erule group.l_inv, assumption)
   3.422 +  done
   3.423 +
   3.424 +lemma (in group) inj_on_const_mult: "a \<in> carrier G \<Longrightarrow> inj_on (\<lambda>x. a \<otimes> x) (carrier G)"
   3.425 +  unfolding inj_on_def by auto
   3.426 +
   3.427 +lemma (in group) surj_const_mult: "a \<in> carrier G \<Longrightarrow> (\<lambda>x. a \<otimes> x) ` carrier G = carrier G"
   3.428 +  apply (auto simp add: image_def)
   3.429 +  apply (rule_tac x = "(m_inv G a) \<otimes> x" in bexI)
   3.430 +  apply auto
   3.431 +(* auto should get this. I suppose we need "comm_monoid_simprules"
   3.432 +   for ac_simps rewriting. *)
   3.433 +  apply (subst m_assoc [symmetric])
   3.434 +  apply auto
   3.435 +  done
   3.436 +
   3.437 +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"
   3.438 +  by (metis Units_eq Units_l_cancel monoid.r_one monoid_axioms one_closed)
   3.439 +
   3.440 +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"
   3.441 +  by (metis monoid.l_one monoid_axioms one_closed right_cancel)
   3.442 +
   3.443 +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"
   3.444 +  using l_cancel_one by fastforce
   3.445 +
   3.446 +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"
   3.447 +  using r_cancel_one by fastforce
   3.448 +
   3.449  end
     4.1 --- a/src/HOL/Algebra/Group_Action.thy	Tue Jun 12 16:09:12 2018 +0100
     4.2 +++ b/src/HOL/Algebra/Group_Action.thy	Thu Jun 14 14:23:38 2018 +0100
     4.3 @@ -1,7 +1,5 @@
     4.4 -(* ************************************************************************** *)
     4.5  (* Title:      Group_Action.thy                                               *)
     4.6  (* Author:     Paulo Emílio de Vilhena                                        *)
     4.7 -(* ************************************************************************** *)
     4.8  
     4.9  theory Group_Action
    4.10  imports Bij Coset Congruence
    4.11 @@ -313,7 +311,7 @@
    4.12  
    4.13  text \<open>In this subsection, we prove the Orbit-Stabilizer theorem.
    4.14        Our approach is to show the existence of a bijection between
    4.15 -      "rcosets (stabilizer G \<phi> x)" and "orbit G \<phi> x". Then we use
    4.16 +      "rcosets (stabilizer G phi x)" and "orbit G phi x". Then we use
    4.17        Lagrange's theorem to find the cardinal of the first set.\<close>
    4.18  
    4.19  subsubsection \<open>Rcosets - Supporting Lemmas\<close>
    4.20 @@ -766,11 +764,11 @@
    4.21    unfolding bij_betw_def
    4.22  proof
    4.23    show "inj_on ?\<phi> {H. subgroup H G}"
    4.24 -    using subgroup_conjugation_is_inj assms inj_on_def subgroup_imp_subset
    4.25 +    using subgroup_conjugation_is_inj assms inj_on_def subgroup.subset
    4.26      by (metis (mono_tags, lifting) inj_on_restrict_eq mem_Collect_eq)
    4.27  next
    4.28    have "\<And>H. H \<in> {H. subgroup H G} \<Longrightarrow> ?\<phi> ((inv g) <# H #> g) = H"
    4.29 -    by (simp add: assms subgroup_imp_subset subgroup_conjugation_is_surj0
    4.30 +    by (simp add: assms subgroup.subset subgroup_conjugation_is_surj0
    4.31                    subgroup_conjugation_is_surj1 is_group)
    4.32    hence "\<And>H. H \<in> {H. subgroup H G} \<Longrightarrow> \<exists>H' \<in> {H. subgroup H G}. ?\<phi> H' = H"
    4.33      using assms subgroup_conjugation_is_surj1 by fastforce
    4.34 @@ -800,11 +798,11 @@
    4.35        by (simp add: H g2 subgroup_conjugation_is_surj2)
    4.36      also have " ... = g1 <# (g2 <# H) #> ((inv g2) \<otimes> (inv g1))"
    4.37        by (simp add: H coset_mult_assoc g1 g2 group.coset_assoc
    4.38 -                    is_group l_coset_subset_G subgroup_imp_subset)
    4.39 +                    is_group l_coset_subset_G subgroup.subset)
    4.40      also have " ... = g1 <# (g2 <# H) #> inv (g1 \<otimes> g2)"
    4.41        using g1 g2 by (simp add: inv_mult_group)
    4.42      finally have "(?\<phi> g1) ((?\<phi> g2) H) = ?\<psi> (g1 \<otimes> g2) H"
    4.43 -      by (simp add: H g1 g2 lcos_m_assoc subgroup_imp_subset)
    4.44 +      by (simp add: H g1 g2 lcos_m_assoc subgroup.subset)
    4.45      thus "?\<psi> (g1 \<otimes> g2) H = (?\<phi> g1) ((?\<phi> g2) H)" by auto
    4.46    qed
    4.47    hence "\<And> g1 g2. \<lbrakk> g1 \<in> carrier G; g2 \<in> carrier G \<rbrakk> \<Longrightarrow>
     5.1 --- a/src/HOL/Algebra/Ideal.thy	Tue Jun 12 16:09:12 2018 +0100
     5.2 +++ b/src/HOL/Algebra/Ideal.thy	Thu Jun 14 14:23:38 2018 +0100
     5.3 @@ -14,7 +14,7 @@
     5.4  
     5.5  locale ideal = additive_subgroup I R + ring R for I and R (structure) +
     5.6    assumes I_l_closed: "\<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> x \<otimes> a \<in> I"
     5.7 -    and I_r_closed: "\<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> a \<otimes> x \<in> I"
     5.8 +      and I_r_closed: "\<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> a \<otimes> x \<in> I"
     5.9  
    5.10  sublocale ideal \<subseteq> abelian_subgroup I R
    5.11    apply (intro abelian_subgroupI3 abelian_group.intro)
    5.12 @@ -74,7 +74,7 @@
    5.13  
    5.14  locale maximalideal = ideal +
    5.15    assumes I_notcarr: "carrier R \<noteq> I"
    5.16 -    and I_maximal: "\<lbrakk>ideal J R; I \<subseteq> J; J \<subseteq> carrier R\<rbrakk> \<Longrightarrow> J = I \<or> J = carrier R"
    5.17 +    and I_maximal: "\<lbrakk>ideal J R; I \<subseteq> J; J \<subseteq> carrier R\<rbrakk> \<Longrightarrow> (J = I) \<or> (J = carrier R)"
    5.18  
    5.19  lemma (in maximalideal) is_maximalideal: "maximalideal I R"
    5.20    by (rule maximalideal_axioms)
    5.21 @@ -83,7 +83,7 @@
    5.22    fixes R
    5.23    assumes "ideal I R"
    5.24      and I_notcarr: "carrier R \<noteq> I"
    5.25 -    and I_maximal: "\<And>J. \<lbrakk>ideal J R; I \<subseteq> J; J \<subseteq> carrier R\<rbrakk> \<Longrightarrow> J = I \<or> J = carrier R"
    5.26 +    and I_maximal: "\<And>J. \<lbrakk>ideal J R; I \<subseteq> J; J \<subseteq> carrier R\<rbrakk> \<Longrightarrow> (J = I) \<or> (J = carrier R)"
    5.27    shows "maximalideal I R"
    5.28  proof -
    5.29    interpret ideal I R by fact
    5.30 @@ -143,26 +143,17 @@
    5.31  subsection \<open>Special Ideals\<close>
    5.32  
    5.33  lemma (in ring) zeroideal: "ideal {\<zero>} R"
    5.34 -  apply (intro idealI subgroup.intro)
    5.35 -        apply (rule is_ring)
    5.36 -       apply simp+
    5.37 -    apply (fold a_inv_def, simp)
    5.38 -   apply simp+
    5.39 -  done
    5.40 +  by (intro idealI subgroup.intro) (simp_all add: is_ring)
    5.41  
    5.42  lemma (in ring) oneideal: "ideal (carrier R) R"
    5.43    by (rule idealI) (auto intro: is_ring add.subgroupI)
    5.44  
    5.45  lemma (in "domain") zeroprimeideal: "primeideal {\<zero>} R"
    5.46 -  apply (intro primeidealI)
    5.47 -     apply (rule zeroideal)
    5.48 -    apply (rule domain.axioms, rule domain_axioms)
    5.49 -   defer 1
    5.50 -   apply (simp add: integral)
    5.51 -proof (rule ccontr, simp)
    5.52 -  assume "carrier R = {\<zero>}"
    5.53 -  then have "\<one> = \<zero>" by (rule one_zeroI)
    5.54 -  with one_not_zero show False by simp
    5.55 +proof -
    5.56 +  have "carrier R \<noteq> {\<zero>}"
    5.57 +    by (simp add: carrier_one_not_zero)
    5.58 +  then show ?thesis
    5.59 +    by (metis (no_types, lifting) domain_axioms domain_def integral primeidealI singleton_iff zeroideal)
    5.60  qed
    5.61  
    5.62  
    5.63 @@ -651,6 +642,46 @@
    5.64  qed
    5.65  
    5.66  
    5.67 +(* Next lemma contributed by Paulo Emílio de Vilhena. *)
    5.68 +
    5.69 +text \<open>This next lemma would be trivial if placed in a theory that imports QuotRing,
    5.70 +      but it makes more sense to have it here (easier to find and coherent with the
    5.71 +      previous developments).\<close>
    5.72 +
    5.73 +lemma (in cring) cgenideal_prod:
    5.74 +  assumes "a \<in> carrier R" "b \<in> carrier R"
    5.75 +  shows "(PIdl a) <#> (PIdl b) = PIdl (a \<otimes> b)"
    5.76 +proof -
    5.77 +  have "(carrier R #> a) <#> (carrier R #> b) = carrier R #> (a \<otimes> b)"
    5.78 +  proof
    5.79 +    show "(carrier R #> a) <#> (carrier R #> b) \<subseteq> carrier R #> a \<otimes> b"
    5.80 +    proof
    5.81 +      fix x assume "x \<in> (carrier R #> a) <#> (carrier R #> b)"
    5.82 +      then obtain r1 r2 where r1: "r1 \<in> carrier R" and r2: "r2 \<in> carrier R"
    5.83 +                          and "x = (r1 \<otimes> a) \<otimes> (r2 \<otimes> b)"
    5.84 +        unfolding set_mult_def r_coset_def by blast
    5.85 +      hence "x = (r1 \<otimes> r2) \<otimes> (a \<otimes> b)"
    5.86 +        by (simp add: assms local.ring_axioms m_lcomm ring.ring_simprules(11))
    5.87 +      thus "x \<in> carrier R #> a \<otimes> b"
    5.88 +        unfolding r_coset_def using r1 r2 assms by blast 
    5.89 +    qed
    5.90 +  next
    5.91 +    show "carrier R #> a \<otimes> b \<subseteq> (carrier R #> a) <#> (carrier R #> b)"
    5.92 +    proof
    5.93 +      fix x assume "x \<in> carrier R #> a \<otimes> b"
    5.94 +      then obtain r where r: "r \<in> carrier R" "x = r \<otimes> (a \<otimes> b)"
    5.95 +        unfolding r_coset_def by blast
    5.96 +      hence "x = (r \<otimes> a) \<otimes> (\<one> \<otimes> b)"
    5.97 +        using assms by (simp add: m_assoc)
    5.98 +      thus "x \<in> (carrier R #> a) <#> (carrier R #> b)"
    5.99 +        unfolding set_mult_def r_coset_def using assms r by blast
   5.100 +    qed
   5.101 +  qed
   5.102 +  thus ?thesis
   5.103 +    using cgenideal_eq_rcos[of a] cgenideal_eq_rcos[of b] cgenideal_eq_rcos[of "a \<otimes> b"] by simp
   5.104 +qed
   5.105 +
   5.106 +
   5.107  subsection \<open>Prime Ideals\<close>
   5.108  
   5.109  lemma (in ideal) primeidealCD:
   5.110 @@ -918,7 +949,7 @@
   5.111    qed
   5.112  qed (simp add: zeroideal oneideal)
   5.113  
   5.114 -\<comment> \<open>Jacobson Theorem 2.2\<close>
   5.115 +\<comment>\<open>"Jacobson Theorem 2.2"\<close>
   5.116  lemma (in cring) trivialideals_eq_field:
   5.117    assumes carrnzero: "carrier R \<noteq> {\<zero>}"
   5.118    shows "({I. ideal I R} = {{\<zero>}, carrier R}) = field R"
     6.1 --- a/src/HOL/Algebra/More_Finite_Product.thy	Tue Jun 12 16:09:12 2018 +0100
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,102 +0,0 @@
     6.4 -(*  Title:      HOL/Algebra/More_Finite_Product.thy
     6.5 -    Author:     Jeremy Avigad
     6.6 -*)
     6.7 -
     6.8 -section \<open>More on finite products\<close>
     6.9 -
    6.10 -theory More_Finite_Product
    6.11 -  imports More_Group
    6.12 -begin
    6.13 -
    6.14 -lemma (in comm_monoid) finprod_UN_disjoint:
    6.15 -  "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>
    6.16 -    (\<forall>i\<in>I. \<forall>x \<in> A i. g x \<in> carrier G) \<longrightarrow>
    6.17 -    finprod G g (UNION I A) = finprod G (\<lambda>i. finprod G g (A i)) I"
    6.18 -  apply (induct set: finite)
    6.19 -   apply force
    6.20 -  apply clarsimp
    6.21 -  apply (subst finprod_Un_disjoint)
    6.22 -       apply blast
    6.23 -      apply (erule finite_UN_I)
    6.24 -      apply blast
    6.25 -     apply (fastforce)
    6.26 -    apply (auto intro!: funcsetI finprod_closed)
    6.27 -  done
    6.28 -
    6.29 -lemma (in comm_monoid) finprod_Union_disjoint:
    6.30 -  "finite C \<Longrightarrow>
    6.31 -    \<forall>A\<in>C. finite A \<and> (\<forall>x\<in>A. f x \<in> carrier G) \<Longrightarrow>
    6.32 -    \<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A \<inter> B = {} \<Longrightarrow>
    6.33 -    finprod G f (\<Union>C) = finprod G (finprod G f) C"
    6.34 -  apply (frule finprod_UN_disjoint [of C id f])
    6.35 -  apply auto
    6.36 -  done
    6.37 -
    6.38 -lemma (in comm_monoid) finprod_one: "finite A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x = \<one>) \<Longrightarrow> finprod G f A = \<one>"
    6.39 -  by (induct set: finite) auto
    6.40 -
    6.41 -
    6.42 -(* need better simplification rules for rings *)
    6.43 -(* the next one holds more generally for abelian groups *)
    6.44 -
    6.45 -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"
    6.46 -  by (metis minus_equality)
    6.47 -
    6.48 -lemma (in domain) square_eq_one:
    6.49 -  fixes x
    6.50 -  assumes [simp]: "x \<in> carrier R"
    6.51 -    and "x \<otimes> x = \<one>"
    6.52 -  shows "x = \<one> \<or> x = \<ominus>\<one>"
    6.53 -proof -
    6.54 -  have "(x \<oplus> \<one>) \<otimes> (x \<oplus> \<ominus> \<one>) = x \<otimes> x \<oplus> \<ominus> \<one>"
    6.55 -    by (simp add: ring_simprules)
    6.56 -  also from \<open>x \<otimes> x = \<one>\<close> have "\<dots> = \<zero>"
    6.57 -    by (simp add: ring_simprules)
    6.58 -  finally have "(x \<oplus> \<one>) \<otimes> (x \<oplus> \<ominus> \<one>) = \<zero>" .
    6.59 -  then have "(x \<oplus> \<one>) = \<zero> \<or> (x \<oplus> \<ominus> \<one>) = \<zero>"
    6.60 -    by (intro integral) auto
    6.61 -  then show ?thesis
    6.62 -    apply auto
    6.63 -     apply (erule notE)
    6.64 -     apply (rule sum_zero_eq_neg)
    6.65 -       apply auto
    6.66 -    apply (subgoal_tac "x = \<ominus> (\<ominus> \<one>)")
    6.67 -     apply (simp add: ring_simprules)
    6.68 -    apply (rule sum_zero_eq_neg)
    6.69 -      apply auto
    6.70 -    done
    6.71 -qed
    6.72 -
    6.73 -lemma (in domain) inv_eq_self: "x \<in> Units R \<Longrightarrow> x = inv x \<Longrightarrow> x = \<one> \<or> x = \<ominus>\<one>"
    6.74 -  by (metis Units_closed Units_l_inv square_eq_one)
    6.75 -
    6.76 -
    6.77 -text \<open>
    6.78 -  The following translates theorems about groups to the facts about
    6.79 -  the units of a ring. (The list should be expanded as more things are
    6.80 -  needed.)
    6.81 -\<close>
    6.82 -
    6.83 -lemma (in ring) finite_ring_finite_units [intro]: "finite (carrier R) \<Longrightarrow> finite (Units R)"
    6.84 -  by (rule finite_subset) auto
    6.85 -
    6.86 -lemma (in monoid) units_of_pow:
    6.87 -  fixes n :: nat
    6.88 -  shows "x \<in> Units G \<Longrightarrow> x [^]\<^bsub>units_of G\<^esub> n = x [^]\<^bsub>G\<^esub> n"
    6.89 -  apply (induct n)
    6.90 -  apply (auto simp add: units_group group.is_monoid
    6.91 -    monoid.nat_pow_0 monoid.nat_pow_Suc units_of_one units_of_mult)
    6.92 -  done
    6.93 -
    6.94 -lemma (in cring) units_power_order_eq_one:
    6.95 -  "finite (Units R) \<Longrightarrow> a \<in> Units R \<Longrightarrow> a [^] card(Units R) = \<one>"
    6.96 -  apply (subst units_of_carrier [symmetric])
    6.97 -  apply (subst units_of_one [symmetric])
    6.98 -  apply (subst units_of_pow [symmetric])
    6.99 -   apply assumption
   6.100 -  apply (rule comm_group.power_order_eq_one)
   6.101 -    apply (rule units_comm_group)
   6.102 -   apply (unfold units_of_def, auto)
   6.103 -  done
   6.104 -
   6.105 -end
     7.1 --- a/src/HOL/Algebra/More_Group.thy	Tue Jun 12 16:09:12 2018 +0100
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,115 +0,0 @@
     7.4 -(*  Title:      HOL/Algebra/More_Group.thy
     7.5 -    Author:     Jeremy Avigad
     7.6 -*)
     7.7 -
     7.8 -section \<open>More on groups\<close>
     7.9 -
    7.10 -theory More_Group
    7.11 -  imports Ring
    7.12 -begin
    7.13 -
    7.14 -text \<open>
    7.15 -  Show that the units in any monoid give rise to a group.
    7.16 -
    7.17 -  The file Residues.thy provides some infrastructure to use
    7.18 -  facts about the unit group within the ring locale.
    7.19 -\<close>
    7.20 -
    7.21 -definition units_of :: "('a, 'b) monoid_scheme \<Rightarrow> 'a monoid"
    7.22 -  where "units_of G =
    7.23 -    \<lparr>carrier = Units G, Group.monoid.mult = Group.monoid.mult G, one  = one G\<rparr>"
    7.24 -
    7.25 -lemma (in monoid) units_group: "group (units_of G)"
    7.26 -  apply (unfold units_of_def)
    7.27 -  apply (rule groupI)
    7.28 -      apply auto
    7.29 -   apply (subst m_assoc)
    7.30 -      apply auto
    7.31 -  apply (rule_tac x = "inv x" in bexI)
    7.32 -   apply auto
    7.33 -  done
    7.34 -
    7.35 -lemma (in comm_monoid) units_comm_group: "comm_group (units_of G)"
    7.36 -  apply (rule group.group_comm_groupI)
    7.37 -   apply (rule units_group)
    7.38 -  apply (insert comm_monoid_axioms)
    7.39 -  apply (unfold units_of_def Units_def comm_monoid_def comm_monoid_axioms_def)
    7.40 -  apply auto
    7.41 -  done
    7.42 -
    7.43 -lemma units_of_carrier: "carrier (units_of G) = Units G"
    7.44 -  by (auto simp: units_of_def)
    7.45 -
    7.46 -lemma units_of_mult: "mult (units_of G) = mult G"
    7.47 -  by (auto simp: units_of_def)
    7.48 -
    7.49 -lemma units_of_one: "one (units_of G) = one G"
    7.50 -  by (auto simp: units_of_def)
    7.51 -
    7.52 -lemma (in monoid) units_of_inv: "x \<in> Units G \<Longrightarrow> m_inv (units_of G) x = m_inv G x"
    7.53 -  apply (rule sym)
    7.54 -  apply (subst m_inv_def)
    7.55 -  apply (rule the1_equality)
    7.56 -   apply (rule ex_ex1I)
    7.57 -    apply (subst (asm) Units_def)
    7.58 -    apply auto
    7.59 -     apply (erule inv_unique)
    7.60 -        apply auto
    7.61 -    apply (rule Units_closed)
    7.62 -    apply (simp_all only: units_of_carrier [symmetric])
    7.63 -    apply (insert units_group)
    7.64 -    apply auto
    7.65 -   apply (subst units_of_mult [symmetric])
    7.66 -   apply (subst units_of_one [symmetric])
    7.67 -   apply (erule group.r_inv, assumption)
    7.68 -  apply (subst units_of_mult [symmetric])
    7.69 -  apply (subst units_of_one [symmetric])
    7.70 -  apply (erule group.l_inv, assumption)
    7.71 -  done
    7.72 -
    7.73 -lemma (in group) inj_on_const_mult: "a \<in> carrier G \<Longrightarrow> inj_on (\<lambda>x. a \<otimes> x) (carrier G)"
    7.74 -  unfolding inj_on_def by auto
    7.75 -
    7.76 -lemma (in group) surj_const_mult: "a \<in> carrier G \<Longrightarrow> (\<lambda>x. a \<otimes> x) ` carrier G = carrier G"
    7.77 -  apply (auto simp add: image_def)
    7.78 -  apply (rule_tac x = "(m_inv G a) \<otimes> x" in bexI)
    7.79 -  apply auto
    7.80 -(* auto should get this. I suppose we need "comm_monoid_simprules"
    7.81 -   for ac_simps rewriting. *)
    7.82 -  apply (subst m_assoc [symmetric])
    7.83 -  apply auto
    7.84 -  done
    7.85 -
    7.86 -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"
    7.87 -  by (metis Units_eq Units_l_cancel monoid.r_one monoid_axioms one_closed)
    7.88 -
    7.89 -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"
    7.90 -  by (metis monoid.l_one monoid_axioms one_closed right_cancel)
    7.91 -
    7.92 -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"
    7.93 -  using l_cancel_one by fastforce
    7.94 -
    7.95 -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"
    7.96 -  using r_cancel_one by fastforce
    7.97 -
    7.98 -(* This should be generalized to arbitrary groups, not just commutative
    7.99 -   ones, using Lagrange's theorem. *)
   7.100 -
   7.101 -lemma (in comm_group) power_order_eq_one:
   7.102 -  assumes fin [simp]: "finite (carrier G)"
   7.103 -    and a [simp]: "a \<in> carrier G"
   7.104 -  shows "a [^] card(carrier G) = one G"
   7.105 -proof -
   7.106 -  have "(\<Otimes>x\<in>carrier G. x) = (\<Otimes>x\<in>carrier G. a \<otimes> x)"
   7.107 -    by (subst (2) finprod_reindex [symmetric],
   7.108 -      auto simp add: Pi_def inj_on_const_mult surj_const_mult)
   7.109 -  also have "\<dots> = (\<Otimes>x\<in>carrier G. a) \<otimes> (\<Otimes>x\<in>carrier G. x)"
   7.110 -    by (auto simp add: finprod_multf Pi_def)
   7.111 -  also have "(\<Otimes>x\<in>carrier G. a) = a [^] card(carrier G)"
   7.112 -    by (auto simp add: finprod_const)
   7.113 -  finally show ?thesis
   7.114 -(* uses the preceeding lemma *)
   7.115 -    by auto
   7.116 -qed
   7.117 -
   7.118 -end
     8.1 --- a/src/HOL/Algebra/More_Ring.thy	Tue Jun 12 16:09:12 2018 +0100
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,74 +0,0 @@
     8.4 -(*  Title:      HOL/Algebra/More_Ring.thy
     8.5 -    Author:     Jeremy Avigad
     8.6 -*)
     8.7 -
     8.8 -section \<open>More on rings etc.\<close>
     8.9 -
    8.10 -theory More_Ring
    8.11 -  imports Ring
    8.12 -begin
    8.13 -
    8.14 -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"
    8.15 -  apply (unfold_locales)
    8.16 -    apply (use cring_axioms in auto)
    8.17 -   apply (rule trans)
    8.18 -    apply (subgoal_tac "a = (a \<otimes> b) \<otimes> inv b")
    8.19 -     apply assumption
    8.20 -    apply (subst m_assoc)
    8.21 -       apply auto
    8.22 -  apply (unfold Units_def)
    8.23 -  apply auto
    8.24 -  done
    8.25 -
    8.26 -lemma (in monoid) inv_char:
    8.27 -  "x \<in> carrier G \<Longrightarrow> y \<in> carrier G \<Longrightarrow> x \<otimes> y = \<one> \<Longrightarrow> y \<otimes> x = \<one> \<Longrightarrow> inv x = y"
    8.28 -  apply (subgoal_tac "x \<in> Units G")
    8.29 -   apply (subgoal_tac "y = inv x \<otimes> \<one>")
    8.30 -    apply simp
    8.31 -   apply (erule subst)
    8.32 -   apply (subst m_assoc [symmetric])
    8.33 -      apply auto
    8.34 -  apply (unfold Units_def)
    8.35 -  apply auto
    8.36 -  done
    8.37 -
    8.38 -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"
    8.39 -  apply (rule inv_char)
    8.40 -     apply auto
    8.41 -  apply (subst m_comm, auto)
    8.42 -  done
    8.43 -
    8.44 -lemma (in ring) inv_neg_one [simp]: "inv (\<ominus> \<one>) = \<ominus> \<one>"
    8.45 -  apply (rule inv_char)
    8.46 -     apply (auto simp add: l_minus r_minus)
    8.47 -  done
    8.48 -
    8.49 -lemma (in monoid) inv_eq_imp_eq: "x \<in> Units G \<Longrightarrow> y \<in> Units G \<Longrightarrow> inv x = inv y \<Longrightarrow> x = y"
    8.50 -  apply (subgoal_tac "inv (inv x) = inv (inv y)")
    8.51 -   apply (subst (asm) Units_inv_inv)+
    8.52 -    apply auto
    8.53 -  done
    8.54 -
    8.55 -lemma (in ring) Units_minus_one_closed [intro]: "\<ominus> \<one> \<in> Units R"
    8.56 -  apply (unfold Units_def)
    8.57 -  apply auto
    8.58 -  apply (rule_tac x = "\<ominus> \<one>" in bexI)
    8.59 -   apply auto
    8.60 -  apply (simp add: l_minus r_minus)
    8.61 -  done
    8.62 -
    8.63 -lemma (in monoid) inv_one [simp]: "inv \<one> = \<one>"
    8.64 -  apply (rule inv_char)
    8.65 -     apply auto
    8.66 -  done
    8.67 -
    8.68 -lemma (in ring) inv_eq_neg_one_eq: "x \<in> Units R \<Longrightarrow> inv x = \<ominus> \<one> \<longleftrightarrow> x = \<ominus> \<one>"
    8.69 -  apply auto
    8.70 -  apply (subst Units_inv_inv [symmetric])
    8.71 -   apply auto
    8.72 -  done
    8.73 -
    8.74 -lemma (in monoid) inv_eq_one_eq: "x \<in> Units G \<Longrightarrow> inv x = \<one> \<longleftrightarrow> x = \<one>"
    8.75 -  by (metis Units_inv_inv inv_one)
    8.76 -
    8.77 -end
     9.1 --- a/src/HOL/Algebra/Multiplicative_Group.thy	Tue Jun 12 16:09:12 2018 +0100
     9.2 +++ b/src/HOL/Algebra/Multiplicative_Group.thy	Thu Jun 14 14:23:38 2018 +0100
     9.3 @@ -7,8 +7,6 @@
     9.4  imports
     9.5    Complex_Main
     9.6    Group
     9.7 -  More_Group
     9.8 -  More_Finite_Product
     9.9    Coset
    9.10    UnivPoly
    9.11  begin
    10.1 --- a/src/HOL/Algebra/Ring.thy	Tue Jun 12 16:09:12 2018 +0100
    10.2 +++ b/src/HOL/Algebra/Ring.thy	Thu Jun 14 14:23:38 2018 +0100
    10.3 @@ -25,10 +25,9 @@
    10.4    a_inv :: "[('a, 'm) ring_scheme, 'a ] \<Rightarrow> 'a" ("\<ominus>\<index> _" [81] 80)
    10.5    where "a_inv R = m_inv (add_monoid R)"
    10.6  
    10.7 -
    10.8  definition
    10.9    a_minus :: "[('a, 'm) ring_scheme, 'a, 'a] => 'a" ("(_ \<ominus>\<index> _)" [65,66] 65)
   10.10 -  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)"
   10.11 +  where "x \<ominus>\<^bsub>R\<^esub> y = x \<oplus>\<^bsub>R\<^esub> (\<ominus>\<^bsub>R\<^esub> y)"
   10.12  
   10.13  definition
   10.14    add_pow :: "[_, ('b :: semiring_1), 'a] \<Rightarrow> 'a" ("[_] \<cdot>\<index> _" [81, 81] 80)
   10.15 @@ -212,7 +211,6 @@
   10.16  
   10.17  lemmas l_neg = add.l_inv [simp del]
   10.18  lemmas r_neg = add.r_inv [simp del]
   10.19 -lemmas minus_zero = add.inv_one
   10.20  lemmas minus_minus = add.inv_inv
   10.21  lemmas a_inv_inj = add.inv_inj
   10.22  lemmas minus_equality = add.inv_equality
   10.23 @@ -344,6 +342,8 @@
   10.24  lemma (in cring) is_cring:
   10.25    "cring R" by (rule cring_axioms)
   10.26  
   10.27 +lemma (in ring) minus_zero [simp]: "\<ominus> \<zero> = \<zero>"
   10.28 +  by (simp add: a_inv_def)
   10.29  
   10.30  subsubsection \<open>Normaliser for Rings\<close>
   10.31  
   10.32 @@ -416,9 +416,8 @@
   10.33  
   10.34  end
   10.35  
   10.36 -lemma (in abelian_group) minus_eq:
   10.37 -  "\<lbrakk> x \<in> carrier G; y \<in> carrier G \<rbrakk> \<Longrightarrow> x \<ominus> y = x \<oplus> (\<ominus> y)"
   10.38 -  by (simp only: a_minus_def)
   10.39 +lemma (in abelian_group) minus_eq: "x \<ominus> y = x \<oplus> (\<ominus> y)"
   10.40 +  by (rule a_minus_def)
   10.41  
   10.42  text \<open>Setup algebra method:
   10.43    compute distributive normal form in locale contexts\<close>
   10.44 @@ -602,7 +601,6 @@
   10.45      using add_pow_int_lt[of k R b] add_pow_int_lt[of k R "a \<otimes> b"]
   10.46            add_pow_rdistr[OF assms, of "nat (- k)"] assms r_minus by auto 
   10.47  qed
   10.48 -(* ************************************************************************** *)
   10.49  
   10.50  
   10.51  subsection \<open>Integral Domains\<close>
   10.52 @@ -631,7 +629,7 @@
   10.53    with R have "a \<otimes> (b \<ominus> c) = \<zero>" by algebra
   10.54    with R have "a = \<zero> \<or> (b \<ominus> c) = \<zero>" by (simp add: integral_iff)
   10.55    with prem and R have "b \<ominus> c = \<zero>" by auto 
   10.56 -  with R have "b = b \<ominus> (b \<ominus> c)" by algebra 
   10.57 +  with R have "b = b \<ominus> (b \<ominus> c)" by algebra
   10.58    also from R have "b \<ominus> (b \<ominus> c) = c" by algebra
   10.59    finally show "b = c" .
   10.60  next
   10.61 @@ -805,4 +803,111 @@
   10.62    "\<lbrakk> f \<in> ring_hom R S; g \<in> ring_hom S T \<rbrakk> \<Longrightarrow> g \<circ> f \<in> ring_hom R T"
   10.63    by (rule ring_hom_memI) (auto simp add: ring_hom_closed ring_hom_mult ring_hom_add ring_hom_one)
   10.64  
   10.65 +subsection\<open>Jeremy Avigad's @{text"More_Finite_Product"} material\<close>
   10.66 +
   10.67 +(* need better simplification rules for rings *)
   10.68 +(* the next one holds more generally for abelian groups *)
   10.69 +
   10.70 +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"
   10.71 +  by (metis minus_equality)
   10.72 +
   10.73 +lemma (in domain) square_eq_one:
   10.74 +  fixes x
   10.75 +  assumes [simp]: "x \<in> carrier R"
   10.76 +    and "x \<otimes> x = \<one>"
   10.77 +  shows "x = \<one> \<or> x = \<ominus>\<one>"
   10.78 +proof -
   10.79 +  have "(x \<oplus> \<one>) \<otimes> (x \<oplus> \<ominus> \<one>) = x \<otimes> x \<oplus> \<ominus> \<one>"
   10.80 +    by (simp add: ring_simprules)
   10.81 +  also from \<open>x \<otimes> x = \<one>\<close> have "\<dots> = \<zero>"
   10.82 +    by (simp add: ring_simprules)
   10.83 +  finally have "(x \<oplus> \<one>) \<otimes> (x \<oplus> \<ominus> \<one>) = \<zero>" .
   10.84 +  then have "(x \<oplus> \<one>) = \<zero> \<or> (x \<oplus> \<ominus> \<one>) = \<zero>"
   10.85 +    by (intro integral) auto
   10.86 +  then show ?thesis
   10.87 +    by (metis add.inv_closed add.inv_solve_right assms(1) l_zero one_closed zero_closed)
   10.88 +qed
   10.89 +
   10.90 +lemma (in domain) inv_eq_self: "x \<in> Units R \<Longrightarrow> x = inv x \<Longrightarrow> x = \<one> \<or> x = \<ominus>\<one>"
   10.91 +  by (metis Units_closed Units_l_inv square_eq_one)
   10.92 +
   10.93 +
   10.94 +text \<open>
   10.95 +  The following translates theorems about groups to the facts about
   10.96 +  the units of a ring. (The list should be expanded as more things are
   10.97 +  needed.)
   10.98 +\<close>
   10.99 +
  10.100 +lemma (in ring) finite_ring_finite_units [intro]: "finite (carrier R) \<Longrightarrow> finite (Units R)"
  10.101 +  by (rule finite_subset) auto
  10.102 +
  10.103 +lemma (in monoid) units_of_pow:
  10.104 +  fixes n :: nat
  10.105 +  shows "x \<in> Units G \<Longrightarrow> x [^]\<^bsub>units_of G\<^esub> n = x [^]\<^bsub>G\<^esub> n"
  10.106 +  apply (induct n)
  10.107 +  apply (auto simp add: units_group group.is_monoid
  10.108 +    monoid.nat_pow_0 monoid.nat_pow_Suc units_of_one units_of_mult)
  10.109 +  done
  10.110 +
  10.111 +lemma (in cring) units_power_order_eq_one:
  10.112 +  "finite (Units R) \<Longrightarrow> a \<in> Units R \<Longrightarrow> a [^] card(Units R) = \<one>"
  10.113 +  by (metis comm_group.power_order_eq_one units_comm_group units_of_carrier units_of_one units_of_pow)
  10.114 +
  10.115 +subsection\<open>Jeremy Avigad's @{text"More_Ring"} material\<close>
  10.116 +
  10.117 +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"
  10.118 +  apply (unfold_locales)
  10.119 +    apply (use cring_axioms in auto)
  10.120 +   apply (rule trans)
  10.121 +    apply (subgoal_tac "a = (a \<otimes> b) \<otimes> inv b")
  10.122 +     apply assumption
  10.123 +    apply (subst m_assoc)
  10.124 +       apply auto
  10.125 +  apply (unfold Units_def)
  10.126 +  apply auto
  10.127 +  done
  10.128 +
  10.129 +lemma (in monoid) inv_char:
  10.130 +  "x \<in> carrier G \<Longrightarrow> y \<in> carrier G \<Longrightarrow> x \<otimes> y = \<one> \<Longrightarrow> y \<otimes> x = \<one> \<Longrightarrow> inv x = y"
  10.131 +  apply (subgoal_tac "x \<in> Units G")
  10.132 +   apply (subgoal_tac "y = inv x \<otimes> \<one>")
  10.133 +    apply simp
  10.134 +   apply (erule subst)
  10.135 +   apply (subst m_assoc [symmetric])
  10.136 +      apply auto
  10.137 +  apply (unfold Units_def)
  10.138 +  apply auto
  10.139 +  done
  10.140 +
  10.141 +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"
  10.142 +  by (simp add: inv_char m_comm)
  10.143 +
  10.144 +lemma (in ring) inv_neg_one [simp]: "inv (\<ominus> \<one>) = \<ominus> \<one>"
  10.145 +  apply (rule inv_char)
  10.146 +     apply (auto simp add: l_minus r_minus)
  10.147 +  done
  10.148 +
  10.149 +lemma (in monoid) inv_eq_imp_eq: "x \<in> Units G \<Longrightarrow> y \<in> Units G \<Longrightarrow> inv x = inv y \<Longrightarrow> x = y"
  10.150 +  apply (subgoal_tac "inv (inv x) = inv (inv y)")
  10.151 +   apply (subst (asm) Units_inv_inv)+
  10.152 +    apply auto
  10.153 +  done
  10.154 +
  10.155 +lemma (in ring) Units_minus_one_closed [intro]: "\<ominus> \<one> \<in> Units R"
  10.156 +  apply (unfold Units_def)
  10.157 +  apply auto
  10.158 +  apply (rule_tac x = "\<ominus> \<one>" in bexI)
  10.159 +   apply auto
  10.160 +  apply (simp add: l_minus r_minus)
  10.161 +  done
  10.162 +
  10.163 +lemma (in ring) inv_eq_neg_one_eq: "x \<in> Units R \<Longrightarrow> inv x = \<ominus> \<one> \<longleftrightarrow> x = \<ominus> \<one>"
  10.164 +  apply auto
  10.165 +  apply (subst Units_inv_inv [symmetric])
  10.166 +   apply auto
  10.167 +  done
  10.168 +
  10.169 +lemma (in monoid) inv_eq_one_eq: "x \<in> Units G \<Longrightarrow> inv x = \<one> \<longleftrightarrow> x = \<one>"
  10.170 +  by (metis Units_inv_inv inv_one)
  10.171 +
  10.172  end
    11.1 --- a/src/HOL/Algebra/Sylow.thy	Tue Jun 12 16:09:12 2018 +0100
    11.2 +++ b/src/HOL/Algebra/Sylow.thy	Thu Jun 14 14:23:38 2018 +0100
    11.3 @@ -223,7 +223,7 @@
    11.4  
    11.5  lemma M_funcset_rcosets_H:
    11.6    "(\<lambda>x\<in>M. H #> (SOME g. g \<in> carrier G \<and> M1 #> g = x)) \<in> M \<rightarrow> rcosets H"
    11.7 -  by (metis (lifting) H_is_subgroup M_elem_map_carrier rcosetsI restrictI subgroup_imp_subset)
    11.8 +  by (metis (lifting) H_is_subgroup M_elem_map_carrier rcosetsI restrictI subgroup.subset)
    11.9  
   11.10  lemma inj_M_GmodH: "\<exists>f \<in> M \<rightarrow> rcosets H. inj_on f M"
   11.11    apply (rule bexI)
    12.1 --- a/src/HOL/Algebra/UnivPoly.thy	Tue Jun 12 16:09:12 2018 +0100
    12.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Thu Jun 14 14:23:38 2018 +0100
    12.3 @@ -116,14 +116,15 @@
    12.4  proof
    12.5    assume R: "p \<in> up R"
    12.6    then obtain n where "bound \<zero> n p" by auto
    12.7 -  then have "bound \<zero> n (\<lambda>i. \<ominus> p i)" by auto
    12.8 +  then have "bound \<zero> n (\<lambda>i. \<ominus> p i)"
    12.9 +    by (simp add: bound_def minus_equality)
   12.10    then show "\<exists>n. bound \<zero> n (\<lambda>i. \<ominus> p i)" by auto
   12.11  qed auto
   12.12  
   12.13  lemma up_minus_closed:
   12.14    "[| p \<in> up R; q \<in> up R |] ==> (\<lambda>i. p i \<ominus> q i) \<in> up R"
   12.15 -  using mem_upD [of p R] mem_upD [of q R] up_add_closed up_a_inv_closed a_minus_def [of _ R]
   12.16 -  by auto
   12.17 +  unfolding a_minus_def
   12.18 +  using mem_upD [of p R] mem_upD [of q R] up_add_closed up_a_inv_closed  by auto
   12.19  
   12.20  lemma up_mult_closed:
   12.21    "[| p \<in> up R; q \<in> up R |] ==>
   12.22 @@ -695,7 +696,7 @@
   12.23  
   12.24  lemma monom_a_inv [simp]:
   12.25    "a \<in> carrier R ==> monom P (\<ominus> a) n = \<ominus>\<^bsub>P\<^esub> monom P a n"
   12.26 -  by (rule up_eqI) simp_all
   12.27 +  by (rule up_eqI) auto
   12.28  
   12.29  lemma monom_inj:
   12.30    "inj_on (\<lambda>a. monom P a n) (carrier R)"
   12.31 @@ -1462,9 +1463,9 @@
   12.32  subsection\<open>The long division algorithm: some previous facts.\<close>
   12.33  
   12.34  lemma coeff_minus [simp]:
   12.35 -  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"
   12.36 -  unfolding a_minus_def [OF p q] unfolding coeff_add [OF p a_inv_closed [OF q]] unfolding coeff_a_inv [OF q]
   12.37 -  using coeff_closed [OF p, of n] using coeff_closed [OF q, of n] by algebra
   12.38 +  assumes p: "p \<in> carrier P" and q: "q \<in> carrier P" 
   12.39 +  shows "coeff P (p \<ominus>\<^bsub>P\<^esub> q) n = coeff P p n \<ominus> coeff P q n"
   12.40 +  by (simp add: a_minus_def p q)
   12.41  
   12.42  lemma lcoeff_closed [simp]: assumes p: "p \<in> carrier P" shows "lcoeff p \<in> carrier R"
   12.43    using coeff_closed [OF p, of "deg R p"] by simp
   12.44 @@ -1719,10 +1720,7 @@
   12.45      and min_mon0_closed: "\<ominus>\<^bsub>P\<^esub> monom P a 0 \<in> carrier P"
   12.46      using a R.a_inv_closed by auto
   12.47    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)"
   12.48 -    unfolding P.minus_eq [OF mon1_closed mon0_closed]
   12.49 -    unfolding hom_add [OF mon1_closed min_mon0_closed]
   12.50 -    unfolding hom_a_inv [OF mon0_closed]
   12.51 -    using R.minus_eq [symmetric] mon1_closed mon0_closed by auto
   12.52 +    by (simp add: a_minus_def mon0_closed)
   12.53    also have "\<dots> = a \<ominus> a"
   12.54      using eval_monom [OF R.one_closed a, of 1] using eval_monom [OF a a, of 0] using a by simp
   12.55    also have "\<dots> = \<zero>"
    13.1 --- a/src/HOL/Algebra/Zassenhaus.thy	Tue Jun 12 16:09:12 2018 +0100
    13.2 +++ b/src/HOL/Algebra/Zassenhaus.thy	Thu Jun 14 14:23:38 2018 +0100
    13.3 @@ -2,220 +2,8 @@
    13.4    imports Coset Group_Action
    13.5  begin
    13.6  
    13.7 -subsection "fundamental lemmas"
    13.8  
    13.9 -
   13.10 -text "Lemmas about subgroups"
   13.11 -
   13.12 -
   13.13 -(*A subgroup included in another subgroup is a subgroup of the subgroup*)
   13.14 -lemma (in group) subgroup_incl :
   13.15 -  assumes "subgroup I G"
   13.16 -    and "subgroup J G"
   13.17 -    and "I\<subseteq>J"
   13.18 -  shows "subgroup I (G\<lparr>carrier:=J\<rparr>)"using assms subgroup_inv_equality
   13.19 -  by (auto simp add: subgroup_def)
   13.20 -
   13.21 -(*A subgroup of a subgroup is a subgroup of the group*)
   13.22 -lemma (in group) incl_subgroup :
   13.23 -  assumes "subgroup J G"
   13.24 -    and "subgroup I (G\<lparr>carrier:=J\<rparr>)"
   13.25 -  shows "subgroup I G" unfolding subgroup_def
   13.26 -proof
   13.27 -  have H1: "I \<subseteq> carrier (G\<lparr>carrier:=J\<rparr>)" using assms(2) subgroup_imp_subset by blast
   13.28 -  also have H2: "...\<subseteq>J" by simp
   13.29 -  also  have "...\<subseteq>(carrier G)"  by (simp add: assms(1) subgroup_imp_subset)
   13.30 -  finally have H: "I \<subseteq> carrier G" by simp
   13.31 -  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)
   13.32 -  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
   13.33 -  have K: "\<one> \<in> I" using assms(2) by (auto simp add: subgroup_def)
   13.34 -  have "(\<And>x. x \<in> I \<Longrightarrow> inv x \<in> I)" using assms  subgroup.m_inv_closed H
   13.35 -    by (metis H1 H2  subgroup_inv_equality subsetCE)
   13.36 -  thus "\<one> \<in> I \<and> (\<forall>x. x \<in> I \<longrightarrow> inv x \<in> I)" using K by blast
   13.37 -qed
   13.38 -
   13.39 -
   13.40 -text "Lemmas about set_mult"
   13.41 -
   13.42 -
   13.43 -lemma (in group) set_mult_same_law :
   13.44 -  assumes "subgroup H G"
   13.45 -and "K1 \<subseteq> H"
   13.46 -and "K2 \<subseteq> H"
   13.47 -shows "K1<#>\<^bsub>(G\<lparr>carrier:=H\<rparr>)\<^esub>K2 = K1<#>K2"
   13.48 -proof 
   13.49 -  show "K1 <#>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> K2 \<subseteq> K1 <#> K2"
   13.50 -  proof
   13.51 -    fix h assume Hyph : "h\<in>K1<#>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub>K2"
   13.52 -    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"
   13.53 -      unfolding set_mult_def by blast
   13.54 -    hence "k1\<in>H" using assms by blast
   13.55 -    moreover have  "k2\<in>H" using Hyp assms by blast
   13.56 -    ultimately have EGAL : "k1 \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> k2 = k1 \<otimes>\<^bsub>G\<^esub> k2" by simp
   13.57 -    have "k1 \<otimes>\<^bsub>G\<^esub> k2 \<in> K1<#>K2" unfolding  set_mult_def using Hyp by blast
   13.58 -    hence "k1 \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> k2 \<in> K1<#>K2" using EGAL by auto
   13.59 -    thus "h \<in> K1<#>K2 " using Hyp by blast
   13.60 -  qed
   13.61 -  show "K1 <#> K2 \<subseteq> K1 <#>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> K2"
   13.62 -  proof
   13.63 -    fix h assume Hyph : "h\<in>K1<#>K2"
   13.64 -    then obtain k1 k2 where Hyp : "k1\<in>K1 \<and> k2\<in>K2 \<and> k1\<otimes>k2 = h" unfolding set_mult_def by blast
   13.65 -    hence k1H: "k1\<in>H" using assms by blast
   13.66 -    have  k2H: "k2\<in>H" using Hyp assms by blast
   13.67 -    have EGAL : "k1 \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> k2 = k1 \<otimes>\<^bsub>G\<^esub> k2" using k1H k2H by simp
   13.68 -    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
   13.69 -    hence "k1 \<otimes> k2 \<in> K1<#>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub>K2" using EGAL by auto
   13.70 -    thus "h \<in> K1<#>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub>K2 " using Hyp by blast
   13.71 -  qed
   13.72 -qed
   13.73 -
   13.74 -
   13.75 -(*A group multiplied by a subgroup stays the same*)
   13.76 -lemma (in group) set_mult_carrier_idem :
   13.77 -  assumes "subgroup H G"
   13.78 -  shows "(carrier G)<#>H = carrier G"
   13.79 -proof
   13.80 -  show "(carrier G)<#>H \<subseteq> carrier G" unfolding set_mult_def using subgroup_imp_subset assms by blast
   13.81 -next
   13.82 -  have " (carrier G) #>  \<one> = carrier G" unfolding set_mult_def r_coset_def group_axioms by simp
   13.83 -  moreover have "(carrier G) #>  \<one> \<subseteq> (carrier G) <#> H" unfolding set_mult_def r_coset_def
   13.84 -    using assms subgroup.one_closed[OF assms] by blast
   13.85 -  ultimately show "carrier G \<subseteq> (carrier G) <#> H" by simp
   13.86 -qed
   13.87 -
   13.88 -(*Same lemma as above, but everything is included in a subgroup*)
   13.89 -lemma (in group) set_mult_subgroup_idem :
   13.90 -  assumes "subgroup H G"
   13.91 -    and "subgroup N (G\<lparr>carrier:=H\<rparr>)"
   13.92 -  shows "H<#>N = H"
   13.93 -  using group.set_mult_carrier_idem[OF subgroup_imp_group] subgroup_imp_subset assms
   13.94 -  by (metis monoid.cases_scheme order_refl partial_object.simps(1)
   13.95 -      partial_object.update_convs(1) set_mult_same_law)
   13.96 -
   13.97 -(*A normal subgroup is commutative with set_mult*)
   13.98 -lemma (in group) commut_normal :
   13.99 -  assumes "subgroup H G"
  13.100 -    and "N\<lhd>G"
  13.101 -  shows "H<#>N = N<#>H" 
  13.102 -proof-
  13.103 -  have aux1 : "{H <#> N} = {\<Union>h\<in>H. h <# N }" unfolding set_mult_def l_coset_def by auto
  13.104 -  also have "... = {\<Union>h\<in>H. N #> h }" using assms normal.coset_eq subgroup.mem_carrier by fastforce
  13.105 -  moreover have aux2 : "{N <#> H} = {\<Union>h\<in>H. N #> h }"unfolding set_mult_def r_coset_def by auto
  13.106 -  ultimately show "H<#>N = N<#>H" by simp
  13.107 -qed
  13.108 -
  13.109 -(*Same lemma as above, but everything is included in a subgroup*)
  13.110 -lemma (in group) commut_normal_subgroup :
  13.111 -  assumes "subgroup H G"
  13.112 -    and "N\<lhd>(G\<lparr>carrier:=H\<rparr>)"
  13.113 -    and "subgroup K (G\<lparr>carrier:=H\<rparr>)"
  13.114 -  shows "K<#>N = N<#>K"
  13.115 -proof-
  13.116 -  have "N \<subseteq> carrier (G\<lparr>carrier := H\<rparr>)" using assms normal_imp_subgroup subgroup_imp_subset by blast
  13.117 -  hence NH : "N \<subseteq> H" by simp
  13.118 -  have "K \<subseteq> carrier(G\<lparr>carrier := H\<rparr>)" using subgroup_imp_subset assms by blast
  13.119 -  hence KH : "K \<subseteq> H" by simp
  13.120 -  have Egal : "K <#>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N = N <#>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> K"
  13.121 -  using group.commut_normal[where ?G = "G\<lparr>carrier :=H\<rparr>", of K N,OF subgroup_imp_group[OF assms(1)]
  13.122 -               assms(3) assms(2)] by auto
  13.123 -  also have "... = N <#> K" using set_mult_same_law[of H N K, OF assms(1) NH KH] by auto
  13.124 -  moreover have "K <#>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N = K <#> N"
  13.125 -    using set_mult_same_law[of H K N, OF assms(1) KH NH] by auto
  13.126 -  ultimately show "K<#>N = N<#>K" by auto
  13.127 -qed
  13.128 -
  13.129 -
  13.130 -
  13.131 -text "Lemmas about intersection and normal subgroups"
  13.132 -
  13.133 -
  13.134 -
  13.135 -lemma (in group) normal_inter:
  13.136 -  assumes "subgroup H G"
  13.137 -    and "subgroup K G"
  13.138 -    and "H1\<lhd>G\<lparr>carrier := H\<rparr>"
  13.139 -  shows " (H1\<inter>K)\<lhd>(G\<lparr>carrier:= (H\<inter>K)\<rparr>)" 
  13.140 -proof-
  13.141 -  define HK and H1K and GH and GHK
  13.142 -    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>)"
  13.143 -  show "H1K\<lhd>GHK"
  13.144 -  proof (intro group.normal_invI[of GHK H1K])
  13.145 -    show "Group.group GHK"
  13.146 -      using GHK_def subgroups_Inter_pair subgroup_imp_group assms by blast
  13.147 -
  13.148 -  next
  13.149 -    have  H1K_incl:"subgroup H1K (G\<lparr>carrier:= (H\<inter>K)\<rparr>)"
  13.150 -    proof(intro subgroup_incl)
  13.151 -          show "subgroup H1K G"
  13.152 -            using assms normal_imp_subgroup subgroups_Inter_pair incl_subgroup H1K_def by blast
  13.153 -        next
  13.154 -          show "subgroup (H\<inter>K) G" using HK_def subgroups_Inter_pair assms by auto
  13.155 -        next
  13.156 -          have "H1 \<subseteq> (carrier (G\<lparr>carrier:=H\<rparr>))" 
  13.157 -            using  assms(3) normal_imp_subgroup subgroup_imp_subset by blast
  13.158 -          also have "... \<subseteq> H" by simp
  13.159 -          thus "H1K \<subseteq>H\<inter>K" 
  13.160 -            using H1K_def calculation by auto
  13.161 -        qed
  13.162 -        thus "subgroup H1K GHK" using GHK_def by simp
  13.163 -
  13.164 -  next
  13.165 -    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"
  13.166 -        proof-
  13.167 -          have invHK: "\<lbrakk>y\<in>HK\<rbrakk> \<Longrightarrow> inv\<^bsub>GHK\<^esub> y = inv\<^bsub>GH\<^esub> y"
  13.168 -            using subgroup_inv_equality assms HK_def GH_def GHK_def subgroups_Inter_pair by simp
  13.169 -          have multHK : "\<lbrakk>x\<in>HK;y\<in>HK\<rbrakk> \<Longrightarrow>  x \<otimes>\<^bsub>(G\<lparr>carrier:=HK\<rparr>)\<^esub> y =  x \<otimes> y"
  13.170 -            using HK_def by simp
  13.171 -          fix x assume p: "x\<in>carrier GHK"
  13.172 -            fix h assume p2 : "h:H1K"
  13.173 -            have "carrier(GHK)\<subseteq>HK"
  13.174 -              using GHK_def HK_def by simp
  13.175 -            hence xHK:"x\<in>HK" using p by auto
  13.176 -            hence invx:"inv\<^bsub>GHK\<^esub> x = inv\<^bsub>GH\<^esub> x"
  13.177 -              using invHK assms GHK_def HK_def GH_def subgroup_inv_equality subgroups_Inter_pair by simp
  13.178 -            have "H1\<subseteq>carrier(GH)"
  13.179 -              using assms GH_def normal_imp_subgroup subgroup_imp_subset by blast
  13.180 -            hence hHK:"h\<in>HK" 
  13.181 -              using p2 H1K_def HK_def GH_def by auto
  13.182 -            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"
  13.183 -              using invx invHK multHK GHK_def GH_def by auto
  13.184 -            have xH:"x\<in>carrier(GH)" 
  13.185 -              using xHK HK_def GH_def by auto 
  13.186 -            have hH:"h\<in>carrier(GH)"
  13.187 -              using hHK HK_def GH_def by auto 
  13.188 -            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)"
  13.189 -              using assms normal_invE GH_def normal.inv_op_closed2 by fastforce
  13.190 -            hence INCL_1 : "x \<otimes>\<^bsub>GH\<^esub> h \<otimes>\<^bsub>GH\<^esub> inv\<^bsub>GH\<^esub> x \<in> H1"
  13.191 -              using  xH H1K_def p2 by blast
  13.192 -            have " x \<otimes>\<^bsub>GH\<^esub> h \<otimes>\<^bsub>GH\<^esub> inv\<^bsub>GH\<^esub> x \<in> HK"
  13.193 -              using assms HK_def subgroups_Inter_pair hHK xHK
  13.194 -              by (metis GH_def inf.cobounded1 subgroup_def subgroup_incl)
  13.195 -            hence " x \<otimes>\<^bsub>GH\<^esub> h \<otimes>\<^bsub>GH\<^esub> inv\<^bsub>GH\<^esub> x \<in> K" using HK_def by simp
  13.196 -            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
  13.197 -            thus  "x \<otimes>\<^bsub>GHK\<^esub> h \<otimes>\<^bsub>GHK\<^esub> inv\<^bsub>GHK\<^esub> x \<in> H1K" using xhx_egal by simp
  13.198 -          qed
  13.199 -    qed
  13.200 -qed
  13.201 -
  13.202 -
  13.203 -lemma (in group) normal_inter_subgroup :
  13.204 -  assumes "subgroup H G"
  13.205 -    and "N \<lhd> G"
  13.206 -  shows "(N\<inter>H) \<lhd> (G\<lparr>carrier := H\<rparr>)"
  13.207 -proof -
  13.208 -  define K where "K = carrier G"
  13.209 -  have "G\<lparr>carrier := K\<rparr> =  G" using K_def by auto
  13.210 -  moreover have "subgroup K G" using K_def subgroup_self by blast
  13.211 -  moreover have "normal N (G \<lparr>carrier :=K\<rparr>)" using assms K_def by simp
  13.212 -  ultimately have "N \<inter> H \<lhd> G\<lparr>carrier := K \<inter> H\<rparr>"
  13.213 -    using normal_inter[of K H N] assms(1) by blast
  13.214 -  moreover have "K \<inter> H = H" using K_def assms subgroup_imp_subset by blast
  13.215 -  ultimately show "normal (N\<inter>H) (G\<lparr>carrier := H\<rparr>)" by auto
  13.216 -qed
  13.217 -
  13.218 -
  13.219 -
  13.220 -text \<open>Lemmas about normalizer\<close>
  13.221 +subsubsection \<open>Lemmas about normalizer\<close>
  13.222  
  13.223  
  13.224  lemma (in group) subgroup_in_normalizer: 
  13.225 @@ -267,39 +55,38 @@
  13.226  qed
  13.227  
  13.228  
  13.229 -lemma (in group) normal_imp_subgroup_normalizer :
  13.230 +lemma (in group) normal_imp_subgroup_normalizer:
  13.231    assumes "subgroup H G"
  13.232 -and "N \<lhd> (G\<lparr>carrier := H\<rparr>)"
  13.233 -shows "subgroup H (G\<lparr>carrier := normalizer G N\<rparr>)" 
  13.234 +    and "N \<lhd> (G\<lparr>carrier := H\<rparr>)"
  13.235 +  shows "subgroup H (G\<lparr>carrier := normalizer G N\<rparr>)" 
  13.236  proof-
  13.237    have N_carrierG : "N \<subseteq> carrier(G)"
  13.238      using assms normal_imp_subgroup subgroup_imp_subset
  13.239      by (smt monoid.cases_scheme order_trans partial_object.simps(1) partial_object.update_convs(1))
  13.240    {have "H \<subseteq> normalizer G N" unfolding normalizer_def stabilizer_def
  13.241      proof
  13.242 -    fix x assume xH : "x \<in> H"
  13.243 -    hence xcarrierG : "x \<in> carrier(G)" using assms subgroup_imp_subset  by auto
  13.244 -    have "   N #> x = x <# N" using assms xH
  13.245 -      unfolding r_coset_def l_coset_def normal_def normal_axioms_def subgroup_imp_group by auto
  13.246 -    hence "x <# N #> inv x =(N #> x) #> inv x"
  13.247 -      by simp
  13.248 -    also have "... = N #> \<one>"
  13.249 -      using  assms r_inv xcarrierG coset_mult_assoc[OF N_carrierG] by simp  
  13.250 -    finally have "x <# N #> inv x = N" by (simp add: N_carrierG)
  13.251 -    thus "x \<in> {g \<in> carrier G. (\<lambda>H\<in>{H. H \<subseteq> carrier G}. g <# H #> inv g) N = N}"
  13.252 -      using xcarrierG by (simp add : N_carrierG)
  13.253 -  qed}
  13.254 +      fix x assume xH : "x \<in> H"
  13.255 +      hence xcarrierG : "x \<in> carrier(G)" using assms subgroup_imp_subset  by auto
  13.256 +      have "   N #> x = x <# N" using assms xH
  13.257 +        unfolding r_coset_def l_coset_def normal_def normal_axioms_def subgroup_imp_group by auto
  13.258 +      hence "x <# N #> inv x =(N #> x) #> inv x"
  13.259 +        by simp
  13.260 +      also have "... = N #> \<one>"
  13.261 +        using  assms r_inv xcarrierG coset_mult_assoc[OF N_carrierG] by simp  
  13.262 +      finally have "x <# N #> inv x = N" by (simp add: N_carrierG)
  13.263 +      thus "x \<in> {g \<in> carrier G. (\<lambda>H\<in>{H. H \<subseteq> carrier G}. g <# H #> inv g) N = N}"
  13.264 +        using xcarrierG by (simp add : N_carrierG)
  13.265 +    qed}
  13.266    thus "subgroup H (G\<lparr>carrier := normalizer G N\<rparr>)"
  13.267      using subgroup_incl[OF assms(1) normalizer_imp_subgroup]
  13.268 -         assms normal_imp_subgroup subgroup_imp_subset
  13.269 +      assms normal_imp_subgroup subgroup_imp_subset
  13.270      by (metis  group.incl_subgroup is_group)
  13.271  qed
  13.272  
  13.273  
  13.274  subsection \<open>Second Isomorphism Theorem\<close>
  13.275  
  13.276 -
  13.277 -lemma (in group) mult_norm_subgroup :
  13.278 +lemma (in group) mult_norm_subgroup:
  13.279    assumes "normal N G"
  13.280      and "subgroup H G"
  13.281    shows "subgroup (N<#>H) G" unfolding subgroup_def
  13.282 @@ -364,7 +151,7 @@
  13.283  qed
  13.284      
  13.285  
  13.286 -lemma (in group) mult_norm_sub_in_sub :
  13.287 +lemma (in group) mult_norm_sub_in_sub:
  13.288    assumes "normal N (G\<lparr>carrier:=K\<rparr>)"
  13.289    assumes "subgroup H (G\<lparr>carrier:=K\<rparr>)"
  13.290    assumes "subgroup K G"
  13.291 @@ -379,12 +166,12 @@
  13.292    also have "... \<subseteq> K" by simp
  13.293    finally have Incl2:"N \<subseteq> K" by simp
  13.294    have "(N <#>\<^bsub>G\<lparr>carrier := K\<rparr>\<^esub> H) = (N <#> H)"
  13.295 -    using set_mult_same_law[of K] assms Incl1 Incl2 by simp
  13.296 +    using subgroup_set_mult_equality[of K] assms Incl1 Incl2 by simp
  13.297    thus "subgroup (N<#>H) (G\<lparr>carrier:=K\<rparr>)" using Hyp by auto
  13.298  qed
  13.299  
  13.300  
  13.301 -lemma (in group) subgroup_of_normal_set_mult :
  13.302 +lemma (in group) subgroup_of_normal_set_mult:
  13.303    assumes "normal N G"
  13.304  and "subgroup H G"
  13.305  shows "subgroup H (G\<lparr>carrier := N <#> H\<rparr>)"
  13.306 @@ -398,7 +185,7 @@
  13.307  qed
  13.308  
  13.309  
  13.310 -lemma (in group) normal_in_normal_set_mult :
  13.311 +lemma (in group) normal_in_normal_set_mult:
  13.312    assumes "normal N G"
  13.313  and "subgroup H G"
  13.314  shows "normal N (G\<lparr>carrier := N <#> H\<rparr>)"
  13.315 @@ -413,7 +200,7 @@
  13.316  qed
  13.317  
  13.318  
  13.319 -proposition (in group) weak_snd_iso_thme :
  13.320 +proposition (in group) weak_snd_iso_thme:
  13.321    assumes "subgroup  H G" 
  13.322      and "N\<lhd>G"
  13.323    shows "(G\<lparr>carrier := N<#>H\<rparr> Mod N \<cong> G\<lparr>carrier:=H\<rparr> Mod (N\<inter>H))"
  13.324 @@ -518,7 +305,7 @@
  13.325  qed
  13.326  
  13.327  
  13.328 -theorem (in group) snd_iso_thme :
  13.329 +theorem (in group) snd_iso_thme:
  13.330    assumes "subgroup H G"
  13.331      and "subgroup N G"
  13.332      and "subgroup H (G\<lparr>carrier:= (normalizer G N)\<rparr>)"
  13.333 @@ -539,7 +326,7 @@
  13.334           G\<lparr>carrier := normalizer G N, carrier := H\<rparr> Mod N \<inter> H =
  13.335            (G\<lparr>carrier:= N<#>H\<rparr> Mod N)  \<cong>
  13.336           G\<lparr>carrier := normalizer G N, carrier := H\<rparr> Mod N \<inter> H" 
  13.337 -    using set_mult_same_law[OF  normalizer_imp_subgroup[OF subgroup_imp_subset[OF assms(2)]], of N H] 
  13.338 +    using subgroup_set_mult_equality[OF  normalizer_imp_subgroup[OF subgroup_imp_subset[OF assms(2)]], of N H] 
  13.339            subgroup_imp_subset[OF assms(3)]
  13.340            subgroup_imp_subset[OF normal_imp_subgroup[OF subgroup_in_normalizer[OF assms(2)]]]
  13.341      by simp
  13.342 @@ -570,7 +357,7 @@
  13.343  subsection\<open>The Zassenhaus Lemma\<close>
  13.344  
  13.345  
  13.346 -lemma (in group) distinc :
  13.347 +lemma (in group) distinc:
  13.348    assumes "subgroup  H G" 
  13.349      and "H1\<lhd>G\<lparr>carrier := H\<rparr>" 
  13.350      and  "subgroup K G" 
  13.351 @@ -623,7 +410,7 @@
  13.352    qed
  13.353  qed
  13.354  
  13.355 -lemma (in group) preliminary1 :
  13.356 +lemma (in group) preliminary1:
  13.357    assumes "subgroup  H G" 
  13.358      and "H1\<lhd>G\<lparr>carrier := H\<rparr>" 
  13.359      and  "subgroup K G" 
  13.360 @@ -664,7 +451,7 @@
  13.361    qed
  13.362  qed
  13.363  
  13.364 -lemma (in group) preliminary2 :
  13.365 +lemma (in group) preliminary2:
  13.366    assumes "subgroup  H G" 
  13.367      and "H1\<lhd>G\<lparr>carrier := H\<rparr>"
  13.368      and  "subgroup K G" 
  13.369 @@ -700,7 +487,7 @@
  13.370      hence allG : "h1 \<in> carrier G" "hk \<in> carrier G" "x \<in> carrier G"
  13.371        using assms subgroup_imp_subset h1hk_def normal_imp_subgroup incl_subgroup apply blast+.
  13.372      hence "x <#\<^bsub>G\<lparr>carrier := H1 <#> H\<inter>K\<rparr>\<^esub> (H1 <#> H\<inter>K1) =h1 \<otimes> hk <# (H1 <#> H\<inter>K1)"
  13.373 -      using set_mult_same_law subgroup_imp_subset xH h1hk_def by (simp add: l_coset_def)
  13.374 +      using subgroup_set_mult_equality subgroup_imp_subset xH h1hk_def by (simp add: l_coset_def)
  13.375      also have "... = h1 <# (hk <# (H1 <#> H\<inter>K1))"
  13.376        using lcos_m_assoc[OF subgroup_imp_subset[OF incl_subgroup[OF assms(1) subH1]]allG(1)allG(2)]
  13.377        by (metis allG(1) allG(2) assms(1) incl_subgroup lcos_m_assoc subH2 subgroup_imp_subset)
  13.378 @@ -742,7 +529,7 @@
  13.379      finally have eq1 : "x <#\<^bsub>G\<lparr>carrier := H1 <#> H \<inter> K\<rparr>\<^esub> (H1 <#> H \<inter> K1) = H1 <#> (H \<inter> K1) #> hk"
  13.380        by (simp add: allG(2) all_inclG inf.coboundedI2 setmult_rcos_assoc)
  13.381      have "H1 <#> H \<inter> K1 #>\<^bsub>G\<lparr>carrier := H1 <#> H \<inter> K\<rparr>\<^esub> x = H1 <#> H \<inter> K1 #> (h1 \<otimes> hk)"
  13.382 -      using set_mult_same_law subgroup_imp_subset xH h1hk_def by (simp add: r_coset_def)
  13.383 +      using subgroup_set_mult_equality subgroup_imp_subset xH h1hk_def by (simp add: r_coset_def)
  13.384      also have "... = H1 <#> H \<inter> K1 #> h1 #> hk"
  13.385        using coset_mult_assoc by (simp add: allG all_inclG inf.coboundedI2 setmult_subset_G)
  13.386      also have"... =  H \<inter> K1 <#> H1 #> h1 #> hk"
  13.387 @@ -762,7 +549,7 @@
  13.388  qed
  13.389  
  13.390  
  13.391 -proposition (in group)  Zassenhaus_1 :
  13.392 +proposition (in group)  Zassenhaus_1:
  13.393    assumes "subgroup  H G" 
  13.394      and "H1\<lhd>G\<lparr>carrier := H\<rparr>" 
  13.395      and  "subgroup K G" 
  13.396 @@ -811,7 +598,7 @@
  13.397  qed
  13.398  
  13.399  
  13.400 -theorem (in group) Zassenhaus :
  13.401 +theorem (in group) Zassenhaus:
  13.402    assumes "subgroup  H G" 
  13.403      and "H1\<lhd>G\<lparr>carrier := H\<rparr>" 
  13.404      and  "subgroup K G" 
    14.1 --- a/src/HOL/ROOT	Tue Jun 12 16:09:12 2018 +0100
    14.2 +++ b/src/HOL/ROOT	Thu Jun 14 14:23:38 2018 +0100
    14.3 @@ -294,22 +294,16 @@
    14.4    theories
    14.5      (* Orders and Lattices *)
    14.6      Galois_Connection    (* Knaster-Tarski theorem and Galois connections *)
    14.7 -
    14.8      (* Groups *)
    14.9      FiniteProduct        (* Product operator for commutative groups *)
   14.10      Sylow                (* Sylow's theorem *)
   14.11      Bij                  (* Automorphism Groups *)
   14.12 -    More_Group
   14.13 -    More_Finite_Product
   14.14      Multiplicative_Group
   14.15      Zassenhaus            (* The Zassenhaus lemma *)
   14.16 -
   14.17 -
   14.18      (* Rings *)
   14.19      Divisibility         (* Rings *)
   14.20      IntRing              (* Ideals and residue classes *)
   14.21      UnivPoly             (* Polynomials *)
   14.22 -    More_Ring
   14.23    document_files "root.bib" "root.tex"
   14.24  
   14.25  session "HOL-Auth" (timing) in Auth = "HOL-Library" +