Re: [isabelle] Mapping multisets



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.