src/HOL/Algebra/Coset.thy
changeset 68555 22d51874f37d
parent 68517 6b5f15387353
child 68582 b9b9e2985878
     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"