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



Am Dienstag, den 20.02.2018, 08:29 +0100 schrieb Tobias Nipkow:
> 
> On 19/02/2018 15:34, Lawrence Paulson wrote:
> > Users (especially beginners) should be aware that a general
> > comprehension could give rise to a large formula. I frequently
> > write expressions using nested unions instead. I don't know whether
> > it really simplifies reasoning steps, but I find it clearer.
> 
> I can never make up my mind.
> Code generation needs Unions, but that is orthogonal.
> 
> Tobias

Another option is to intruduce the applicative <*>

  (<*>) :: ('a => 'b) set => 'a set => 'b set

  F <*> A = { f a | f a. f : F & a : A}

This allows some nice point-free style:

  {(+)} <*> A <*> B   (or (+) ` A <*> B)

But still gives nice rules, especially for finiteness, countability:

  finite A ==> finite F ==> finite (F <*> A)

And it should work well with code generation.

A counter point is that it is a very CS style notation and uncommon in
mathematics.

 - Johannes





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