*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Syntax for Min/Max, or the notation for images*From*: Joachim Breitner <joachim at cis.upenn.edu>*Date*: Sun, 18 Feb 2018 10:43:49 -0500*In-reply-to*: <bdeb60d8-de79-05c2-62a4-0d875241a876@in.tum.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>

Hi, I have, in the past, missed a concise quantifier-free syntax for set image, and would have wanted (expected, even?) something like {a i. i ∈ I} Cheers, Joachim Am Sonntag, den 18.02.2018, 13:28 +0100 schrieb Tobias Nipkow: > I agree with Peter because the SUP syntax ultimately stands for "a ` I", which > is what you want (because it avoids the quantifier). It is a very natural syntax > and avoids inventing a new syntax for image. > > Tobias > > On 16/02/2018 17:38, Peter Lammich wrote: > > On Fr, 2018-02-16 at 16:14 +0000, Lawrence Paulson wrote: > > > I've noticed that Isabelle/HOL has no syntax for the minimum/maximum > > > of a finite set. Or rather, while one can write Max {a i| i. i ∈ I}, > > > such a set comprehension can translate into a complicated formula > > > involving existential quantifiers, with the reasoning similarly > > > complicated. Or one could instead use the image operator and write > > > Max (a ` I). > > > > > > In fact (a ` I) = {a i| i. i ∈ I}, and a more general form of this > > > result exists as the lemma setcompr_eq_image. > > > > > > Arguably what's needed here isn't special syntax for Min/Max but > > > rather an alternative syntax for image, e.g. {a i. i ∈ I}. Are there > > > any views? > > > > Why not use the existing Syntax for INF/SUP ? > > > > term "SUP x:X. f x" > > > > i.e. one could declare syntax: > > MAX i:I. a i > > > > -- Peter > > > > > > > > > > > > Larry Paulson > > > > > > > > > > > > > > -- Joachim Breitner Post-Doctoral researcher http://cis.upenn.edu/~joachim

**Attachment:
signature.asc**

**Follow-Ups**:

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

- 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