Error: 'Non-constructor pattern not allowed in sequential mode' (Isabelle)

Question

我正在尝试定义一个函数 Sum f k，它将 f 从 0 到 k-1 求和，使得

Sum f k = f 0 + ⋯ + f (k - 1).

我定义如下：

fun Sum :: "(nat => nat) => nat => nat" where
  "Sum f 1 = f 0"
| "Sum f k = f (k-1) + Sum f (k-1)"

但是，这给出了以下错误消息：

Malformed definition:
Non-constructor pattern not allowed in sequential mode.
⋀f. Sum f 1 = f 0

当我定义 Sum f 0 = f 0 时，此错误消息消失，但这不是我要定义的函数。我也可以使用 function 并自己给出健全性证明，但如果有必要，我会感到非常惊讶

有人可以解释错误信息并推荐 workaround/correction 吗？

Answer 1

您只能在模式匹配中使用构造函数。 nat 的构造函数是 0 和 Suc。所以如果你把 1 写成 (Suc 0) 它应该可以工作。

function