# Re: [isabelle] set comprehension with pairs

Andrei Popescu wrote:
> Hello,
>
> Given P :: 'a => 'b => bool,
>
> I would like to know what does the expression
>
> {(x,y). P x y}
>
> *precisely* stand for.
Collect (split P)
> Is it something like
>
> {z. EX x y. z = (x,y) /\ P x y} ?
No. That is what you get when you use the syntax {(x,y)| x y. P x y}
> Knowing this would help me deal more easily with some trivial set theory that seems reluctant to blasting.
I believe "blast" is mostly superior to "fast", but in the case of
tuples "fast" can be superior - try that.
> I would also appreciate if someone showed me not only the answer to this, but also the way I could have found out myself looking at the online libraries.
See the Isabelle/HOL tutorial, 8.2 Pairs and Tuples.
The syntax is defined in theory Product_type. However, this is difficult
to spot because sets are not mentioned at all at that point. This is
were patterns (syntax _patterns) are extended with tuples - the fact
that {_ . _} allows patterns is found in theory Set.
Best
Tobias
> Thank you in advance,
> Andrei Popescu
>
>
>
>

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