*To*: Andreas Lochbihler <mail at andreas-lochbihler.de>*Subject*: Re: [isabelle] Syntax for Min/Max, or the notation for images*From*: Dominique Unruh <unruh at ut.ee>*Date*: Mon, 19 Feb 2018 08:54:54 +0200*Cc*: Lawrence Paulson <lp15 at cam.ac.uk>, Julian <parsert.julian at gmail.com>, cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*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>

I wonder why there is an existential quantifier in the translation of the set comprehension in the first place. If {a i | i. M} would translate to "image a (Collect M)", the awkward existential quantifier would be gone (I suppose that the simplifier can deal much more easily with "image a" than with the existential quantifier.) For example, {a i |i. i ∈ I} would translate to "image a (Collect (%x. x:I))" which the simplifier can easily rewrite to "image a I". Of course, I also understand that changing this might introduce too many breaking changes in proofs. Best wishes, Dominique. On 19 February 2018 at 08:39, Andreas Lochbihler <mail at andreas-lochbihler.de > wrote: > The map operation on multisets, image_mset, already uses the proposed > syntax: > > {# a i. i :# M #} = image_mset (%i. a i) M > > So extending this syntax to ordinary sets would be just more uniform > syntax. But how does it interoperate with ordinary set comprehension? How > do we want to distinguish 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 >> 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 >> >> >> >> >

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