isabelle - 为什么我不能在 Isabelle 中定义 nat ？

Question

我正在关注 tutorial for Isabelle ，并输入第 2.2.2 节中的以下示例:

theory FailedBasicAdditionProof
  imports Main
begin

datatype nat = 0 | Suc nat

fun add :: "nat ⇒ nat ⇒ nat" where
"add 0 n = n" |
"add (Suc m) n = Suc(add m n)"

lemma add_02: "add m 0 = m"
apply(induction m)
apply(auto)
  done
end

但出现错误

Legacy feature! Bad name binding: "nat.0"⌂ 
Legacy feature! Bad name binding: "nat.0"⌂ 
Bad name: "nat.0"

我做错了什么？

Answer 1

如果您碰巧查看the datatype docs ，完成了完全相同的示例，只不过使用单词 Zero 而不是数字 0。

如果将 0 替换为 0，该示例应该可以运行。我认为这是一个命名约定，可能是后来更改或添加的。

正确的例子在这里:

theory CorrectBasicAdditionProof
  imports Main
begin

datatype nat = Zero | Suc nat

fun add :: "nat ⇒ nat ⇒ nat" where
"add Zero n = n" |
"add (Suc m) n = Suc(add m n)"

lemma add_02: "add m Zero = m"
apply(induction m)
apply(auto)
  done
end