了解添加方法在Isabelle中的工作原理

Posted 2021-05-01

书籍Concrete Semantics第8页中有一个自定义添加方法。如下代码和证明，该函数的原始名称称为add但我将其重命名为add1以避免内置方法添加Isabelle的问题：

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

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

我没看到该功能如何能够停止，例如：

add1 10 1

add1（Suc 10）1 = Suc（add1 10 1）

add1（Suc 10）1 = Suc（add1 10 1）

...

参数何时会减少为“0 n”，以便模式匹配适用于“add 1 0 n = n”？

答案

简单的解释

详细说明Bergi的评论：如果你使用的是内置的自然数，2基本上只是语法糖，最终相当于Suc (Suc 0)，类似于10等其他数字。每个自然数都是0或Suc something。

您可以将nat视为代数数据类型

datatype nat = 0 | Suc nat

例如， “2”只是一个定义

definition 2 :: nat where "2 = Suc (Suc 0)"

更多关于好奇读者的自然数字

自然数字在系统内部根深蒂固。他们的构造是这样的：你公理地假设存在一些无限类型（即一种带有一些元素a的类型和另外满足f的内射函数∀x. f x ≠ a）。然后，你可以通过重复使用a将自然数字划分为f“可达”的所有数据。这个想法是a是零，f是继承函数Suc。

然后做一些魔术使这种类型的nat表现得好像它被定义为像上面提到的代数数据类型一样。 nat没有直接用datatype命令定义的原因可能是因为该命令需要内部自然数来完成它的构造。

更多关于非常好奇的读者的数字

Isabelle中的数字存在于任何类numeral（必须是一个半群w.r.t.加法和指定元素1）。有一个数据类型num定义为

datatype num = One | Bit0 num | Bit1 num

由于One代表数字1的想法，Bit0在末尾添加了一个零位，而Bit1在末尾添加了一个位。

如果你强迫伊莎贝尔揭示例如数字6，例如通过做

ML ‹
  val _ = @{term "6"} |> dest_comb |> snd |> Syntax.pretty_term @{context} |> Pretty.writeln
›

你会发现数字6表示为num.Bit0 (num.Bit1 num.One)。要将此数据类型转换为实际数字，请执行以下功能：

primrec numeral :: "num ⇒ 'a"
  where
    "numeral One = 1"
  | "numeral (Bit0 n) = numeral n + numeral n"
  | "numeral (Bit1 n) = numeral n + numeral n + 1"

因此，当您在Isabelle中编写6时，在解析之后，这在内部表示为numeral (num.Bit0 (num.Bit1 num.One))。对于自然数，可以使用例如Suc表示法将这种表示重写为eval_nat_numeral表示法。事实集合lemma "6 = Suc (Suc (Suc (Suc (Suc (Suc 0)))))" by (simp add: eval_nat_numeral) ：

qazxswpoi