*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Syntax for Min/Max, or the notation for images*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Sun, 18 Feb 2018 13:28:12 +0100*In-reply-to*: <1518799126.17422.18.camel@in.tum.de>*References*: <876D88B5-D41B-467A-9FD6-264E08ECF1FD@cam.ac.uk> <1518799126.17422.18.camel@in.tum.de>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.10; rv:52.0) Gecko/20100101 Thunderbird/52.6.0

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 -- PeterLarry Paulson

**Attachment:
smime.p7s**

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

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

- 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