# Re: [isabelle] Mapping multisets

*To*: Peter Chapman <pc at cs.st-and.ac.uk>
*Subject*: Re: [isabelle] Mapping multisets
*From*: Jeremy Dawson <jeremy at rsise.anu.edu.au>
*Date*: Tue, 07 Oct 2008 12:38:27 +1100
*Cc*: isabelle-users at cl.cam.ac.uk
*In-reply-to*: <3747AAA8-0920-419D-94EA-A4515D1211A3@cs.st-and.ac.uk>
*References*: <3747AAA8-0920-419D-94EA-A4515D1211A3@cs.st-and.ac.uk>
*User-agent*: Thunderbird 1.5.0.12 (X11/20070604)

Peter Chapman wrote:

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

Peter,
I've done exactly this in the last few months.

`The definition looks like this (it's based on the function ext - which
``also gives a monad structure):
`
(* multisets as monads *)
constdefs
mset_ext_count :: "('a => 'b multiset) => 'a multiset => 'b => nat"
"mset_ext_count f M b == setsum (%a. count M a * count (f a) b) (set_of M)"
mset_ext :: "('a => 'b multiset) => 'a multiset => 'b multiset"
"mset_ext f M == Abs_multiset (mset_ext_count f M)"

`
`` mset_map :: "('a => 'b) => 'a multiset => 'b multiset"
` "mset_map f == mset_ext (single o f)"

`
`` mset_join :: "'a multiset multiset => 'a multiset"
` "mset_join == mset_ext id"
See http://users.rsise.anu.edu.au/~jeremy/isabelle/2005/seqms/Multiset_no_le.thy
Then some relevant theorems are in
http://users.rsise.anu.edu.au/~jeremy/isabelle/2005/seqms/Multiset_no_le.ML
Jeremy

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