# HG changeset patch # User paulson # Date 1532471105 -7200 # Node ID 9a42b84f8838f920950c7140e3147b8589dd4154 # Parent d69127c6e80ffefc5e62d5315ec1be5c3876d2cd de-applying diff -r d69127c6e80f -r 9a42b84f8838 src/HOL/Algebra/AbelCoset.thy --- a/src/HOL/Algebra/AbelCoset.thy Sun Jul 22 21:04:49 2018 +0200 +++ b/src/HOL/Algebra/AbelCoset.thy Wed Jul 25 00:25:05 2018 +0200 @@ -269,17 +269,15 @@ by (rule a_comm_group) interpret subgroup "H" "(add_monoid G)" by (rule a_subgroup) - - show "abelian_subgroup H G" - apply unfold_locales - proof (simp add: r_coset_def l_coset_def, clarsimp) - fix x - assume xcarr: "x \ carrier G" - from a_subgroup have Hcarr: "H \ carrier G" - unfolding subgroup_def by simp - from xcarr Hcarr show "(\h\H. {h \\<^bsub>G\<^esub> x}) = (\h\H. {x \\<^bsub>G\<^esub> h})" + have "(\xa\H. {xa \ x}) = (\xa\H. {x \ xa})" if "x \ carrier G" for x + proof - + have "H \ carrier G" + using a_subgroup that unfolding subgroup_def by simp + with that show "(\h\H. {h \\<^bsub>G\<^esub> x}) = (\h\H. {x \\<^bsub>G\<^esub> h})" using m_comm [simplified] by fastforce qed + then show "abelian_subgroup H G" + by unfold_locales (auto simp: r_coset_def l_coset_def) qed lemma abelian_subgroupI3: @@ -304,14 +302,6 @@ by (rule normal.inv_op_closed2 [OF a_normal, folded a_inv_def, simplified monoid_record_simps]) -text\Alternative characterization of normal subgroups\ -lemma (in abelian_group) a_normal_inv_iff: - "(N \ (add_monoid G)) = - (subgroup N (add_monoid G) & (\x \ carrier G. \h \ N. x \ h \ (\ x) \ N))" - (is "_ = ?rhs") -by (rule group.normal_inv_iff [OF a_group, - folded a_inv_def, simplified monoid_record_simps]) - lemma (in abelian_group) a_lcos_m_assoc: "\ M \ carrier G; g \ carrier G; h \ carrier G \ \ g <+ (h <+ M) = (g \ h) <+ M" by (rule group.lcos_m_assoc [OF a_group, @@ -322,13 +312,11 @@ by (rule group.lcos_mult_one [OF a_group, folded a_l_coset_def, simplified monoid_record_simps]) - lemma (in abelian_group) a_l_coset_subset_G: "\ H \ carrier G; x \ carrier G \ \ x <+ H \ carrier G" by (rule group.l_coset_subset_G [OF a_group, folded a_l_coset_def, simplified monoid_record_simps]) - lemma (in abelian_group) a_l_coset_swap: "\y \ x <+ H; x \ carrier G; subgroup H (add_monoid G)\ \ x \ y <+ H" by (rule group.l_coset_swap [OF a_group, @@ -498,15 +486,15 @@ text \Since the Factorization is based on an \emph{abelian} subgroup, is results in a commutative group\ -theorem (in abelian_subgroup) a_factorgroup_is_comm_group: - "comm_group (G A_Mod H)" -apply (intro comm_group.intro comm_monoid.intro) prefer 3 - apply (rule a_factorgroup_is_group) - apply (rule group.axioms[OF a_factorgroup_is_group]) -apply (rule comm_monoid_axioms.intro) -apply (unfold A_FactGroup_def FactGroup_def RCOSETS_def, fold set_add_def a_r_coset_def, clarsimp) -apply (simp add: a_rcos_sum a_comm) -done +theorem (in abelian_subgroup) a_factorgroup_is_comm_group: "comm_group (G A_Mod H)" +proof - + have "Group.comm_monoid_axioms (G A_Mod H)" + apply (rule comm_monoid_axioms.intro) + apply (auto simp: A_FactGroup_def FactGroup_def RCOSETS_def a_normal add.m_comm normal.rcos_sum) + done + then show ?thesis + by (intro comm_group.intro comm_monoid.intro) (simp_all add: a_factorgroup_is_group group.is_monoid) +qed lemma add_A_FactGroup [simp]: "X \\<^bsub>(G A_Mod H)\<^esub> X' = X <+>\<^bsub>G\<^esub> X'" by (simp add: A_FactGroup_def set_add_def) @@ -552,11 +540,8 @@ interpret G: abelian_group G by fact interpret H: abelian_group H by fact show ?thesis - apply (intro abelian_group_hom.intro abelian_group_hom_axioms.intro) - apply fact - apply fact - apply (rule a_group_hom) - done + by (intro abelian_group_hom.intro abelian_group_hom_axioms.intro + G.abelian_group_axioms H.abelian_group_axioms a_group_hom) qed lemma (in abelian_group_hom) is_abelian_group_hom: @@ -576,8 +561,7 @@ lemma (in abelian_group_hom) zero_closed [simp]: "h \ \ carrier H" -by (rule group_hom.one_closed[OF a_group_hom, - simplified ring_record_simps]) + by simp lemma (in abelian_group_hom) hom_zero [simp]: "h \ = \\<^bsub>H\<^esub>" @@ -586,8 +570,7 @@ lemma (in abelian_group_hom) a_inv_closed [simp]: "x \ carrier G ==> h (\x) \ carrier H" -by (rule group_hom.inv_closed[OF a_group_hom, - folded a_inv_def, simplified ring_record_simps]) + by simp lemma (in abelian_group_hom) hom_a_inv [simp]: "x \ carrier G ==> h (\x) = \\<^bsub>H\<^esub> (h x)" @@ -596,19 +579,15 @@ lemma (in abelian_group_hom) additive_subgroup_a_kernel: "additive_subgroup (a_kernel G H h) G" -apply (rule additive_subgroup.intro) -apply (rule group_hom.subgroup_kernel[OF a_group_hom, - folded a_kernel_def, simplified ring_record_simps]) -done + by (simp add: additive_subgroup.intro a_group_hom a_kernel_def group_hom.subgroup_kernel) text\The kernel of a homomorphism is an abelian subgroup\ lemma (in abelian_group_hom) abelian_subgroup_a_kernel: "abelian_subgroup (a_kernel G H h) G" -apply (rule abelian_subgroupI) -apply (rule group_hom.normal_kernel[OF a_group_hom, - folded a_kernel_def, simplified ring_record_simps]) -apply (simp add: G.a_comm) -done + apply (rule abelian_subgroupI) + apply (simp add: G.abelian_group_axioms abelian_subgroup.a_normal abelian_subgroupI3 additive_subgroup_a_kernel) + apply (simp add: G.a_comm) + done lemma (in abelian_group_hom) A_FactGroup_nonempty: assumes X: "X \ carrier (G A_Mod a_kernel G H h)" @@ -715,48 +694,34 @@ qed lemma (in abelian_subgroup) a_repr_independence': - assumes y: "y \ H +> x" - and xcarr: "x \ carrier G" + assumes "y \ H +> x" "x \ carrier G" shows "H +> x = H +> y" - apply (rule a_repr_independence) - apply (rule y) - apply (rule xcarr) - apply (rule a_subgroup) - done + using a_repr_independence a_subgroup assms by blast lemma (in abelian_subgroup) a_repr_independenceD: - assumes ycarr: "y \ carrier G" - and repr: "H +> x = H +> y" + assumes "y \ carrier G" "H +> x = H +> y" shows "y \ H +> x" -by (rule group.repr_independenceD [OF a_group a_subgroup, - folded a_r_coset_def, simplified monoid_record_simps]) (rule ycarr, rule repr) + by (simp add: a_rcos_self assms) lemma (in abelian_subgroup) a_rcosets_carrier: "X \ a_rcosets H \ X \ carrier G" -by (rule subgroup.rcosets_carrier [OF a_subgroup a_group, - folded A_RCOSETS_def, simplified monoid_record_simps]) + using a_rcosets_part_G by auto subsubsection \Addition of Subgroups\ lemma (in abelian_monoid) set_add_closed: - assumes Acarr: "A \ carrier G" - and Bcarr: "B \ carrier G" + assumes "A \ carrier G" "B \ carrier G" shows "A <+> B \ carrier G" -by (rule monoid.set_mult_closed [OF a_monoid, - folded set_add_def, simplified monoid_record_simps]) (rule Acarr, rule Bcarr) + by (simp add: assms add.set_mult_closed set_add_defs(1)) lemma (in abelian_group) add_additive_subgroups: assumes subH: "additive_subgroup H G" - and subK: "additive_subgroup K G" + and subK: "additive_subgroup K G" shows "additive_subgroup (H <+> K) G" -apply (rule additive_subgroup.intro) -apply (unfold set_add_def) -apply (intro comm_group.mult_subgroups) - apply (rule a_comm_group) - apply (rule additive_subgroup.a_subgroup[OF subH]) -apply (rule additive_subgroup.a_subgroup[OF subK]) -done + unfolding set_add_def + using add.mult_subgroups additive_subgroup_def subH subK + by (blast intro: additive_subgroup.intro) end diff -r d69127c6e80f -r 9a42b84f8838 src/HOL/Algebra/Complete_Lattice.thy --- a/src/HOL/Algebra/Complete_Lattice.thy Sun Jul 22 21:04:49 2018 +0200 +++ b/src/HOL/Algebra/Complete_Lattice.thy Wed Jul 25 00:25:05 2018 +0200 @@ -680,22 +680,25 @@ next case False show ?thesis - proof (rule_tac x="\\<^bsub>L\<^esub> A" in exI, rule least_UpperI, simp_all) + proof (intro exI least_UpperI, simp_all) show b:"\ x. x \ A \ x \\<^bsub>L\<^esub> \\<^bsub>L\<^esub>A" using a by (auto intro: L.sup_upper, meson L.at_least_at_most_closed L.sup_upper subset_trans) show "\y. y \ Upper (L\carrier := \a..b\\<^bsub>L\<^esub>\) A \ \\<^bsub>L\<^esub>A \\<^bsub>L\<^esub> y" using a L.at_least_at_most_closed by (rule_tac L.sup_least, auto intro: funcset_mem simp add: Upper_def) - from a show "A \ \a..b\\<^bsub>L\<^esub>" - by (auto) - from a show "\\<^bsub>L\<^esub>A \ \a..b\\<^bsub>L\<^esub>" - apply (rule_tac L.at_least_at_most_member) - apply (auto) - apply (meson L.at_least_at_most_closed L.sup_closed subset_trans) - apply (meson False L.at_least_at_most_closed L.at_least_at_most_lower L.le_trans L.sup_closed b all_not_in_conv assms(2) contra_subsetD subset_trans) - apply (rule L.sup_least) - apply (auto simp add: assms) - using L.at_least_at_most_closed apply blast - done + from a show *: "A \ \a..b\\<^bsub>L\<^esub>" + by auto + show "\\<^bsub>L\<^esub>A \ \a..b\\<^bsub>L\<^esub>" + proof (rule_tac L.at_least_at_most_member) + show 1: "\\<^bsub>L\<^esub>A \ carrier L" + by (meson L.at_least_at_most_closed L.sup_closed subset_trans *) + show "a \\<^bsub>L\<^esub> \\<^bsub>L\<^esub>A" + by (meson "*" False L.at_least_at_most_closed L.at_least_at_most_lower L.le_trans L.sup_upper 1 all_not_in_conv assms(2) set_mp subset_trans) + show "\\<^bsub>L\<^esub>A \\<^bsub>L\<^esub> b" + proof (rule L.sup_least) + show "A \ carrier L" "\x. x \ A \ x \\<^bsub>L\<^esub> b" + using * L.at_least_at_most_closed by blast+ + qed (simp add: assms) + qed qed qed show "\s. is_glb (L\carrier := \a..b\\<^bsub>L\<^esub>\) s A" @@ -711,15 +714,17 @@ using a L.at_least_at_most_closed by (force intro!: L.inf_lower) show "\y. y \ Lower (L\carrier := \a..b\\<^bsub>L\<^esub>\) A \ y \\<^bsub>L\<^esub> \\<^bsub>L\<^esub>A" using a L.at_least_at_most_closed by (rule_tac L.inf_greatest, auto intro: funcset_carrier' simp add: Lower_def) - from a show "A \ \a..b\\<^bsub>L\<^esub>" - by (auto) - from a show "\\<^bsub>L\<^esub>A \ \a..b\\<^bsub>L\<^esub>" - apply (rule_tac L.at_least_at_most_member) - apply (auto) - apply (meson L.at_least_at_most_closed L.inf_closed subset_trans) - apply (meson L.at_least_at_most_closed L.at_least_at_most_lower L.inf_greatest assms(2) set_rev_mp subset_trans) - apply (meson False L.at_least_at_most_closed L.at_least_at_most_upper L.inf_closed L.le_trans b all_not_in_conv assms(3) contra_subsetD subset_trans) - done + from a show *: "A \ \a..b\\<^bsub>L\<^esub>" + by auto + show "\\<^bsub>L\<^esub>A \ \a..b\\<^bsub>L\<^esub>" + proof (rule_tac L.at_least_at_most_member) + show 1: "\\<^bsub>L\<^esub>A \ carrier L" + by (meson "*" L.at_least_at_most_closed L.inf_closed subset_trans) + show "a \\<^bsub>L\<^esub> \\<^bsub>L\<^esub>A" + by (meson "*" L.at_least_at_most_closed L.at_least_at_most_lower L.inf_greatest assms(2) subsetD subset_trans) + show "\\<^bsub>L\<^esub>A \\<^bsub>L\<^esub> b" + by (meson * 1 False L.at_least_at_most_closed L.at_least_at_most_upper L.inf_lower L.le_trans all_not_in_conv assms(3) set_mp subset_trans) + qed qed qed qed @@ -731,7 +736,7 @@ text \The set of fixed points of a complete lattice is itself a complete lattice\ theorem Knaster_Tarski: - assumes "weak_complete_lattice L" "f \ carrier L \ carrier L" "isotone L L f" + assumes "weak_complete_lattice L" and f: "f \ carrier L \ carrier L" and "isotone L L f" shows "weak_complete_lattice (fpl L f)" (is "weak_complete_lattice ?L'") proof - interpret L: weak_complete_lattice L @@ -805,15 +810,14 @@ show "is_lub ?L'' (LFP\<^bsub>?L'\<^esub> f) A" proof (rule least_UpperI, simp_all) fix x - assume "x \ Upper ?L'' A" - hence "LFP\<^bsub>?L'\<^esub> f \\<^bsub>?L'\<^esub> x" - apply (rule_tac L'.LFP_lowerbound) - apply (auto simp add: Upper_def) - apply (simp add: A AL L.at_least_at_most_member L.sup_least set_rev_mp) - apply (simp add: Pi_iff assms(2) fps_def, rule_tac L.weak_refl) - apply (auto) - apply (rule funcset_mem[of f "carrier L"], simp_all add: assms(2)) - done + assume x: "x \ Upper ?L'' A" + have "LFP\<^bsub>?L'\<^esub> f \\<^bsub>?L'\<^esub> x" + proof (rule L'.LFP_lowerbound, simp_all) + show "x \ \\\<^bsub>L\<^esub>A..\\<^bsub>L\<^esub>\\<^bsub>L\<^esub>" + using x by (auto simp add: Upper_def A AL L.at_least_at_most_member L.sup_least set_rev_mp) + with x show "f x \\<^bsub>L\<^esub> x" + by (simp add: Upper_def) (meson L.at_least_at_most_closed L.use_fps L.weak_refl subsetD f_top_chain imageI) + qed thus " LFP\<^bsub>?L'\<^esub> f \\<^bsub>L\<^esub> x" by (simp) next @@ -838,17 +842,13 @@ by (auto simp add: at_least_at_most_def) have "LFP\<^bsub>?L'\<^esub> f .=\<^bsub>?L'\<^esub> f (LFP\<^bsub>?L'\<^esub> f)" proof (rule "L'.LFP_weak_unfold", simp_all) - show "f \ \\\<^bsub>L\<^esub>A..\\<^bsub>L\<^esub>\\<^bsub>L\<^esub> \ \\\<^bsub>L\<^esub>A..\\<^bsub>L\<^esub>\\<^bsub>L\<^esub>" - apply (auto simp add: Pi_def at_least_at_most_def) - using assms(2) apply blast - apply (meson AL funcset_mem L.le_trans L.sup_closed assms(2) assms(3) pf_w use_iso2) - using assms(2) apply blast - done - from assms(3) show "Mono\<^bsub>L\carrier := \\\<^bsub>L\<^esub>A..\\<^bsub>L\<^esub>\\<^bsub>L\<^esub>\\<^esub> f" - apply (auto simp add: isotone_def) - using L'.weak_partial_order_axioms apply blast - apply (meson L.at_least_at_most_closed subsetCE) - done + have "\x. \x \ carrier L; \\<^bsub>L\<^esub>A \\<^bsub>L\<^esub> x\ \ \\<^bsub>L\<^esub>A \\<^bsub>L\<^esub> f x" + by (meson AL funcset_mem L.le_trans L.sup_closed assms(2) assms(3) pf_w use_iso2) + with f show "f \ \\\<^bsub>L\<^esub>A..\\<^bsub>L\<^esub>\\<^bsub>L\<^esub> \ \\\<^bsub>L\<^esub>A..\\<^bsub>L\<^esub>\\<^bsub>L\<^esub>" + by (auto simp add: Pi_def at_least_at_most_def) + show "Mono\<^bsub>L\carrier := \\\<^bsub>L\<^esub>A..\\<^bsub>L\<^esub>\\<^bsub>L\<^esub>\\<^esub> f" + using L'.weak_partial_order_axioms assms(3) + by (auto simp add: isotone_def) (meson L.at_least_at_most_closed subsetCE) qed thus "f (LFP\<^bsub>?L'\<^esub> f) .=\<^bsub>L\<^esub> LFP\<^bsub>?L'\<^esub> f" by (simp add: L.equivalence_axioms funcset_carrier' c assms(2) equivalence.sym) @@ -889,7 +889,6 @@ thus ?thesis by (meson AL L.inf_closed L.le_trans assms(3) b(1) b(2) fx use_iso2 w) qed - show "\\<^bsub>L\<^esub> \\<^bsub>L\<^esub> f x" by (simp add: fx) qed @@ -905,12 +904,16 @@ proof (rule greatest_LowerI, simp_all) fix x assume "x \ Lower ?L'' A" - hence "x \\<^bsub>?L'\<^esub> GFP\<^bsub>?L'\<^esub> f" - apply (rule_tac L'.GFP_upperbound) - apply (auto simp add: Lower_def) - apply (meson A AL L.at_least_at_most_member L.bottom_lower L.weak_complete_lattice_axioms fps_carrier subsetCE weak_complete_lattice.inf_greatest) - apply (simp add: funcset_carrier' L.sym assms(2) fps_def) - done + then have x: "\y. y \ A \ y \ fps L f \ x \\<^bsub>L\<^esub> y" "x \ fps L f" + by (auto simp add: Lower_def) + have "x \\<^bsub>?L'\<^esub> GFP\<^bsub>?L'\<^esub> f" + unfolding Lower_def + proof (rule_tac L'.GFP_upperbound; simp) + show "x \ \\\<^bsub>L\<^esub>..\\<^bsub>L\<^esub>A\\<^bsub>L\<^esub>" + by (meson x A AL L.at_least_at_most_member L.bottom_lower L.inf_greatest contra_subsetD fps_carrier) + show "x \\<^bsub>L\<^esub> f x" + using x by (simp add: funcset_carrier' L.sym assms(2) fps_def) + qed thus "x \\<^bsub>L\<^esub> GFP\<^bsub>?L'\<^esub> f" by (simp) next @@ -935,17 +938,14 @@ by (auto simp add: at_least_at_most_def) have "GFP\<^bsub>?L'\<^esub> f .=\<^bsub>?L'\<^esub> f (GFP\<^bsub>?L'\<^esub> f)" proof (rule "L'.GFP_weak_unfold", simp_all) - show "f \ \\\<^bsub>L\<^esub>..?w\\<^bsub>L\<^esub> \ \\\<^bsub>L\<^esub>..?w\\<^bsub>L\<^esub>" - apply (auto simp add: Pi_def at_least_at_most_def) - using assms(2) apply blast - apply (simp add: funcset_carrier' assms(2)) - apply (meson AL funcset_carrier L.inf_closed L.le_trans assms(2) assms(3) pf_w use_iso2) - done - from assms(3) show "Mono\<^bsub>L\carrier := \\\<^bsub>L\<^esub>..?w\\<^bsub>L\<^esub>\\<^esub> f" - apply (auto simp add: isotone_def) - using L'.weak_partial_order_axioms apply blast - using L.at_least_at_most_closed apply (blast intro: funcset_carrier') - done + have "\x. \x \ carrier L; x \\<^bsub>L\<^esub> \\<^bsub>L\<^esub>A\ \ f x \\<^bsub>L\<^esub> \\<^bsub>L\<^esub>A" + by (meson AL funcset_carrier L.inf_closed L.le_trans assms(2) assms(3) pf_w use_iso2) + with assms(2) show "f \ \\\<^bsub>L\<^esub>..?w\\<^bsub>L\<^esub> \ \\\<^bsub>L\<^esub>..?w\\<^bsub>L\<^esub>" + by (auto simp add: Pi_def at_least_at_most_def) + have "\x y. \x \ \\\<^bsub>L\<^esub>..\\<^bsub>L\<^esub>A\\<^bsub>L\<^esub>; y \ \\\<^bsub>L\<^esub>..\\<^bsub>L\<^esub>A\\<^bsub>L\<^esub>; x \\<^bsub>L\<^esub> y\ \ f x \\<^bsub>L\<^esub> f y" + by (meson L.at_least_at_most_closed subsetD use_iso1 assms(3)) + with L'.weak_partial_order_axioms show "Mono\<^bsub>L\carrier := \\\<^bsub>L\<^esub>..?w\\<^bsub>L\<^esub>\\<^esub> f" + by (auto simp add: isotone_def) qed thus "f (GFP\<^bsub>?L'\<^esub> f) .=\<^bsub>L\<^esub> GFP\<^bsub>?L'\<^esub> f" by (simp add: L.equivalence_axioms funcset_carrier' c assms(2) equivalence.sym) @@ -1117,17 +1117,16 @@ qed show "\\<^bsub>fpl L f\<^esub>A \\<^bsub>L\<^esub> f (\\<^bsub>L\<^esub>A)" proof - + have *: "\\<^bsub>fpl L f\<^esub>A \ carrier L" + using FA infA by blast have "\x. x \ A \ \\<^bsub>fpl L f\<^esub>A \\<^bsub>fpl L f\<^esub> x" by (rule L'.inf_lower, simp_all add: assms) hence "\\<^bsub>fpl L f\<^esub>A \\<^bsub>L\<^esub> (\\<^bsub>L\<^esub>A)" - apply (rule_tac L.inf_greatest, simp_all add: A) - using FA infA apply blast - done + by (rule_tac L.inf_greatest, simp_all add: A *) hence 1:"f(\\<^bsub>fpl L f\<^esub>A) \\<^bsub>L\<^esub> f(\\<^bsub>L\<^esub>A)" by (metis (no_types, lifting) A FA L.inf_closed assms(2) infA subsetCE use_iso1) have 2:"\\<^bsub>fpl L f\<^esub>A \\<^bsub>L\<^esub> f (\\<^bsub>fpl L f\<^esub>A)" by (metis (no_types, lifting) FA L.sym L.use_fps L.weak_complete_lattice_axioms PiE assms(4) infA subsetCE weak_complete_lattice_def weak_partial_order.weak_refl) - show ?thesis using FA fA infA by (auto intro!: L.le_trans[OF 2 1] ic fc, metis FA PiE assms(4) subsetCE) qed @@ -1189,21 +1188,11 @@ lemma sup_pres_is_join_pres: assumes "weak_sup_pres X Y f" shows "join_pres X Y f" - using assms - apply (simp add: join_pres_def weak_sup_pres_def, safe) - apply (rename_tac x y) - apply (drule_tac x="{x, y}" in spec) - apply (auto simp add: join_def) -done + using assms by (auto simp: join_pres_def weak_sup_pres_def join_def) lemma inf_pres_is_meet_pres: assumes "weak_inf_pres X Y f" shows "meet_pres X Y f" - using assms - apply (simp add: meet_pres_def weak_inf_pres_def, safe) - apply (rename_tac x y) - apply (drule_tac x="{x, y}" in spec) - apply (auto simp add: meet_def) -done + using assms by (auto simp: meet_pres_def weak_inf_pres_def meet_def) end diff -r d69127c6e80f -r 9a42b84f8838 src/HOL/Algebra/Divisibility.thy --- a/src/HOL/Algebra/Divisibility.thy Sun Jul 22 21:04:49 2018 +0200 +++ b/src/HOL/Algebra/Divisibility.thy Wed Jul 25 00:25:05 2018 +0200 @@ -547,22 +547,14 @@ using pf by (elim properfactorE) lemma (in monoid) properfactor_trans1 [trans]: - assumes dvds: "a divides b" "properfactor G b c" - and carr: "a \ carrier G" "c \ carrier G" + assumes "a divides b" "properfactor G b c" "a \ carrier G" "c \ carrier G" shows "properfactor G a c" - using dvds carr - apply (elim properfactorE, intro properfactorI) - apply (iprover intro: divides_trans)+ - done + by (meson divides_trans properfactorE properfactorI assms) lemma (in monoid) properfactor_trans2 [trans]: - assumes dvds: "properfactor G a b" "b divides c" - and carr: "a \ carrier G" "b \ carrier G" + assumes "properfactor G a b" "b divides c" "a \ carrier G" "b \ carrier G" shows "properfactor G a c" - using dvds carr - apply (elim properfactorE, intro properfactorI) - apply (iprover intro: divides_trans)+ - done + by (meson divides_trans properfactorE properfactorI assms) lemma properfactor_lless: fixes G (structure) @@ -660,23 +652,20 @@ using assms by (fast elim: irreducibleE) lemma (in monoid_cancel) irreducible_cong [trans]: - assumes irred: "irreducible G a" - and aa': "a \ a'" "a \ carrier G" "a' \ carrier G" + assumes "irreducible G a" "a \ a'" "a \ carrier G" "a' \ carrier G" shows "irreducible G a'" - using assms - apply (auto simp: irreducible_def assoc_unit_l) - apply (metis aa' associated_sym properfactor_cong_r) - done +proof - + have "a' divides a" + by (meson \a \ a'\ associated_def) + then show ?thesis + by (metis (no_types) assms assoc_unit_l irreducibleE irreducibleI monoid.properfactor_trans2 monoid_axioms) +qed lemma (in monoid) irreducible_prod_rI: - assumes airr: "irreducible G a" - and bunit: "b \ Units G" - and carr[simp]: "a \ carrier G" "b \ carrier G" + assumes "irreducible G a" "b \ Units G" "a \ carrier G" "b \ carrier G" shows "irreducible G (a \ b)" - using airr carr bunit - apply (elim irreducibleE, intro irreducibleI) - using prod_unit_r apply blast - using associatedI2' properfactor_cong_r by auto + using assms + by (metis (no_types, lifting) associatedI2' irreducible_def monoid.m_closed monoid_axioms prod_unit_r properfactor_cong_r) lemma (in comm_monoid) irreducible_prod_lI: assumes birr: "irreducible G b" @@ -764,9 +753,7 @@ and pp': "p \ p'" "p \ carrier G" "p' \ carrier G" shows "prime G p'" using assms - apply (auto simp: prime_def assoc_unit_l) - apply (metis pp' associated_sym divides_cong_l) - done + by (auto simp: prime_def assoc_unit_l) (metis pp' associated_sym divides_cong_l) (*by Paulo Emílio de Vilhena*) lemma (in comm_monoid_cancel) prime_irreducible: @@ -849,9 +836,7 @@ and "set as \ carrier G" and "set bs \ carrier G" shows "\a\set bs. irreducible G a" using assms - apply (clarsimp simp add: list_all2_conv_all_nth set_conv_nth) - apply (blast intro: irreducible_cong) - done + by (fastforce simp add: list_all2_conv_all_nth set_conv_nth intro: irreducible_cong) text \Permutations\ @@ -1001,15 +986,7 @@ then have f: "f \ carrier G" by blast show ?case - proof (cases "f = a") - case True - then show ?thesis - using Cons.prems by auto - next - case False - with Cons show ?thesis - by clarsimp (metis f divides_prod_l multlist_closed) - qed + using Cons.IH Cons.prems(1) Cons.prems(2) divides_prod_l f by auto qed auto lemma (in comm_monoid_cancel) multlist_listassoc_cong: @@ -1051,9 +1028,7 @@ and "set fs \ carrier G" and "set fs' \ carrier G" shows "foldr (\) fs \ \ foldr (\) fs' \" using assms - apply (elim essentially_equalE) - apply (simp add: multlist_perm_cong multlist_listassoc_cong perm_closed) - done + by (metis essentially_equal_def multlist_listassoc_cong multlist_perm_cong perm_closed) subsubsection \Factorization in irreducible elements\ @@ -1120,9 +1095,6 @@ and carr[simp]: "set fs \ carrier G" shows "fs = []" proof (cases fs) - case Nil - then show ?thesis . -next case fs: (Cons f fs') from carr have fcarr[simp]: "f \ carrier G" and carr'[simp]: "set fs' \ carrier G" by (simp_all add: fs) @@ -1874,6 +1846,18 @@ qed lemma (in factorial_monoid) properfactor_fmset: + assumes "properfactor G a b" + and "wfactors G as a" + and "wfactors G bs b" + and "a \ carrier G" + and "b \ carrier G" + and "set as \ carrier G" + and "set bs \ carrier G" + shows "fmset G as \# fmset G bs" + using assms + by (meson divides_as_fmsubset properfactor_divides) + +lemma (in factorial_monoid) properfactor_fmset_ne: assumes pf: "properfactor G a b" and "wfactors G as a" and "wfactors G bs b" @@ -1881,11 +1865,8 @@ and "b \ carrier G" and "set as \ carrier G" and "set bs \ carrier G" - shows "fmset G as \# fmset G bs \ fmset G as \ fmset G bs" - using pf - apply safe - apply (meson assms divides_as_fmsubset monoid.properfactor_divides monoid_axioms) - by (meson assms associated_def comm_monoid_cancel.ee_wfactorsD comm_monoid_cancel.fmset_ee factorial_monoid_axioms factorial_monoid_def properfactorE) + shows "fmset G as \ fmset G bs" + using properfactorE [OF pf] assms divides_as_fmsubset by force subsection \Irreducible Elements are Prime\ @@ -2246,75 +2227,70 @@ qed lemma (in gcd_condition_monoid) gcdof_cong_l: - assumes a'a: "a' \ a" - and agcd: "a gcdof b c" - and a'carr: "a' \ carrier G" and carr': "a \ carrier G" "b \ carrier G" "c \ carrier G" + assumes "a' \ a" "a gcdof b c" "a' \ carrier G" and carr': "a \ carrier G" "b \ carrier G" "c \ carrier G" shows "a' gcdof b c" proof - - note carr = a'carr carr' interpret weak_lower_semilattice "division_rel G" by simp have "is_glb (division_rel G) a' {b, c}" - by (subst greatest_Lower_cong_l[of _ a]) (simp_all add: a'a carr gcdof_greatestLower[symmetric] agcd) + by (subst greatest_Lower_cong_l[of _ a]) (simp_all add: assms gcdof_greatestLower[symmetric]) then have "a' \ carrier G \ a' gcdof b c" by (simp add: gcdof_greatestLower carr') then show ?thesis .. qed lemma (in gcd_condition_monoid) gcd_closed [simp]: - assumes carr: "a \ carrier G" "b \ carrier G" + assumes "a \ carrier G" "b \ carrier G" shows "somegcd G a b \ carrier G" proof - interpret weak_lower_semilattice "division_rel G" by simp show ?thesis - apply (simp add: somegcd_meet[OF carr]) - apply (rule meet_closed[simplified], fact+) - done + using assms meet_closed by (simp add: somegcd_meet) qed lemma (in gcd_condition_monoid) gcd_isgcd: - assumes carr: "a \ carrier G" "b \ carrier G" + assumes "a \ carrier G" "b \ carrier G" shows "(somegcd G a b) gcdof a b" proof - interpret weak_lower_semilattice "division_rel G" by simp - from carr have "somegcd G a b \ carrier G \ (somegcd G a b) gcdof a b" + from assms have "somegcd G a b \ carrier G \ (somegcd G a b) gcdof a b" by (simp add: gcdof_greatestLower inf_of_two_greatest meet_def somegcd_meet) then show "(somegcd G a b) gcdof a b" by simp qed lemma (in gcd_condition_monoid) gcd_exists: - assumes carr: "a \ carrier G" "b \ carrier G" + assumes "a \ carrier G" "b \ carrier G" shows "\x\carrier G. x = somegcd G a b" proof - interpret weak_lower_semilattice "division_rel G" by simp show ?thesis - by (metis carr(1) carr(2) gcd_closed) + by (metis assms gcd_closed) qed lemma (in gcd_condition_monoid) gcd_divides_l: - assumes carr: "a \ carrier G" "b \ carrier G" + assumes "a \ carrier G" "b \ carrier G" shows "(somegcd G a b) divides a" proof - interpret weak_lower_semilattice "division_rel G" by simp show ?thesis - by (metis carr(1) carr(2) gcd_isgcd isgcd_def) + by (metis assms gcd_isgcd isgcd_def) qed lemma (in gcd_condition_monoid) gcd_divides_r: - assumes carr: "a \ carrier G" "b \ carrier G" + assumes "a \ carrier G" "b \ carrier G" shows "(somegcd G a b) divides b" proof - interpret weak_lower_semilattice "division_rel G" by simp show ?thesis - by (metis carr gcd_isgcd isgcd_def) + by (metis assms gcd_isgcd isgcd_def) qed lemma (in gcd_condition_monoid) gcd_divides: - assumes sub: "z divides x" "z divides y" + assumes "z divides x" "z divides y" and L: "x \ carrier G" "y \ carrier G" "z \ carrier G" shows "z divides (somegcd G x y)" proof - @@ -2325,49 +2301,25 @@ qed lemma (in gcd_condition_monoid) gcd_cong_l: - assumes xx': "x \ x'" - and carr: "x \ carrier G" "x' \ carrier G" "y \ carrier G" + assumes "x \ x'" "x \ carrier G" "x' \ carrier G" "y \ carrier G" shows "somegcd G x y \ somegcd G x' y" proof - interpret weak_lower_semilattice "division_rel G" by simp show ?thesis - apply (simp add: somegcd_meet carr) - apply (rule meet_cong_l[simplified], fact+) - done + using somegcd_meet assms + by (metis eq_object.select_convs(1) meet_cong_l partial_object.select_convs(1)) qed lemma (in gcd_condition_monoid) gcd_cong_r: - assumes carr: "x \ carrier G" "y \ carrier G" "y' \ carrier G" - and yy': "y \ y'" + assumes "y \ y'" "x \ carrier G" "y \ carrier G" "y' \ carrier G" shows "somegcd G x y \ somegcd G x y'" proof - interpret weak_lower_semilattice "division_rel G" by simp show ?thesis - apply (simp add: somegcd_meet carr) - apply (rule meet_cong_r[simplified], fact+) - done + by (meson associated_def assms gcd_closed gcd_divides gcd_divides_l gcd_divides_r monoid.divides_trans monoid_axioms) qed -(* -lemma (in gcd_condition_monoid) asc_cong_gcd_l [intro]: - assumes carr: "b \ carrier G" - shows "asc_cong (\a. somegcd G a b)" -using carr -unfolding CONG_def -by clarsimp (blast intro: gcd_cong_l) - -lemma (in gcd_condition_monoid) asc_cong_gcd_r [intro]: - assumes carr: "a \ carrier G" - shows "asc_cong (\b. somegcd G a b)" -using carr -unfolding CONG_def -by clarsimp (blast intro: gcd_cong_r) - -lemmas (in gcd_condition_monoid) asc_cong_gcd_split [simp] = - assoc_split[OF _ asc_cong_gcd_l] assoc_split[OF _ asc_cong_gcd_r] -*) - lemma (in gcd_condition_monoid) gcdI: assumes dvd: "a divides b" "a divides c" and others: "\y. \y\carrier G; y divides b; y divides c\ \ y divides a" @@ -2390,25 +2342,23 @@ lemma (in gcd_condition_monoid) SomeGcd_ex: assumes "finite A" "A \ carrier G" "A \ {}" - shows "\x\ carrier G. x = SomeGcd G A" + shows "\x \ carrier G. x = SomeGcd G A" proof - interpret weak_lower_semilattice "division_rel G" by simp show ?thesis - apply (simp add: SomeGcd_def) - apply (rule finite_inf_closed[simplified], fact+) - done + using finite_inf_closed by (simp add: assms SomeGcd_def) qed lemma (in gcd_condition_monoid) gcd_assoc: - assumes carr: "a \ carrier G" "b \ carrier G" "c \ carrier G" + assumes "a \ carrier G" "b \ carrier G" "c \ carrier G" shows "somegcd G (somegcd G a b) c \ somegcd G a (somegcd G b c)" proof - interpret weak_lower_semilattice "division_rel G" by simp show ?thesis unfolding associated_def - by (meson carr divides_trans gcd_divides gcd_divides_l gcd_divides_r gcd_exists) + by (meson assms divides_trans gcd_divides gcd_divides_l gcd_divides_r gcd_exists) qed lemma (in gcd_condition_monoid) gcd_mult: @@ -2641,141 +2591,124 @@ using Cons.IH Cons.prems(1) by force qed - -lemma (in primeness_condition_monoid) wfactors_unique__hlp_induct: - "\a as'. a \ carrier G \ set as \ carrier G \ set as' \ carrier G \ - wfactors G as a \ wfactors G as' a \ essentially_equal G as as'" -proof (induct as) +proposition (in primeness_condition_monoid) wfactors_unique: + assumes "wfactors G as a" "wfactors G as' a" + and "a \ carrier G" "set as \ carrier G" "set as' \ carrier G" + shows "essentially_equal G as as'" + using assms +proof (induct as arbitrary: a as') case Nil - show ?case - apply (clarsimp simp: wfactors_def) - by (metis Units_one_closed assoc_unit_r list_update_nonempty unit_wfactors_empty unitfactor_ee wfactorsI) + then have "a \ \" + by (meson Units_one_closed one_closed perm.Nil perm_wfactorsD unit_wfactors) + then have "as' = []" + using Nil.prems assoc_unit_l unit_wfactors_empty by blast + then show ?case + by auto next case (Cons ah as) - then show ?case - proof clarsimp - fix a as' - assume ih [rule_format]: - "\a as'. a \ carrier G \ set as' \ carrier G \ wfactors G as a \ - wfactors G as' a \ essentially_equal G as as'" - and acarr: "a \ carrier G" and ahcarr: "ah \ carrier G" - and ascarr: "set as \ carrier G" and as'carr: "set as' \ carrier G" - and afs: "wfactors G (ah # as) a" - and afs': "wfactors G as' a" - then have ahdvda: "ah divides a" - by (intro wfactors_dividesI[of "ah#as" "a"]) simp_all + then have ahdvda: "ah divides a" + using wfactors_dividesI by auto then obtain a' where a'carr: "a' \ carrier G" and a: "a = ah \ a'" by blast + have carr_ah: "ah \ carrier G" "set as \ carrier G" + using Cons.prems by fastforce+ + have "ah \ foldr (\) as \ \ a" + by (rule wfactorsE[OF \wfactors G (ah # as) a\]) auto + then have "foldr (\) as \ \ a'" + by (metis Cons.prems(4) a a'carr assoc_l_cancel insert_subset list.set(2) monoid.multlist_closed monoid_axioms) + then have a'fs: "wfactors G as a'" - apply (rule wfactorsE[OF afs], rule wfactorsI, simp) - by (metis a a'carr ahcarr ascarr assoc_l_cancel factorsI factors_def factors_mult_single list.set_intros(1) list.set_intros(2) multlist_closed) - from afs have ahirr: "irreducible G ah" - by (elim wfactorsE) simp - with ascarr have ahprime: "prime G ah" - by (intro irreducible_prime ahcarr) - - note carr [simp] = acarr ahcarr ascarr as'carr a'carr - + by (meson Cons.prems(1) set_subset_Cons subset_iff wfactorsE wfactorsI) + then have ahirr: "irreducible G ah" + by (meson Cons.prems(1) list.set_intros(1) wfactorsE) + with Cons have ahprime: "prime G ah" + by (simp add: irreducible_prime) note ahdvda - also from afs' have "a divides (foldr (\) as' \)" - by (elim wfactorsE associatedE, simp) + also have "a divides (foldr (\) as' \)" + by (meson Cons.prems(2) associatedE wfactorsE) finally have "ah divides (foldr (\) as' \)" - by simp + using Cons.prems(4) by auto with ahprime have "\i carrier G" - unfolding set_conv_nth by force - note carr = carr asicarr - - from ahdvd obtain x where "x \ carrier G" and asi: "as'!i = ah \ x" + then obtain x where "x \ carrier G" and asi: "as'!i = ah \ x" by blast - with carr irrasi[simplified asi] have asiah: "as'!i \ ah" - by (metis ahprime associatedI2 irreducible_prodE primeE) + have irrasi: "irreducible G (as'!i)" + using nth_mem[OF len] wfactorsE + by (metis Cons.prems(2)) + have asicarr[simp]: "as'!i \ carrier G" + using len \set as' \ carrier G\ nth_mem by blast + have asiah: "as'!i \ ah" + by (metis \ah \ carrier G\ \x \ carrier G\ asi irrasi ahprime associatedI2 irreducible_prodE primeE) note setparts = set_take_subset[of i as'] set_drop_subset[of "Suc i" as'] - note partscarr [simp] = setparts[THEN subset_trans[OF _ as'carr]] - note carr = carr partscarr - have "\aa_1. aa_1 \ carrier G \ wfactors G (take i as') aa_1" - by (meson afs' in_set_takeD partscarr(1) wfactorsE wfactors_prod_exists) - then obtain aa_1 where aa1carr: "aa_1 \ carrier G" and aa1fs: "wfactors G (take i as') aa_1" + using Cons + by (metis setparts(1) subset_trans in_set_takeD wfactorsE wfactors_prod_exists) + then obtain aa_1 where aa1carr [simp]: "aa_1 \ carrier G" and aa1fs: "wfactors G (take i as') aa_1" by auto - - have "\aa_2. aa_2 \ carrier G \ wfactors G (drop (Suc i) as') aa_2" - by (meson afs' in_set_dropD partscarr(2) wfactors_def wfactors_prod_exists) - then obtain aa_2 where aa2carr: "aa_2 \ carrier G" + obtain aa_2 where aa2carr [simp]: "aa_2 \ carrier G" and aa2fs: "wfactors G (drop (Suc i) as') aa_2" - by auto - - note carr = carr aa1carr[simp] aa2carr[simp] - - from aa1fs aa2fs - have v1: "wfactors G (take i as' @ drop (Suc i) as') (aa_1 \ aa_2)" - by (intro wfactors_mult, simp+) - then have v1': "wfactors G (as'!i # take i as' @ drop (Suc i) as') (as'!i \ (aa_1 \ aa_2))" - using irrasi wfactors_mult_single by auto - from aa2carr carr aa1fs aa2fs have "wfactors G (as'!i # drop (Suc i) as') (as'!i \ aa_2)" - by (metis irrasi wfactors_mult_single) - with len carr aa1carr aa2carr aa1fs + by (metis Cons.prems(2) Cons.prems(5) subset_code(1) in_set_dropD wfactors_def wfactors_prod_exists) + + have set_drop: "set (drop (Suc i) as') \ carrier G" + using Cons.prems(5) setparts(2) by blast + moreover have set_take: "set (take i as') \ carrier G" + using Cons.prems(5) setparts by auto + moreover have v1: "wfactors G (take i as' @ drop (Suc i) as') (aa_1 \ aa_2)" + using aa1fs aa2fs \set as' \ carrier G\ by (force simp add: dest: in_set_takeD in_set_dropD) + ultimately have v1': "wfactors G (as'!i # take i as' @ drop (Suc i) as') (as'!i \ (aa_1 \ aa_2))" + using irrasi wfactors_mult_single + by (simp add: irrasi v1 wfactors_mult_single) + have "wfactors G (as'!i # drop (Suc i) as') (as'!i \ aa_2)" + by (simp add: aa2fs irrasi set_drop wfactors_mult_single) + with len aa1carr aa2carr aa1fs have v2: "wfactors G (take i as' @ as'!i # drop (Suc i) as') (aa_1 \ (as'!i \ aa_2))" - using wfactors_mult by auto + using wfactors_mult by (simp add: set_take set_drop) from len have as': "as' = (take i as' @ as'!i # drop (Suc i) as')" by (simp add: Cons_nth_drop_Suc) - with carr have eer: "essentially_equal G (take i as' @ as'!i # drop (Suc i) as') as'" - by simp - with v2 afs' carr aa1carr aa2carr nth_mem[OF len] have "aa_1 \ (as'!i \ aa_2) \ a" - by (metis as' ee_wfactorsD m_closed) + have eer: "essentially_equal G (take i as' @ as'!i # drop (Suc i) as') as'" + using Cons.prems(5) as' by auto + with v2 aa1carr aa2carr nth_mem[OF len] have "aa_1 \ (as'!i \ aa_2) \ a" + using Cons.prems as' comm_monoid_cancel.ee_wfactorsD is_comm_monoid_cancel by fastforce then have t1: "as'!i \ (aa_1 \ aa_2) \ a" by (metis aa1carr aa2carr asicarr m_lcomm) - from carr asiah have "ah \ (aa_1 \ aa_2) \ as'!i \ (aa_1 \ aa_2)" - by (metis associated_sym m_closed mult_cong_l) + from asiah have "ah \ (aa_1 \ aa_2) \ as'!i \ (aa_1 \ aa_2)" + by (simp add: \ah \ carrier G\ associated_sym mult_cong_l) also note t1 - finally have "ah \ (aa_1 \ aa_2) \ a" by simp - - with carr aa1carr aa2carr a'carr nth_mem[OF len] have a': "aa_1 \ aa_2 \ a'" - by (simp add: a, fast intro: assoc_l_cancel[of ah _ a']) - + finally have "ah \ (aa_1 \ aa_2) \ a" + using Cons.prems(3) carr_ah aa1carr aa2carr by blast + with aa1carr aa2carr a'carr nth_mem[OF len] have a': "aa_1 \ aa_2 \ a'" + using a assoc_l_cancel carr_ah(1) by blast note v1 also note a' finally have "wfactors G (take i as' @ drop (Suc i) as') a'" - by simp - - from a'fs this carr have "essentially_equal G as (take i as' @ drop (Suc i) as')" - by (intro ih[of a']) simp - then have ee1: "essentially_equal G (ah # as) (ah # take i as' @ drop (Suc i) as')" - by (elim essentially_equalE) (fastforce intro: essentially_equalI) - - from carr have ee2: "essentially_equal G (ah # take i as' @ drop (Suc i) as') + by (simp add: a'carr set_drop set_take) + from a'fs this have "essentially_equal G as (take i as' @ drop (Suc i) as')" + using Cons.hyps a'carr carr_ah(2) set_drop set_take by auto + with carr_ah have ee1: "essentially_equal G (ah # as) (ah # take i as' @ drop (Suc i) as')" + by (auto simp: essentially_equal_def) + have ee2: "essentially_equal G (ah # take i as' @ drop (Suc i) as') (as' ! i # take i as' @ drop (Suc i) as')" proof (intro essentially_equalI) show "ah # take i as' @ drop (Suc i) as' <~~> ah # take i as' @ drop (Suc i) as'" by simp next show "ah # take i as' @ drop (Suc i) as' [\] as' ! i # take i as' @ drop (Suc i) as'" - by (simp add: list_all2_append) (simp add: asiah[symmetric]) + by (simp add: asiah associated_sym set_drop set_take) qed note ee1 also note ee2 also have "essentially_equal G (as' ! i # take i as' @ drop (Suc i) as') (take i as' @ as' ! i # drop (Suc i) as')" - by (metis as' as'carr listassoc_refl essentially_equalI perm_append_Cons) + by (metis Cons.prems(5) as' essentially_equalI listassoc_refl perm_append_Cons) finally have "essentially_equal G (ah # as) (take i as' @ as' ! i # drop (Suc i) as')" - by simp - then show "essentially_equal G (ah # as) as'" - by (subst as') - qed + using Cons.prems(4) set_drop set_take by auto + then show ?case + using as' by auto qed -lemma (in primeness_condition_monoid) wfactors_unique: - assumes "wfactors G as a" "wfactors G as' a" - and "a \ carrier G" "set as \ carrier G" "set as' \ carrier G" - shows "essentially_equal G as as'" - by (rule wfactors_unique__hlp_induct[rule_format, of a]) (simp add: assms) - subsubsection \Application to factorial monoids\ @@ -2841,7 +2774,6 @@ by blast note [simp] = acarr bcarr ccarr ascarr cscarr - assume b: "b = a \ c" from afs cfs have "wfactors G (as@cs) (a \ c)" by (intro wfactors_mult) simp_all @@ -2918,9 +2850,7 @@ apply unfold_locales apply (rule wfUNIVI) apply (rule measure_induct[of "factorcount G"]) - apply simp - apply (metis properfactor_fcount) - done + using properfactor_fcount by auto sublocale factorial_monoid \ primeness_condition_monoid by standard (rule irreducible_prime)