Isabelle中rtrancl表达式求值出现nat类排序错误如何解决

• trancl（传递闭包）的默认求值规则仅基于给定的有限边集做可达性计算，不需要枚举所属类型的全部元素，因此可以直接对nat类型的输入正常求值。
• Isabelle 默认配置中，rtrancl（自反传递闭包）的代码生成规则是为有限枚举类型设计的：它会先枚举所属类型的所有元素生成全量自反边Id，再和传递闭包的结果合并。而nat是无限类型，不满足enum（可枚举）类的约束，因此触发 Wellsortedness 错误。

你添加的Id代码引理不生效的原因是：默认的rtrancl代码方程并不会将成员判断展开为(x,y) ∈ trancl R ∨ (x,y) ∈ Id的形式，所以修改Id的求值规则不会被触发。

直接为rtrancl添加适配非枚举类型的代码生成引理即可：

lemma rtrancl_code [code]: "(x, y) ∈ rtrancl R ⟷ x = y ∨ (x, y) ∈ trancl R"
  by (simp add: rtrancl_eq_or_trancl)

添加该引理后，代码生成器对rtrancl的成员判断会直接拆分为相等判断和trancl判断，两者都不需要enum类约束，你给出的测试语句就可以正常返回True。

该问题没有更底层的逻辑限制，只是Isabelle默认仅为rtrancl提供了适配有限枚举类型的求值规则，没有配置通用的非枚举类型求值规则，属于代码生成规则配置的缺失，不是逻辑层面的限制。

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