*To*: isabelle-users at cl.cam.ac.uk*Subject*: Re: [isabelle] Notation issues trying to make Multiset more convenient*From*: "Viktor Kuncak" <viktor.kuncak at epfl.ch>*Date*: Wed, 28 Nov 2007 16:21:49 +0100*In-reply-to*: <473C2D0D.1060702@cse.unsw.edu.au>*References*: <473BE428.8000008@cse.unsw.edu.au> <473C26FE.7060405@uni-muenster.de> <473C2D0D.1060702@cse.unsw.edu.au>*Reply-to*: viktor.kuncak at epfl.ch*Sender*: vkuncak at gmail.com

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

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

**Re: [isabelle] Notation issues trying to make Multiset more convenient***From:*Tobias Nipkow

**Re: [isabelle] Notation issues trying to make Multiset more convenient***From:*Tobias Nipkow

**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

- Previous by Date: Re: [isabelle] ProofGeneral 3.7pre071112 gets out of sync with Isabelle process
- Next by Date: [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