The following expression is evaluated fine:
value "{fst x | x. x ∈ {(1::nat,2::nat),(2,4),(3,4)}}"
But for the following expression:
value "{fst x | x. x ∈ {(1::nat,2::nat),(2,4),(3,4)} ∧ snd x = 4}"
I get error:
Wellsortedness error:
Type nat × nat not of sort enum
No type arity nat :: enum
How to evaluate such an expression? Is it possible without replacing set by fset or list types?
Set comprehensions are a bit tricky to convert to code because behind that pretty syntax with the {f x y |x y. …}, there are (unbounded) existential quantifiers for x and y, and unbounded existentials and code generation do not mix well for obvious reasons: an unbounded existential can only be evaluated if the underlying type has finitely many values and those values can be enumerated constructively – hence the inferred nat :: enum constraint.
A good way around this is to make what the way to compute this a bit more explicit by using the ‘set image’ operator ` and the Set.filter function:
lemma "{fst x | x. x ∈ {(1::nat,2::nat),(2,4),(3,4)} ∧ snd x = 4} =
fst ` Set.filter (λx. snd x = 4) {(1::nat,2::nat),(2,4),(3,4)}"
unfolding Set.filter_def by blast
value "fst ` Set.filter (λx. snd x = 4) {(1::nat,2::nat),(2,4),(3,4)}"