Re: [isabelle] Code-equations for multisets

René, thanks for your implementation, it is "in" now. I have defined your
auxiliary function List.extract (which may be of general interest for list
manipulators) via takeWhile and dropWhile, but the implementation is still via
your code equations.

Note that there is actually a faster implementation of multisets in
Library/DAList_Multiset.thy. Nevertheless it is nice that the default one
terminates more often now ;-)


On 25/02/2014 17:01, René Thiemann wrote:
> 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é

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