Re: [isabelle] set comprehension with pairs

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}".


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.