merged
authorwenzelm
Sun Jul 29 18:24:47 2018 +0200 (15 months ago ago)
changeset 68706f3763989d589
parent 68705 5cbd9cda7626
parent 68688 3a58abb11840
child 68707 5b269897df9d
merged
NEWS
     1.1 --- a/CONTRIBUTORS	Sun Jul 29 13:18:10 2018 +0200
     1.2 +++ b/CONTRIBUTORS	Sun Jul 29 18:24:47 2018 +0200
     1.3 @@ -3,6 +3,10 @@
     1.4  listed as an author in one of the source files of this Isabelle distribution.
     1.5  
     1.6  
     1.7 +Contributions to this Isabelle version
     1.8 +--------------------------------------
     1.9 +
    1.10 +
    1.11  Contributions to Isabelle2018
    1.12  -----------------------------
    1.13  
     2.1 --- a/NEWS	Sun Jul 29 13:18:10 2018 +0200
     2.2 +++ b/NEWS	Sun Jul 29 18:24:47 2018 +0200
     2.3 @@ -4,6 +4,11 @@
     2.4  (Note: Isabelle/jEdit shows a tree-view of the NEWS file in Sidekick.)
     2.5  
     2.6  
     2.7 +New in this Isabelle version
     2.8 +----------------------------
     2.9 +
    2.10 +
    2.11 +
    2.12  New in Isabelle2018 (August 2018)
    2.13  ---------------------------------
    2.14  
     3.1 --- a/src/HOL/Algebra/AbelCoset.thy	Sun Jul 29 13:18:10 2018 +0200
     3.2 +++ b/src/HOL/Algebra/AbelCoset.thy	Sun Jul 29 18:24:47 2018 +0200
     3.3 @@ -269,17 +269,15 @@
     3.4      by (rule a_comm_group)
     3.5    interpret subgroup "H" "(add_monoid G)"
     3.6      by (rule a_subgroup)
     3.7 -
     3.8 -  show "abelian_subgroup H G"
     3.9 -    apply unfold_locales
    3.10 -  proof (simp add: r_coset_def l_coset_def, clarsimp)
    3.11 -    fix x
    3.12 -    assume xcarr: "x \<in> carrier G"
    3.13 -    from a_subgroup have Hcarr: "H \<subseteq> carrier G"
    3.14 -      unfolding subgroup_def by simp
    3.15 -    from xcarr Hcarr show "(\<Union>h\<in>H. {h \<oplus>\<^bsub>G\<^esub> x}) = (\<Union>h\<in>H. {x \<oplus>\<^bsub>G\<^esub> h})"
    3.16 +  have "(\<Union>xa\<in>H. {xa \<oplus> x}) = (\<Union>xa\<in>H. {x \<oplus> xa})" if "x \<in> carrier G" for x
    3.17 +  proof -
    3.18 +    have "H \<subseteq> carrier G"
    3.19 +      using a_subgroup that unfolding subgroup_def by simp
    3.20 +    with that show "(\<Union>h\<in>H. {h \<oplus>\<^bsub>G\<^esub> x}) = (\<Union>h\<in>H. {x \<oplus>\<^bsub>G\<^esub> h})"
    3.21        using m_comm [simplified] by fastforce
    3.22    qed
    3.23 +  then show "abelian_subgroup H G"
    3.24 +    by unfold_locales (auto simp: r_coset_def l_coset_def)
    3.25  qed
    3.26  
    3.27  lemma abelian_subgroupI3:
    3.28 @@ -304,14 +302,6 @@
    3.29  by (rule normal.inv_op_closed2 [OF a_normal,
    3.30      folded a_inv_def, simplified monoid_record_simps])
    3.31  
    3.32 -text\<open>Alternative characterization of normal subgroups\<close>
    3.33 -lemma (in abelian_group) a_normal_inv_iff:
    3.34 -     "(N \<lhd> (add_monoid G)) = 
    3.35 -      (subgroup N (add_monoid G) & (\<forall>x \<in> carrier G. \<forall>h \<in> N. x \<oplus> h \<oplus> (\<ominus> x) \<in> N))"
    3.36 -      (is "_ = ?rhs")
    3.37 -by (rule group.normal_inv_iff [OF a_group,
    3.38 -    folded a_inv_def, simplified monoid_record_simps])
    3.39 -
    3.40  lemma (in abelian_group) a_lcos_m_assoc:
    3.41    "\<lbrakk> M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G \<rbrakk> \<Longrightarrow> g <+ (h <+ M) = (g \<oplus> h) <+ M"
    3.42  by (rule group.lcos_m_assoc [OF a_group,
    3.43 @@ -322,13 +312,11 @@
    3.44  by (rule group.lcos_mult_one [OF a_group,
    3.45      folded a_l_coset_def, simplified monoid_record_simps])
    3.46  
    3.47 -
    3.48  lemma (in abelian_group) a_l_coset_subset_G:
    3.49    "\<lbrakk> H \<subseteq> carrier G; x \<in> carrier G \<rbrakk> \<Longrightarrow> x <+ H \<subseteq> carrier G"
    3.50  by (rule group.l_coset_subset_G [OF a_group,
    3.51      folded a_l_coset_def, simplified monoid_record_simps])
    3.52  
    3.53 -
    3.54  lemma (in abelian_group) a_l_coset_swap:
    3.55       "\<lbrakk>y \<in> x <+ H;  x \<in> carrier G;  subgroup H (add_monoid G)\<rbrakk> \<Longrightarrow> x \<in> y <+ H"
    3.56  by (rule group.l_coset_swap [OF a_group,
    3.57 @@ -498,15 +486,15 @@
    3.58  
    3.59  text \<open>Since the Factorization is based on an \emph{abelian} subgroup, is results in 
    3.60          a commutative group\<close>
    3.61 -theorem (in abelian_subgroup) a_factorgroup_is_comm_group:
    3.62 -  "comm_group (G A_Mod H)"
    3.63 -apply (intro comm_group.intro comm_monoid.intro) prefer 3
    3.64 -  apply (rule a_factorgroup_is_group)
    3.65 - apply (rule group.axioms[OF a_factorgroup_is_group])
    3.66 -apply (rule comm_monoid_axioms.intro)
    3.67 -apply (unfold A_FactGroup_def FactGroup_def RCOSETS_def, fold set_add_def a_r_coset_def, clarsimp)
    3.68 -apply (simp add: a_rcos_sum a_comm)
    3.69 -done
    3.70 +theorem (in abelian_subgroup) a_factorgroup_is_comm_group: "comm_group (G A_Mod H)"
    3.71 +proof -
    3.72 +  have "Group.comm_monoid_axioms (G A_Mod H)"
    3.73 +    apply (rule comm_monoid_axioms.intro)
    3.74 +    apply (auto simp: A_FactGroup_def FactGroup_def RCOSETS_def a_normal add.m_comm normal.rcos_sum)
    3.75 +    done
    3.76 +  then show ?thesis
    3.77 +    by (intro comm_group.intro comm_monoid.intro) (simp_all add: a_factorgroup_is_group group.is_monoid)
    3.78 +qed
    3.79  
    3.80  lemma add_A_FactGroup [simp]: "X \<otimes>\<^bsub>(G A_Mod H)\<^esub> X' = X <+>\<^bsub>G\<^esub> X'"
    3.81  by (simp add: A_FactGroup_def set_add_def)
    3.82 @@ -552,11 +540,8 @@
    3.83    interpret G: abelian_group G by fact
    3.84    interpret H: abelian_group H by fact
    3.85    show ?thesis
    3.86 -    apply (intro abelian_group_hom.intro abelian_group_hom_axioms.intro)
    3.87 -      apply fact
    3.88 -     apply fact
    3.89 -    apply (rule a_group_hom)
    3.90 -    done
    3.91 +    by (intro abelian_group_hom.intro abelian_group_hom_axioms.intro 
    3.92 +        G.abelian_group_axioms H.abelian_group_axioms a_group_hom)
    3.93  qed
    3.94  
    3.95  lemma (in abelian_group_hom) is_abelian_group_hom:
    3.96 @@ -576,8 +561,7 @@
    3.97  
    3.98  lemma (in abelian_group_hom) zero_closed [simp]:
    3.99    "h \<zero> \<in> carrier H"
   3.100 -by (rule group_hom.one_closed[OF a_group_hom,
   3.101 -    simplified ring_record_simps])
   3.102 +  by simp
   3.103  
   3.104  lemma (in abelian_group_hom) hom_zero [simp]:
   3.105    "h \<zero> = \<zero>\<^bsub>H\<^esub>"
   3.106 @@ -586,8 +570,7 @@
   3.107  
   3.108  lemma (in abelian_group_hom) a_inv_closed [simp]:
   3.109    "x \<in> carrier G ==> h (\<ominus>x) \<in> carrier H"
   3.110 -by (rule group_hom.inv_closed[OF a_group_hom,
   3.111 -    folded a_inv_def, simplified ring_record_simps])
   3.112 +  by simp
   3.113  
   3.114  lemma (in abelian_group_hom) hom_a_inv [simp]:
   3.115    "x \<in> carrier G ==> h (\<ominus>x) = \<ominus>\<^bsub>H\<^esub> (h x)"
   3.116 @@ -596,19 +579,15 @@
   3.117  
   3.118  lemma (in abelian_group_hom) additive_subgroup_a_kernel:
   3.119    "additive_subgroup (a_kernel G H h) G"
   3.120 -apply (rule additive_subgroup.intro)
   3.121 -apply (rule group_hom.subgroup_kernel[OF a_group_hom,
   3.122 -       folded a_kernel_def, simplified ring_record_simps])
   3.123 -done
   3.124 +  by (simp add: additive_subgroup.intro a_group_hom a_kernel_def group_hom.subgroup_kernel)
   3.125  
   3.126  text\<open>The kernel of a homomorphism is an abelian subgroup\<close>
   3.127  lemma (in abelian_group_hom) abelian_subgroup_a_kernel:
   3.128    "abelian_subgroup (a_kernel G H h) G"
   3.129 -apply (rule abelian_subgroupI)
   3.130 -apply (rule group_hom.normal_kernel[OF a_group_hom,
   3.131 -       folded a_kernel_def, simplified ring_record_simps])
   3.132 -apply (simp add: G.a_comm)
   3.133 -done
   3.134 +  apply (rule abelian_subgroupI)
   3.135 +   apply (simp add: G.abelian_group_axioms abelian_subgroup.a_normal abelian_subgroupI3 additive_subgroup_a_kernel)
   3.136 +  apply (simp add: G.a_comm)
   3.137 +  done
   3.138  
   3.139  lemma (in abelian_group_hom) A_FactGroup_nonempty:
   3.140    assumes X: "X \<in> carrier (G A_Mod a_kernel G H h)"
   3.141 @@ -715,48 +694,34 @@
   3.142  qed
   3.143  
   3.144  lemma (in abelian_subgroup) a_repr_independence':
   3.145 -  assumes y: "y \<in> H +> x"
   3.146 -      and xcarr: "x \<in> carrier G"
   3.147 +  assumes "y \<in> H +> x" "x \<in> carrier G"
   3.148    shows "H +> x = H +> y"
   3.149 -  apply (rule a_repr_independence)
   3.150 -    apply (rule y)
   3.151 -   apply (rule xcarr)
   3.152 -  apply (rule a_subgroup)
   3.153 -  done
   3.154 +  using a_repr_independence a_subgroup assms by blast
   3.155  
   3.156  lemma (in abelian_subgroup) a_repr_independenceD:
   3.157 -  assumes ycarr: "y \<in> carrier G"
   3.158 -      and repr:  "H +> x = H +> y"
   3.159 +  assumes "y \<in> carrier G" "H +> x = H +> y"
   3.160    shows "y \<in> H +> x"
   3.161 -by (rule group.repr_independenceD [OF a_group a_subgroup,
   3.162 -    folded a_r_coset_def, simplified monoid_record_simps]) (rule ycarr, rule repr)
   3.163 +  by (simp add: a_rcos_self assms)
   3.164  
   3.165  
   3.166  lemma (in abelian_subgroup) a_rcosets_carrier:
   3.167    "X \<in> a_rcosets H \<Longrightarrow> X \<subseteq> carrier G"
   3.168 -by (rule subgroup.rcosets_carrier [OF a_subgroup a_group,
   3.169 -    folded A_RCOSETS_def, simplified monoid_record_simps])
   3.170 +  using a_rcosets_part_G by auto
   3.171  
   3.172  
   3.173  subsubsection \<open>Addition of Subgroups\<close>
   3.174  
   3.175  lemma (in abelian_monoid) set_add_closed:
   3.176 -  assumes Acarr: "A \<subseteq> carrier G"
   3.177 -      and Bcarr: "B \<subseteq> carrier G"
   3.178 +  assumes "A \<subseteq> carrier G" "B \<subseteq> carrier G"
   3.179    shows "A <+> B \<subseteq> carrier G"
   3.180 -by (rule monoid.set_mult_closed [OF a_monoid,
   3.181 -    folded set_add_def, simplified monoid_record_simps]) (rule Acarr, rule Bcarr)
   3.182 +  by (simp add: assms add.set_mult_closed set_add_defs(1))
   3.183  
   3.184  lemma (in abelian_group) add_additive_subgroups:
   3.185    assumes subH: "additive_subgroup H G"
   3.186 -      and subK: "additive_subgroup K G"
   3.187 +    and subK: "additive_subgroup K G"
   3.188    shows "additive_subgroup (H <+> K) G"
   3.189 -apply (rule additive_subgroup.intro)
   3.190 -apply (unfold set_add_def)
   3.191 -apply (intro comm_group.mult_subgroups)
   3.192 -  apply (rule a_comm_group)
   3.193 - apply (rule additive_subgroup.a_subgroup[OF subH])
   3.194 -apply (rule additive_subgroup.a_subgroup[OF subK])
   3.195 -done
   3.196 +  unfolding set_add_def
   3.197 +  using add.mult_subgroups additive_subgroup_def subH subK
   3.198 +  by (blast intro: additive_subgroup.intro)
   3.199  
   3.200  end
     4.1 --- a/src/HOL/Algebra/Bij.thy	Sun Jul 29 13:18:10 2018 +0200
     4.2 +++ b/src/HOL/Algebra/Bij.thy	Sun Jul 29 18:24:47 2018 +0200
     4.3 @@ -46,15 +46,11 @@
     4.4    by (simp add: Bij_def compose_inv_into_id)
     4.5  
     4.6  theorem group_BijGroup: "group (BijGroup S)"
     4.7 -apply (simp add: BijGroup_def)
     4.8 -apply (rule groupI)
     4.9 -    apply (simp add: compose_Bij)
    4.10 -   apply (simp add: id_Bij)
    4.11 -  apply (simp add: compose_Bij)
    4.12 -  apply (blast intro: compose_assoc [symmetric] dest: Bij_imp_funcset)
    4.13 - apply (simp add: id_Bij Bij_imp_funcset Bij_imp_extensional, simp)
    4.14 -apply (blast intro: Bij_compose_restrict_eq restrict_inv_into_Bij)
    4.15 -done
    4.16 +  apply (simp add: BijGroup_def)
    4.17 +  apply (rule groupI)
    4.18 +      apply (auto simp: compose_Bij id_Bij Bij_imp_funcset Bij_imp_extensional compose_assoc [symmetric])
    4.19 +  apply (blast intro: Bij_compose_restrict_eq restrict_inv_into_Bij)
    4.20 +  done
    4.21  
    4.22  
    4.23  subsection\<open>Automorphisms Form a Group\<close>
    4.24 @@ -63,13 +59,18 @@
    4.25  by (simp add: Bij_def bij_betw_def inv_into_into)
    4.26  
    4.27  lemma Bij_inv_into_lemma:
    4.28 - assumes eq: "\<And>x y. \<lbrakk>x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> h(g x y) = g (h x) (h y)"
    4.29 - shows "\<lbrakk>h \<in> Bij S;  g \<in> S \<rightarrow> S \<rightarrow> S;  x \<in> S;  y \<in> S\<rbrakk>
    4.30 -        \<Longrightarrow> inv_into S h (g x y) = g (inv_into S h x) (inv_into S h y)"
    4.31 -apply (simp add: Bij_def bij_betw_def)
    4.32 -apply (subgoal_tac "\<exists>x'\<in>S. \<exists>y'\<in>S. x = h x' \<and> y = h y'", clarify)
    4.33 - apply (simp add: eq [symmetric] inv_f_f funcset_mem [THEN funcset_mem], blast)
    4.34 -done
    4.35 +  assumes eq: "\<And>x y. \<lbrakk>x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> h(g x y) = g (h x) (h y)"
    4.36 +      and hg: "h \<in> Bij S" "g \<in> S \<rightarrow> S \<rightarrow> S" and "x \<in> S" "y \<in> S"
    4.37 +  shows "inv_into S h (g x y) = g (inv_into S h x) (inv_into S h y)"
    4.38 +proof -
    4.39 +  have "h ` S = S"
    4.40 +    by (metis (no_types) Bij_def Int_iff assms(2) bij_betw_def mem_Collect_eq)
    4.41 +  with \<open>x \<in> S\<close> \<open>y \<in> S\<close> have "\<exists>x'\<in>S. \<exists>y'\<in>S. x = h x' \<and> y = h y'"
    4.42 +    by auto
    4.43 +  then show ?thesis
    4.44 +    using assms
    4.45 +    by (auto simp add: Bij_def bij_betw_def eq [symmetric] inv_f_f funcset_mem [THEN funcset_mem])
    4.46 +qed
    4.47  
    4.48  
    4.49  definition
    4.50 @@ -94,8 +95,7 @@
    4.51  
    4.52  lemma inv_BijGroup:
    4.53       "f \<in> Bij S \<Longrightarrow> m_inv (BijGroup S) f = (\<lambda>x \<in> S. (inv_into S f) x)"
    4.54 -apply (rule group.inv_equality)
    4.55 -apply (rule group_BijGroup)
    4.56 +apply (rule group.inv_equality [OF group_BijGroup])
    4.57  apply (simp_all add:BijGroup_def restrict_inv_into_Bij Bij_compose_restrict_eq)
    4.58  done
    4.59  
     5.1 --- a/src/HOL/Algebra/Complete_Lattice.thy	Sun Jul 29 13:18:10 2018 +0200
     5.2 +++ b/src/HOL/Algebra/Complete_Lattice.thy	Sun Jul 29 18:24:47 2018 +0200
     5.3 @@ -680,22 +680,25 @@
     5.4      next
     5.5        case False
     5.6        show ?thesis
     5.7 -      proof (rule_tac x="\<Squnion>\<^bsub>L\<^esub> A" in exI, rule least_UpperI, simp_all)
     5.8 +      proof (intro exI least_UpperI, simp_all)
     5.9          show b:"\<And> x. x \<in> A \<Longrightarrow> x \<sqsubseteq>\<^bsub>L\<^esub> \<Squnion>\<^bsub>L\<^esub>A"
    5.10            using a by (auto intro: L.sup_upper, meson L.at_least_at_most_closed L.sup_upper subset_trans)
    5.11          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"
    5.12            using a L.at_least_at_most_closed by (rule_tac L.sup_least, auto intro: funcset_mem simp add: Upper_def)
    5.13 -        from a show "A \<subseteq> \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>"
    5.14 -          by (auto)
    5.15 -        from a show "\<Squnion>\<^bsub>L\<^esub>A \<in> \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>"
    5.16 -          apply (rule_tac L.at_least_at_most_member)
    5.17 -          apply (auto)
    5.18 -          apply (meson L.at_least_at_most_closed L.sup_closed subset_trans)
    5.19 -          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)
    5.20 -          apply (rule L.sup_least)
    5.21 -          apply (auto simp add: assms)
    5.22 -          using L.at_least_at_most_closed apply blast
    5.23 -        done
    5.24 +        from a show *: "A \<subseteq> \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>"
    5.25 +          by auto
    5.26 +        show "\<Squnion>\<^bsub>L\<^esub>A \<in> \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>"
    5.27 +        proof (rule_tac L.at_least_at_most_member)
    5.28 +          show 1: "\<Squnion>\<^bsub>L\<^esub>A \<in> carrier L"
    5.29 +            by (meson L.at_least_at_most_closed L.sup_closed subset_trans *)
    5.30 +          show "a \<sqsubseteq>\<^bsub>L\<^esub> \<Squnion>\<^bsub>L\<^esub>A"
    5.31 +            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)
    5.32 +          show "\<Squnion>\<^bsub>L\<^esub>A \<sqsubseteq>\<^bsub>L\<^esub> b"
    5.33 +          proof (rule L.sup_least)
    5.34 +            show "A \<subseteq> carrier L" "\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq>\<^bsub>L\<^esub> b"
    5.35 +              using * L.at_least_at_most_closed by blast+
    5.36 +          qed (simp add: assms)
    5.37 +        qed
    5.38        qed
    5.39      qed
    5.40      show "\<exists>s. is_glb (L\<lparr>carrier := \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>\<rparr>) s A"
    5.41 @@ -711,15 +714,17 @@
    5.42            using a L.at_least_at_most_closed by (force intro!: L.inf_lower)
    5.43          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"
    5.44             using a L.at_least_at_most_closed by (rule_tac L.inf_greatest, auto intro: funcset_carrier' simp add: Lower_def)
    5.45 -        from a show "A \<subseteq> \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>"
    5.46 -          by (auto)
    5.47 -        from a show "\<Sqinter>\<^bsub>L\<^esub>A \<in> \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>"
    5.48 -          apply (rule_tac L.at_least_at_most_member)
    5.49 -          apply (auto)
    5.50 -          apply (meson L.at_least_at_most_closed L.inf_closed subset_trans)
    5.51 -          apply (meson L.at_least_at_most_closed L.at_least_at_most_lower L.inf_greatest assms(2) set_rev_mp subset_trans)
    5.52 -          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)            
    5.53 -        done
    5.54 +        from a show *: "A \<subseteq> \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>"
    5.55 +          by auto
    5.56 +        show "\<Sqinter>\<^bsub>L\<^esub>A \<in> \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>"
    5.57 +        proof (rule_tac L.at_least_at_most_member)
    5.58 +          show 1: "\<Sqinter>\<^bsub>L\<^esub>A \<in> carrier L"
    5.59 +            by (meson "*" L.at_least_at_most_closed L.inf_closed subset_trans)
    5.60 +          show "a \<sqsubseteq>\<^bsub>L\<^esub> \<Sqinter>\<^bsub>L\<^esub>A"
    5.61 +            by (meson "*" L.at_least_at_most_closed L.at_least_at_most_lower L.inf_greatest assms(2) subsetD subset_trans)
    5.62 +          show "\<Sqinter>\<^bsub>L\<^esub>A \<sqsubseteq>\<^bsub>L\<^esub> b"
    5.63 +            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)
    5.64 +        qed
    5.65        qed
    5.66      qed
    5.67    qed
    5.68 @@ -731,7 +736,7 @@
    5.69  text \<open>The set of fixed points of a complete lattice is itself a complete lattice\<close>
    5.70  
    5.71  theorem Knaster_Tarski:
    5.72 -  assumes "weak_complete_lattice L" "f \<in> carrier L \<rightarrow> carrier L" "isotone L L f"
    5.73 +  assumes "weak_complete_lattice L" and f: "f \<in> carrier L \<rightarrow> carrier L" and "isotone L L f"
    5.74    shows "weak_complete_lattice (fpl L f)" (is "weak_complete_lattice ?L'")
    5.75  proof -
    5.76    interpret L: weak_complete_lattice L
    5.77 @@ -805,15 +810,14 @@
    5.78        show "is_lub ?L'' (LFP\<^bsub>?L'\<^esub> f) A"
    5.79        proof (rule least_UpperI, simp_all)
    5.80          fix x
    5.81 -        assume "x \<in> Upper ?L'' A"
    5.82 -        hence "LFP\<^bsub>?L'\<^esub> f \<sqsubseteq>\<^bsub>?L'\<^esub> x"
    5.83 -          apply (rule_tac L'.LFP_lowerbound)
    5.84 -          apply (auto simp add: Upper_def)
    5.85 -          apply (simp add: A AL L.at_least_at_most_member L.sup_least set_rev_mp)          
    5.86 -          apply (simp add: Pi_iff assms(2) fps_def, rule_tac L.weak_refl)
    5.87 -          apply (auto)
    5.88 -          apply (rule funcset_mem[of f "carrier L"], simp_all add: assms(2))
    5.89 -        done
    5.90 +        assume x: "x \<in> Upper ?L'' A"
    5.91 +        have "LFP\<^bsub>?L'\<^esub> f \<sqsubseteq>\<^bsub>?L'\<^esub> x"
    5.92 +        proof (rule L'.LFP_lowerbound, simp_all)
    5.93 +          show "x \<in> \<lbrace>\<Squnion>\<^bsub>L\<^esub>A..\<top>\<^bsub>L\<^esub>\<rbrace>\<^bsub>L\<^esub>"
    5.94 +            using x by (auto simp add: Upper_def A AL L.at_least_at_most_member L.sup_least set_rev_mp)    
    5.95 +          with x show "f x \<sqsubseteq>\<^bsub>L\<^esub> x"
    5.96 +            by (simp add: Upper_def) (meson L.at_least_at_most_closed L.use_fps L.weak_refl subsetD f_top_chain imageI)
    5.97 +        qed
    5.98          thus " LFP\<^bsub>?L'\<^esub> f \<sqsubseteq>\<^bsub>L\<^esub> x"
    5.99            by (simp)
   5.100        next
   5.101 @@ -838,17 +842,13 @@
   5.102               by (auto simp add: at_least_at_most_def)
   5.103            have "LFP\<^bsub>?L'\<^esub> f .=\<^bsub>?L'\<^esub> f (LFP\<^bsub>?L'\<^esub> f)"
   5.104            proof (rule "L'.LFP_weak_unfold", simp_all)
   5.105 -            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>"
   5.106 -              apply (auto simp add: Pi_def at_least_at_most_def)
   5.107 -              using assms(2) apply blast
   5.108 -              apply (meson AL funcset_mem L.le_trans L.sup_closed assms(2) assms(3) pf_w use_iso2)
   5.109 -              using assms(2) apply blast
   5.110 -            done
   5.111 -            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"
   5.112 -              apply (auto simp add: isotone_def)
   5.113 -              using L'.weak_partial_order_axioms apply blast
   5.114 -              apply (meson L.at_least_at_most_closed subsetCE)
   5.115 -            done
   5.116 +            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"
   5.117 +              by (meson AL funcset_mem L.le_trans L.sup_closed assms(2) assms(3) pf_w use_iso2)
   5.118 +            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>"
   5.119 +              by (auto simp add: Pi_def at_least_at_most_def)
   5.120 +            show "Mono\<^bsub>L\<lparr>carrier := \<lbrace>\<Squnion>\<^bsub>L\<^esub>A..\<top>\<^bsub>L\<^esub>\<rbrace>\<^bsub>L\<^esub>\<rparr>\<^esub> f"
   5.121 +              using L'.weak_partial_order_axioms assms(3) 
   5.122 +              by (auto simp add: isotone_def) (meson L.at_least_at_most_closed subsetCE)
   5.123            qed
   5.124            thus "f (LFP\<^bsub>?L'\<^esub> f) .=\<^bsub>L\<^esub> LFP\<^bsub>?L'\<^esub> f"
   5.125              by (simp add: L.equivalence_axioms funcset_carrier' c assms(2) equivalence.sym) 
   5.126 @@ -889,7 +889,6 @@
   5.127            thus ?thesis
   5.128              by (meson AL L.inf_closed L.le_trans assms(3) b(1) b(2) fx use_iso2 w)
   5.129          qed
   5.130 -   
   5.131          show "\<bottom>\<^bsub>L\<^esub> \<sqsubseteq>\<^bsub>L\<^esub> f x"
   5.132            by (simp add: fx)
   5.133        qed
   5.134 @@ -905,12 +904,16 @@
   5.135        proof (rule greatest_LowerI, simp_all)
   5.136          fix x
   5.137          assume "x \<in> Lower ?L'' A"
   5.138 -        hence "x \<sqsubseteq>\<^bsub>?L'\<^esub> GFP\<^bsub>?L'\<^esub> f"
   5.139 -          apply (rule_tac L'.GFP_upperbound)
   5.140 -          apply (auto simp add: Lower_def)
   5.141 -          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)
   5.142 -          apply (simp add: funcset_carrier' L.sym assms(2) fps_def)          
   5.143 -        done
   5.144 +        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"
   5.145 +          by (auto simp add: Lower_def)
   5.146 +        have "x \<sqsubseteq>\<^bsub>?L'\<^esub> GFP\<^bsub>?L'\<^esub> f"
   5.147 +          unfolding Lower_def
   5.148 +        proof (rule_tac L'.GFP_upperbound; simp)
   5.149 +          show "x \<in> \<lbrace>\<bottom>\<^bsub>L\<^esub>..\<Sqinter>\<^bsub>L\<^esub>A\<rbrace>\<^bsub>L\<^esub>"
   5.150 +            by (meson x A AL L.at_least_at_most_member L.bottom_lower L.inf_greatest contra_subsetD fps_carrier)
   5.151 +          show "x \<sqsubseteq>\<^bsub>L\<^esub> f x"
   5.152 +            using x by (simp add: funcset_carrier' L.sym assms(2) fps_def)
   5.153 +        qed
   5.154          thus "x \<sqsubseteq>\<^bsub>L\<^esub> GFP\<^bsub>?L'\<^esub> f"
   5.155            by (simp)
   5.156        next
   5.157 @@ -935,17 +938,14 @@
   5.158               by (auto simp add: at_least_at_most_def)
   5.159            have "GFP\<^bsub>?L'\<^esub> f .=\<^bsub>?L'\<^esub> f (GFP\<^bsub>?L'\<^esub> f)"
   5.160            proof (rule "L'.GFP_weak_unfold", simp_all)
   5.161 -            show "f \<in> \<lbrace>\<bottom>\<^bsub>L\<^esub>..?w\<rbrace>\<^bsub>L\<^esub> \<rightarrow> \<lbrace>\<bottom>\<^bsub>L\<^esub>..?w\<rbrace>\<^bsub>L\<^esub>"
   5.162 -              apply (auto simp add: Pi_def at_least_at_most_def)
   5.163 -              using assms(2) apply blast
   5.164 -              apply (simp add: funcset_carrier' assms(2))
   5.165 -              apply (meson AL funcset_carrier L.inf_closed L.le_trans assms(2) assms(3) pf_w use_iso2)
   5.166 -            done
   5.167 -            from assms(3) show "Mono\<^bsub>L\<lparr>carrier := \<lbrace>\<bottom>\<^bsub>L\<^esub>..?w\<rbrace>\<^bsub>L\<^esub>\<rparr>\<^esub> f"
   5.168 -              apply (auto simp add: isotone_def)
   5.169 -              using L'.weak_partial_order_axioms apply blast
   5.170 -              using L.at_least_at_most_closed apply (blast intro: funcset_carrier')
   5.171 -            done
   5.172 +            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"
   5.173 +              by (meson AL funcset_carrier L.inf_closed L.le_trans assms(2) assms(3) pf_w use_iso2)
   5.174 +            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>"
   5.175 +              by (auto simp add: Pi_def at_least_at_most_def)
   5.176 +            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"
   5.177 +              by (meson L.at_least_at_most_closed subsetD use_iso1  assms(3)) 
   5.178 +            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"
   5.179 +              by (auto simp add: isotone_def)
   5.180            qed
   5.181            thus "f (GFP\<^bsub>?L'\<^esub> f) .=\<^bsub>L\<^esub> GFP\<^bsub>?L'\<^esub> f"
   5.182              by (simp add: L.equivalence_axioms funcset_carrier' c assms(2) equivalence.sym) 
   5.183 @@ -1117,17 +1117,16 @@
   5.184      qed
   5.185      show "\<Sqinter>\<^bsub>fpl L f\<^esub>A \<sqsubseteq>\<^bsub>L\<^esub> f (\<Sqinter>\<^bsub>L\<^esub>A)"
   5.186      proof -
   5.187 +      have *: "\<Sqinter>\<^bsub>fpl L f\<^esub>A \<in> carrier L"
   5.188 +        using FA infA by blast
   5.189        have "\<And>x. x \<in> A \<Longrightarrow> \<Sqinter>\<^bsub>fpl L f\<^esub>A \<sqsubseteq>\<^bsub>fpl L f\<^esub> x"
   5.190          by (rule L'.inf_lower, simp_all add: assms)
   5.191        hence "\<Sqinter>\<^bsub>fpl L f\<^esub>A \<sqsubseteq>\<^bsub>L\<^esub> (\<Sqinter>\<^bsub>L\<^esub>A)"
   5.192 -        apply (rule_tac L.inf_greatest, simp_all add: A)
   5.193 -        using FA infA apply blast
   5.194 -        done
   5.195 +        by (rule_tac L.inf_greatest, simp_all add: A *)
   5.196        hence 1:"f(\<Sqinter>\<^bsub>fpl L f\<^esub>A) \<sqsubseteq>\<^bsub>L\<^esub> f(\<Sqinter>\<^bsub>L\<^esub>A)"
   5.197          by (metis (no_types, lifting) A FA L.inf_closed assms(2) infA subsetCE use_iso1)
   5.198        have 2:"\<Sqinter>\<^bsub>fpl L f\<^esub>A \<sqsubseteq>\<^bsub>L\<^esub> f (\<Sqinter>\<^bsub>fpl L f\<^esub>A)"
   5.199          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)
   5.200 -        
   5.201        show ?thesis  
   5.202          using FA fA infA by (auto intro!: L.le_trans[OF 2 1] ic fc, metis FA PiE assms(4) subsetCE)
   5.203      qed
   5.204 @@ -1189,21 +1188,11 @@
   5.205  lemma sup_pres_is_join_pres:
   5.206    assumes "weak_sup_pres X Y f"
   5.207    shows "join_pres X Y f"
   5.208 -  using assms
   5.209 -  apply (simp add: join_pres_def weak_sup_pres_def, safe)
   5.210 -  apply (rename_tac x y)
   5.211 -  apply (drule_tac x="{x, y}" in spec)
   5.212 -  apply (auto simp add: join_def)
   5.213 -done
   5.214 +  using assms by (auto simp: join_pres_def weak_sup_pres_def join_def)
   5.215  
   5.216  lemma inf_pres_is_meet_pres:
   5.217    assumes "weak_inf_pres X Y f"
   5.218    shows "meet_pres X Y f"
   5.219 -  using assms
   5.220 -  apply (simp add: meet_pres_def weak_inf_pres_def, safe)
   5.221 -  apply (rename_tac x y)
   5.222 -  apply (drule_tac x="{x, y}" in spec)
   5.223 -  apply (auto simp add: meet_def)
   5.224 -done
   5.225 +  using assms by (auto simp: meet_pres_def weak_inf_pres_def meet_def)
   5.226  
   5.227  end
     6.1 --- a/src/HOL/Algebra/Coset.thy	Sun Jul 29 13:18:10 2018 +0200
     6.2 +++ b/src/HOL/Algebra/Coset.thy	Sun Jul 29 18:24:47 2018 +0200
     6.3 @@ -440,45 +440,36 @@
     6.4    shows "N \<lhd> G"
     6.5    using assms normal_inv_iff by blast
     6.6  
     6.7 -corollary (in group) normal_invE:
     6.8 -  assumes "N \<lhd> G"
     6.9 -  shows "subgroup N G" and "\<And>x h. \<lbrakk> x \<in> carrier G; h \<in> N \<rbrakk> \<Longrightarrow> x \<otimes> h \<otimes> inv x \<in> N"
    6.10 -  using assms normal_inv_iff apply blast
    6.11 -  by (simp add: assms normal.inv_op_closed2)
    6.12 -
    6.13 -
    6.14 -lemma (in group) one_is_normal :
    6.15 -   "{\<one>} \<lhd> G"
    6.16 -proof(intro normal_invI )
    6.17 +lemma (in group) one_is_normal: "{\<one>} \<lhd> G"
    6.18 +proof(intro normal_invI)
    6.19    show "subgroup {\<one>} G"
    6.20      by (simp add: subgroup_def)
    6.21 -  show "\<And>x h. x \<in> carrier G \<Longrightarrow> h \<in> {\<one>} \<Longrightarrow> x \<otimes> h \<otimes> inv x \<in> {\<one>}" by simp
    6.22 -qed
    6.23 +qed simp
    6.24  
    6.25  
    6.26  subsection\<open>More Properties of Left Cosets\<close>
    6.27  
    6.28  lemma (in group) l_repr_independence:
    6.29 -  assumes "y \<in> x <# H" "x \<in> carrier G" "subgroup H G"
    6.30 +  assumes "y \<in> x <# H" "x \<in> carrier G" and HG: "subgroup H G"
    6.31    shows "x <# H = y <# H"
    6.32  proof -
    6.33    obtain h' where h': "h' \<in> H" "y = x \<otimes> h'"
    6.34      using assms(1) unfolding l_coset_def by blast
    6.35    hence "x \<otimes> h = y \<otimes> ((inv h') \<otimes> h)" if "h \<in> H" for h
    6.36    proof -
    6.37 -    have f3: "h' \<in> carrier G"
    6.38 -      by (meson assms(3) h'(1) subgroup.mem_carrier)
    6.39 -    have f4: "h \<in> carrier G"
    6.40 -      by (meson assms(3) subgroup.mem_carrier that)
    6.41 -    then show ?thesis
    6.42 -      by (metis assms(2) f3 h'(2) inv_closed inv_solve_right m_assoc m_closed)
    6.43 +    have "h' \<in> carrier G"
    6.44 +      by (meson HG h'(1) subgroup.mem_carrier)
    6.45 +    moreover have "h \<in> carrier G"
    6.46 +      by (meson HG subgroup.mem_carrier that)
    6.47 +    ultimately show ?thesis
    6.48 +      by (metis assms(2) h'(2) inv_closed inv_solve_right m_assoc m_closed)
    6.49    qed
    6.50 -  hence "\<And> xh. xh \<in> x <# H \<Longrightarrow> xh \<in> y <# H"
    6.51 -    unfolding l_coset_def by (metis (no_types, lifting) UN_iff assms(3) h'(1) subgroup_def)
    6.52 -  moreover have "\<And> h. h \<in> H \<Longrightarrow> y \<otimes> h = x \<otimes> (h' \<otimes> h)"
    6.53 -    using h' by (meson assms(2) assms(3) m_assoc subgroup.mem_carrier)
    6.54 -  hence "\<And> yh. yh \<in> y <# H \<Longrightarrow> yh \<in> x <# H"
    6.55 -    unfolding l_coset_def using subgroup.m_closed[OF assms(3) h'(1)] by blast
    6.56 +  hence "\<And>xh. xh \<in> x <# H \<Longrightarrow> xh \<in> y <# H"
    6.57 +    unfolding l_coset_def by (metis (no_types, lifting) UN_iff HG h'(1) subgroup_def)
    6.58 +  moreover have "\<And>h. h \<in> H \<Longrightarrow> y \<otimes> h = x \<otimes> (h' \<otimes> h)"
    6.59 +    using h' by (meson assms(2) HG m_assoc subgroup.mem_carrier)
    6.60 +  hence "\<And>yh. yh \<in> y <# H \<Longrightarrow> yh \<in> x <# H"
    6.61 +    unfolding l_coset_def using subgroup.m_closed[OF HG h'(1)] by blast
    6.62    ultimately show ?thesis by blast
    6.63  qed
    6.64  
    6.65 @@ -655,8 +646,8 @@
    6.66    shows "hb \<otimes> a \<in> (\<Union>h\<in>H. {h \<otimes> b})"
    6.67  proof -
    6.68    interpret subgroup H G by fact
    6.69 -  from p show ?thesis apply (rule_tac UN_I [of "hb \<otimes> ((inv ha) \<otimes> h)"])
    6.70 -    apply blast by (simp add: inv_solve_left m_assoc)
    6.71 +  from p show ?thesis 
    6.72 +    by (rule_tac UN_I [of "hb \<otimes> ((inv ha) \<otimes> h)"]) (auto simp: inv_solve_left m_assoc)
    6.73  qed
    6.74  
    6.75  lemma (in group) rcos_disjoint:
    6.76 @@ -666,9 +657,8 @@
    6.77  proof -
    6.78    interpret subgroup H G by fact
    6.79    from p show ?thesis
    6.80 -    apply (simp add: RCOSETS_def r_coset_def)
    6.81 -    apply (blast intro: rcos_equation assms sym)
    6.82 -    done
    6.83 +    unfolding RCOSETS_def r_coset_def
    6.84 +    by (blast intro: rcos_equation assms sym)
    6.85  qed
    6.86  
    6.87  
    6.88 @@ -761,26 +751,26 @@
    6.89  proof -
    6.90    interpret subgroup H G by fact
    6.91    show ?thesis
    6.92 -    apply (rule equalityI)
    6.93 -    apply (force simp add: RCOSETS_def r_coset_def)
    6.94 -    apply (auto simp add: RCOSETS_def intro: rcos_self assms)
    6.95 -    done
    6.96 +    unfolding RCOSETS_def r_coset_def by auto
    6.97  qed
    6.98  
    6.99  lemma (in group) cosets_finite:
   6.100       "\<lbrakk>c \<in> rcosets H;  H \<subseteq> carrier G;  finite (carrier G)\<rbrakk> \<Longrightarrow> finite c"
   6.101 -apply (auto simp add: RCOSETS_def)
   6.102 -apply (simp add: r_coset_subset_G [THEN finite_subset])
   6.103 -done
   6.104 +  unfolding RCOSETS_def
   6.105 +  by (auto simp add: r_coset_subset_G [THEN finite_subset])
   6.106  
   6.107  text\<open>The next two lemmas support the proof of \<open>card_cosets_equal\<close>.\<close>
   6.108  lemma (in group) inj_on_f:
   6.109 -    "\<lbrakk>H \<subseteq> carrier G;  a \<in> carrier G\<rbrakk> \<Longrightarrow> inj_on (\<lambda>y. y \<otimes> inv a) (H #> a)"
   6.110 -apply (rule inj_onI)
   6.111 -apply (subgoal_tac "x \<in> carrier G \<and> y \<in> carrier G")
   6.112 - prefer 2 apply (blast intro: r_coset_subset_G [THEN subsetD])
   6.113 -apply (simp add: subsetD)
   6.114 -done
   6.115 +  assumes "H \<subseteq> carrier G" and a: "a \<in> carrier G"
   6.116 +  shows "inj_on (\<lambda>y. y \<otimes> inv a) (H #> a)"
   6.117 +proof 
   6.118 +  fix x y
   6.119 +  assume "x \<in> H #> a" "y \<in> H #> a" and xy: "x \<otimes> inv a = y \<otimes> inv a"
   6.120 +  then have "x \<in> carrier G" "y \<in> carrier G"
   6.121 +    using assms r_coset_subset_G by blast+
   6.122 +  with xy a show "x = y"
   6.123 +    by auto
   6.124 +qed
   6.125  
   6.126  lemma (in group) inj_on_g:
   6.127      "\<lbrakk>H \<subseteq> carrier G;  a \<in> carrier G\<rbrakk> \<Longrightarrow> inj_on (\<lambda>y. y \<otimes> a) H"
   6.128 @@ -827,16 +817,17 @@
   6.129    using rcosets_part_G by auto
   6.130  
   6.131  proposition (in group) lagrange_finite:
   6.132 -     "\<lbrakk>finite(carrier G); subgroup H G\<rbrakk>
   6.133 -      \<Longrightarrow> card(rcosets H) * card(H) = order(G)"
   6.134 -apply (simp (no_asm_simp) add: order_def rcosets_part_G [symmetric])
   6.135 -apply (subst mult.commute)
   6.136 -apply (rule card_partition)
   6.137 -   apply (simp add: rcosets_subset_PowG [THEN finite_subset])
   6.138 -  apply (simp add: rcosets_part_G)
   6.139 -  apply (simp add: card_rcosets_equal subgroup.subset)
   6.140 -apply (simp add: rcos_disjoint)
   6.141 -done
   6.142 +  assumes "finite(carrier G)" and HG: "subgroup H G"
   6.143 +  shows "card(rcosets H) * card(H) = order(G)"
   6.144 +proof -
   6.145 +  have "card H * card (rcosets H) = card (\<Union>(rcosets H))"
   6.146 +  proof (rule card_partition)
   6.147 +    show "\<And>c1 c2. \<lbrakk>c1 \<in> rcosets H; c2 \<in> rcosets H; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}"
   6.148 +      using HG rcos_disjoint by auto
   6.149 +  qed (auto simp: assms finite_UnionD rcosets_part_G card_rcosets_equal subgroup.subset)
   6.150 +  then show ?thesis
   6.151 +    by (simp add: HG mult.commute order_def rcosets_part_G)
   6.152 +qed
   6.153  
   6.154  theorem (in group) lagrange:
   6.155    assumes "subgroup H G"
   6.156 @@ -844,29 +835,29 @@
   6.157  proof (cases "finite (carrier G)")
   6.158    case True thus ?thesis using lagrange_finite assms by simp
   6.159  next
   6.160 -  case False note inf_G = this
   6.161 +  case False 
   6.162    thus ?thesis
   6.163    proof (cases "finite H")
   6.164 -    case False thus ?thesis using inf_G  by (simp add: order_def)
   6.165 +    case False thus ?thesis using \<open>infinite (carrier G)\<close>  by (simp add: order_def)
   6.166    next
   6.167 -    case True note finite_H = this
   6.168 +    case True 
   6.169      have "infinite (rcosets H)"
   6.170 -    proof (rule ccontr)
   6.171 -      assume "\<not> infinite (rcosets H)"
   6.172 +    proof 
   6.173 +      assume "finite (rcosets H)"
   6.174        hence finite_rcos: "finite (rcosets H)" by simp
   6.175        hence "card (\<Union>(rcosets H)) = (\<Sum>R\<in>(rcosets H). card R)"
   6.176 -        using card_Union_disjoint[of "rcosets H"] finite_H rcos_disjoint[OF assms(1)]
   6.177 +        using card_Union_disjoint[of "rcosets H"] \<open>finite H\<close> rcos_disjoint[OF assms(1)]
   6.178                rcosets_finite[where ?H = H] by (simp add: assms subgroup.subset)
   6.179        hence "order G = (\<Sum>R\<in>(rcosets H). card R)"
   6.180          by (simp add: assms order_def rcosets_part_G)
   6.181        hence "order G = (\<Sum>R\<in>(rcosets H). card H)"
   6.182          using card_rcosets_equal by (simp add: assms subgroup.subset)
   6.183        hence "order G = (card H) * (card (rcosets H))" by simp
   6.184 -      hence "order G \<noteq> 0" using finite_rcos finite_H assms ex_in_conv
   6.185 +      hence "order G \<noteq> 0" using finite_rcos \<open>finite H\<close> assms ex_in_conv
   6.186                                  rcosets_part_G subgroup.one_closed by fastforce
   6.187 -      thus False using inf_G order_gt_0_iff_finite by blast
   6.188 +      thus False using \<open>infinite (carrier G)\<close> order_gt_0_iff_finite by blast
   6.189      qed
   6.190 -    thus ?thesis using inf_G by (simp add: order_def)
   6.191 +    thus ?thesis using \<open>infinite (carrier G)\<close> by (simp add: order_def)
   6.192    qed
   6.193  qed
   6.194  
   6.195 @@ -908,8 +899,8 @@
   6.196  
   6.197  theorem (in normal) factorgroup_is_group:
   6.198    "group (G Mod H)"
   6.199 -apply (simp add: FactGroup_def)
   6.200 -apply (rule groupI)
   6.201 +  unfolding FactGroup_def
   6.202 +  apply (rule groupI)
   6.203      apply (simp add: setmult_closed)
   6.204     apply (simp add: normal_imp_subgroup subgroup_in_rcosets [OF is_group])
   6.205    apply (simp add: restrictI setmult_closed rcosets_assoc)
   6.206 @@ -922,10 +913,20 @@
   6.207    by (simp add: FactGroup_def)
   6.208  
   6.209  lemma (in normal) inv_FactGroup:
   6.210 -     "X \<in> carrier (G Mod H) \<Longrightarrow> inv\<^bsub>G Mod H\<^esub> X = set_inv X"
   6.211 -apply (rule group.inv_equality [OF factorgroup_is_group])
   6.212 -apply (simp_all add: FactGroup_def setinv_closed rcosets_inv_mult_group_eq)
   6.213 -done
   6.214 +  assumes "X \<in> carrier (G Mod H)"
   6.215 +  shows "inv\<^bsub>G Mod H\<^esub> X = set_inv X"
   6.216 +proof -
   6.217 +  have X: "X \<in> rcosets H"
   6.218 +    using assms by (simp add: FactGroup_def)
   6.219 +  moreover have "set_inv X <#> X = H"
   6.220 +    using X by (simp add: normal.rcosets_inv_mult_group_eq normal_axioms)
   6.221 +  moreover have "Group.group (G Mod H)"
   6.222 +    using normal.factorgroup_is_group normal_axioms by blast
   6.223 +  moreover have "set_inv X \<in> rcosets H"
   6.224 +    by (simp add: \<open>X \<in> rcosets H\<close> setinv_closed)
   6.225 +  ultimately show ?thesis
   6.226 +    by (simp add: FactGroup_def group.inv_equality)
   6.227 +qed
   6.228  
   6.229  text\<open>The coset map is a homomorphism from @{term G} to the quotient group
   6.230    @{term "G Mod H"}\<close>
   6.231 @@ -945,15 +946,13 @@
   6.232    where "kernel G H h = {x. x \<in> carrier G \<and> h x = \<one>\<^bsub>H\<^esub>}"
   6.233  
   6.234  lemma (in group_hom) subgroup_kernel: "subgroup (kernel G H h) G"
   6.235 -apply (rule subgroup.intro)
   6.236 -apply (auto simp add: kernel_def group.intro is_group)
   6.237 -done
   6.238 +  by (auto simp add: kernel_def group.intro is_group intro: subgroup.intro)
   6.239  
   6.240  text\<open>The kernel of a homomorphism is a normal subgroup\<close>
   6.241  lemma (in group_hom) normal_kernel: "(kernel G H h) \<lhd> G"
   6.242 -apply (simp add: G.normal_inv_iff subgroup_kernel)
   6.243 -apply (simp add: kernel_def)
   6.244 -done
   6.245 +  apply (simp only: G.normal_inv_iff subgroup_kernel)
   6.246 +  apply (simp add: kernel_def)
   6.247 +  done
   6.248  
   6.249  lemma (in group_hom) FactGroup_nonempty:
   6.250    assumes X: "X \<in> carrier (G Mod kernel G H h)"
   6.251 @@ -982,37 +981,40 @@
   6.252  
   6.253  lemma (in group_hom) FactGroup_hom:
   6.254       "(\<lambda>X. the_elem (h`X)) \<in> hom (G Mod (kernel G H h)) H"
   6.255 -apply (simp add: hom_def FactGroup_the_elem_mem normal.factorgroup_is_group [OF normal_kernel] group.axioms monoid.m_closed)
   6.256 -proof (intro ballI)
   6.257 -  fix X and X'
   6.258 -  assume X:  "X  \<in> carrier (G Mod kernel G H h)"
   6.259 -     and X': "X' \<in> carrier (G Mod kernel G H h)"
   6.260 -  then
   6.261 -  obtain g and g'
   6.262 -           where "g \<in> carrier G" and "g' \<in> carrier G"
   6.263 -             and "X = kernel G H h #> g" and "X' = kernel G H h #> g'"
   6.264 -    by (auto simp add: FactGroup_def RCOSETS_def)
   6.265 -  hence all: "\<forall>x\<in>X. h x = h g" "\<forall>x\<in>X'. h x = h g'"
   6.266 -    and Xsub: "X \<subseteq> carrier G" and X'sub: "X' \<subseteq> carrier G"
   6.267 -    by (force simp add: kernel_def r_coset_def image_def)+
   6.268 -  hence "h ` (X <#> X') = {h g \<otimes>\<^bsub>H\<^esub> h g'}" using X X'
   6.269 -    by (auto dest!: FactGroup_nonempty intro!: image_eqI
   6.270 -             simp add: set_mult_def
   6.271 -                       subsetD [OF Xsub] subsetD [OF X'sub])
   6.272 -  then show "the_elem (h ` (X <#> X')) = the_elem (h ` X) \<otimes>\<^bsub>H\<^esub> the_elem (h ` X')"
   6.273 -    by (auto simp add: all FactGroup_nonempty X X' the_elem_image_unique)
   6.274 +proof -
   6.275 +  have "the_elem (h ` (X <#> X')) = the_elem (h ` X) \<otimes>\<^bsub>H\<^esub> the_elem (h ` X')"
   6.276 +    if X: "X  \<in> carrier (G Mod kernel G H h)" and X': "X' \<in> carrier (G Mod kernel G H h)" for X X'
   6.277 +  proof -
   6.278 +    obtain g and g'
   6.279 +      where "g \<in> carrier G" and "g' \<in> carrier G"
   6.280 +        and "X = kernel G H h #> g" and "X' = kernel G H h #> g'"
   6.281 +      using X X' by (auto simp add: FactGroup_def RCOSETS_def)
   6.282 +    hence all: "\<forall>x\<in>X. h x = h g" "\<forall>x\<in>X'. h x = h g'"
   6.283 +      and Xsub: "X \<subseteq> carrier G" and X'sub: "X' \<subseteq> carrier G"
   6.284 +      by (force simp add: kernel_def r_coset_def image_def)+
   6.285 +    hence "h ` (X <#> X') = {h g \<otimes>\<^bsub>H\<^esub> h g'}" using X X'
   6.286 +      by (auto dest!: FactGroup_nonempty intro!: image_eqI
   6.287 +          simp add: set_mult_def
   6.288 +          subsetD [OF Xsub] subsetD [OF X'sub])
   6.289 +    then show "the_elem (h ` (X <#> X')) = the_elem (h ` X) \<otimes>\<^bsub>H\<^esub> the_elem (h ` X')"
   6.290 +      by (auto simp add: all FactGroup_nonempty X X' the_elem_image_unique)
   6.291 +  qed
   6.292 +  then show ?thesis
   6.293 +    by (simp add: hom_def FactGroup_the_elem_mem normal.factorgroup_is_group [OF normal_kernel] group.axioms monoid.m_closed)
   6.294  qed
   6.295  
   6.296  
   6.297  text\<open>Lemma for the following injectivity result\<close>
   6.298  lemma (in group_hom) FactGroup_subset:
   6.299 -     "\<lbrakk>g \<in> carrier G; g' \<in> carrier G; h g = h g'\<rbrakk>
   6.300 -      \<Longrightarrow>  kernel G H h #> g \<subseteq> kernel G H h #> g'"
   6.301 -apply (clarsimp simp add: kernel_def r_coset_def)
   6.302 -apply (rename_tac y)
   6.303 -apply (rule_tac x="y \<otimes> g \<otimes> inv g'" in exI)
   6.304 -apply (simp add: G.m_assoc)
   6.305 -done
   6.306 +  assumes "g \<in> carrier G" "g' \<in> carrier G" "h g = h g'"
   6.307 +  shows "kernel G H h #> g \<subseteq> kernel G H h #> g'"
   6.308 +  unfolding kernel_def r_coset_def
   6.309 +proof clarsimp
   6.310 +  fix y 
   6.311 +  assume "y \<in> carrier G" "h y = \<one>\<^bsub>H\<^esub>"
   6.312 +  with assms show "\<exists>x. x \<in> carrier G \<and> h x = \<one>\<^bsub>H\<^esub> \<and> y \<otimes> g = x \<otimes> g'"
   6.313 +    by (rule_tac x="y \<otimes> g \<otimes> inv g'" in exI) (auto simp: G.m_assoc)
   6.314 +qed
   6.315  
   6.316  lemma (in group_hom) FactGroup_inj_on:
   6.317       "inj_on (\<lambda>X. the_elem (h ` X)) (carrier (G Mod kernel G H h))"
   6.318 @@ -1113,13 +1115,13 @@
   6.319      from hHN obtain h1 h2 where h1h2 : "h1 \<in> H" "h2 \<in> N" "h = (h1,h2)"
   6.320        unfolding DirProd_def by fastforce
   6.321      hence h1h2GK : "h1 \<in> carrier G" "h2 \<in> carrier K"
   6.322 -      using normal_imp_subgroup subgroup.subset assms apply blast+.
   6.323 +      using normal_imp_subgroup subgroup.subset assms by blast+
   6.324      have "inv\<^bsub>G \<times>\<times> K\<^esub> x = (inv\<^bsub>G\<^esub> x1,inv\<^bsub>K\<^esub> x2)"
   6.325        using inv_DirProd[OF group_axioms assms(1) x1x2(1)x1x2(2)] x1x2 by auto
   6.326      hence "x \<otimes>\<^bsub>G \<times>\<times> K\<^esub> h \<otimes>\<^bsub>G \<times>\<times> K\<^esub> inv\<^bsub>G \<times>\<times> K\<^esub> x = (x1 \<otimes> h1 \<otimes> inv x1,x2 \<otimes>\<^bsub>K\<^esub> h2 \<otimes>\<^bsub>K\<^esub> inv\<^bsub>K\<^esub> x2)"
   6.327        using h1h2 x1x2 h1h2GK by auto
   6.328      moreover have "x1 \<otimes> h1 \<otimes> inv x1 \<in> H" "x2 \<otimes>\<^bsub>K\<^esub> h2 \<otimes>\<^bsub>K\<^esub> inv\<^bsub>K\<^esub> x2 \<in> N"
   6.329 -      using normal_invE group.normal_invE[OF assms(1)] assms x1x2 h1h2 apply auto.
   6.330 +      using assms x1x2 h1h2 assms by (simp_all add: normal.inv_op_closed2)
   6.331      hence "(x1 \<otimes> h1 \<otimes> inv x1, x2 \<otimes>\<^bsub>K\<^esub> h2 \<otimes>\<^bsub>K\<^esub> inv\<^bsub>K\<^esub> x2)\<in> H \<times> N" by auto
   6.332      ultimately show " x \<otimes>\<^bsub>G \<times>\<times> K\<^esub> h \<otimes>\<^bsub>G \<times>\<times> K\<^esub> inv\<^bsub>G \<times>\<times> K\<^esub> x \<in> H \<times> N" by auto
   6.333    qed
   6.334 @@ -1133,7 +1135,7 @@
   6.335  
   6.336  proof-
   6.337    have R :"(\<lambda>(X, Y). X \<times> Y) \<in> carrier (G Mod H) \<times> carrier (K Mod N) \<rightarrow> carrier (G \<times>\<times> K Mod H \<times> N)"
   6.338 -    unfolding r_coset_def Sigma_def DirProd_def FactGroup_def RCOSETS_def apply simp by blast
   6.339 +    unfolding r_coset_def Sigma_def DirProd_def FactGroup_def RCOSETS_def by force
   6.340    moreover have "(\<forall>x\<in>carrier (G Mod H). \<forall>y\<in>carrier (K Mod N). \<forall>xa\<in>carrier (G Mod H).
   6.341                  \<forall>ya\<in>carrier (K Mod N). (x <#> xa) \<times> (y <#>\<^bsub>K\<^esub> ya) =  x \<times> y <#>\<^bsub>G \<times>\<times> K\<^esub> xa \<times> ya)"
   6.342      unfolding set_mult_def by force
   6.343 @@ -1143,8 +1145,14 @@
   6.344      by (metis assms(2) assms(3) normal_def partial_object.select_convs(1))
   6.345    moreover have "(\<lambda>(X, Y). X \<times> Y) ` (carrier (G Mod H) \<times> carrier (K Mod N)) =
   6.346                                       carrier (G \<times>\<times> K Mod H \<times> N)"
   6.347 -    unfolding image_def  apply auto using R apply force
   6.348 -    unfolding DirProd_def FactGroup_def RCOSETS_def r_coset_def by force
   6.349 +  proof -
   6.350 +    have 1: "\<And>x a b. \<lbrakk>a \<in> carrier (G Mod H); b \<in> carrier (K Mod N)\<rbrakk> \<Longrightarrow> a \<times> b \<in> carrier (G \<times>\<times> K Mod H \<times> N)"
   6.351 +      using R by force
   6.352 +    have 2: "\<And>z. z \<in> carrier (G \<times>\<times> K Mod H \<times> N) \<Longrightarrow> \<exists>x\<in>carrier (G Mod H). \<exists>y\<in>carrier (K Mod N). z = x \<times> y"
   6.353 +      unfolding DirProd_def FactGroup_def RCOSETS_def r_coset_def by force
   6.354 +    show ?thesis
   6.355 +      unfolding image_def by (auto simp: intro: 1 2)
   6.356 +  qed
   6.357    ultimately show ?thesis
   6.358      unfolding iso_def hom_def bij_betw_def inj_on_def by simp
   6.359  qed
   6.360 @@ -1262,7 +1270,7 @@
   6.361        have hH:"h\<in>carrier(GH)"
   6.362          using hHK HK_def GH_def by auto
   6.363        have  "(\<forall>x\<in>carrier (GH). \<forall>h\<in>H1.  x \<otimes>\<^bsub>GH\<^esub> h \<otimes>\<^bsub>GH\<^esub> inv\<^bsub>GH\<^esub> x \<in> H1)"
   6.364 -        using assms normal_invE GH_def normal.inv_op_closed2 by fastforce
   6.365 +        using assms GH_def normal.inv_op_closed2 by fastforce
   6.366        hence INCL_1 : "x \<otimes>\<^bsub>GH\<^esub> h \<otimes>\<^bsub>GH\<^esub> inv\<^bsub>GH\<^esub> x \<in> H1"
   6.367          using  xH H1K_def p2 by blast
   6.368        have " x \<otimes>\<^bsub>GH\<^esub> h \<otimes>\<^bsub>GH\<^esub> inv\<^bsub>GH\<^esub> x \<in> HK"
   6.369 @@ -1275,7 +1283,6 @@
   6.370    qed
   6.371  qed
   6.372  
   6.373 -
   6.374  lemma (in group) normal_inter_subgroup:
   6.375    assumes "subgroup H G"
   6.376      and "N \<lhd> G"
   6.377 @@ -1288,8 +1295,8 @@
   6.378    ultimately have "N \<inter> H \<lhd> G\<lparr>carrier := K \<inter> H\<rparr>"
   6.379      using normal_inter[of K H N] assms(1) by blast
   6.380    moreover have "K \<inter> H = H" using K_def assms subgroup.subset by blast
   6.381 -  ultimately show "normal (N\<inter>H) (G\<lparr>carrier := H\<rparr>)" by auto
   6.382 +  ultimately show "normal (N\<inter>H) (G\<lparr>carrier := H\<rparr>)"
   6.383 + by auto
   6.384  qed
   6.385  
   6.386 -
   6.387  end
     7.1 --- a/src/HOL/Algebra/Divisibility.thy	Sun Jul 29 13:18:10 2018 +0200
     7.2 +++ b/src/HOL/Algebra/Divisibility.thy	Sun Jul 29 18:24:47 2018 +0200
     7.3 @@ -547,22 +547,14 @@
     7.4    using pf by (elim properfactorE)
     7.5  
     7.6  lemma (in monoid) properfactor_trans1 [trans]:
     7.7 -  assumes dvds: "a divides b"  "properfactor G b c"
     7.8 -    and carr: "a \<in> carrier G"  "c \<in> carrier G"
     7.9 +  assumes "a divides b"  "properfactor G b c" "a \<in> carrier G"  "c \<in> carrier G"
    7.10    shows "properfactor G a c"
    7.11 -  using dvds carr
    7.12 -  apply (elim properfactorE, intro properfactorI)
    7.13 -   apply (iprover intro: divides_trans)+
    7.14 -  done
    7.15 +  by (meson divides_trans properfactorE properfactorI assms)
    7.16  
    7.17  lemma (in monoid) properfactor_trans2 [trans]:
    7.18 -  assumes dvds: "properfactor G a b"  "b divides c"
    7.19 -    and carr: "a \<in> carrier G"  "b \<in> carrier G"
    7.20 +  assumes "properfactor G a b"  "b divides c" "a \<in> carrier G"  "b \<in> carrier G"
    7.21    shows "properfactor G a c"
    7.22 -  using dvds carr
    7.23 -  apply (elim properfactorE, intro properfactorI)
    7.24 -   apply (iprover intro: divides_trans)+
    7.25 -  done
    7.26 +  by (meson divides_trans properfactorE properfactorI assms)
    7.27  
    7.28  lemma properfactor_lless:
    7.29    fixes G (structure)
    7.30 @@ -660,23 +652,20 @@
    7.31    using assms by (fast elim: irreducibleE)
    7.32  
    7.33  lemma (in monoid_cancel) irreducible_cong [trans]:
    7.34 -  assumes irred: "irreducible G a"
    7.35 -    and aa': "a \<sim> a'" "a \<in> carrier G"  "a' \<in> carrier G"
    7.36 +  assumes "irreducible G a" "a \<sim> a'" "a \<in> carrier G"  "a' \<in> carrier G"
    7.37    shows "irreducible G a'"
    7.38 -  using assms
    7.39 -  apply (auto simp: irreducible_def assoc_unit_l)
    7.40 -  apply (metis aa' associated_sym properfactor_cong_r)
    7.41 -  done
    7.42 +proof -
    7.43 +  have "a' divides a"
    7.44 +    by (meson \<open>a \<sim> a'\<close> associated_def)
    7.45 +  then show ?thesis
    7.46 +    by (metis (no_types) assms assoc_unit_l irreducibleE irreducibleI monoid.properfactor_trans2 monoid_axioms)
    7.47 +qed
    7.48  
    7.49  lemma (in monoid) irreducible_prod_rI:
    7.50 -  assumes airr: "irreducible G a"
    7.51 -    and bunit: "b \<in> Units G"
    7.52 -    and carr[simp]: "a \<in> carrier G"  "b \<in> carrier G"
    7.53 +  assumes "irreducible G a" "b \<in> Units G" "a \<in> carrier G"  "b \<in> carrier G"
    7.54    shows "irreducible G (a \<otimes> b)"
    7.55 -  using airr carr bunit
    7.56 -  apply (elim irreducibleE, intro irreducibleI)
    7.57 -  using prod_unit_r apply blast
    7.58 -  using associatedI2' properfactor_cong_r by auto
    7.59 +  using assms
    7.60 +  by (metis (no_types, lifting) associatedI2' irreducible_def monoid.m_closed monoid_axioms prod_unit_r properfactor_cong_r)
    7.61  
    7.62  lemma (in comm_monoid) irreducible_prod_lI:
    7.63    assumes birr: "irreducible G b"
    7.64 @@ -764,9 +753,7 @@
    7.65      and pp': "p \<sim> p'" "p \<in> carrier G"  "p' \<in> carrier G"
    7.66    shows "prime G p'"
    7.67    using assms
    7.68 -  apply (auto simp: prime_def assoc_unit_l)
    7.69 -  apply (metis pp' associated_sym divides_cong_l)
    7.70 -  done
    7.71 +  by (auto simp: prime_def assoc_unit_l) (metis pp' associated_sym divides_cong_l)
    7.72  
    7.73  (*by Paulo Emílio de Vilhena*)
    7.74  lemma (in comm_monoid_cancel) prime_irreducible:
    7.75 @@ -849,9 +836,7 @@
    7.76      and "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G"
    7.77    shows "\<forall>a\<in>set bs. irreducible G a"
    7.78    using assms
    7.79 -  apply (clarsimp simp add: list_all2_conv_all_nth set_conv_nth)
    7.80 -  apply (blast intro: irreducible_cong)
    7.81 -  done
    7.82 +  by (fastforce simp add: list_all2_conv_all_nth set_conv_nth intro: irreducible_cong)
    7.83  
    7.84  
    7.85  text \<open>Permutations\<close>
    7.86 @@ -1001,15 +986,7 @@
    7.87    then have f: "f \<in> carrier G"
    7.88      by blast
    7.89    show ?case
    7.90 -  proof (cases "f = a")
    7.91 -    case True
    7.92 -    then show ?thesis
    7.93 -      using Cons.prems by auto
    7.94 -  next
    7.95 -    case False
    7.96 -    with Cons show ?thesis
    7.97 -      by clarsimp (metis f divides_prod_l multlist_closed)
    7.98 -  qed
    7.99 +    using Cons.IH Cons.prems(1) Cons.prems(2) divides_prod_l f by auto
   7.100  qed auto
   7.101  
   7.102  lemma (in comm_monoid_cancel) multlist_listassoc_cong:
   7.103 @@ -1051,9 +1028,7 @@
   7.104      and "set fs \<subseteq> carrier G" and "set fs' \<subseteq> carrier G"
   7.105    shows "foldr (\<otimes>) fs \<one> \<sim> foldr (\<otimes>) fs' \<one>"
   7.106    using assms
   7.107 -  apply (elim essentially_equalE)
   7.108 -  apply (simp add: multlist_perm_cong multlist_listassoc_cong perm_closed)
   7.109 -  done
   7.110 +  by (metis essentially_equal_def multlist_listassoc_cong multlist_perm_cong perm_closed)
   7.111  
   7.112  
   7.113  subsubsection \<open>Factorization in irreducible elements\<close>
   7.114 @@ -1120,9 +1095,6 @@
   7.115      and carr[simp]: "set fs \<subseteq> carrier G"
   7.116    shows "fs = []"
   7.117  proof (cases fs)
   7.118 -  case Nil
   7.119 -  then show ?thesis .
   7.120 -next
   7.121    case fs: (Cons f fs')
   7.122    from carr have fcarr[simp]: "f \<in> carrier G" and carr'[simp]: "set fs' \<subseteq> carrier G"
   7.123      by (simp_all add: fs)
   7.124 @@ -1874,6 +1846,18 @@
   7.125  qed
   7.126  
   7.127  lemma (in factorial_monoid) properfactor_fmset:
   7.128 +  assumes "properfactor G a b"
   7.129 +    and "wfactors G as a"
   7.130 +    and "wfactors G bs b"
   7.131 +    and "a \<in> carrier G"
   7.132 +    and "b \<in> carrier G"
   7.133 +    and "set as \<subseteq> carrier G"
   7.134 +    and "set bs \<subseteq> carrier G"
   7.135 +  shows "fmset G as \<subseteq># fmset G bs"
   7.136 +  using assms
   7.137 +  by (meson divides_as_fmsubset properfactor_divides)
   7.138 +
   7.139 +lemma (in factorial_monoid) properfactor_fmset_ne:
   7.140    assumes pf: "properfactor G a b"
   7.141      and "wfactors G as a"
   7.142      and "wfactors G bs b"
   7.143 @@ -1881,11 +1865,8 @@
   7.144      and "b \<in> carrier G"
   7.145      and "set as \<subseteq> carrier G"
   7.146      and "set bs \<subseteq> carrier G"
   7.147 -  shows "fmset G as \<subseteq># fmset G bs \<and> fmset G as \<noteq> fmset G bs"
   7.148 -  using pf
   7.149 -  apply safe
   7.150 -   apply (meson assms divides_as_fmsubset monoid.properfactor_divides monoid_axioms)
   7.151 -  by (meson assms associated_def comm_monoid_cancel.ee_wfactorsD comm_monoid_cancel.fmset_ee factorial_monoid_axioms factorial_monoid_def properfactorE)
   7.152 +  shows "fmset G as \<noteq> fmset G bs"
   7.153 +  using properfactorE [OF pf] assms divides_as_fmsubset by force
   7.154  
   7.155  subsection \<open>Irreducible Elements are Prime\<close>
   7.156  
   7.157 @@ -2246,75 +2227,70 @@
   7.158  qed
   7.159  
   7.160  lemma (in gcd_condition_monoid) gcdof_cong_l:
   7.161 -  assumes a'a: "a' \<sim> a"
   7.162 -    and agcd: "a gcdof b c"
   7.163 -    and a'carr: "a' \<in> carrier G" and carr': "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
   7.164 +  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"
   7.165    shows "a' gcdof b c"
   7.166  proof -
   7.167 -  note carr = a'carr carr'
   7.168    interpret weak_lower_semilattice "division_rel G" by simp
   7.169    have "is_glb (division_rel G) a' {b, c}"
   7.170 -    by (subst greatest_Lower_cong_l[of _ a]) (simp_all add: a'a carr gcdof_greatestLower[symmetric] agcd)
   7.171 +    by (subst greatest_Lower_cong_l[of _ a]) (simp_all add: assms gcdof_greatestLower[symmetric])
   7.172    then have "a' \<in> carrier G \<and> a' gcdof b c"
   7.173      by (simp add: gcdof_greatestLower carr')
   7.174    then show ?thesis ..
   7.175  qed
   7.176  
   7.177  lemma (in gcd_condition_monoid) gcd_closed [simp]:
   7.178 -  assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
   7.179 +  assumes "a \<in> carrier G" "b \<in> carrier G"
   7.180    shows "somegcd G a b \<in> carrier G"
   7.181  proof -
   7.182    interpret weak_lower_semilattice "division_rel G" by simp
   7.183    show ?thesis
   7.184 -    apply (simp add: somegcd_meet[OF carr])
   7.185 -    apply (rule meet_closed[simplified], fact+)
   7.186 -    done
   7.187 +  using  assms meet_closed by (simp add: somegcd_meet)
   7.188  qed
   7.189  
   7.190  lemma (in gcd_condition_monoid) gcd_isgcd:
   7.191 -  assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
   7.192 +  assumes "a \<in> carrier G"  "b \<in> carrier G"
   7.193    shows "(somegcd G a b) gcdof a b"
   7.194  proof -
   7.195    interpret weak_lower_semilattice "division_rel G"
   7.196      by simp
   7.197 -  from carr have "somegcd G a b \<in> carrier G \<and> (somegcd G a b) gcdof a b"
   7.198 +  from assms have "somegcd G a b \<in> carrier G \<and> (somegcd G a b) gcdof a b"
   7.199      by (simp add: gcdof_greatestLower inf_of_two_greatest meet_def somegcd_meet)
   7.200    then show "(somegcd G a b) gcdof a b"
   7.201      by simp
   7.202  qed
   7.203  
   7.204  lemma (in gcd_condition_monoid) gcd_exists:
   7.205 -  assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
   7.206 +  assumes "a \<in> carrier G"  "b \<in> carrier G"
   7.207    shows "\<exists>x\<in>carrier G. x = somegcd G a b"
   7.208  proof -
   7.209    interpret weak_lower_semilattice "division_rel G"
   7.210      by simp
   7.211    show ?thesis
   7.212 -    by (metis carr(1) carr(2) gcd_closed)
   7.213 +    by (metis assms gcd_closed)
   7.214  qed
   7.215  
   7.216  lemma (in gcd_condition_monoid) gcd_divides_l:
   7.217 -  assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
   7.218 +  assumes "a \<in> carrier G" "b \<in> carrier G"
   7.219    shows "(somegcd G a b) divides a"
   7.220  proof -
   7.221    interpret weak_lower_semilattice "division_rel G"
   7.222      by simp
   7.223    show ?thesis
   7.224 -    by (metis carr(1) carr(2) gcd_isgcd isgcd_def)
   7.225 +    by (metis assms gcd_isgcd isgcd_def)
   7.226  qed
   7.227  
   7.228  lemma (in gcd_condition_monoid) gcd_divides_r:
   7.229 -  assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
   7.230 +  assumes "a \<in> carrier G"  "b \<in> carrier G"
   7.231    shows "(somegcd G a b) divides b"
   7.232  proof -
   7.233    interpret weak_lower_semilattice "division_rel G"
   7.234      by simp
   7.235    show ?thesis
   7.236 -    by (metis carr gcd_isgcd isgcd_def)
   7.237 +    by (metis assms gcd_isgcd isgcd_def)
   7.238  qed
   7.239  
   7.240  lemma (in gcd_condition_monoid) gcd_divides:
   7.241 -  assumes sub: "z divides x"  "z divides y"
   7.242 +  assumes "z divides x" "z divides y"
   7.243      and L: "x \<in> carrier G"  "y \<in> carrier G"  "z \<in> carrier G"
   7.244    shows "z divides (somegcd G x y)"
   7.245  proof -
   7.246 @@ -2325,49 +2301,25 @@
   7.247  qed
   7.248  
   7.249  lemma (in gcd_condition_monoid) gcd_cong_l:
   7.250 -  assumes xx': "x \<sim> x'"
   7.251 -    and carr: "x \<in> carrier G"  "x' \<in> carrier G"  "y \<in> carrier G"
   7.252 +  assumes "x \<sim> x'" "x \<in> carrier G"  "x' \<in> carrier G"  "y \<in> carrier G"
   7.253    shows "somegcd G x y \<sim> somegcd G x' y"
   7.254  proof -
   7.255    interpret weak_lower_semilattice "division_rel G"
   7.256      by simp
   7.257    show ?thesis
   7.258 -    apply (simp add: somegcd_meet carr)
   7.259 -    apply (rule meet_cong_l[simplified], fact+)
   7.260 -    done
   7.261 +    using somegcd_meet assms
   7.262 +    by (metis eq_object.select_convs(1) meet_cong_l partial_object.select_convs(1))
   7.263  qed
   7.264  
   7.265  lemma (in gcd_condition_monoid) gcd_cong_r:
   7.266 -  assumes carr: "x \<in> carrier G"  "y \<in> carrier G"  "y' \<in> carrier G"
   7.267 -    and yy': "y \<sim> y'"
   7.268 +  assumes "y \<sim> y'" "x \<in> carrier G"  "y \<in> carrier G" "y' \<in> carrier G"
   7.269    shows "somegcd G x y \<sim> somegcd G x y'"
   7.270  proof -
   7.271    interpret weak_lower_semilattice "division_rel G" by simp
   7.272    show ?thesis
   7.273 -    apply (simp add: somegcd_meet carr)
   7.274 -    apply (rule meet_cong_r[simplified], fact+)
   7.275 -    done
   7.276 +    by (meson associated_def assms gcd_closed gcd_divides gcd_divides_l gcd_divides_r monoid.divides_trans monoid_axioms)
   7.277  qed
   7.278  
   7.279 -(*
   7.280 -lemma (in gcd_condition_monoid) asc_cong_gcd_l [intro]:
   7.281 -  assumes carr: "b \<in> carrier G"
   7.282 -  shows "asc_cong (\<lambda>a. somegcd G a b)"
   7.283 -using carr
   7.284 -unfolding CONG_def
   7.285 -by clarsimp (blast intro: gcd_cong_l)
   7.286 -
   7.287 -lemma (in gcd_condition_monoid) asc_cong_gcd_r [intro]:
   7.288 -  assumes carr: "a \<in> carrier G"
   7.289 -  shows "asc_cong (\<lambda>b. somegcd G a b)"
   7.290 -using carr
   7.291 -unfolding CONG_def
   7.292 -by clarsimp (blast intro: gcd_cong_r)
   7.293 -
   7.294 -lemmas (in gcd_condition_monoid) asc_cong_gcd_split [simp] =
   7.295 -    assoc_split[OF _ asc_cong_gcd_l] assoc_split[OF _ asc_cong_gcd_r]
   7.296 -*)
   7.297 -
   7.298  lemma (in gcd_condition_monoid) gcdI:
   7.299    assumes dvd: "a divides b"  "a divides c"
   7.300      and others: "\<And>y. \<lbrakk>y\<in>carrier G; y divides b; y divides c\<rbrakk> \<Longrightarrow> y divides a"
   7.301 @@ -2390,25 +2342,23 @@
   7.302  
   7.303  lemma (in gcd_condition_monoid) SomeGcd_ex:
   7.304    assumes "finite A"  "A \<subseteq> carrier G"  "A \<noteq> {}"
   7.305 -  shows "\<exists>x\<in> carrier G. x = SomeGcd G A"
   7.306 +  shows "\<exists>x \<in> carrier G. x = SomeGcd G A"
   7.307  proof -
   7.308    interpret weak_lower_semilattice "division_rel G"
   7.309      by simp
   7.310    show ?thesis
   7.311 -    apply (simp add: SomeGcd_def)
   7.312 -    apply (rule finite_inf_closed[simplified], fact+)
   7.313 -    done
   7.314 +    using finite_inf_closed by (simp add: assms SomeGcd_def)
   7.315  qed
   7.316  
   7.317  lemma (in gcd_condition_monoid) gcd_assoc:
   7.318 -  assumes carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
   7.319 +  assumes "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
   7.320    shows "somegcd G (somegcd G a b) c \<sim> somegcd G a (somegcd G b c)"
   7.321  proof -
   7.322    interpret weak_lower_semilattice "division_rel G"
   7.323      by simp
   7.324    show ?thesis
   7.325      unfolding associated_def
   7.326 -    by (meson carr divides_trans gcd_divides gcd_divides_l gcd_divides_r gcd_exists)
   7.327 +    by (meson assms divides_trans gcd_divides gcd_divides_l gcd_divides_r gcd_exists)
   7.328  qed
   7.329  
   7.330  lemma (in gcd_condition_monoid) gcd_mult:
   7.331 @@ -2641,141 +2591,124 @@
   7.332      using Cons.IH Cons.prems(1) by force
   7.333  qed
   7.334  
   7.335 -
   7.336 -lemma (in primeness_condition_monoid) wfactors_unique__hlp_induct:
   7.337 -  "\<forall>a as'. a \<in> carrier G \<and> set as \<subseteq> carrier G \<and> set as' \<subseteq> carrier G \<and>
   7.338 -           wfactors G as a \<and> wfactors G as' a \<longrightarrow> essentially_equal G as as'"
   7.339 -proof (induct as)
   7.340 +proposition (in primeness_condition_monoid) wfactors_unique:
   7.341 +  assumes "wfactors G as a"  "wfactors G as' a"
   7.342 +    and "a \<in> carrier G"  "set as \<subseteq> carrier G"  "set as' \<subseteq> carrier G"
   7.343 +  shows "essentially_equal G as as'"
   7.344 +  using assms
   7.345 +proof (induct as arbitrary: a as')
   7.346    case Nil
   7.347 -  show ?case
   7.348 -    apply (clarsimp simp: wfactors_def)
   7.349 -    by (metis Units_one_closed assoc_unit_r list_update_nonempty unit_wfactors_empty unitfactor_ee wfactorsI)
   7.350 +  then have "a \<sim> \<one>"
   7.351 +    by (meson Units_one_closed one_closed perm.Nil perm_wfactorsD unit_wfactors)
   7.352 +  then have "as' = []"
   7.353 +    using Nil.prems assoc_unit_l unit_wfactors_empty by blast
   7.354 +  then show ?case
   7.355 +    by auto
   7.356  next
   7.357    case (Cons ah as)
   7.358 -  then show ?case
   7.359 -  proof clarsimp
   7.360 -    fix a as'
   7.361 -    assume ih [rule_format]:
   7.362 -      "\<forall>a as'. a \<in> carrier G \<and> set as' \<subseteq> carrier G \<and> wfactors G as a \<and>
   7.363 -        wfactors G as' a \<longrightarrow> essentially_equal G as as'"
   7.364 -      and acarr: "a \<in> carrier G" and ahcarr: "ah \<in> carrier G"
   7.365 -      and ascarr: "set as \<subseteq> carrier G" and as'carr: "set as' \<subseteq> carrier G"
   7.366 -      and afs: "wfactors G (ah # as) a"
   7.367 -      and afs': "wfactors G as' a"
   7.368 -    then have ahdvda: "ah divides a"
   7.369 -      by (intro wfactors_dividesI[of "ah#as" "a"]) simp_all
   7.370 +  then have ahdvda: "ah divides a"
   7.371 +    using wfactors_dividesI by auto
   7.372      then obtain a' where a'carr: "a' \<in> carrier G" and a: "a = ah \<otimes> a'"
   7.373        by blast
   7.374 +    have carr_ah: "ah \<in> carrier G" "set as \<subseteq> carrier G"
   7.375 +      using Cons.prems by fastforce+
   7.376 +    have "ah \<otimes> foldr (\<otimes>) as \<one> \<sim> a"
   7.377 +      by (rule wfactorsE[OF \<open>wfactors G (ah # as) a\<close>]) auto
   7.378 +    then have "foldr (\<otimes>) as \<one> \<sim> a'"
   7.379 +      by (metis Cons.prems(4) a a'carr assoc_l_cancel insert_subset list.set(2) monoid.multlist_closed monoid_axioms)
   7.380 +    then
   7.381      have a'fs: "wfactors G as a'"
   7.382 -      apply (rule wfactorsE[OF afs], rule wfactorsI, simp)
   7.383 -      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)
   7.384 -    from afs have ahirr: "irreducible G ah"
   7.385 -      by (elim wfactorsE) simp
   7.386 -    with ascarr have ahprime: "prime G ah"
   7.387 -      by (intro irreducible_prime ahcarr)
   7.388 -
   7.389 -    note carr [simp] = acarr ahcarr ascarr as'carr a'carr
   7.390 -
   7.391 +      by (meson Cons.prems(1) set_subset_Cons subset_iff wfactorsE wfactorsI)
   7.392 +    then have ahirr: "irreducible G ah"
   7.393 +      by (meson Cons.prems(1) list.set_intros(1) wfactorsE)
   7.394 +    with Cons have ahprime: "prime G ah"
   7.395 +      by (simp add: irreducible_prime)
   7.396      note ahdvda
   7.397 -    also from afs' have "a divides (foldr (\<otimes>) as' \<one>)"
   7.398 -      by (elim wfactorsE associatedE, simp)
   7.399 +    also have "a divides (foldr (\<otimes>) as' \<one>)"
   7.400 +      by (meson Cons.prems(2) associatedE wfactorsE)
   7.401      finally have "ah divides (foldr (\<otimes>) as' \<one>)"
   7.402 -      by simp
   7.403 +      using Cons.prems(4) by auto
   7.404      with ahprime have "\<exists>i<length as'. ah divides as'!i"
   7.405 -      by (intro multlist_prime_pos) simp_all
   7.406 +      by (intro multlist_prime_pos) (use Cons.prems in auto)
   7.407      then obtain i where len: "i<length as'" and ahdvd: "ah divides as'!i"
   7.408        by blast
   7.409 -    from afs' carr have irrasi: "irreducible G (as'!i)"
   7.410 -      by (fast intro: nth_mem[OF len] elim: wfactorsE)
   7.411 -    from len carr have asicarr[simp]: "as'!i \<in> carrier G"
   7.412 -      unfolding set_conv_nth by force
   7.413 -    note carr = carr asicarr
   7.414 -
   7.415 -    from ahdvd obtain x where "x \<in> carrier G" and asi: "as'!i = ah \<otimes> x"
   7.416 +    then obtain x where "x \<in> carrier G" and asi: "as'!i = ah \<otimes> x"
   7.417        by blast
   7.418 -    with carr irrasi[simplified asi] have asiah: "as'!i \<sim> ah"
   7.419 -      by (metis ahprime associatedI2 irreducible_prodE primeE)
   7.420 +    have irrasi: "irreducible G (as'!i)"
   7.421 +      using nth_mem[OF len] wfactorsE
   7.422 +      by (metis Cons.prems(2))
   7.423 +    have asicarr[simp]: "as'!i \<in> carrier G"
   7.424 +      using len \<open>set as' \<subseteq> carrier G\<close> nth_mem by blast
   7.425 +    have asiah: "as'!i \<sim> ah"
   7.426 +      by (metis \<open>ah \<in> carrier G\<close> \<open>x \<in> carrier G\<close> asi irrasi ahprime associatedI2 irreducible_prodE primeE)
   7.427      note setparts = set_take_subset[of i as'] set_drop_subset[of "Suc i" as']
   7.428 -    note partscarr [simp] = setparts[THEN subset_trans[OF _ as'carr]]
   7.429 -    note carr = carr partscarr
   7.430 -
   7.431      have "\<exists>aa_1. aa_1 \<in> carrier G \<and> wfactors G (take i as') aa_1"
   7.432 -      by (meson afs' in_set_takeD partscarr(1) wfactorsE wfactors_prod_exists)
   7.433 -    then obtain aa_1 where aa1carr: "aa_1 \<in> carrier G" and aa1fs: "wfactors G (take i as') aa_1"
   7.434 +      using Cons
   7.435 +      by (metis setparts(1) subset_trans in_set_takeD wfactorsE wfactors_prod_exists)
   7.436 +    then obtain aa_1 where aa1carr [simp]: "aa_1 \<in> carrier G" and aa1fs: "wfactors G (take i as') aa_1"
   7.437        by auto
   7.438 -
   7.439 -    have "\<exists>aa_2. aa_2 \<in> carrier G \<and> wfactors G (drop (Suc i) as') aa_2"
   7.440 -      by (meson afs' in_set_dropD partscarr(2) wfactors_def wfactors_prod_exists)
   7.441 -    then obtain aa_2 where aa2carr: "aa_2 \<in> carrier G"
   7.442 +    obtain aa_2 where aa2carr [simp]: "aa_2 \<in> carrier G"
   7.443        and aa2fs: "wfactors G (drop (Suc i) as') aa_2"
   7.444 -      by auto
   7.445 -
   7.446 -    note carr = carr aa1carr[simp] aa2carr[simp]
   7.447 -
   7.448 -    from aa1fs aa2fs
   7.449 -    have v1: "wfactors G (take i as' @ drop (Suc i) as') (aa_1 \<otimes> aa_2)"
   7.450 -      by (intro wfactors_mult, simp+)
   7.451 -    then have v1': "wfactors G (as'!i # take i as' @ drop (Suc i) as') (as'!i \<otimes> (aa_1 \<otimes> aa_2))"
   7.452 -      using irrasi wfactors_mult_single by auto
   7.453 -    from aa2carr carr aa1fs aa2fs have "wfactors G (as'!i # drop (Suc i) as') (as'!i \<otimes> aa_2)"
   7.454 -      by (metis irrasi wfactors_mult_single)
   7.455 -    with len carr aa1carr aa2carr aa1fs
   7.456 +      by (metis Cons.prems(2) Cons.prems(5) subset_code(1) in_set_dropD wfactors_def wfactors_prod_exists)
   7.457 +
   7.458 +    have set_drop: "set (drop (Suc i) as') \<subseteq> carrier G"
   7.459 +      using Cons.prems(5) setparts(2) by blast
   7.460 +    moreover have set_take: "set (take i as') \<subseteq> carrier G"
   7.461 +      using  Cons.prems(5) setparts by auto
   7.462 +    moreover have v1: "wfactors G (take i as' @ drop (Suc i) as') (aa_1 \<otimes> aa_2)"
   7.463 +      using aa1fs aa2fs \<open>set as' \<subseteq> carrier G\<close> by (force simp add: dest: in_set_takeD in_set_dropD)
   7.464 +    ultimately have v1': "wfactors G (as'!i # take i as' @ drop (Suc i) as') (as'!i \<otimes> (aa_1 \<otimes> aa_2))"
   7.465 +      using irrasi wfactors_mult_single
   7.466 +        by (simp add: irrasi v1 wfactors_mult_single)      
   7.467 +    have "wfactors G (as'!i # drop (Suc i) as') (as'!i \<otimes> aa_2)"
   7.468 +      by (simp add: aa2fs irrasi set_drop wfactors_mult_single)
   7.469 +    with len  aa1carr aa2carr aa1fs
   7.470      have v2: "wfactors G (take i as' @ as'!i # drop (Suc i) as') (aa_1 \<otimes> (as'!i \<otimes> aa_2))"
   7.471 -      using wfactors_mult by auto
   7.472 +      using wfactors_mult  by (simp add: set_take set_drop) 
   7.473      from len have as': "as' = (take i as' @ as'!i # drop (Suc i) as')"
   7.474        by (simp add: Cons_nth_drop_Suc)
   7.475 -    with carr have eer: "essentially_equal G (take i as' @ as'!i # drop (Suc i) as') as'"
   7.476 -      by simp
   7.477 -    with v2 afs' carr aa1carr aa2carr nth_mem[OF len] have "aa_1 \<otimes> (as'!i \<otimes> aa_2) \<sim> a"
   7.478 -      by (metis as' ee_wfactorsD m_closed)
   7.479 +    have eer: "essentially_equal G (take i as' @ as'!i # drop (Suc i) as') as'"
   7.480 +      using Cons.prems(5) as' by auto
   7.481 +    with v2 aa1carr aa2carr nth_mem[OF len] have "aa_1 \<otimes> (as'!i \<otimes> aa_2) \<sim> a"
   7.482 +      using Cons.prems as' comm_monoid_cancel.ee_wfactorsD is_comm_monoid_cancel by fastforce
   7.483      then have t1: "as'!i \<otimes> (aa_1 \<otimes> aa_2) \<sim> a"
   7.484        by (metis aa1carr aa2carr asicarr m_lcomm)
   7.485 -    from carr asiah have "ah \<otimes> (aa_1 \<otimes> aa_2) \<sim> as'!i \<otimes> (aa_1 \<otimes> aa_2)"
   7.486 -      by (metis associated_sym m_closed mult_cong_l)
   7.487 +    from asiah have "ah \<otimes> (aa_1 \<otimes> aa_2) \<sim> as'!i \<otimes> (aa_1 \<otimes> aa_2)"
   7.488 +      by (simp add: \<open>ah \<in> carrier G\<close> associated_sym mult_cong_l)
   7.489      also note t1
   7.490 -    finally have "ah \<otimes> (aa_1 \<otimes> aa_2) \<sim> a" by simp
   7.491 -
   7.492 -    with carr aa1carr aa2carr a'carr nth_mem[OF len] have a': "aa_1 \<otimes> aa_2 \<sim> a'"
   7.493 -      by (simp add: a, fast intro: assoc_l_cancel[of ah _ a'])
   7.494 -
   7.495 +    finally have "ah \<otimes> (aa_1 \<otimes> aa_2) \<sim> a"
   7.496 +      using Cons.prems(3) carr_ah aa1carr aa2carr by blast
   7.497 +    with aa1carr aa2carr a'carr nth_mem[OF len] have a': "aa_1 \<otimes> aa_2 \<sim> a'"
   7.498 +      using a assoc_l_cancel carr_ah(1) by blast
   7.499      note v1
   7.500      also note a'
   7.501      finally have "wfactors G (take i as' @ drop (Suc i) as') a'"
   7.502 -      by simp
   7.503 -
   7.504 -    from a'fs this carr have "essentially_equal G as (take i as' @ drop (Suc i) as')"
   7.505 -      by (intro ih[of a']) simp
   7.506 -    then have ee1: "essentially_equal G (ah # as) (ah # take i as' @ drop (Suc i) as')"
   7.507 -      by (elim essentially_equalE) (fastforce intro: essentially_equalI)
   7.508 -
   7.509 -    from carr have ee2: "essentially_equal G (ah # take i as' @ drop (Suc i) as')
   7.510 +      by (simp add: a'carr set_drop set_take)
   7.511 +    from a'fs this have "essentially_equal G as (take i as' @ drop (Suc i) as')"
   7.512 +      using Cons.hyps a'carr carr_ah(2) set_drop set_take by auto
   7.513 +    with carr_ah have ee1: "essentially_equal G (ah # as) (ah # take i as' @ drop (Suc i) as')"
   7.514 +      by (auto simp: essentially_equal_def)
   7.515 +    have ee2: "essentially_equal G (ah # take i as' @ drop (Suc i) as')
   7.516        (as' ! i # take i as' @ drop (Suc i) as')"
   7.517      proof (intro essentially_equalI)
   7.518        show "ah # take i as' @ drop (Suc i) as' <~~> ah # take i as' @ drop (Suc i) as'"
   7.519          by simp
   7.520      next
   7.521        show "ah # take i as' @ drop (Suc i) as' [\<sim>] as' ! i # take i as' @ drop (Suc i) as'"
   7.522 -        by (simp add: list_all2_append) (simp add: asiah[symmetric])
   7.523 +        by (simp add: asiah associated_sym set_drop set_take)
   7.524      qed
   7.525  
   7.526      note ee1
   7.527      also note ee2
   7.528      also have "essentially_equal G (as' ! i # take i as' @ drop (Suc i) as')
   7.529                                     (take i as' @ as' ! i # drop (Suc i) as')"
   7.530 -      by (metis as' as'carr listassoc_refl essentially_equalI perm_append_Cons)
   7.531 +      by (metis Cons.prems(5) as' essentially_equalI listassoc_refl perm_append_Cons)
   7.532      finally have "essentially_equal G (ah # as) (take i as' @ as' ! i # drop (Suc i) as')"
   7.533 -      by simp
   7.534 -    then show "essentially_equal G (ah # as) as'"
   7.535 -      by (subst as')
   7.536 -  qed
   7.537 +      using Cons.prems(4) set_drop set_take by auto
   7.538 +    then show ?case
   7.539 +      using as' by auto
   7.540  qed
   7.541  
   7.542 -lemma (in primeness_condition_monoid) wfactors_unique:
   7.543 -  assumes "wfactors G as a"  "wfactors G as' a"
   7.544 -    and "a \<in> carrier G"  "set as \<subseteq> carrier G"  "set as' \<subseteq> carrier G"
   7.545 -  shows "essentially_equal G as as'"
   7.546 -  by (rule wfactors_unique__hlp_induct[rule_format, of a]) (simp add: assms)
   7.547 -
   7.548  
   7.549  subsubsection \<open>Application to factorial monoids\<close>
   7.550  
   7.551 @@ -2841,7 +2774,6 @@
   7.552      by blast
   7.553  
   7.554    note [simp] = acarr bcarr ccarr ascarr cscarr
   7.555 -
   7.556    assume b: "b = a \<otimes> c"
   7.557    from afs cfs have "wfactors G (as@cs) (a \<otimes> c)"
   7.558      by (intro wfactors_mult) simp_all
   7.559 @@ -2918,9 +2850,7 @@
   7.560    apply unfold_locales
   7.561    apply (rule wfUNIVI)
   7.562    apply (rule measure_induct[of "factorcount G"])
   7.563 -  apply simp
   7.564 -  apply (metis properfactor_fcount)
   7.565 -  done
   7.566 +  using properfactor_fcount by auto
   7.567  
   7.568  sublocale factorial_monoid \<subseteq> primeness_condition_monoid
   7.569    by standard (rule irreducible_prime)
     8.1 --- a/src/HOL/Algebra/Embedded_Algebras.thy	Sun Jul 29 13:18:10 2018 +0200
     8.2 +++ b/src/HOL/Algebra/Embedded_Algebras.thy	Sun Jul 29 18:24:47 2018 +0200
     8.3 @@ -187,7 +187,7 @@
     8.4  
     8.5  corollary Span_is_add_subgroup:
     8.6    "set Us \<subseteq> carrier R \<Longrightarrow> subgroup (Span K Us) (add_monoid R)"
     8.7 -  using line_extension_is_subgroup add.normal_invE(1)[OF add.one_is_normal] by (induct Us) (auto)
     8.8 +  using line_extension_is_subgroup normal_imp_subgroup[OF add.one_is_normal] by (induct Us) (auto)
     8.9  
    8.10  lemma line_extension_smult_closed:
    8.11    assumes "\<And>k v. \<lbrakk> k \<in> K; v \<in> E \<rbrakk> \<Longrightarrow> k \<otimes> v \<in> E" and "E \<subseteq> carrier R" "a \<in> carrier R"
    8.12 @@ -246,7 +246,7 @@
    8.13  
    8.14  lemma line_extension_of_combine_set:
    8.15    assumes "u \<in> carrier R"
    8.16 -  shows "line_extension K u { combine Ks Us | Ks. set Ks \<subseteq> K } = 
    8.17 +  shows "line_extension K u { combine Ks Us | Ks. set Ks \<subseteq> K } =
    8.18                  { combine Ks (u # Us) | Ks. set Ks \<subseteq> K }"
    8.19    (is "?line_extension = ?combinations")
    8.20  proof
    8.21 @@ -292,7 +292,7 @@
    8.22  
    8.23  lemma line_extension_of_combine_set_length_version:
    8.24    assumes "u \<in> carrier R"
    8.25 -  shows "line_extension K u { combine Ks Us | Ks. length Ks = length Us \<and> set Ks \<subseteq> K } = 
    8.26 +  shows "line_extension K u { combine Ks Us | Ks. length Ks = length Us \<and> set Ks \<subseteq> K } =
    8.27                        { combine Ks (u # Us) | Ks. length Ks = length (u # Us) \<and> set Ks \<subseteq> K }"
    8.28    (is "?line_extension = ?combinations")
    8.29  proof
    8.30 @@ -329,16 +329,16 @@
    8.31    assumes "set Us \<subseteq> carrier R" and "a \<in> carrier R"
    8.32    shows "a \<in> Span K Us \<longleftrightarrow> (\<exists>k \<in> K - { \<zero> }. \<exists>Ks. set Ks \<subseteq> K \<and> combine (k # Ks) (a # Us) = \<zero>)"
    8.33           (is "?in_Span \<longleftrightarrow> ?exists_combine")
    8.34 -proof 
    8.35 +proof
    8.36    assume "?in_Span"
    8.37    then obtain Ks where Ks: "set Ks \<subseteq> K" "a = combine Ks Us"
    8.38      using Span_eq_combine_set[OF assms(1)] by auto
    8.39    hence "((\<ominus> \<one>) \<otimes> a) \<oplus> a = combine ((\<ominus> \<one>) # Ks) (a # Us)"
    8.40      by auto
    8.41    moreover have "((\<ominus> \<one>) \<otimes> a) \<oplus> a = \<zero>"
    8.42 -    using assms(2) l_minus l_neg by auto  
    8.43 +    using assms(2) l_minus l_neg by auto
    8.44    moreover have "\<ominus> \<one> \<noteq> \<zero>"
    8.45 -    using subfieldE(6)[OF K] l_neg by force 
    8.46 +    using subfieldE(6)[OF K] l_neg by force
    8.47    ultimately show "?exists_combine"
    8.48      using subring_props(3,5) Ks(1) by (force simp del: combine.simps)
    8.49  next
    8.50 @@ -391,14 +391,14 @@
    8.51      proof (induct Ks Us rule: combine.induct)
    8.52        case (1 k Ks u Us)
    8.53        hence "k \<in> K" and "u \<in> set (u # Us)" by auto
    8.54 -      hence "k \<otimes> u \<in> E" 
    8.55 +      hence "k \<otimes> u \<in> E"
    8.56          using 1(4) unfolding set_mult_def by auto
    8.57        moreover have "K <#> set Us \<subseteq> E"
    8.58          using 1(4) unfolding set_mult_def by auto
    8.59        hence "combine Ks Us \<in> E"
    8.60          using 1 by auto
    8.61        ultimately show ?case
    8.62 -        using add.subgroupE(4)[OF assms(2)] by auto 
    8.63 +        using add.subgroupE(4)[OF assms(2)] by auto
    8.64      next
    8.65        case "2_1" thus ?case
    8.66          using subgroup.one_closed[OF assms(2)] by auto
    8.67 @@ -436,7 +436,7 @@
    8.68        hence "combine [ k ] (u # Us) \<in> Span K (u # Us)"
    8.69          using Span_eq_combine_set[OF Cons(2)] by (auto simp del: combine.simps)
    8.70        moreover have "k \<in> carrier R" and "u \<in> carrier R"
    8.71 -        using Cons(2) k subring_props(1) by (blast, auto) 
    8.72 +        using Cons(2) k subring_props(1) by (blast, auto)
    8.73        ultimately show "k \<otimes> u \<in> Span K (u # Us)"
    8.74          by (auto simp del: Span.simps)
    8.75      qed
    8.76 @@ -455,7 +455,7 @@
    8.77  corollary Span_same_set:
    8.78    assumes "set Us \<subseteq> carrier R"
    8.79    shows "set Us = set Vs \<Longrightarrow> Span K Us = Span K Vs"
    8.80 -  using Span_eq_generate assms by auto 
    8.81 +  using Span_eq_generate assms by auto
    8.82  
    8.83  corollary Span_incl: "set Us \<subseteq> carrier R \<Longrightarrow> K <#> (set Us) \<subseteq> Span K Us"
    8.84    using Span_eq_generate generate.incl[of _ _ "add_monoid R"] by auto
    8.85 @@ -583,7 +583,7 @@
    8.86    moreover have "Span K Us \<subseteq> Span K (u # Us)"
    8.87      using mono_Span independent_in_carrier[OF assms] by auto
    8.88    ultimately show ?thesis
    8.89 -    using independent_backwards(1)[OF assms] by auto 
    8.90 +    using independent_backwards(1)[OF assms] by auto
    8.91  qed
    8.92  
    8.93  corollary independent_replacement:
    8.94 @@ -624,7 +624,7 @@
    8.95    from assms show "Span K Us \<inter> Span K Vs = { \<zero> }"
    8.96    proof (induct Us rule: list.induct)
    8.97      case Nil thus ?case
    8.98 -      using Span_subgroup_props(2)[OF independent_in_carrier[of K Vs]] by simp 
    8.99 +      using Span_subgroup_props(2)[OF independent_in_carrier[of K Vs]] by simp
   8.100    next
   8.101      case (Cons u Us)
   8.102      hence IH: "Span K Us \<inter> Span K Vs = {\<zero>}" by auto
   8.103 @@ -653,7 +653,7 @@
   8.104        hence "k \<otimes> u = (\<ominus> u') \<oplus> v'"
   8.105          using in_carrier(1) k(2) u'(2) v'(2) add.m_comm r_neg1 by auto
   8.106        hence "k \<otimes> u \<in> Span K (Us @ Vs)"
   8.107 -        using Span_subgroup_props(4)[OF in_carrier(2) u'(1)] v'(1) 
   8.108 +        using Span_subgroup_props(4)[OF in_carrier(2) u'(1)] v'(1)
   8.109                Span_append_eq_set_add[OF in_carrier(2-3)] unfolding set_add_def' by blast
   8.110        hence "u \<in> Span K (Us @ Vs)"
   8.111          using Cons(2) Span_m_inv_simprule[OF _ _ in_carrier(1), of "Us @ Vs" k]
   8.112 @@ -678,7 +678,7 @@
   8.113    hence in_carrier:
   8.114      "u \<in> carrier R" "set Us \<subseteq> carrier R" "set Vs \<subseteq> carrier R" "set (u # Us) \<subseteq> carrier R"
   8.115      using Cons(2-3)[THEN independent_in_carrier] by auto
   8.116 -  hence "Span K Us \<subseteq> Span K (u # Us)" 
   8.117 +  hence "Span K Us \<subseteq> Span K (u # Us)"
   8.118      using mono_Span by auto
   8.119    hence "Span K Us \<inter> Span K Vs = { \<zero> }"
   8.120      using Cons(4) Span_subgroup_props(2)[OF in_carrier(2)] by auto
   8.121 @@ -733,7 +733,7 @@
   8.122      hence "combine Ks' Us = \<zero>"
   8.123        using combine_in_carrier[OF _ Us, of Ks'] Ks' u Cons(3) subring_props(1) unfolding Ks by auto
   8.124      hence "set (take (length Us) Ks') \<subseteq> { \<zero> }"
   8.125 -      using Cons(1)[OF Ks' _ independent_backwards(2)[OF Cons(4)]] by simp 
   8.126 +      using Cons(1)[OF Ks' _ independent_backwards(2)[OF Cons(4)]] by simp
   8.127      thus ?thesis
   8.128        using k_zero unfolding Ks by auto
   8.129    qed
   8.130 @@ -878,10 +878,10 @@
   8.131      case (Cons u Us)
   8.132      then obtain Vs' Vs'' where Vs: "Vs = Vs' @ (u # Vs'')"
   8.133        by (metis list.set_intros(1) split_list)
   8.134 -    
   8.135 +
   8.136      have in_carrier: "u \<in> carrier R" "set Us \<subseteq> carrier R"
   8.137 -      using independent_in_carrier[OF Cons(2)] by auto 
   8.138 -    
   8.139 +      using independent_in_carrier[OF Cons(2)] by auto
   8.140 +
   8.141      have "distinct Vs"
   8.142        using Cons(3-4) independent_distinct[OF Cons(2)]
   8.143        by (metis card_distinct distinct_card)
   8.144 @@ -905,7 +905,7 @@
   8.145    shows "\<exists>Vs'. set Vs' \<subseteq> set Vs \<and> length Vs' = length Us' \<and> independent K (Vs' @ Us)"
   8.146    using assms
   8.147  proof (induct "length Us'" arbitrary: Us' Us)
   8.148 -  case 0 thus ?case by auto 
   8.149 +  case 0 thus ?case by auto
   8.150  next
   8.151    case (Suc n)
   8.152    then obtain u Us'' where Us'': "Us' = Us'' @ [u]"
   8.153 @@ -1074,9 +1074,9 @@
   8.154          using space_subgroup_props(1)[OF assms(1)] li_Cons[OF _ v(2) step(4)] by auto
   8.155        then obtain Vs
   8.156          where "length (Vs @ (v # Us)) = n" "independent K (Vs @ (v # Us))" "Span K (Vs @ (v # Us)) = E"
   8.157 -        using step(3)[of "v # Us"] step(1-2,4-6) v by auto 
   8.158 +        using step(3)[of "v # Us"] step(1-2,4-6) v by auto
   8.159        thus ?case
   8.160 -        by (metis append.assoc append_Cons append_Nil)  
   8.161 +        by (metis append.assoc append_Cons append_Nil)
   8.162      qed } note aux_lemma = this
   8.163  
   8.164    have "length Us \<le> n"
   8.165 @@ -1119,7 +1119,7 @@
   8.166    hence in_carrier: "set Us \<subseteq> carrier R" "set (Vs @ Bs) \<subseteq> carrier R"
   8.167      using independent_in_carrier[OF Us(2)] independent_in_carrier[OF Vs(2)] by auto
   8.168    hence "Span K Us \<inter> (Span K (Vs @ Bs)) \<subseteq> Span K Bs"
   8.169 -    using Bs(4) Us(3) Vs(3) mono_Span_append(1)[OF _ Bs(1), of Us] by auto 
   8.170 +    using Bs(4) Us(3) Vs(3) mono_Span_append(1)[OF _ Bs(1), of Us] by auto
   8.171    hence "Span K Us \<inter> (Span K (Vs @ Bs)) \<subseteq> { \<zero> }"
   8.172      using independent_split(3)[OF Us(2)] by blast
   8.173    hence "Span K Us \<inter> (Span K (Vs @ Bs)) = { \<zero> }"
   8.174 @@ -1147,7 +1147,7 @@
   8.175      ultimately show "v \<in> (Span K Us) <+>\<^bsub>R\<^esub> F"
   8.176        using u1' unfolding set_add_def' by auto
   8.177    qed
   8.178 -  ultimately have "Span K (Us @ (Vs @ Bs)) = E <+>\<^bsub>R\<^esub> F" 
   8.179 +  ultimately have "Span K (Us @ (Vs @ Bs)) = E <+>\<^bsub>R\<^esub> F"
   8.180      using Span_append_eq_set_add[OF in_carrier] Vs(3) by auto
   8.181  
   8.182    thus ?thesis using dim by simp
   8.183 @@ -1169,7 +1169,7 @@
   8.184      by (metis One_nat_def length_0_conv length_Suc_conv)
   8.185    have in_carrier: "set (map (\<lambda>u'. u' \<otimes> u) Us) \<subseteq> carrier R"
   8.186      using Us(1) u(1) by (induct Us) (auto)
   8.187 -  
   8.188 +
   8.189    have li: "independent K (map (\<lambda>u'. u' \<otimes> u) Us)"
   8.190    proof (rule trivial_combine_imp_independent[OF assms(1) in_carrier])
   8.191      fix Ks assume Ks: "set Ks \<subseteq> K" and "combine Ks (map (\<lambda>u'. u' \<otimes> u) Us) = \<zero>"
   8.192 @@ -1244,7 +1244,7 @@
   8.193    ultimately have "dimension (n * Suc m) K (Span F [ v ] <+>\<^bsub>R\<^esub> Span F Vs')"
   8.194      using dimension_direct_sum_space[OF assms(1) _ _ inter] by auto
   8.195    thus "dimension (n * Suc m) K E"
   8.196 -    using Span_append_eq_set_add[OF assms(2) li[THEN independent_in_carrier]] Vs(4) v by auto 
   8.197 +    using Span_append_eq_set_add[OF assms(2) li[THEN independent_in_carrier]] Vs(4) v by auto
   8.198  qed
   8.199  
   8.200  
   8.201 @@ -1271,14 +1271,14 @@
   8.202    hence "combine Ks Us = (combine (take (length Us) Ks) Us) \<oplus> \<zero>"
   8.203      using combine_append[OF _ _ assms(2), of "take (length Us) Ks" "drop (length Us) Ks" "[]"] len by auto
   8.204    also have " ... = combine (take (length Us) Ks) Us"
   8.205 -    using combine_in_carrier[OF set_t assms(2)] by auto 
   8.206 +    using combine_in_carrier[OF set_t assms(2)] by auto
   8.207    finally show "combine Ks Us = combine (take (length Us) Ks) Us" .
   8.208  qed
   8.209  *)
   8.210  
   8.211  (*
   8.212  lemma combine_normalize:
   8.213 -  assumes "set Ks \<subseteq> K" "set Us \<subseteq> carrier R" "a = combine Ks Us" 
   8.214 +  assumes "set Ks \<subseteq> K" "set Us \<subseteq> carrier R" "a = combine Ks Us"
   8.215    shows "\<exists>Ks'. set Ks' \<subseteq> K \<and> length Ks' = length Us \<and> a = combine Ks' Us"
   8.216  proof (cases "length Ks \<le> length Us")
   8.217    assume "\<not> length Ks \<le> length Us"
   8.218 @@ -1291,12 +1291,12 @@
   8.219  next
   8.220    assume len: "length Ks \<le> length Us"
   8.221    have Ks: "set Ks \<subseteq> carrier R" and set_r: "set (replicate (length Us - length Ks) \<zero>) \<subseteq> carrier R"
   8.222 -    using assms subring_props(1) zero_closed by (metis dual_order.trans, auto) 
   8.223 +    using assms subring_props(1) zero_closed by (metis dual_order.trans, auto)
   8.224    moreover
   8.225    have set_t: "set (take (length Ks) Us) \<subseteq> carrier R"
   8.226     and set_d: "set (drop (length Ks) Us) \<subseteq> carrier R"
   8.227      using assms(2) len dual_order.trans by (metis set_take_subset, metis set_drop_subset)
   8.228 -  ultimately 
   8.229 +  ultimately
   8.230    have "combine (Ks @ (replicate (length Us - length Ks) \<zero>)) Us =
   8.231         (combine Ks (take (length Ks) Us)) \<oplus>
   8.232         (combine (replicate (length Us - length Ks) \<zero>) (drop (length Ks) Us))"
     9.1 --- a/src/HOL/Algebra/Generated_Groups.thy	Sun Jul 29 13:18:10 2018 +0200
     9.2 +++ b/src/HOL/Algebra/Generated_Groups.thy	Sun Jul 29 18:24:47 2018 +0200
     9.3 @@ -466,7 +466,7 @@
     9.4    shows "derived G H \<lhd> G" unfolding derived_def
     9.5  proof (rule normal_generateI)
     9.6    show "(\<Union>h1 \<in> H. \<Union>h2 \<in> H. { h1 \<otimes> h2 \<otimes> inv h1 \<otimes> inv h2 }) \<subseteq> carrier G"
     9.7 -    using subgroup.subset assms normal_invE(1) by blast
     9.8 +    using subgroup.subset assms normal_imp_subgroup by blast
     9.9  next
    9.10    show "\<And>h g. \<lbrakk> h \<in> derived_set G H; g \<in> carrier G \<rbrakk> \<Longrightarrow> g \<otimes> h \<otimes> inv g \<in> derived_set G H"
    9.11    proof -
    9.12 @@ -474,7 +474,7 @@
    9.13      then obtain h1 h2 where h1: "h1 \<in> H" "h1 \<in> carrier G"
    9.14                          and h2: "h2 \<in> H" "h2 \<in> carrier G"
    9.15                          and h:  "h = h1 \<otimes> h2 \<otimes> inv h1 \<otimes> inv h2"
    9.16 -      using subgroup.subset assms normal_invE(1) by blast
    9.17 +      using subgroup.subset assms normal_imp_subgroup by blast
    9.18      hence "g \<otimes> h \<otimes> inv g =
    9.19             g \<otimes> h1 \<otimes> (inv g \<otimes> g) \<otimes> h2 \<otimes> (inv g \<otimes> g) \<otimes> inv h1 \<otimes> (inv g \<otimes> g) \<otimes> inv h2 \<otimes> inv g"
    9.20        by (simp add: g m_assoc)
    9.21 @@ -486,8 +486,8 @@
    9.22      have "g \<otimes> h \<otimes> inv g =
    9.23           (g \<otimes> h1 \<otimes> inv g) \<otimes> (g \<otimes> h2 \<otimes> inv g) \<otimes> inv (g \<otimes> h1 \<otimes> inv g) \<otimes> inv (g \<otimes> h2 \<otimes> inv g)"
    9.24        by (simp add: g h1 h2 inv_mult_group m_assoc)
    9.25 -    moreover have "g \<otimes> h1 \<otimes> inv g \<in> H" by (simp add: assms normal_invE(2) g h1)
    9.26 -    moreover have "g \<otimes> h2 \<otimes> inv g \<in> H" by (simp add: assms normal_invE(2) g h2)
    9.27 +    moreover have "g \<otimes> h1 \<otimes> inv g \<in> H" by (simp add: assms normal.inv_op_closed2 g h1)
    9.28 +    moreover have "g \<otimes> h2 \<otimes> inv g \<in> H" by (simp add: assms normal.inv_op_closed2 g h2)
    9.29      ultimately show "g \<otimes> h \<otimes> inv g \<in> derived_set G H" by blast
    9.30    qed
    9.31  qed
    10.1 --- a/src/HOL/Algebra/Group.thy	Sun Jul 29 13:18:10 2018 +0200
    10.2 +++ b/src/HOL/Algebra/Group.thy	Sun Jul 29 18:24:47 2018 +0200
    10.3 @@ -763,13 +763,13 @@
    10.4      and "subgroup I K"
    10.5    shows "subgroup (H \<times> I) (G \<times>\<times> K)"
    10.6  proof (intro group.group_incl_imp_subgroup[OF DirProd_group[OF assms(1)assms(3)]])
    10.7 -  have "H \<subseteq> carrier G" "I \<subseteq> carrier K" using subgroup.subset assms apply blast+.
    10.8 +  have "H \<subseteq> carrier G" "I \<subseteq> carrier K" using subgroup.subset assms by blast+
    10.9    thus "(H \<times> I) \<subseteq> carrier (G \<times>\<times> K)" unfolding DirProd_def by auto
   10.10    have "Group.group ((G\<lparr>carrier := H\<rparr>) \<times>\<times> (K\<lparr>carrier := I\<rparr>))"
   10.11      using DirProd_group[OF subgroup.subgroup_is_group[OF assms(2)assms(1)]
   10.12          subgroup.subgroup_is_group[OF assms(4)assms(3)]].
   10.13    moreover have "((G\<lparr>carrier := H\<rparr>) \<times>\<times> (K\<lparr>carrier := I\<rparr>)) = ((G \<times>\<times> K)\<lparr>carrier := H \<times> I\<rparr>)"
   10.14 -    unfolding DirProd_def using assms apply simp.
   10.15 +    unfolding DirProd_def using assms by simp
   10.16    ultimately show "Group.group ((G \<times>\<times> K)\<lparr>carrier := H \<times> I\<rparr>)" by simp
   10.17  qed
   10.18  
   10.19 @@ -1054,7 +1054,7 @@
   10.20  lemma (in group_hom) img_is_subgroup: "subgroup (h ` (carrier G)) H"
   10.21    apply (rule subgroupI)
   10.22    apply (auto simp add: image_subsetI)
   10.23 -  apply (metis (no_types, hide_lams) G.inv_closed hom_inv image_iff)
   10.24 +  apply (metis G.inv_closed hom_inv image_iff)
   10.25    by (metis G.monoid_axioms hom_mult image_eqI monoid.m_closed)
   10.26  
   10.27  lemma (in group_hom) subgroup_img_is_subgroup:
   10.28 @@ -1157,9 +1157,8 @@
   10.29    show "monoid (G\<lparr>carrier := H\<rparr>)"
   10.30      using submonoid.submonoid_is_monoid assms comm_monoid_axioms comm_monoid_def by blast
   10.31    show "\<And>x y. x \<in> carrier (G\<lparr>carrier := H\<rparr>) \<Longrightarrow> y \<in> carrier (G\<lparr>carrier := H\<rparr>)
   10.32 -        \<Longrightarrow> x \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> y = y \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> x" apply simp
   10.33 -    using  assms comm_monoid_axioms_def submonoid.mem_carrier
   10.34 -    by (metis m_comm)
   10.35 +        \<Longrightarrow> x \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> y = y \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> x" 
   10.36 +    by simp (meson assms m_comm submonoid.mem_carrier)
   10.37  qed
   10.38  
   10.39  locale comm_group = comm_monoid + group
    11.1 --- a/src/HOL/Algebra/Ideal.thy	Sun Jul 29 13:18:10 2018 +0200
    11.2 +++ b/src/HOL/Algebra/Ideal.thy	Sun Jul 29 18:24:47 2018 +0200
    11.3 @@ -128,10 +128,9 @@
    11.4  proof -
    11.5    interpret additive_subgroup I R by fact
    11.6    interpret cring R by fact
    11.7 -  show ?thesis apply intro_locales
    11.8 -    apply (intro ideal_axioms.intro)
    11.9 -    apply (erule (1) I_l_closed)
   11.10 -    apply (erule (1) I_r_closed)
   11.11 +  show ?thesis
   11.12 +    apply intro_locales
   11.13 +    apply (simp add: I_l_closed I_r_closed ideal_axioms_def)
   11.14      by (simp add: I_notcarr I_prime primeideal_axioms.intro)
   11.15  qed
   11.16  
    12.1 --- a/src/HOL/Algebra/RingHom.thy	Sun Jul 29 13:18:10 2018 +0200
    12.2 +++ b/src/HOL/Algebra/RingHom.thy	Sun Jul 29 18:24:47 2018 +0200
    12.3 @@ -20,11 +20,10 @@
    12.4    by standard (rule homh)
    12.5  
    12.6  sublocale ring_hom_ring \<subseteq> abelian_group?: abelian_group_hom R S
    12.7 -apply (intro abelian_group_homI R.is_abelian_group S.is_abelian_group)
    12.8 -apply (intro group_hom.intro group_hom_axioms.intro R.a_group S.a_group)
    12.9 -apply (insert homh, unfold hom_def ring_hom_def)
   12.10 -apply simp
   12.11 -done
   12.12 +proof 
   12.13 +  show "h \<in> hom (add_monoid R) (add_monoid S)"
   12.14 +    using homh by (simp add: hom_def ring_hom_def)
   12.15 +qed
   12.16  
   12.17  lemma (in ring_hom_ring) is_ring_hom_ring:
   12.18    "ring_hom_ring R S h"
   12.19 @@ -33,8 +32,7 @@
   12.20  lemma ring_hom_ringI:
   12.21    fixes R (structure) and S (structure)
   12.22    assumes "ring R" "ring S"
   12.23 -  assumes (* morphism: "h \<in> carrier R \<rightarrow> carrier S" *)
   12.24 -          hom_closed: "!!x. x \<in> carrier R ==> h x \<in> carrier S"
   12.25 +  assumes hom_closed: "!!x. x \<in> carrier R ==> h x \<in> carrier S"
   12.26        and compatible_mult: "\<And>x y. [| x \<in> carrier R; y \<in> carrier R |] ==> h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y"
   12.27        and compatible_add: "\<And>x y. [| x \<in> carrier R; y \<in> carrier R |] ==> h (x \<oplus> y) = h x \<oplus>\<^bsub>S\<^esub> h y"
   12.28        and compatible_one: "h \<one> = \<one>\<^bsub>S\<^esub>"
   12.29 @@ -42,13 +40,12 @@
   12.30  proof -
   12.31    interpret ring R by fact
   12.32    interpret ring S by fact
   12.33 -  show ?thesis apply unfold_locales
   12.34 -apply (unfold ring_hom_def, safe)
   12.35 -   apply (simp add: hom_closed Pi_def)
   12.36 -  apply (erule (1) compatible_mult)
   12.37 - apply (erule (1) compatible_add)
   12.38 -apply (rule compatible_one)
   12.39 -done
   12.40 +  show ?thesis
   12.41 +  proof
   12.42 +    show "h \<in> ring_hom R S"
   12.43 +      unfolding ring_hom_def
   12.44 +      by (auto simp: compatible_mult compatible_add compatible_one hom_closed)
   12.45 +  qed
   12.46  qed
   12.47  
   12.48  lemma ring_hom_ringI2:
   12.49 @@ -58,11 +55,11 @@
   12.50  proof -
   12.51    interpret R: ring R by fact
   12.52    interpret S: ring S by fact
   12.53 -  show ?thesis apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro)
   12.54 -    apply (rule R.is_ring)
   12.55 -    apply (rule S.is_ring)
   12.56 -    apply (rule h)
   12.57 -    done
   12.58 +  show ?thesis 
   12.59 +  proof
   12.60 +    show "h \<in> ring_hom R S"
   12.61 +      using h .
   12.62 +  qed
   12.63  qed
   12.64  
   12.65  lemma ring_hom_ringI3:
   12.66 @@ -75,13 +72,11 @@
   12.67    interpret abelian_group_hom R S h by fact
   12.68    interpret R: ring R by fact
   12.69    interpret S: ring S by fact
   12.70 -  show ?thesis apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro, rule R.is_ring, rule S.is_ring)
   12.71 -    apply (insert group_hom.homh[OF a_group_hom])
   12.72 -    apply (unfold hom_def ring_hom_def, simp)
   12.73 -    apply safe
   12.74 -    apply (erule (1) compatible_mult)
   12.75 -    apply (rule compatible_one)
   12.76 -    done
   12.77 +  show ?thesis
   12.78 +  proof
   12.79 +    show "h \<in> ring_hom R S"
   12.80 +      unfolding ring_hom_def by (auto simp: compatible_one compatible_mult)
   12.81 +  qed
   12.82  qed
   12.83  
   12.84  lemma ring_hom_cringI:
   12.85 @@ -91,21 +86,22 @@
   12.86    interpret ring_hom_ring R S h by fact
   12.87    interpret R: cring R by fact
   12.88    interpret S: cring S by fact
   12.89 -  show ?thesis by (intro ring_hom_cring.intro ring_hom_cring_axioms.intro)
   12.90 -    (rule R.is_cring, rule S.is_cring, rule homh)
   12.91 +  show ?thesis 
   12.92 +  proof
   12.93 +    show "h \<in> ring_hom R S"
   12.94 +      by (simp add: homh)
   12.95 +  qed
   12.96  qed
   12.97  
   12.98  
   12.99  subsection \<open>The Kernel of a Ring Homomorphism\<close>
  12.100  
  12.101  \<comment> \<open>the kernel of a ring homomorphism is an ideal\<close>
  12.102 -lemma (in ring_hom_ring) kernel_is_ideal:
  12.103 -  shows "ideal (a_kernel R S h) R"
  12.104 -apply (rule idealI)
  12.105 -   apply (rule R.is_ring)
  12.106 -  apply (rule additive_subgroup.a_subgroup[OF additive_subgroup_a_kernel])
  12.107 - apply (unfold a_kernel_def', simp+)
  12.108 -done
  12.109 +lemma (in ring_hom_ring) kernel_is_ideal: "ideal (a_kernel R S h) R"
  12.110 +  apply (rule idealI [OF R.is_ring])
  12.111 +    apply (rule additive_subgroup.a_subgroup[OF additive_subgroup_a_kernel])
  12.112 +   apply (auto simp: a_kernel_def')
  12.113 +  done
  12.114  
  12.115  text \<open>Elements of the kernel are mapped to zero\<close>
  12.116  lemma (in abelian_group_hom) kernel_zero [simp]:
  12.117 @@ -174,29 +170,10 @@
  12.118  corollary (in ring_hom_ring) rcos_eq_homeq:
  12.119    assumes acarr: "a \<in> carrier R"
  12.120    shows "(a_kernel R S h) +> a = {x \<in> carrier R. h x = h a}"
  12.121 -  apply rule defer 1
  12.122 -   apply clarsimp defer 1
  12.123 -proof
  12.124 +proof -
  12.125    interpret ideal "a_kernel R S h" "R" by (rule kernel_is_ideal)
  12.126 -
  12.127 -  fix x
  12.128 -  assume xrcos: "x \<in> a_kernel R S h +> a"
  12.129 -  from acarr and this
  12.130 -  have xcarr: "x \<in> carrier R"
  12.131 -    by (rule a_elemrcos_carrier)
  12.132 -
  12.133 -  from xrcos
  12.134 -  have "h x = h a" by (rule rcos_imp_homeq[OF acarr])
  12.135 -  from xcarr and this
  12.136 -  show "x \<in> {x \<in> carrier R. h x = h a}" by fast
  12.137 -next
  12.138 -  interpret ideal "a_kernel R S h" "R" by (rule kernel_is_ideal)
  12.139 -
  12.140 -  fix x
  12.141 -  assume xcarr: "x \<in> carrier R"
  12.142 -    and hx: "h x = h a"
  12.143 -  from acarr xcarr hx
  12.144 -  show "x \<in> a_kernel R S h +> a" by (rule homeq_imp_rcos)
  12.145 +  show ?thesis
  12.146 +    using assms by (auto simp: intro: homeq_imp_rcos rcos_imp_homeq a_elemrcos_carrier)
  12.147  qed
  12.148  
  12.149  lemma (in ring_hom_ring) nat_pow_hom:
    13.1 --- a/src/HOL/Library/FuncSet.thy	Sun Jul 29 13:18:10 2018 +0200
    13.2 +++ b/src/HOL/Library/FuncSet.thy	Sun Jul 29 18:24:47 2018 +0200
    13.3 @@ -163,8 +163,6 @@
    13.4  
    13.5  lemma compose_assoc:
    13.6    assumes "f \<in> A \<rightarrow> B"
    13.7 -    and "g \<in> B \<rightarrow> C"
    13.8 -    and "h \<in> C \<rightarrow> D"
    13.9    shows "compose A h (compose A g f) = compose A (compose B h g) f"
   13.10    using assms by (simp add: fun_eq_iff Pi_def compose_def restrict_def)
   13.11  
    14.1 --- a/src/HOL/Library/datatype_records.ML	Sun Jul 29 13:18:10 2018 +0200
    14.2 +++ b/src/HOL/Library/datatype_records.ML	Sun Jul 29 18:24:47 2018 +0200
    14.3 @@ -7,10 +7,10 @@
    14.4  
    14.5    val mk_update_defs: string -> local_theory -> local_theory
    14.6  
    14.7 -  val bnf_record: binding -> ctr_options -> (binding option * (typ * sort)) list ->
    14.8 +  val record: binding -> ctr_options -> (binding option * (typ * sort)) list ->
    14.9      (binding * typ) list -> local_theory -> local_theory
   14.10  
   14.11 -  val bnf_record_cmd: binding -> ctr_options_cmd ->
   14.12 +  val record_cmd: binding -> ctr_options_cmd ->
   14.13      (binding option * (string * string option)) list -> (binding * string) list -> local_theory ->
   14.14      local_theory
   14.15  
   14.16 @@ -35,21 +35,31 @@
   14.17    val extend = I
   14.18  )
   14.19  
   14.20 +fun mk_eq_dummy (lhs, rhs) =
   14.21 +  Const (@{const_name HOL.eq}, dummyT --> dummyT --> @{typ bool}) $ lhs $ rhs
   14.22 +
   14.23 +val dummify = map_types (K dummyT)
   14.24 +fun repeat_split_tac ctxt thm = REPEAT_ALL_NEW (CHANGED o Splitter.split_tac ctxt [thm])
   14.25 +
   14.26  fun mk_update_defs typ_name lthy =
   14.27    let
   14.28      val short_name = Long_Name.base_name typ_name
   14.29 +    val {ctrs, casex, selss, split, sel_thmss, injects, ...} =
   14.30 +      the (Ctr_Sugar.ctr_sugar_of lthy typ_name)
   14.31 +    val ctr = case ctrs of [ctr] => ctr | _ => error "Datatype_Records.mk_update_defs: expected only single constructor"
   14.32 +    val sels = case selss of [sels] => sels | _ => error "Datatype_Records.mk_update_defs: expected selectors"
   14.33 +    val sels_dummy = map dummify sels
   14.34 +    val ctr_dummy = dummify ctr
   14.35 +    val casex_dummy = dummify casex
   14.36 +    val len = length sels
   14.37  
   14.38 -    val {ctrs, casex, selss, ...} = the (Ctr_Sugar.ctr_sugar_of lthy typ_name)
   14.39 -    val ctr = case ctrs of [ctr] => ctr | _ => error "BNF_Record.mk_update_defs: expected only single constructor"
   14.40 -    val sels = case selss of [sels] => sels | _ => error "BNF_Record.mk_update_defs: expected selectors"
   14.41 -    val ctr_dummy = Const (fst (dest_Const ctr), dummyT)
   14.42 -    val casex_dummy = Const (fst (dest_Const casex), dummyT)
   14.43 -
   14.44 -    val len = length sels
   14.45 +    val simp_thms = flat sel_thmss @ injects
   14.46  
   14.47      fun mk_name sel =
   14.48        Binding.name ("update_" ^ Long_Name.base_name (fst (dest_Const sel)))
   14.49  
   14.50 +    val thms_binding = (@{binding record_simps}, @{attributes [simp]})
   14.51 +
   14.52      fun mk_t idx =
   14.53        let
   14.54          val body =
   14.55 @@ -59,22 +69,143 @@
   14.56          Abs ("f", dummyT, casex_dummy $ body)
   14.57        end
   14.58  
   14.59 -    fun define name t =
   14.60 -      Local_Theory.define ((name, NoSyn), ((Binding.empty, @{attributes [datatype_record_update, code]}), t)) #> snd
   14.61 +    fun simp_only_tac ctxt =
   14.62 +      REPEAT_ALL_NEW (resolve_tac ctxt @{thms impI allI}) THEN'
   14.63 +        asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps simp_thms)
   14.64 +
   14.65 +    fun prove ctxt defs ts n =
   14.66 +      let
   14.67 +        val t = nth ts n
   14.68 +
   14.69 +        val sel_dummy = nth sels_dummy n
   14.70 +        val t_dummy = dummify t
   14.71 +        fun tac {context = ctxt, ...} =
   14.72 +          Goal.conjunction_tac 1 THEN
   14.73 +            Local_Defs.unfold_tac ctxt defs THEN
   14.74 +            PARALLEL_ALLGOALS (repeat_split_tac ctxt split THEN' simp_only_tac ctxt)
   14.75 +
   14.76 +        val sel_upd_same_thm =
   14.77 +          let
   14.78 +            val ([f, x], ctxt') = Variable.add_fixes ["f", "x"] ctxt
   14.79 +            val f = Free (f, dummyT)
   14.80 +            val x = Free (x, dummyT)
   14.81 +
   14.82 +            val lhs = sel_dummy $ (t_dummy $ f $ x)
   14.83 +            val rhs = f $ (sel_dummy $ x)
   14.84 +            val prop = Syntax.check_term ctxt' (HOLogic.mk_Trueprop (mk_eq_dummy (lhs, rhs)))
   14.85 +          in
   14.86 +            [Goal.prove_future ctxt' [] [] prop tac]
   14.87 +            |> Variable.export ctxt' ctxt
   14.88 +          end
   14.89 +
   14.90 +        val sel_upd_diff_thms =
   14.91 +          let
   14.92 +            val ([f, x], ctxt') = Variable.add_fixes ["f", "x"] ctxt
   14.93 +            val f = Free (f, dummyT)
   14.94 +            val x = Free (x, dummyT)
   14.95 +
   14.96 +            fun lhs sel = sel $ (t_dummy $ f $ x)
   14.97 +            fun rhs sel = sel $ x
   14.98 +            fun eq sel = (lhs sel, rhs sel)
   14.99 +            fun is_n i = i = n
  14.100 +            val props =
  14.101 +              sels_dummy ~~ (0 upto len - 1)
  14.102 +              |> filter_out (is_n o snd)
  14.103 +              |> map (HOLogic.mk_Trueprop o mk_eq_dummy o eq o fst)
  14.104 +              |> Syntax.check_terms ctxt'
  14.105 +          in
  14.106 +            if length props > 0 then
  14.107 +              Goal.prove_common ctxt' (SOME ~1) [] [] props tac
  14.108 +              |> Variable.export ctxt' ctxt
  14.109 +            else
  14.110 +              []
  14.111 +          end
  14.112 +
  14.113 +        val upd_comp_thm =
  14.114 +          let
  14.115 +            val ([f, g, x], ctxt') = Variable.add_fixes ["f", "g", "x"] ctxt
  14.116 +            val f = Free (f, dummyT)
  14.117 +            val g = Free (g, dummyT)
  14.118 +            val x = Free (x, dummyT)
  14.119  
  14.120 -    val lthy' =
  14.121 -      Local_Theory.map_background_naming (Name_Space.qualified_path false (Binding.name short_name)) lthy
  14.122 +            val lhs = t_dummy $ f $ (t_dummy $ g $ x)
  14.123 +            val rhs = t_dummy $ Abs ("a", dummyT, f $ (g $ Bound 0)) $ x
  14.124 +            val prop = Syntax.check_term ctxt' (HOLogic.mk_Trueprop (mk_eq_dummy (lhs, rhs)))
  14.125 +          in
  14.126 +            [Goal.prove_future ctxt' [] [] prop tac]
  14.127 +            |> Variable.export ctxt' ctxt
  14.128 +          end
  14.129 +
  14.130 +        val upd_comm_thms =
  14.131 +          let
  14.132 +            fun prop i ctxt =
  14.133 +              let
  14.134 +                val ([f, g, x], ctxt') = Variable.variant_fixes ["f", "g", "x"] ctxt
  14.135 +                val self = t_dummy $ Free (f, dummyT)
  14.136 +                val other = dummify (nth ts i) $ Free (g, dummyT)
  14.137 +                val lhs = other $ (self $ Free (x, dummyT))
  14.138 +                val rhs = self $ (other $ Free (x, dummyT))
  14.139 +              in
  14.140 +                (HOLogic.mk_Trueprop (mk_eq_dummy (lhs, rhs)), ctxt')
  14.141 +              end
  14.142 +            val (props, ctxt') = fold_map prop (0 upto n - 1) ctxt
  14.143 +            val props = Syntax.check_terms ctxt' props
  14.144 +          in
  14.145 +            if length props > 0 then
  14.146 +              Goal.prove_common ctxt' (SOME ~1) [] [] props tac
  14.147 +              |> Variable.export ctxt' ctxt
  14.148 +            else
  14.149 +              []
  14.150 +          end
  14.151 +
  14.152 +        val upd_sel_thm =
  14.153 +          let
  14.154 +            val ([x], ctxt') = Variable.add_fixes ["x"] ctxt
  14.155 +
  14.156 +            val lhs = t_dummy $ Abs("_", dummyT, (sel_dummy $ Free(x, dummyT))) $ Free (x, dummyT)
  14.157 +            val rhs = Free (x, dummyT)
  14.158 +            val prop = Syntax.check_term ctxt (HOLogic.mk_Trueprop (mk_eq_dummy (lhs, rhs)))
  14.159 +          in
  14.160 +            [Goal.prove_future ctxt [] [] prop tac]
  14.161 +            |> Variable.export ctxt' ctxt
  14.162 +          end
  14.163 +      in
  14.164 +        sel_upd_same_thm @ sel_upd_diff_thms @ upd_comp_thm @ upd_comm_thms @ upd_sel_thm
  14.165 +      end
  14.166 +
  14.167 +    fun define name t =
  14.168 +      Local_Theory.define ((name, NoSyn), ((Binding.empty, @{attributes [datatype_record_update, code]}),t))
  14.169 +      #> apfst (apsnd snd)
  14.170 +
  14.171 +    val (updates, (lthy'', lthy')) =
  14.172 +      lthy
  14.173 +      |> Local_Theory.open_target
  14.174 +      |> snd
  14.175 +      |> Local_Theory.map_background_naming (Name_Space.qualified_path false (Binding.name short_name))
  14.176 +      |> @{fold_map 2} define (map mk_name sels) (Syntax.check_terms lthy (map mk_t (0 upto len - 1)))
  14.177 +      ||> `Local_Theory.close_target
  14.178 +
  14.179 +    val phi = Proof_Context.export_morphism lthy' lthy''
  14.180 +
  14.181 +    val (update_ts, update_defs) =
  14.182 +      split_list updates
  14.183 +      |>> map (Morphism.term phi)
  14.184 +      ||> map (Morphism.thm phi)
  14.185 +
  14.186 +    val thms = flat (map (prove lthy'' update_defs update_ts) (0 upto len-1))
  14.187  
  14.188      fun insert sel =
  14.189        Symtab.insert op = (fst (dest_Const sel), Local_Theory.full_name lthy' (mk_name sel))
  14.190    in
  14.191 -    lthy'
  14.192 -    |> @{fold 2} define (map mk_name sels) (Syntax.check_terms lthy (map mk_t (0 upto len - 1)))
  14.193 +    lthy''
  14.194 +    |> Local_Theory.map_background_naming (Name_Space.mandatory_path short_name)
  14.195 +    |> Local_Theory.note (thms_binding, thms)
  14.196 +    |> snd
  14.197 +    |> Local_Theory.restore_background_naming lthy
  14.198      |> Local_Theory.background_theory (Data.map (fold insert sels))
  14.199 -    |> Local_Theory.restore_background_naming lthy
  14.200    end
  14.201  
  14.202 -fun bnf_record binding opts tyargs args lthy =
  14.203 +fun record binding opts tyargs args lthy =
  14.204    let
  14.205      val constructor =
  14.206        (((Binding.empty, Binding.map_name (fn c => "make_" ^ c) binding), args), NoSyn)
  14.207 @@ -93,8 +224,8 @@
  14.208      lthy'
  14.209    end
  14.210  
  14.211 -fun bnf_record_cmd binding opts tyargs args lthy =
  14.212 -  bnf_record binding (opts lthy)
  14.213 +fun record_cmd binding opts tyargs args lthy =
  14.214 +  record binding (opts lthy)
  14.215      (map (apsnd (apfst (Syntax.parse_typ lthy) o apsnd (Typedecl.read_constraint lthy))) tyargs)
  14.216      (map (apsnd (Syntax.parse_typ lthy)) args) lthy
  14.217  
  14.218 @@ -172,7 +303,7 @@
  14.219      @{command_keyword datatype_record}
  14.220      "Defines a record based on the BNF/datatype machinery"
  14.221      (parser >> (fn (((ctr_options, tyargs), binding), args) =>
  14.222 -      bnf_record_cmd binding ctr_options tyargs args))
  14.223 +      record_cmd binding ctr_options tyargs args))
  14.224  
  14.225  val setup =
  14.226     (Sign.parse_translation
    15.1 --- a/src/HOL/ex/Datatype_Record_Examples.thy	Sun Jul 29 13:18:10 2018 +0200
    15.2 +++ b/src/HOL/ex/Datatype_Record_Examples.thy	Sun Jul 29 18:24:47 2018 +0200
    15.3 @@ -45,4 +45,23 @@
    15.4  lemma "b_set \<lparr> field_1 = True, field_2 = False \<rparr> = {False}"
    15.5    by simp
    15.6  
    15.7 +text \<open>More tests\<close>
    15.8 +
    15.9 +datatype_record ('a, 'b) test1 =
   15.10 +  field_t11 :: 'a
   15.11 +  field_t12 :: 'b
   15.12 +  field_t13 :: nat
   15.13 +  field_t14 :: int
   15.14 +
   15.15 +thm test1.record_simps
   15.16 +
   15.17 +definition ID where "ID x = x"
   15.18 +lemma ID_cong[cong]: "ID x = ID x" by (rule refl)
   15.19 +
   15.20 +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))"
   15.21 +  apply (simp only: test1.record_simps)
   15.22 +  apply (subst ID_def)
   15.23 +  apply (rule refl)
   15.24 +  done
   15.25 +
   15.26  end
   15.27 \ No newline at end of file