# [isabelle] Proposal: An update to Multiset theory

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,
- add lemmas:
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)â=
- optionally add trivial lemmas:
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

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