*To*: "Jens-D. Doll" <jd at cococo.de>*Subject*: Re: [isabelle] Code-equations for multisets*From*: René Thiemann <rene.thiemann at uibk.ac.at>*Date*: Tue, 25 Feb 2014 20:59:11 +0100*Cc*: Isabelle Users List <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <op.xbumoeo7sgirxy@g2s>*References*: <op.xbumoeo7sgirxy@g2s>

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! Cheers, René

**Follow-Ups**:**[isabelle] Code-equations for multisets***From:*Jens-D. Doll

**References**:**[isabelle] Code-equations for multisets***From:*Jens-D. Doll

- Previous by Date: [isabelle] Code-equations for multisets
- Next by Date: [isabelle] Isabelle (JEDIT) seems slower than Isabelle(emacs)
- Previous by Thread: [isabelle] Code-equations for multisets
- Next by Thread: [isabelle] Code-equations for multisets
- Cl-isabelle-users February 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list