function - 错误: '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自己提供健全性证明，但是如果有必要，我会感到非常惊讶

有人可以解释该错误信息并建议解决方法/纠正方法吗？

Answer 1

您只能在模式匹配中使用构造函数。 nat的构造函数是0和Suc。因此，如果您将1编写为(Suc 0)，则应该可以使用。