# 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
• 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):
```
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.