评估复杂的集合理解表达式

Question

以下表达式的计算结果很好：

value "{fst x | x. x ∈ {(1::nat,2::nat),(2,4),(3,4)}}"

但是对于下面的表达式：

value "{fst x | x. x ∈ {(1::nat,2::nat),(2,4),(3,4)} ∧ snd x = 4}"

我收到错误：

Wellsortedness error:
Type nat × nat not of sort enum
No type arity nat :: enum

如何计算这样的表达式？是否可以不将 set 替换为 fset 或 list 类型？

Answer 1

集合理解转换为代码有点棘手，因为在 {f x y |x y. …} 的漂亮语法背后，有 x 和 y 的（无界）存在量词，并且无界由于显而易见的原因，存在和代码生成不能很好地混合：只有当底层类型具有有限多个值并且这些值可以被建设性地枚举时，才能评估无界存在 - 因此推断出 nat :: enum 约束。

解决此问题的一个好方法是使用“设置图像”运算符 ` 和 Set.filter 函数使计算方法更明确一些：

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

评估复杂的集合理解表达式

Evaluate complex set comprehension expression

isabelle