Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] set comprehension with pairs

Email Gateway (Aug 18 2022 at 13:44):

From: Andrei Popescu <uuomul@yahoo.com>
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

Email Gateway (Aug 18 2022 at 13:45):

From: Tobias Nipkow <nipkow@in.tum.de>
Andrei Popescu wrote:

Hello,

Given P :: 'a => 'b => bool,

I would like to know what does the expression

{(x,y). P x y}

precisely stand for.

Collect (split P)

Is it something like

{z. EX x y. z = (x,y) /\ P x y} ?

No. That is what you get when you use the syntax {(x,y)| x y. P x y}

Knowing this would help me deal more easily with some trivial set theory that seems reluctant to blasting.

I believe "blast" is mostly superior to "fast", but in the case of
tuples "fast" can be superior - try that.

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.

See the Isabelle/HOL tutorial, 8.2 Pairs and Tuples.
The syntax is defined in theory Product_type. However, this is difficult
to spot because sets are not mentioned at all at that point. This is
were patterns (syntax _patterns) are extended with tuples - the fact
that {_ . _} allows patterns is found in theory Set.

Best
Tobias

Thank you in advance,
Andrei Popescu

Email Gateway (Aug 18 2022 at 13:46):

From: Andreas Lochbihler <lochbihl@ipd.info.uni-karlsruhe.de>
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

Andrei Popescu schrieb:

Email Gateway (Aug 18 2022 at 13:47):

From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
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

Email Gateway (Aug 18 2022 at 13:47):

From: Peter Lammich <peter.lammich@uni-muenster.de>

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

Email Gateway (Aug 18 2022 at 13:48):

From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
Peter Lammich wrote:
No, I definitely meant the command "term", though from the
documentation, it looks as though the antiquotation "term" should have a
similar effect

Regards,

Jeremy

Last updated: May 03 2024 at 12:27 UTC