isabelle - 无法使用自反传递闭包评估表达式

Question

以下表达式几乎相同：

value "(1,5) ∈ trancl {(1::nat,2::nat),(2,5)}"
value "(1,5) ∈ rtrancl {(1::nat,2::nat),(2,5)}"

但是，第一个评估得很好，而第二个我收到以下错误：

Wellsortedness error:
Type nat not of sort {enum,equal}
No type arity nat :: enum

似乎错误是由身份关系引起的：

value "(1::nat,5::nat) ∈ Id"

但是，以下代码引理无济于事：

lemma Id_code [code]: "(a, b) ∈ Id ⟷ a = b" by simp

你能建议如何解决它吗？为什么它不能从头开始工作？仅仅是代码引理的不完整还是有更根本的原因？

标签： isabelle

Answer 1