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



Florian Haftmann wrote:
> 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.

> > lemma [code]:
> >   "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))))"
> >   by (simp add: multp_def)
> 
> for an efficient execution.

That's an easy change to make; in fact we can simply adjust the
definition of multp itself accordingly, without losing any proofs.

Does this affect the verdict on having both multp and multeqp?

Cheers,

Bertram





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