*To*: revantha at rsise.anu.edu.au*Subject*: Re: [isabelle] converting a multiset to a list*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Thu, 29 Nov 2007 21:53:17 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <474EBA38.1050709@rsise.anu.edu.au>*References*: <474D93BC.5060705@rsise.anu.edu.au> <474E90E3.4060200@in.tum.de> <474EBA38.1050709@rsise.anu.edu.au>*User-agent*: Thunderbird 2.0.0.0 (Macintosh/20070326)

http://www4.informatik.tu-muenchen.de/~nipkow/pubs/tphols05.html Similar combinators for multisets would be welcome.

Tobias Revantha Ramanayake schrieb:

Well, my need is the following:suppose I have a function "f :: form => nat ". I want to define afunction "g :: form multiset => nat" like this:g {# #} = 0 g ({# a #} + M) = f( {# a #}) + g(M).Basically I want to 'strip away' the multiset, element by element. Ofcourse I gather that the above definitionwould not work because a multiset is not defined in terms ofconstructors i.e. it doesn't have the nice structure.(this is why I wanted to first convert it to a list. for then I coulddefine the function g above, replacing {# #} with [] etc. )Using "inv multiset_of" I suppose things would look something like this: Define f :: form => nat g' :: form list => nat g :: form multiset => nat g' [] = 0 g' (x#ys) = f(x)+g'(ys) and g(M) = g'(inv multiset_of M)This seems to do the trick. Is this what you had in mind? and why do youadvise against it?cheers, revantha. Tobias Nipkow wrote:Unless you have very specific and good reasons for doing so, I wouldadvise against this and would recommend to go in the other direction.If you absolutely insist, you can always use "inv multiset_of". Goodluck.Tobias Revantha Ramanayake wrote:Hi, this question concerns multisets as defined in the theory fileMultisets in the standard distribution.It is easy to define the function multiset_of :: " 'a list => 'amultiset " which forms a multiset from a list in the obvious way.How do I define a function (of type " 'a multiset => 'a list ") thataccepts a multiset and returns a list (where eachoccurrence in the multiset is an occurrence in the list and viceversa) ? I realizethat there are many possible output lists. I am interested inobtaining one such list.Cheers, Revantha.

**Follow-Ups**:**Re: [isabelle] converting a multiset to a list***From:*Rafal Kolanski

**References**:**[isabelle] converting a multiset to a list***From:*Revantha Ramanayake

**Re: [isabelle] converting a multiset to a list***From:*Tobias Nipkow

**Re: [isabelle] converting a multiset to a list***From:*Revantha Ramanayake

- Previous by Date: Re: [isabelle] Isabelle 2007 destroys heaps
- Next by Date: Re: [isabelle] Notation issues trying to make Multiset more convenient
- Previous by Thread: Re: [isabelle] converting a multiset to a list
- Next by Thread: Re: [isabelle] converting a multiset to a list
- Cl-isabelle-users November 2007 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