de-applying
authorpaulson <lp15@cam.ac.uk>
Wed Jul 25 00:25:05 2018 +0200 (14 months ago)
changeset 686849a42b84f8838
parent 68683 d69127c6e80f
child 68685 4b367da119ed
de-applying
src/HOL/Algebra/AbelCoset.thy
src/HOL/Algebra/Complete_Lattice.thy
src/HOL/Algebra/Divisibility.thy
     1.1 --- a/src/HOL/Algebra/AbelCoset.thy	Sun Jul 22 21:04:49 2018 +0200
     1.2 +++ b/src/HOL/Algebra/AbelCoset.thy	Wed Jul 25 00:25:05 2018 +0200
     1.3 @@ -269,17 +269,15 @@
     1.4      by (rule a_comm_group)
     1.5    interpret subgroup "H" "(add_monoid G)"
     1.6      by (rule a_subgroup)
     1.7 -
     1.8 -  show "abelian_subgroup H G"
     1.9 -    apply unfold_locales
    1.10 -  proof (simp add: r_coset_def l_coset_def, clarsimp)
    1.11 -    fix x
    1.12 -    assume xcarr: "x \<in> carrier G"
    1.13 -    from a_subgroup have Hcarr: "H \<subseteq> carrier G"
    1.14 -      unfolding subgroup_def by simp
    1.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})"
    1.16 +  have "(\<Union>xa\<in>H. {xa \<oplus> x}) = (\<Union>xa\<in>H. {x \<oplus> xa})" if "x \<in> carrier G" for x
    1.17 +  proof -
    1.18 +    have "H \<subseteq> carrier G"
    1.19 +      using a_subgroup that unfolding subgroup_def by simp
    1.20 +    with that show "(\<Union>h\<in>H. {h \<oplus>\<^bsub>G\<^esub> x}) = (\<Union>h\<in>H. {x \<oplus>\<^bsub>G\<^esub> h})"
    1.21        using m_comm [simplified] by fastforce
    1.22    qed
    1.23 +  then show "abelian_subgroup H G"
    1.24 +    by unfold_locales (auto simp: r_coset_def l_coset_def)
    1.25  qed
    1.26  
    1.27  lemma abelian_subgroupI3:
    1.28 @@ -304,14 +302,6 @@
    1.29  by (rule normal.inv_op_closed2 [OF a_normal,
    1.30      folded a_inv_def, simplified monoid_record_simps])
    1.31  
    1.32 -text\<open>Alternative characterization of normal subgroups\<close>
    1.33 -lemma (in abelian_group) a_normal_inv_iff:
    1.34 -     "(N \<lhd> (add_monoid G)) = 
    1.35 -      (subgroup N (add_monoid G) & (\<forall>x \<in> carrier G. \<forall>h \<in> N. x \<oplus> h \<oplus> (\<ominus> x) \<in> N))"
    1.36 -      (is "_ = ?rhs")
    1.37 -by (rule group.normal_inv_iff [OF a_group,
    1.38 -    folded a_inv_def, simplified monoid_record_simps])
    1.39 -
    1.40  lemma (in abelian_group) a_lcos_m_assoc:
    1.41    "\<lbrakk> M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G \<rbrakk> \<Longrightarrow> g <+ (h <+ M) = (g \<oplus> h) <+ M"
    1.42  by (rule group.lcos_m_assoc [OF a_group,
    1.43 @@ -322,13 +312,11 @@
    1.44  by (rule group.lcos_mult_one [OF a_group,
    1.45      folded a_l_coset_def, simplified monoid_record_simps])
    1.46  
    1.47 -
    1.48  lemma (in abelian_group) a_l_coset_subset_G:
    1.49    "\<lbrakk> H \<subseteq> carrier G; x \<in> carrier G \<rbrakk> \<Longrightarrow> x <+ H \<subseteq> carrier G"
    1.50  by (rule group.l_coset_subset_G [OF a_group,
    1.51      folded a_l_coset_def, simplified monoid_record_simps])
    1.52  
    1.53 -
    1.54  lemma (in abelian_group) a_l_coset_swap:
    1.55       "\<lbrakk>y \<in> x <+ H;  x \<in> carrier G;  subgroup H (add_monoid G)\<rbrakk> \<Longrightarrow> x \<in> y <+ H"
    1.56  by (rule group.l_coset_swap [OF a_group,
    1.57 @@ -498,15 +486,15 @@
    1.58  
    1.59  text \<open>Since the Factorization is based on an \emph{abelian} subgroup, is results in 
    1.60          a commutative group\<close>
    1.61 -theorem (in abelian_subgroup) a_factorgroup_is_comm_group:
    1.62 -  "comm_group (G A_Mod H)"
    1.63 -apply (intro comm_group.intro comm_monoid.intro) prefer 3
    1.64 -  apply (rule a_factorgroup_is_group)
    1.65 - apply (rule group.axioms[OF a_factorgroup_is_group])
    1.66 -apply (rule comm_monoid_axioms.intro)
    1.67 -apply (unfold A_FactGroup_def FactGroup_def RCOSETS_def, fold set_add_def a_r_coset_def, clarsimp)
    1.68 -apply (simp add: a_rcos_sum a_comm)
    1.69 -done
    1.70 +theorem (in abelian_subgroup) a_factorgroup_is_comm_group: "comm_group (G A_Mod H)"
    1.71 +proof -
    1.72 +  have "Group.comm_monoid_axioms (G A_Mod H)"
    1.73 +    apply (rule comm_monoid_axioms.intro)
    1.74 +    apply (auto simp: A_FactGroup_def FactGroup_def RCOSETS_def a_normal add.m_comm normal.rcos_sum)
    1.75 +    done
    1.76 +  then show ?thesis
    1.77 +    by (intro comm_group.intro comm_monoid.intro) (simp_all add: a_factorgroup_is_group group.is_monoid)
    1.78 +qed
    1.79  
    1.80  lemma add_A_FactGroup [simp]: "X \<otimes>\<^bsub>(G A_Mod H)\<^esub> X' = X <+>\<^bsub>G\<^esub> X'"
    1.81  by (simp add: A_FactGroup_def set_add_def)
    1.82 @@ -552,11 +540,8 @@
    1.83    interpret G: abelian_group G by fact
    1.84    interpret H: abelian_group H by fact
    1.85    show ?thesis
    1.86 -    apply (intro abelian_group_hom.intro abelian_group_hom_axioms.intro)
    1.87 -      apply fact
    1.88 -     apply fact
    1.89 -    apply (rule a_group_hom)
    1.90 -    done
    1.91 +    by (intro abelian_group_hom.intro abelian_group_hom_axioms.intro 
    1.92 +        G.abelian_group_axioms H.abelian_group_axioms a_group_hom)
    1.93  qed
    1.94  
    1.95  lemma (in abelian_group_hom) is_abelian_group_hom:
    1.96 @@ -576,8 +561,7 @@
    1.97  
    1.98  lemma (in abelian_group_hom) zero_closed [simp]:
    1.99    "h \<zero> \<in> carrier H"
   1.100 -by (rule group_hom.one_closed[OF a_group_hom,
   1.101 -    simplified ring_record_simps])
   1.102 +  by simp
   1.103  
   1.104  lemma (in abelian_group_hom) hom_zero [simp]:
   1.105    "h \<zero> = \<zero>\<^bsub>H\<^esub>"
   1.106 @@ -586,8 +570,7 @@
   1.107  
   1.108  lemma (in abelian_group_hom) a_inv_closed [simp]:
   1.109    "x \<in> carrier G ==> h (\<ominus>x) \<in> carrier H"
   1.110 -by (rule group_hom.inv_closed[OF a_group_hom,
   1.111 -    folded a_inv_def, simplified ring_record_simps])
   1.112 +  by simp
   1.113  
   1.114  lemma (in abelian_group_hom) hom_a_inv [simp]:
   1.115    "x \<in> carrier G ==> h (\<ominus>x) = \<ominus>\<^bsub>H\<^esub> (h x)"
   1.116 @@ -596,19 +579,15 @@
   1.117  
   1.118  lemma (in abelian_group_hom) additive_subgroup_a_kernel:
   1.119    "additive_subgroup (a_kernel G H h) G"
   1.120 -apply (rule additive_subgroup.intro)
   1.121 -apply (rule group_hom.subgroup_kernel[OF a_group_hom,
   1.122 -       folded a_kernel_def, simplified ring_record_simps])
   1.123 -done
   1.124 +  by (simp add: additive_subgroup.intro a_group_hom a_kernel_def group_hom.subgroup_kernel)
   1.125  
   1.126  text\<open>The kernel of a homomorphism is an abelian subgroup\<close>
   1.127  lemma (in abelian_group_hom) abelian_subgroup_a_kernel:
   1.128    "abelian_subgroup (a_kernel G H h) G"
   1.129 -apply (rule abelian_subgroupI)
   1.130 -apply (rule group_hom.normal_kernel[OF a_group_hom,
   1.131 -       folded a_kernel_def, simplified ring_record_simps])
   1.132 -apply (simp add: G.a_comm)
   1.133 -done
   1.134 +  apply (rule abelian_subgroupI)
   1.135 +   apply (simp add: G.abelian_group_axioms abelian_subgroup.a_normal abelian_subgroupI3 additive_subgroup_a_kernel)
   1.136 +  apply (simp add: G.a_comm)
   1.137 +  done
   1.138  
   1.139  lemma (in abelian_group_hom) A_FactGroup_nonempty:
   1.140    assumes X: "X \<in> carrier (G A_Mod a_kernel G H h)"
   1.141 @@ -715,48 +694,34 @@
   1.142  qed
   1.143  
   1.144  lemma (in abelian_subgroup) a_repr_independence':
   1.145 -  assumes y: "y \<in> H +> x"
   1.146 -      and xcarr: "x \<in> carrier G"
   1.147 +  assumes "y \<in> H +> x" "x \<in> carrier G"
   1.148    shows "H +> x = H +> y"
   1.149 -  apply (rule a_repr_independence)
   1.150 -    apply (rule y)
   1.151 -   apply (rule xcarr)
   1.152 -  apply (rule a_subgroup)
   1.153 -  done
   1.154 +  using a_repr_independence a_subgroup assms by blast
   1.155  
   1.156  lemma (in abelian_subgroup) a_repr_independenceD:
   1.157 -  assumes ycarr: "y \<in> carrier G"
   1.158 -      and repr:  "H +> x = H +> y"
   1.159 +  assumes "y \<in> carrier G" "H +> x = H +> y"
   1.160    shows "y \<in> H +> x"
   1.161 -by (rule group.repr_independenceD [OF a_group a_subgroup,
   1.162 -    folded a_r_coset_def, simplified monoid_record_simps]) (rule ycarr, rule repr)
   1.163 +  by (simp add: a_rcos_self assms)
   1.164  
   1.165  
   1.166  lemma (in abelian_subgroup) a_rcosets_carrier:
   1.167    "X \<in> a_rcosets H \<Longrightarrow> X \<subseteq> carrier G"
   1.168 -by (rule subgroup.rcosets_carrier [OF a_subgroup a_group,
   1.169 -    folded A_RCOSETS_def, simplified monoid_record_simps])
   1.170 +  using a_rcosets_part_G by auto
   1.171  
   1.172  
   1.173  subsubsection \<open>Addition of Subgroups\<close>
   1.174  
   1.175  lemma (in abelian_monoid) set_add_closed:
   1.176 -  assumes Acarr: "A \<subseteq> carrier G"
   1.177 -      and Bcarr: "B \<subseteq> carrier G"
   1.178 +  assumes "A \<subseteq> carrier G" "B \<subseteq> carrier G"
   1.179    shows "A <+> B \<subseteq> carrier G"
   1.180 -by (rule monoid.set_mult_closed [OF a_monoid,
   1.181 -    folded set_add_def, simplified monoid_record_simps]) (rule Acarr, rule Bcarr)
   1.182 +  by (simp add: assms add.set_mult_closed set_add_defs(1))
   1.183  
   1.184  lemma (in abelian_group) add_additive_subgroups:
   1.185    assumes subH: "additive_subgroup H G"
   1.186 -      and subK: "additive_subgroup K G"
   1.187 +    and subK: "additive_subgroup K G"
   1.188    shows "additive_subgroup (H <+> K) G"
   1.189 -apply (rule additive_subgroup.intro)
   1.190 -apply (unfold set_add_def)
   1.191 -apply (intro comm_group.mult_subgroups)
   1.192 -  apply (rule a_comm_group)
   1.193 - apply (rule additive_subgroup.a_subgroup[OF subH])
   1.194 -apply (rule additive_subgroup.a_subgroup[OF subK])
   1.195 -done
   1.196 +  unfolding set_add_def
   1.197 +  using add.mult_subgroups additive_subgroup_def subH subK
   1.198 +  by (blast intro: additive_subgroup.intro)
   1.199  
   1.200  end
     2.1 --- a/src/HOL/Algebra/Complete_Lattice.thy	Sun Jul 22 21:04:49 2018 +0200
     2.2 +++ b/src/HOL/Algebra/Complete_Lattice.thy	Wed Jul 25 00:25:05 2018 +0200
     2.3 @@ -680,22 +680,25 @@
     2.4      next
     2.5        case False
     2.6        show ?thesis
     2.7 -      proof (rule_tac x="\<Squnion>\<^bsub>L\<^esub> A" in exI, rule least_UpperI, simp_all)
     2.8 +      proof (intro exI least_UpperI, simp_all)
     2.9          show b:"\<And> x. x \<in> A \<Longrightarrow> x \<sqsubseteq>\<^bsub>L\<^esub> \<Squnion>\<^bsub>L\<^esub>A"
    2.10            using a by (auto intro: L.sup_upper, meson L.at_least_at_most_closed L.sup_upper subset_trans)
    2.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"
    2.12            using a L.at_least_at_most_closed by (rule_tac L.sup_least, auto intro: funcset_mem simp add: Upper_def)
    2.13 -        from a show "A \<subseteq> \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>"
    2.14 -          by (auto)
    2.15 -        from a show "\<Squnion>\<^bsub>L\<^esub>A \<in> \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>"
    2.16 -          apply (rule_tac L.at_least_at_most_member)
    2.17 -          apply (auto)
    2.18 -          apply (meson L.at_least_at_most_closed L.sup_closed subset_trans)
    2.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)
    2.20 -          apply (rule L.sup_least)
    2.21 -          apply (auto simp add: assms)
    2.22 -          using L.at_least_at_most_closed apply blast
    2.23 -        done
    2.24 +        from a show *: "A \<subseteq> \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>"
    2.25 +          by auto
    2.26 +        show "\<Squnion>\<^bsub>L\<^esub>A \<in> \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>"
    2.27 +        proof (rule_tac L.at_least_at_most_member)
    2.28 +          show 1: "\<Squnion>\<^bsub>L\<^esub>A \<in> carrier L"
    2.29 +            by (meson L.at_least_at_most_closed L.sup_closed subset_trans *)
    2.30 +          show "a \<sqsubseteq>\<^bsub>L\<^esub> \<Squnion>\<^bsub>L\<^esub>A"
    2.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)
    2.32 +          show "\<Squnion>\<^bsub>L\<^esub>A \<sqsubseteq>\<^bsub>L\<^esub> b"
    2.33 +          proof (rule L.sup_least)
    2.34 +            show "A \<subseteq> carrier L" "\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq>\<^bsub>L\<^esub> b"
    2.35 +              using * L.at_least_at_most_closed by blast+
    2.36 +          qed (simp add: assms)
    2.37 +        qed
    2.38        qed
    2.39      qed
    2.40      show "\<exists>s. is_glb (L\<lparr>carrier := \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>\<rparr>) s A"
    2.41 @@ -711,15 +714,17 @@
    2.42            using a L.at_least_at_most_closed by (force intro!: L.inf_lower)
    2.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"
    2.44             using a L.at_least_at_most_closed by (rule_tac L.inf_greatest, auto intro: funcset_carrier' simp add: Lower_def)
    2.45 -        from a show "A \<subseteq> \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>"
    2.46 -          by (auto)
    2.47 -        from a show "\<Sqinter>\<^bsub>L\<^esub>A \<in> \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>"
    2.48 -          apply (rule_tac L.at_least_at_most_member)
    2.49 -          apply (auto)
    2.50 -          apply (meson L.at_least_at_most_closed L.inf_closed subset_trans)
    2.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)
    2.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)            
    2.53 -        done
    2.54 +        from a show *: "A \<subseteq> \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>"
    2.55 +          by auto
    2.56 +        show "\<Sqinter>\<^bsub>L\<^esub>A \<in> \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>"
    2.57 +        proof (rule_tac L.at_least_at_most_member)
    2.58 +          show 1: "\<Sqinter>\<^bsub>L\<^esub>A \<in> carrier L"
    2.59 +            by (meson "*" L.at_least_at_most_closed L.inf_closed subset_trans)
    2.60 +          show "a \<sqsubseteq>\<^bsub>L\<^esub> \<Sqinter>\<^bsub>L\<^esub>A"
    2.61 +            by (meson "*" L.at_least_at_most_closed L.at_least_at_most_lower L.inf_greatest assms(2) subsetD subset_trans)
    2.62 +          show "\<Sqinter>\<^bsub>L\<^esub>A \<sqsubseteq>\<^bsub>L\<^esub> b"
    2.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)
    2.64 +        qed
    2.65        qed
    2.66      qed
    2.67    qed
    2.68 @@ -731,7 +736,7 @@
    2.69  text \<open>The set of fixed points of a complete lattice is itself a complete lattice\<close>
    2.70  
    2.71  theorem Knaster_Tarski:
    2.72 -  assumes "weak_complete_lattice L" "f \<in> carrier L \<rightarrow> carrier L" "isotone L L f"
    2.73 +  assumes "weak_complete_lattice L" and f: "f \<in> carrier L \<rightarrow> carrier L" and "isotone L L f"
    2.74    shows "weak_complete_lattice (fpl L f)" (is "weak_complete_lattice ?L'")
    2.75  proof -
    2.76    interpret L: weak_complete_lattice L
    2.77 @@ -805,15 +810,14 @@
    2.78        show "is_lub ?L'' (LFP\<^bsub>?L'\<^esub> f) A"
    2.79        proof (rule least_UpperI, simp_all)
    2.80          fix x
    2.81 -        assume "x \<in> Upper ?L'' A"
    2.82 -        hence "LFP\<^bsub>?L'\<^esub> f \<sqsubseteq>\<^bsub>?L'\<^esub> x"
    2.83 -          apply (rule_tac L'.LFP_lowerbound)
    2.84 -          apply (auto simp add: Upper_def)
    2.85 -          apply (simp add: A AL L.at_least_at_most_member L.sup_least set_rev_mp)          
    2.86 -          apply (simp add: Pi_iff assms(2) fps_def, rule_tac L.weak_refl)
    2.87 -          apply (auto)
    2.88 -          apply (rule funcset_mem[of f "carrier L"], simp_all add: assms(2))
    2.89 -        done
    2.90 +        assume x: "x \<in> Upper ?L'' A"
    2.91 +        have "LFP\<^bsub>?L'\<^esub> f \<sqsubseteq>\<^bsub>?L'\<^esub> x"
    2.92 +        proof (rule L'.LFP_lowerbound, simp_all)
    2.93 +          show "x \<in> \<lbrace>\<Squnion>\<^bsub>L\<^esub>A..\<top>\<^bsub>L\<^esub>\<rbrace>\<^bsub>L\<^esub>"
    2.94 +            using x by (auto simp add: Upper_def A AL L.at_least_at_most_member L.sup_least set_rev_mp)    
    2.95 +          with x show "f x \<sqsubseteq>\<^bsub>L\<^esub> x"
    2.96 +            by (simp add: Upper_def) (meson L.at_least_at_most_closed L.use_fps L.weak_refl subsetD f_top_chain imageI)
    2.97 +        qed
    2.98          thus " LFP\<^bsub>?L'\<^esub> f \<sqsubseteq>\<^bsub>L\<^esub> x"
    2.99            by (simp)
   2.100        next
   2.101 @@ -838,17 +842,13 @@
   2.102               by (auto simp add: at_least_at_most_def)
   2.103            have "LFP\<^bsub>?L'\<^esub> f .=\<^bsub>?L'\<^esub> f (LFP\<^bsub>?L'\<^esub> f)"
   2.104            proof (rule "L'.LFP_weak_unfold", simp_all)
   2.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>"
   2.106 -              apply (auto simp add: Pi_def at_least_at_most_def)
   2.107 -              using assms(2) apply blast
   2.108 -              apply (meson AL funcset_mem L.le_trans L.sup_closed assms(2) assms(3) pf_w use_iso2)
   2.109 -              using assms(2) apply blast
   2.110 -            done
   2.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"
   2.112 -              apply (auto simp add: isotone_def)
   2.113 -              using L'.weak_partial_order_axioms apply blast
   2.114 -              apply (meson L.at_least_at_most_closed subsetCE)
   2.115 -            done
   2.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"
   2.117 +              by (meson AL funcset_mem L.le_trans L.sup_closed assms(2) assms(3) pf_w use_iso2)
   2.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>"
   2.119 +              by (auto simp add: Pi_def at_least_at_most_def)
   2.120 +            show "Mono\<^bsub>L\<lparr>carrier := \<lbrace>\<Squnion>\<^bsub>L\<^esub>A..\<top>\<^bsub>L\<^esub>\<rbrace>\<^bsub>L\<^esub>\<rparr>\<^esub> f"
   2.121 +              using L'.weak_partial_order_axioms assms(3) 
   2.122 +              by (auto simp add: isotone_def) (meson L.at_least_at_most_closed subsetCE)
   2.123            qed
   2.124            thus "f (LFP\<^bsub>?L'\<^esub> f) .=\<^bsub>L\<^esub> LFP\<^bsub>?L'\<^esub> f"
   2.125              by (simp add: L.equivalence_axioms funcset_carrier' c assms(2) equivalence.sym) 
   2.126 @@ -889,7 +889,6 @@
   2.127            thus ?thesis
   2.128              by (meson AL L.inf_closed L.le_trans assms(3) b(1) b(2) fx use_iso2 w)
   2.129          qed
   2.130 -   
   2.131          show "\<bottom>\<^bsub>L\<^esub> \<sqsubseteq>\<^bsub>L\<^esub> f x"
   2.132            by (simp add: fx)
   2.133        qed
   2.134 @@ -905,12 +904,16 @@
   2.135        proof (rule greatest_LowerI, simp_all)
   2.136          fix x
   2.137          assume "x \<in> Lower ?L'' A"
   2.138 -        hence "x \<sqsubseteq>\<^bsub>?L'\<^esub> GFP\<^bsub>?L'\<^esub> f"
   2.139 -          apply (rule_tac L'.GFP_upperbound)
   2.140 -          apply (auto simp add: Lower_def)
   2.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)
   2.142 -          apply (simp add: funcset_carrier' L.sym assms(2) fps_def)          
   2.143 -        done
   2.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"
   2.145 +          by (auto simp add: Lower_def)
   2.146 +        have "x \<sqsubseteq>\<^bsub>?L'\<^esub> GFP\<^bsub>?L'\<^esub> f"
   2.147 +          unfolding Lower_def
   2.148 +        proof (rule_tac L'.GFP_upperbound; simp)
   2.149 +          show "x \<in> \<lbrace>\<bottom>\<^bsub>L\<^esub>..\<Sqinter>\<^bsub>L\<^esub>A\<rbrace>\<^bsub>L\<^esub>"
   2.150 +            by (meson x A AL L.at_least_at_most_member L.bottom_lower L.inf_greatest contra_subsetD fps_carrier)
   2.151 +          show "x \<sqsubseteq>\<^bsub>L\<^esub> f x"
   2.152 +            using x by (simp add: funcset_carrier' L.sym assms(2) fps_def)
   2.153 +        qed
   2.154          thus "x \<sqsubseteq>\<^bsub>L\<^esub> GFP\<^bsub>?L'\<^esub> f"
   2.155            by (simp)
   2.156        next
   2.157 @@ -935,17 +938,14 @@
   2.158               by (auto simp add: at_least_at_most_def)
   2.159            have "GFP\<^bsub>?L'\<^esub> f .=\<^bsub>?L'\<^esub> f (GFP\<^bsub>?L'\<^esub> f)"
   2.160            proof (rule "L'.GFP_weak_unfold", simp_all)
   2.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>"
   2.162 -              apply (auto simp add: Pi_def at_least_at_most_def)
   2.163 -              using assms(2) apply blast
   2.164 -              apply (simp add: funcset_carrier' assms(2))
   2.165 -              apply (meson AL funcset_carrier L.inf_closed L.le_trans assms(2) assms(3) pf_w use_iso2)
   2.166 -            done
   2.167 -            from assms(3) show "Mono\<^bsub>L\<lparr>carrier := \<lbrace>\<bottom>\<^bsub>L\<^esub>..?w\<rbrace>\<^bsub>L\<^esub>\<rparr>\<^esub> f"
   2.168 -              apply (auto simp add: isotone_def)
   2.169 -              using L'.weak_partial_order_axioms apply blast
   2.170 -              using L.at_least_at_most_closed apply (blast intro: funcset_carrier')
   2.171 -            done
   2.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"
   2.173 +              by (meson AL funcset_carrier L.inf_closed L.le_trans assms(2) assms(3) pf_w use_iso2)
   2.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>"
   2.175 +              by (auto simp add: Pi_def at_least_at_most_def)
   2.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"
   2.177 +              by (meson L.at_least_at_most_closed subsetD use_iso1  assms(3)) 
   2.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"
   2.179 +              by (auto simp add: isotone_def)
   2.180            qed
   2.181            thus "f (GFP\<^bsub>?L'\<^esub> f) .=\<^bsub>L\<^esub> GFP\<^bsub>?L'\<^esub> f"
   2.182              by (simp add: L.equivalence_axioms funcset_carrier' c assms(2) equivalence.sym) 
   2.183 @@ -1117,17 +1117,16 @@
   2.184      qed
   2.185      show "\<Sqinter>\<^bsub>fpl L f\<^esub>A \<sqsubseteq>\<^bsub>L\<^esub> f (\<Sqinter>\<^bsub>L\<^esub>A)"
   2.186      proof -
   2.187 +      have *: "\<Sqinter>\<^bsub>fpl L f\<^esub>A \<in> carrier L"
   2.188 +        using FA infA by blast
   2.189        have "\<And>x. x \<in> A \<Longrightarrow> \<Sqinter>\<^bsub>fpl L f\<^esub>A \<sqsubseteq>\<^bsub>fpl L f\<^esub> x"
   2.190          by (rule L'.inf_lower, simp_all add: assms)
   2.191        hence "\<Sqinter>\<^bsub>fpl L f\<^esub>A \<sqsubseteq>\<^bsub>L\<^esub> (\<Sqinter>\<^bsub>L\<^esub>A)"
   2.192 -        apply (rule_tac L.inf_greatest, simp_all add: A)
   2.193 -        using FA infA apply blast
   2.194 -        done
   2.195 +        by (rule_tac L.inf_greatest, simp_all add: A *)
   2.196        hence 1:"f(\<Sqinter>\<^bsub>fpl L f\<^esub>A) \<sqsubseteq>\<^bsub>L\<^esub> f(\<Sqinter>\<^bsub>L\<^esub>A)"
   2.197          by (metis (no_types, lifting) A FA L.inf_closed assms(2) infA subsetCE use_iso1)
   2.198        have 2:"\<Sqinter>\<^bsub>fpl L f\<^esub>A \<sqsubseteq>\<^bsub>L\<^esub> f (\<Sqinter>\<^bsub>fpl L f\<^esub>A)"
   2.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)
   2.200 -        
   2.201        show ?thesis  
   2.202          using FA fA infA by (auto intro!: L.le_trans[OF 2 1] ic fc, metis FA PiE assms(4) subsetCE)
   2.203      qed
   2.204 @@ -1189,21 +1188,11 @@
   2.205  lemma sup_pres_is_join_pres:
   2.206    assumes "weak_sup_pres X Y f"
   2.207    shows "join_pres X Y f"
   2.208 -  using assms
   2.209 -  apply (simp add: join_pres_def weak_sup_pres_def, safe)
   2.210 -  apply (rename_tac x y)
   2.211 -  apply (drule_tac x="{x, y}" in spec)
   2.212 -  apply (auto simp add: join_def)
   2.213 -done
   2.214 +  using assms by (auto simp: join_pres_def weak_sup_pres_def join_def)
   2.215  
   2.216  lemma inf_pres_is_meet_pres:
   2.217    assumes "weak_inf_pres X Y f"
   2.218    shows "meet_pres X Y f"
   2.219 -  using assms
   2.220 -  apply (simp add: meet_pres_def weak_inf_pres_def, safe)
   2.221 -  apply (rename_tac x y)
   2.222 -  apply (drule_tac x="{x, y}" in spec)
   2.223 -  apply (auto simp add: meet_def)
   2.224 -done
   2.225 +  using assms by (auto simp: meet_pres_def weak_inf_pres_def meet_def)
   2.226  
   2.227  end
     3.1 --- a/src/HOL/Algebra/Divisibility.thy	Sun Jul 22 21:04:49 2018 +0200
     3.2 +++ b/src/HOL/Algebra/Divisibility.thy	Wed Jul 25 00:25:05 2018 +0200
     3.3 @@ -547,22 +547,14 @@
     3.4    using pf by (elim properfactorE)
     3.5  
     3.6  lemma (in monoid) properfactor_trans1 [trans]:
     3.7 -  assumes dvds: "a divides b"  "properfactor G b c"
     3.8 -    and carr: "a \<in> carrier G"  "c \<in> carrier G"
     3.9 +  assumes "a divides b"  "properfactor G b c" "a \<in> carrier G"  "c \<in> carrier G"
    3.10    shows "properfactor G a c"
    3.11 -  using dvds carr
    3.12 -  apply (elim properfactorE, intro properfactorI)
    3.13 -   apply (iprover intro: divides_trans)+
    3.14 -  done
    3.15 +  by (meson divides_trans properfactorE properfactorI assms)
    3.16  
    3.17  lemma (in monoid) properfactor_trans2 [trans]:
    3.18 -  assumes dvds: "properfactor G a b"  "b divides c"
    3.19 -    and carr: "a \<in> carrier G"  "b \<in> carrier G"
    3.20 +  assumes "properfactor G a b"  "b divides c" "a \<in> carrier G"  "b \<in> carrier G"
    3.21    shows "properfactor G a c"
    3.22 -  using dvds carr
    3.23 -  apply (elim properfactorE, intro properfactorI)
    3.24 -   apply (iprover intro: divides_trans)+
    3.25 -  done
    3.26 +  by (meson divides_trans properfactorE properfactorI assms)
    3.27  
    3.28  lemma properfactor_lless:
    3.29    fixes G (structure)
    3.30 @@ -660,23 +652,20 @@
    3.31    using assms by (fast elim: irreducibleE)
    3.32  
    3.33  lemma (in monoid_cancel) irreducible_cong [trans]:
    3.34 -  assumes irred: "irreducible G a"
    3.35 -    and aa': "a \<sim> a'" "a \<in> carrier G"  "a' \<in> carrier G"
    3.36 +  assumes "irreducible G a" "a \<sim> a'" "a \<in> carrier G"  "a' \<in> carrier G"
    3.37    shows "irreducible G a'"
    3.38 -  using assms
    3.39 -  apply (auto simp: irreducible_def assoc_unit_l)
    3.40 -  apply (metis aa' associated_sym properfactor_cong_r)
    3.41 -  done
    3.42 +proof -
    3.43 +  have "a' divides a"
    3.44 +    by (meson \<open>a \<sim> a'\<close> associated_def)
    3.45 +  then show ?thesis
    3.46 +    by (metis (no_types) assms assoc_unit_l irreducibleE irreducibleI monoid.properfactor_trans2 monoid_axioms)
    3.47 +qed
    3.48  
    3.49  lemma (in monoid) irreducible_prod_rI:
    3.50 -  assumes airr: "irreducible G a"
    3.51 -    and bunit: "b \<in> Units G"
    3.52 -    and carr[simp]: "a \<in> carrier G"  "b \<in> carrier G"
    3.53 +  assumes "irreducible G a" "b \<in> Units G" "a \<in> carrier G"  "b \<in> carrier G"
    3.54    shows "irreducible G (a \<otimes> b)"
    3.55 -  using airr carr bunit
    3.56 -  apply (elim irreducibleE, intro irreducibleI)
    3.57 -  using prod_unit_r apply blast
    3.58 -  using associatedI2' properfactor_cong_r by auto
    3.59 +  using assms
    3.60 +  by (metis (no_types, lifting) associatedI2' irreducible_def monoid.m_closed monoid_axioms prod_unit_r properfactor_cong_r)
    3.61  
    3.62  lemma (in comm_monoid) irreducible_prod_lI:
    3.63    assumes birr: "irreducible G b"
    3.64 @@ -764,9 +753,7 @@
    3.65      and pp': "p \<sim> p'" "p \<in> carrier G"  "p' \<in> carrier G"
    3.66    shows "prime G p'"
    3.67    using assms
    3.68 -  apply (auto simp: prime_def assoc_unit_l)
    3.69 -  apply (metis pp' associated_sym divides_cong_l)
    3.70 -  done
    3.71 +  by (auto simp: prime_def assoc_unit_l) (metis pp' associated_sym divides_cong_l)
    3.72  
    3.73  (*by Paulo Emílio de Vilhena*)
    3.74  lemma (in comm_monoid_cancel) prime_irreducible:
    3.75 @@ -849,9 +836,7 @@
    3.76      and "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G"
    3.77    shows "\<forall>a\<in>set bs. irreducible G a"
    3.78    using assms
    3.79 -  apply (clarsimp simp add: list_all2_conv_all_nth set_conv_nth)
    3.80 -  apply (blast intro: irreducible_cong)
    3.81 -  done
    3.82 +  by (fastforce simp add: list_all2_conv_all_nth set_conv_nth intro: irreducible_cong)
    3.83  
    3.84  
    3.85  text \<open>Permutations\<close>
    3.86 @@ -1001,15 +986,7 @@
    3.87    then have f: "f \<in> carrier G"
    3.88      by blast
    3.89    show ?case
    3.90 -  proof (cases "f = a")
    3.91 -    case True
    3.92 -    then show ?thesis
    3.93 -      using Cons.prems by auto
    3.94 -  next
    3.95 -    case False
    3.96 -    with Cons show ?thesis
    3.97 -      by clarsimp (metis f divides_prod_l multlist_closed)
    3.98 -  qed
    3.99 +    using Cons.IH Cons.prems(1) Cons.prems(2) divides_prod_l f by auto
   3.100  qed auto
   3.101  
   3.102  lemma (in comm_monoid_cancel) multlist_listassoc_cong:
   3.103 @@ -1051,9 +1028,7 @@
   3.104      and "set fs \<subseteq> carrier G" and "set fs' \<subseteq> carrier G"
   3.105    shows "foldr (\<otimes>) fs \<one> \<sim> foldr (\<otimes>) fs' \<one>"
   3.106    using assms
   3.107 -  apply (elim essentially_equalE)
   3.108 -  apply (simp add: multlist_perm_cong multlist_listassoc_cong perm_closed)
   3.109 -  done
   3.110 +  by (metis essentially_equal_def multlist_listassoc_cong multlist_perm_cong perm_closed)
   3.111  
   3.112  
   3.113  subsubsection \<open>Factorization in irreducible elements\<close>
   3.114 @@ -1120,9 +1095,6 @@
   3.115      and carr[simp]: "set fs \<subseteq> carrier G"
   3.116    shows "fs = []"
   3.117  proof (cases fs)
   3.118 -  case Nil
   3.119 -  then show ?thesis .
   3.120 -next
   3.121    case fs: (Cons f fs')
   3.122    from carr have fcarr[simp]: "f \<in> carrier G" and carr'[simp]: "set fs' \<subseteq> carrier G"
   3.123      by (simp_all add: fs)
   3.124 @@ -1874,6 +1846,18 @@
   3.125  qed
   3.126  
   3.127  lemma (in factorial_monoid) properfactor_fmset:
   3.128 +  assumes "properfactor G a b"
   3.129 +    and "wfactors G as a"
   3.130 +    and "wfactors G bs b"
   3.131 +    and "a \<in> carrier G"
   3.132 +    and "b \<in> carrier G"
   3.133 +    and "set as \<subseteq> carrier G"
   3.134 +    and "set bs \<subseteq> carrier G"
   3.135 +  shows "fmset G as \<subseteq># fmset G bs"
   3.136 +  using assms
   3.137 +  by (meson divides_as_fmsubset properfactor_divides)
   3.138 +
   3.139 +lemma (in factorial_monoid) properfactor_fmset_ne:
   3.140    assumes pf: "properfactor G a b"
   3.141      and "wfactors G as a"
   3.142      and "wfactors G bs b"
   3.143 @@ -1881,11 +1865,8 @@
   3.144      and "b \<in> carrier G"
   3.145      and "set as \<subseteq> carrier G"
   3.146      and "set bs \<subseteq> carrier G"
   3.147 -  shows "fmset G as \<subseteq># fmset G bs \<and> fmset G as \<noteq> fmset G bs"
   3.148 -  using pf
   3.149 -  apply safe
   3.150 -   apply (meson assms divides_as_fmsubset monoid.properfactor_divides monoid_axioms)
   3.151 -  by (meson assms associated_def comm_monoid_cancel.ee_wfactorsD comm_monoid_cancel.fmset_ee factorial_monoid_axioms factorial_monoid_def properfactorE)
   3.152 +  shows "fmset G as \<noteq> fmset G bs"
   3.153 +  using properfactorE [OF pf] assms divides_as_fmsubset by force
   3.154  
   3.155  subsection \<open>Irreducible Elements are Prime\<close>
   3.156  
   3.157 @@ -2246,75 +2227,70 @@
   3.158  qed
   3.159  
   3.160  lemma (in gcd_condition_monoid) gcdof_cong_l:
   3.161 -  assumes a'a: "a' \<sim> a"
   3.162 -    and agcd: "a gcdof b c"
   3.163 -    and a'carr: "a' \<in> carrier G" and carr': "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
   3.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"
   3.165    shows "a' gcdof b c"
   3.166  proof -
   3.167 -  note carr = a'carr carr'
   3.168    interpret weak_lower_semilattice "division_rel G" by simp
   3.169    have "is_glb (division_rel G) a' {b, c}"
   3.170 -    by (subst greatest_Lower_cong_l[of _ a]) (simp_all add: a'a carr gcdof_greatestLower[symmetric] agcd)
   3.171 +    by (subst greatest_Lower_cong_l[of _ a]) (simp_all add: assms gcdof_greatestLower[symmetric])
   3.172    then have "a' \<in> carrier G \<and> a' gcdof b c"
   3.173      by (simp add: gcdof_greatestLower carr')
   3.174    then show ?thesis ..
   3.175  qed
   3.176  
   3.177  lemma (in gcd_condition_monoid) gcd_closed [simp]:
   3.178 -  assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
   3.179 +  assumes "a \<in> carrier G" "b \<in> carrier G"
   3.180    shows "somegcd G a b \<in> carrier G"
   3.181  proof -
   3.182    interpret weak_lower_semilattice "division_rel G" by simp
   3.183    show ?thesis
   3.184 -    apply (simp add: somegcd_meet[OF carr])
   3.185 -    apply (rule meet_closed[simplified], fact+)
   3.186 -    done
   3.187 +  using  assms meet_closed by (simp add: somegcd_meet)
   3.188  qed
   3.189  
   3.190  lemma (in gcd_condition_monoid) gcd_isgcd:
   3.191 -  assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
   3.192 +  assumes "a \<in> carrier G"  "b \<in> carrier G"
   3.193    shows "(somegcd G a b) gcdof a b"
   3.194  proof -
   3.195    interpret weak_lower_semilattice "division_rel G"
   3.196      by simp
   3.197 -  from carr have "somegcd G a b \<in> carrier G \<and> (somegcd G a b) gcdof a b"
   3.198 +  from assms have "somegcd G a b \<in> carrier G \<and> (somegcd G a b) gcdof a b"
   3.199      by (simp add: gcdof_greatestLower inf_of_two_greatest meet_def somegcd_meet)
   3.200    then show "(somegcd G a b) gcdof a b"
   3.201      by simp
   3.202  qed
   3.203  
   3.204  lemma (in gcd_condition_monoid) gcd_exists:
   3.205 -  assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
   3.206 +  assumes "a \<in> carrier G"  "b \<in> carrier G"
   3.207    shows "\<exists>x\<in>carrier G. x = somegcd G a b"
   3.208  proof -
   3.209    interpret weak_lower_semilattice "division_rel G"
   3.210      by simp
   3.211    show ?thesis
   3.212 -    by (metis carr(1) carr(2) gcd_closed)
   3.213 +    by (metis assms gcd_closed)
   3.214  qed
   3.215  
   3.216  lemma (in gcd_condition_monoid) gcd_divides_l:
   3.217 -  assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
   3.218 +  assumes "a \<in> carrier G" "b \<in> carrier G"
   3.219    shows "(somegcd G a b) divides a"
   3.220  proof -
   3.221    interpret weak_lower_semilattice "division_rel G"
   3.222      by simp
   3.223    show ?thesis
   3.224 -    by (metis carr(1) carr(2) gcd_isgcd isgcd_def)
   3.225 +    by (metis assms gcd_isgcd isgcd_def)
   3.226  qed
   3.227  
   3.228  lemma (in gcd_condition_monoid) gcd_divides_r:
   3.229 -  assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
   3.230 +  assumes "a \<in> carrier G"  "b \<in> carrier G"
   3.231    shows "(somegcd G a b) divides b"
   3.232  proof -
   3.233    interpret weak_lower_semilattice "division_rel G"
   3.234      by simp
   3.235    show ?thesis
   3.236 -    by (metis carr gcd_isgcd isgcd_def)
   3.237 +    by (metis assms gcd_isgcd isgcd_def)
   3.238  qed
   3.239  
   3.240  lemma (in gcd_condition_monoid) gcd_divides:
   3.241 -  assumes sub: "z divides x"  "z divides y"
   3.242 +  assumes "z divides x" "z divides y"
   3.243      and L: "x \<in> carrier G"  "y \<in> carrier G"  "z \<in> carrier G"
   3.244    shows "z divides (somegcd G x y)"
   3.245  proof -
   3.246 @@ -2325,49 +2301,25 @@
   3.247  qed
   3.248  
   3.249  lemma (in gcd_condition_monoid) gcd_cong_l:
   3.250 -  assumes xx': "x \<sim> x'"
   3.251 -    and carr: "x \<in> carrier G"  "x' \<in> carrier G"  "y \<in> carrier G"
   3.252 +  assumes "x \<sim> x'" "x \<in> carrier G"  "x' \<in> carrier G"  "y \<in> carrier G"
   3.253    shows "somegcd G x y \<sim> somegcd G x' y"
   3.254  proof -
   3.255    interpret weak_lower_semilattice "division_rel G"
   3.256      by simp
   3.257    show ?thesis
   3.258 -    apply (simp add: somegcd_meet carr)
   3.259 -    apply (rule meet_cong_l[simplified], fact+)
   3.260 -    done
   3.261 +    using somegcd_meet assms
   3.262 +    by (metis eq_object.select_convs(1) meet_cong_l partial_object.select_convs(1))
   3.263  qed
   3.264  
   3.265  lemma (in gcd_condition_monoid) gcd_cong_r:
   3.266 -  assumes carr: "x \<in> carrier G"  "y \<in> carrier G"  "y' \<in> carrier G"
   3.267 -    and yy': "y \<sim> y'"
   3.268 +  assumes "y \<sim> y'" "x \<in> carrier G"  "y \<in> carrier G" "y' \<in> carrier G"
   3.269    shows "somegcd G x y \<sim> somegcd G x y'"
   3.270  proof -
   3.271    interpret weak_lower_semilattice "division_rel G" by simp
   3.272    show ?thesis
   3.273 -    apply (simp add: somegcd_meet carr)
   3.274 -    apply (rule meet_cong_r[simplified], fact+)
   3.275 -    done
   3.276 +    by (meson associated_def assms gcd_closed gcd_divides gcd_divides_l gcd_divides_r monoid.divides_trans monoid_axioms)
   3.277  qed
   3.278  
   3.279 -(*
   3.280 -lemma (in gcd_condition_monoid) asc_cong_gcd_l [intro]:
   3.281 -  assumes carr: "b \<in> carrier G"
   3.282 -  shows "asc_cong (\<lambda>a. somegcd G a b)"
   3.283 -using carr
   3.284 -unfolding CONG_def
   3.285 -by clarsimp (blast intro: gcd_cong_l)
   3.286 -
   3.287 -lemma (in gcd_condition_monoid) asc_cong_gcd_r [intro]:
   3.288 -  assumes carr: "a \<in> carrier G"
   3.289 -  shows "asc_cong (\<lambda>b. somegcd G a b)"
   3.290 -using carr
   3.291 -unfolding CONG_def
   3.292 -by clarsimp (blast intro: gcd_cong_r)
   3.293 -
   3.294 -lemmas (in gcd_condition_monoid) asc_cong_gcd_split [simp] =
   3.295 -    assoc_split[OF _ asc_cong_gcd_l] assoc_split[OF _ asc_cong_gcd_r]
   3.296 -*)
   3.297 -
   3.298  lemma (in gcd_condition_monoid) gcdI:
   3.299    assumes dvd: "a divides b"  "a divides c"
   3.300      and others: "\<And>y. \<lbrakk>y\<in>carrier G; y divides b; y divides c\<rbrakk> \<Longrightarrow> y divides a"
   3.301 @@ -2390,25 +2342,23 @@
   3.302  
   3.303  lemma (in gcd_condition_monoid) SomeGcd_ex:
   3.304    assumes "finite A"  "A \<subseteq> carrier G"  "A \<noteq> {}"
   3.305 -  shows "\<exists>x\<in> carrier G. x = SomeGcd G A"
   3.306 +  shows "\<exists>x \<in> carrier G. x = SomeGcd G A"
   3.307  proof -
   3.308    interpret weak_lower_semilattice "division_rel G"
   3.309      by simp
   3.310    show ?thesis
   3.311 -    apply (simp add: SomeGcd_def)
   3.312 -    apply (rule finite_inf_closed[simplified], fact+)
   3.313 -    done
   3.314 +    using finite_inf_closed by (simp add: assms SomeGcd_def)
   3.315  qed
   3.316  
   3.317  lemma (in gcd_condition_monoid) gcd_assoc:
   3.318 -  assumes carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
   3.319 +  assumes "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
   3.320    shows "somegcd G (somegcd G a b) c \<sim> somegcd G a (somegcd G b c)"
   3.321  proof -
   3.322    interpret weak_lower_semilattice "division_rel G"
   3.323      by simp
   3.324    show ?thesis
   3.325      unfolding associated_def
   3.326 -    by (meson carr divides_trans gcd_divides gcd_divides_l gcd_divides_r gcd_exists)
   3.327 +    by (meson assms divides_trans gcd_divides gcd_divides_l gcd_divides_r gcd_exists)
   3.328  qed
   3.329  
   3.330  lemma (in gcd_condition_monoid) gcd_mult:
   3.331 @@ -2641,141 +2591,124 @@
   3.332      using Cons.IH Cons.prems(1) by force
   3.333  qed
   3.334  
   3.335 -
   3.336 -lemma (in primeness_condition_monoid) wfactors_unique__hlp_induct:
   3.337 -  "\<forall>a as'. a \<in> carrier G \<and> set as \<subseteq> carrier G \<and> set as' \<subseteq> carrier G \<and>
   3.338 -           wfactors G as a \<and> wfactors G as' a \<longrightarrow> essentially_equal G as as'"
   3.339 -proof (induct as)
   3.340 +proposition (in primeness_condition_monoid) wfactors_unique:
   3.341 +  assumes "wfactors G as a"  "wfactors G as' a"
   3.342 +    and "a \<in> carrier G"  "set as \<subseteq> carrier G"  "set as' \<subseteq> carrier G"
   3.343 +  shows "essentially_equal G as as'"
   3.344 +  using assms
   3.345 +proof (induct as arbitrary: a as')
   3.346    case Nil
   3.347 -  show ?case
   3.348 -    apply (clarsimp simp: wfactors_def)
   3.349 -    by (metis Units_one_closed assoc_unit_r list_update_nonempty unit_wfactors_empty unitfactor_ee wfactorsI)
   3.350 +  then have "a \<sim> \<one>"
   3.351 +    by (meson Units_one_closed one_closed perm.Nil perm_wfactorsD unit_wfactors)
   3.352 +  then have "as' = []"
   3.353 +    using Nil.prems assoc_unit_l unit_wfactors_empty by blast
   3.354 +  then show ?case
   3.355 +    by auto
   3.356  next
   3.357    case (Cons ah as)
   3.358 -  then show ?case
   3.359 -  proof clarsimp
   3.360 -    fix a as'
   3.361 -    assume ih [rule_format]:
   3.362 -      "\<forall>a as'. a \<in> carrier G \<and> set as' \<subseteq> carrier G \<and> wfactors G as a \<and>
   3.363 -        wfactors G as' a \<longrightarrow> essentially_equal G as as'"
   3.364 -      and acarr: "a \<in> carrier G" and ahcarr: "ah \<in> carrier G"
   3.365 -      and ascarr: "set as \<subseteq> carrier G" and as'carr: "set as' \<subseteq> carrier G"
   3.366 -      and afs: "wfactors G (ah # as) a"
   3.367 -      and afs': "wfactors G as' a"
   3.368 -    then have ahdvda: "ah divides a"
   3.369 -      by (intro wfactors_dividesI[of "ah#as" "a"]) simp_all
   3.370 +  then have ahdvda: "ah divides a"
   3.371 +    using wfactors_dividesI by auto
   3.372      then obtain a' where a'carr: "a' \<in> carrier G" and a: "a = ah \<otimes> a'"
   3.373        by blast
   3.374 +    have carr_ah: "ah \<in> carrier G" "set as \<subseteq> carrier G"
   3.375 +      using Cons.prems by fastforce+
   3.376 +    have "ah \<otimes> foldr (\<otimes>) as \<one> \<sim> a"
   3.377 +      by (rule wfactorsE[OF \<open>wfactors G (ah # as) a\<close>]) auto
   3.378 +    then have "foldr (\<otimes>) as \<one> \<sim> a'"
   3.379 +      by (metis Cons.prems(4) a a'carr assoc_l_cancel insert_subset list.set(2) monoid.multlist_closed monoid_axioms)
   3.380 +    then
   3.381      have a'fs: "wfactors G as a'"
   3.382 -      apply (rule wfactorsE[OF afs], rule wfactorsI, simp)
   3.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)
   3.384 -    from afs have ahirr: "irreducible G ah"
   3.385 -      by (elim wfactorsE) simp
   3.386 -    with ascarr have ahprime: "prime G ah"
   3.387 -      by (intro irreducible_prime ahcarr)
   3.388 -
   3.389 -    note carr [simp] = acarr ahcarr ascarr as'carr a'carr
   3.390 -
   3.391 +      by (meson Cons.prems(1) set_subset_Cons subset_iff wfactorsE wfactorsI)
   3.392 +    then have ahirr: "irreducible G ah"
   3.393 +      by (meson Cons.prems(1) list.set_intros(1) wfactorsE)
   3.394 +    with Cons have ahprime: "prime G ah"
   3.395 +      by (simp add: irreducible_prime)
   3.396      note ahdvda
   3.397 -    also from afs' have "a divides (foldr (\<otimes>) as' \<one>)"
   3.398 -      by (elim wfactorsE associatedE, simp)
   3.399 +    also have "a divides (foldr (\<otimes>) as' \<one>)"
   3.400 +      by (meson Cons.prems(2) associatedE wfactorsE)
   3.401      finally have "ah divides (foldr (\<otimes>) as' \<one>)"
   3.402 -      by simp
   3.403 +      using Cons.prems(4) by auto
   3.404      with ahprime have "\<exists>i<length as'. ah divides as'!i"
   3.405 -      by (intro multlist_prime_pos) simp_all
   3.406 +      by (intro multlist_prime_pos) (use Cons.prems in auto)
   3.407      then obtain i where len: "i<length as'" and ahdvd: "ah divides as'!i"
   3.408        by blast
   3.409 -    from afs' carr have irrasi: "irreducible G (as'!i)"
   3.410 -      by (fast intro: nth_mem[OF len] elim: wfactorsE)
   3.411 -    from len carr have asicarr[simp]: "as'!i \<in> carrier G"
   3.412 -      unfolding set_conv_nth by force
   3.413 -    note carr = carr asicarr
   3.414 -
   3.415 -    from ahdvd obtain x where "x \<in> carrier G" and asi: "as'!i = ah \<otimes> x"
   3.416 +    then obtain x where "x \<in> carrier G" and asi: "as'!i = ah \<otimes> x"
   3.417        by blast
   3.418 -    with carr irrasi[simplified asi] have asiah: "as'!i \<sim> ah"
   3.419 -      by (metis ahprime associatedI2 irreducible_prodE primeE)
   3.420 +    have irrasi: "irreducible G (as'!i)"
   3.421 +      using nth_mem[OF len] wfactorsE
   3.422 +      by (metis Cons.prems(2))
   3.423 +    have asicarr[simp]: "as'!i \<in> carrier G"
   3.424 +      using len \<open>set as' \<subseteq> carrier G\<close> nth_mem by blast
   3.425 +    have asiah: "as'!i \<sim> ah"
   3.426 +      by (metis \<open>ah \<in> carrier G\<close> \<open>x \<in> carrier G\<close> asi irrasi ahprime associatedI2 irreducible_prodE primeE)
   3.427      note setparts = set_take_subset[of i as'] set_drop_subset[of "Suc i" as']
   3.428 -    note partscarr [simp] = setparts[THEN subset_trans[OF _ as'carr]]
   3.429 -    note carr = carr partscarr
   3.430 -
   3.431      have "\<exists>aa_1. aa_1 \<in> carrier G \<and> wfactors G (take i as') aa_1"
   3.432 -      by (meson afs' in_set_takeD partscarr(1) wfactorsE wfactors_prod_exists)
   3.433 -    then obtain aa_1 where aa1carr: "aa_1 \<in> carrier G" and aa1fs: "wfactors G (take i as') aa_1"
   3.434 +      using Cons
   3.435 +      by (metis setparts(1) subset_trans in_set_takeD wfactorsE wfactors_prod_exists)
   3.436 +    then obtain aa_1 where aa1carr [simp]: "aa_1 \<in> carrier G" and aa1fs: "wfactors G (take i as') aa_1"
   3.437        by auto
   3.438 -
   3.439 -    have "\<exists>aa_2. aa_2 \<in> carrier G \<and> wfactors G (drop (Suc i) as') aa_2"
   3.440 -      by (meson afs' in_set_dropD partscarr(2) wfactors_def wfactors_prod_exists)
   3.441 -    then obtain aa_2 where aa2carr: "aa_2 \<in> carrier G"
   3.442 +    obtain aa_2 where aa2carr [simp]: "aa_2 \<in> carrier G"
   3.443        and aa2fs: "wfactors G (drop (Suc i) as') aa_2"
   3.444 -      by auto
   3.445 -
   3.446 -    note carr = carr aa1carr[simp] aa2carr[simp]
   3.447 -
   3.448 -    from aa1fs aa2fs
   3.449 -    have v1: "wfactors G (take i as' @ drop (Suc i) as') (aa_1 \<otimes> aa_2)"
   3.450 -      by (intro wfactors_mult, simp+)
   3.451 -    then have v1': "wfactors G (as'!i # take i as' @ drop (Suc i) as') (as'!i \<otimes> (aa_1 \<otimes> aa_2))"
   3.452 -      using irrasi wfactors_mult_single by auto
   3.453 -    from aa2carr carr aa1fs aa2fs have "wfactors G (as'!i # drop (Suc i) as') (as'!i \<otimes> aa_2)"
   3.454 -      by (metis irrasi wfactors_mult_single)
   3.455 -    with len carr aa1carr aa2carr aa1fs
   3.456 +      by (metis Cons.prems(2) Cons.prems(5) subset_code(1) in_set_dropD wfactors_def wfactors_prod_exists)
   3.457 +
   3.458 +    have set_drop: "set (drop (Suc i) as') \<subseteq> carrier G"
   3.459 +      using Cons.prems(5) setparts(2) by blast
   3.460 +    moreover have set_take: "set (take i as') \<subseteq> carrier G"
   3.461 +      using  Cons.prems(5) setparts by auto
   3.462 +    moreover have v1: "wfactors G (take i as' @ drop (Suc i) as') (aa_1 \<otimes> aa_2)"
   3.463 +      using aa1fs aa2fs \<open>set as' \<subseteq> carrier G\<close> by (force simp add: dest: in_set_takeD in_set_dropD)
   3.464 +    ultimately have v1': "wfactors G (as'!i # take i as' @ drop (Suc i) as') (as'!i \<otimes> (aa_1 \<otimes> aa_2))"
   3.465 +      using irrasi wfactors_mult_single
   3.466 +        by (simp add: irrasi v1 wfactors_mult_single)      
   3.467 +    have "wfactors G (as'!i # drop (Suc i) as') (as'!i \<otimes> aa_2)"
   3.468 +      by (simp add: aa2fs irrasi set_drop wfactors_mult_single)
   3.469 +    with len  aa1carr aa2carr aa1fs
   3.470      have v2: "wfactors G (take i as' @ as'!i # drop (Suc i) as') (aa_1 \<otimes> (as'!i \<otimes> aa_2))"
   3.471 -      using wfactors_mult by auto
   3.472 +      using wfactors_mult  by (simp add: set_take set_drop) 
   3.473      from len have as': "as' = (take i as' @ as'!i # drop (Suc i) as')"
   3.474        by (simp add: Cons_nth_drop_Suc)
   3.475 -    with carr have eer: "essentially_equal G (take i as' @ as'!i # drop (Suc i) as') as'"
   3.476 -      by simp
   3.477 -    with v2 afs' carr aa1carr aa2carr nth_mem[OF len] have "aa_1 \<otimes> (as'!i \<otimes> aa_2) \<sim> a"
   3.478 -      by (metis as' ee_wfactorsD m_closed)
   3.479 +    have eer: "essentially_equal G (take i as' @ as'!i # drop (Suc i) as') as'"
   3.480 +      using Cons.prems(5) as' by auto
   3.481 +    with v2 aa1carr aa2carr nth_mem[OF len] have "aa_1 \<otimes> (as'!i \<otimes> aa_2) \<sim> a"
   3.482 +      using Cons.prems as' comm_monoid_cancel.ee_wfactorsD is_comm_monoid_cancel by fastforce
   3.483      then have t1: "as'!i \<otimes> (aa_1 \<otimes> aa_2) \<sim> a"
   3.484        by (metis aa1carr aa2carr asicarr m_lcomm)
   3.485 -    from carr asiah have "ah \<otimes> (aa_1 \<otimes> aa_2) \<sim> as'!i \<otimes> (aa_1 \<otimes> aa_2)"
   3.486 -      by (metis associated_sym m_closed mult_cong_l)
   3.487 +    from asiah have "ah \<otimes> (aa_1 \<otimes> aa_2) \<sim> as'!i \<otimes> (aa_1 \<otimes> aa_2)"
   3.488 +      by (simp add: \<open>ah \<in> carrier G\<close> associated_sym mult_cong_l)
   3.489      also note t1
   3.490 -    finally have "ah \<otimes> (aa_1 \<otimes> aa_2) \<sim> a" by simp
   3.491 -
   3.492 -    with carr aa1carr aa2carr a'carr nth_mem[OF len] have a': "aa_1 \<otimes> aa_2 \<sim> a'"
   3.493 -      by (simp add: a, fast intro: assoc_l_cancel[of ah _ a'])
   3.494 -
   3.495 +    finally have "ah \<otimes> (aa_1 \<otimes> aa_2) \<sim> a"
   3.496 +      using Cons.prems(3) carr_ah aa1carr aa2carr by blast
   3.497 +    with aa1carr aa2carr a'carr nth_mem[OF len] have a': "aa_1 \<otimes> aa_2 \<sim> a'"
   3.498 +      using a assoc_l_cancel carr_ah(1) by blast
   3.499      note v1
   3.500      also note a'
   3.501      finally have "wfactors G (take i as' @ drop (Suc i) as') a'"
   3.502 -      by simp
   3.503 -
   3.504 -    from a'fs this carr have "essentially_equal G as (take i as' @ drop (Suc i) as')"
   3.505 -      by (intro ih[of a']) simp
   3.506 -    then have ee1: "essentially_equal G (ah # as) (ah # take i as' @ drop (Suc i) as')"
   3.507 -      by (elim essentially_equalE) (fastforce intro: essentially_equalI)
   3.508 -
   3.509 -    from carr have ee2: "essentially_equal G (ah # take i as' @ drop (Suc i) as')
   3.510 +      by (simp add: a'carr set_drop set_take)
   3.511 +    from a'fs this have "essentially_equal G as (take i as' @ drop (Suc i) as')"
   3.512 +      using Cons.hyps a'carr carr_ah(2) set_drop set_take by auto
   3.513 +    with carr_ah have ee1: "essentially_equal G (ah # as) (ah # take i as' @ drop (Suc i) as')"
   3.514 +      by (auto simp: essentially_equal_def)
   3.515 +    have ee2: "essentially_equal G (ah # take i as' @ drop (Suc i) as')
   3.516        (as' ! i # take i as' @ drop (Suc i) as')"
   3.517      proof (intro essentially_equalI)
   3.518        show "ah # take i as' @ drop (Suc i) as' <~~> ah # take i as' @ drop (Suc i) as'"
   3.519          by simp
   3.520      next
   3.521        show "ah # take i as' @ drop (Suc i) as' [\<sim>] as' ! i # take i as' @ drop (Suc i) as'"
   3.522 -        by (simp add: list_all2_append) (simp add: asiah[symmetric])
   3.523 +        by (simp add: asiah associated_sym set_drop set_take)
   3.524      qed
   3.525  
   3.526      note ee1
   3.527      also note ee2
   3.528      also have "essentially_equal G (as' ! i # take i as' @ drop (Suc i) as')
   3.529                                     (take i as' @ as' ! i # drop (Suc i) as')"
   3.530 -      by (metis as' as'carr listassoc_refl essentially_equalI perm_append_Cons)
   3.531 +      by (metis Cons.prems(5) as' essentially_equalI listassoc_refl perm_append_Cons)
   3.532      finally have "essentially_equal G (ah # as) (take i as' @ as' ! i # drop (Suc i) as')"
   3.533 -      by simp
   3.534 -    then show "essentially_equal G (ah # as) as'"
   3.535 -      by (subst as')
   3.536 -  qed
   3.537 +      using Cons.prems(4) set_drop set_take by auto
   3.538 +    then show ?case
   3.539 +      using as' by auto
   3.540  qed
   3.541  
   3.542 -lemma (in primeness_condition_monoid) wfactors_unique:
   3.543 -  assumes "wfactors G as a"  "wfactors G as' a"
   3.544 -    and "a \<in> carrier G"  "set as \<subseteq> carrier G"  "set as' \<subseteq> carrier G"
   3.545 -  shows "essentially_equal G as as'"
   3.546 -  by (rule wfactors_unique__hlp_induct[rule_format, of a]) (simp add: assms)
   3.547 -
   3.548  
   3.549  subsubsection \<open>Application to factorial monoids\<close>
   3.550  
   3.551 @@ -2841,7 +2774,6 @@
   3.552      by blast
   3.553  
   3.554    note [simp] = acarr bcarr ccarr ascarr cscarr
   3.555 -
   3.556    assume b: "b = a \<otimes> c"
   3.557    from afs cfs have "wfactors G (as@cs) (a \<otimes> c)"
   3.558      by (intro wfactors_mult) simp_all
   3.559 @@ -2918,9 +2850,7 @@
   3.560    apply unfold_locales
   3.561    apply (rule wfUNIVI)
   3.562    apply (rule measure_induct[of "factorcount G"])
   3.563 -  apply simp
   3.564 -  apply (metis properfactor_fcount)
   3.565 -  done
   3.566 +  using properfactor_fcount by auto
   3.567  
   3.568  sublocale factorial_monoid \<subseteq> primeness_condition_monoid
   3.569    by standard (rule irreducible_prime)