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.