函数定义不会终止...？

Question

我有以下伊莎贝尔代码片段：

type_synonym vname = string
datatype aexp = N int | V vname | Plus aexp aexp

fun full_plus :: "aexp ⇒ aexp ⇒ aexp" where
"full_plus (N n⇩1) (N n⇩2) = N (n⇩1+n⇩2)" |
"full_plus (N n⇩1) (Plus (N n⇩2) a) = (Plus (N (n⇩1+n⇩2)) a)" |
"full_plus (N n⇩1) (Plus a (N n⇩2)) = (Plus (N (n⇩1+n⇩2)) a)" |
"full_plus (Plus (N n⇩1) a) (N n⇩2) = (Plus (N (n⇩1+n⇩2)) a)" |
"full_plus (Plus a (N n⇩1)) (N n⇩2) = (Plus (N (n⇩1+n⇩2)) a)" |
"full_plus (Plus a⇩1 (N n⇩1)) (Plus a⇩2 (N n⇩2)) = (Plus (N (n⇩1+n⇩2)) (Plus a⇩1 a⇩2))" |
"full_plus (Plus a⇩1 (N n⇩1)) (Plus (N n⇩2) a⇩2) = (Plus (N (n⇩1+n⇩2)) (Plus a⇩1 a⇩2))" |
"full_plus (Plus (N n⇩1) a⇩1) (Plus a⇩2 (N n⇩2)) = (Plus (N (n⇩1+n⇩2)) (Plus a⇩1 a⇩2))" |
"full_plus (Plus (N n⇩1) a⇩1) (Plus (N n⇩2) a⇩2) = (Plus (N (n⇩1+n⇩2)) (Plus a⇩1 a⇩2))" |
"full_plus a⇩1 a⇩2 = Plus a⇩1 a⇩2"

但是，函数定义在 jEdit 中变为紫色。当我将递归引理标记为 [simp] 时，我已经看到这种情况发生，所以我假设这意味着后端冻结或陷入无限循环，但从来没有函数。在我看来 full_plus 不会递归......？我已将 declare [[simp_trace]] 添加到程序中，但这只会产生很长且（对我来说，初学者）难以理解的痕迹。如果有人想看，我可以post在这里，但是它很长。

供参考，这是免费在线具体语义书中的练习 3.2。希望有人能帮帮我！

Answer 1

我运行你的函数定义在我的电脑上，它最终完成了。

提供fun的函数包将您的函数定义重写为可用于Isabelle证明的方程。为此，它必须检查您的定义和左侧的模式是否不重叠。如果有重叠（这里就是这种情况），它必须将定义重写为非重叠的¹。鉴于您的复杂定义，需要很长时间才能做到这一点。

简而言之，您定义左侧的模式太复杂并且有很多重叠。尽量简化它们。

¹另请参阅下面 Manuel Eberl 的评论。

函数定义不会终止...？

Function definition does not terminate...?

function

termination

isabelle