Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Executing set comprehensions

Email Gateway (Sep 05 2025 at 09:22):

From: Tobias Nipkow <nipkow@in.tum.de>
Dear readers,

For a change I would like to describe a solution rather than ask a question.

If one is interested in executability, but wants to stay at an abstract level,
one is sometimes faced with the challenge of executing set comprehensions. Of
course there is no silver bullet for those, but often they feel almost
executable, but Isabelle fails to recognize this.

A brute force approach is to define a second version on the list level and prove
the equivalence and execute the list version. Here I want to show how to stay on
the set level, yet make it executable.

A typical example:

definition f :: "(int * int) set ⇒ int set" where
"f M = {b. ∃a. (a,b) ∈ M ∧ a > b}"

This is not executable because of the EX. So we need to reformulate f:

lemma f_exec[code]: "f M = (λ(a,b). b) ` {(a,b) ∈ M. a > b}"
unfolding f_def f'_def by auto

The equivalence is automatic and the result executable, eg

value "f {(2,1), (1,2), (3,1)}"

In general, you can make a set comprehension executable by transforming it into
compositions of ` (= map) and {a : M. ...} (= filter), where each component is
executable. (UN may also come in handy, but if frequently leads to "UN x : M.
{...}", which is better expressed with map and filter.)

Note that the filter pattern is restricted:
It works for variables x in {x : M. ...}; in the latest distribution it also
works for pairs (see above) and triples. Arbitrary tuples would require a simproc.

Best
Tobias

smime.p7s

Email Gateway (Sep 05 2025 at 09:25):

From: Tobias Nipkow <nipkow@in.tum.de>
Sorry, ignore the "f'_def". - Tobias

On 05/09/2025 11:22, Tobias Nipkow wrote:

Dear readers,

For a change I would like to describe a solution rather than ask a question.

If one is interested in executability, but wants to stay at an abstract level,
one is sometimes faced with the challenge of executing set comprehensions. Of
course there is no silver bullet for those, but often they feel almost
executable, but Isabelle fails to recognize this.

A brute force approach is to define a second version on the list level and prove
the equivalence and execute the list version. Here I want to show how to stay on
the set level, yet make it executable.

A typical example:

definition f :: "(int * int) set ⇒ int set" where
"f M = {b. ∃a. (a,b) ∈ M ∧ a > b}"

This is not executable because of the EX. So we need to reformulate f:

lemma f_exec[code]: "f M = (λ(a,b). b) ` {(a,b) ∈ M. a > b}"
unfolding f_def f'_def by auto

The equivalence is automatic and the result executable, eg

value "f {(2,1), (1,2), (3,1)}"

In general, you can make a set comprehension executable by transforming it into
compositions of ` (= map) and {a : M. ...} (= filter), where each component is
executable. (UN may also come in handy, but if frequently leads to "UN x : M.
{...}", which is better expressed with map and filter.)

Note that the filter pattern is restricted:
It works for variables x in {x : M. ...}; in the latest distribution it also
works for pairs (see above) and triples. Arbitrary tuples would require a simproc.

Best
Tobias

smime.p7s

Email Gateway (Sep 05 2025 at 09:52):

From: "\"Lammich, Peter (UT-EEMCS)\"" <cl-isabelle-users@lists.cam.ac.uk>
So can we add some generic simp lemmas ( and later maybe a simproc) to the code preprocessor simpset? By default or as a library they?

Peter

On 5 Sept 2025 11:25, Tobias Nipkow <nipkow@in.tum.de> wrote:
Sorry, ignore the "f'_def". - Tobias

On 05/09/2025 11:22, Tobias Nipkow wrote:

Dear readers,

For a change I would like to describe a solution rather than ask a question.

If one is interested in executability, but wants to stay at an abstract level,
one is sometimes faced with the challenge of executing set comprehensions. Of
course there is no silver bullet for those, but often they feel almost
executable, but Isabelle fails to recognize this.

A brute force approach is to define a second version on the list level and prove
the equivalence and execute the list version. Here I want to show how to stay on
the set level, yet make it executable.

A typical example:

definition f :: "(int * int) set ⇒ int set" where
"f M = {b. ∃a. (a,b) ∈ M ∧ a > b}"

This is not executable because of the EX. So we need to reformulate f:

lemma f_exec[code]: "f M = (λ(a,b). b) ` {(a,b) ∈ M. a > b}"
unfolding f_def f'_def by auto

The equivalence is automatic and the result executable, eg

value "f {(2,1), (1,2), (3,1)}"

In general, you can make a set comprehension executable by transforming it into
compositions of ` (= map) and {a : M. ...} (= filter), where each component is
executable. (UN may also come in handy, but if frequently leads to "UN x : M.
{...}", which is better expressed with map and filter.)

Note that the filter pattern is restricted:
It works for variables x in {x : M. ...}; in the latest distribution it also
works for pairs (see above) and triples. Arbitrary tuples would require a simproc.

Best
Tobias

Email Gateway (Sep 05 2025 at 11:16):

From: Manuel Eberl <manuel@pruvisto.org>
DId something change about the code generator preprocessing here? In the
past I often explicitly put "Set.filter" into the code equations instead
of "{x. P x}" to make this sort of stuff work.

On 05/09/2025 11:22, Tobias Nipkow wrote:

Dear readers,

For a change I would like to describe a solution rather than ask a
question.

If one is interested in executability, but wants to stay at an
abstract level, one is sometimes faced with the challenge of executing
set comprehensions. Of course there is no silver bullet for those, but
often they feel almost executable, but Isabelle fails to recognize this.

A brute force approach is to define a second version on the list level
and prove the equivalence and execute the list version. Here I want to
show how to stay on the set level, yet make it executable.

A typical example:

definition f :: "(int * int) set ⇒ int set" where
"f M = {b. ∃a. (a,b) ∈ M ∧ a > b}"

This is not executable because of the EX. So we need to reformulate f:

lemma f_exec[code]: "f M = (λ(a,b). b) ` {(a,b) ∈ M. a > b}"
unfolding f_def f'_def by auto

The equivalence is automatic and the result executable, eg

value "f {(2,1), (1,2), (3,1)}"

In general, you can make a set comprehension executable by
transforming it into compositions of ` (= map) and {a : M. ...} (=
filter), where each component is executable. (UN may also come in
handy, but if frequently leads to "UN x : M. {...}", which is better
expressed with map and filter.)

Note that the filter pattern is restricted:
It works for variables x in {x : M. ...}; in the latest distribution
it also works for pairs (see above) and triples. Arbitrary tuples
would require a simproc.

Best
Tobias

Email Gateway (Sep 05 2025 at 13:08):

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

On 05/09/2025 13:16, Manuel Eberl wrote:

DId something change about the code generator preprocessing here? In the past I
often explicitly put "Set.filter" into the code equations instead of "{x. P x}"
to make this sort of stuff work.

Yes, Florian has recently modified this because I felt Set.filter" wasn't ideal.

Tobias

On 05/09/2025 11:22, Tobias Nipkow wrote:

Dear readers,

For a change I would like to describe a solution rather than ask a question.

If one is interested in executability, but wants to stay at an abstract level,
one is sometimes faced with the challenge of executing set comprehensions. Of
course there is no silver bullet for those, but often they feel almost
executable, but Isabelle fails to recognize this.

A brute force approach is to define a second version on the list level and
prove the equivalence and execute the list version. Here I want to show how to
stay on the set level, yet make it executable.

A typical example:

definition f :: "(int * int) set ⇒ int set" where
"f M = {b. ∃a. (a,b) ∈ M ∧ a > b}"

This is not executable because of the EX. So we need to reformulate f:

lemma f_exec[code]: "f M = (λ(a,b). b) ` {(a,b) ∈ M. a > b}"
unfolding f_def f'_def by auto

The equivalence is automatic and the result executable, eg

value "f {(2,1), (1,2), (3,1)}"

In general, you can make a set comprehension executable by transforming it
into compositions of ` (= map) and {a : M. ...} (= filter), where each
component is executable. (UN may also come in handy, but if frequently leads
to "UN x : M. {...}", which is better expressed with map and filter.)

Note that the filter pattern is restricted:
It works for variables x in {x : M. ...}; in the latest distribution it also
works for pairs (see above) and triples. Arbitrary tuples would require a
simproc.

Best
Tobias

smime.p7s

Email Gateway (Sep 05 2025 at 13:18):

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

On 05/09/2025 11:52, "Lammich, Peter (UT-EEMCS)" (via cl-isabelle-users Mailing
List) wrote:

So can we add some generic simp lemmas ( and later maybe a simproc) to the code
preprocessor simpset? By default or as a library they?

Correct. Like this:

lemma Collect_triple_member [code_unfold, no_atp]:
\<open>{(x, y, z). List.member xs (x, y, z) \<and> P x y z} = Set.filter
(\<lambda>(x, y, z). P x y z) (set xs)\<close>
by auto

Tobias

Peter

On 5 Sept 2025 11:25, Tobias Nipkow <nipkow@in.tum.de> wrote:
Sorry, ignore the "f'_def". - Tobias

On 05/09/2025 11:22, Tobias Nipkow wrote:

Dear readers,

For a change I would like to describe a solution rather than ask a question.

If one is interested in executability, but wants to stay at an abstract level,
one is sometimes faced with the challenge of executing set comprehensions. Of
course there is no silver bullet for those, but often they feel almost
executable, but Isabelle fails to recognize this.

A brute force approach is to define a second version on the list level and prove
the equivalence and execute the list version. Here I want to show how to stay on
the set level, yet make it executable.

A typical example:

definition f :: "(int * int) set ⇒ int set" where
"f M = {b. ∃a. (a,b) ∈ M ∧ a > b}"

This is not executable because of the EX. So we need to reformulate f:

lemma f_exec[code]: "f M = (λ(a,b). b) ` {(a,b) ∈ M. a > b}"
unfolding f_def f'_def by auto

The equivalence is automatic and the result executable, eg

value "f {(2,1), (1,2), (3,1)}"

In general, you can make a set comprehension executable by transforming it into
compositions of ` (= map) and {a : M. ...} (= filter), where each component is
executable. (UN may also come in handy, but if frequently leads to "UN x : M.
{...}", which is better expressed with map and filter.)

Note that the filter pattern is restricted:
It works for variables x in {x : M. ...}; in the latest distribution it also
works for pairs (see above) and triples. Arbitrary tuples would require a simproc.

Best
Tobias

smime.p7s

Last updated: Sep 13 2025 at 04:22 UTC