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

I agree with Peter Lammich that multiset image is the right way to define these concepts:

{# f x| x :# M. P x #} = f `# {#x:M. P x#}

And maybe one should indeed modify the current multiset comprehension syntax to distinguish between :# and :. I will gladly add this, and Peter's theory (esp a cleaned up version) might be a good starting point.


PS A recursion cominator for multisets would enable us to define image without the detour via an inductive definition. Any volunteers?

Viktor Kuncak schrieb:
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.