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



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






Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



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