[isabelle] Mapping multisets


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


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