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



Dear Jasmin,
> > 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?

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




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