格式错误的定义：顺序模式中不允许使用非线性模式

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。这是一个非常强大且用途广泛的工具，但如果您仅凭“乐趣”就能获得想要的东西，那通常就是您想要的方式。

格式错误的定义：顺序模式中不允许使用非线性模式

Malformed definition: Nonlinear patterns not allowed in sequential mode

isabelle