*To*: Lawrence Paulson <lp15 at cam.ac.uk>, Julian <parsert.julian at gmail.com>*Subject*: Re: [isabelle] Syntax for Min/Max, or the notation for images*From*: Andreas Lochbihler <mail at andreas-lochbihler.de>*Date*: Mon, 19 Feb 2018 07:39:08 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <50A95F56-2495-4044-9849-6EF928B1B286@cam.ac.uk>*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>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:52.0) Gecko/20100101 Thunderbird/52.6.0

The map operation on multisets, image_mset, already uses the proposed syntax: {# a i. i :# M #} = image_mset (%i. a i) M

{ 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 have a uniform syntax for all future situations. E.g. the current (⋃x∈A. B x) could also be written ⋃{B x. x∈A}. Larry

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

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

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

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