merged
authorpaulson
Sat Jul 28 16:06:51 2018 +0100 (11 months ago)
changeset 686883a58abb11840
parent 68686 7f8db1c4ebec
parent 68687 2976a4a3b126
child 68706 f3763989d589
merged
     1.1 --- a/src/HOL/Algebra/Bij.thy	Sat Jul 28 07:28:18 2018 +0200
     1.2 +++ b/src/HOL/Algebra/Bij.thy	Sat Jul 28 16:06:51 2018 +0100
     1.3 @@ -46,15 +46,11 @@
     1.4    by (simp add: Bij_def compose_inv_into_id)
     1.5  
     1.6  theorem group_BijGroup: "group (BijGroup S)"
     1.7 -apply (simp add: BijGroup_def)
     1.8 -apply (rule groupI)
     1.9 -    apply (simp add: compose_Bij)
    1.10 -   apply (simp add: id_Bij)
    1.11 -  apply (simp add: compose_Bij)
    1.12 -  apply (blast intro: compose_assoc [symmetric] dest: Bij_imp_funcset)
    1.13 - apply (simp add: id_Bij Bij_imp_funcset Bij_imp_extensional, simp)
    1.14 -apply (blast intro: Bij_compose_restrict_eq restrict_inv_into_Bij)
    1.15 -done
    1.16 +  apply (simp add: BijGroup_def)
    1.17 +  apply (rule groupI)
    1.18 +      apply (auto simp: compose_Bij id_Bij Bij_imp_funcset Bij_imp_extensional compose_assoc [symmetric])
    1.19 +  apply (blast intro: Bij_compose_restrict_eq restrict_inv_into_Bij)
    1.20 +  done
    1.21  
    1.22  
    1.23  subsection\<open>Automorphisms Form a Group\<close>
    1.24 @@ -63,13 +59,18 @@
    1.25  by (simp add: Bij_def bij_betw_def inv_into_into)
    1.26  
    1.27  lemma Bij_inv_into_lemma:
    1.28 - assumes eq: "\<And>x y. \<lbrakk>x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> h(g x y) = g (h x) (h y)"
    1.29 - shows "\<lbrakk>h \<in> Bij S;  g \<in> S \<rightarrow> S \<rightarrow> S;  x \<in> S;  y \<in> S\<rbrakk>
    1.30 -        \<Longrightarrow> inv_into S h (g x y) = g (inv_into S h x) (inv_into S h y)"
    1.31 -apply (simp add: Bij_def bij_betw_def)
    1.32 -apply (subgoal_tac "\<exists>x'\<in>S. \<exists>y'\<in>S. x = h x' \<and> y = h y'", clarify)
    1.33 - apply (simp add: eq [symmetric] inv_f_f funcset_mem [THEN funcset_mem], blast)
    1.34 -done
    1.35 +  assumes eq: "\<And>x y. \<lbrakk>x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> h(g x y) = g (h x) (h y)"
    1.36 +      and hg: "h \<in> Bij S" "g \<in> S \<rightarrow> S \<rightarrow> S" and "x \<in> S" "y \<in> S"
    1.37 +  shows "inv_into S h (g x y) = g (inv_into S h x) (inv_into S h y)"
    1.38 +proof -
    1.39 +  have "h ` S = S"
    1.40 +    by (metis (no_types) Bij_def Int_iff assms(2) bij_betw_def mem_Collect_eq)
    1.41 +  with \<open>x \<in> S\<close> \<open>y \<in> S\<close> have "\<exists>x'\<in>S. \<exists>y'\<in>S. x = h x' \<and> y = h y'"
    1.42 +    by auto
    1.43 +  then show ?thesis
    1.44 +    using assms
    1.45 +    by (auto simp add: Bij_def bij_betw_def eq [symmetric] inv_f_f funcset_mem [THEN funcset_mem])
    1.46 +qed
    1.47  
    1.48  
    1.49  definition
    1.50 @@ -94,8 +95,7 @@
    1.51  
    1.52  lemma inv_BijGroup:
    1.53       "f \<in> Bij S \<Longrightarrow> m_inv (BijGroup S) f = (\<lambda>x \<in> S. (inv_into S f) x)"
    1.54 -apply (rule group.inv_equality)
    1.55 -apply (rule group_BijGroup)
    1.56 +apply (rule group.inv_equality [OF group_BijGroup])
    1.57  apply (simp_all add:BijGroup_def restrict_inv_into_Bij Bij_compose_restrict_eq)
    1.58  done
    1.59  
     2.1 --- a/src/HOL/Algebra/Coset.thy	Sat Jul 28 07:28:18 2018 +0200
     2.2 +++ b/src/HOL/Algebra/Coset.thy	Sat Jul 28 16:06:51 2018 +0100
     2.3 @@ -440,45 +440,36 @@
     2.4    shows "N \<lhd> G"
     2.5    using assms normal_inv_iff by blast
     2.6  
     2.7 -corollary (in group) normal_invE:
     2.8 -  assumes "N \<lhd> G"
     2.9 -  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"
    2.10 -  using assms normal_inv_iff apply blast
    2.11 -  by (simp add: assms normal.inv_op_closed2)
    2.12 -
    2.13 -
    2.14 -lemma (in group) one_is_normal :
    2.15 -   "{\<one>} \<lhd> G"
    2.16 -proof(intro normal_invI )
    2.17 +lemma (in group) one_is_normal: "{\<one>} \<lhd> G"
    2.18 +proof(intro normal_invI)
    2.19    show "subgroup {\<one>} G"
    2.20      by (simp add: subgroup_def)
    2.21 -  show "\<And>x h. x \<in> carrier G \<Longrightarrow> h \<in> {\<one>} \<Longrightarrow> x \<otimes> h \<otimes> inv x \<in> {\<one>}" by simp
    2.22 -qed
    2.23 +qed simp
    2.24  
    2.25  
    2.26  subsection\<open>More Properties of Left Cosets\<close>
    2.27  
    2.28  lemma (in group) l_repr_independence:
    2.29 -  assumes "y \<in> x <# H" "x \<in> carrier G" "subgroup H G"
    2.30 +  assumes "y \<in> x <# H" "x \<in> carrier G" and HG: "subgroup H G"
    2.31    shows "x <# H = y <# H"
    2.32  proof -
    2.33    obtain h' where h': "h' \<in> H" "y = x \<otimes> h'"
    2.34      using assms(1) unfolding l_coset_def by blast
    2.35    hence "x \<otimes> h = y \<otimes> ((inv h') \<otimes> h)" if "h \<in> H" for h
    2.36    proof -
    2.37 -    have f3: "h' \<in> carrier G"
    2.38 -      by (meson assms(3) h'(1) subgroup.mem_carrier)
    2.39 -    have f4: "h \<in> carrier G"
    2.40 -      by (meson assms(3) subgroup.mem_carrier that)
    2.41 -    then show ?thesis
    2.42 -      by (metis assms(2) f3 h'(2) inv_closed inv_solve_right m_assoc m_closed)
    2.43 +    have "h' \<in> carrier G"
    2.44 +      by (meson HG h'(1) subgroup.mem_carrier)
    2.45 +    moreover have "h \<in> carrier G"
    2.46 +      by (meson HG subgroup.mem_carrier that)
    2.47 +    ultimately show ?thesis
    2.48 +      by (metis assms(2) h'(2) inv_closed inv_solve_right m_assoc m_closed)
    2.49    qed
    2.50 -  hence "\<And> xh. xh \<in> x <# H \<Longrightarrow> xh \<in> y <# H"
    2.51 -    unfolding l_coset_def by (metis (no_types, lifting) UN_iff assms(3) h'(1) subgroup_def)
    2.52 -  moreover have "\<And> h. h \<in> H \<Longrightarrow> y \<otimes> h = x \<otimes> (h' \<otimes> h)"
    2.53 -    using h' by (meson assms(2) assms(3) m_assoc subgroup.mem_carrier)
    2.54 -  hence "\<And> yh. yh \<in> y <# H \<Longrightarrow> yh \<in> x <# H"
    2.55 -    unfolding l_coset_def using subgroup.m_closed[OF assms(3) h'(1)] by blast
    2.56 +  hence "\<And>xh. xh \<in> x <# H \<Longrightarrow> xh \<in> y <# H"
    2.57 +    unfolding l_coset_def by (metis (no_types, lifting) UN_iff HG h'(1) subgroup_def)
    2.58 +  moreover have "\<And>h. h \<in> H \<Longrightarrow> y \<otimes> h = x \<otimes> (h' \<otimes> h)"
    2.59 +    using h' by (meson assms(2) HG m_assoc subgroup.mem_carrier)
    2.60 +  hence "\<And>yh. yh \<in> y <# H \<Longrightarrow> yh \<in> x <# H"
    2.61 +    unfolding l_coset_def using subgroup.m_closed[OF HG h'(1)] by blast
    2.62    ultimately show ?thesis by blast
    2.63  qed
    2.64  
    2.65 @@ -655,8 +646,8 @@
    2.66    shows "hb \<otimes> a \<in> (\<Union>h\<in>H. {h \<otimes> b})"
    2.67  proof -
    2.68    interpret subgroup H G by fact
    2.69 -  from p show ?thesis apply (rule_tac UN_I [of "hb \<otimes> ((inv ha) \<otimes> h)"])
    2.70 -    apply blast by (simp add: inv_solve_left m_assoc)
    2.71 +  from p show ?thesis 
    2.72 +    by (rule_tac UN_I [of "hb \<otimes> ((inv ha) \<otimes> h)"]) (auto simp: inv_solve_left m_assoc)
    2.73  qed
    2.74  
    2.75  lemma (in group) rcos_disjoint:
    2.76 @@ -666,9 +657,8 @@
    2.77  proof -
    2.78    interpret subgroup H G by fact
    2.79    from p show ?thesis
    2.80 -    apply (simp add: RCOSETS_def r_coset_def)
    2.81 -    apply (blast intro: rcos_equation assms sym)
    2.82 -    done
    2.83 +    unfolding RCOSETS_def r_coset_def
    2.84 +    by (blast intro: rcos_equation assms sym)
    2.85  qed
    2.86  
    2.87  
    2.88 @@ -761,26 +751,26 @@
    2.89  proof -
    2.90    interpret subgroup H G by fact
    2.91    show ?thesis
    2.92 -    apply (rule equalityI)
    2.93 -    apply (force simp add: RCOSETS_def r_coset_def)
    2.94 -    apply (auto simp add: RCOSETS_def intro: rcos_self assms)
    2.95 -    done
    2.96 +    unfolding RCOSETS_def r_coset_def by auto
    2.97  qed
    2.98  
    2.99  lemma (in group) cosets_finite:
   2.100       "\<lbrakk>c \<in> rcosets H;  H \<subseteq> carrier G;  finite (carrier G)\<rbrakk> \<Longrightarrow> finite c"
   2.101 -apply (auto simp add: RCOSETS_def)
   2.102 -apply (simp add: r_coset_subset_G [THEN finite_subset])
   2.103 -done
   2.104 +  unfolding RCOSETS_def
   2.105 +  by (auto simp add: r_coset_subset_G [THEN finite_subset])
   2.106  
   2.107  text\<open>The next two lemmas support the proof of \<open>card_cosets_equal\<close>.\<close>
   2.108  lemma (in group) inj_on_f:
   2.109 -    "\<lbrakk>H \<subseteq> carrier G;  a \<in> carrier G\<rbrakk> \<Longrightarrow> inj_on (\<lambda>y. y \<otimes> inv a) (H #> a)"
   2.110 -apply (rule inj_onI)
   2.111 -apply (subgoal_tac "x \<in> carrier G \<and> y \<in> carrier G")
   2.112 - prefer 2 apply (blast intro: r_coset_subset_G [THEN subsetD])
   2.113 -apply (simp add: subsetD)
   2.114 -done
   2.115 +  assumes "H \<subseteq> carrier G" and a: "a \<in> carrier G"
   2.116 +  shows "inj_on (\<lambda>y. y \<otimes> inv a) (H #> a)"
   2.117 +proof 
   2.118 +  fix x y
   2.119 +  assume "x \<in> H #> a" "y \<in> H #> a" and xy: "x \<otimes> inv a = y \<otimes> inv a"
   2.120 +  then have "x \<in> carrier G" "y \<in> carrier G"
   2.121 +    using assms r_coset_subset_G by blast+
   2.122 +  with xy a show "x = y"
   2.123 +    by auto
   2.124 +qed
   2.125  
   2.126  lemma (in group) inj_on_g:
   2.127      "\<lbrakk>H \<subseteq> carrier G;  a \<in> carrier G\<rbrakk> \<Longrightarrow> inj_on (\<lambda>y. y \<otimes> a) H"
   2.128 @@ -827,16 +817,17 @@
   2.129    using rcosets_part_G by auto
   2.130  
   2.131  proposition (in group) lagrange_finite:
   2.132 -     "\<lbrakk>finite(carrier G); subgroup H G\<rbrakk>
   2.133 -      \<Longrightarrow> card(rcosets H) * card(H) = order(G)"
   2.134 -apply (simp (no_asm_simp) add: order_def rcosets_part_G [symmetric])
   2.135 -apply (subst mult.commute)
   2.136 -apply (rule card_partition)
   2.137 -   apply (simp add: rcosets_subset_PowG [THEN finite_subset])
   2.138 -  apply (simp add: rcosets_part_G)
   2.139 -  apply (simp add: card_rcosets_equal subgroup.subset)
   2.140 -apply (simp add: rcos_disjoint)
   2.141 -done
   2.142 +  assumes "finite(carrier G)" and HG: "subgroup H G"
   2.143 +  shows "card(rcosets H) * card(H) = order(G)"
   2.144 +proof -
   2.145 +  have "card H * card (rcosets H) = card (\<Union>(rcosets H))"
   2.146 +  proof (rule card_partition)
   2.147 +    show "\<And>c1 c2. \<lbrakk>c1 \<in> rcosets H; c2 \<in> rcosets H; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}"
   2.148 +      using HG rcos_disjoint by auto
   2.149 +  qed (auto simp: assms finite_UnionD rcosets_part_G card_rcosets_equal subgroup.subset)
   2.150 +  then show ?thesis
   2.151 +    by (simp add: HG mult.commute order_def rcosets_part_G)
   2.152 +qed
   2.153  
   2.154  theorem (in group) lagrange:
   2.155    assumes "subgroup H G"
   2.156 @@ -844,29 +835,29 @@
   2.157  proof (cases "finite (carrier G)")
   2.158    case True thus ?thesis using lagrange_finite assms by simp
   2.159  next
   2.160 -  case False note inf_G = this
   2.161 +  case False 
   2.162    thus ?thesis
   2.163    proof (cases "finite H")
   2.164 -    case False thus ?thesis using inf_G  by (simp add: order_def)
   2.165 +    case False thus ?thesis using \<open>infinite (carrier G)\<close>  by (simp add: order_def)
   2.166    next
   2.167 -    case True note finite_H = this
   2.168 +    case True 
   2.169      have "infinite (rcosets H)"
   2.170 -    proof (rule ccontr)
   2.171 -      assume "\<not> infinite (rcosets H)"
   2.172 +    proof 
   2.173 +      assume "finite (rcosets H)"
   2.174        hence finite_rcos: "finite (rcosets H)" by simp
   2.175        hence "card (\<Union>(rcosets H)) = (\<Sum>R\<in>(rcosets H). card R)"
   2.176 -        using card_Union_disjoint[of "rcosets H"] finite_H rcos_disjoint[OF assms(1)]
   2.177 +        using card_Union_disjoint[of "rcosets H"] \<open>finite H\<close> rcos_disjoint[OF assms(1)]
   2.178                rcosets_finite[where ?H = H] by (simp add: assms subgroup.subset)
   2.179        hence "order G = (\<Sum>R\<in>(rcosets H). card R)"
   2.180          by (simp add: assms order_def rcosets_part_G)
   2.181        hence "order G = (\<Sum>R\<in>(rcosets H). card H)"
   2.182          using card_rcosets_equal by (simp add: assms subgroup.subset)
   2.183        hence "order G = (card H) * (card (rcosets H))" by simp
   2.184 -      hence "order G \<noteq> 0" using finite_rcos finite_H assms ex_in_conv
   2.185 +      hence "order G \<noteq> 0" using finite_rcos \<open>finite H\<close> assms ex_in_conv
   2.186                                  rcosets_part_G subgroup.one_closed by fastforce
   2.187 -      thus False using inf_G order_gt_0_iff_finite by blast
   2.188 +      thus False using \<open>infinite (carrier G)\<close> order_gt_0_iff_finite by blast
   2.189      qed
   2.190 -    thus ?thesis using inf_G by (simp add: order_def)
   2.191 +    thus ?thesis using \<open>infinite (carrier G)\<close> by (simp add: order_def)
   2.192    qed
   2.193  qed
   2.194  
   2.195 @@ -908,8 +899,8 @@
   2.196  
   2.197  theorem (in normal) factorgroup_is_group:
   2.198    "group (G Mod H)"
   2.199 -apply (simp add: FactGroup_def)
   2.200 -apply (rule groupI)
   2.201 +  unfolding FactGroup_def
   2.202 +  apply (rule groupI)
   2.203      apply (simp add: setmult_closed)
   2.204     apply (simp add: normal_imp_subgroup subgroup_in_rcosets [OF is_group])
   2.205    apply (simp add: restrictI setmult_closed rcosets_assoc)
   2.206 @@ -922,10 +913,20 @@
   2.207    by (simp add: FactGroup_def)
   2.208  
   2.209  lemma (in normal) inv_FactGroup:
   2.210 -     "X \<in> carrier (G Mod H) \<Longrightarrow> inv\<^bsub>G Mod H\<^esub> X = set_inv X"
   2.211 -apply (rule group.inv_equality [OF factorgroup_is_group])
   2.212 -apply (simp_all add: FactGroup_def setinv_closed rcosets_inv_mult_group_eq)
   2.213 -done
   2.214 +  assumes "X \<in> carrier (G Mod H)"
   2.215 +  shows "inv\<^bsub>G Mod H\<^esub> X = set_inv X"
   2.216 +proof -
   2.217 +  have X: "X \<in> rcosets H"
   2.218 +    using assms by (simp add: FactGroup_def)
   2.219 +  moreover have "set_inv X <#> X = H"
   2.220 +    using X by (simp add: normal.rcosets_inv_mult_group_eq normal_axioms)
   2.221 +  moreover have "Group.group (G Mod H)"
   2.222 +    using normal.factorgroup_is_group normal_axioms by blast
   2.223 +  moreover have "set_inv X \<in> rcosets H"
   2.224 +    by (simp add: \<open>X \<in> rcosets H\<close> setinv_closed)
   2.225 +  ultimately show ?thesis
   2.226 +    by (simp add: FactGroup_def group.inv_equality)
   2.227 +qed
   2.228  
   2.229  text\<open>The coset map is a homomorphism from @{term G} to the quotient group
   2.230    @{term "G Mod H"}\<close>
   2.231 @@ -945,15 +946,13 @@
   2.232    where "kernel G H h = {x. x \<in> carrier G \<and> h x = \<one>\<^bsub>H\<^esub>}"
   2.233  
   2.234  lemma (in group_hom) subgroup_kernel: "subgroup (kernel G H h) G"
   2.235 -apply (rule subgroup.intro)
   2.236 -apply (auto simp add: kernel_def group.intro is_group)
   2.237 -done
   2.238 +  by (auto simp add: kernel_def group.intro is_group intro: subgroup.intro)
   2.239  
   2.240  text\<open>The kernel of a homomorphism is a normal subgroup\<close>
   2.241  lemma (in group_hom) normal_kernel: "(kernel G H h) \<lhd> G"
   2.242 -apply (simp add: G.normal_inv_iff subgroup_kernel)
   2.243 -apply (simp add: kernel_def)
   2.244 -done
   2.245 +  apply (simp only: G.normal_inv_iff subgroup_kernel)
   2.246 +  apply (simp add: kernel_def)
   2.247 +  done
   2.248  
   2.249  lemma (in group_hom) FactGroup_nonempty:
   2.250    assumes X: "X \<in> carrier (G Mod kernel G H h)"
   2.251 @@ -982,37 +981,40 @@
   2.252  
   2.253  lemma (in group_hom) FactGroup_hom:
   2.254       "(\<lambda>X. the_elem (h`X)) \<in> hom (G Mod (kernel G H h)) H"
   2.255 -apply (simp add: hom_def FactGroup_the_elem_mem normal.factorgroup_is_group [OF normal_kernel] group.axioms monoid.m_closed)
   2.256 -proof (intro ballI)
   2.257 -  fix X and X'
   2.258 -  assume X:  "X  \<in> carrier (G Mod kernel G H h)"
   2.259 -     and X': "X' \<in> carrier (G Mod kernel G H h)"
   2.260 -  then
   2.261 -  obtain g and g'
   2.262 -           where "g \<in> carrier G" and "g' \<in> carrier G"
   2.263 -             and "X = kernel G H h #> g" and "X' = kernel G H h #> g'"
   2.264 -    by (auto simp add: FactGroup_def RCOSETS_def)
   2.265 -  hence all: "\<forall>x\<in>X. h x = h g" "\<forall>x\<in>X'. h x = h g'"
   2.266 -    and Xsub: "X \<subseteq> carrier G" and X'sub: "X' \<subseteq> carrier G"
   2.267 -    by (force simp add: kernel_def r_coset_def image_def)+
   2.268 -  hence "h ` (X <#> X') = {h g \<otimes>\<^bsub>H\<^esub> h g'}" using X X'
   2.269 -    by (auto dest!: FactGroup_nonempty intro!: image_eqI
   2.270 -             simp add: set_mult_def
   2.271 -                       subsetD [OF Xsub] subsetD [OF X'sub])
   2.272 -  then show "the_elem (h ` (X <#> X')) = the_elem (h ` X) \<otimes>\<^bsub>H\<^esub> the_elem (h ` X')"
   2.273 -    by (auto simp add: all FactGroup_nonempty X X' the_elem_image_unique)
   2.274 +proof -
   2.275 +  have "the_elem (h ` (X <#> X')) = the_elem (h ` X) \<otimes>\<^bsub>H\<^esub> the_elem (h ` X')"
   2.276 +    if X: "X  \<in> carrier (G Mod kernel G H h)" and X': "X' \<in> carrier (G Mod kernel G H h)" for X X'
   2.277 +  proof -
   2.278 +    obtain g and g'
   2.279 +      where "g \<in> carrier G" and "g' \<in> carrier G"
   2.280 +        and "X = kernel G H h #> g" and "X' = kernel G H h #> g'"
   2.281 +      using X X' by (auto simp add: FactGroup_def RCOSETS_def)
   2.282 +    hence all: "\<forall>x\<in>X. h x = h g" "\<forall>x\<in>X'. h x = h g'"
   2.283 +      and Xsub: "X \<subseteq> carrier G" and X'sub: "X' \<subseteq> carrier G"
   2.284 +      by (force simp add: kernel_def r_coset_def image_def)+
   2.285 +    hence "h ` (X <#> X') = {h g \<otimes>\<^bsub>H\<^esub> h g'}" using X X'
   2.286 +      by (auto dest!: FactGroup_nonempty intro!: image_eqI
   2.287 +          simp add: set_mult_def
   2.288 +          subsetD [OF Xsub] subsetD [OF X'sub])
   2.289 +    then show "the_elem (h ` (X <#> X')) = the_elem (h ` X) \<otimes>\<^bsub>H\<^esub> the_elem (h ` X')"
   2.290 +      by (auto simp add: all FactGroup_nonempty X X' the_elem_image_unique)
   2.291 +  qed
   2.292 +  then show ?thesis
   2.293 +    by (simp add: hom_def FactGroup_the_elem_mem normal.factorgroup_is_group [OF normal_kernel] group.axioms monoid.m_closed)
   2.294  qed
   2.295  
   2.296  
   2.297  text\<open>Lemma for the following injectivity result\<close>
   2.298  lemma (in group_hom) FactGroup_subset:
   2.299 -     "\<lbrakk>g \<in> carrier G; g' \<in> carrier G; h g = h g'\<rbrakk>
   2.300 -      \<Longrightarrow>  kernel G H h #> g \<subseteq> kernel G H h #> g'"
   2.301 -apply (clarsimp simp add: kernel_def r_coset_def)
   2.302 -apply (rename_tac y)
   2.303 -apply (rule_tac x="y \<otimes> g \<otimes> inv g'" in exI)
   2.304 -apply (simp add: G.m_assoc)
   2.305 -done
   2.306 +  assumes "g \<in> carrier G" "g' \<in> carrier G" "h g = h g'"
   2.307 +  shows "kernel G H h #> g \<subseteq> kernel G H h #> g'"
   2.308 +  unfolding kernel_def r_coset_def
   2.309 +proof clarsimp
   2.310 +  fix y 
   2.311 +  assume "y \<in> carrier G" "h y = \<one>\<^bsub>H\<^esub>"
   2.312 +  with assms show "\<exists>x. x \<in> carrier G \<and> h x = \<one>\<^bsub>H\<^esub> \<and> y \<otimes> g = x \<otimes> g'"
   2.313 +    by (rule_tac x="y \<otimes> g \<otimes> inv g'" in exI) (auto simp: G.m_assoc)
   2.314 +qed
   2.315  
   2.316  lemma (in group_hom) FactGroup_inj_on:
   2.317       "inj_on (\<lambda>X. the_elem (h ` X)) (carrier (G Mod kernel G H h))"
   2.318 @@ -1113,13 +1115,13 @@
   2.319      from hHN obtain h1 h2 where h1h2 : "h1 \<in> H" "h2 \<in> N" "h = (h1,h2)"
   2.320        unfolding DirProd_def by fastforce
   2.321      hence h1h2GK : "h1 \<in> carrier G" "h2 \<in> carrier K"
   2.322 -      using normal_imp_subgroup subgroup.subset assms apply blast+.
   2.323 +      using normal_imp_subgroup subgroup.subset assms by blast+
   2.324      have "inv\<^bsub>G \<times>\<times> K\<^esub> x = (inv\<^bsub>G\<^esub> x1,inv\<^bsub>K\<^esub> x2)"
   2.325        using inv_DirProd[OF group_axioms assms(1) x1x2(1)x1x2(2)] x1x2 by auto
   2.326      hence "x \<otimes>\<^bsub>G \<times>\<times> K\<^esub> h \<otimes>\<^bsub>G \<times>\<times> K\<^esub> inv\<^bsub>G \<times>\<times> K\<^esub> x = (x1 \<otimes> h1 \<otimes> inv x1,x2 \<otimes>\<^bsub>K\<^esub> h2 \<otimes>\<^bsub>K\<^esub> inv\<^bsub>K\<^esub> x2)"
   2.327        using h1h2 x1x2 h1h2GK by auto
   2.328      moreover have "x1 \<otimes> h1 \<otimes> inv x1 \<in> H" "x2 \<otimes>\<^bsub>K\<^esub> h2 \<otimes>\<^bsub>K\<^esub> inv\<^bsub>K\<^esub> x2 \<in> N"
   2.329 -      using normal_invE group.normal_invE[OF assms(1)] assms x1x2 h1h2 apply auto.
   2.330 +      using assms x1x2 h1h2 assms by (simp_all add: normal.inv_op_closed2)
   2.331      hence "(x1 \<otimes> h1 \<otimes> inv x1, x2 \<otimes>\<^bsub>K\<^esub> h2 \<otimes>\<^bsub>K\<^esub> inv\<^bsub>K\<^esub> x2)\<in> H \<times> N" by auto
   2.332      ultimately show " x \<otimes>\<^bsub>G \<times>\<times> K\<^esub> h \<otimes>\<^bsub>G \<times>\<times> K\<^esub> inv\<^bsub>G \<times>\<times> K\<^esub> x \<in> H \<times> N" by auto
   2.333    qed
   2.334 @@ -1133,7 +1135,7 @@
   2.335  
   2.336  proof-
   2.337    have R :"(\<lambda>(X, Y). X \<times> Y) \<in> carrier (G Mod H) \<times> carrier (K Mod N) \<rightarrow> carrier (G \<times>\<times> K Mod H \<times> N)"
   2.338 -    unfolding r_coset_def Sigma_def DirProd_def FactGroup_def RCOSETS_def apply simp by blast
   2.339 +    unfolding r_coset_def Sigma_def DirProd_def FactGroup_def RCOSETS_def by force
   2.340    moreover have "(\<forall>x\<in>carrier (G Mod H). \<forall>y\<in>carrier (K Mod N). \<forall>xa\<in>carrier (G Mod H).
   2.341                  \<forall>ya\<in>carrier (K Mod N). (x <#> xa) \<times> (y <#>\<^bsub>K\<^esub> ya) =  x \<times> y <#>\<^bsub>G \<times>\<times> K\<^esub> xa \<times> ya)"
   2.342      unfolding set_mult_def by force
   2.343 @@ -1143,8 +1145,14 @@
   2.344      by (metis assms(2) assms(3) normal_def partial_object.select_convs(1))
   2.345    moreover have "(\<lambda>(X, Y). X \<times> Y) ` (carrier (G Mod H) \<times> carrier (K Mod N)) =
   2.346                                       carrier (G \<times>\<times> K Mod H \<times> N)"
   2.347 -    unfolding image_def  apply auto using R apply force
   2.348 -    unfolding DirProd_def FactGroup_def RCOSETS_def r_coset_def by force
   2.349 +  proof -
   2.350 +    have 1: "\<And>x a b. \<lbrakk>a \<in> carrier (G Mod H); b \<in> carrier (K Mod N)\<rbrakk> \<Longrightarrow> a \<times> b \<in> carrier (G \<times>\<times> K Mod H \<times> N)"
   2.351 +      using R by force
   2.352 +    have 2: "\<And>z. z \<in> carrier (G \<times>\<times> K Mod H \<times> N) \<Longrightarrow> \<exists>x\<in>carrier (G Mod H). \<exists>y\<in>carrier (K Mod N). z = x \<times> y"
   2.353 +      unfolding DirProd_def FactGroup_def RCOSETS_def r_coset_def by force
   2.354 +    show ?thesis
   2.355 +      unfolding image_def by (auto simp: intro: 1 2)
   2.356 +  qed
   2.357    ultimately show ?thesis
   2.358      unfolding iso_def hom_def bij_betw_def inj_on_def by simp
   2.359  qed
   2.360 @@ -1262,7 +1270,7 @@
   2.361        have hH:"h\<in>carrier(GH)"
   2.362          using hHK HK_def GH_def by auto
   2.363        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)"
   2.364 -        using assms normal_invE GH_def normal.inv_op_closed2 by fastforce
   2.365 +        using assms GH_def normal.inv_op_closed2 by fastforce
   2.366        hence INCL_1 : "x \<otimes>\<^bsub>GH\<^esub> h \<otimes>\<^bsub>GH\<^esub> inv\<^bsub>GH\<^esub> x \<in> H1"
   2.367          using  xH H1K_def p2 by blast
   2.368        have " x \<otimes>\<^bsub>GH\<^esub> h \<otimes>\<^bsub>GH\<^esub> inv\<^bsub>GH\<^esub> x \<in> HK"
   2.369 @@ -1275,7 +1283,6 @@
   2.370    qed
   2.371  qed
   2.372  
   2.373 -
   2.374  lemma (in group) normal_inter_subgroup:
   2.375    assumes "subgroup H G"
   2.376      and "N \<lhd> G"
   2.377 @@ -1288,8 +1295,8 @@
   2.378    ultimately have "N \<inter> H \<lhd> G\<lparr>carrier := K \<inter> H\<rparr>"
   2.379      using normal_inter[of K H N] assms(1) by blast
   2.380    moreover have "K \<inter> H = H" using K_def assms subgroup.subset by blast
   2.381 -  ultimately show "normal (N\<inter>H) (G\<lparr>carrier := H\<rparr>)" by auto
   2.382 +  ultimately show "normal (N\<inter>H) (G\<lparr>carrier := H\<rparr>)"
   2.383 + by auto
   2.384  qed
   2.385  
   2.386 -
   2.387  end
     3.1 --- a/src/HOL/Algebra/Embedded_Algebras.thy	Sat Jul 28 07:28:18 2018 +0200
     3.2 +++ b/src/HOL/Algebra/Embedded_Algebras.thy	Sat Jul 28 16:06:51 2018 +0100
     3.3 @@ -187,7 +187,7 @@
     3.4  
     3.5  corollary Span_is_add_subgroup:
     3.6    "set Us \<subseteq> carrier R \<Longrightarrow> subgroup (Span K Us) (add_monoid R)"
     3.7 -  using line_extension_is_subgroup add.normal_invE(1)[OF add.one_is_normal] by (induct Us) (auto)
     3.8 +  using line_extension_is_subgroup normal_imp_subgroup[OF add.one_is_normal] by (induct Us) (auto)
     3.9  
    3.10  lemma line_extension_smult_closed:
    3.11    assumes "\<And>k v. \<lbrakk> k \<in> K; v \<in> E \<rbrakk> \<Longrightarrow> k \<otimes> v \<in> E" and "E \<subseteq> carrier R" "a \<in> carrier R"
    3.12 @@ -246,7 +246,7 @@
    3.13  
    3.14  lemma line_extension_of_combine_set:
    3.15    assumes "u \<in> carrier R"
    3.16 -  shows "line_extension K u { combine Ks Us | Ks. set Ks \<subseteq> K } = 
    3.17 +  shows "line_extension K u { combine Ks Us | Ks. set Ks \<subseteq> K } =
    3.18                  { combine Ks (u # Us) | Ks. set Ks \<subseteq> K }"
    3.19    (is "?line_extension = ?combinations")
    3.20  proof
    3.21 @@ -292,7 +292,7 @@
    3.22  
    3.23  lemma line_extension_of_combine_set_length_version:
    3.24    assumes "u \<in> carrier R"
    3.25 -  shows "line_extension K u { combine Ks Us | Ks. length Ks = length Us \<and> set Ks \<subseteq> K } = 
    3.26 +  shows "line_extension K u { combine Ks Us | Ks. length Ks = length Us \<and> set Ks \<subseteq> K } =
    3.27                        { combine Ks (u # Us) | Ks. length Ks = length (u # Us) \<and> set Ks \<subseteq> K }"
    3.28    (is "?line_extension = ?combinations")
    3.29  proof
    3.30 @@ -329,16 +329,16 @@
    3.31    assumes "set Us \<subseteq> carrier R" and "a \<in> carrier R"
    3.32    shows "a \<in> Span K Us \<longleftrightarrow> (\<exists>k \<in> K - { \<zero> }. \<exists>Ks. set Ks \<subseteq> K \<and> combine (k # Ks) (a # Us) = \<zero>)"
    3.33           (is "?in_Span \<longleftrightarrow> ?exists_combine")
    3.34 -proof 
    3.35 +proof
    3.36    assume "?in_Span"
    3.37    then obtain Ks where Ks: "set Ks \<subseteq> K" "a = combine Ks Us"
    3.38      using Span_eq_combine_set[OF assms(1)] by auto
    3.39    hence "((\<ominus> \<one>) \<otimes> a) \<oplus> a = combine ((\<ominus> \<one>) # Ks) (a # Us)"
    3.40      by auto
    3.41    moreover have "((\<ominus> \<one>) \<otimes> a) \<oplus> a = \<zero>"
    3.42 -    using assms(2) l_minus l_neg by auto  
    3.43 +    using assms(2) l_minus l_neg by auto
    3.44    moreover have "\<ominus> \<one> \<noteq> \<zero>"
    3.45 -    using subfieldE(6)[OF K] l_neg by force 
    3.46 +    using subfieldE(6)[OF K] l_neg by force
    3.47    ultimately show "?exists_combine"
    3.48      using subring_props(3,5) Ks(1) by (force simp del: combine.simps)
    3.49  next
    3.50 @@ -391,14 +391,14 @@
    3.51      proof (induct Ks Us rule: combine.induct)
    3.52        case (1 k Ks u Us)
    3.53        hence "k \<in> K" and "u \<in> set (u # Us)" by auto
    3.54 -      hence "k \<otimes> u \<in> E" 
    3.55 +      hence "k \<otimes> u \<in> E"
    3.56          using 1(4) unfolding set_mult_def by auto
    3.57        moreover have "K <#> set Us \<subseteq> E"
    3.58          using 1(4) unfolding set_mult_def by auto
    3.59        hence "combine Ks Us \<in> E"
    3.60          using 1 by auto
    3.61        ultimately show ?case
    3.62 -        using add.subgroupE(4)[OF assms(2)] by auto 
    3.63 +        using add.subgroupE(4)[OF assms(2)] by auto
    3.64      next
    3.65        case "2_1" thus ?case
    3.66          using subgroup.one_closed[OF assms(2)] by auto
    3.67 @@ -436,7 +436,7 @@
    3.68        hence "combine [ k ] (u # Us) \<in> Span K (u # Us)"
    3.69          using Span_eq_combine_set[OF Cons(2)] by (auto simp del: combine.simps)
    3.70        moreover have "k \<in> carrier R" and "u \<in> carrier R"
    3.71 -        using Cons(2) k subring_props(1) by (blast, auto) 
    3.72 +        using Cons(2) k subring_props(1) by (blast, auto)
    3.73        ultimately show "k \<otimes> u \<in> Span K (u # Us)"
    3.74          by (auto simp del: Span.simps)
    3.75      qed
    3.76 @@ -455,7 +455,7 @@
    3.77  corollary Span_same_set:
    3.78    assumes "set Us \<subseteq> carrier R"
    3.79    shows "set Us = set Vs \<Longrightarrow> Span K Us = Span K Vs"
    3.80 -  using Span_eq_generate assms by auto 
    3.81 +  using Span_eq_generate assms by auto
    3.82  
    3.83  corollary Span_incl: "set Us \<subseteq> carrier R \<Longrightarrow> K <#> (set Us) \<subseteq> Span K Us"
    3.84    using Span_eq_generate generate.incl[of _ _ "add_monoid R"] by auto
    3.85 @@ -583,7 +583,7 @@
    3.86    moreover have "Span K Us \<subseteq> Span K (u # Us)"
    3.87      using mono_Span independent_in_carrier[OF assms] by auto
    3.88    ultimately show ?thesis
    3.89 -    using independent_backwards(1)[OF assms] by auto 
    3.90 +    using independent_backwards(1)[OF assms] by auto
    3.91  qed
    3.92  
    3.93  corollary independent_replacement:
    3.94 @@ -624,7 +624,7 @@
    3.95    from assms show "Span K Us \<inter> Span K Vs = { \<zero> }"
    3.96    proof (induct Us rule: list.induct)
    3.97      case Nil thus ?case
    3.98 -      using Span_subgroup_props(2)[OF independent_in_carrier[of K Vs]] by simp 
    3.99 +      using Span_subgroup_props(2)[OF independent_in_carrier[of K Vs]] by simp
   3.100    next
   3.101      case (Cons u Us)
   3.102      hence IH: "Span K Us \<inter> Span K Vs = {\<zero>}" by auto
   3.103 @@ -653,7 +653,7 @@
   3.104        hence "k \<otimes> u = (\<ominus> u') \<oplus> v'"
   3.105          using in_carrier(1) k(2) u'(2) v'(2) add.m_comm r_neg1 by auto
   3.106        hence "k \<otimes> u \<in> Span K (Us @ Vs)"
   3.107 -        using Span_subgroup_props(4)[OF in_carrier(2) u'(1)] v'(1) 
   3.108 +        using Span_subgroup_props(4)[OF in_carrier(2) u'(1)] v'(1)
   3.109                Span_append_eq_set_add[OF in_carrier(2-3)] unfolding set_add_def' by blast
   3.110        hence "u \<in> Span K (Us @ Vs)"
   3.111          using Cons(2) Span_m_inv_simprule[OF _ _ in_carrier(1), of "Us @ Vs" k]
   3.112 @@ -678,7 +678,7 @@
   3.113    hence in_carrier:
   3.114      "u \<in> carrier R" "set Us \<subseteq> carrier R" "set Vs \<subseteq> carrier R" "set (u # Us) \<subseteq> carrier R"
   3.115      using Cons(2-3)[THEN independent_in_carrier] by auto
   3.116 -  hence "Span K Us \<subseteq> Span K (u # Us)" 
   3.117 +  hence "Span K Us \<subseteq> Span K (u # Us)"
   3.118      using mono_Span by auto
   3.119    hence "Span K Us \<inter> Span K Vs = { \<zero> }"
   3.120      using Cons(4) Span_subgroup_props(2)[OF in_carrier(2)] by auto
   3.121 @@ -733,7 +733,7 @@
   3.122      hence "combine Ks' Us = \<zero>"
   3.123        using combine_in_carrier[OF _ Us, of Ks'] Ks' u Cons(3) subring_props(1) unfolding Ks by auto
   3.124      hence "set (take (length Us) Ks') \<subseteq> { \<zero> }"
   3.125 -      using Cons(1)[OF Ks' _ independent_backwards(2)[OF Cons(4)]] by simp 
   3.126 +      using Cons(1)[OF Ks' _ independent_backwards(2)[OF Cons(4)]] by simp
   3.127      thus ?thesis
   3.128        using k_zero unfolding Ks by auto
   3.129    qed
   3.130 @@ -878,10 +878,10 @@
   3.131      case (Cons u Us)
   3.132      then obtain Vs' Vs'' where Vs: "Vs = Vs' @ (u # Vs'')"
   3.133        by (metis list.set_intros(1) split_list)
   3.134 -    
   3.135 +
   3.136      have in_carrier: "u \<in> carrier R" "set Us \<subseteq> carrier R"
   3.137 -      using independent_in_carrier[OF Cons(2)] by auto 
   3.138 -    
   3.139 +      using independent_in_carrier[OF Cons(2)] by auto
   3.140 +
   3.141      have "distinct Vs"
   3.142        using Cons(3-4) independent_distinct[OF Cons(2)]
   3.143        by (metis card_distinct distinct_card)
   3.144 @@ -905,7 +905,7 @@
   3.145    shows "\<exists>Vs'. set Vs' \<subseteq> set Vs \<and> length Vs' = length Us' \<and> independent K (Vs' @ Us)"
   3.146    using assms
   3.147  proof (induct "length Us'" arbitrary: Us' Us)
   3.148 -  case 0 thus ?case by auto 
   3.149 +  case 0 thus ?case by auto
   3.150  next
   3.151    case (Suc n)
   3.152    then obtain u Us'' where Us'': "Us' = Us'' @ [u]"
   3.153 @@ -1074,9 +1074,9 @@
   3.154          using space_subgroup_props(1)[OF assms(1)] li_Cons[OF _ v(2) step(4)] by auto
   3.155        then obtain Vs
   3.156          where "length (Vs @ (v # Us)) = n" "independent K (Vs @ (v # Us))" "Span K (Vs @ (v # Us)) = E"
   3.157 -        using step(3)[of "v # Us"] step(1-2,4-6) v by auto 
   3.158 +        using step(3)[of "v # Us"] step(1-2,4-6) v by auto
   3.159        thus ?case
   3.160 -        by (metis append.assoc append_Cons append_Nil)  
   3.161 +        by (metis append.assoc append_Cons append_Nil)
   3.162      qed } note aux_lemma = this
   3.163  
   3.164    have "length Us \<le> n"
   3.165 @@ -1119,7 +1119,7 @@
   3.166    hence in_carrier: "set Us \<subseteq> carrier R" "set (Vs @ Bs) \<subseteq> carrier R"
   3.167      using independent_in_carrier[OF Us(2)] independent_in_carrier[OF Vs(2)] by auto
   3.168    hence "Span K Us \<inter> (Span K (Vs @ Bs)) \<subseteq> Span K Bs"
   3.169 -    using Bs(4) Us(3) Vs(3) mono_Span_append(1)[OF _ Bs(1), of Us] by auto 
   3.170 +    using Bs(4) Us(3) Vs(3) mono_Span_append(1)[OF _ Bs(1), of Us] by auto
   3.171    hence "Span K Us \<inter> (Span K (Vs @ Bs)) \<subseteq> { \<zero> }"
   3.172      using independent_split(3)[OF Us(2)] by blast
   3.173    hence "Span K Us \<inter> (Span K (Vs @ Bs)) = { \<zero> }"
   3.174 @@ -1147,7 +1147,7 @@
   3.175      ultimately show "v \<in> (Span K Us) <+>\<^bsub>R\<^esub> F"
   3.176        using u1' unfolding set_add_def' by auto
   3.177    qed
   3.178 -  ultimately have "Span K (Us @ (Vs @ Bs)) = E <+>\<^bsub>R\<^esub> F" 
   3.179 +  ultimately have "Span K (Us @ (Vs @ Bs)) = E <+>\<^bsub>R\<^esub> F"
   3.180      using Span_append_eq_set_add[OF in_carrier] Vs(3) by auto
   3.181  
   3.182    thus ?thesis using dim by simp
   3.183 @@ -1169,7 +1169,7 @@
   3.184      by (metis One_nat_def length_0_conv length_Suc_conv)
   3.185    have in_carrier: "set (map (\<lambda>u'. u' \<otimes> u) Us) \<subseteq> carrier R"
   3.186      using Us(1) u(1) by (induct Us) (auto)
   3.187 -  
   3.188 +
   3.189    have li: "independent K (map (\<lambda>u'. u' \<otimes> u) Us)"
   3.190    proof (rule trivial_combine_imp_independent[OF assms(1) in_carrier])
   3.191      fix Ks assume Ks: "set Ks \<subseteq> K" and "combine Ks (map (\<lambda>u'. u' \<otimes> u) Us) = \<zero>"
   3.192 @@ -1244,7 +1244,7 @@
   3.193    ultimately have "dimension (n * Suc m) K (Span F [ v ] <+>\<^bsub>R\<^esub> Span F Vs')"
   3.194      using dimension_direct_sum_space[OF assms(1) _ _ inter] by auto
   3.195    thus "dimension (n * Suc m) K E"
   3.196 -    using Span_append_eq_set_add[OF assms(2) li[THEN independent_in_carrier]] Vs(4) v by auto 
   3.197 +    using Span_append_eq_set_add[OF assms(2) li[THEN independent_in_carrier]] Vs(4) v by auto
   3.198  qed
   3.199  
   3.200  
   3.201 @@ -1271,14 +1271,14 @@
   3.202    hence "combine Ks Us = (combine (take (length Us) Ks) Us) \<oplus> \<zero>"
   3.203      using combine_append[OF _ _ assms(2), of "take (length Us) Ks" "drop (length Us) Ks" "[]"] len by auto
   3.204    also have " ... = combine (take (length Us) Ks) Us"
   3.205 -    using combine_in_carrier[OF set_t assms(2)] by auto 
   3.206 +    using combine_in_carrier[OF set_t assms(2)] by auto
   3.207    finally show "combine Ks Us = combine (take (length Us) Ks) Us" .
   3.208  qed
   3.209  *)
   3.210  
   3.211  (*
   3.212  lemma combine_normalize:
   3.213 -  assumes "set Ks \<subseteq> K" "set Us \<subseteq> carrier R" "a = combine Ks Us" 
   3.214 +  assumes "set Ks \<subseteq> K" "set Us \<subseteq> carrier R" "a = combine Ks Us"
   3.215    shows "\<exists>Ks'. set Ks' \<subseteq> K \<and> length Ks' = length Us \<and> a = combine Ks' Us"
   3.216  proof (cases "length Ks \<le> length Us")
   3.217    assume "\<not> length Ks \<le> length Us"
   3.218 @@ -1291,12 +1291,12 @@
   3.219  next
   3.220    assume len: "length Ks \<le> length Us"
   3.221    have Ks: "set Ks \<subseteq> carrier R" and set_r: "set (replicate (length Us - length Ks) \<zero>) \<subseteq> carrier R"
   3.222 -    using assms subring_props(1) zero_closed by (metis dual_order.trans, auto) 
   3.223 +    using assms subring_props(1) zero_closed by (metis dual_order.trans, auto)
   3.224    moreover
   3.225    have set_t: "set (take (length Ks) Us) \<subseteq> carrier R"
   3.226     and set_d: "set (drop (length Ks) Us) \<subseteq> carrier R"
   3.227      using assms(2) len dual_order.trans by (metis set_take_subset, metis set_drop_subset)
   3.228 -  ultimately 
   3.229 +  ultimately
   3.230    have "combine (Ks @ (replicate (length Us - length Ks) \<zero>)) Us =
   3.231         (combine Ks (take (length Ks) Us)) \<oplus>
   3.232         (combine (replicate (length Us - length Ks) \<zero>) (drop (length Ks) Us))"
     4.1 --- a/src/HOL/Algebra/Generated_Groups.thy	Sat Jul 28 07:28:18 2018 +0200
     4.2 +++ b/src/HOL/Algebra/Generated_Groups.thy	Sat Jul 28 16:06:51 2018 +0100
     4.3 @@ -466,7 +466,7 @@
     4.4    shows "derived G H \<lhd> G" unfolding derived_def
     4.5  proof (rule normal_generateI)
     4.6    show "(\<Union>h1 \<in> H. \<Union>h2 \<in> H. { h1 \<otimes> h2 \<otimes> inv h1 \<otimes> inv h2 }) \<subseteq> carrier G"
     4.7 -    using subgroup.subset assms normal_invE(1) by blast
     4.8 +    using subgroup.subset assms normal_imp_subgroup by blast
     4.9  next
    4.10    show "\<And>h g. \<lbrakk> h \<in> derived_set G H; g \<in> carrier G \<rbrakk> \<Longrightarrow> g \<otimes> h \<otimes> inv g \<in> derived_set G H"
    4.11    proof -
    4.12 @@ -474,7 +474,7 @@
    4.13      then obtain h1 h2 where h1: "h1 \<in> H" "h1 \<in> carrier G"
    4.14                          and h2: "h2 \<in> H" "h2 \<in> carrier G"
    4.15                          and h:  "h = h1 \<otimes> h2 \<otimes> inv h1 \<otimes> inv h2"
    4.16 -      using subgroup.subset assms normal_invE(1) by blast
    4.17 +      using subgroup.subset assms normal_imp_subgroup by blast
    4.18      hence "g \<otimes> h \<otimes> inv g =
    4.19             g \<otimes> h1 \<otimes> (inv g \<otimes> g) \<otimes> h2 \<otimes> (inv g \<otimes> g) \<otimes> inv h1 \<otimes> (inv g \<otimes> g) \<otimes> inv h2 \<otimes> inv g"
    4.20        by (simp add: g m_assoc)
    4.21 @@ -486,8 +486,8 @@
    4.22      have "g \<otimes> h \<otimes> inv g =
    4.23           (g \<otimes> h1 \<otimes> inv g) \<otimes> (g \<otimes> h2 \<otimes> inv g) \<otimes> inv (g \<otimes> h1 \<otimes> inv g) \<otimes> inv (g \<otimes> h2 \<otimes> inv g)"
    4.24        by (simp add: g h1 h2 inv_mult_group m_assoc)
    4.25 -    moreover have "g \<otimes> h1 \<otimes> inv g \<in> H" by (simp add: assms normal_invE(2) g h1)
    4.26 -    moreover have "g \<otimes> h2 \<otimes> inv g \<in> H" by (simp add: assms normal_invE(2) g h2)
    4.27 +    moreover have "g \<otimes> h1 \<otimes> inv g \<in> H" by (simp add: assms normal.inv_op_closed2 g h1)
    4.28 +    moreover have "g \<otimes> h2 \<otimes> inv g \<in> H" by (simp add: assms normal.inv_op_closed2 g h2)
    4.29      ultimately show "g \<otimes> h \<otimes> inv g \<in> derived_set G H" by blast
    4.30    qed
    4.31  qed
     5.1 --- a/src/HOL/Algebra/Group.thy	Sat Jul 28 07:28:18 2018 +0200
     5.2 +++ b/src/HOL/Algebra/Group.thy	Sat Jul 28 16:06:51 2018 +0100
     5.3 @@ -763,13 +763,13 @@
     5.4      and "subgroup I K"
     5.5    shows "subgroup (H \<times> I) (G \<times>\<times> K)"
     5.6  proof (intro group.group_incl_imp_subgroup[OF DirProd_group[OF assms(1)assms(3)]])
     5.7 -  have "H \<subseteq> carrier G" "I \<subseteq> carrier K" using subgroup.subset assms apply blast+.
     5.8 +  have "H \<subseteq> carrier G" "I \<subseteq> carrier K" using subgroup.subset assms by blast+
     5.9    thus "(H \<times> I) \<subseteq> carrier (G \<times>\<times> K)" unfolding DirProd_def by auto
    5.10    have "Group.group ((G\<lparr>carrier := H\<rparr>) \<times>\<times> (K\<lparr>carrier := I\<rparr>))"
    5.11      using DirProd_group[OF subgroup.subgroup_is_group[OF assms(2)assms(1)]
    5.12          subgroup.subgroup_is_group[OF assms(4)assms(3)]].
    5.13    moreover have "((G\<lparr>carrier := H\<rparr>) \<times>\<times> (K\<lparr>carrier := I\<rparr>)) = ((G \<times>\<times> K)\<lparr>carrier := H \<times> I\<rparr>)"
    5.14 -    unfolding DirProd_def using assms apply simp.
    5.15 +    unfolding DirProd_def using assms by simp
    5.16    ultimately show "Group.group ((G \<times>\<times> K)\<lparr>carrier := H \<times> I\<rparr>)" by simp
    5.17  qed
    5.18  
    5.19 @@ -1054,7 +1054,7 @@
    5.20  lemma (in group_hom) img_is_subgroup: "subgroup (h ` (carrier G)) H"
    5.21    apply (rule subgroupI)
    5.22    apply (auto simp add: image_subsetI)
    5.23 -  apply (metis (no_types, hide_lams) G.inv_closed hom_inv image_iff)
    5.24 +  apply (metis G.inv_closed hom_inv image_iff)
    5.25    by (metis G.monoid_axioms hom_mult image_eqI monoid.m_closed)
    5.26  
    5.27  lemma (in group_hom) subgroup_img_is_subgroup:
    5.28 @@ -1157,9 +1157,8 @@
    5.29    show "monoid (G\<lparr>carrier := H\<rparr>)"
    5.30      using submonoid.submonoid_is_monoid assms comm_monoid_axioms comm_monoid_def by blast
    5.31    show "\<And>x y. x \<in> carrier (G\<lparr>carrier := H\<rparr>) \<Longrightarrow> y \<in> carrier (G\<lparr>carrier := H\<rparr>)
    5.32 -        \<Longrightarrow> x \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> y = y \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> x" apply simp
    5.33 -    using  assms comm_monoid_axioms_def submonoid.mem_carrier
    5.34 -    by (metis m_comm)
    5.35 +        \<Longrightarrow> x \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> y = y \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> x" 
    5.36 +    by simp (meson assms m_comm submonoid.mem_carrier)
    5.37  qed
    5.38  
    5.39  locale comm_group = comm_monoid + group
     6.1 --- a/src/HOL/Algebra/Ideal.thy	Sat Jul 28 07:28:18 2018 +0200
     6.2 +++ b/src/HOL/Algebra/Ideal.thy	Sat Jul 28 16:06:51 2018 +0100
     6.3 @@ -128,10 +128,9 @@
     6.4  proof -
     6.5    interpret additive_subgroup I R by fact
     6.6    interpret cring R by fact
     6.7 -  show ?thesis apply intro_locales
     6.8 -    apply (intro ideal_axioms.intro)
     6.9 -    apply (erule (1) I_l_closed)
    6.10 -    apply (erule (1) I_r_closed)
    6.11 +  show ?thesis
    6.12 +    apply intro_locales
    6.13 +    apply (simp add: I_l_closed I_r_closed ideal_axioms_def)
    6.14      by (simp add: I_notcarr I_prime primeideal_axioms.intro)
    6.15  qed
    6.16  
     7.1 --- a/src/HOL/Algebra/RingHom.thy	Sat Jul 28 07:28:18 2018 +0200
     7.2 +++ b/src/HOL/Algebra/RingHom.thy	Sat Jul 28 16:06:51 2018 +0100
     7.3 @@ -20,11 +20,10 @@
     7.4    by standard (rule homh)
     7.5  
     7.6  sublocale ring_hom_ring \<subseteq> abelian_group?: abelian_group_hom R S
     7.7 -apply (intro abelian_group_homI R.is_abelian_group S.is_abelian_group)
     7.8 -apply (intro group_hom.intro group_hom_axioms.intro R.a_group S.a_group)
     7.9 -apply (insert homh, unfold hom_def ring_hom_def)
    7.10 -apply simp
    7.11 -done
    7.12 +proof 
    7.13 +  show "h \<in> hom (add_monoid R) (add_monoid S)"
    7.14 +    using homh by (simp add: hom_def ring_hom_def)
    7.15 +qed
    7.16  
    7.17  lemma (in ring_hom_ring) is_ring_hom_ring:
    7.18    "ring_hom_ring R S h"
    7.19 @@ -33,8 +32,7 @@
    7.20  lemma ring_hom_ringI:
    7.21    fixes R (structure) and S (structure)
    7.22    assumes "ring R" "ring S"
    7.23 -  assumes (* morphism: "h \<in> carrier R \<rightarrow> carrier S" *)
    7.24 -          hom_closed: "!!x. x \<in> carrier R ==> h x \<in> carrier S"
    7.25 +  assumes hom_closed: "!!x. x \<in> carrier R ==> h x \<in> carrier S"
    7.26        and compatible_mult: "\<And>x y. [| x \<in> carrier R; y \<in> carrier R |] ==> h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y"
    7.27        and compatible_add: "\<And>x y. [| x \<in> carrier R; y \<in> carrier R |] ==> h (x \<oplus> y) = h x \<oplus>\<^bsub>S\<^esub> h y"
    7.28        and compatible_one: "h \<one> = \<one>\<^bsub>S\<^esub>"
    7.29 @@ -42,13 +40,12 @@
    7.30  proof -
    7.31    interpret ring R by fact
    7.32    interpret ring S by fact
    7.33 -  show ?thesis apply unfold_locales
    7.34 -apply (unfold ring_hom_def, safe)
    7.35 -   apply (simp add: hom_closed Pi_def)
    7.36 -  apply (erule (1) compatible_mult)
    7.37 - apply (erule (1) compatible_add)
    7.38 -apply (rule compatible_one)
    7.39 -done
    7.40 +  show ?thesis
    7.41 +  proof
    7.42 +    show "h \<in> ring_hom R S"
    7.43 +      unfolding ring_hom_def
    7.44 +      by (auto simp: compatible_mult compatible_add compatible_one hom_closed)
    7.45 +  qed
    7.46  qed
    7.47  
    7.48  lemma ring_hom_ringI2:
    7.49 @@ -58,11 +55,11 @@
    7.50  proof -
    7.51    interpret R: ring R by fact
    7.52    interpret S: ring S by fact
    7.53 -  show ?thesis apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro)
    7.54 -    apply (rule R.is_ring)
    7.55 -    apply (rule S.is_ring)
    7.56 -    apply (rule h)
    7.57 -    done
    7.58 +  show ?thesis 
    7.59 +  proof
    7.60 +    show "h \<in> ring_hom R S"
    7.61 +      using h .
    7.62 +  qed
    7.63  qed
    7.64  
    7.65  lemma ring_hom_ringI3:
    7.66 @@ -75,13 +72,11 @@
    7.67    interpret abelian_group_hom R S h by fact
    7.68    interpret R: ring R by fact
    7.69    interpret S: ring S by fact
    7.70 -  show ?thesis apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro, rule R.is_ring, rule S.is_ring)
    7.71 -    apply (insert group_hom.homh[OF a_group_hom])
    7.72 -    apply (unfold hom_def ring_hom_def, simp)
    7.73 -    apply safe
    7.74 -    apply (erule (1) compatible_mult)
    7.75 -    apply (rule compatible_one)
    7.76 -    done
    7.77 +  show ?thesis
    7.78 +  proof
    7.79 +    show "h \<in> ring_hom R S"
    7.80 +      unfolding ring_hom_def by (auto simp: compatible_one compatible_mult)
    7.81 +  qed
    7.82  qed
    7.83  
    7.84  lemma ring_hom_cringI:
    7.85 @@ -91,21 +86,22 @@
    7.86    interpret ring_hom_ring R S h by fact
    7.87    interpret R: cring R by fact
    7.88    interpret S: cring S by fact
    7.89 -  show ?thesis by (intro ring_hom_cring.intro ring_hom_cring_axioms.intro)
    7.90 -    (rule R.is_cring, rule S.is_cring, rule homh)
    7.91 +  show ?thesis 
    7.92 +  proof
    7.93 +    show "h \<in> ring_hom R S"
    7.94 +      by (simp add: homh)
    7.95 +  qed
    7.96  qed
    7.97  
    7.98  
    7.99  subsection \<open>The Kernel of a Ring Homomorphism\<close>
   7.100  
   7.101  \<comment> \<open>the kernel of a ring homomorphism is an ideal\<close>
   7.102 -lemma (in ring_hom_ring) kernel_is_ideal:
   7.103 -  shows "ideal (a_kernel R S h) R"
   7.104 -apply (rule idealI)
   7.105 -   apply (rule R.is_ring)
   7.106 -  apply (rule additive_subgroup.a_subgroup[OF additive_subgroup_a_kernel])
   7.107 - apply (unfold a_kernel_def', simp+)
   7.108 -done
   7.109 +lemma (in ring_hom_ring) kernel_is_ideal: "ideal (a_kernel R S h) R"
   7.110 +  apply (rule idealI [OF R.is_ring])
   7.111 +    apply (rule additive_subgroup.a_subgroup[OF additive_subgroup_a_kernel])
   7.112 +   apply (auto simp: a_kernel_def')
   7.113 +  done
   7.114  
   7.115  text \<open>Elements of the kernel are mapped to zero\<close>
   7.116  lemma (in abelian_group_hom) kernel_zero [simp]:
   7.117 @@ -174,29 +170,10 @@
   7.118  corollary (in ring_hom_ring) rcos_eq_homeq:
   7.119    assumes acarr: "a \<in> carrier R"
   7.120    shows "(a_kernel R S h) +> a = {x \<in> carrier R. h x = h a}"
   7.121 -  apply rule defer 1
   7.122 -   apply clarsimp defer 1
   7.123 -proof
   7.124 +proof -
   7.125    interpret ideal "a_kernel R S h" "R" by (rule kernel_is_ideal)
   7.126 -
   7.127 -  fix x
   7.128 -  assume xrcos: "x \<in> a_kernel R S h +> a"
   7.129 -  from acarr and this
   7.130 -  have xcarr: "x \<in> carrier R"
   7.131 -    by (rule a_elemrcos_carrier)
   7.132 -
   7.133 -  from xrcos
   7.134 -  have "h x = h a" by (rule rcos_imp_homeq[OF acarr])
   7.135 -  from xcarr and this
   7.136 -  show "x \<in> {x \<in> carrier R. h x = h a}" by fast
   7.137 -next
   7.138 -  interpret ideal "a_kernel R S h" "R" by (rule kernel_is_ideal)
   7.139 -
   7.140 -  fix x
   7.141 -  assume xcarr: "x \<in> carrier R"
   7.142 -    and hx: "h x = h a"
   7.143 -  from acarr xcarr hx
   7.144 -  show "x \<in> a_kernel R S h +> a" by (rule homeq_imp_rcos)
   7.145 +  show ?thesis
   7.146 +    using assms by (auto simp: intro: homeq_imp_rcos rcos_imp_homeq a_elemrcos_carrier)
   7.147  qed
   7.148  
   7.149  lemma (in ring_hom_ring) nat_pow_hom:
     8.1 --- a/src/HOL/Library/FuncSet.thy	Sat Jul 28 07:28:18 2018 +0200
     8.2 +++ b/src/HOL/Library/FuncSet.thy	Sat Jul 28 16:06:51 2018 +0100
     8.3 @@ -163,8 +163,6 @@
     8.4  
     8.5  lemma compose_assoc:
     8.6    assumes "f \<in> A \<rightarrow> B"
     8.7 -    and "g \<in> B \<rightarrow> C"
     8.8 -    and "h \<in> C \<rightarrow> D"
     8.9    shows "compose A h (compose A g f) = compose A (compose B h g) f"
    8.10    using assms by (simp add: fun_eq_iff Pi_def compose_def restrict_def)
    8.11