isabelle - 定义格式错误 : Nonlinear patterns not allowed in sequential mode

Question

我定义了以下函数:

fun count:: "'a ⇒ 'a list ⇒ nat" where
"count a Nil = 0" |
"count a (Cons b xs) = (count a xs)" |
"count a (Cons a xs) = (count a xs) + (Suc 0)"

它应该计算元素 a 在列表中出现的次数，以及与 a 具有相同类型的元素。我收到以下错误:

Malformed definition:
Nonlinear patterns not allowed in sequential mode.
⋀a xs. count a (a # xs) = count a xs + Suc 0 

Answer 1

就模式而言，“线性”意味着每个自由变量仅出现一次。在第三行中，左侧的模式包含两次 a ，这使其成为非线性的。函数包的“顺序”模式不支持此功能。在这种模式下，您可以依次指定可能重叠的函数方程，并且第一个匹配的函数方程才是重要的。这也是“fun”命令使用的模式，也是 Haskell 等函数式编程语言通常采用的模式(请注意，这些语言通常也不允许非线性模式)。

这里基本上有两种可能性:如果你绝对想使用非线性模式，你可以写

function count:: "'a ⇒ 'a list ⇒ nat" where
  "count a Nil = 0"
| "a ≠ b ⟹ count a (Cons b xs) = (count a xs)"
| "count a (Cons a xs) = (count a xs) + (Suc 0)"
  by (metis neq_Nil_conv surj_pair) auto
termination by lexicographic_order

请注意，您必须手动证明模式是详尽且不重叠的，并且必须终止。 “fun”功能较弱，但会自动完成所有这些事情。

更简单、更好的方法是以更适合系统自动化的方式重新表述您的定义:

fun count:: "'a ⇒ 'a list ⇒ nat" where
  "count a Nil = 0"
| "count a (Cons b xs) = (count a xs) + (if a = b then 1 else 0)‹›

出于多种原因(更短、更容易、更适合代码生成)，这几乎总是更可取的。

有关功能包的更多信息，请参阅documentation 。它是一个非常强大且多功能的工具，但如果您可以仅通过“乐趣”来获得您想要的东西，那么这通常就是您想要的方式。