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



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
Description: This is a digitally signed message part



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