# Re: [isabelle] Syntax for Min/Max, or the notation for images

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

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*