# [isabelle] Mapping multisets

Hi
How can I define a map for multisets, similar to the one for lists
map f [] = []
map f (x # xs) = (f x) # map f xs
and the equivalent for sets
map f A == {f x. x : A} ?

`I cannot use the first, primrec, way of doing things, because I get an
``error about multisets not being datatypes, and I cannot use the second
``because I cannot find a way to directly represent a multiset.
``Ideally, I would want to say
`
map f A == {# f x. x :#A #}

`but I don't think this is possible. There is an induction rule for
``multisets, which suggests there should be some way to define "map".
``Currently I am using two axioms, corresponding to the two inductive
``cases:
`
map f {#} == {#}
map f (A + {#x#}) == (map f A) + {# f x #}
but this is not ideal.
Many thanks
Peter

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