--- a/src/HOL/Library/Multiset.thy Sat Nov 27 17:02:04 2021 +0100
+++ b/src/HOL/Library/Multiset.thy Sat Nov 27 22:20:27 2021 +0100
@@ -10,7 +10,7 @@
section \<open>(Finite) Multisets\<close>
theory Multiset
-imports Cancellation
+ imports Cancellation
begin
subsection \<open>The type of multisets\<close>
@@ -2789,8 +2789,6 @@
subsection \<open>The multiset order\<close>
-subsubsection \<open>Well-foundedness\<close>
-
definition mult1 :: "('a \<times> 'a) set \<Rightarrow> ('a multiset \<times> 'a multiset) set" where
"mult1 r = {(N, M). \<exists>a M0 K. M = add_mset a M0 \<and> N = M0 + K \<and>
(\<forall>b. b \<in># K \<longrightarrow> (b, a) \<in> r)}"
@@ -2798,6 +2796,9 @@
definition mult :: "('a \<times> 'a) set \<Rightarrow> ('a multiset \<times> 'a multiset) set" where
"mult r = (mult1 r)\<^sup>+"
+definition multp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
+ "multp r M N \<longleftrightarrow> (M, N) \<in> mult {(x, y). r x y}"
+
lemma mult1I:
assumes "M = add_mset a M0" and "N = M0 + K" and "\<And>b. b \<in># K \<Longrightarrow> (b, a) \<in> r"
shows "(N, M) \<in> mult1 r"
@@ -2810,14 +2811,29 @@
lemma mono_mult1:
assumes "r \<subseteq> r'" shows "mult1 r \<subseteq> mult1 r'"
-unfolding mult1_def using assms by blast
+ unfolding mult1_def using assms by blast
lemma mono_mult:
assumes "r \<subseteq> r'" shows "mult r \<subseteq> mult r'"
-unfolding mult_def using mono_mult1[OF assms] trancl_mono by blast
+ unfolding mult_def using mono_mult1[OF assms] trancl_mono by blast
+
+lemma mono_multp[mono]: "r \<le> r' \<Longrightarrow> multp r \<le> multp r'"
+ unfolding le_fun_def le_bool_def
+proof (intro allI impI)
+ fix M N :: "'a multiset"
+ assume "\<forall>x xa. r x xa \<longrightarrow> r' x xa"
+ hence "{(x, y). r x y} \<subseteq> {(x, y). r' x y}"
+ by blast
+ thus "multp r M N \<Longrightarrow> multp r' M N"
+ unfolding multp_def
+ by (fact mono_mult[THEN subsetD, rotated])
+qed
lemma not_less_empty [iff]: "(M, {#}) \<notin> mult1 r"
-by (simp add: mult1_def)
+ by (simp add: mult1_def)
+
+
+subsubsection \<open>Well-foundedness\<close>
lemma less_add:
assumes mult1: "(N, add_mset a M0) \<in> mult1 r"
@@ -2919,11 +2935,15 @@
qed
qed
-theorem wf_mult1: "wf r \<Longrightarrow> wf (mult1 r)"
-by (rule acc_wfI) (rule all_accessible)
-
-theorem wf_mult: "wf r \<Longrightarrow> wf (mult r)"
-unfolding mult_def by (rule wf_trancl) (rule wf_mult1)
+lemma wf_mult1: "wf r \<Longrightarrow> wf (mult1 r)"
+ by (rule acc_wfI) (rule all_accessible)
+
+lemma wf_mult: "wf r \<Longrightarrow> wf (mult r)"
+ unfolding mult_def by (rule wf_trancl) (rule wf_mult1)
+
+lemma wfP_multp: "wfP r \<Longrightarrow> wfP (multp r)"
+ unfolding multp_def wfP_def
+ by (simp add: wf_mult)
subsubsection \<open>Closure-free presentation\<close>
@@ -2966,6 +2986,9 @@
qed
qed
+lemmas multp_implies_one_step =
+ mult_implies_one_step[of "{(x, y). r x y}" for r, folded multp_def transp_trans, simplified]
+
lemma one_step_implies_mult:
assumes
"J \<noteq> {#}" and
@@ -2998,6 +3021,9 @@
qed
qed
+lemmas one_step_implies_multp =
+ one_step_implies_mult[of _ _ "{(x, y). r x y}" for r, folded multp_def, simplified]
+
lemma subset_implies_mult:
assumes sub: "A \<subset># B"
shows "(A, B) \<in> mult r"
@@ -3010,8 +3036,10 @@
by (rule one_step_implies_mult[of "B - A" "{#}" _ A, unfolded ApBmA, simplified])
qed
-
-subsection \<open>The multiset extension is cancellative for multiset union\<close>
+lemmas subset_implies_multp = subset_implies_mult[of _ _ "{(x, y). r x y}" for r, folded multp_def]
+
+
+subsubsection \<open>The multiset extension is cancellative for multiset union\<close>
lemma mult_cancel:
assumes "trans s" and "irrefl s"
@@ -3046,9 +3074,17 @@
thus ?L using one_step_implies_mult[of J K s "I + Z"] by (auto simp: ac_simps)
qed
+lemmas multp_cancel =
+ mult_cancel[of "{(x, y). r x y}" for r,
+ folded multp_def transp_trans irreflp_irrefl_eq, simplified]
+
lemmas mult_cancel_add_mset =
mult_cancel[of _ _ "{#_#}", unfolded union_mset_add_mset_right add.comm_neutral]
+lemmas multp_cancel_add_mset =
+ mult_cancel_add_mset[of "{(x, y). r x y}" for r,
+ folded multp_def transp_trans irreflp_irrefl_eq, simplified]
+
lemma mult_cancel_max0:
assumes "trans s" and "irrefl s"
shows "(X, Y) \<in> mult s \<longleftrightarrow> (X - X \<inter># Y, Y - X \<inter># Y) \<in> mult s" (is "?L \<longleftrightarrow> ?R")
@@ -3059,6 +3095,104 @@
lemmas mult_cancel_max = mult_cancel_max0[simplified]
+lemmas multp_cancel_max =
+ mult_cancel_max[of "{(x, y). r x y}" for r,
+ 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
+
+lemma trans_mult: "trans r \<Longrightarrow> trans (mult r)"
+ by (simp add: mult_def)
+
+lemma transp_multp: "transp r \<Longrightarrow> transp (multp r)"
+ unfolding multp_def transp_trans_eq
+ by (fact trans_mult[of "{(x, y). r x y}" for r, folded transp_trans])
+
+lemma irrefl_mult:
+ assumes "trans r" "irrefl r"
+ shows "irrefl (mult r)"
+proof (intro irreflI notI)
+ fix M
+ assume "(M, M) \<in> mult r"
+ 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> r)"
+ using mult_implies_one_step[OF \<open>trans r\<close>] by blast
+ then have *: "K \<noteq> {#}" and **: "\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset K. (k, j) \<in> r" by auto
+ have "finite (set_mset K)" by simp
+ hence "set_mset K = {}"
+ using **
+ proof (induction rule: finite_induct)
+ case empty
+ thus ?case by simp
+ next
+ case (insert x F)
+ have False
+ using \<open>irrefl r\<close>[unfolded irrefl_def, rule_format]
+ using \<open>trans r\<close>[THEN transD]
+ by (metis equals0D insert.IH insert.prems insertE insertI1 insertI2)
+ thus ?case ..
+ qed
+ with * show False by simp
+qed
+
+lemmas irreflp_multp =
+ irrefl_mult[of "{(x, y). r x y}" for r,
+ folded transp_trans_eq irreflp_irrefl_eq, simplified, folded multp_def]
+
+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 intro_classes
+ fix M N :: "'a multiset"
+ show "(M < N) = (M \<le> N \<and> \<not> N \<le> M)"
+ unfolding less_eq_multiset_def less_multiset_def
+ by (metis irreflp_def irreflp_less irreflp_multp transpE transp_less transp_multp)
+next
+ fix M :: "'a multiset"
+ show "M \<le> M"
+ unfolding less_eq_multiset_def
+ by simp
+next
+ fix M1 M2 M3 :: "'a multiset"
+ show "M1 \<le> M2 \<Longrightarrow> M2 \<le> M3 \<Longrightarrow> M1 \<le> M3"
+ unfolding less_eq_multiset_def less_multiset_def
+ using transp_multp[OF transp_less, THEN transpD]
+ by blast
+next
+ fix M N :: "'a multiset"
+ show "M \<le> N \<Longrightarrow> N \<le> M \<Longrightarrow> M = N"
+ unfolding less_eq_multiset_def less_multiset_def
+ using transp_multp[OF transp_less, THEN transpD]
+ using irreflp_multp[OF transp_less irreflp_less, unfolded irreflp_def, rule_format]
+ by blast
+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>
@@ -3100,6 +3234,11 @@
qed
qed
+lemma multp_code_eq_multp: "irreflp r \<Longrightarrow> transp r \<Longrightarrow> multp_code r = multp r"
+ using multp_code_iff_mult[of "{(x, y). r x y}" r for r,
+ folded irreflp_irrefl_eq transp_trans multp_def, simplified]
+ by blast
+
lemma multeqp_code_iff_reflcl_mult:
assumes "irrefl R" and "trans R" and "\<And>x y. P x y \<longleftrightarrow> (x, y) \<in> R"
shows "multeqp_code P N M \<longleftrightarrow> (N, M) \<in> (mult R)\<^sup>="
@@ -3114,62 +3253,10 @@
thus ?thesis using multp_code_iff_mult[OF assms] by simp
qed
-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
+lemma multeqp_code_eq_reflclp_multp: "irreflp r \<Longrightarrow> transp r \<Longrightarrow> multeqp_code r = (multp r)\<^sup>=\<^sup>="
+ using multeqp_code_iff_reflcl_mult[of "{(x, y). r x y}" r for r,
+ folded irreflp_irrefl_eq transp_trans, simplified, folded multp_def]
+ by blast
subsubsection \<open>Monotonicity of multiset union\<close>
@@ -3178,7 +3265,7 @@
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 17:02:04 2021 +0100
+++ b/src/HOL/Library/Multiset_Order.thy Sat Nov 27 22:20:27 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