Isabelle中带过滤条件的nat类型集合推导式求值报错如何解决？

你遇到的排序错误是Isabelle的value命令默认求值策略导致的：

• 无过滤条件的集合推导式可以被正常识别为「遍历给定有限集合映射取值」，无需枚举整个类型
• 添加∧连接的过滤条件后，默认的求值器不会自动识别到约束仅作用于给定的有限集合，会尝试枚举整个nat × nat类型来匹配谓词，而nat是无限类型，没有实现enum（可枚举）类型类，因此抛出错误。

方案1：改写集合推导式结构 #

将过滤条件内化为给定集合的子集约束，让求值器明确只需遍历有限范围：

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

这种写法与你原有的带过滤条件的推导式完全等价，可直接正常求值得到结果{2, 3}。

方案2：指定value命令的code求值模式 #

不需要修改推导式写法，仅需给value命令加上[code]参数，启用代码生成器模式的求值逻辑，该模式可以正确识别有限集合的约束范围，不会触发全类型枚举逻辑：

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

执行后可直接得到正确的求值结果。

以上两种方案都不需要将set替换为fset或list类型，可直接满足需求。

内容的提问来源于stack exchange，提问作者Denis