Re: [isabelle] Notation issues trying to make Multiset more convenient

I was wondering whether it also makes sense to extend set
comprehensions with function image {# f x| x:M. P x #} in analogy with
set comprehensions.  The multiset image preserves multiplicities by
adding up the number of occurrences of each element that maps to a
given one.  That is, I think we would like to have the following
theorem hold (and perhaps this can be a definition):

count {# f x| x:M. P x #} a = size {# y:M. f y = a & P y #}

Actually, it seems more sensible for me to write :# within set
comprehension whenever we refer to multisets, so that we can have both

{# f x| x : S. P x #}     when S is a set, and
{# f x| x :# M. P x #}     when M is a multiset.

Am I mistaken that this is currently not in the library?


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