author paulson Sun Jul 01 16:13:25 2018 +0100 (9 months ago) changeset 68555 22d51874f37d parent 68552 391e89e03eef child 68556 fcffdcb8f506
a few more lemmas from Paulo and Martin
 src/HOL/Algebra/Coset.thy file | annotate | diff | revisions src/HOL/Algebra/Group.thy file | annotate | diff | revisions src/HOL/Algebra/Zassenhaus.thy file | annotate | diff | revisions
```     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.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.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.339 -                       subsetD [OF Xsub] subsetD [OF X'sub])
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.352 +apply (rename_tac y)
1.353 +apply (rule_tac x="y \<otimes> g \<otimes> inv g'" in exI)
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"
```