*To*: Andreas Lochbihler <lochbihl at ipd.info.uni-karlsruhe.de>*Subject*: Re: [isabelle] set comprehension with pairs*From*: Jeremy Dawson <jeremy at rsise.anu.edu.au>*Date*: Tue, 14 Jul 2009 10:20:26 +1000*Cc*: Andrei Popescu <uuomul at yahoo.com>, cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <4A571CAE.1050107@ipd.info.uni-karlsruhe.de>*References*: <918087.81106.qm@web56103.mail.re3.yahoo.com> <4A571CAE.1050107@ipd.info.uni-karlsruhe.de>*User-agent*: Thunderbird 1.5.0.12 (X11/20070604)

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 theoryProduct_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 nicesyntax if "split P" is eta-expanded to "%z. split P z": "{z. split P z}".Regards, Andreas

(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

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 settheory that seems reluctant to blasting. I would also appreciate ifsomeone showed me not only the answer to this, but also the way Icould have found out myself looking at the online libraries.Thank you in advance, Andrei Popescu

**Follow-Ups**:**Re: [isabelle] set comprehension with pairs***From:*Peter Lammich

**References**:**[isabelle] set comprehension with pairs***From:*Andrei Popescu

**Re: [isabelle] set comprehension with pairs***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] collections of rules for automatic proof methods
- Next by Date: Re: [isabelle] Isabelle and latex questions
- Previous by Thread: Re: [isabelle] set comprehension with pairs
- Next by Thread: Re: [isabelle] set comprehension with pairs
- Cl-isabelle-users July 2009 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list