# Re: [isabelle] converting a multiset to a list

Indeed, you cannot define functions by recursion over finite multisets. Same as for sets. For a general solution of recursion over sets see
```http://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 would be nicer.
```
Tobias

Revantha Ramanayake schrieb:
```
```Well, my need is the following:

```
suppose I have a function "f :: form => nat ". I want to define a function "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. Of course I gather that the above definition would not work because a multiset is not defined in terms of constructors i.e. it doesn't have the nice structure.
```
```
(this is why I wanted to first convert it to a list. for then I could define 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 you advise against it?
```
cheers,

revantha.

Tobias Nipkow wrote:

```
Unless you have very specific and good reasons for doing so, I would advise against this and would recommend to go in the other direction. If you absolutely insist, you can always use "inv multiset_of". Good luck.
```
Tobias

Revantha Ramanayake wrote:

```
Hi, this question concerns multisets as defined in the theory file Multisets in the standard distribution.
```
```
It is easy to define the function multiset_of :: " 'a list => 'a multiset " which forms a multiset from a list in the obvious way.
```
```
How do I define a function (of type " 'a multiset => 'a list ") that accepts a multiset and returns a list (where each occurrence in the multiset is an occurrence in the list and vice versa) ? I realize that there are many possible output lists. I am interested in obtaining one such list.
```
Cheers,

Revantha.
```
```
```
```

```

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