author paulson Sat, 28 Jul 2018 16:06:51 +0100 changeset 68688 3a58abb11840 parent 68686 7f8db1c4ebec (current diff) parent 68687 2976a4a3b126 (diff) child 68706 f3763989d589
merged
```--- a/src/HOL/Algebra/Bij.thy	Sat Jul 28 07:28:18 2018 +0200
+++ b/src/HOL/Algebra/Bij.thy	Sat Jul 28 16:06:51 2018 +0100
@@ -46,15 +46,11 @@

theorem group_BijGroup: "group (BijGroup S)"
-apply (rule groupI)
-  apply (blast intro: compose_assoc [symmetric] dest: Bij_imp_funcset)
- apply (simp add: id_Bij Bij_imp_funcset Bij_imp_extensional, simp)
-apply (blast intro: Bij_compose_restrict_eq restrict_inv_into_Bij)
-done
+  apply (rule groupI)
+      apply (auto simp: compose_Bij id_Bij Bij_imp_funcset Bij_imp_extensional compose_assoc [symmetric])
+  apply (blast intro: Bij_compose_restrict_eq restrict_inv_into_Bij)
+  done

subsection\<open>Automorphisms Form a Group\<close>
@@ -63,13 +59,18 @@
by (simp add: Bij_def bij_betw_def inv_into_into)

lemma Bij_inv_into_lemma:
- assumes eq: "\<And>x y. \<lbrakk>x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> h(g x y) = g (h x) (h y)"
- shows "\<lbrakk>h \<in> Bij S;  g \<in> S \<rightarrow> S \<rightarrow> S;  x \<in> S;  y \<in> S\<rbrakk>
-        \<Longrightarrow> inv_into S h (g x y) = g (inv_into S h x) (inv_into S h y)"
-apply (subgoal_tac "\<exists>x'\<in>S. \<exists>y'\<in>S. x = h x' \<and> y = h y'", clarify)
- apply (simp add: eq [symmetric] inv_f_f funcset_mem [THEN funcset_mem], blast)
-done
+  assumes eq: "\<And>x y. \<lbrakk>x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> h(g x y) = g (h x) (h y)"
+      and hg: "h \<in> Bij S" "g \<in> S \<rightarrow> S \<rightarrow> S" and "x \<in> S" "y \<in> S"
+  shows "inv_into S h (g x y) = g (inv_into S h x) (inv_into S h y)"
+proof -
+  have "h ` S = S"
+    by (metis (no_types) Bij_def Int_iff assms(2) bij_betw_def mem_Collect_eq)
+  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'"
+    by auto
+  then show ?thesis
+    using assms
+    by (auto simp add: Bij_def bij_betw_def eq [symmetric] inv_f_f funcset_mem [THEN funcset_mem])
+qed

definition
@@ -94,8 +95,7 @@

lemma inv_BijGroup:
"f \<in> Bij S \<Longrightarrow> m_inv (BijGroup S) f = (\<lambda>x \<in> S. (inv_into S f) x)"
-apply (rule group.inv_equality)
-apply (rule group_BijGroup)
+apply (rule group.inv_equality [OF group_BijGroup])
done
```
```--- a/src/HOL/Algebra/Coset.thy	Sat Jul 28 07:28:18 2018 +0200
+++ b/src/HOL/Algebra/Coset.thy	Sat Jul 28 16:06:51 2018 +0100
@@ -440,45 +440,36 @@
shows "N \<lhd> G"
using assms normal_inv_iff by blast

-corollary (in group) normal_invE:
-  assumes "N \<lhd> G"
-  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"
-  using assms normal_inv_iff apply blast
-  by (simp add: assms normal.inv_op_closed2)
-
-
-lemma (in group) one_is_normal :
-   "{\<one>} \<lhd> G"
-proof(intro normal_invI )
+lemma (in group) one_is_normal: "{\<one>} \<lhd> G"
+proof(intro normal_invI)
show "subgroup {\<one>} G"
-  show "\<And>x h. x \<in> carrier G \<Longrightarrow> h \<in> {\<one>} \<Longrightarrow> x \<otimes> h \<otimes> inv x \<in> {\<one>}" by simp
-qed
+qed simp

subsection\<open>More Properties of Left Cosets\<close>

lemma (in group) l_repr_independence:
-  assumes "y \<in> x <# H" "x \<in> carrier G" "subgroup H G"
+  assumes "y \<in> x <# H" "x \<in> carrier G" and HG: "subgroup H G"
shows "x <# H = y <# H"
proof -
obtain h' where h': "h' \<in> H" "y = x \<otimes> h'"
using assms(1) unfolding l_coset_def by blast
hence "x \<otimes> h = y \<otimes> ((inv h') \<otimes> h)" if "h \<in> H" for h
proof -
-    have f3: "h' \<in> carrier G"
-      by (meson assms(3) h'(1) subgroup.mem_carrier)
-    have f4: "h \<in> carrier G"
-      by (meson assms(3) subgroup.mem_carrier that)
-    then show ?thesis
-      by (metis assms(2) f3 h'(2) inv_closed inv_solve_right m_assoc m_closed)
+    have "h' \<in> carrier G"
+      by (meson HG h'(1) subgroup.mem_carrier)
+    moreover have "h \<in> carrier G"
+      by (meson HG subgroup.mem_carrier that)
+    ultimately show ?thesis
+      by (metis assms(2) h'(2) inv_closed inv_solve_right m_assoc m_closed)
qed
-  hence "\<And> xh. xh \<in> x <# H \<Longrightarrow> xh \<in> y <# H"
-    unfolding l_coset_def by (metis (no_types, lifting) UN_iff assms(3) h'(1) subgroup_def)
-  moreover have "\<And> h. h \<in> H \<Longrightarrow> y \<otimes> h = x \<otimes> (h' \<otimes> h)"
-    using h' by (meson assms(2) assms(3) m_assoc subgroup.mem_carrier)
-  hence "\<And> yh. yh \<in> y <# H \<Longrightarrow> yh \<in> x <# H"
-    unfolding l_coset_def using subgroup.m_closed[OF assms(3) h'(1)] by blast
+  hence "\<And>xh. xh \<in> x <# H \<Longrightarrow> xh \<in> y <# H"
+    unfolding l_coset_def by (metis (no_types, lifting) UN_iff HG h'(1) subgroup_def)
+  moreover have "\<And>h. h \<in> H \<Longrightarrow> y \<otimes> h = x \<otimes> (h' \<otimes> h)"
+    using h' by (meson assms(2) HG m_assoc subgroup.mem_carrier)
+  hence "\<And>yh. yh \<in> y <# H \<Longrightarrow> yh \<in> x <# H"
+    unfolding l_coset_def using subgroup.m_closed[OF HG h'(1)] by blast
ultimately show ?thesis by blast
qed

@@ -655,8 +646,8 @@
shows "hb \<otimes> a \<in> (\<Union>h\<in>H. {h \<otimes> b})"
proof -
interpret subgroup H G by fact
-  from p show ?thesis apply (rule_tac UN_I [of "hb \<otimes> ((inv ha) \<otimes> h)"])
-    apply blast by (simp add: inv_solve_left m_assoc)
+  from p show ?thesis
+    by (rule_tac UN_I [of "hb \<otimes> ((inv ha) \<otimes> h)"]) (auto simp: inv_solve_left m_assoc)
qed

lemma (in group) rcos_disjoint:
@@ -666,9 +657,8 @@
proof -
interpret subgroup H G by fact
from p show ?thesis
-    apply (simp add: RCOSETS_def r_coset_def)
-    apply (blast intro: rcos_equation assms sym)
-    done
+    unfolding RCOSETS_def r_coset_def
+    by (blast intro: rcos_equation assms sym)
qed

@@ -761,26 +751,26 @@
proof -
interpret subgroup H G by fact
show ?thesis
-    apply (rule equalityI)
-    apply (force simp add: RCOSETS_def r_coset_def)
-    apply (auto simp add: RCOSETS_def intro: rcos_self assms)
-    done
+    unfolding RCOSETS_def r_coset_def by auto
qed

lemma (in group) cosets_finite:
"\<lbrakk>c \<in> rcosets H;  H \<subseteq> carrier G;  finite (carrier G)\<rbrakk> \<Longrightarrow> finite c"
-apply (simp add: r_coset_subset_G [THEN finite_subset])
-done
+  unfolding RCOSETS_def
+  by (auto simp add: r_coset_subset_G [THEN finite_subset])

text\<open>The next two lemmas support the proof of \<open>card_cosets_equal\<close>.\<close>
lemma (in group) inj_on_f:
-    "\<lbrakk>H \<subseteq> carrier G;  a \<in> carrier G\<rbrakk> \<Longrightarrow> inj_on (\<lambda>y. y \<otimes> inv a) (H #> a)"
-apply (rule inj_onI)
-apply (subgoal_tac "x \<in> carrier G \<and> y \<in> carrier G")
- prefer 2 apply (blast intro: r_coset_subset_G [THEN subsetD])
-done
+  assumes "H \<subseteq> carrier G" and a: "a \<in> carrier G"
+  shows "inj_on (\<lambda>y. y \<otimes> inv a) (H #> a)"
+proof
+  fix x y
+  assume "x \<in> H #> a" "y \<in> H #> a" and xy: "x \<otimes> inv a = y \<otimes> inv a"
+  then have "x \<in> carrier G" "y \<in> carrier G"
+    using assms r_coset_subset_G by blast+
+  with xy a show "x = y"
+    by auto
+qed

lemma (in group) inj_on_g:
"\<lbrakk>H \<subseteq> carrier G;  a \<in> carrier G\<rbrakk> \<Longrightarrow> inj_on (\<lambda>y. y \<otimes> a) H"
@@ -827,16 +817,17 @@
using rcosets_part_G by auto

proposition (in group) lagrange_finite:
-     "\<lbrakk>finite(carrier G); subgroup H G\<rbrakk>
-      \<Longrightarrow> card(rcosets H) * card(H) = order(G)"
-apply (simp (no_asm_simp) add: order_def rcosets_part_G [symmetric])
-apply (subst mult.commute)
-apply (rule card_partition)
-   apply (simp add: rcosets_subset_PowG [THEN finite_subset])
-  apply (simp add: card_rcosets_equal subgroup.subset)
-done
+  assumes "finite(carrier G)" and HG: "subgroup H G"
+  shows "card(rcosets H) * card(H) = order(G)"
+proof -
+  have "card H * card (rcosets H) = card (\<Union>(rcosets H))"
+  proof (rule card_partition)
+    show "\<And>c1 c2. \<lbrakk>c1 \<in> rcosets H; c2 \<in> rcosets H; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}"
+      using HG rcos_disjoint by auto
+  qed (auto simp: assms finite_UnionD rcosets_part_G card_rcosets_equal subgroup.subset)
+  then show ?thesis
+    by (simp add: HG mult.commute order_def rcosets_part_G)
+qed

theorem (in group) lagrange:
assumes "subgroup H G"
@@ -844,29 +835,29 @@
proof (cases "finite (carrier G)")
case True thus ?thesis using lagrange_finite assms by simp
next
-  case False note inf_G = this
+  case False
thus ?thesis
proof (cases "finite H")
-    case False thus ?thesis using inf_G  by (simp add: order_def)
+    case False thus ?thesis using \<open>infinite (carrier G)\<close>  by (simp add: order_def)
next
-    case True note finite_H = this
+    case True
have "infinite (rcosets H)"
-    proof (rule ccontr)
-      assume "\<not> infinite (rcosets H)"
+    proof
+      assume "finite (rcosets H)"
hence finite_rcos: "finite (rcosets H)" by simp
hence "card (\<Union>(rcosets H)) = (\<Sum>R\<in>(rcosets H). card R)"
-        using card_Union_disjoint[of "rcosets H"] finite_H rcos_disjoint[OF assms(1)]
+        using card_Union_disjoint[of "rcosets H"] \<open>finite H\<close> rcos_disjoint[OF assms(1)]
rcosets_finite[where ?H = H] by (simp add: assms subgroup.subset)
hence "order G = (\<Sum>R\<in>(rcosets H). card R)"
by (simp add: assms order_def rcosets_part_G)
hence "order G = (\<Sum>R\<in>(rcosets H). card H)"
using card_rcosets_equal by (simp add: assms subgroup.subset)
hence "order G = (card H) * (card (rcosets H))" by simp
-      hence "order G \<noteq> 0" using finite_rcos finite_H assms ex_in_conv
+      hence "order G \<noteq> 0" using finite_rcos \<open>finite H\<close> assms ex_in_conv
rcosets_part_G subgroup.one_closed by fastforce
-      thus False using inf_G order_gt_0_iff_finite by blast
+      thus False using \<open>infinite (carrier G)\<close> order_gt_0_iff_finite by blast
qed
-    thus ?thesis using inf_G by (simp add: order_def)
+    thus ?thesis using \<open>infinite (carrier G)\<close> by (simp add: order_def)
qed
qed

@@ -908,8 +899,8 @@

theorem (in normal) factorgroup_is_group:
"group (G Mod H)"
-apply (rule groupI)
+  unfolding FactGroup_def
+  apply (rule groupI)
apply (simp add: normal_imp_subgroup subgroup_in_rcosets [OF is_group])
apply (simp add: restrictI setmult_closed rcosets_assoc)
@@ -922,10 +913,20 @@

lemma (in normal) inv_FactGroup:
-     "X \<in> carrier (G Mod H) \<Longrightarrow> inv\<^bsub>G Mod H\<^esub> X = set_inv X"
-apply (rule group.inv_equality [OF factorgroup_is_group])
-apply (simp_all add: FactGroup_def setinv_closed rcosets_inv_mult_group_eq)
-done
+  assumes "X \<in> carrier (G Mod H)"
+  shows "inv\<^bsub>G Mod H\<^esub> X = set_inv X"
+proof -
+  have X: "X \<in> rcosets H"
+    using assms by (simp add: FactGroup_def)
+  moreover have "set_inv X <#> X = H"
+    using X by (simp add: normal.rcosets_inv_mult_group_eq normal_axioms)
+  moreover have "Group.group (G Mod H)"
+    using normal.factorgroup_is_group normal_axioms by blast
+  moreover have "set_inv X \<in> rcosets H"
+    by (simp add: \<open>X \<in> rcosets H\<close> setinv_closed)
+  ultimately show ?thesis
+    by (simp add: FactGroup_def group.inv_equality)
+qed

text\<open>The coset map is a homomorphism from @{term G} to the quotient group
@{term "G Mod H"}\<close>
@@ -945,15 +946,13 @@
where "kernel G H h = {x. x \<in> carrier G \<and> h x = \<one>\<^bsub>H\<^esub>}"

lemma (in group_hom) subgroup_kernel: "subgroup (kernel G H h) G"
-apply (rule subgroup.intro)
-apply (auto simp add: kernel_def group.intro is_group)
-done
+  by (auto simp add: kernel_def group.intro is_group intro: subgroup.intro)

text\<open>The kernel of a homomorphism is a normal subgroup\<close>
lemma (in group_hom) normal_kernel: "(kernel G H h) \<lhd> G"
-done
+  apply (simp only: G.normal_inv_iff subgroup_kernel)
+  done

lemma (in group_hom) FactGroup_nonempty:
assumes X: "X \<in> carrier (G Mod kernel G H h)"
@@ -982,37 +981,40 @@

lemma (in group_hom) FactGroup_hom:
"(\<lambda>X. the_elem (h`X)) \<in> hom (G Mod (kernel G H h)) H"
-apply (simp add: hom_def FactGroup_the_elem_mem normal.factorgroup_is_group [OF normal_kernel] group.axioms monoid.m_closed)
-proof (intro ballI)
-  fix X and X'
-  assume X:  "X  \<in> carrier (G Mod kernel G H h)"
-     and X': "X' \<in> carrier (G Mod kernel G H h)"
-  then
-  obtain g and g'
-           where "g \<in> carrier G" and "g' \<in> carrier G"
-             and "X = kernel G H h #> g" and "X' = kernel G H h #> g'"
-    by (auto simp add: FactGroup_def RCOSETS_def)
-  hence all: "\<forall>x\<in>X. h x = h g" "\<forall>x\<in>X'. h x = h g'"
-    and Xsub: "X \<subseteq> carrier G" and X'sub: "X' \<subseteq> carrier G"
-    by (force simp add: kernel_def r_coset_def image_def)+
-  hence "h ` (X <#> X') = {h g \<otimes>\<^bsub>H\<^esub> h g'}" using X X'
-    by (auto dest!: FactGroup_nonempty intro!: image_eqI
-                       subsetD [OF Xsub] subsetD [OF X'sub])
-  then show "the_elem (h ` (X <#> X')) = the_elem (h ` X) \<otimes>\<^bsub>H\<^esub> the_elem (h ` X')"
-    by (auto simp add: all FactGroup_nonempty X X' the_elem_image_unique)
+proof -
+  have "the_elem (h ` (X <#> X')) = the_elem (h ` X) \<otimes>\<^bsub>H\<^esub> the_elem (h ` X')"
+    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'
+  proof -
+    obtain g and g'
+      where "g \<in> carrier G" and "g' \<in> carrier G"
+        and "X = kernel G H h #> g" and "X' = kernel G H h #> g'"
+      using X X' by (auto simp add: FactGroup_def RCOSETS_def)
+    hence all: "\<forall>x\<in>X. h x = h g" "\<forall>x\<in>X'. h x = h g'"
+      and Xsub: "X \<subseteq> carrier G" and X'sub: "X' \<subseteq> carrier G"
+      by (force simp add: kernel_def r_coset_def image_def)+
+    hence "h ` (X <#> X') = {h g \<otimes>\<^bsub>H\<^esub> h g'}" using X X'
+      by (auto dest!: FactGroup_nonempty intro!: image_eqI
+          subsetD [OF Xsub] subsetD [OF X'sub])
+    then show "the_elem (h ` (X <#> X')) = the_elem (h ` X) \<otimes>\<^bsub>H\<^esub> the_elem (h ` X')"
+      by (auto simp add: all FactGroup_nonempty X X' the_elem_image_unique)
+  qed
+  then show ?thesis
+    by (simp add: hom_def FactGroup_the_elem_mem normal.factorgroup_is_group [OF normal_kernel] group.axioms monoid.m_closed)
qed

text\<open>Lemma for the following injectivity result\<close>
lemma (in group_hom) FactGroup_subset:
-     "\<lbrakk>g \<in> carrier G; g' \<in> carrier G; h g = h g'\<rbrakk>
-      \<Longrightarrow>  kernel G H h #> g \<subseteq> kernel G H h #> g'"
-apply (clarsimp simp add: kernel_def r_coset_def)
-apply (rename_tac y)
-apply (rule_tac x="y \<otimes> g \<otimes> inv g'" in exI)
-done
+  assumes "g \<in> carrier G" "g' \<in> carrier G" "h g = h g'"
+  shows "kernel G H h #> g \<subseteq> kernel G H h #> g'"
+  unfolding kernel_def r_coset_def
+proof clarsimp
+  fix y
+  assume "y \<in> carrier G" "h y = \<one>\<^bsub>H\<^esub>"
+  with assms show "\<exists>x. x \<in> carrier G \<and> h x = \<one>\<^bsub>H\<^esub> \<and> y \<otimes> g = x \<otimes> g'"
+    by (rule_tac x="y \<otimes> g \<otimes> inv g'" in exI) (auto simp: G.m_assoc)
+qed

lemma (in group_hom) FactGroup_inj_on:
"inj_on (\<lambda>X. the_elem (h ` X)) (carrier (G Mod kernel G H h))"
@@ -1113,13 +1115,13 @@
from hHN obtain h1 h2 where h1h2 : "h1 \<in> H" "h2 \<in> N" "h = (h1,h2)"
unfolding DirProd_def by fastforce
hence h1h2GK : "h1 \<in> carrier G" "h2 \<in> carrier K"
-      using normal_imp_subgroup subgroup.subset assms apply blast+.
+      using normal_imp_subgroup subgroup.subset assms by blast+
have "inv\<^bsub>G \<times>\<times> K\<^esub> x = (inv\<^bsub>G\<^esub> x1,inv\<^bsub>K\<^esub> x2)"
using inv_DirProd[OF group_axioms assms(1) x1x2(1)x1x2(2)] x1x2 by auto
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)"
using h1h2 x1x2 h1h2GK by auto
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"
-      using normal_invE group.normal_invE[OF assms(1)] assms x1x2 h1h2 apply auto.
+      using assms x1x2 h1h2 assms by (simp_all add: normal.inv_op_closed2)
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
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
qed
@@ -1133,7 +1135,7 @@

proof-
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)"
-    unfolding r_coset_def Sigma_def DirProd_def FactGroup_def RCOSETS_def apply simp by blast
+    unfolding r_coset_def Sigma_def DirProd_def FactGroup_def RCOSETS_def by force
moreover have "(\<forall>x\<in>carrier (G Mod H). \<forall>y\<in>carrier (K Mod N). \<forall>xa\<in>carrier (G Mod H).
\<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)"
unfolding set_mult_def by force
@@ -1143,8 +1145,14 @@
by (metis assms(2) assms(3) normal_def partial_object.select_convs(1))
moreover have "(\<lambda>(X, Y). X \<times> Y) ` (carrier (G Mod H) \<times> carrier (K Mod N)) =
carrier (G \<times>\<times> K Mod H \<times> N)"
-    unfolding image_def  apply auto using R apply force
-    unfolding DirProd_def FactGroup_def RCOSETS_def r_coset_def by force
+  proof -
+    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)"
+      using R by force
+    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"
+      unfolding DirProd_def FactGroup_def RCOSETS_def r_coset_def by force
+    show ?thesis
+      unfolding image_def by (auto simp: intro: 1 2)
+  qed
ultimately show ?thesis
unfolding iso_def hom_def bij_betw_def inj_on_def by simp
qed
@@ -1262,7 +1270,7 @@
have hH:"h\<in>carrier(GH)"
using hHK HK_def GH_def by auto
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)"
-        using assms normal_invE GH_def normal.inv_op_closed2 by fastforce
+        using assms GH_def normal.inv_op_closed2 by fastforce
hence INCL_1 : "x \<otimes>\<^bsub>GH\<^esub> h \<otimes>\<^bsub>GH\<^esub> inv\<^bsub>GH\<^esub> x \<in> H1"
using  xH H1K_def p2 by blast
have " x \<otimes>\<^bsub>GH\<^esub> h \<otimes>\<^bsub>GH\<^esub> inv\<^bsub>GH\<^esub> x \<in> HK"
@@ -1275,7 +1283,6 @@
qed
qed

-
lemma (in group) normal_inter_subgroup:
assumes "subgroup H G"
and "N \<lhd> G"
@@ -1288,8 +1295,8 @@
ultimately have "N \<inter> H \<lhd> G\<lparr>carrier := K \<inter> H\<rparr>"
using normal_inter[of K H N] assms(1) by blast
moreover have "K \<inter> H = H" using K_def assms subgroup.subset by blast
-  ultimately show "normal (N\<inter>H) (G\<lparr>carrier := H\<rparr>)" by auto
+  ultimately show "normal (N\<inter>H) (G\<lparr>carrier := H\<rparr>)"
+ by auto
qed

-
end```
```--- a/src/HOL/Algebra/Embedded_Algebras.thy	Sat Jul 28 07:28:18 2018 +0200
+++ b/src/HOL/Algebra/Embedded_Algebras.thy	Sat Jul 28 16:06:51 2018 +0100
@@ -187,7 +187,7 @@

"set Us \<subseteq> carrier R \<Longrightarrow> subgroup (Span K Us) (add_monoid R)"
+  using line_extension_is_subgroup normal_imp_subgroup[OF add.one_is_normal] by (induct Us) (auto)

lemma line_extension_smult_closed:
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"
@@ -246,7 +246,7 @@

lemma line_extension_of_combine_set:
assumes "u \<in> carrier R"
-  shows "line_extension K u { combine Ks Us | Ks. set Ks \<subseteq> K } =
+  shows "line_extension K u { combine Ks Us | Ks. set Ks \<subseteq> K } =
{ combine Ks (u # Us) | Ks. set Ks \<subseteq> K }"
(is "?line_extension = ?combinations")
proof
@@ -292,7 +292,7 @@

lemma line_extension_of_combine_set_length_version:
assumes "u \<in> carrier R"
-  shows "line_extension K u { combine Ks Us | Ks. length Ks = length Us \<and> set Ks \<subseteq> K } =
+  shows "line_extension K u { combine Ks Us | Ks. length Ks = length Us \<and> set Ks \<subseteq> K } =
{ combine Ks (u # Us) | Ks. length Ks = length (u # Us) \<and> set Ks \<subseteq> K }"
(is "?line_extension = ?combinations")
proof
@@ -329,16 +329,16 @@
assumes "set Us \<subseteq> carrier R" and "a \<in> carrier R"
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>)"
(is "?in_Span \<longleftrightarrow> ?exists_combine")
-proof
+proof
assume "?in_Span"
then obtain Ks where Ks: "set Ks \<subseteq> K" "a = combine Ks Us"
using Span_eq_combine_set[OF assms(1)] by auto
hence "((\<ominus> \<one>) \<otimes> a) \<oplus> a = combine ((\<ominus> \<one>) # Ks) (a # Us)"
by auto
moreover have "((\<ominus> \<one>) \<otimes> a) \<oplus> a = \<zero>"
-    using assms(2) l_minus l_neg by auto
+    using assms(2) l_minus l_neg by auto
moreover have "\<ominus> \<one> \<noteq> \<zero>"
-    using subfieldE(6)[OF K] l_neg by force
+    using subfieldE(6)[OF K] l_neg by force
ultimately show "?exists_combine"
using subring_props(3,5) Ks(1) by (force simp del: combine.simps)
next
@@ -391,14 +391,14 @@
proof (induct Ks Us rule: combine.induct)
case (1 k Ks u Us)
hence "k \<in> K" and "u \<in> set (u # Us)" by auto
-      hence "k \<otimes> u \<in> E"
+      hence "k \<otimes> u \<in> E"
using 1(4) unfolding set_mult_def by auto
moreover have "K <#> set Us \<subseteq> E"
using 1(4) unfolding set_mult_def by auto
hence "combine Ks Us \<in> E"
using 1 by auto
ultimately show ?case
-        using add.subgroupE(4)[OF assms(2)] by auto
+        using add.subgroupE(4)[OF assms(2)] by auto
next
case "2_1" thus ?case
using subgroup.one_closed[OF assms(2)] by auto
@@ -436,7 +436,7 @@
hence "combine [ k ] (u # Us) \<in> Span K (u # Us)"
using Span_eq_combine_set[OF Cons(2)] by (auto simp del: combine.simps)
moreover have "k \<in> carrier R" and "u \<in> carrier R"
-        using Cons(2) k subring_props(1) by (blast, auto)
+        using Cons(2) k subring_props(1) by (blast, auto)
ultimately show "k \<otimes> u \<in> Span K (u # Us)"
by (auto simp del: Span.simps)
qed
@@ -455,7 +455,7 @@
corollary Span_same_set:
assumes "set Us \<subseteq> carrier R"
shows "set Us = set Vs \<Longrightarrow> Span K Us = Span K Vs"
-  using Span_eq_generate assms by auto
+  using Span_eq_generate assms by auto

corollary Span_incl: "set Us \<subseteq> carrier R \<Longrightarrow> K <#> (set Us) \<subseteq> Span K Us"
using Span_eq_generate generate.incl[of _ _ "add_monoid R"] by auto
@@ -583,7 +583,7 @@
moreover have "Span K Us \<subseteq> Span K (u # Us)"
using mono_Span independent_in_carrier[OF assms] by auto
ultimately show ?thesis
-    using independent_backwards(1)[OF assms] by auto
+    using independent_backwards(1)[OF assms] by auto
qed

corollary independent_replacement:
@@ -624,7 +624,7 @@
from assms show "Span K Us \<inter> Span K Vs = { \<zero> }"
proof (induct Us rule: list.induct)
case Nil thus ?case
-      using Span_subgroup_props(2)[OF independent_in_carrier[of K Vs]] by simp
+      using Span_subgroup_props(2)[OF independent_in_carrier[of K Vs]] by simp
next
case (Cons u Us)
hence IH: "Span K Us \<inter> Span K Vs = {\<zero>}" by auto
@@ -653,7 +653,7 @@
hence "k \<otimes> u = (\<ominus> u') \<oplus> v'"
using in_carrier(1) k(2) u'(2) v'(2) add.m_comm r_neg1 by auto
hence "k \<otimes> u \<in> Span K (Us @ Vs)"
-        using Span_subgroup_props(4)[OF in_carrier(2) u'(1)] v'(1)
+        using Span_subgroup_props(4)[OF in_carrier(2) u'(1)] v'(1)
hence "u \<in> Span K (Us @ Vs)"
using Cons(2) Span_m_inv_simprule[OF _ _ in_carrier(1), of "Us @ Vs" k]
@@ -678,7 +678,7 @@
hence in_carrier:
"u \<in> carrier R" "set Us \<subseteq> carrier R" "set Vs \<subseteq> carrier R" "set (u # Us) \<subseteq> carrier R"
using Cons(2-3)[THEN independent_in_carrier] by auto
-  hence "Span K Us \<subseteq> Span K (u # Us)"
+  hence "Span K Us \<subseteq> Span K (u # Us)"
using mono_Span by auto
hence "Span K Us \<inter> Span K Vs = { \<zero> }"
using Cons(4) Span_subgroup_props(2)[OF in_carrier(2)] by auto
@@ -733,7 +733,7 @@
hence "combine Ks' Us = \<zero>"
using combine_in_carrier[OF _ Us, of Ks'] Ks' u Cons(3) subring_props(1) unfolding Ks by auto
hence "set (take (length Us) Ks') \<subseteq> { \<zero> }"
-      using Cons(1)[OF Ks' _ independent_backwards(2)[OF Cons(4)]] by simp
+      using Cons(1)[OF Ks' _ independent_backwards(2)[OF Cons(4)]] by simp
thus ?thesis
using k_zero unfolding Ks by auto
qed
@@ -878,10 +878,10 @@
case (Cons u Us)
then obtain Vs' Vs'' where Vs: "Vs = Vs' @ (u # Vs'')"
by (metis list.set_intros(1) split_list)
-
+
have in_carrier: "u \<in> carrier R" "set Us \<subseteq> carrier R"
-      using independent_in_carrier[OF Cons(2)] by auto
-
+      using independent_in_carrier[OF Cons(2)] by auto
+
have "distinct Vs"
using Cons(3-4) independent_distinct[OF Cons(2)]
by (metis card_distinct distinct_card)
@@ -905,7 +905,7 @@
shows "\<exists>Vs'. set Vs' \<subseteq> set Vs \<and> length Vs' = length Us' \<and> independent K (Vs' @ Us)"
using assms
proof (induct "length Us'" arbitrary: Us' Us)
-  case 0 thus ?case by auto
+  case 0 thus ?case by auto
next
case (Suc n)
then obtain u Us'' where Us'': "Us' = Us'' @ [u]"
@@ -1074,9 +1074,9 @@
using space_subgroup_props(1)[OF assms(1)] li_Cons[OF _ v(2) step(4)] by auto
then obtain Vs
where "length (Vs @ (v # Us)) = n" "independent K (Vs @ (v # Us))" "Span K (Vs @ (v # Us)) = E"
-        using step(3)[of "v # Us"] step(1-2,4-6) v by auto
+        using step(3)[of "v # Us"] step(1-2,4-6) v by auto
thus ?case
-        by (metis append.assoc append_Cons append_Nil)
+        by (metis append.assoc append_Cons append_Nil)
qed } note aux_lemma = this

have "length Us \<le> n"
@@ -1119,7 +1119,7 @@
hence in_carrier: "set Us \<subseteq> carrier R" "set (Vs @ Bs) \<subseteq> carrier R"
using independent_in_carrier[OF Us(2)] independent_in_carrier[OF Vs(2)] by auto
hence "Span K Us \<inter> (Span K (Vs @ Bs)) \<subseteq> Span K Bs"
-    using Bs(4) Us(3) Vs(3) mono_Span_append(1)[OF _ Bs(1), of Us] by auto
+    using Bs(4) Us(3) Vs(3) mono_Span_append(1)[OF _ Bs(1), of Us] by auto
hence "Span K Us \<inter> (Span K (Vs @ Bs)) \<subseteq> { \<zero> }"
using independent_split(3)[OF Us(2)] by blast
hence "Span K Us \<inter> (Span K (Vs @ Bs)) = { \<zero> }"
@@ -1147,7 +1147,7 @@
ultimately show "v \<in> (Span K Us) <+>\<^bsub>R\<^esub> F"
using u1' unfolding set_add_def' by auto
qed
-  ultimately have "Span K (Us @ (Vs @ Bs)) = E <+>\<^bsub>R\<^esub> F"
+  ultimately have "Span K (Us @ (Vs @ Bs)) = E <+>\<^bsub>R\<^esub> F"
using Span_append_eq_set_add[OF in_carrier] Vs(3) by auto

thus ?thesis using dim by simp
@@ -1169,7 +1169,7 @@
by (metis One_nat_def length_0_conv length_Suc_conv)
have in_carrier: "set (map (\<lambda>u'. u' \<otimes> u) Us) \<subseteq> carrier R"
using Us(1) u(1) by (induct Us) (auto)
-
+
have li: "independent K (map (\<lambda>u'. u' \<otimes> u) Us)"
proof (rule trivial_combine_imp_independent[OF assms(1) in_carrier])
fix Ks assume Ks: "set Ks \<subseteq> K" and "combine Ks (map (\<lambda>u'. u' \<otimes> u) Us) = \<zero>"
@@ -1244,7 +1244,7 @@
ultimately have "dimension (n * Suc m) K (Span F [ v ] <+>\<^bsub>R\<^esub> Span F Vs')"
using dimension_direct_sum_space[OF assms(1) _ _ inter] by auto
thus "dimension (n * Suc m) K E"
-    using Span_append_eq_set_add[OF assms(2) li[THEN independent_in_carrier]] Vs(4) v by auto
+    using Span_append_eq_set_add[OF assms(2) li[THEN independent_in_carrier]] Vs(4) v by auto
qed

@@ -1271,14 +1271,14 @@
hence "combine Ks Us = (combine (take (length Us) Ks) Us) \<oplus> \<zero>"
using combine_append[OF _ _ assms(2), of "take (length Us) Ks" "drop (length Us) Ks" "[]"] len by auto
also have " ... = combine (take (length Us) Ks) Us"
-    using combine_in_carrier[OF set_t assms(2)] by auto
+    using combine_in_carrier[OF set_t assms(2)] by auto
finally show "combine Ks Us = combine (take (length Us) Ks) Us" .
qed
*)

(*
lemma combine_normalize:
-  assumes "set Ks \<subseteq> K" "set Us \<subseteq> carrier R" "a = combine Ks Us"
+  assumes "set Ks \<subseteq> K" "set Us \<subseteq> carrier R" "a = combine Ks Us"
shows "\<exists>Ks'. set Ks' \<subseteq> K \<and> length Ks' = length Us \<and> a = combine Ks' Us"
proof (cases "length Ks \<le> length Us")
assume "\<not> length Ks \<le> length Us"
@@ -1291,12 +1291,12 @@
next
assume len: "length Ks \<le> length Us"
have Ks: "set Ks \<subseteq> carrier R" and set_r: "set (replicate (length Us - length Ks) \<zero>) \<subseteq> carrier R"
-    using assms subring_props(1) zero_closed by (metis dual_order.trans, auto)
+    using assms subring_props(1) zero_closed by (metis dual_order.trans, auto)
moreover
have set_t: "set (take (length Ks) Us) \<subseteq> carrier R"
and set_d: "set (drop (length Ks) Us) \<subseteq> carrier R"
using assms(2) len dual_order.trans by (metis set_take_subset, metis set_drop_subset)
-  ultimately
+  ultimately
have "combine (Ks @ (replicate (length Us - length Ks) \<zero>)) Us =
(combine Ks (take (length Ks) Us)) \<oplus>
(combine (replicate (length Us - length Ks) \<zero>) (drop (length Ks) Us))"```
```--- a/src/HOL/Algebra/Generated_Groups.thy	Sat Jul 28 07:28:18 2018 +0200
+++ b/src/HOL/Algebra/Generated_Groups.thy	Sat Jul 28 16:06:51 2018 +0100
@@ -466,7 +466,7 @@
shows "derived G H \<lhd> G" unfolding derived_def
proof (rule normal_generateI)
show "(\<Union>h1 \<in> H. \<Union>h2 \<in> H. { h1 \<otimes> h2 \<otimes> inv h1 \<otimes> inv h2 }) \<subseteq> carrier G"
-    using subgroup.subset assms normal_invE(1) by blast
+    using subgroup.subset assms normal_imp_subgroup by blast
next
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"
proof -
@@ -474,7 +474,7 @@
then obtain h1 h2 where h1: "h1 \<in> H" "h1 \<in> carrier G"
and h2: "h2 \<in> H" "h2 \<in> carrier G"
and h:  "h = h1 \<otimes> h2 \<otimes> inv h1 \<otimes> inv h2"
-      using subgroup.subset assms normal_invE(1) by blast
+      using subgroup.subset assms normal_imp_subgroup by blast
hence "g \<otimes> h \<otimes> inv g =
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"
@@ -486,8 +486,8 @@
have "g \<otimes> h \<otimes> inv g =
(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)"
by (simp add: g h1 h2 inv_mult_group m_assoc)
-    moreover have "g \<otimes> h1 \<otimes> inv g \<in> H" by (simp add: assms normal_invE(2) g h1)
-    moreover have "g \<otimes> h2 \<otimes> inv g \<in> H" by (simp add: assms normal_invE(2) g h2)
+    moreover have "g \<otimes> h1 \<otimes> inv g \<in> H" by (simp add: assms normal.inv_op_closed2 g h1)
+    moreover have "g \<otimes> h2 \<otimes> inv g \<in> H" by (simp add: assms normal.inv_op_closed2 g h2)
ultimately show "g \<otimes> h \<otimes> inv g \<in> derived_set G H" by blast
qed
qed```
```--- a/src/HOL/Algebra/Group.thy	Sat Jul 28 07:28:18 2018 +0200
+++ b/src/HOL/Algebra/Group.thy	Sat Jul 28 16:06:51 2018 +0100
@@ -763,13 +763,13 @@
and "subgroup I K"
shows "subgroup (H \<times> I) (G \<times>\<times> K)"
proof (intro group.group_incl_imp_subgroup[OF DirProd_group[OF assms(1)assms(3)]])
-  have "H \<subseteq> carrier G" "I \<subseteq> carrier K" using subgroup.subset assms apply blast+.
+  have "H \<subseteq> carrier G" "I \<subseteq> carrier K" using subgroup.subset assms by blast+
thus "(H \<times> I) \<subseteq> carrier (G \<times>\<times> K)" unfolding DirProd_def by auto
have "Group.group ((G\<lparr>carrier := H\<rparr>) \<times>\<times> (K\<lparr>carrier := I\<rparr>))"
using DirProd_group[OF subgroup.subgroup_is_group[OF assms(2)assms(1)]
subgroup.subgroup_is_group[OF assms(4)assms(3)]].
moreover have "((G\<lparr>carrier := H\<rparr>) \<times>\<times> (K\<lparr>carrier := I\<rparr>)) = ((G \<times>\<times> K)\<lparr>carrier := H \<times> I\<rparr>)"
-    unfolding DirProd_def using assms apply simp.
+    unfolding DirProd_def using assms by simp
ultimately show "Group.group ((G \<times>\<times> K)\<lparr>carrier := H \<times> I\<rparr>)" by simp
qed

@@ -1054,7 +1054,7 @@
lemma (in group_hom) img_is_subgroup: "subgroup (h ` (carrier G)) H"
apply (rule subgroupI)
-  apply (metis (no_types, hide_lams) G.inv_closed hom_inv image_iff)
+  apply (metis G.inv_closed hom_inv image_iff)
by (metis G.monoid_axioms hom_mult image_eqI monoid.m_closed)

lemma (in group_hom) subgroup_img_is_subgroup:
@@ -1157,9 +1157,8 @@
show "monoid (G\<lparr>carrier := H\<rparr>)"
using submonoid.submonoid_is_monoid assms comm_monoid_axioms comm_monoid_def by blast
show "\<And>x y. x \<in> carrier (G\<lparr>carrier := H\<rparr>) \<Longrightarrow> y \<in> carrier (G\<lparr>carrier := H\<rparr>)
-        \<Longrightarrow> x \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> y = y \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> x" apply simp
-    using  assms comm_monoid_axioms_def submonoid.mem_carrier
-    by (metis m_comm)
+        \<Longrightarrow> x \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> y = y \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> x"
+    by simp (meson assms m_comm submonoid.mem_carrier)
qed

locale comm_group = comm_monoid + group```
```--- a/src/HOL/Algebra/Ideal.thy	Sat Jul 28 07:28:18 2018 +0200
+++ b/src/HOL/Algebra/Ideal.thy	Sat Jul 28 16:06:51 2018 +0100
@@ -128,10 +128,9 @@
proof -
interpret additive_subgroup I R by fact
interpret cring R by fact
-  show ?thesis apply intro_locales
-    apply (intro ideal_axioms.intro)
-    apply (erule (1) I_l_closed)
-    apply (erule (1) I_r_closed)
+  show ?thesis
+    apply intro_locales
+    apply (simp add: I_l_closed I_r_closed ideal_axioms_def)
by (simp add: I_notcarr I_prime primeideal_axioms.intro)
qed
```
```--- a/src/HOL/Algebra/RingHom.thy	Sat Jul 28 07:28:18 2018 +0200
+++ b/src/HOL/Algebra/RingHom.thy	Sat Jul 28 16:06:51 2018 +0100
@@ -20,11 +20,10 @@
by standard (rule homh)

sublocale ring_hom_ring \<subseteq> abelian_group?: abelian_group_hom R S
-apply (intro abelian_group_homI R.is_abelian_group S.is_abelian_group)
-apply (intro group_hom.intro group_hom_axioms.intro R.a_group S.a_group)
-apply (insert homh, unfold hom_def ring_hom_def)
-apply simp
-done
+proof
+    using homh by (simp add: hom_def ring_hom_def)
+qed

lemma (in ring_hom_ring) is_ring_hom_ring:
"ring_hom_ring R S h"
@@ -33,8 +32,7 @@
lemma ring_hom_ringI:
fixes R (structure) and S (structure)
assumes "ring R" "ring S"
-  assumes (* morphism: "h \<in> carrier R \<rightarrow> carrier S" *)
-          hom_closed: "!!x. x \<in> carrier R ==> h x \<in> carrier S"
+  assumes hom_closed: "!!x. x \<in> carrier R ==> h x \<in> carrier S"
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"
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"
and compatible_one: "h \<one> = \<one>\<^bsub>S\<^esub>"
@@ -42,13 +40,12 @@
proof -
interpret ring R by fact
interpret ring S by fact
-  show ?thesis apply unfold_locales
-apply (unfold ring_hom_def, safe)
-   apply (simp add: hom_closed Pi_def)
-  apply (erule (1) compatible_mult)
-apply (rule compatible_one)
-done
+  show ?thesis
+  proof
+    show "h \<in> ring_hom R S"
+      unfolding ring_hom_def
+      by (auto simp: compatible_mult compatible_add compatible_one hom_closed)
+  qed
qed

lemma ring_hom_ringI2:
@@ -58,11 +55,11 @@
proof -
interpret R: ring R by fact
interpret S: ring S by fact
-  show ?thesis apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro)
-    apply (rule R.is_ring)
-    apply (rule S.is_ring)
-    apply (rule h)
-    done
+  show ?thesis
+  proof
+    show "h \<in> ring_hom R S"
+      using h .
+  qed
qed

lemma ring_hom_ringI3:
@@ -75,13 +72,11 @@
interpret abelian_group_hom R S h by fact
interpret R: ring R by fact
interpret S: ring S by fact
-  show ?thesis apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro, rule R.is_ring, rule S.is_ring)
-    apply (insert group_hom.homh[OF a_group_hom])
-    apply (unfold hom_def ring_hom_def, simp)
-    apply safe
-    apply (erule (1) compatible_mult)
-    apply (rule compatible_one)
-    done
+  show ?thesis
+  proof
+    show "h \<in> ring_hom R S"
+      unfolding ring_hom_def by (auto simp: compatible_one compatible_mult)
+  qed
qed

lemma ring_hom_cringI:
@@ -91,21 +86,22 @@
interpret ring_hom_ring R S h by fact
interpret R: cring R by fact
interpret S: cring S by fact
-  show ?thesis by (intro ring_hom_cring.intro ring_hom_cring_axioms.intro)
-    (rule R.is_cring, rule S.is_cring, rule homh)
+  show ?thesis
+  proof
+    show "h \<in> ring_hom R S"
+  qed
qed

subsection \<open>The Kernel of a Ring Homomorphism\<close>

\<comment> \<open>the kernel of a ring homomorphism is an ideal\<close>
-lemma (in ring_hom_ring) kernel_is_ideal:
-  shows "ideal (a_kernel R S h) R"
-apply (rule idealI)
-   apply (rule R.is_ring)
- apply (unfold a_kernel_def', simp+)
-done
+lemma (in ring_hom_ring) kernel_is_ideal: "ideal (a_kernel R S h) R"
+  apply (rule idealI [OF R.is_ring])
+   apply (auto simp: a_kernel_def')
+  done

text \<open>Elements of the kernel are mapped to zero\<close>
lemma (in abelian_group_hom) kernel_zero [simp]:
@@ -174,29 +170,10 @@
corollary (in ring_hom_ring) rcos_eq_homeq:
assumes acarr: "a \<in> carrier R"
shows "(a_kernel R S h) +> a = {x \<in> carrier R. h x = h a}"
-  apply rule defer 1
-   apply clarsimp defer 1
-proof
+proof -
interpret ideal "a_kernel R S h" "R" by (rule kernel_is_ideal)
-
-  fix x
-  assume xrcos: "x \<in> a_kernel R S h +> a"
-  from acarr and this
-  have xcarr: "x \<in> carrier R"
-    by (rule a_elemrcos_carrier)
-
-  from xrcos
-  have "h x = h a" by (rule rcos_imp_homeq[OF acarr])
-  from xcarr and this
-  show "x \<in> {x \<in> carrier R. h x = h a}" by fast
-next
-  interpret ideal "a_kernel R S h" "R" by (rule kernel_is_ideal)
-
-  fix x
-  assume xcarr: "x \<in> carrier R"
-    and hx: "h x = h a"
-  from acarr xcarr hx
-  show "x \<in> a_kernel R S h +> a" by (rule homeq_imp_rcos)
+  show ?thesis
+    using assms by (auto simp: intro: homeq_imp_rcos rcos_imp_homeq a_elemrcos_carrier)
qed

lemma (in ring_hom_ring) nat_pow_hom:```
```--- a/src/HOL/Library/FuncSet.thy	Sat Jul 28 07:28:18 2018 +0200
+++ b/src/HOL/Library/FuncSet.thy	Sat Jul 28 16:06:51 2018 +0100
@@ -163,8 +163,6 @@

lemma compose_assoc:
assumes "f \<in> A \<rightarrow> B"
-    and "g \<in> B \<rightarrow> C"
-    and "h \<in> C \<rightarrow> D"
shows "compose A h (compose A g f) = compose A (compose B h g) f"
using assms by (simp add: fun_eq_iff Pi_def compose_def restrict_def)
```