[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?



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