*To*: Isabelle Users <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Syntax for Min/Max, or the notation for images*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Mon, 19 Feb 2018 07:58:54 +0100*In-reply-to*: <46e5366f-4cb2-9b7c-39c2-827450f24c24@andreas-lochbihler.de>*References*: <876D88B5-D41B-467A-9FD6-264E08ECF1FD@cam.ac.uk> <1518799126.17422.18.camel@in.tum.de> <bdeb60d8-de79-05c2-62a4-0d875241a876@in.tum.de> <1518968629.1092.1.camel@cis.upenn.edu> <bc7029e1-e9ee-af7e-10de-e281df81efbd@gmail.com> <50A95F56-2495-4044-9849-6EF928B1B286@cam.ac.uk> <46e5366f-4cb2-9b7c-39c2-827450f24c24@andreas-lochbihler.de>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.10; rv:52.0) Gecko/20100101 Thunderbird/52.6.0

Tobias On 19/02/2018 07:39, Andreas Lochbihler wrote:

The map operation on multisets, image_mset, already uses the proposed syntax: {# a i. i :# M #} = image_mset (%i. a i) MSo extending this syntax to ordinary sets would be just more uniform syntax. Buthow does it interoperate with ordinary set comprehension? How do we want todistinguish the following two cases:{ i. i : M } = Collect (%i. i : M) vs. { i. i : M } = image (%i. i) M Andreas On 18/02/18 19:08, Lawrence Paulson wrote:On 18 Feb 2018, at 15:48, Julian <parsert.julian at gmail.com> wrote: do you mean the same as {a i |i. i ∈ I}?This is logically equivalent to the image operator, but denotes something like{x. ∃i∈I. x = a i}, while “image” is a single constant.The advantage of introducing something like {a i. i ∈ I} is that we would havea uniform syntax for all future situations. E.g. the current (⋃x∈A. B x) couldalso be written ⋃{B x. x∈A}.Larry

**Attachment:
smime.p7s**

**Follow-Ups**:**Re: [isabelle] Syntax for Min/Max, or the notation for images***From:*Lawrence Paulson

**References**:**[isabelle] Syntax for Min/Max, or the notation for images***From:*Lawrence Paulson

**Re: [isabelle] Syntax for Min/Max, or the notation for images***From:*Peter Lammich

**Re: [isabelle] Syntax for Min/Max, or the notation for images***From:*Tobias Nipkow

**Re: [isabelle] Syntax for Min/Max, or the notation for images***From:*Joachim Breitner

**Re: [isabelle] Syntax for Min/Max, or the notation for images***From:*Julian

**Re: [isabelle] Syntax for Min/Max, or the notation for images***From:*Lawrence Paulson

**Re: [isabelle] Syntax for Min/Max, or the notation for images***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] Syntax for Min/Max, or the notation for images
- Next by Date: Re: [isabelle] Proof of concept: BNF-based records
- Previous by Thread: Re: [isabelle] Syntax for Min/Max, or the notation for images
- Next by Thread: Re: [isabelle] Syntax for Min/Max, or the notation for images
- Cl-isabelle-users February 2018 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