# Re: [isabelle] set comprehension with pairs

```Andreas Lochbihler wrote:
```
```Hi Andrei,

the sytnax translation "{x. P}" == "Collect (%x. P)" in theory Set
tells you that "{(x, y). P x y}" is "Collect (%(x, y). P x y)".
```
Now, the translation "%(x,y).b" == "split(%x y. b)" in theory Product_Type defines the syntax "%(x, y). P x y" for
```"split (%x y. P x y)". "%x y. P x y" eta-contracts to "P".

```
Hence, your expression stands for "Collect (split P)", or in nice syntax if "split P" is eta-expanded to "%z. split P z": "{z. split P z}".
```
Regards,
Andreas

```
In general I find it easiest to answer questions like this in the following way:
```(which I think has been removed from more recent versions of Isabelle)
> val it = () : unit
> read "{(x, y). P x y}"  ;
val it =
Const ("Collect", "(('a, 'b) * => bool) => ('a, 'b) * set") \$
(Const ("split", "('a => 'b => bool) => ('a, 'b) * => bool") \$
Abs
("x",
"'a"
Abs
("y",
"'b",
Free ("P", "'a => 'b => bool") \$ Bound 1 \$ Bound 0)))
: Term.term

```
And I recall being told that there is some Isar equivalent to this (possibly involving the command "term" ? )
```
Jeremy

```
```
Andrei Popescu schrieb:
```
```Hello,
Given  P :: 'a => 'b => bool,
I would like to know what does the expression
{(x,y). P x y}
*precisely* stand for.
Is it something like
{z. EX x y. z = (x,y) /\ P x y} ?

```
Knowing this would help me deal more easily with some trivial set theory that seems reluctant to blasting. 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. Thank you in advance, Andrei Popescu
```

```
```

```
```

```

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