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



Hi all,

I have no objection towards Bertram's proposed extension.

There is, however, one point which I don't understand:

> But "multeqp" can be implemented more efficiently than "multp" (and these predicates appear to be designed for code generation).

Comparing the two definitions

> definition multeqp :: "('a â 'a â bool) â 'a multiset â 'a multiset â bool" where
>   "multeqp P N M =
>     (let Z = M #â N; X = M - Z; Y = N - Z in
>     (ây â set_mset Y. âx â set_mset X. P y x))"
> 
> definition multp :: "('a â 'a â bool) â 'a multiset â 'a multiset â bool" where
>   "multp P N M =
>     (let Z = M #â N; X = M - Z; Y = N - Z in
>     X â {#} â (ây â set_mset Y. âx â set_mset X. P y x))"

it is difficult to see why this should actually be the case.  The only
difference is the emptiness check for the local X, which should be
efficient to execute.  Maybe the emptiness check has to be carried out
more earlier

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

Cheers,
	Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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