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



I wonder why there is an existential quantifier in the translation of the
set comprehension in the first place.
If {a i | i. M} would translate to "image a (Collect M)", the awkward
existential quantifier would be gone (I suppose that the simplifier can
deal much more easily with "image a" than with the existential quantifier.)
For example, {a i |i. i ∈ I} would translate to "image a (Collect (%x.
x:I))" which the simplifier can easily rewrite to "image a I".

Of course, I also understand that changing this might introduce too many
breaking changes in proofs.

Best wishes,
Dominique.



On 19 February 2018 at 08:39, Andreas Lochbihler <mail at andreas-lochbihler.de
> 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
>>
>>
>>
>>
>



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