# Re: [isabelle] Proposal: An update to Multiset theory

```(Once more with an attachment)

Dear Isabelle users and maintainers,

I have been working with the multiset extension from the HOL library
recently. In the course of doing so, I proved that the multiset
extension is cancellative w.r.t. the multiset union, to wit:

lemma mult_cancel:
assumes "trans s" "irrefl s"
shows "(X + Z, Y + Z) â mult s â (X, Y) â mult s" (is "?L â ?R")

I believe that this lemma is generally useful and would be a good
candidate for inclusion in the Isabelle HOL library. However, it
overlaps with the `decreasing_parts_disj` lemma from the recent addition
of an executable version of the multiset extension (f2177f5d2aed).
I propose to eliminate the latter lemma in favor of mult_cancel.

See the attached theory for details. To summarize, I propose to

- remove lemma decreasing_parts_disj,

mult_cancel: ... (X + Z, Y + Z) â mult s â (X, Y) â mult s
mult_cancel_max: ... (X, Y) â mult s â (X - X #â Y, Y - X #â Y) â mult s
multp_iff: ... multp P N M â (N, M) â mult R
(and corresponding definition of multp)

- reprove the existing lemma
multeqp_iff: multeqp P N M â (N, M) â (mult R)â=

mono_mult1: assumes "s â s'" shows "mult1 s â mult1 s'"
mono_mult: assumes "s â s'" shows "mult s â mult s'"

The reason for adding the multp version of multeqp is that multp_iff is
(to me) a natural intermediate result on the way towards the proof of
the existing lemma multeqp_iff.

The mult_cancel_max lemma is used in the proof of multp_iff.

What do you think? Also, are there any users of the
decreasing_parts_disj lemma?

Cheers,

Bertram
```
```theory Multiset_new
imports "~~/src/HOL/Library/Multiset"
begin

subsection \<open>The multiset extension is cancellative for multiset union\<close>

lemma mult_cancel:
assumes "trans s" "irrefl s"
shows "(X + Z, Y + Z) \<in> mult s \<longleftrightarrow> (X, Y) \<in> mult s" (is "?L \<longleftrightarrow> ?R")
proof
assume ?L thus ?R
proof (induct Z)
obtain X' Y' Z' where *: "X + Z + {#z#} = Z' + X'" "Y + Z + {#z#} = Z' + Y'" "Y' \<noteq> {#}"
"\<forall>x \<in> set_mset X'. \<exists>y \<in> set_mset Y'. (x, y) \<in> s"
using mult_implies_one_step[OF `trans s` add(2)] unfolding union_assoc by blast
consider Z2 where "Z' = Z2 + {#z#}" | X2 Y2 where "X' = X2 + {#z#}" "Y' = Y2 + {#z#}"
by (metis *(1,2) insert_DiffM2 add.right_neutral count_union multi_member_split neq0_conv
union_single_eq_member)
thus ?case
proof (cases)
case 1 thus ?thesis using * one_step_implies_mult[OF `trans s`, of Y' X' Z2]
by (auto simp: union_commute[of _ "{#_#}"] union_assoc intro: add(1))
next
case 2 then obtain y where "y \<in> set_mset Y2" "(z, y) \<in> s" using *(4) `irrefl s`
by (auto simp: irrefl_def)
moreover with transD[OF `trans s` _ this(2)]
have "x' \<in> set_mset X2 \<Longrightarrow> \<exists>y \<in> set_mset Y2. (x', y) \<in> s" for x'
using 2 *(4)[rule_format, of x'] by (auto simp: set_mset_def split: if_splits)
ultimately show ?thesis using  * one_step_implies_mult[OF `trans s`, of Y2 X2 Z'] 2
by (force simp: union_commute[of "{#_#}"] union_assoc[symmetric] intro: add(1))
qed
qed auto
next
assume ?R then obtain I J K
where "Y = I + J" "X = I + K" "J \<noteq> {#}" "\<forall>k \<in> set_mset K. \<exists>j \<in> set_mset J. (k, j) \<in> s"
using mult_implies_one_step[OF `trans s`] by blast
thus ?L using one_step_implies_mult[of s J K "I + Z"] `trans s` by (auto simp add: ac_simps)
qed

lemma mult_cancel_max:
assumes "trans s" "irrefl s"
shows "(X, Y) \<in> mult s \<longleftrightarrow> (X - X #\<inter> Y, Y - X #\<inter> Y) \<in> mult s" (is "?L \<longleftrightarrow> ?R")
proof -
have "X - X #\<inter> Y + X #\<inter> Y = X" "Y - X #\<inter> Y + X #\<inter> Y = Y" by (auto simp: count_inject[symmetric])
thus ?thesis using mult_cancel[OF assms, of "X - X #\<inter> Y"  "X #\<inter> Y" "Y - X #\<inter> Y"] by auto
qed

subsection \<open>Quasi-executable version of the multiset extension\<close>

text \<open>
Predicate variants of \<open>mult\<close> and the reflexive closure of \<open>mult\<close>, which are
executable whenever the given predicate \<open>P\<close> is. Together with the
standard code equations for \<open>op #\<inter>\<close> and \<open>op -\<close> this should yield
a quadratic (with respect to calls to \<open>P\<close>) implementation of \<open>multeqp\<close>.
\<close>

definition multp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
"multp P N M =
(let Z = M #\<inter> N; X = M - Z; Y = N - Z in
X \<noteq> {#} \<and> (\<forall>y \<in> set_mset Y. \<exists>x \<in> set_mset X. P y x))"

definition multeqp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
"multeqp P N M =
(let Z = M #\<inter> N; X = M - Z; Y = N - Z in
(\<forall>y \<in> set_mset Y. \<exists>x \<in> set_mset X. P y x))"

lemma multp_iff:
assumes "irrefl R" and "trans R" and [simp]: "\<And>x y. P x y \<longleftrightarrow> (x, y) \<in> R"
shows "multp P N M \<longleftrightarrow> (N, M) \<in> mult R" (is "?L \<longleftrightarrow> ?R")
proof -
have *: "M #\<inter> N + (N - M #\<inter> N) = N" "M #\<inter> N + (M - M #\<inter> N) = M"
"(M - M #\<inter> N) #\<inter> (N - M #\<inter> N) = {#}" by (auto simp: count_inject[symmetric])
show ?thesis
proof
assume ?L thus ?R
using one_step_implies_mult[OF assms(2), of "M - M #\<inter> N" "N - M #\<inter> N" "M #\<inter> N"] *
by (auto simp: multp_def Let_def)
next
{ fix I J K :: "'a multiset" assume "(I + J) #\<inter> (I + K) = {#}"
then have "\<not> x \<in># I" for x by (auto simp: count_inject[symmetric] dest!: fun_cong[of _ _ x])
then have "I = {#}" by (auto simp: count_inject[symmetric])
} note [dest!] = this
assume ?R thus ?L
using mult_implies_one_step[OF assms(2), of "N - M #\<inter> N" "M - M #\<inter> N"]
mult_cancel_max[OF assms(2,1), of "N" "M"] * by (auto simp: multp_def ac_simps)
qed
qed

lemma multeqp_iff:
assumes "irrefl R" and "trans R" and "\<And>x y. P x y \<longleftrightarrow> (x, y) \<in> R"
shows "multeqp P N M \<longleftrightarrow> (N, M) \<in> (mult R)\<^sup>="
proof -
{ assume "N \<noteq> M" "M - M #\<inter> N = {#}"
then obtain y where "count N y \<noteq> count M y" by (auto simp: count_inject[symmetric])
then have "\<exists>y. count M y < count N y" using `M - M #\<inter> N = {#}`
by (auto simp: count_inject[symmetric] dest!: le_neq_implies_less fun_cong[of _ _ y])
}
then have "multeqp P N M \<longleftrightarrow> multp P N M \<or> N = M"
by (auto simp: multeqp_def multp_def Let_def) (simp add: min.strict_order_iff)
thus ?thesis using multp_iff[OF assms] by simp
qed

subsection \<open>Monotonicity of the multiset extension\<close>

lemma mono_mult1:
assumes "s \<subseteq> s'" shows "mult1 s \<subseteq> mult1 s'"
unfolding mult1_def using assms by blast

lemma mono_mult:
assumes "s \<subseteq> s'" shows "mult s \<subseteq> mult s'"
unfolding mult_def using mono_mult1[OF assms] trancl_mono by blast

end```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.