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



Dear Bertram,

> 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.

This sounds reasonable to me.

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

> 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





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