Email Gateway (Aug 18 2022 at 12:28): Email Gateway (Aug 18 2022 at 12:28):From: Peter Chapman <pc@cs.st-and.ac.uk>
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
Email Gateway (Aug 18 2022 at 12:29):From: Tjark Weber <tjark.weber@gmx.de>
Peter,
theory Multiset in Isabelle 2008 already contains
"image_mset f == fold_mset (op + o single o f) {#}"
See http://isabelle.in.tum.de/dist/library/HOL/Library/Multiset.html for
further details.
Best,
Tjark
Email Gateway (Aug 18 2022 at 12:34):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
Peter Chapman wrote:
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
Last updated: May 03 2024 at 04:19 UTC