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

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