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.