Bertram Felgenhauer via Cl-isabelle-users

2016-07-26 12:56:14 UTC

Permalink

(Once more with an attachment)Raw Message

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