函数定义不终止...？

Question

我有以下 isabelle 代码 sn-p:

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]] 添加到程序中，但这只会产生很长且（对我来说是初学者）难以理解的跟踪。如果有人想看，我可以在这里发布，但它很长。

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

Answer 1

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

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

简而言之，定义左侧的模式太复杂了，而且重叠很多。尝试简化它们。

---

¹另见下方 Manuel Eberl 的评论。