# HG changeset patch
# User wenzelm
# Date 1532881487 -7200
# Node ID f3763989d589e0c9dee3761da938f1d45b3b295a
# Parent  5cbd9cda76262996c60d70e9224687f47b943b72# Parent  3a58abb1184019b83686a4a643371bf374b8eeb2
merged

diff -r 5cbd9cda7626 -r f3763989d589 CONTRIBUTORS
--- a/CONTRIBUTORS	Sun Jul 29 13:18:10 2018 +0200
+++ b/CONTRIBUTORS	Sun Jul 29 18:24:47 2018 +0200
@@ -3,6 +3,10 @@
 listed as an author in one of the source files of this Isabelle distribution.
 
 
+Contributions to this Isabelle version
+--------------------------------------
+
+
 Contributions to Isabelle2018
 -----------------------------
 
diff -r 5cbd9cda7626 -r f3763989d589 NEWS
--- a/NEWS	Sun Jul 29 13:18:10 2018 +0200
+++ b/NEWS	Sun Jul 29 18:24:47 2018 +0200
@@ -4,6 +4,11 @@
 (Note: Isabelle/jEdit shows a tree-view of the NEWS file in Sidekick.)
 
 
+New in this Isabelle version
+----------------------------
+
+
+
 New in Isabelle2018 (August 2018)
 ---------------------------------
 
diff -r 5cbd9cda7626 -r f3763989d589 src/HOL/Algebra/AbelCoset.thy
--- a/src/HOL/Algebra/AbelCoset.thy	Sun Jul 29 13:18:10 2018 +0200
+++ b/src/HOL/Algebra/AbelCoset.thy	Sun Jul 29 18:24:47 2018 +0200
@@ -269,17 +269,15 @@
     by (rule a_comm_group)
   interpret subgroup "H" "(add_monoid G)"
     by (rule a_subgroup)
-
-  show "abelian_subgroup H G"
-    apply unfold_locales
-  proof (simp add: r_coset_def l_coset_def, clarsimp)
-    fix x
-    assume xcarr: "x \<in> carrier G"
-    from a_subgroup have Hcarr: "H \<subseteq> carrier G"
-      unfolding subgroup_def by simp
-    from xcarr Hcarr show "(\<Union>h\<in>H. {h \<oplus>\<^bsub>G\<^esub> x}) = (\<Union>h\<in>H. {x \<oplus>\<^bsub>G\<^esub> h})"
+  have "(\<Union>xa\<in>H. {xa \<oplus> x}) = (\<Union>xa\<in>H. {x \<oplus> xa})" if "x \<in> carrier G" for x
+  proof -
+    have "H \<subseteq> carrier G"
+      using a_subgroup that unfolding subgroup_def by simp
+    with that show "(\<Union>h\<in>H. {h \<oplus>\<^bsub>G\<^esub> x}) = (\<Union>h\<in>H. {x \<oplus>\<^bsub>G\<^esub> h})"
       using m_comm [simplified] by fastforce
   qed
+  then show "abelian_subgroup H G"
+    by unfold_locales (auto simp: r_coset_def l_coset_def)
 qed
 
 lemma abelian_subgroupI3:
@@ -304,14 +302,6 @@
 by (rule normal.inv_op_closed2 [OF a_normal,
     folded a_inv_def, simplified monoid_record_simps])
 
-text\<open>Alternative characterization of normal subgroups\<close>
-lemma (in abelian_group) a_normal_inv_iff:
-     "(N \<lhd> (add_monoid G)) = 
-      (subgroup N (add_monoid G) & (\<forall>x \<in> carrier G. \<forall>h \<in> N. x \<oplus> h \<oplus> (\<ominus> x) \<in> N))"
-      (is "_ = ?rhs")
-by (rule group.normal_inv_iff [OF a_group,
-    folded a_inv_def, simplified monoid_record_simps])
-
 lemma (in abelian_group) a_lcos_m_assoc:
   "\<lbrakk> M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G \<rbrakk> \<Longrightarrow> g <+ (h <+ M) = (g \<oplus> h) <+ M"
 by (rule group.lcos_m_assoc [OF a_group,
@@ -322,13 +312,11 @@
 by (rule group.lcos_mult_one [OF a_group,
     folded a_l_coset_def, simplified monoid_record_simps])
 
-
 lemma (in abelian_group) a_l_coset_subset_G:
   "\<lbrakk> H \<subseteq> carrier G; x \<in> carrier G \<rbrakk> \<Longrightarrow> x <+ H \<subseteq> carrier G"
 by (rule group.l_coset_subset_G [OF a_group,
     folded a_l_coset_def, simplified monoid_record_simps])
 
-
 lemma (in abelian_group) a_l_coset_swap:
      "\<lbrakk>y \<in> x <+ H;  x \<in> carrier G;  subgroup H (add_monoid G)\<rbrakk> \<Longrightarrow> x \<in> y <+ H"
 by (rule group.l_coset_swap [OF a_group,
@@ -498,15 +486,15 @@
 
 text \<open>Since the Factorization is based on an \emph{abelian} subgroup, is results in 
         a commutative group\<close>
-theorem (in abelian_subgroup) a_factorgroup_is_comm_group:
-  "comm_group (G A_Mod H)"
-apply (intro comm_group.intro comm_monoid.intro) prefer 3
-  apply (rule a_factorgroup_is_group)
- apply (rule group.axioms[OF a_factorgroup_is_group])
-apply (rule comm_monoid_axioms.intro)
-apply (unfold A_FactGroup_def FactGroup_def RCOSETS_def, fold set_add_def a_r_coset_def, clarsimp)
-apply (simp add: a_rcos_sum a_comm)
-done
+theorem (in abelian_subgroup) a_factorgroup_is_comm_group: "comm_group (G A_Mod H)"
+proof -
+  have "Group.comm_monoid_axioms (G A_Mod H)"
+    apply (rule comm_monoid_axioms.intro)
+    apply (auto simp: A_FactGroup_def FactGroup_def RCOSETS_def a_normal add.m_comm normal.rcos_sum)
+    done
+  then show ?thesis
+    by (intro comm_group.intro comm_monoid.intro) (simp_all add: a_factorgroup_is_group group.is_monoid)
+qed
 
 lemma add_A_FactGroup [simp]: "X \<otimes>\<^bsub>(G A_Mod H)\<^esub> X' = X <+>\<^bsub>G\<^esub> X'"
 by (simp add: A_FactGroup_def set_add_def)
@@ -552,11 +540,8 @@
   interpret G: abelian_group G by fact
   interpret H: abelian_group H by fact
   show ?thesis
-    apply (intro abelian_group_hom.intro abelian_group_hom_axioms.intro)
-      apply fact
-     apply fact
-    apply (rule a_group_hom)
-    done
+    by (intro abelian_group_hom.intro abelian_group_hom_axioms.intro 
+        G.abelian_group_axioms H.abelian_group_axioms a_group_hom)
 qed
 
 lemma (in abelian_group_hom) is_abelian_group_hom:
@@ -576,8 +561,7 @@
 
 lemma (in abelian_group_hom) zero_closed [simp]:
   "h \<zero> \<in> carrier H"
-by (rule group_hom.one_closed[OF a_group_hom,
-    simplified ring_record_simps])
+  by simp
 
 lemma (in abelian_group_hom) hom_zero [simp]:
   "h \<zero> = \<zero>\<^bsub>H\<^esub>"
@@ -586,8 +570,7 @@
 
 lemma (in abelian_group_hom) a_inv_closed [simp]:
   "x \<in> carrier G ==> h (\<ominus>x) \<in> carrier H"
-by (rule group_hom.inv_closed[OF a_group_hom,
-    folded a_inv_def, simplified ring_record_simps])
+  by simp
 
 lemma (in abelian_group_hom) hom_a_inv [simp]:
   "x \<in> carrier G ==> h (\<ominus>x) = \<ominus>\<^bsub>H\<^esub> (h x)"
@@ -596,19 +579,15 @@
 
 lemma (in abelian_group_hom) additive_subgroup_a_kernel:
   "additive_subgroup (a_kernel G H h) G"
-apply (rule additive_subgroup.intro)
-apply (rule group_hom.subgroup_kernel[OF a_group_hom,
-       folded a_kernel_def, simplified ring_record_simps])
-done
+  by (simp add: additive_subgroup.intro a_group_hom a_kernel_def group_hom.subgroup_kernel)
 
 text\<open>The kernel of a homomorphism is an abelian subgroup\<close>
 lemma (in abelian_group_hom) abelian_subgroup_a_kernel:
   "abelian_subgroup (a_kernel G H h) G"
-apply (rule abelian_subgroupI)
-apply (rule group_hom.normal_kernel[OF a_group_hom,
-       folded a_kernel_def, simplified ring_record_simps])
-apply (simp add: G.a_comm)
-done
+  apply (rule abelian_subgroupI)
+   apply (simp add: G.abelian_group_axioms abelian_subgroup.a_normal abelian_subgroupI3 additive_subgroup_a_kernel)
+  apply (simp add: G.a_comm)
+  done
 
 lemma (in abelian_group_hom) A_FactGroup_nonempty:
   assumes X: "X \<in> carrier (G A_Mod a_kernel G H h)"
@@ -715,48 +694,34 @@
 qed
 
 lemma (in abelian_subgroup) a_repr_independence':
-  assumes y: "y \<in> H +> x"
-      and xcarr: "x \<in> carrier G"
+  assumes "y \<in> H +> x" "x \<in> carrier G"
   shows "H +> x = H +> y"
-  apply (rule a_repr_independence)
-    apply (rule y)
-   apply (rule xcarr)
-  apply (rule a_subgroup)
-  done
+  using a_repr_independence a_subgroup assms by blast
 
 lemma (in abelian_subgroup) a_repr_independenceD:
-  assumes ycarr: "y \<in> carrier G"
-      and repr:  "H +> x = H +> y"
+  assumes "y \<in> carrier G" "H +> x = H +> y"
   shows "y \<in> H +> x"
-by (rule group.repr_independenceD [OF a_group a_subgroup,
-    folded a_r_coset_def, simplified monoid_record_simps]) (rule ycarr, rule repr)
+  by (simp add: a_rcos_self assms)
 
 
 lemma (in abelian_subgroup) a_rcosets_carrier:
   "X \<in> a_rcosets H \<Longrightarrow> X \<subseteq> carrier G"
-by (rule subgroup.rcosets_carrier [OF a_subgroup a_group,
-    folded A_RCOSETS_def, simplified monoid_record_simps])
+  using a_rcosets_part_G by auto
 
 
 subsubsection \<open>Addition of Subgroups\<close>
 
 lemma (in abelian_monoid) set_add_closed:
-  assumes Acarr: "A \<subseteq> carrier G"
-      and Bcarr: "B \<subseteq> carrier G"
+  assumes "A \<subseteq> carrier G" "B \<subseteq> carrier G"
   shows "A <+> B \<subseteq> carrier G"
-by (rule monoid.set_mult_closed [OF a_monoid,
-    folded set_add_def, simplified monoid_record_simps]) (rule Acarr, rule Bcarr)
+  by (simp add: assms add.set_mult_closed set_add_defs(1))
 
 lemma (in abelian_group) add_additive_subgroups:
   assumes subH: "additive_subgroup H G"
-      and subK: "additive_subgroup K G"
+    and subK: "additive_subgroup K G"
   shows "additive_subgroup (H <+> K) G"
-apply (rule additive_subgroup.intro)
-apply (unfold set_add_def)
-apply (intro comm_group.mult_subgroups)
-  apply (rule a_comm_group)
- apply (rule additive_subgroup.a_subgroup[OF subH])
-apply (rule additive_subgroup.a_subgroup[OF subK])
-done
+  unfolding set_add_def
+  using add.mult_subgroups additive_subgroup_def subH subK
+  by (blast intro: additive_subgroup.intro)
 
 end
diff -r 5cbd9cda7626 -r f3763989d589 src/HOL/Algebra/Bij.thy
--- a/src/HOL/Algebra/Bij.thy	Sun Jul 29 13:18:10 2018 +0200
+++ b/src/HOL/Algebra/Bij.thy	Sun Jul 29 18:24:47 2018 +0200
@@ -46,15 +46,11 @@
   by (simp add: Bij_def compose_inv_into_id)
 
 theorem group_BijGroup: "group (BijGroup S)"
-apply (simp add: BijGroup_def)
-apply (rule groupI)
-    apply (simp add: compose_Bij)
-   apply (simp add: id_Bij)
-  apply (simp add: compose_Bij)
-  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 (simp add: BijGroup_def)
+  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 (simp add: Bij_def bij_betw_def)
-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])
 apply (simp_all add:BijGroup_def restrict_inv_into_Bij Bij_compose_restrict_eq)
 done
 
diff -r 5cbd9cda7626 -r f3763989d589 src/HOL/Algebra/Complete_Lattice.thy
--- a/src/HOL/Algebra/Complete_Lattice.thy	Sun Jul 29 13:18:10 2018 +0200
+++ b/src/HOL/Algebra/Complete_Lattice.thy	Sun Jul 29 18:24:47 2018 +0200
@@ -680,22 +680,25 @@
     next
       case False
       show ?thesis
-      proof (rule_tac x="\<Squnion>\<^bsub>L\<^esub> A" in exI, rule least_UpperI, simp_all)
+      proof (intro exI least_UpperI, simp_all)
         show b:"\<And> x. x \<in> A \<Longrightarrow> x \<sqsubseteq>\<^bsub>L\<^esub> \<Squnion>\<^bsub>L\<^esub>A"
           using a by (auto intro: L.sup_upper, meson L.at_least_at_most_closed L.sup_upper subset_trans)
         show "\<And>y. y \<in> Upper (L\<lparr>carrier := \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>\<rparr>) A \<Longrightarrow> \<Squnion>\<^bsub>L\<^esub>A \<sqsubseteq>\<^bsub>L\<^esub> y"
           using a L.at_least_at_most_closed by (rule_tac L.sup_least, auto intro: funcset_mem simp add: Upper_def)
-        from a show "A \<subseteq> \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>"
-          by (auto)
-        from a show "\<Squnion>\<^bsub>L\<^esub>A \<in> \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>"
-          apply (rule_tac L.at_least_at_most_member)
-          apply (auto)
-          apply (meson L.at_least_at_most_closed L.sup_closed subset_trans)
-          apply (meson False L.at_least_at_most_closed L.at_least_at_most_lower L.le_trans L.sup_closed b all_not_in_conv assms(2) contra_subsetD subset_trans)
-          apply (rule L.sup_least)
-          apply (auto simp add: assms)
-          using L.at_least_at_most_closed apply blast
-        done
+        from a show *: "A \<subseteq> \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>"
+          by auto
+        show "\<Squnion>\<^bsub>L\<^esub>A \<in> \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>"
+        proof (rule_tac L.at_least_at_most_member)
+          show 1: "\<Squnion>\<^bsub>L\<^esub>A \<in> carrier L"
+            by (meson L.at_least_at_most_closed L.sup_closed subset_trans *)
+          show "a \<sqsubseteq>\<^bsub>L\<^esub> \<Squnion>\<^bsub>L\<^esub>A"
+            by (meson "*" False L.at_least_at_most_closed L.at_least_at_most_lower L.le_trans L.sup_upper 1 all_not_in_conv assms(2) set_mp subset_trans)
+          show "\<Squnion>\<^bsub>L\<^esub>A \<sqsubseteq>\<^bsub>L\<^esub> b"
+          proof (rule L.sup_least)
+            show "A \<subseteq> carrier L" "\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq>\<^bsub>L\<^esub> b"
+              using * L.at_least_at_most_closed by blast+
+          qed (simp add: assms)
+        qed
       qed
     qed
     show "\<exists>s. is_glb (L\<lparr>carrier := \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>\<rparr>) s A"
@@ -711,15 +714,17 @@
           using a L.at_least_at_most_closed by (force intro!: L.inf_lower)
         show "\<And>y. y \<in> Lower (L\<lparr>carrier := \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>\<rparr>) A \<Longrightarrow> y \<sqsubseteq>\<^bsub>L\<^esub> \<Sqinter>\<^bsub>L\<^esub>A"
            using a L.at_least_at_most_closed by (rule_tac L.inf_greatest, auto intro: funcset_carrier' simp add: Lower_def)
-        from a show "A \<subseteq> \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>"
-          by (auto)
-        from a show "\<Sqinter>\<^bsub>L\<^esub>A \<in> \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>"
-          apply (rule_tac L.at_least_at_most_member)
-          apply (auto)
-          apply (meson L.at_least_at_most_closed L.inf_closed subset_trans)
-          apply (meson L.at_least_at_most_closed L.at_least_at_most_lower L.inf_greatest assms(2) set_rev_mp subset_trans)
-          apply (meson False L.at_least_at_most_closed L.at_least_at_most_upper L.inf_closed L.le_trans b all_not_in_conv assms(3) contra_subsetD subset_trans)            
-        done
+        from a show *: "A \<subseteq> \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>"
+          by auto
+        show "\<Sqinter>\<^bsub>L\<^esub>A \<in> \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>"
+        proof (rule_tac L.at_least_at_most_member)
+          show 1: "\<Sqinter>\<^bsub>L\<^esub>A \<in> carrier L"
+            by (meson "*" L.at_least_at_most_closed L.inf_closed subset_trans)
+          show "a \<sqsubseteq>\<^bsub>L\<^esub> \<Sqinter>\<^bsub>L\<^esub>A"
+            by (meson "*" L.at_least_at_most_closed L.at_least_at_most_lower L.inf_greatest assms(2) subsetD subset_trans)
+          show "\<Sqinter>\<^bsub>L\<^esub>A \<sqsubseteq>\<^bsub>L\<^esub> b"
+            by (meson * 1 False L.at_least_at_most_closed L.at_least_at_most_upper L.inf_lower L.le_trans all_not_in_conv assms(3) set_mp subset_trans)
+        qed
       qed
     qed
   qed
@@ -731,7 +736,7 @@
 text \<open>The set of fixed points of a complete lattice is itself a complete lattice\<close>
 
 theorem Knaster_Tarski:
-  assumes "weak_complete_lattice L" "f \<in> carrier L \<rightarrow> carrier L" "isotone L L f"
+  assumes "weak_complete_lattice L" and f: "f \<in> carrier L \<rightarrow> carrier L" and "isotone L L f"
   shows "weak_complete_lattice (fpl L f)" (is "weak_complete_lattice ?L'")
 proof -
   interpret L: weak_complete_lattice L
@@ -805,15 +810,14 @@
       show "is_lub ?L'' (LFP\<^bsub>?L'\<^esub> f) A"
       proof (rule least_UpperI, simp_all)
         fix x
-        assume "x \<in> Upper ?L'' A"
-        hence "LFP\<^bsub>?L'\<^esub> f \<sqsubseteq>\<^bsub>?L'\<^esub> x"
-          apply (rule_tac L'.LFP_lowerbound)
-          apply (auto simp add: Upper_def)
-          apply (simp add: A AL L.at_least_at_most_member L.sup_least set_rev_mp)          
-          apply (simp add: Pi_iff assms(2) fps_def, rule_tac L.weak_refl)
-          apply (auto)
-          apply (rule funcset_mem[of f "carrier L"], simp_all add: assms(2))
-        done
+        assume x: "x \<in> Upper ?L'' A"
+        have "LFP\<^bsub>?L'\<^esub> f \<sqsubseteq>\<^bsub>?L'\<^esub> x"
+        proof (rule L'.LFP_lowerbound, simp_all)
+          show "x \<in> \<lbrace>\<Squnion>\<^bsub>L\<^esub>A..\<top>\<^bsub>L\<^esub>\<rbrace>\<^bsub>L\<^esub>"
+            using x by (auto simp add: Upper_def A AL L.at_least_at_most_member L.sup_least set_rev_mp)    
+          with x show "f x \<sqsubseteq>\<^bsub>L\<^esub> x"
+            by (simp add: Upper_def) (meson L.at_least_at_most_closed L.use_fps L.weak_refl subsetD f_top_chain imageI)
+        qed
         thus " LFP\<^bsub>?L'\<^esub> f \<sqsubseteq>\<^bsub>L\<^esub> x"
           by (simp)
       next
@@ -838,17 +842,13 @@
              by (auto simp add: at_least_at_most_def)
           have "LFP\<^bsub>?L'\<^esub> f .=\<^bsub>?L'\<^esub> f (LFP\<^bsub>?L'\<^esub> f)"
           proof (rule "L'.LFP_weak_unfold", simp_all)
-            show "f \<in> \<lbrace>\<Squnion>\<^bsub>L\<^esub>A..\<top>\<^bsub>L\<^esub>\<rbrace>\<^bsub>L\<^esub> \<rightarrow> \<lbrace>\<Squnion>\<^bsub>L\<^esub>A..\<top>\<^bsub>L\<^esub>\<rbrace>\<^bsub>L\<^esub>"
-              apply (auto simp add: Pi_def at_least_at_most_def)
-              using assms(2) apply blast
-              apply (meson AL funcset_mem L.le_trans L.sup_closed assms(2) assms(3) pf_w use_iso2)
-              using assms(2) apply blast
-            done
-            from assms(3) show "Mono\<^bsub>L\<lparr>carrier := \<lbrace>\<Squnion>\<^bsub>L\<^esub>A..\<top>\<^bsub>L\<^esub>\<rbrace>\<^bsub>L\<^esub>\<rparr>\<^esub> f"
-              apply (auto simp add: isotone_def)
-              using L'.weak_partial_order_axioms apply blast
-              apply (meson L.at_least_at_most_closed subsetCE)
-            done
+            have "\<And>x. \<lbrakk>x \<in> carrier L; \<Squnion>\<^bsub>L\<^esub>A \<sqsubseteq>\<^bsub>L\<^esub> x\<rbrakk> \<Longrightarrow> \<Squnion>\<^bsub>L\<^esub>A \<sqsubseteq>\<^bsub>L\<^esub> f x"
+              by (meson AL funcset_mem L.le_trans L.sup_closed assms(2) assms(3) pf_w use_iso2)
+            with f show "f \<in> \<lbrace>\<Squnion>\<^bsub>L\<^esub>A..\<top>\<^bsub>L\<^esub>\<rbrace>\<^bsub>L\<^esub> \<rightarrow> \<lbrace>\<Squnion>\<^bsub>L\<^esub>A..\<top>\<^bsub>L\<^esub>\<rbrace>\<^bsub>L\<^esub>"
+              by (auto simp add: Pi_def at_least_at_most_def)
+            show "Mono\<^bsub>L\<lparr>carrier := \<lbrace>\<Squnion>\<^bsub>L\<^esub>A..\<top>\<^bsub>L\<^esub>\<rbrace>\<^bsub>L\<^esub>\<rparr>\<^esub> f"
+              using L'.weak_partial_order_axioms assms(3) 
+              by (auto simp add: isotone_def) (meson L.at_least_at_most_closed subsetCE)
           qed
           thus "f (LFP\<^bsub>?L'\<^esub> f) .=\<^bsub>L\<^esub> LFP\<^bsub>?L'\<^esub> f"
             by (simp add: L.equivalence_axioms funcset_carrier' c assms(2) equivalence.sym) 
@@ -889,7 +889,6 @@
           thus ?thesis
             by (meson AL L.inf_closed L.le_trans assms(3) b(1) b(2) fx use_iso2 w)
         qed
-   
         show "\<bottom>\<^bsub>L\<^esub> \<sqsubseteq>\<^bsub>L\<^esub> f x"
           by (simp add: fx)
       qed
@@ -905,12 +904,16 @@
       proof (rule greatest_LowerI, simp_all)
         fix x
         assume "x \<in> Lower ?L'' A"
-        hence "x \<sqsubseteq>\<^bsub>?L'\<^esub> GFP\<^bsub>?L'\<^esub> f"
-          apply (rule_tac L'.GFP_upperbound)
-          apply (auto simp add: Lower_def)
-          apply (meson A AL L.at_least_at_most_member L.bottom_lower L.weak_complete_lattice_axioms fps_carrier subsetCE weak_complete_lattice.inf_greatest)
-          apply (simp add: funcset_carrier' L.sym assms(2) fps_def)          
-        done
+        then have x: "\<forall>y. y \<in> A \<and> y \<in> fps L f \<longrightarrow> x \<sqsubseteq>\<^bsub>L\<^esub> y" "x \<in> fps L f"
+          by (auto simp add: Lower_def)
+        have "x \<sqsubseteq>\<^bsub>?L'\<^esub> GFP\<^bsub>?L'\<^esub> f"
+          unfolding Lower_def
+        proof (rule_tac L'.GFP_upperbound; simp)
+          show "x \<in> \<lbrace>\<bottom>\<^bsub>L\<^esub>..\<Sqinter>\<^bsub>L\<^esub>A\<rbrace>\<^bsub>L\<^esub>"
+            by (meson x A AL L.at_least_at_most_member L.bottom_lower L.inf_greatest contra_subsetD fps_carrier)
+          show "x \<sqsubseteq>\<^bsub>L\<^esub> f x"
+            using x by (simp add: funcset_carrier' L.sym assms(2) fps_def)
+        qed
         thus "x \<sqsubseteq>\<^bsub>L\<^esub> GFP\<^bsub>?L'\<^esub> f"
           by (simp)
       next
@@ -935,17 +938,14 @@
              by (auto simp add: at_least_at_most_def)
           have "GFP\<^bsub>?L'\<^esub> f .=\<^bsub>?L'\<^esub> f (GFP\<^bsub>?L'\<^esub> f)"
           proof (rule "L'.GFP_weak_unfold", simp_all)
-            show "f \<in> \<lbrace>\<bottom>\<^bsub>L\<^esub>..?w\<rbrace>\<^bsub>L\<^esub> \<rightarrow> \<lbrace>\<bottom>\<^bsub>L\<^esub>..?w\<rbrace>\<^bsub>L\<^esub>"
-              apply (auto simp add: Pi_def at_least_at_most_def)
-              using assms(2) apply blast
-              apply (simp add: funcset_carrier' assms(2))
-              apply (meson AL funcset_carrier L.inf_closed L.le_trans assms(2) assms(3) pf_w use_iso2)
-            done
-            from assms(3) show "Mono\<^bsub>L\<lparr>carrier := \<lbrace>\<bottom>\<^bsub>L\<^esub>..?w\<rbrace>\<^bsub>L\<^esub>\<rparr>\<^esub> f"
-              apply (auto simp add: isotone_def)
-              using L'.weak_partial_order_axioms apply blast
-              using L.at_least_at_most_closed apply (blast intro: funcset_carrier')
-            done
+            have "\<And>x. \<lbrakk>x \<in> carrier L; x \<sqsubseteq>\<^bsub>L\<^esub> \<Sqinter>\<^bsub>L\<^esub>A\<rbrakk> \<Longrightarrow> f x \<sqsubseteq>\<^bsub>L\<^esub> \<Sqinter>\<^bsub>L\<^esub>A"
+              by (meson AL funcset_carrier L.inf_closed L.le_trans assms(2) assms(3) pf_w use_iso2)
+            with assms(2) show "f \<in> \<lbrace>\<bottom>\<^bsub>L\<^esub>..?w\<rbrace>\<^bsub>L\<^esub> \<rightarrow> \<lbrace>\<bottom>\<^bsub>L\<^esub>..?w\<rbrace>\<^bsub>L\<^esub>"
+              by (auto simp add: Pi_def at_least_at_most_def)
+            have "\<And>x y. \<lbrakk>x \<in> \<lbrace>\<bottom>\<^bsub>L\<^esub>..\<Sqinter>\<^bsub>L\<^esub>A\<rbrace>\<^bsub>L\<^esub>; y \<in> \<lbrace>\<bottom>\<^bsub>L\<^esub>..\<Sqinter>\<^bsub>L\<^esub>A\<rbrace>\<^bsub>L\<^esub>; x \<sqsubseteq>\<^bsub>L\<^esub> y\<rbrakk> \<Longrightarrow> f x \<sqsubseteq>\<^bsub>L\<^esub> f y"
+              by (meson L.at_least_at_most_closed subsetD use_iso1  assms(3)) 
+            with L'.weak_partial_order_axioms show "Mono\<^bsub>L\<lparr>carrier := \<lbrace>\<bottom>\<^bsub>L\<^esub>..?w\<rbrace>\<^bsub>L\<^esub>\<rparr>\<^esub> f"
+              by (auto simp add: isotone_def)
           qed
           thus "f (GFP\<^bsub>?L'\<^esub> f) .=\<^bsub>L\<^esub> GFP\<^bsub>?L'\<^esub> f"
             by (simp add: L.equivalence_axioms funcset_carrier' c assms(2) equivalence.sym) 
@@ -1117,17 +1117,16 @@
     qed
     show "\<Sqinter>\<^bsub>fpl L f\<^esub>A \<sqsubseteq>\<^bsub>L\<^esub> f (\<Sqinter>\<^bsub>L\<^esub>A)"
     proof -
+      have *: "\<Sqinter>\<^bsub>fpl L f\<^esub>A \<in> carrier L"
+        using FA infA by blast
       have "\<And>x. x \<in> A \<Longrightarrow> \<Sqinter>\<^bsub>fpl L f\<^esub>A \<sqsubseteq>\<^bsub>fpl L f\<^esub> x"
         by (rule L'.inf_lower, simp_all add: assms)
       hence "\<Sqinter>\<^bsub>fpl L f\<^esub>A \<sqsubseteq>\<^bsub>L\<^esub> (\<Sqinter>\<^bsub>L\<^esub>A)"
-        apply (rule_tac L.inf_greatest, simp_all add: A)
-        using FA infA apply blast
-        done
+        by (rule_tac L.inf_greatest, simp_all add: A *)
       hence 1:"f(\<Sqinter>\<^bsub>fpl L f\<^esub>A) \<sqsubseteq>\<^bsub>L\<^esub> f(\<Sqinter>\<^bsub>L\<^esub>A)"
         by (metis (no_types, lifting) A FA L.inf_closed assms(2) infA subsetCE use_iso1)
       have 2:"\<Sqinter>\<^bsub>fpl L f\<^esub>A \<sqsubseteq>\<^bsub>L\<^esub> f (\<Sqinter>\<^bsub>fpl L f\<^esub>A)"
         by (metis (no_types, lifting) FA L.sym L.use_fps L.weak_complete_lattice_axioms PiE assms(4) infA subsetCE weak_complete_lattice_def weak_partial_order.weak_refl)
-        
       show ?thesis  
         using FA fA infA by (auto intro!: L.le_trans[OF 2 1] ic fc, metis FA PiE assms(4) subsetCE)
     qed
@@ -1189,21 +1188,11 @@
 lemma sup_pres_is_join_pres:
   assumes "weak_sup_pres X Y f"
   shows "join_pres X Y f"
-  using assms
-  apply (simp add: join_pres_def weak_sup_pres_def, safe)
-  apply (rename_tac x y)
-  apply (drule_tac x="{x, y}" in spec)
-  apply (auto simp add: join_def)
-done
+  using assms by (auto simp: join_pres_def weak_sup_pres_def join_def)
 
 lemma inf_pres_is_meet_pres:
   assumes "weak_inf_pres X Y f"
   shows "meet_pres X Y f"
-  using assms
-  apply (simp add: meet_pres_def weak_inf_pres_def, safe)
-  apply (rename_tac x y)
-  apply (drule_tac x="{x, y}" in spec)
-  apply (auto simp add: meet_def)
-done
+  using assms by (auto simp: meet_pres_def weak_inf_pres_def meet_def)
 
 end
diff -r 5cbd9cda7626 -r f3763989d589 src/HOL/Algebra/Coset.thy
--- a/src/HOL/Algebra/Coset.thy	Sun Jul 29 13:18:10 2018 +0200
+++ b/src/HOL/Algebra/Coset.thy	Sun Jul 29 18:24:47 2018 +0200
@@ -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"
     by (simp add: subgroup_def)
-  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 (auto simp add: RCOSETS_def)
-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])
-apply (simp add: 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: rcosets_part_G)
-  apply (simp add: card_rcosets_equal subgroup.subset)
-apply (simp add: rcos_disjoint)
-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 (simp add: FactGroup_def)
-apply (rule groupI)
+  unfolding FactGroup_def
+  apply (rule groupI)
     apply (simp add: setmult_closed)
    apply (simp add: normal_imp_subgroup subgroup_in_rcosets [OF is_group])
   apply (simp add: restrictI setmult_closed rcosets_assoc)
@@ -922,10 +913,20 @@
   by (simp add: FactGroup_def)
 
 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"
-apply (simp add: G.normal_inv_iff subgroup_kernel)
-apply (simp add: kernel_def)
-done
+  apply (simp only: G.normal_inv_iff subgroup_kernel)
+  apply (simp add: kernel_def)
+  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
-             simp add: set_mult_def
-                       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
+          simp add: set_mult_def
+          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)
-apply (simp add: G.m_assoc)
-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
diff -r 5cbd9cda7626 -r f3763989d589 src/HOL/Algebra/Divisibility.thy
--- a/src/HOL/Algebra/Divisibility.thy	Sun Jul 29 13:18:10 2018 +0200
+++ b/src/HOL/Algebra/Divisibility.thy	Sun Jul 29 18:24:47 2018 +0200
@@ -547,22 +547,14 @@
   using pf by (elim properfactorE)
 
 lemma (in monoid) properfactor_trans1 [trans]:
-  assumes dvds: "a divides b"  "properfactor G b c"
-    and carr: "a \<in> carrier G"  "c \<in> carrier G"
+  assumes "a divides b"  "properfactor G b c" "a \<in> carrier G"  "c \<in> carrier G"
   shows "properfactor G a c"
-  using dvds carr
-  apply (elim properfactorE, intro properfactorI)
-   apply (iprover intro: divides_trans)+
-  done
+  by (meson divides_trans properfactorE properfactorI assms)
 
 lemma (in monoid) properfactor_trans2 [trans]:
-  assumes dvds: "properfactor G a b"  "b divides c"
-    and carr: "a \<in> carrier G"  "b \<in> carrier G"
+  assumes "properfactor G a b"  "b divides c" "a \<in> carrier G"  "b \<in> carrier G"
   shows "properfactor G a c"
-  using dvds carr
-  apply (elim properfactorE, intro properfactorI)
-   apply (iprover intro: divides_trans)+
-  done
+  by (meson divides_trans properfactorE properfactorI assms)
 
 lemma properfactor_lless:
   fixes G (structure)
@@ -660,23 +652,20 @@
   using assms by (fast elim: irreducibleE)
 
 lemma (in monoid_cancel) irreducible_cong [trans]:
-  assumes irred: "irreducible G a"
-    and aa': "a \<sim> a'" "a \<in> carrier G"  "a' \<in> carrier G"
+  assumes "irreducible G a" "a \<sim> a'" "a \<in> carrier G"  "a' \<in> carrier G"
   shows "irreducible G a'"
-  using assms
-  apply (auto simp: irreducible_def assoc_unit_l)
-  apply (metis aa' associated_sym properfactor_cong_r)
-  done
+proof -
+  have "a' divides a"
+    by (meson \<open>a \<sim> a'\<close> associated_def)
+  then show ?thesis
+    by (metis (no_types) assms assoc_unit_l irreducibleE irreducibleI monoid.properfactor_trans2 monoid_axioms)
+qed
 
 lemma (in monoid) irreducible_prod_rI:
-  assumes airr: "irreducible G a"
-    and bunit: "b \<in> Units G"
-    and carr[simp]: "a \<in> carrier G"  "b \<in> carrier G"
+  assumes "irreducible G a" "b \<in> Units G" "a \<in> carrier G"  "b \<in> carrier G"
   shows "irreducible G (a \<otimes> b)"
-  using airr carr bunit
-  apply (elim irreducibleE, intro irreducibleI)
-  using prod_unit_r apply blast
-  using associatedI2' properfactor_cong_r by auto
+  using assms
+  by (metis (no_types, lifting) associatedI2' irreducible_def monoid.m_closed monoid_axioms prod_unit_r properfactor_cong_r)
 
 lemma (in comm_monoid) irreducible_prod_lI:
   assumes birr: "irreducible G b"
@@ -764,9 +753,7 @@
     and pp': "p \<sim> p'" "p \<in> carrier G"  "p' \<in> carrier G"
   shows "prime G p'"
   using assms
-  apply (auto simp: prime_def assoc_unit_l)
-  apply (metis pp' associated_sym divides_cong_l)
-  done
+  by (auto simp: prime_def assoc_unit_l) (metis pp' associated_sym divides_cong_l)
 
 (*by Paulo Emílio de Vilhena*)
 lemma (in comm_monoid_cancel) prime_irreducible:
@@ -849,9 +836,7 @@
     and "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G"
   shows "\<forall>a\<in>set bs. irreducible G a"
   using assms
-  apply (clarsimp simp add: list_all2_conv_all_nth set_conv_nth)
-  apply (blast intro: irreducible_cong)
-  done
+  by (fastforce simp add: list_all2_conv_all_nth set_conv_nth intro: irreducible_cong)
 
 
 text \<open>Permutations\<close>
@@ -1001,15 +986,7 @@
   then have f: "f \<in> carrier G"
     by blast
   show ?case
-  proof (cases "f = a")
-    case True
-    then show ?thesis
-      using Cons.prems by auto
-  next
-    case False
-    with Cons show ?thesis
-      by clarsimp (metis f divides_prod_l multlist_closed)
-  qed
+    using Cons.IH Cons.prems(1) Cons.prems(2) divides_prod_l f by auto
 qed auto
 
 lemma (in comm_monoid_cancel) multlist_listassoc_cong:
@@ -1051,9 +1028,7 @@
     and "set fs \<subseteq> carrier G" and "set fs' \<subseteq> carrier G"
   shows "foldr (\<otimes>) fs \<one> \<sim> foldr (\<otimes>) fs' \<one>"
   using assms
-  apply (elim essentially_equalE)
-  apply (simp add: multlist_perm_cong multlist_listassoc_cong perm_closed)
-  done
+  by (metis essentially_equal_def multlist_listassoc_cong multlist_perm_cong perm_closed)
 
 
 subsubsection \<open>Factorization in irreducible elements\<close>
@@ -1120,9 +1095,6 @@
     and carr[simp]: "set fs \<subseteq> carrier G"
   shows "fs = []"
 proof (cases fs)
-  case Nil
-  then show ?thesis .
-next
   case fs: (Cons f fs')
   from carr have fcarr[simp]: "f \<in> carrier G" and carr'[simp]: "set fs' \<subseteq> carrier G"
     by (simp_all add: fs)
@@ -1874,6 +1846,18 @@
 qed
 
 lemma (in factorial_monoid) properfactor_fmset:
+  assumes "properfactor G a b"
+    and "wfactors G as a"
+    and "wfactors G bs b"
+    and "a \<in> carrier G"
+    and "b \<in> carrier G"
+    and "set as \<subseteq> carrier G"
+    and "set bs \<subseteq> carrier G"
+  shows "fmset G as \<subseteq># fmset G bs"
+  using assms
+  by (meson divides_as_fmsubset properfactor_divides)
+
+lemma (in factorial_monoid) properfactor_fmset_ne:
   assumes pf: "properfactor G a b"
     and "wfactors G as a"
     and "wfactors G bs b"
@@ -1881,11 +1865,8 @@
     and "b \<in> carrier G"
     and "set as \<subseteq> carrier G"
     and "set bs \<subseteq> carrier G"
-  shows "fmset G as \<subseteq># fmset G bs \<and> fmset G as \<noteq> fmset G bs"
-  using pf
-  apply safe
-   apply (meson assms divides_as_fmsubset monoid.properfactor_divides monoid_axioms)
-  by (meson assms associated_def comm_monoid_cancel.ee_wfactorsD comm_monoid_cancel.fmset_ee factorial_monoid_axioms factorial_monoid_def properfactorE)
+  shows "fmset G as \<noteq> fmset G bs"
+  using properfactorE [OF pf] assms divides_as_fmsubset by force
 
 subsection \<open>Irreducible Elements are Prime\<close>
 
@@ -2246,75 +2227,70 @@
 qed
 
 lemma (in gcd_condition_monoid) gcdof_cong_l:
-  assumes a'a: "a' \<sim> a"
-    and agcd: "a gcdof b c"
-    and a'carr: "a' \<in> carrier G" and carr': "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
+  assumes "a' \<sim> a" "a gcdof b c" "a' \<in> carrier G" and carr': "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
   shows "a' gcdof b c"
 proof -
-  note carr = a'carr carr'
   interpret weak_lower_semilattice "division_rel G" by simp
   have "is_glb (division_rel G) a' {b, c}"
-    by (subst greatest_Lower_cong_l[of _ a]) (simp_all add: a'a carr gcdof_greatestLower[symmetric] agcd)
+    by (subst greatest_Lower_cong_l[of _ a]) (simp_all add: assms gcdof_greatestLower[symmetric])
   then have "a' \<in> carrier G \<and> a' gcdof b c"
     by (simp add: gcdof_greatestLower carr')
   then show ?thesis ..
 qed
 
 lemma (in gcd_condition_monoid) gcd_closed [simp]:
-  assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
+  assumes "a \<in> carrier G" "b \<in> carrier G"
   shows "somegcd G a b \<in> carrier G"
 proof -
   interpret weak_lower_semilattice "division_rel G" by simp
   show ?thesis
-    apply (simp add: somegcd_meet[OF carr])
-    apply (rule meet_closed[simplified], fact+)
-    done
+  using  assms meet_closed by (simp add: somegcd_meet)
 qed
 
 lemma (in gcd_condition_monoid) gcd_isgcd:
-  assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
+  assumes "a \<in> carrier G"  "b \<in> carrier G"
   shows "(somegcd G a b) gcdof a b"
 proof -
   interpret weak_lower_semilattice "division_rel G"
     by simp
-  from carr have "somegcd G a b \<in> carrier G \<and> (somegcd G a b) gcdof a b"
+  from assms have "somegcd G a b \<in> carrier G \<and> (somegcd G a b) gcdof a b"
     by (simp add: gcdof_greatestLower inf_of_two_greatest meet_def somegcd_meet)
   then show "(somegcd G a b) gcdof a b"
     by simp
 qed
 
 lemma (in gcd_condition_monoid) gcd_exists:
-  assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
+  assumes "a \<in> carrier G"  "b \<in> carrier G"
   shows "\<exists>x\<in>carrier G. x = somegcd G a b"
 proof -
   interpret weak_lower_semilattice "division_rel G"
     by simp
   show ?thesis
-    by (metis carr(1) carr(2) gcd_closed)
+    by (metis assms gcd_closed)
 qed
 
 lemma (in gcd_condition_monoid) gcd_divides_l:
-  assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
+  assumes "a \<in> carrier G" "b \<in> carrier G"
   shows "(somegcd G a b) divides a"
 proof -
   interpret weak_lower_semilattice "division_rel G"
     by simp
   show ?thesis
-    by (metis carr(1) carr(2) gcd_isgcd isgcd_def)
+    by (metis assms gcd_isgcd isgcd_def)
 qed
 
 lemma (in gcd_condition_monoid) gcd_divides_r:
-  assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
+  assumes "a \<in> carrier G"  "b \<in> carrier G"
   shows "(somegcd G a b) divides b"
 proof -
   interpret weak_lower_semilattice "division_rel G"
     by simp
   show ?thesis
-    by (metis carr gcd_isgcd isgcd_def)
+    by (metis assms gcd_isgcd isgcd_def)
 qed
 
 lemma (in gcd_condition_monoid) gcd_divides:
-  assumes sub: "z divides x"  "z divides y"
+  assumes "z divides x" "z divides y"
     and L: "x \<in> carrier G"  "y \<in> carrier G"  "z \<in> carrier G"
   shows "z divides (somegcd G x y)"
 proof -
@@ -2325,49 +2301,25 @@
 qed
 
 lemma (in gcd_condition_monoid) gcd_cong_l:
-  assumes xx': "x \<sim> x'"
-    and carr: "x \<in> carrier G"  "x' \<in> carrier G"  "y \<in> carrier G"
+  assumes "x \<sim> x'" "x \<in> carrier G"  "x' \<in> carrier G"  "y \<in> carrier G"
   shows "somegcd G x y \<sim> somegcd G x' y"
 proof -
   interpret weak_lower_semilattice "division_rel G"
     by simp
   show ?thesis
-    apply (simp add: somegcd_meet carr)
-    apply (rule meet_cong_l[simplified], fact+)
-    done
+    using somegcd_meet assms
+    by (metis eq_object.select_convs(1) meet_cong_l partial_object.select_convs(1))
 qed
 
 lemma (in gcd_condition_monoid) gcd_cong_r:
-  assumes carr: "x \<in> carrier G"  "y \<in> carrier G"  "y' \<in> carrier G"
-    and yy': "y \<sim> y'"
+  assumes "y \<sim> y'" "x \<in> carrier G"  "y \<in> carrier G" "y' \<in> carrier G"
   shows "somegcd G x y \<sim> somegcd G x y'"
 proof -
   interpret weak_lower_semilattice "division_rel G" by simp
   show ?thesis
-    apply (simp add: somegcd_meet carr)
-    apply (rule meet_cong_r[simplified], fact+)
-    done
+    by (meson associated_def assms gcd_closed gcd_divides gcd_divides_l gcd_divides_r monoid.divides_trans monoid_axioms)
 qed
 
-(*
-lemma (in gcd_condition_monoid) asc_cong_gcd_l [intro]:
-  assumes carr: "b \<in> carrier G"
-  shows "asc_cong (\<lambda>a. somegcd G a b)"
-using carr
-unfolding CONG_def
-by clarsimp (blast intro: gcd_cong_l)
-
-lemma (in gcd_condition_monoid) asc_cong_gcd_r [intro]:
-  assumes carr: "a \<in> carrier G"
-  shows "asc_cong (\<lambda>b. somegcd G a b)"
-using carr
-unfolding CONG_def
-by clarsimp (blast intro: gcd_cong_r)
-
-lemmas (in gcd_condition_monoid) asc_cong_gcd_split [simp] =
-    assoc_split[OF _ asc_cong_gcd_l] assoc_split[OF _ asc_cong_gcd_r]
-*)
-
 lemma (in gcd_condition_monoid) gcdI:
   assumes dvd: "a divides b"  "a divides c"
     and others: "\<And>y. \<lbrakk>y\<in>carrier G; y divides b; y divides c\<rbrakk> \<Longrightarrow> y divides a"
@@ -2390,25 +2342,23 @@
 
 lemma (in gcd_condition_monoid) SomeGcd_ex:
   assumes "finite A"  "A \<subseteq> carrier G"  "A \<noteq> {}"
-  shows "\<exists>x\<in> carrier G. x = SomeGcd G A"
+  shows "\<exists>x \<in> carrier G. x = SomeGcd G A"
 proof -
   interpret weak_lower_semilattice "division_rel G"
     by simp
   show ?thesis
-    apply (simp add: SomeGcd_def)
-    apply (rule finite_inf_closed[simplified], fact+)
-    done
+    using finite_inf_closed by (simp add: assms SomeGcd_def)
 qed
 
 lemma (in gcd_condition_monoid) gcd_assoc:
-  assumes carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
+  assumes "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
   shows "somegcd G (somegcd G a b) c \<sim> somegcd G a (somegcd G b c)"
 proof -
   interpret weak_lower_semilattice "division_rel G"
     by simp
   show ?thesis
     unfolding associated_def
-    by (meson carr divides_trans gcd_divides gcd_divides_l gcd_divides_r gcd_exists)
+    by (meson assms divides_trans gcd_divides gcd_divides_l gcd_divides_r gcd_exists)
 qed
 
 lemma (in gcd_condition_monoid) gcd_mult:
@@ -2641,141 +2591,124 @@
     using Cons.IH Cons.prems(1) by force
 qed
 
-
-lemma (in primeness_condition_monoid) wfactors_unique__hlp_induct:
-  "\<forall>a as'. a \<in> carrier G \<and> set as \<subseteq> carrier G \<and> set as' \<subseteq> carrier G \<and>
-           wfactors G as a \<and> wfactors G as' a \<longrightarrow> essentially_equal G as as'"
-proof (induct as)
+proposition (in primeness_condition_monoid) wfactors_unique:
+  assumes "wfactors G as a"  "wfactors G as' a"
+    and "a \<in> carrier G"  "set as \<subseteq> carrier G"  "set as' \<subseteq> carrier G"
+  shows "essentially_equal G as as'"
+  using assms
+proof (induct as arbitrary: a as')
   case Nil
-  show ?case
-    apply (clarsimp simp: wfactors_def)
-    by (metis Units_one_closed assoc_unit_r list_update_nonempty unit_wfactors_empty unitfactor_ee wfactorsI)
+  then have "a \<sim> \<one>"
+    by (meson Units_one_closed one_closed perm.Nil perm_wfactorsD unit_wfactors)
+  then have "as' = []"
+    using Nil.prems assoc_unit_l unit_wfactors_empty by blast
+  then show ?case
+    by auto
 next
   case (Cons ah as)
-  then show ?case
-  proof clarsimp
-    fix a as'
-    assume ih [rule_format]:
-      "\<forall>a as'. a \<in> carrier G \<and> set as' \<subseteq> carrier G \<and> wfactors G as a \<and>
-        wfactors G as' a \<longrightarrow> essentially_equal G as as'"
-      and acarr: "a \<in> carrier G" and ahcarr: "ah \<in> carrier G"
-      and ascarr: "set as \<subseteq> carrier G" and as'carr: "set as' \<subseteq> carrier G"
-      and afs: "wfactors G (ah # as) a"
-      and afs': "wfactors G as' a"
-    then have ahdvda: "ah divides a"
-      by (intro wfactors_dividesI[of "ah#as" "a"]) simp_all
+  then have ahdvda: "ah divides a"
+    using wfactors_dividesI by auto
     then obtain a' where a'carr: "a' \<in> carrier G" and a: "a = ah \<otimes> a'"
       by blast
+    have carr_ah: "ah \<in> carrier G" "set as \<subseteq> carrier G"
+      using Cons.prems by fastforce+
+    have "ah \<otimes> foldr (\<otimes>) as \<one> \<sim> a"
+      by (rule wfactorsE[OF \<open>wfactors G (ah # as) a\<close>]) auto
+    then have "foldr (\<otimes>) as \<one> \<sim> a'"
+      by (metis Cons.prems(4) a a'carr assoc_l_cancel insert_subset list.set(2) monoid.multlist_closed monoid_axioms)
+    then
     have a'fs: "wfactors G as a'"
-      apply (rule wfactorsE[OF afs], rule wfactorsI, simp)
-      by (metis a a'carr ahcarr ascarr assoc_l_cancel factorsI factors_def factors_mult_single list.set_intros(1) list.set_intros(2) multlist_closed)
-    from afs have ahirr: "irreducible G ah"
-      by (elim wfactorsE) simp
-    with ascarr have ahprime: "prime G ah"
-      by (intro irreducible_prime ahcarr)
-
-    note carr [simp] = acarr ahcarr ascarr as'carr a'carr
-
+      by (meson Cons.prems(1) set_subset_Cons subset_iff wfactorsE wfactorsI)
+    then have ahirr: "irreducible G ah"
+      by (meson Cons.prems(1) list.set_intros(1) wfactorsE)
+    with Cons have ahprime: "prime G ah"
+      by (simp add: irreducible_prime)
     note ahdvda
-    also from afs' have "a divides (foldr (\<otimes>) as' \<one>)"
-      by (elim wfactorsE associatedE, simp)
+    also have "a divides (foldr (\<otimes>) as' \<one>)"
+      by (meson Cons.prems(2) associatedE wfactorsE)
     finally have "ah divides (foldr (\<otimes>) as' \<one>)"
-      by simp
+      using Cons.prems(4) by auto
     with ahprime have "\<exists>i<length as'. ah divides as'!i"
-      by (intro multlist_prime_pos) simp_all
+      by (intro multlist_prime_pos) (use Cons.prems in auto)
     then obtain i where len: "i<length as'" and ahdvd: "ah divides as'!i"
       by blast
-    from afs' carr have irrasi: "irreducible G (as'!i)"
-      by (fast intro: nth_mem[OF len] elim: wfactorsE)
-    from len carr have asicarr[simp]: "as'!i \<in> carrier G"
-      unfolding set_conv_nth by force
-    note carr = carr asicarr
-
-    from ahdvd obtain x where "x \<in> carrier G" and asi: "as'!i = ah \<otimes> x"
+    then obtain x where "x \<in> carrier G" and asi: "as'!i = ah \<otimes> x"
       by blast
-    with carr irrasi[simplified asi] have asiah: "as'!i \<sim> ah"
-      by (metis ahprime associatedI2 irreducible_prodE primeE)
+    have irrasi: "irreducible G (as'!i)"
+      using nth_mem[OF len] wfactorsE
+      by (metis Cons.prems(2))
+    have asicarr[simp]: "as'!i \<in> carrier G"
+      using len \<open>set as' \<subseteq> carrier G\<close> nth_mem by blast
+    have asiah: "as'!i \<sim> ah"
+      by (metis \<open>ah \<in> carrier G\<close> \<open>x \<in> carrier G\<close> asi irrasi ahprime associatedI2 irreducible_prodE primeE)
     note setparts = set_take_subset[of i as'] set_drop_subset[of "Suc i" as']
-    note partscarr [simp] = setparts[THEN subset_trans[OF _ as'carr]]
-    note carr = carr partscarr
-
     have "\<exists>aa_1. aa_1 \<in> carrier G \<and> wfactors G (take i as') aa_1"
-      by (meson afs' in_set_takeD partscarr(1) wfactorsE wfactors_prod_exists)
-    then obtain aa_1 where aa1carr: "aa_1 \<in> carrier G" and aa1fs: "wfactors G (take i as') aa_1"
+      using Cons
+      by (metis setparts(1) subset_trans in_set_takeD wfactorsE wfactors_prod_exists)
+    then obtain aa_1 where aa1carr [simp]: "aa_1 \<in> carrier G" and aa1fs: "wfactors G (take i as') aa_1"
       by auto
-
-    have "\<exists>aa_2. aa_2 \<in> carrier G \<and> wfactors G (drop (Suc i) as') aa_2"
-      by (meson afs' in_set_dropD partscarr(2) wfactors_def wfactors_prod_exists)
-    then obtain aa_2 where aa2carr: "aa_2 \<in> carrier G"
+    obtain aa_2 where aa2carr [simp]: "aa_2 \<in> carrier G"
       and aa2fs: "wfactors G (drop (Suc i) as') aa_2"
-      by auto
-
-    note carr = carr aa1carr[simp] aa2carr[simp]
-
-    from aa1fs aa2fs
-    have v1: "wfactors G (take i as' @ drop (Suc i) as') (aa_1 \<otimes> aa_2)"
-      by (intro wfactors_mult, simp+)
-    then have v1': "wfactors G (as'!i # take i as' @ drop (Suc i) as') (as'!i \<otimes> (aa_1 \<otimes> aa_2))"
-      using irrasi wfactors_mult_single by auto
-    from aa2carr carr aa1fs aa2fs have "wfactors G (as'!i # drop (Suc i) as') (as'!i \<otimes> aa_2)"
-      by (metis irrasi wfactors_mult_single)
-    with len carr aa1carr aa2carr aa1fs
+      by (metis Cons.prems(2) Cons.prems(5) subset_code(1) in_set_dropD wfactors_def wfactors_prod_exists)
+
+    have set_drop: "set (drop (Suc i) as') \<subseteq> carrier G"
+      using Cons.prems(5) setparts(2) by blast
+    moreover have set_take: "set (take i as') \<subseteq> carrier G"
+      using  Cons.prems(5) setparts by auto
+    moreover have v1: "wfactors G (take i as' @ drop (Suc i) as') (aa_1 \<otimes> aa_2)"
+      using aa1fs aa2fs \<open>set as' \<subseteq> carrier G\<close> by (force simp add: dest: in_set_takeD in_set_dropD)
+    ultimately have v1': "wfactors G (as'!i # take i as' @ drop (Suc i) as') (as'!i \<otimes> (aa_1 \<otimes> aa_2))"
+      using irrasi wfactors_mult_single
+        by (simp add: irrasi v1 wfactors_mult_single)      
+    have "wfactors G (as'!i # drop (Suc i) as') (as'!i \<otimes> aa_2)"
+      by (simp add: aa2fs irrasi set_drop wfactors_mult_single)
+    with len  aa1carr aa2carr aa1fs
     have v2: "wfactors G (take i as' @ as'!i # drop (Suc i) as') (aa_1 \<otimes> (as'!i \<otimes> aa_2))"
-      using wfactors_mult by auto
+      using wfactors_mult  by (simp add: set_take set_drop) 
     from len have as': "as' = (take i as' @ as'!i # drop (Suc i) as')"
       by (simp add: Cons_nth_drop_Suc)
-    with carr have eer: "essentially_equal G (take i as' @ as'!i # drop (Suc i) as') as'"
-      by simp
-    with v2 afs' carr aa1carr aa2carr nth_mem[OF len] have "aa_1 \<otimes> (as'!i \<otimes> aa_2) \<sim> a"
-      by (metis as' ee_wfactorsD m_closed)
+    have eer: "essentially_equal G (take i as' @ as'!i # drop (Suc i) as') as'"
+      using Cons.prems(5) as' by auto
+    with v2 aa1carr aa2carr nth_mem[OF len] have "aa_1 \<otimes> (as'!i \<otimes> aa_2) \<sim> a"
+      using Cons.prems as' comm_monoid_cancel.ee_wfactorsD is_comm_monoid_cancel by fastforce
     then have t1: "as'!i \<otimes> (aa_1 \<otimes> aa_2) \<sim> a"
       by (metis aa1carr aa2carr asicarr m_lcomm)
-    from carr asiah have "ah \<otimes> (aa_1 \<otimes> aa_2) \<sim> as'!i \<otimes> (aa_1 \<otimes> aa_2)"
-      by (metis associated_sym m_closed mult_cong_l)
+    from asiah have "ah \<otimes> (aa_1 \<otimes> aa_2) \<sim> as'!i \<otimes> (aa_1 \<otimes> aa_2)"
+      by (simp add: \<open>ah \<in> carrier G\<close> associated_sym mult_cong_l)
     also note t1
-    finally have "ah \<otimes> (aa_1 \<otimes> aa_2) \<sim> a" by simp
-
-    with carr aa1carr aa2carr a'carr nth_mem[OF len] have a': "aa_1 \<otimes> aa_2 \<sim> a'"
-      by (simp add: a, fast intro: assoc_l_cancel[of ah _ a'])
-
+    finally have "ah \<otimes> (aa_1 \<otimes> aa_2) \<sim> a"
+      using Cons.prems(3) carr_ah aa1carr aa2carr by blast
+    with aa1carr aa2carr a'carr nth_mem[OF len] have a': "aa_1 \<otimes> aa_2 \<sim> a'"
+      using a assoc_l_cancel carr_ah(1) by blast
     note v1
     also note a'
     finally have "wfactors G (take i as' @ drop (Suc i) as') a'"
-      by simp
-
-    from a'fs this carr have "essentially_equal G as (take i as' @ drop (Suc i) as')"
-      by (intro ih[of a']) simp
-    then have ee1: "essentially_equal G (ah # as) (ah # take i as' @ drop (Suc i) as')"
-      by (elim essentially_equalE) (fastforce intro: essentially_equalI)
-
-    from carr have ee2: "essentially_equal G (ah # take i as' @ drop (Suc i) as')
+      by (simp add: a'carr set_drop set_take)
+    from a'fs this have "essentially_equal G as (take i as' @ drop (Suc i) as')"
+      using Cons.hyps a'carr carr_ah(2) set_drop set_take by auto
+    with carr_ah have ee1: "essentially_equal G (ah # as) (ah # take i as' @ drop (Suc i) as')"
+      by (auto simp: essentially_equal_def)
+    have ee2: "essentially_equal G (ah # take i as' @ drop (Suc i) as')
       (as' ! i # take i as' @ drop (Suc i) as')"
     proof (intro essentially_equalI)
       show "ah # take i as' @ drop (Suc i) as' <~~> ah # take i as' @ drop (Suc i) as'"
         by simp
     next
       show "ah # take i as' @ drop (Suc i) as' [\<sim>] as' ! i # take i as' @ drop (Suc i) as'"
-        by (simp add: list_all2_append) (simp add: asiah[symmetric])
+        by (simp add: asiah associated_sym set_drop set_take)
     qed
 
     note ee1
     also note ee2
     also have "essentially_equal G (as' ! i # take i as' @ drop (Suc i) as')
                                    (take i as' @ as' ! i # drop (Suc i) as')"
-      by (metis as' as'carr listassoc_refl essentially_equalI perm_append_Cons)
+      by (metis Cons.prems(5) as' essentially_equalI listassoc_refl perm_append_Cons)
     finally have "essentially_equal G (ah # as) (take i as' @ as' ! i # drop (Suc i) as')"
-      by simp
-    then show "essentially_equal G (ah # as) as'"
-      by (subst as')
-  qed
+      using Cons.prems(4) set_drop set_take by auto
+    then show ?case
+      using as' by auto
 qed
 
-lemma (in primeness_condition_monoid) wfactors_unique:
-  assumes "wfactors G as a"  "wfactors G as' a"
-    and "a \<in> carrier G"  "set as \<subseteq> carrier G"  "set as' \<subseteq> carrier G"
-  shows "essentially_equal G as as'"
-  by (rule wfactors_unique__hlp_induct[rule_format, of a]) (simp add: assms)
-
 
 subsubsection \<open>Application to factorial monoids\<close>
 
@@ -2841,7 +2774,6 @@
     by blast
 
   note [simp] = acarr bcarr ccarr ascarr cscarr
-
   assume b: "b = a \<otimes> c"
   from afs cfs have "wfactors G (as@cs) (a \<otimes> c)"
     by (intro wfactors_mult) simp_all
@@ -2918,9 +2850,7 @@
   apply unfold_locales
   apply (rule wfUNIVI)
   apply (rule measure_induct[of "factorcount G"])
-  apply simp
-  apply (metis properfactor_fcount)
-  done
+  using properfactor_fcount by auto
 
 sublocale factorial_monoid \<subseteq> primeness_condition_monoid
   by standard (rule irreducible_prime)
diff -r 5cbd9cda7626 -r f3763989d589 src/HOL/Algebra/Embedded_Algebras.thy
--- a/src/HOL/Algebra/Embedded_Algebras.thy	Sun Jul 29 13:18:10 2018 +0200
+++ b/src/HOL/Algebra/Embedded_Algebras.thy	Sun Jul 29 18:24:47 2018 +0200
@@ -187,7 +187,7 @@
 
 corollary Span_is_add_subgroup:
   "set Us \<subseteq> carrier R \<Longrightarrow> subgroup (Span K Us) (add_monoid R)"
-  using line_extension_is_subgroup add.normal_invE(1)[OF add.one_is_normal] by (induct Us) (auto)
+  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)
               Span_append_eq_set_add[OF in_carrier(2-3)] unfolding set_add_def' by blast
       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))"
diff -r 5cbd9cda7626 -r f3763989d589 src/HOL/Algebra/Generated_Groups.thy
--- a/src/HOL/Algebra/Generated_Groups.thy	Sun Jul 29 13:18:10 2018 +0200
+++ b/src/HOL/Algebra/Generated_Groups.thy	Sun Jul 29 18:24:47 2018 +0200
@@ -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"
       by (simp add: g m_assoc)
@@ -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
diff -r 5cbd9cda7626 -r f3763989d589 src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Sun Jul 29 13:18:10 2018 +0200
+++ b/src/HOL/Algebra/Group.thy	Sun Jul 29 18:24:47 2018 +0200
@@ -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 (auto simp add: image_subsetI)
-  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
diff -r 5cbd9cda7626 -r f3763989d589 src/HOL/Algebra/Ideal.thy
--- a/src/HOL/Algebra/Ideal.thy	Sun Jul 29 13:18:10 2018 +0200
+++ b/src/HOL/Algebra/Ideal.thy	Sun Jul 29 18:24:47 2018 +0200
@@ -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
 
diff -r 5cbd9cda7626 -r f3763989d589 src/HOL/Algebra/RingHom.thy
--- a/src/HOL/Algebra/RingHom.thy	Sun Jul 29 13:18:10 2018 +0200
+++ b/src/HOL/Algebra/RingHom.thy	Sun Jul 29 18:24:47 2018 +0200
@@ -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 
+  show "h \<in> hom (add_monoid R) (add_monoid S)"
+    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 (erule (1) compatible_add)
-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"
+      by (simp add: homh)
+  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 (rule additive_subgroup.a_subgroup[OF additive_subgroup_a_kernel])
- 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 (rule additive_subgroup.a_subgroup[OF additive_subgroup_a_kernel])
+   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:
diff -r 5cbd9cda7626 -r f3763989d589 src/HOL/Library/FuncSet.thy
--- a/src/HOL/Library/FuncSet.thy	Sun Jul 29 13:18:10 2018 +0200
+++ b/src/HOL/Library/FuncSet.thy	Sun Jul 29 18:24:47 2018 +0200
@@ -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)
 
diff -r 5cbd9cda7626 -r f3763989d589 src/HOL/Library/datatype_records.ML
--- a/src/HOL/Library/datatype_records.ML	Sun Jul 29 13:18:10 2018 +0200
+++ b/src/HOL/Library/datatype_records.ML	Sun Jul 29 18:24:47 2018 +0200
@@ -7,10 +7,10 @@
 
   val mk_update_defs: string -> local_theory -> local_theory
 
-  val bnf_record: binding -> ctr_options -> (binding option * (typ * sort)) list ->
+  val record: binding -> ctr_options -> (binding option * (typ * sort)) list ->
     (binding * typ) list -> local_theory -> local_theory
 
-  val bnf_record_cmd: binding -> ctr_options_cmd ->
+  val record_cmd: binding -> ctr_options_cmd ->
     (binding option * (string * string option)) list -> (binding * string) list -> local_theory ->
     local_theory
 
@@ -35,21 +35,31 @@
   val extend = I
 )
 
+fun mk_eq_dummy (lhs, rhs) =
+  Const (@{const_name HOL.eq}, dummyT --> dummyT --> @{typ bool}) $ lhs $ rhs
+
+val dummify = map_types (K dummyT)
+fun repeat_split_tac ctxt thm = REPEAT_ALL_NEW (CHANGED o Splitter.split_tac ctxt [thm])
+
 fun mk_update_defs typ_name lthy =
   let
     val short_name = Long_Name.base_name typ_name
+    val {ctrs, casex, selss, split, sel_thmss, injects, ...} =
+      the (Ctr_Sugar.ctr_sugar_of lthy typ_name)
+    val ctr = case ctrs of [ctr] => ctr | _ => error "Datatype_Records.mk_update_defs: expected only single constructor"
+    val sels = case selss of [sels] => sels | _ => error "Datatype_Records.mk_update_defs: expected selectors"
+    val sels_dummy = map dummify sels
+    val ctr_dummy = dummify ctr
+    val casex_dummy = dummify casex
+    val len = length sels
 
-    val {ctrs, casex, selss, ...} = the (Ctr_Sugar.ctr_sugar_of lthy typ_name)
-    val ctr = case ctrs of [ctr] => ctr | _ => error "BNF_Record.mk_update_defs: expected only single constructor"
-    val sels = case selss of [sels] => sels | _ => error "BNF_Record.mk_update_defs: expected selectors"
-    val ctr_dummy = Const (fst (dest_Const ctr), dummyT)
-    val casex_dummy = Const (fst (dest_Const casex), dummyT)
-
-    val len = length sels
+    val simp_thms = flat sel_thmss @ injects
 
     fun mk_name sel =
       Binding.name ("update_" ^ Long_Name.base_name (fst (dest_Const sel)))
 
+    val thms_binding = (@{binding record_simps}, @{attributes [simp]})
+
     fun mk_t idx =
       let
         val body =
@@ -59,22 +69,143 @@
         Abs ("f", dummyT, casex_dummy $ body)
       end
 
-    fun define name t =
-      Local_Theory.define ((name, NoSyn), ((Binding.empty, @{attributes [datatype_record_update, code]}), t)) #> snd
+    fun simp_only_tac ctxt =
+      REPEAT_ALL_NEW (resolve_tac ctxt @{thms impI allI}) THEN'
+        asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps simp_thms)
+
+    fun prove ctxt defs ts n =
+      let
+        val t = nth ts n
+
+        val sel_dummy = nth sels_dummy n
+        val t_dummy = dummify t
+        fun tac {context = ctxt, ...} =
+          Goal.conjunction_tac 1 THEN
+            Local_Defs.unfold_tac ctxt defs THEN
+            PARALLEL_ALLGOALS (repeat_split_tac ctxt split THEN' simp_only_tac ctxt)
+
+        val sel_upd_same_thm =
+          let
+            val ([f, x], ctxt') = Variable.add_fixes ["f", "x"] ctxt
+            val f = Free (f, dummyT)
+            val x = Free (x, dummyT)
+
+            val lhs = sel_dummy $ (t_dummy $ f $ x)
+            val rhs = f $ (sel_dummy $ x)
+            val prop = Syntax.check_term ctxt' (HOLogic.mk_Trueprop (mk_eq_dummy (lhs, rhs)))
+          in
+            [Goal.prove_future ctxt' [] [] prop tac]
+            |> Variable.export ctxt' ctxt
+          end
+
+        val sel_upd_diff_thms =
+          let
+            val ([f, x], ctxt') = Variable.add_fixes ["f", "x"] ctxt
+            val f = Free (f, dummyT)
+            val x = Free (x, dummyT)
+
+            fun lhs sel = sel $ (t_dummy $ f $ x)
+            fun rhs sel = sel $ x
+            fun eq sel = (lhs sel, rhs sel)
+            fun is_n i = i = n
+            val props =
+              sels_dummy ~~ (0 upto len - 1)
+              |> filter_out (is_n o snd)
+              |> map (HOLogic.mk_Trueprop o mk_eq_dummy o eq o fst)
+              |> Syntax.check_terms ctxt'
+          in
+            if length props > 0 then
+              Goal.prove_common ctxt' (SOME ~1) [] [] props tac
+              |> Variable.export ctxt' ctxt
+            else
+              []
+          end
+
+        val upd_comp_thm =
+          let
+            val ([f, g, x], ctxt') = Variable.add_fixes ["f", "g", "x"] ctxt
+            val f = Free (f, dummyT)
+            val g = Free (g, dummyT)
+            val x = Free (x, dummyT)
 
-    val lthy' =
-      Local_Theory.map_background_naming (Name_Space.qualified_path false (Binding.name short_name)) lthy
+            val lhs = t_dummy $ f $ (t_dummy $ g $ x)
+            val rhs = t_dummy $ Abs ("a", dummyT, f $ (g $ Bound 0)) $ x
+            val prop = Syntax.check_term ctxt' (HOLogic.mk_Trueprop (mk_eq_dummy (lhs, rhs)))
+          in
+            [Goal.prove_future ctxt' [] [] prop tac]
+            |> Variable.export ctxt' ctxt
+          end
+
+        val upd_comm_thms =
+          let
+            fun prop i ctxt =
+              let
+                val ([f, g, x], ctxt') = Variable.variant_fixes ["f", "g", "x"] ctxt
+                val self = t_dummy $ Free (f, dummyT)
+                val other = dummify (nth ts i) $ Free (g, dummyT)
+                val lhs = other $ (self $ Free (x, dummyT))
+                val rhs = self $ (other $ Free (x, dummyT))
+              in
+                (HOLogic.mk_Trueprop (mk_eq_dummy (lhs, rhs)), ctxt')
+              end
+            val (props, ctxt') = fold_map prop (0 upto n - 1) ctxt
+            val props = Syntax.check_terms ctxt' props
+          in
+            if length props > 0 then
+              Goal.prove_common ctxt' (SOME ~1) [] [] props tac
+              |> Variable.export ctxt' ctxt
+            else
+              []
+          end
+
+        val upd_sel_thm =
+          let
+            val ([x], ctxt') = Variable.add_fixes ["x"] ctxt
+
+            val lhs = t_dummy $ Abs("_", dummyT, (sel_dummy $ Free(x, dummyT))) $ Free (x, dummyT)
+            val rhs = Free (x, dummyT)
+            val prop = Syntax.check_term ctxt (HOLogic.mk_Trueprop (mk_eq_dummy (lhs, rhs)))
+          in
+            [Goal.prove_future ctxt [] [] prop tac]
+            |> Variable.export ctxt' ctxt
+          end
+      in
+        sel_upd_same_thm @ sel_upd_diff_thms @ upd_comp_thm @ upd_comm_thms @ upd_sel_thm
+      end
+
+    fun define name t =
+      Local_Theory.define ((name, NoSyn), ((Binding.empty, @{attributes [datatype_record_update, code]}),t))
+      #> apfst (apsnd snd)
+
+    val (updates, (lthy'', lthy')) =
+      lthy
+      |> Local_Theory.open_target
+      |> snd
+      |> Local_Theory.map_background_naming (Name_Space.qualified_path false (Binding.name short_name))
+      |> @{fold_map 2} define (map mk_name sels) (Syntax.check_terms lthy (map mk_t (0 upto len - 1)))
+      ||> `Local_Theory.close_target
+
+    val phi = Proof_Context.export_morphism lthy' lthy''
+
+    val (update_ts, update_defs) =
+      split_list updates
+      |>> map (Morphism.term phi)
+      ||> map (Morphism.thm phi)
+
+    val thms = flat (map (prove lthy'' update_defs update_ts) (0 upto len-1))
 
     fun insert sel =
       Symtab.insert op = (fst (dest_Const sel), Local_Theory.full_name lthy' (mk_name sel))
   in
-    lthy'
-    |> @{fold 2} define (map mk_name sels) (Syntax.check_terms lthy (map mk_t (0 upto len - 1)))
+    lthy''
+    |> Local_Theory.map_background_naming (Name_Space.mandatory_path short_name)
+    |> Local_Theory.note (thms_binding, thms)
+    |> snd
+    |> Local_Theory.restore_background_naming lthy
     |> Local_Theory.background_theory (Data.map (fold insert sels))
-    |> Local_Theory.restore_background_naming lthy
   end
 
-fun bnf_record binding opts tyargs args lthy =
+fun record binding opts tyargs args lthy =
   let
     val constructor =
       (((Binding.empty, Binding.map_name (fn c => "make_" ^ c) binding), args), NoSyn)
@@ -93,8 +224,8 @@
     lthy'
   end
 
-fun bnf_record_cmd binding opts tyargs args lthy =
-  bnf_record binding (opts lthy)
+fun record_cmd binding opts tyargs args lthy =
+  record binding (opts lthy)
     (map (apsnd (apfst (Syntax.parse_typ lthy) o apsnd (Typedecl.read_constraint lthy))) tyargs)
     (map (apsnd (Syntax.parse_typ lthy)) args) lthy
 
@@ -172,7 +303,7 @@
     @{command_keyword datatype_record}
     "Defines a record based on the BNF/datatype machinery"
     (parser >> (fn (((ctr_options, tyargs), binding), args) =>
-      bnf_record_cmd binding ctr_options tyargs args))
+      record_cmd binding ctr_options tyargs args))
 
 val setup =
    (Sign.parse_translation
diff -r 5cbd9cda7626 -r f3763989d589 src/HOL/ex/Datatype_Record_Examples.thy
--- a/src/HOL/ex/Datatype_Record_Examples.thy	Sun Jul 29 13:18:10 2018 +0200
+++ b/src/HOL/ex/Datatype_Record_Examples.thy	Sun Jul 29 18:24:47 2018 +0200
@@ -45,4 +45,23 @@
 lemma "b_set \<lparr> field_1 = True, field_2 = False \<rparr> = {False}"
   by simp
 
+text \<open>More tests\<close>
+
+datatype_record ('a, 'b) test1 =
+  field_t11 :: 'a
+  field_t12 :: 'b
+  field_t13 :: nat
+  field_t14 :: int
+
+thm test1.record_simps
+
+definition ID where "ID x = x"
+lemma ID_cong[cong]: "ID x = ID x" by (rule refl)
+
+lemma "update_field_t11 f (update_field_t12 g (update_field_t11 h x)) = ID (update_field_t12 g (update_field_t11 (\<lambda>x. f (h x)) x))"
+  apply (simp only: test1.record_simps)
+  apply (subst ID_def)
+  apply (rule refl)
+  done
+
 end
\ No newline at end of file