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



The map operation on multisets, image_mset, already uses the proposed syntax:

{# a i. i :# M #} = image_mset (%i. a i) M

So extending this syntax to ordinary sets would be just more uniform syntax. But how does it interoperate with ordinary set comprehension? How do we want to distinguish the following two cases:

{ i. i : M } = Collect (%i. i : M)

vs.

{ i. i : M } = image (%i. i) M

Andreas

On 18/02/18 19:08, Lawrence Paulson wrote:
On 18 Feb 2018, at 15:48, Julian <parsert.julian at gmail.com> wrote:

do you mean the same as {a i |i. i ∈ I}?

This is logically equivalent to the image operator, but denotes something like {x. ∃i∈I. x = a i}, while “image” is a single constant.

The advantage of introducing something like {a i. i ∈ I} is that we would have a uniform syntax for all future situations. E.g. the current (⋃x∈A. B x) could also be written ⋃{B x. x∈A}.

Larry







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