How can I extract data from all elements of a multiset?

Question

Let's say I have a datatype called dtyp. It looks like this

datatype dtype = T bool int

I'd like to define a function extr :: "dtype multiset => int multiset" which takes a multiset of these dtype elements and returns a multiset containing the ints in each of the dtype elements. So for example:

value "extr {#T True 4, T False 5, T False 7#}" should give {#4,5,7#}

I first thought of iterating through the multiset, but I know it isn't possible as these multisets are based off normal sets which are not iterable. I then thought about universal quantifiers, but I'm not sure how to use them in this situation. Could I please have some help?

Thanks in advance!

Answer 1

Some fancy syntax to define the extractor directly:

datatype dtype = T bool (payload: int)

Thinking about sets is a good starting point: you are looking for image for multisets. That function exists and it is called image_mset. So:

definition extr :: "dtype multiset => int multiset" where
  "extr = image_mset payload"

The syntax `# for image_mset has not yet been added to the Multiset entry, but it is used by various people.

notation image_mset (infixr "`#" 90)