錯誤：「非構造圖案不允許在順序模式」（伊莎貝爾）

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，並給我一個健全的證明，但我會很驚訝，如果這是必要的

有人可以解釋錯誤消息，並建議一個解決方法/糾正？

2016-08-16 IIM

您只能在模式匹配中使用構造函數。 nat的構造函數是0和Suc。所以，如果你寫1爲(Suc 0)它應該工作。

2016-08-16 15:13:35 peq

謝謝，我遵循你的建議，但現在有'未完成的子目標'。我希望這意味着我需要使用'功能'，而不是 - 雖然我不願意。 – IIM

好吧，我嘗試過'樂趣Sum ::「（nat => nat）=> nat => nat」「Sum f 0 = 0」 | 「Sum f（Suc k）= f k + Sum f k」'這似乎有效！我想它到處都需要「Suc」（現在「基本案例」更有意義）。 – IIM

你有未完成的子目標，因爲你的原始定義沒有終止：'和f 0 = f（0-1）+和f（0-1）= f 0 +和f 0 = ...'。爲0添加案例解決了這個問題。 – peq

回答