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.


> Thank you in advance, 
>    Andrei Popescu 

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