[isabelle] Code-equations for multisets



Dear all,

I recently played around with the available code-equations for multisets.
(I wanted to get rid of manual data refinement in our formalization)

Here, the current problem is that the code for comparing multisets is non-terminating:

E.g., equality is implemented via two calls to <=,
and <= is implemented via intersection and equality.
Hence, even 

value[code] "{#} = {#}" 

does not terminate.

To solve this problem, I wrote a tiny implementation for comparisons.
Everybody can use it, and it would be nice, if 
this algorithm or another proper implementation would find its
way into the distribution in src/HOL/Library/Multiset.thy.

Kind regards,
René

Attachment: Multiset_Code.thy
Description: Binary data



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