Re: [isabelle] Code-equations for multisets

Hi Jens,

> could you explain the results for code comparison from conventional theory a little?

The problem is easily explained. At the end of Multiset.thy, multisets are implemented via (not necessarily sorted) lists.
I.e., now all multiset-operations must be implemented on lists, where multiset_of is seen as a constructor.

E.g., it would be possible to implement membership via the lemma

lemma [code]: "(x :# multiset_of xs) = (x : set xs)"

Pattern matching on multiset_of is however not required. It is perfectly fine to implement multiset-equality via 
the multiset subset-relation in general, i.e., without any specialization on the implementation type:

lemma[code]: "(A = (B :: 'a multiset)) = (A <= B & B <= A)"

However, the problem in Multiset.thy is, that the subset-relation is again implemented via equality:

lemma[code]: "(A <= B) = (inf_multiset A B = A)

Then, when trying to evaluate "A = B" we immediately invoke "A <= B" which in turn
invokes "inf_multiset A B = A" which invokes "<=", etc.

So, at least "=" or "<=" must be implemented directly, which is what I did in the previously attached theory.

Of course, one can think of smarter representations for multisets, like sorted lists,
or maps "'a => nat" which store the multiplicity of each element, but this is a bit more effort
than just fixing the current implementation of multisets by lists which is provided in Multiset.thy.

> Aren't there some undecidable areas? And which results do we have on normal forms and reducability?

Can you be more precise? The above problems at least have nothing to do with undecidability!


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