Discussion:
[isabelle] Proposal: An update to Multiset theory
Bertram Felgenhauer via Cl-isabelle-users
2016-07-26 12:56:14 UTC
(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
Bertram Felgenhauer via Cl-isabelle-users
2016-07-26 13:23:37 UTC
Post by Bertram Felgenhauer via Cl-isabelle-users
(Once more with an attachment)
And once more. This version works with the current development version
of Isabelle (3a0f40a6fa42). Sorry for the spam!

Cheers,

Bertram
Jasmin Blanchette
2016-08-01 08:23:53 UTC
Dear Bertram,
Post by Bertram Felgenhauer via Cl-isabelle-users
I have been working with the multiset extension from the HOL library
recently. In the course of doing so, I proved that the multiset
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.
This sounds reasonable to me.
Post by Bertram Felgenhauer via Cl-isabelle-users
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.
I was hoping Florian would comment this part, since it's related to the code setup. I'm not sure it's a gain to add yet another concept, esp. if the motivation is only a minor simplification of an existing proof. Or did I misunderstand your motivation?
Post by Bertram Felgenhauer via Cl-isabelle-users
What do you think? Also, are there any users of the
decreasing_parts_disj lemma?
Previous queries on the mailing list revealed that few formalizations use multisets much. The main consumers of Multisets would appear to be the Isabelle distribution, the AFP, IsaFoR, and IsaFoL [*]. A quick grep in these repositories reveals nothing. I would be in favor of that simplification.

Cheers,

Jasmin

[*] https://bitbucket.org/jasmin_blanchette/isafol/wiki/Home
Bertram Felgenhauer via Cl-isabelle-users
2016-08-01 12:58:45 UTC
Dear Jasmin,
Post by Jasmin Blanchette
Post by Bertram Felgenhauer via Cl-isabelle-users
I have been working with the multiset extension from the HOL library
recently. In the course of doing so, I proved that the multiset
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.
This sounds reasonable to me.
Post by Bertram Felgenhauer via Cl-isabelle-users
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.
I was hoping Florian would comment this part, since it's related to the
code setup. I'm not sure it's a gain to add yet another concept, esp.
if the motivation is only a minor simplification of an existing proof.
Or did I misunderstand your motivation?
I believe multp is the more fundamental of the two predicates; after
all, the rest of the theory is mostly concerned with the strict multiset
extension. But I was reluctant to drop the existing multeqp predicate in
favor of multp.

Maybe Christian Sternagel can comment on this?

Cheers,

Bertram
Jasmin Blanchette
2016-08-01 14:47:45 UTC
Dear Bertram,
Post by Bertram Felgenhauer via Cl-isabelle-users
I believe multp is the more fundamental of the two predicates; after
all, the rest of the theory is mostly concerned with the strict multiset
extension. But I was reluctant to drop the existing multeqp predicate in
favor of multp.
I see. I cannot find any use of "multeqp" in the repositories I mentioned in my previous email, except for some occurrences in IsaFoR. But "multeqp" can be implemented more efficiently than "multp" (and these predicates appear to be designed for code generation).

If nobody speaks up against or for one or the other predicate, I suggest you proceed with your intended change.

Cheers,

Jasmin
Christian Sternagel
2016-08-02 08:06:45 UTC
Post by Jasmin Blanchette
Dear Bertram,
Post by Bertram Felgenhauer via Cl-isabelle-users
I believe multp is the more fundamental of the two predicates; after
all, the rest of the theory is mostly concerned with the strict multiset
extension. But I was reluctant to drop the existing multeqp predicate in
favor of multp.
I see. I cannot find any use of "multeqp" in the repositories I mentioned in my previous email, except for some occurrences in IsaFoR. But "multeqp" can be implemented more efficiently than "multp" (and these predicates appear to be designed for code generation).
Right, code generation was my only reason to investigate this in the
first place (since we had situations where CeTA timed out while trying
to compare "tiny" -- around 10 elements -- multisets), so that's the
only reason why I went with multeqp instead of multp.

cheers

chris
Jasmin Blanchette
2016-08-04 08:12:39 UTC
Hi Florian,
Post by Jasmin Blanchette
But "multeqp" can be implemented more efficiently than "multp" (and these predicates appear to be designed for code generation).
Comparing the two definitions
...
it is difficult to see why this should actually be the case.
Indeed. You can forget my comment. I misparsed the emptiness check as the disequality check "M ~= N" in the Huet-Oppen formulation of the multiset extension (cf. less_multiset\<^sub>H\<^sub>O in Multiset_Order.thy).

Jasmin
Bertram Felgenhauer via Cl-isabelle-users
2016-08-05 15:02:20 UTC
I have no objection towards Bertram's proposed extension.
Nice!

How shall we proceed? As I hinted at earlier I do not have (nor want, at
this point) push access, but I can prepare a patch or clone of the repo,
if that helps, or just provide a plain theory file that works with the
development version of Isabelle.
"multp P N M ⟷ (let Z = M #∩ N; X = M - Z
in X ≠ {#} ∧ (let Y = N - Z in (∀y∈#Y. Multiset.Bex X (P y))))"