*To*: Tobias Nipkow <nipkow at in.tum.de>*Subject*: Re: [isabelle] converting a multiset to a list*From*: Rafal Kolanski <rafalk at cse.unsw.edu.au>*Date*: Fri, 30 Nov 2007 12:32:07 +1100*Cc*: revantha at rsise.anu.edu.au, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <474F26BD.7000805@in.tum.de>*References*: <474D93BC.5060705@rsise.anu.edu.au> <474E90E3.4060200@in.tum.de> <474EBA38.1050709@rsise.anu.edu.au> <474F26BD.7000805@in.tum.de>*User-agent*: Thunderbird 2.0.0.9 (Windows/20071031)

Rafal Kolanski. Tobias Nipkow wrote:

Indeed, you cannot define functions by recursion over finite multisets.Same as for sets. For a general solution of recursion over sets seehttp://www4.informatik.tu-muenchen.de/~nipkow/pubs/tphols05.html Similar combinators for multisets would be welcome.Concerning using "inv": you can do it, but it will be a bit tedious,although probably not too bad. But a general recursion combinator wouldbe nicer.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 doyou advise 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.

**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

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

- Previous by Date: Re: [isabelle] Notation issues trying to make Multiset more convenient
- Next by Date: [isabelle] IJCAR Call for Papers, and Workshop and Tutorial Proposals
- Previous by Thread: Re: [isabelle] converting a multiset to a list
- Next by Thread: [isabelle] Help with Cauchy Schwarz
- 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