I know I am missing something obvious, but I am lost in how to make this one work. I am trying to write the set comprehension for a kind of "Cartesian product". Given a finite set S of finite sets, I would like to build a sets of sets of pairs, where each pair is given by one of the sets in S and one value v in that set; and each set has exactly one pair for each of set sets in S.
Basically, given the (simplistic) example
definition s1 :: "nat set" where
"s1 = {1, 2}"
definition s2 :: "nat set" where
"s2 = {4, 5}"
definition S :: "nat set set" where
"S = {s1, s2}"
value "{{(s, v) | s. s ∈ S} | v. v ∈ s}"
I would like the evaluation to become {{({1, 2}, 1), ({4, 5}, 4)}, {({1, 2}, 1), ({4, 5}, 5)}, {({1, 2}, 2), ({4, 5}, 4)}, {({1, 2}, 2), ({4, 5}, 5)}}
Instead, it does evaluate to (what it is supposed to, I realize that)
"(λu. {({1, 2}, u), ({4, 5}, u)}) ` s"
:: "(nat set × 'a) set set"
The u variable is bound to a free variable "s", I don't know how to have different "u"s and bound each u to its "associated"
s ∈ S
Thank you for any points or directions.
The simple way is to avoid the problem and express everything as image over the set:
value "(λv. (Pair v) ` S) ` S"
In general, there are two ways to do this kind of things: make the code generator work or the better way, namely adapt the definition to make them easier to fit the evaluation model.