Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Set notation for tuples broken

Email Gateway (Aug 19 2022 at 10:41):

From: John Wickerson <jpw48@cam.ac.uk>
When you want to use a pattern in your set comprehension, you can't just write

{(a,b). P a b}

you have to write:

{(a,b) | a b. P a b}

cheers,
john

Email Gateway (Aug 19 2022 at 10:42):

From: Tobias Nipkow <nipkow@in.tum.de>
Am 10/03/2013 00:00, schrieb C. Diekmann:

Hi,

I want to report that the following set notation is unfortunately not accepted:
{(a,b) ∈ X. P a}

The following work-around is accepted:
{(a,b). (a, b) ∈ X ∧ P a b}

lemma split_conv_set: "{x ∈ X. case x of (a,b) ⇒ P a b} = {(a,b). (a,
b) ∈ X ∧ P a b}"
by fastforce

What must I do to use the first notation?

It does not exist is the short answer. It may be possible to modify the syntax
to support it, but not as an extension: I would have to modify the basic set
syntax. I'll look into it. (In any case, it would only be available as input
syntax.)

Regards
Tobias

Regards
Cornelius

Email Gateway (Aug 19 2022 at 10:42):

From: Tobias Nipkow <nipkow@in.tum.de>
Am 10/03/2013 08:36, schrieb John Wickerson:

When you want to use a pattern in your set comprehension, you can't just write

{(a,b). P a b}

Yes, you can. It stands for Collect(%(a,b). P a).

you have to write:

{(a,b) | a b. P a b}

This produces Collect(%p. EX a b. p = (a,b) & P a b).

Tobias

cheers,
john

On 10 Mar 2013, at 00:00, C. Diekmann wrote:

Hi,

I want to report that the following set notation is unfortunately not accepted:
{(a,b) ∈ X. P a}

The following work-around is accepted:
{(a,b). (a, b) ∈ X ∧ P a b}

lemma split_conv_set: "{x ∈ X. case x of (a,b) ⇒ P a b} = {(a,b). (a,
b) ∈ X ∧ P a b}"
by fastforce

What must I do to use the first notation?

Regards
Cornelius

Email Gateway (Aug 19 2022 at 10:42):

From: John Wickerson <jpw48@cam.ac.uk>
Oh, that's new to me. Just to clarify, should that be "Collect(%(a,b). P a b)" or do you really mean "Collect(%(a,b). P a)" ?

Email Gateway (Aug 19 2022 at 10:42):

From: Tobias Nipkow <nipkow@in.tum.de>
Sorry, P a b it should have been.

Tobias

Email Gateway (Aug 19 2022 at 10:43):

From: Tobias Nipkow <nipkow@in.tum.de>
Now it is, in the development version. It is input syntax that tranlates into
{(a,b). (a,b) ∈ X & P a}.

Tobias

Email Gateway (Aug 19 2022 at 10:43):

From: "C. Diekmann" <diekmann@in.tum.de>
Great :)

I guess the lemma I called split_conv_set might be also very useful
for the simplifier then?

Cheers
Cornelius

Email Gateway (Aug 19 2022 at 10:44):

From: Tobias Nipkow <nipkow@in.tum.de>
Am 12/03/2013 13:04, schrieb C. Diekmann:

2013/3/12 Tobias Nipkow <nipkow@in.tum.de>:

Am 10/03/2013 00:00, schrieb C. Diekmann:

I want to report that the following set notation is unfortunately not accepted:
{(a,b) ∈ X. P a}

Now it is, in the development version. It is input syntax that tranlates into
{(a,b). (a,b) ∈ X & P a}.

Great :)

I guess the lemma I called split_conv_set might be also very useful
for the simplifier then?

I don't see that it would help much.

Tobias

Cheers
Cornelius

Last updated: Apr 24 2024 at 08:20 UTC