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

Using a standard set-comprehension syntax for image is plain misleading and will create more confusion (even if we manage to resolve the ambiguity that Andreas pointed out).


On 19/02/2018 07:39, Andreas Lochbihler wrote:
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)


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


On 18/02/18 19:08, Lawrence Paulson wrote:
On 18 Feb 2018, at 15:48, Julian <parsert.julian at> 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}.


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

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