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



Hi Bertram,

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

a repo URL or a patch is indeed the best thing to proceed: there is not
Âthe development version but an ongoing agile development.

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

OK.

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

Both make sense: reflexive and strict order often occur as pairs in
theory Isabelle developments.

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.