--- a/src/HOL/Library/Multiset_Order.thy Mon Jul 01 12:59:18 2024 +0200
+++ b/src/HOL/Library/Multiset_Order.thy Mon Jul 01 12:59:46 2024 +0200
@@ -59,51 +59,49 @@
by (metis asympD add_cancel_right_right add_diff_cancel_left' add_mset_add_single count_inI
count_union diff_diff_add_mset diff_single_trivial in_diff_count multi_member_last)
moreover
- { assume "count P a \<le> count M a"
- with \<open>a \<notin># K\<close> have "count N a < count M a" unfolding *(1,2)
- by (auto simp add: not_in_iff)
- with ** obtain z where z: "r a z" "count M z < count N z"
- by blast
- with * have "count N z \<le> count P z"
- using \<open>asymp r\<close>
- by (metis add_diff_cancel_left' add_mset_add_single asympD diff_diff_add_mset
- diff_single_trivial in_diff_count not_le_imp_less)
- with z have "\<exists>z. r a z \<and> count M z < count P z" by auto
- } note count_a = this
- { fix y
- assume count_y: "count P y < count M y"
- have "\<exists>x. r y x \<and> count M x < count P x"
- proof (cases "y = a")
+ have count_a: "\<exists>z. r a z \<and> count M z < count P z" if "count P a \<le> count M a"
+ proof -
+ from \<open>a \<notin># K\<close> and that have "count N a < count M a"
+ unfolding *(1,2) by (auto simp add: not_in_iff)
+ with ** obtain z where z: "r a z" "count M z < count N z"
+ by blast
+ with * have "count N z \<le> count P z"
+ using \<open>asymp r\<close>
+ by (metis add_diff_cancel_left' add_mset_add_single asympD diff_diff_add_mset
+ diff_single_trivial in_diff_count not_le_imp_less)
+ with z show ?thesis by auto
+ qed
+ have "\<exists>x. r y x \<and> count M x < count P x" if count_y: "count P y < count M y" for y
+ proof (cases "y = a")
+ case True
+ with count_y count_a show ?thesis by auto
+ next
+ case False
+ show ?thesis
+ proof (cases "y \<in># K")
case True
- with count_y count_a show ?thesis by auto
+ with *(4) have "r y a" by simp
+ then show ?thesis
+ by (cases "count P a \<le> count M a") (auto dest: count_a intro: \<open>transp r\<close>[THEN transpD])
next
case False
+ with \<open>y \<noteq> a\<close> have "count P y = count N y" unfolding *(1,2)
+ by (simp add: not_in_iff)
+ with count_y ** obtain z where z: "r y z" "count M z < count N z" by auto
show ?thesis
- proof (cases "y \<in># K")
+ proof (cases "z \<in># K")
case True
- with *(4) have "r y a" by simp
- then show ?thesis
- by (cases "count P a \<le> count M a") (auto dest: count_a intro: \<open>transp r\<close>[THEN transpD])
+ with *(4) have "r z a" by simp
+ with z(1) show ?thesis
+ by (cases "count P a \<le> count M a") (auto dest!: count_a intro: \<open>transp r\<close>[THEN transpD])
next
case False
- with \<open>y \<noteq> a\<close> have "count P y = count N y" unfolding *(1,2)
- by (simp add: not_in_iff)
- with count_y ** obtain z where z: "r y z" "count M z < count N z" by auto
- show ?thesis
- proof (cases "z \<in># K")
- case True
- with *(4) have "r z a" by simp
- with z(1) show ?thesis
- by (cases "count P a \<le> count M a") (auto dest!: count_a intro: \<open>transp r\<close>[THEN transpD])
- next
- case False
- with \<open>a \<notin># K\<close> have "count N z \<le> count P z" unfolding *
- by (auto simp add: not_in_iff)
- with z show ?thesis by auto
- qed
+ with \<open>a \<notin># K\<close> have "count N z \<le> count P z" unfolding *
+ by (auto simp add: not_in_iff)
+ with z show ?thesis by auto
qed
qed
- }
+ qed
ultimately show ?case unfolding multp\<^sub>H\<^sub>O_def by blast
qed
@@ -312,8 +310,7 @@
paragraph \<open>Transitivity\<close>
lemma transp_on_multp\<^sub>H\<^sub>O:
- assumes "asymp_on A R" and "transp_on A R" and
- B_sub_A: "\<And>M. M \<in> B \<Longrightarrow> set_mset M \<subseteq> A"
+ assumes "asymp_on A R" and "transp_on A R" and B_sub_A: "\<And>M. M \<in> B \<Longrightarrow> set_mset M \<subseteq> A"
shows "transp_on B (multp\<^sub>H\<^sub>O R)"
proof (rule transp_onI)
from assms have "asymp_on B (multp\<^sub>H\<^sub>O R)"
@@ -570,8 +567,7 @@
lemma le_multiset_right_total: "M < add_mset x M"
unfolding less_eq_multiset_def less_multiset\<^sub>H\<^sub>O by simp
-lemma less_eq_multiset_empty_left[simp]:
- shows "{#} \<le> M"
+lemma less_eq_multiset_empty_left[simp]: "{#} \<le> M"
by (simp add: subset_eq_imp_le_multiset)
lemma ex_gt_imp_less_multiset: "(\<exists>y. y \<in># N \<and> (\<forall>x. x \<in># M \<longrightarrow> x < y)) \<Longrightarrow> M < N"
@@ -604,16 +600,14 @@
lemma
fixes M N :: "'a multiset"
- shows
- less_eq_multiset_plus_left: "N \<le> (M + N)" and
- less_eq_multiset_plus_right: "M \<le> (M + N)"
+ shows less_eq_multiset_plus_left: "N \<le> (M + N)"
+ and less_eq_multiset_plus_right: "M \<le> (M + N)"
by simp_all
lemma
fixes M N :: "'a multiset"
- shows
- le_multiset_plus_left_nonempty: "M \<noteq> {#} \<Longrightarrow> N < M + N" and
- le_multiset_plus_right_nonempty: "N \<noteq> {#} \<Longrightarrow> M < M + N"
+ shows le_multiset_plus_left_nonempty: "M \<noteq> {#} \<Longrightarrow> N < M + N"
+ and le_multiset_plus_right_nonempty: "N \<noteq> {#} \<Longrightarrow> M < M + N"
by simp_all
end
@@ -628,9 +622,8 @@
by (simp add: order.not_eq_order_implies_strict subset_eq_imp_le_multiset)
lemma image_mset_strict_mono:
- assumes
- mono_f: "\<forall>x \<in> set_mset M. \<forall>y \<in> set_mset N. x < y \<longrightarrow> f x < f y" and
- less: "M < N"
+ assumes mono_f: "\<forall>x \<in> set_mset M. \<forall>y \<in> set_mset N. x < y \<longrightarrow> f x < f y"
+ and less: "M < N"
shows "image_mset f M < image_mset f N"
proof -
obtain Y X where
@@ -672,9 +665,8 @@
qed
lemma image_mset_mono:
- assumes
- mono_f: "\<forall>x \<in> set_mset M. \<forall>y \<in> set_mset N. x < y \<longrightarrow> f x < f y" and
- less: "M \<le> N"
+ assumes mono_f: "\<forall>x \<in> set_mset M. \<forall>y \<in> set_mset N. x < y \<longrightarrow> f x < f y"
+ and less: "M \<le> N"
shows "image_mset f M \<le> image_mset f N"
by (metis eq_iff image_mset_strict_mono less less_imp_le mono_f order.not_eq_order_implies_strict)
@@ -802,9 +794,7 @@
instance multiset :: (linorder) linordered_cancel_ab_semigroup_add
by standard (metis less_eq_multiset\<^sub>H\<^sub>O not_less_iff_gr_or_eq)
-lemma less_eq_multiset_total:
- fixes M N :: "'a :: linorder multiset"
- shows "\<not> M \<le> N \<Longrightarrow> N \<le> M"
+lemma less_eq_multiset_total: "\<not> M \<le> N \<Longrightarrow> N \<le> M" for M N :: "'a :: linorder multiset"
by simp
instantiation multiset :: (wellorder) wellorder
@@ -905,18 +895,17 @@
have "M \<noteq> N"
using max by auto
moreover
- {
- fix y
- assume "count N y < count M y"
- hence "y \<in># M"
+ have "\<exists>x > y. count M x < count N x" if "count N y < count M y" for y
+ proof -
+ from that have "y \<in># M"
by (simp add: count_inI)
- hence "?max_M \<ge> y"
+ then have "?max_M \<ge> y"
by simp
- hence "?max_N > y"
+ then have "?max_N > y"
using max by auto
- hence "\<exists>x > y. count M x < count N x"
+ then show ?thesis
using max_n_nin_m max_n_in_n count_inI by force
- }
+ qed
ultimately show ?thesis
unfolding less_multiset\<^sub>H\<^sub>O by blast
qed (auto simp: n_nemp)