Re: [isabelle] set comprehension with pairs



> 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
>>>
>>>
>>>       
>>
>>
>
>






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