--- a/NEWS Sat Nov 27 10:28:48 2021 +0100
+++ b/NEWS Sat Nov 27 10:46:57 2021 +0100
@@ -26,6 +26,7 @@
- Added predicate multp equivalent to set mult. Reuse name previously
used for what is now called multp_code. Minor INCOMPATIBILITY.
- Lifted multiple lemmas from mult to multp.
+ - Redefined less_multiset to be based on multp. INCOMPATIBILITY.
New in Isabelle2021-1 (December 2021)
--- a/src/HOL/Library/Multiset.thy Sat Nov 27 10:28:48 2021 +0100
+++ b/src/HOL/Library/Multiset.thy Sat Nov 27 10:46:57 2021 +0100
@@ -3100,6 +3100,63 @@
folded multp_def transp_trans irreflp_irrefl_eq, simplified]
+subsubsection \<open>Partial-order properties\<close>
+
+lemma mult1_lessE:
+ assumes "(N, M) \<in> mult1 {(a, b). r a b}" and "asymp r"
+ obtains a M0 K where "M = add_mset a M0" "N = M0 + K"
+ "a \<notin># K" "\<And>b. b \<in># K \<Longrightarrow> r b a"
+proof -
+ from assms obtain a M0 K where "M = add_mset a M0" "N = M0 + K" and
+ *: "b \<in># K \<Longrightarrow> r b a" for b by (blast elim: mult1E)
+ moreover from * [of a] have "a \<notin># K"
+ using \<open>asymp r\<close> by (meson asymp.cases)
+ ultimately show thesis by (auto intro: that)
+qed
+
+instantiation multiset :: (preorder) order begin
+
+definition less_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"
+ where "M < N \<longleftrightarrow> multp (<) M N"
+
+definition less_eq_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"
+ where "less_eq_multiset M N \<longleftrightarrow> M < N \<or> M = N"
+
+instance
+proof -
+ have irrefl: "\<not> M < M" for M :: "'a multiset"
+ proof
+ assume "M < M"
+ then have MM: "(M, M) \<in> mult {(x, y). x < y}" by (simp add: less_multiset_def multp_def)
+ have "trans {(x'::'a, x). x' < x}"
+ by (metis (mono_tags, lifting) case_prodD case_prodI less_trans mem_Collect_eq transI)
+ moreover note MM
+ ultimately have "\<exists>I J K. M = I + J \<and> M = I + K
+ \<and> J \<noteq> {#} \<and> (\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset J. (k, j) \<in> {(x, y). x < y})"
+ by (rule mult_implies_one_step)
+ then obtain I J K where "M = I + J" and "M = I + K"
+ and "J \<noteq> {#}" and "(\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset J. (k, j) \<in> {(x, y). x < y})" by blast
+ then have *: "K \<noteq> {#}" and **: "\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset K. k < j" by auto
+ have "finite (set_mset K)" by simp
+ moreover note **
+ ultimately have "set_mset K = {}"
+ by (induct rule: finite_induct) (auto intro: order_less_trans)
+ with * show False by simp
+ qed
+ have trans: "K < M \<Longrightarrow> M < N \<Longrightarrow> K < N" for K M N :: "'a multiset"
+ unfolding less_multiset_def multp_def mult_def by (blast intro: trancl_trans)
+ show "OFCLASS('a multiset, order_class)"
+ by standard (auto simp add: less_eq_multiset_def irrefl dest: trans)
+qed
+
+end
+
+lemma mset_le_irrefl [elim!]:
+ fixes M :: "'a::preorder multiset"
+ shows "M < M \<Longrightarrow> R"
+ by simp
+
+
subsection \<open>Quasi-executable version of the multiset extension\<close>
text \<open>
@@ -3165,71 +3222,13 @@
by blast
-subsubsection \<open>Partial-order properties\<close>
-
-lemma mult1_lessE:
- assumes "(N, M) \<in> mult1 {(a, b). r a b}" and "asymp r"
- obtains a M0 K where "M = add_mset a M0" "N = M0 + K"
- "a \<notin># K" "\<And>b. b \<in># K \<Longrightarrow> r b a"
-proof -
- from assms obtain a M0 K where "M = add_mset a M0" "N = M0 + K" and
- *: "b \<in># K \<Longrightarrow> r b a" for b by (blast elim: mult1E)
- moreover from * [of a] have "a \<notin># K"
- using \<open>asymp r\<close> by (meson asymp.cases)
- ultimately show thesis by (auto intro: that)
-qed
-
-instantiation multiset :: (preorder) order
-begin
-
-definition less_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"
- where "M' < M \<longleftrightarrow> (M', M) \<in> mult {(x', x). x' < x}"
-
-definition less_eq_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"
- where "less_eq_multiset M' M \<longleftrightarrow> M' < M \<or> M' = M"
-
-instance
-proof -
- have irrefl: "\<not> M < M" for M :: "'a multiset"
- proof
- assume "M < M"
- then have MM: "(M, M) \<in> mult {(x, y). x < y}" by (simp add: less_multiset_def)
- have "trans {(x'::'a, x). x' < x}"
- by (metis (mono_tags, lifting) case_prodD case_prodI less_trans mem_Collect_eq transI)
- moreover note MM
- ultimately have "\<exists>I J K. M = I + J \<and> M = I + K
- \<and> J \<noteq> {#} \<and> (\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset J. (k, j) \<in> {(x, y). x < y})"
- by (rule mult_implies_one_step)
- then obtain I J K where "M = I + J" and "M = I + K"
- and "J \<noteq> {#}" and "(\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset J. (k, j) \<in> {(x, y). x < y})" by blast
- then have *: "K \<noteq> {#}" and **: "\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset K. k < j" by auto
- have "finite (set_mset K)" by simp
- moreover note **
- ultimately have "set_mset K = {}"
- by (induct rule: finite_induct) (auto intro: order_less_trans)
- with * show False by simp
- qed
- have trans: "K < M \<Longrightarrow> M < N \<Longrightarrow> K < N" for K M N :: "'a multiset"
- unfolding less_multiset_def mult_def by (blast intro: trancl_trans)
- show "OFCLASS('a multiset, order_class)"
- by standard (auto simp add: less_eq_multiset_def irrefl dest: trans)
-qed
-
-end
-
-lemma mset_le_irrefl [elim!]:
- fixes M :: "'a::preorder multiset"
- shows "M < M \<Longrightarrow> R"
- by simp
-
-
subsubsection \<open>Monotonicity of multiset union\<close>
lemma mult1_union: "(B, D) \<in> mult1 r \<Longrightarrow> (C + B, C + D) \<in> mult1 r"
by (force simp: mult1_def)
lemma union_le_mono2: "B < D \<Longrightarrow> C + B < C + (D::'a::preorder multiset)"
-apply (unfold less_multiset_def mult_def)
+apply (unfold less_multiset_def multp_def mult_def)
apply (erule trancl_induct)
apply (blast intro: mult1_union)
apply (blast intro: mult1_union trancl_trans)
--- a/src/HOL/Library/Multiset_Order.thy Sat Nov 27 10:28:48 2021 +0100
+++ b/src/HOL/Library/Multiset_Order.thy Sat Nov 27 10:46:57 2021 +0100
@@ -167,26 +167,26 @@
end
lemma less_multiset_less_multiset\<^sub>H\<^sub>O: "M < N \<longleftrightarrow> less_multiset\<^sub>H\<^sub>O M N"
- unfolding less_multiset_def mult\<^sub>H\<^sub>O less_multiset\<^sub>H\<^sub>O_def ..
+ unfolding less_multiset_def multp_def mult\<^sub>H\<^sub>O less_multiset\<^sub>H\<^sub>O_def ..
lemmas less_multiset\<^sub>D\<^sub>M = mult\<^sub>D\<^sub>M[folded less_multiset_def]
lemmas less_multiset\<^sub>H\<^sub>O = mult\<^sub>H\<^sub>O[folded less_multiset_def]
lemma subset_eq_imp_le_multiset:
shows "M \<subseteq># N \<Longrightarrow> M \<le> N"
- unfolding less_eq_multiset_def less_multiset\<^sub>H\<^sub>O
+ unfolding less_eq_multiset_def less_multiset_def multp_def less_multiset\<^sub>H\<^sub>O
by (simp add: less_le_not_le subseteq_mset_def)
(* FIXME: "le" should be "less" in this and other names *)
lemma le_multiset_right_total: "M < add_mset x M"
- unfolding less_eq_multiset_def less_multiset\<^sub>H\<^sub>O by simp
+ unfolding less_eq_multiset_def less_multiset_def multp_def less_multiset\<^sub>H\<^sub>O by simp
lemma less_eq_multiset_empty_left[simp]:
shows "{#} \<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"
- unfolding less_multiset\<^sub>H\<^sub>O
+ unfolding less_multiset_def multp_def less_multiset\<^sub>H\<^sub>O
by (metis count_eq_zero_iff count_greater_zero_iff less_le_not_le)
lemma less_eq_multiset_empty_right[simp]: "M \<noteq> {#} \<Longrightarrow> \<not> M \<le> {#}"
@@ -194,11 +194,11 @@
(* FIXME: "le" should be "less" in this and other names *)
lemma le_multiset_empty_left[simp]: "M \<noteq> {#} \<Longrightarrow> {#} < M"
- by (simp add: less_multiset\<^sub>H\<^sub>O)
+ by (simp add: less_multiset_def multp_def less_multiset\<^sub>H\<^sub>O)
(* FIXME: "le" should be "less" in this and other names *)
lemma le_multiset_empty_right[simp]: "\<not> M < {#}"
- using subset_mset.le_zero_eq less_multiset\<^sub>D\<^sub>M by blast
+ using subset_mset.le_zero_eq less_multiset_def multp_def less_multiset\<^sub>D\<^sub>M by blast
(* FIXME: "le" should be "less" in this and other names *)
lemma union_le_diff_plus: "P \<subseteq># M \<Longrightarrow> N < P \<Longrightarrow> M - P + N < M"
@@ -209,7 +209,7 @@
lemma less_eq_multiset\<^sub>H\<^sub>O:
"M \<le> N \<longleftrightarrow> (\<forall>y. count N y < count M y \<longrightarrow> (\<exists>x. y < x \<and> count M x < count N x))"
- by (auto simp: less_eq_multiset_def less_multiset\<^sub>H\<^sub>O)
+ by (auto simp: less_eq_multiset_def less_multiset_def multp_def less_multiset\<^sub>H\<^sub>O)
instance by standard (auto simp: less_eq_multiset\<^sub>H\<^sub>O)
@@ -247,7 +247,7 @@
obtain Y X where
y_nemp: "Y \<noteq> {#}" and y_sub_N: "Y \<subseteq># N" and M_eq: "M = N - Y + X" and
ex_y: "\<forall>x. x \<in># X \<longrightarrow> (\<exists>y. y \<in># Y \<and> x < y)"
- using less[unfolded less_multiset\<^sub>D\<^sub>M] by blast
+ using less[unfolded less_multiset_def multp_def less_multiset\<^sub>D\<^sub>M] by blast
have x_sub_M: "X \<subseteq># M"
using M_eq by simp
@@ -256,7 +256,7 @@
let ?fX = "image_mset f X"
show ?thesis
- unfolding less_multiset\<^sub>D\<^sub>M
+ unfolding less_multiset_def multp_def less_multiset\<^sub>D\<^sub>M
proof (intro exI conjI)
show "image_mset f M = image_mset f N - ?fY + ?fX"
using M_eq[THEN arg_cong, of "image_mset f"] y_sub_N
@@ -360,11 +360,11 @@
lemma ex_gt_count_imp_le_multiset:
"(\<forall>y :: 'a :: order. y \<in># M + N \<longrightarrow> y \<le> x) \<Longrightarrow> count M x < count N x \<Longrightarrow> M < N"
- unfolding less_multiset\<^sub>H\<^sub>O
+ unfolding less_multiset_def multp_def less_multiset\<^sub>H\<^sub>O
by (metis count_greater_zero_iff le_imp_less_or_eq less_imp_not_less not_gr_zero union_iff)
lemma mset_lt_single_iff[iff]: "{#x#} < {#y#} \<longleftrightarrow> x < y"
- unfolding less_multiset\<^sub>H\<^sub>O by simp
+ unfolding less_multiset_def multp_def less_multiset\<^sub>H\<^sub>O by simp
lemma mset_le_single_iff[iff]: "{#x#} \<le> {#y#} \<longleftrightarrow> x \<le> y" for x y :: "'a::order"
unfolding less_eq_multiset\<^sub>H\<^sub>O by force
@@ -381,9 +381,9 @@
begin
lemma wf_less_multiset: "wf {(M :: 'a multiset, N). M < N}"
- unfolding less_multiset_def by (auto intro: wf_mult wf)
+ unfolding less_multiset_def multp_def by (auto intro: wf_mult wf)
-instance by standard (metis less_multiset_def wf wf_def wf_mult)
+instance by standard (metis less_multiset_def multp_def wf wf_def wf_mult)
end