a few more lemmas from Paulo and Martin
authorpaulson <lp15@cam.ac.uk>
Sun Jul 01 16:13:25 2018 +0100 (9 months ago)
changeset 6855522d51874f37d
parent 68552 391e89e03eef
child 68556 fcffdcb8f506
a few more lemmas from Paulo and Martin
src/HOL/Algebra/Coset.thy
src/HOL/Algebra/Group.thy
src/HOL/Algebra/Zassenhaus.thy
     1.1 --- a/src/HOL/Algebra/Coset.thy	Sat Jun 30 18:58:13 2018 +0100
     1.2 +++ b/src/HOL/Algebra/Coset.thy	Sun Jul 01 16:13:25 2018 +0100
     1.3 @@ -37,13 +37,12 @@
     1.4    normal_rel :: "['a set, ('a, 'b) monoid_scheme] \<Rightarrow> bool"  (infixl "\<lhd>" 60) where
     1.5    "H \<lhd> G \<equiv> normal H G"
     1.6  
     1.7 -(* ************************************************************************** *)
     1.8 -(* Next two lemmas contributed by Martin Baillon.                                  *)
     1.9 +(*Next two lemmas contributed by Martin Baillon.*)
    1.10  
    1.11  lemma l_coset_eq_set_mult:
    1.12    fixes G (structure)
    1.13    shows "x <# H = {x} <#> H"
    1.14 -  unfolding l_coset_def set_mult_def by simp 
    1.15 +  unfolding l_coset_def set_mult_def by simp
    1.16  
    1.17  lemma r_coset_eq_set_mult:
    1.18    fixes G (structure)
    1.19 @@ -74,7 +73,7 @@
    1.20                        and h2: "h2 \<in> H" "r2 = h2 \<otimes> g"
    1.21      using r1 r2 unfolding r_coset_def by blast
    1.22    hence "r1 \<otimes> (inv r2) = (h1 \<otimes> g) \<otimes> ((inv g) \<otimes> (inv h2))"
    1.23 -    using inv_mult_group is_group assms(1) g(1) subgroup.mem_carrier by fastforce 
    1.24 +    using inv_mult_group is_group assms(1) g(1) subgroup.mem_carrier by fastforce
    1.25    also have " ... =  (h1 \<otimes> (g \<otimes> inv g) \<otimes> inv h2)"
    1.26      using h1 h2 assms(1) g(1) inv_closed m_closed monoid.m_assoc
    1.27            monoid_axioms subgroup.mem_carrier by smt
    1.28 @@ -89,21 +88,6 @@
    1.29  
    1.30  subsection \<open>Stable Operations for Subgroups\<close>
    1.31  
    1.32 -lemma (in group) subgroup_set_mult_equality[simp]:
    1.33 -  assumes "subgroup H G" "I \<subseteq> H" "J \<subseteq> H"
    1.34 -  shows "I <#>\<^bsub>G \<lparr> carrier := H \<rparr>\<^esub> J = I <#> J"
    1.35 -  unfolding set_mult_def subgroup_mult_equality[OF assms(1)] by auto
    1.36 -
    1.37 -lemma (in group) subgroup_rcos_equality[simp]:
    1.38 -  assumes "subgroup H G" "I \<subseteq> H" "h \<in> H"
    1.39 -  shows "I #>\<^bsub>G \<lparr> carrier := H \<rparr>\<^esub> h = I #> h"
    1.40 -  using subgroup_set_mult_equality by (simp add: r_coset_eq_set_mult assms)
    1.41 -
    1.42 -lemma (in group) subgroup_lcos_equality[simp]:
    1.43 -  assumes "subgroup H G" "I \<subseteq> H" "h \<in> H"
    1.44 -  shows "h <#\<^bsub>G \<lparr> carrier := H \<rparr>\<^esub> I = h <# I"
    1.45 -  using subgroup_set_mult_equality by (simp add: l_coset_eq_set_mult assms)
    1.46 -
    1.47  lemma set_mult_consistent [simp]:
    1.48    "N <#>\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> K = N <#>\<^bsub>G\<^esub> K"
    1.49    unfolding set_mult_def by simp
    1.50 @@ -184,7 +168,7 @@
    1.51    assumes "M #> x = M #> y"
    1.52      and "x \<in> carrier G"  "y \<in> carrier G" "M \<subseteq> carrier G"
    1.53    shows "M #> (x \<otimes> (inv y)) = M " using assms
    1.54 -  by (metis group.coset_mult_assoc group.coset_mult_one inv_closed is_group r_inv) 
    1.55 +  by (metis group.coset_mult_assoc group.coset_mult_one inv_closed is_group r_inv)
    1.56  
    1.57  lemma (in group) coset_join1:
    1.58    assumes "H #> x = H"
    1.59 @@ -297,12 +281,12 @@
    1.60    shows "(x' \<in> H #> x) = (x' \<otimes> inv x \<in> H)"
    1.61    using rcos_module_rev rcos_module_imp assms by blast
    1.62  
    1.63 -text \<open>Right cosets are subsets of the carrier.\<close> 
    1.64 +text \<open>Right cosets are subsets of the carrier.\<close>
    1.65  lemma (in subgroup) rcosets_carrier:
    1.66    assumes "group G" "X \<in> rcosets H"
    1.67    shows "X \<subseteq> carrier G"
    1.68    using assms elemrcos_carrier singletonD
    1.69 -  subset_eq unfolding RCOSETS_def by force 
    1.70 +  subset_eq unfolding RCOSETS_def by force
    1.71  
    1.72  
    1.73  text \<open>Multiplication of general subsets\<close>
    1.74 @@ -369,7 +353,7 @@
    1.75  lemma normal_imp_subgroup: "H \<lhd> G \<Longrightarrow> subgroup H G"
    1.76    by (simp add: normal_def subgroup_def)
    1.77  
    1.78 -lemma (in group) normalI: 
    1.79 +lemma (in group) normalI:
    1.80    "subgroup H G \<Longrightarrow> (\<forall>x \<in> carrier G. H #> x = x <# H) \<Longrightarrow> H \<lhd> G"
    1.81    by (simp add: normal_def normal_axioms_def is_group)
    1.82  
    1.83 @@ -378,32 +362,32 @@
    1.84    shows "(inv x) \<otimes> h \<otimes> x \<in> H"
    1.85  proof -
    1.86    have "h \<otimes> x \<in> x <# H"
    1.87 -    using assms coset_eq assms(1) unfolding r_coset_def by blast 
    1.88 +    using assms coset_eq assms(1) unfolding r_coset_def by blast
    1.89    then obtain h' where "h' \<in> H" "h \<otimes> x = x \<otimes> h'"
    1.90      unfolding l_coset_def by blast
    1.91 -  thus ?thesis by (metis assms inv_closed l_inv l_one m_assoc mem_carrier) 
    1.92 +  thus ?thesis by (metis assms inv_closed l_inv l_one m_assoc mem_carrier)
    1.93  qed
    1.94  
    1.95  lemma (in normal) inv_op_closed2:
    1.96    assumes "x \<in> carrier G" and "h \<in> H"
    1.97    shows "x \<otimes> h \<otimes> (inv x) \<in> H"
    1.98 -  using assms inv_op_closed1 by (metis inv_closed inv_inv) 
    1.99 +  using assms inv_op_closed1 by (metis inv_closed inv_inv)
   1.100  
   1.101  
   1.102  text\<open>Alternative characterization of normal subgroups\<close>
   1.103  lemma (in group) normal_inv_iff:
   1.104 -     "(N \<lhd> G) = 
   1.105 +     "(N \<lhd> G) =
   1.106        (subgroup N G \<and> (\<forall>x \<in> carrier G. \<forall>h \<in> N. x \<otimes> h \<otimes> (inv x) \<in> N))"
   1.107        (is "_ = ?rhs")
   1.108  proof
   1.109    assume N: "N \<lhd> G"
   1.110    show ?rhs
   1.111 -    by (blast intro: N normal.inv_op_closed2 normal_imp_subgroup) 
   1.112 +    by (blast intro: N normal.inv_op_closed2 normal_imp_subgroup)
   1.113  next
   1.114    assume ?rhs
   1.115 -  hence sg: "subgroup N G" 
   1.116 +  hence sg: "subgroup N G"
   1.117      and closed: "\<And>x. x\<in>carrier G \<Longrightarrow> \<forall>h\<in>N. x \<otimes> h \<otimes> inv x \<in> N" by auto
   1.118 -  hence sb: "N \<subseteq> carrier G" by (simp add: subgroup.subset) 
   1.119 +  hence sb: "N \<subseteq> carrier G" by (simp add: subgroup.subset)
   1.120    show "N \<lhd> G"
   1.121    proof (intro normalI [OF sg], simp add: l_coset_def r_coset_def, clarify)
   1.122      fix x
   1.123 @@ -413,9 +397,9 @@
   1.124        show "(\<Union>h\<in>N. {h \<otimes> x}) \<subseteq> (\<Union>h\<in>N. {x \<otimes> h})"
   1.125        proof clarify
   1.126          fix n
   1.127 -        assume n: "n \<in> N" 
   1.128 +        assume n: "n \<in> N"
   1.129          show "n \<otimes> x \<in> (\<Union>h\<in>N. {x \<otimes> h})"
   1.130 -        proof 
   1.131 +        proof
   1.132            from closed [of "inv x"]
   1.133            show "inv x \<otimes> n \<otimes> x \<in> N" by (simp add: x n)
   1.134            show "n \<otimes> x \<in> {x \<otimes> (inv x \<otimes> n \<otimes> x)}"
   1.135 @@ -426,9 +410,9 @@
   1.136        show "(\<Union>h\<in>N. {x \<otimes> h}) \<subseteq> (\<Union>h\<in>N. {h \<otimes> x})"
   1.137        proof clarify
   1.138          fix n
   1.139 -        assume n: "n \<in> N" 
   1.140 +        assume n: "n \<in> N"
   1.141          show "x \<otimes> n \<in> (\<Union>h\<in>N. {h \<otimes> x})"
   1.142 -        proof 
   1.143 +        proof
   1.144            show "x \<otimes> n \<otimes> inv x \<in> N" by (simp add: x n closed)
   1.145            show "x \<otimes> n \<in> {x \<otimes> n \<otimes> inv x \<otimes> x}"
   1.146              by (simp add: x n m_assoc sb [THEN subsetD])
   1.147 @@ -444,14 +428,14 @@
   1.148    using assms normal_inv_iff by blast
   1.149  
   1.150  corollary (in group) normal_invE:
   1.151 -  assumes "N \<lhd> G" 
   1.152 +  assumes "N \<lhd> G"
   1.153    shows "subgroup N G" and "\<And>x h. \<lbrakk> x \<in> carrier G; h \<in> N \<rbrakk> \<Longrightarrow> x \<otimes> h \<otimes> inv x \<in> N"
   1.154    using assms normal_inv_iff apply blast
   1.155 -  by (simp add: assms normal.inv_op_closed2) 
   1.156 +  by (simp add: assms normal.inv_op_closed2)
   1.157  
   1.158  
   1.159  lemma (in group) one_is_normal :
   1.160 -   "{\<one>} \<lhd> G" 
   1.161 +   "{\<one>} \<lhd> G"
   1.162  proof(intro normal_invI )
   1.163    show "subgroup {\<one>} G"
   1.164      by (simp add: subgroup_def)
   1.165 @@ -470,7 +454,7 @@
   1.166    hence "\<And> h. h \<in> H \<Longrightarrow> x \<otimes> h = y \<otimes> ((inv h') \<otimes> h)"
   1.167      by (smt assms(2-3) inv_closed inv_solve_right m_assoc m_closed subgroup.mem_carrier)
   1.168    hence "\<And> xh. xh \<in> x <# H \<Longrightarrow> xh \<in> y <# H"
   1.169 -    unfolding l_coset_def by (metis (no_types, lifting) UN_iff assms(3) h'(1) subgroup_def) 
   1.170 +    unfolding l_coset_def by (metis (no_types, lifting) UN_iff assms(3) h'(1) subgroup_def)
   1.171    moreover have "\<And> h. h \<in> H \<Longrightarrow> y \<otimes> h = x \<otimes> (h' \<otimes> h)"
   1.172      using h' by (meson assms(2) assms(3) m_assoc subgroup.mem_carrier)
   1.173    hence "\<And> yh. yh \<in> y <# H \<Longrightarrow> yh \<in> x <# H"
   1.174 @@ -494,7 +478,7 @@
   1.175    by (auto simp add: l_coset_def m_assoc  subgroup.subset [THEN subsetD] subgroup.m_closed)
   1.176  
   1.177  lemma (in group) l_coset_swap:
   1.178 -  assumes "y \<in> x <# H" "x \<in> carrier G" "subgroup H G" 
   1.179 +  assumes "y \<in> x <# H" "x \<in> carrier G" "subgroup H G"
   1.180    shows "x \<in> y <# H"
   1.181    using assms(2) l_repr_independence[OF assms] subgroup.one_closed[OF assms(3)]
   1.182    unfolding l_coset_def by fastforce
   1.183 @@ -518,7 +502,7 @@
   1.184  
   1.185  lemma (in normal) rcos_inv:
   1.186    assumes x:     "x \<in> carrier G"
   1.187 -  shows "set_inv (H #> x) = H #> (inv x)" 
   1.188 +  shows "set_inv (H #> x) = H #> (inv x)"
   1.189  proof (simp add: r_coset_def SET_INV_def x inv_mult_group, safe)
   1.190    fix h
   1.191    assume h: "h \<in> H"
   1.192 @@ -595,12 +579,12 @@
   1.193    show ?thesis
   1.194    proof (intro equivI)
   1.195      show "refl_on (carrier G) (rcong H)"
   1.196 -      by (auto simp add: r_congruent_def refl_on_def) 
   1.197 +      by (auto simp add: r_congruent_def refl_on_def)
   1.198    next
   1.199      show "sym (rcong H)"
   1.200      proof (simp add: r_congruent_def sym_def, clarify)
   1.201        fix x y
   1.202 -      assume [simp]: "x \<in> carrier G" "y \<in> carrier G" 
   1.203 +      assume [simp]: "x \<in> carrier G" "y \<in> carrier G"
   1.204           and "inv x \<otimes> y \<in> H"
   1.205        hence "inv (inv x \<otimes> y) \<in> H" by simp
   1.206        thus "inv y \<otimes> x \<in> H" by (simp add: inv_mult_group)
   1.207 @@ -613,7 +597,7 @@
   1.208           and "inv x \<otimes> y \<in> H" and "inv y \<otimes> z \<in> H"
   1.209        hence "(inv x \<otimes> y) \<otimes> (inv y \<otimes> z) \<in> H" by simp
   1.210        hence "inv x \<otimes> (y \<otimes> inv y) \<otimes> z \<in> H"
   1.211 -        by (simp add: m_assoc del: r_inv Units_r_inv) 
   1.212 +        by (simp add: m_assoc del: r_inv Units_r_inv)
   1.213        thus "inv x \<otimes> z \<in> H" by simp
   1.214      qed
   1.215    qed
   1.216 @@ -639,7 +623,7 @@
   1.217    shows "a <# H = (rcong H) `` {a}"
   1.218  proof -
   1.219    interpret group G by fact
   1.220 -  show ?thesis by (force simp add: r_congruent_def l_coset_def m_assoc [symmetric] a ) 
   1.221 +  show ?thesis by (force simp add: r_congruent_def l_coset_def m_assoc [symmetric] a )
   1.222  qed
   1.223  
   1.224  
   1.225 @@ -692,9 +676,9 @@
   1.226        have "inv c \<otimes> (inv a \<otimes> b) \<otimes> c \<in> H" by (rule inv_op_closed1)
   1.227    moreover
   1.228        from carr and inv_closed
   1.229 -      have "inv c \<otimes> (inv a \<otimes> b) \<otimes> c = (inv c \<otimes> inv a) \<otimes> (b \<otimes> c)" 
   1.230 +      have "inv c \<otimes> (inv a \<otimes> b) \<otimes> c = (inv c \<otimes> inv a) \<otimes> (b \<otimes> c)"
   1.231        by (force cong: m_assoc)
   1.232 -  moreover 
   1.233 +  moreover
   1.234        from carr and inv_closed
   1.235        have "\<dots> = (inv (a \<otimes> c)) \<otimes> (b \<otimes> c)"
   1.236        by (simp add: inv_mult_group)
   1.237 @@ -803,7 +787,7 @@
   1.238    moreover have "?f ` H \<subseteq> R"
   1.239      using g unfolding r_coset_def by blast
   1.240    ultimately show ?thesis using inj_on_g unfolding bij_betw_def
   1.241 -    using assms(2) g(1) by auto 
   1.242 +    using assms(2) g(1) by auto
   1.243  qed
   1.244  
   1.245  corollary (in group) card_rcosets_equal:
   1.246 @@ -843,7 +827,7 @@
   1.247    case False note inf_G = this
   1.248    thus ?thesis
   1.249    proof (cases "finite H")
   1.250 -    case False thus ?thesis using inf_G  by (simp add: order_def)  
   1.251 +    case False thus ?thesis using inf_G  by (simp add: order_def)
   1.252    next
   1.253      case True note finite_H = this
   1.254      have "infinite (rcosets H)"
   1.255 @@ -860,7 +844,7 @@
   1.256        hence "order G = (card H) * (card (rcosets H))" by simp
   1.257        hence "order G \<noteq> 0" using finite_rcos finite_H assms ex_in_conv
   1.258                                  rcosets_part_G subgroup.one_closed by fastforce
   1.259 -      thus False using inf_G order_gt_0_iff_finite by blast 
   1.260 +      thus False using inf_G order_gt_0_iff_finite by blast
   1.261      qed
   1.262      thus ?thesis using inf_G by (simp add: order_def)
   1.263    qed
   1.264 @@ -915,11 +899,11 @@
   1.265  done
   1.266  
   1.267  lemma mult_FactGroup [simp]: "X \<otimes>\<^bsub>(G Mod H)\<^esub> X' = X <#>\<^bsub>G\<^esub> X'"
   1.268 -  by (simp add: FactGroup_def) 
   1.269 +  by (simp add: FactGroup_def)
   1.270  
   1.271  lemma (in normal) inv_FactGroup:
   1.272       "X \<in> carrier (G Mod H) \<Longrightarrow> inv\<^bsub>G Mod H\<^esub> X = set_inv X"
   1.273 -apply (rule group.inv_equality [OF factorgroup_is_group]) 
   1.274 +apply (rule group.inv_equality [OF factorgroup_is_group])
   1.275  apply (simp_all add: FactGroup_def setinv_closed rcosets_inv_mult_group_eq)
   1.276  done
   1.277  
   1.278 @@ -929,10 +913,10 @@
   1.279    "(\<lambda>a. H #> a) \<in> hom G (G Mod H)"
   1.280    by (auto simp add: FactGroup_def RCOSETS_def Pi_def hom_def rcos_sum)
   1.281  
   1.282 - 
   1.283 +
   1.284  subsection\<open>The First Isomorphism Theorem\<close>
   1.285  
   1.286 -text\<open>The quotient by the kernel of a homomorphism is isomorphic to the 
   1.287 +text\<open>The quotient by the kernel of a homomorphism is isomorphic to the
   1.288    range of that homomorphism.\<close>
   1.289  
   1.290  definition
   1.291 @@ -941,8 +925,8 @@
   1.292    where "kernel G H h = {x. x \<in> carrier G \<and> h x = \<one>\<^bsub>H\<^esub>}"
   1.293  
   1.294  lemma (in group_hom) subgroup_kernel: "subgroup (kernel G H h) G"
   1.295 -apply (rule subgroup.intro) 
   1.296 -apply (auto simp add: kernel_def group.intro is_group) 
   1.297 +apply (rule subgroup.intro)
   1.298 +apply (auto simp add: kernel_def group.intro is_group)
   1.299  done
   1.300  
   1.301  text\<open>The kernel of a homomorphism is a normal subgroup\<close>
   1.302 @@ -956,10 +940,10 @@
   1.303    shows "X \<noteq> {}"
   1.304  proof -
   1.305    from X
   1.306 -  obtain g where "g \<in> carrier G" 
   1.307 +  obtain g where "g \<in> carrier G"
   1.308               and "X = kernel G H h #> g"
   1.309      by (auto simp add: FactGroup_def RCOSETS_def)
   1.310 -  thus ?thesis 
   1.311 +  thus ?thesis
   1.312     by (auto simp add: kernel_def r_coset_def image_def intro: hom_one)
   1.313  qed
   1.314  
   1.315 @@ -969,7 +953,7 @@
   1.316    shows "the_elem (h`X) \<in> carrier H"
   1.317  proof -
   1.318    from X
   1.319 -  obtain g where g: "g \<in> carrier G" 
   1.320 +  obtain g where g: "g \<in> carrier G"
   1.321               and "X = kernel G H h #> g"
   1.322      by (auto simp add: FactGroup_def RCOSETS_def)
   1.323    hence "h ` X = {h g}" by (auto simp add: kernel_def r_coset_def g intro!: imageI)
   1.324 @@ -985,16 +969,16 @@
   1.325       and X': "X' \<in> carrier (G Mod kernel G H h)"
   1.326    then
   1.327    obtain g and g'
   1.328 -           where "g \<in> carrier G" and "g' \<in> carrier G" 
   1.329 +           where "g \<in> carrier G" and "g' \<in> carrier G"
   1.330               and "X = kernel G H h #> g" and "X' = kernel G H h #> g'"
   1.331      by (auto simp add: FactGroup_def RCOSETS_def)
   1.332 -  hence all: "\<forall>x\<in>X. h x = h g" "\<forall>x\<in>X'. h x = h g'" 
   1.333 +  hence all: "\<forall>x\<in>X. h x = h g" "\<forall>x\<in>X'. h x = h g'"
   1.334      and Xsub: "X \<subseteq> carrier G" and X'sub: "X' \<subseteq> carrier G"
   1.335      by (force simp add: kernel_def r_coset_def image_def)+
   1.336    hence "h ` (X <#> X') = {h g \<otimes>\<^bsub>H\<^esub> h g'}" using X X'
   1.337      by (auto dest!: FactGroup_nonempty intro!: image_eqI
   1.338 -             simp add: set_mult_def 
   1.339 -                       subsetD [OF Xsub] subsetD [OF X'sub]) 
   1.340 +             simp add: set_mult_def
   1.341 +                       subsetD [OF Xsub] subsetD [OF X'sub])
   1.342    then show "the_elem (h ` (X <#> X')) = the_elem (h ` X) \<otimes>\<^bsub>H\<^esub> the_elem (h ` X')"
   1.343      by (auto simp add: all FactGroup_nonempty X X' the_elem_image_unique)
   1.344  qed
   1.345 @@ -1005,28 +989,28 @@
   1.346       "\<lbrakk>g \<in> carrier G; g' \<in> carrier G; h g = h g'\<rbrakk>
   1.347        \<Longrightarrow>  kernel G H h #> g \<subseteq> kernel G H h #> g'"
   1.348  apply (clarsimp simp add: kernel_def r_coset_def)
   1.349 -apply (rename_tac y)  
   1.350 -apply (rule_tac x="y \<otimes> g \<otimes> inv g'" in exI) 
   1.351 -apply (simp add: G.m_assoc) 
   1.352 +apply (rename_tac y)
   1.353 +apply (rule_tac x="y \<otimes> g \<otimes> inv g'" in exI)
   1.354 +apply (simp add: G.m_assoc)
   1.355  done
   1.356  
   1.357  lemma (in group_hom) FactGroup_inj_on:
   1.358       "inj_on (\<lambda>X. the_elem (h ` X)) (carrier (G Mod kernel G H h))"
   1.359 -proof (simp add: inj_on_def, clarify) 
   1.360 +proof (simp add: inj_on_def, clarify)
   1.361    fix X and X'
   1.362    assume X:  "X  \<in> carrier (G Mod kernel G H h)"
   1.363       and X': "X' \<in> carrier (G Mod kernel G H h)"
   1.364    then
   1.365    obtain g and g'
   1.366 -           where gX: "g \<in> carrier G"  "g' \<in> carrier G" 
   1.367 +           where gX: "g \<in> carrier G"  "g' \<in> carrier G"
   1.368                "X = kernel G H h #> g" "X' = kernel G H h #> g'"
   1.369      by (auto simp add: FactGroup_def RCOSETS_def)
   1.370 -  hence all: "\<forall>x\<in>X. h x = h g" "\<forall>x\<in>X'. h x = h g'" 
   1.371 +  hence all: "\<forall>x\<in>X. h x = h g" "\<forall>x\<in>X'. h x = h g'"
   1.372      by (force simp add: kernel_def r_coset_def image_def)+
   1.373    assume "the_elem (h ` X) = the_elem (h ` X')"
   1.374    hence h: "h g = h g'"
   1.375 -    by (simp add: all FactGroup_nonempty X X' the_elem_image_unique) 
   1.376 -  show "X=X'" by (rule equalityI) (simp_all add: FactGroup_subset h gX) 
   1.377 +    by (simp add: all FactGroup_nonempty X X' the_elem_image_unique)
   1.378 +  show "X=X'" by (rule equalityI) (simp_all add: FactGroup_subset h gX)
   1.379  qed
   1.380  
   1.381  text\<open>If the homomorphism @{term h} is onto @{term H}, then so is the
   1.382 @@ -1042,10 +1026,10 @@
   1.383      fix y
   1.384      assume y: "y \<in> carrier H"
   1.385      with h obtain g where g: "g \<in> carrier G" "h g = y"
   1.386 -      by (blast elim: equalityE) 
   1.387 -    hence "(\<Union>x\<in>kernel G H h #> g. {h x}) = {y}" 
   1.388 -      by (auto simp add: y kernel_def r_coset_def) 
   1.389 -    with g show "y \<in> (\<lambda>X. the_elem (h ` X)) ` carrier (G Mod kernel G H h)" 
   1.390 +      by (blast elim: equalityE)
   1.391 +    hence "(\<Union>x\<in>kernel G H h #> g. {h x}) = {y}"
   1.392 +      by (auto simp add: y kernel_def r_coset_def)
   1.393 +    with g show "y \<in> (\<lambda>X. the_elem (h ` X)) ` carrier (G Mod kernel G H h)"
   1.394        apply (auto intro!: bexI image_eqI simp add: FactGroup_def RCOSETS_def)
   1.395        apply (subst the_elem_image_unique)
   1.396        apply auto
   1.397 @@ -1059,8 +1043,8 @@
   1.398  theorem (in group_hom) FactGroup_iso_set:
   1.399    "h ` carrier G = carrier H
   1.400     \<Longrightarrow> (\<lambda>X. the_elem (h`X)) \<in> iso (G Mod (kernel G H h)) H"
   1.401 -by (simp add: iso_def FactGroup_hom FactGroup_inj_on bij_betw_def 
   1.402 -              FactGroup_onto) 
   1.403 +by (simp add: iso_def FactGroup_hom FactGroup_inj_on bij_betw_def
   1.404 +              FactGroup_onto)
   1.405  
   1.406  corollary (in group_hom) FactGroup_iso :
   1.407    "h ` carrier G = carrier H
   1.408 @@ -1137,7 +1121,7 @@
   1.409                   \<forall>ya\<in>carrier (K Mod N).  x \<times> y = xa \<times> ya \<longrightarrow> x = xa \<and> y = ya)"
   1.410      unfolding  FactGroup_def using times_eq_iff subgroup.rcosets_non_empty
   1.411      by (metis assms(2) assms(3) normal_def partial_object.select_convs(1))
   1.412 -  moreover have "(\<lambda>(X, Y). X \<times> Y) ` (carrier (G Mod H) \<times> carrier (K Mod N)) = 
   1.413 +  moreover have "(\<lambda>(X, Y). X \<times> Y) ` (carrier (G Mod H) \<times> carrier (K Mod N)) =
   1.414                                       carrier (G \<times>\<times> K Mod H \<times> N)"
   1.415      unfolding image_def  apply auto using R apply force
   1.416      unfolding DirProd_def FactGroup_def RCOSETS_def r_coset_def by force
   1.417 @@ -1168,7 +1152,7 @@
   1.418    assumes "subgroup H G"
   1.419    shows "(carrier G) <#> H = carrier G"
   1.420  proof
   1.421 -  show "(carrier G)<#>H \<subseteq> carrier G" 
   1.422 +  show "(carrier G)<#>H \<subseteq> carrier G"
   1.423      unfolding set_mult_def using subgroup.subset assms by blast
   1.424  next
   1.425    have " (carrier G) #>  \<one> = carrier G" unfolding set_mult_def r_coset_def group_axioms by simp
   1.426 @@ -1179,18 +1163,14 @@
   1.427  
   1.428  (*Same lemma as above, but everything is included in a subgroup*)
   1.429  lemma (in group) set_mult_subgroup_idem:
   1.430 -  assumes "subgroup H G"
   1.431 -    and "subgroup N (G\<lparr>carrier:=H\<rparr>)"
   1.432 -  shows "H<#>N = H"
   1.433 -  using group.set_mult_carrier_idem[OF subgroup_imp_group] subgroup.subset assms
   1.434 -  by (metis monoid.cases_scheme order_refl partial_object.simps(1)
   1.435 -      partial_object.update_convs(1) subgroup_set_mult_equality)
   1.436 +  assumes HG: "subgroup H G" and NG: "subgroup N (G \<lparr> carrier := H \<rparr>)"
   1.437 +  shows "H <#> N = H"
   1.438 +  using group.set_mult_carrier_idem[OF subgroup.subgroup_is_group[OF HG group_axioms] NG] by simp
   1.439  
   1.440  (*A normal subgroup is commutative with set_mult*)
   1.441  lemma (in group) commut_normal:
   1.442 -  assumes "subgroup H G"
   1.443 -    and "N\<lhd>G"
   1.444 -  shows "H<#>N = N<#>H" 
   1.445 +  assumes "subgroup H G" and "N\<lhd>G"
   1.446 +  shows "H<#>N = N<#>H"
   1.447  proof-
   1.448    have aux1: "{H <#> N} = {\<Union>h\<in>H. h <# N }" unfolding set_mult_def l_coset_def by auto
   1.449    also have "... = {\<Union>h\<in>H. N #> h }" using assms normal.coset_eq subgroup.mem_carrier by fastforce
   1.450 @@ -1200,23 +1180,10 @@
   1.451  
   1.452  (*Same lemma as above, but everything is included in a subgroup*)
   1.453  lemma (in group) commut_normal_subgroup:
   1.454 -  assumes "subgroup H G"
   1.455 -    and "N\<lhd>(G\<lparr>carrier:=H\<rparr>)"
   1.456 -    and "subgroup K (G\<lparr>carrier:=H\<rparr>)"
   1.457 -  shows "K<#>N = N<#>K"
   1.458 -proof-
   1.459 -  have "N \<subseteq> carrier (G\<lparr>carrier := H\<rparr>)" using assms normal_imp_subgroup subgroup.subset by blast
   1.460 -  hence NH : "N \<subseteq> H" by simp
   1.461 -  have "K \<subseteq> carrier(G\<lparr>carrier := H\<rparr>)" using subgroup.subset assms by blast
   1.462 -  hence KH : "K \<subseteq> H" by simp
   1.463 -  have Egal : "K <#>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N = N <#>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> K"
   1.464 -  using group.commut_normal[where ?G = "G\<lparr>carrier :=H\<rparr>", of K N,OF subgroup_imp_group[OF assms(1)]
   1.465 -               assms(3) assms(2)] by auto
   1.466 -  also have "... = N <#> K" using subgroup_set_mult_equality[of H N K, OF assms(1) NH KH] by auto
   1.467 -  moreover have "K <#>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N = K <#> N"
   1.468 -    using subgroup_set_mult_equality[of H K N, OF assms(1) KH NH] by auto
   1.469 -  ultimately show "K<#>N = N<#>K" by auto
   1.470 -qed
   1.471 +  assumes "subgroup H G" and "N \<lhd> (G\<lparr> carrier := H \<rparr>)"
   1.472 +    and "subgroup K (G \<lparr> carrier := H \<rparr>)"
   1.473 +  shows "K <#> N = N <#> K"
   1.474 +  using group.commut_normal[OF subgroup.subgroup_is_group[OF assms(1) group_axioms] assms(3,2)] by simp
   1.475  
   1.476  
   1.477  
   1.478 @@ -1226,7 +1193,7 @@
   1.479    assumes "subgroup H G"
   1.480      and "subgroup K G"
   1.481      and "H1\<lhd>G\<lparr>carrier := H\<rparr>"
   1.482 -  shows " (H1\<inter>K)\<lhd>(G\<lparr>carrier:= (H\<inter>K)\<rparr>)" 
   1.483 +  shows " (H1\<inter>K)\<lhd>(G\<lparr>carrier:= (H\<inter>K)\<rparr>)"
   1.484  proof-
   1.485    define HK and H1K and GH and GHK
   1.486      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.487 @@ -1243,10 +1210,10 @@
   1.488      next
   1.489        show "subgroup (H\<inter>K) G" using HK_def subgroups_Inter_pair assms by auto
   1.490      next
   1.491 -      have "H1 \<subseteq> (carrier (G\<lparr>carrier:=H\<rparr>))" 
   1.492 +      have "H1 \<subseteq> (carrier (G\<lparr>carrier:=H\<rparr>))"
   1.493          using  assms(3) normal_imp_subgroup subgroup.subset by blast
   1.494        also have "... \<subseteq> H" by simp
   1.495 -      thus "H1K \<subseteq>H\<inter>K" 
   1.496 +      thus "H1K \<subseteq>H\<inter>K"
   1.497          using H1K_def calculation by auto
   1.498      qed
   1.499      thus "subgroup H1K GHK" using GHK_def by simp
   1.500 @@ -1254,7 +1221,7 @@
   1.501      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.502      proof-
   1.503        have invHK: "\<lbrakk>y\<in>HK\<rbrakk> \<Longrightarrow> inv\<^bsub>GHK\<^esub> y = inv\<^bsub>GH\<^esub> y"
   1.504 -        using subgroup_inv_equality assms HK_def GH_def GHK_def subgroups_Inter_pair by simp
   1.505 +        using m_inv_consistent assms HK_def GH_def GHK_def subgroups_Inter_pair by simp
   1.506        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.507          using HK_def by simp
   1.508        fix x assume p: "x\<in>carrier GHK"
   1.509 @@ -1263,17 +1230,17 @@
   1.510          using GHK_def HK_def by simp
   1.511        hence xHK:"x\<in>HK" using p by auto
   1.512        hence invx:"inv\<^bsub>GHK\<^esub> x = inv\<^bsub>GH\<^esub> x"
   1.513 -        using invHK assms GHK_def HK_def GH_def subgroup_inv_equality subgroups_Inter_pair by simp
   1.514 +        using invHK assms GHK_def HK_def GH_def m_inv_consistent subgroups_Inter_pair by simp
   1.515        have "H1\<subseteq>carrier(GH)"
   1.516          using assms GH_def normal_imp_subgroup subgroup.subset by blast
   1.517 -      hence hHK:"h\<in>HK" 
   1.518 +      hence hHK:"h\<in>HK"
   1.519          using p2 H1K_def HK_def GH_def by auto
   1.520        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.521          using invx invHK multHK GHK_def GH_def by auto
   1.522 -      have xH:"x\<in>carrier(GH)" 
   1.523 -        using xHK HK_def GH_def by auto 
   1.524 +      have xH:"x\<in>carrier(GH)"
   1.525 +        using xHK HK_def GH_def by auto
   1.526        have hH:"h\<in>carrier(GH)"
   1.527 -        using hHK HK_def GH_def by auto 
   1.528 +        using hHK HK_def GH_def by auto
   1.529        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.530          using assms normal_invE GH_def normal.inv_op_closed2 by fastforce
   1.531        hence INCL_1 : "x \<otimes>\<^bsub>GH\<^esub> h \<otimes>\<^bsub>GH\<^esub> inv\<^bsub>GH\<^esub> x \<in> H1"
     2.1 --- a/src/HOL/Algebra/Group.thy	Sat Jun 30 18:58:13 2018 +0100
     2.2 +++ b/src/HOL/Algebra/Group.thy	Sun Jul 01 16:13:25 2018 +0100
     2.3 @@ -590,12 +590,18 @@
     2.4      by (rule monoid.group_l_invI) (auto intro: l_inv mem_carrier)
     2.5  qed
     2.6  
     2.7 -lemma (in group) subgroup_inv_equality:
     2.8 +lemma subgroup_is_submonoid:
     2.9 +  assumes "subgroup H G" shows "submonoid H G"
    2.10 +  using assms by (auto intro: submonoid.intro simp add: subgroup_def)
    2.11 +
    2.12 +lemma (in group) subgroup_Units:
    2.13 +  assumes "subgroup H G" shows "H \<subseteq> Units (G \<lparr> carrier := H \<rparr>)"
    2.14 +  using group.Units[OF subgroup.subgroup_is_group[OF assms group_axioms]] by simp
    2.15 +
    2.16 +lemma (in group) m_inv_consistent:
    2.17    assumes "subgroup H G" "x \<in> H"
    2.18 -  shows "m_inv (G \<lparr>carrier := H\<rparr>) x = inv x"
    2.19 -  unfolding m_inv_def apply auto
    2.20 -  using subgroup.m_inv_closed[OF assms] inv_equality
    2.21 -  by (metis (no_types, hide_lams) assms subgroup.mem_carrier)
    2.22 +  shows "inv\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> x = inv x"
    2.23 +  using assms m_inv_monoid_consistent[OF _ subgroup_is_submonoid] subgroup_Units[of H] by auto
    2.24  
    2.25  lemma (in group) int_pow_consistent: (* by Paulo *)
    2.26    assumes "subgroup H G" "x \<in> H"
    2.27 @@ -616,7 +622,7 @@
    2.28    also have " ... = (inv x) [^] (nat (- n))"
    2.29      by (metis assms nat_pow_inv subgroup.mem_carrier)
    2.30    also have " ... = (inv\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> x) [^]\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> (nat (- n))"
    2.31 -    using subgroup_inv_equality[OF assms] nat_pow_consistent by auto
    2.32 +    using m_inv_consistent[OF assms] nat_pow_consistent by auto
    2.33    also have " ... = inv\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> (x [^]\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> (nat (- n)))"
    2.34      using group.nat_pow_inv[OF subgroup.subgroup_is_group[OF assms(1) is_group]] assms(2) by auto
    2.35    also have " ... = x [^]\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> n"
    2.36 @@ -1290,18 +1296,16 @@
    2.37    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
    2.38    have K: "\<one> \<in> I" using assms(2) by (auto simp add: subgroup_def)
    2.39    have "(\<And>x. x \<in> I \<Longrightarrow> inv x \<in> I)" using assms  subgroup.m_inv_closed H
    2.40 -    by (metis H1 H2  subgroup_inv_equality subsetCE)
    2.41 +    by (metis H1 H2 m_inv_consistent subsetCE)
    2.42    thus "\<one> \<in> I \<and> (\<forall>x. x \<in> I \<longrightarrow> inv x \<in> I)" using K by blast
    2.43  qed
    2.44  
    2.45  (*A subgroup included in another subgroup is a subgroup of the subgroup*)
    2.46  lemma (in group) subgroup_incl:
    2.47 -  assumes "subgroup I G"
    2.48 -    and "subgroup J G"
    2.49 -    and "I\<subseteq>J"
    2.50 -  shows "subgroup I (G\<lparr>carrier:=J\<rparr>)"using assms subgroup_inv_equality
    2.51 -  by (auto simp add: subgroup_def)
    2.52 -
    2.53 +  assumes "subgroup I G" and "subgroup J G" and "I \<subseteq> J"
    2.54 +  shows "subgroup I (G \<lparr> carrier := J \<rparr>)"
    2.55 +  using group.group_incl_imp_subgroup[of "G \<lparr> carrier := J \<rparr>" I]
    2.56 +        assms(1-2)[THEN subgroup.subgroup_is_group[OF _ group_axioms]] assms(3) by auto
    2.57  
    2.58  
    2.59  subsection \<open>The Lattice of Subgroups of a Group\<close>
    2.60 @@ -1433,7 +1437,7 @@
    2.61  lemma units_of_one: "one (units_of G) = one G"
    2.62    by (auto simp: units_of_def)
    2.63  
    2.64 -lemma (in monoid) units_of_inv: 
    2.65 +lemma (in monoid) units_of_inv:
    2.66    assumes "x \<in> Units G"
    2.67    shows "m_inv (units_of G) x = m_inv G x"
    2.68    by (simp add: assms group.inv_equality units_group units_of_carrier units_of_mult units_of_one)
     3.1 --- a/src/HOL/Algebra/Zassenhaus.thy	Sat Jun 30 18:58:13 2018 +0100
     3.2 +++ b/src/HOL/Algebra/Zassenhaus.thy	Sun Jul 01 16:13:25 2018 +0100
     3.3 @@ -43,7 +43,7 @@
     3.4      ultimately have "x \<otimes>\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> h = x \<otimes> h" by simp
     3.5      moreover have " inv\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> x =  inv x"
     3.6        using xnormalizer
     3.7 -      by (simp add: assms normalizer_imp_subgroup subgroup.subset subgroup_inv_equality)
     3.8 +      by (simp add: assms normalizer_imp_subgroup subgroup.subset m_inv_consistent)
     3.9      ultimately  have xhxegal: "x \<otimes>\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> h
    3.10                  \<otimes>\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> inv\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> x
    3.11                    = x \<otimes>h \<otimes> inv x"
    3.12 @@ -172,7 +172,7 @@
    3.13    also have "... \<subseteq> K" by simp
    3.14    finally have Incl2:"N \<subseteq> K" by simp
    3.15    have "(N <#>\<^bsub>G\<lparr>carrier := K\<rparr>\<^esub> H) = (N <#> H)"
    3.16 -    using subgroup_set_mult_equality[of K] assms Incl1 Incl2 by simp
    3.17 +    using set_mult_consistent by simp
    3.18    thus "subgroup (N<#>H) (G\<lparr>carrier:=K\<rparr>)" using Hyp by auto
    3.19  qed
    3.20  
    3.21 @@ -332,8 +332,7 @@
    3.22           G\<lparr>carrier := normalizer G N, carrier := H\<rparr> Mod N \<inter> H =
    3.23            (G\<lparr>carrier:= N<#>H\<rparr> Mod N)  \<cong>
    3.24           G\<lparr>carrier := normalizer G N, carrier := H\<rparr> Mod N \<inter> H"
    3.25 -    using subgroup_set_mult_equality[OF  normalizer_imp_subgroup[OF subgroup.subset[OF assms(2)]], of N H]
    3.26 -          subgroup.subset[OF assms(3)]
    3.27 +    using subgroup.subset[OF assms(3)]
    3.28            subgroup.subset[OF normal_imp_subgroup[OF subgroup_in_normalizer[OF assms(2)]]]
    3.29      by simp
    3.30    ultimately have "G\<lparr>carrier := normalizer G N,
    3.31 @@ -493,7 +492,7 @@
    3.32      hence allG : "h1 \<in> carrier G" "hk \<in> carrier G" "x \<in> carrier G"
    3.33        using assms subgroup.subset h1hk_def normal_imp_subgroup incl_subgroup apply blast+.
    3.34      hence "x <#\<^bsub>G\<lparr>carrier := H1 <#> H\<inter>K\<rparr>\<^esub> (H1 <#> H\<inter>K1) =h1 \<otimes> hk <# (H1 <#> H\<inter>K1)"
    3.35 -      using subgroup_set_mult_equality subgroup.subset xH h1hk_def by (simp add: l_coset_def)
    3.36 +      using subgroup.subset xH h1hk_def by (simp add: l_coset_def)
    3.37      also have "... = h1 <# (hk <# (H1 <#> H\<inter>K1))"
    3.38        using lcos_m_assoc[OF subgroup.subset[OF incl_subgroup[OF assms(1) subH1]]allG(1)allG(2)]
    3.39        by (metis allG(1) allG(2) assms(1) incl_subgroup lcos_m_assoc subH2 subgroup.subset)
    3.40 @@ -535,7 +534,7 @@
    3.41      finally have eq1 : "x <#\<^bsub>G\<lparr>carrier := H1 <#> H \<inter> K\<rparr>\<^esub> (H1 <#> H \<inter> K1) = H1 <#> (H \<inter> K1) #> hk"
    3.42        by (simp add: allG(2) all_inclG inf.coboundedI2 setmult_rcos_assoc)
    3.43      have "H1 <#> H \<inter> K1 #>\<^bsub>G\<lparr>carrier := H1 <#> H \<inter> K\<rparr>\<^esub> x = H1 <#> H \<inter> K1 #> (h1 \<otimes> hk)"
    3.44 -      using subgroup_set_mult_equality subgroup.subset xH h1hk_def by (simp add: r_coset_def)
    3.45 +      using subgroup.subset xH h1hk_def by (simp add: r_coset_def)
    3.46      also have "... = H1 <#> H \<inter> K1 #> h1 #> hk"
    3.47        using coset_mult_assoc by (simp add: allG all_inclG inf.coboundedI2 setmult_subset_G)
    3.48      also have"... =  H \<inter> K1 <#> H1 #> h1 #> hk"