量化列表的函数：语法和类型错误 (Isabelle)

Question

我目前正在完成 http://isabelle.in.tum.de/exercises/ 的 'Quantifying Lists' 练习。它要求“使用原始递归在列表上定义一个通用量词和一个存在量词”。表达式@{term "alls P xs"} 应该为真当且仅当 @{term "P x"} 对每个元素 @{term x} 成立 @{term xs}...'

我觉得这个尝试很可信：

primrec alls :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
"alls P x # [] = (if P x then True else False)"
| "alls P x # xs = (if P x then alls P xs else False)"

我想写下我想用数学符号表示的内容：

alls(P,[x]) = { 如果 Px 则为 true 否则为 false

和

alls(P, [x, ...]) = { 如果 Px 则 alls(P,[...]) 否则为假。

但是，Isabelle 说有一个 'type error in unification' 并表明 x 被假定为 'a list 类型。我觉得我没有表达正确的语法，但我不知道应该如何改变它。

Answer 1

为了将 x # foo 视为单个操作数，应将其括在括号中：(x # foo).

然而，这还不是故事的结局：在应用上述修复程序后，您会收到一个错误 Nonprimitive pattern in left-hand side at "alls P [x]" ... 违规模式 x # [] 与单元素列表相匹配。

列表是使用两个构造函数 Nil 和 Cons 定义的，而 primrec 不允许使用非原始构造函数，包括单元素列表（看起来像 Cons x Nil).可以将 primrec 替换为 fun 来避免此错误，但如果您想定义一个总函数，即也处理空列表，则问题会更深。

为了解决这个问题，函数应该有原始构造函数的模式 Nil 和 Cons:

primrec alls :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
  "alls P [] = ..."
| "alls P (x # xs) = (if P x then alls P xs else False)"

... 部分是故意遗漏的，以便您可以用适当的值填充它。

量化列表的函数：语法和类型错误 (Isabelle)

Function for quantifying lists: syntax and type error (Isabelle)

recursion

function

isabelle