如何定义交换(X)以使这个定理没有错误?

Question

我正在学习使用Isabelle来证明某些理论，但我遇到了一个问题。我想知道如何定义exchange(X)以确保下面代码清单中提出的定理可以在不引起错误的情况下陈述？

theorem exchange_wp2_1:
"
preOrder(T) =X @ preOrder(q) @ F(S) ∧ exchange(X) ∧ q ≠ null ⟹
preOrder(T)=X @ (data q) @ preOrder(ltree q) @ F ([rtree q] @ S)
"

错误：

类型统一失败："_list"和"_tree"类型的现金类型错误 在应用中：不兼容的操作数类型 运算符：交换：：？？ '树⇒布尔运算符：X：：？？'b 列表

Answer 1

我不知道预序和交换的确切定义，但似乎preOrder返回一个列表，而exchange期望一个树作为输入。所以，在你的表达中，不清楚X应该具有什么类型：它是一棵树还是一个列表？

preOrder(T) = X        (so X is list)
exchange X             (so X is a tree)

这就是错误消息告诉您的。