*To*: viktor.kuncak at epfl.ch*Subject*: Re: [isabelle] Notation issues trying to make Multiset more convenient*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Thu, 29 Nov 2007 22:30:32 +0100*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <b0a0d4300711280721taeac1a4p600eca29f324482a@mail.gmail.com>*References*: <473BE428.8000008@cse.unsw.edu.au> <473C26FE.7060405@uni-muenster.de> <473C2D0D.1060702@cse.unsw.edu.au> <b0a0d4300711280721taeac1a4p600eca29f324482a@mail.gmail.com>*User-agent*: Thunderbird 2.0.0.0 (Macintosh/20070326)

I just realize that image can be defined very directly: "f `# M == Abs_multiset (%x. size {# y:M. x = f y #})" Look, no hands ;-) Tobias 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? Viktor

**References**:**[isabelle] Notation issues trying to make Multiset more convenient***From:*Rafal Kolanski

**Re: [isabelle] Notation issues trying to make Multiset more convenient***From:*Peter Lammich

**Re: [isabelle] Notation issues trying to make Multiset more convenient***From:*Rafal Kolanski

**Re: [isabelle] Notation issues trying to make Multiset more convenient***From:*Viktor Kuncak

- Previous by Date: Re: [isabelle] Notation issues trying to make Multiset more convenient
- Next by Date: Re: [isabelle] converting a multiset to a list
- Previous by Thread: Re: [isabelle] Notation issues trying to make Multiset more convenient
- Next by Thread: Re: [isabelle] Notation issues trying to make Multiset more convenient
- Cl-isabelle-users November 2007 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list