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

> 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" ? ) > You probably mean the @{term ...} antiqotation, i.e. from Isar-level: ML {* @{term "{(x, y). P x y}"} *} -- Peter > 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 >>> >>> >>> >> >> > >

**Follow-Ups**:**Re: [isabelle] set comprehension with pairs***From:*Jeremy Dawson

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

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

**Re: [isabelle] set comprehension with pairs***From:*Jeremy Dawson

- Previous by Date: Re: [isabelle] Isabelle and latex questions
- Next by Date: [isabelle] Silly problem with maps and
- 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