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).

Tobias

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)

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






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



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