伊莎贝尔的双重功能

Question

我尝试通过 this 教程来学习 Isabelle/HOL。我对双重功能的练习有疑问。我是这样定义的：

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

但是当试图证明 double m = 在我的定理中添加 m m 时：

theorem add_d [simp] : "double x = add x x"
apply(induction x)
apply(auto)
done

apply(auto) 永远不会被评估（它的背景是粉红色的（？））。同样的练习要求证明 add 的交换性和结合性，这工作正常。我使用 Isabelle2014 和默认 (Jedit) IDE.

Answer 1

在您评论的代码中，许多定理都有 [simp] 属性，告诉伊莎贝尔将它们添加到简单集。然而，其中一些不适合作为重写规则（由 simp 和 auto 使用），因为它们导致可以再次应用相同规则的术语，从而导致无限循环。从简单集中删除有问题的定理就可以了：

theorem add_d: "double x = add x x"
  apply (induction x)
  apply (auto simp del: add_zero)
done

但更好的解决方案是首先避免将此类定理添加到简单集，例如从声明中删除 [simp] 属性：

lemma add_zero: "add x 0 = add 0 x"
  apply (induction x)
  apply (auto)
done

之后 add_d 不需要 simp del 部分。但是可能需要明确告知其他一些定理才能使用此特定规则，例如这个：

theorem add_com: "add x y = add y x"
  apply (induction x)
  apply (auto simp add: add_zero)
done

请注意，与您的代码相比，如果在别处使用 add_com，则再次删除 [simp] 属性以避免循环重写。

Answer 2

虽然 Alexander 关于 simp-rules 的建议很合理，但让我给出一些进一步的评论。

首先，在您对 double 的定义中，我会将 add 0 0 替换为 0。一般建议：相对于复杂的表达式，更喜欢简单的表达式。

其次，Isabelle 的简化器实际上 "smart" 足以处理 AC 重写（即结合律和交换律）而无需循环，即你的两个引理

lemma add_assoc [simp]:
  "add (add x y) z = add x (add y z)"

和

lemma add_commute [simp]:
  "add x y = add y x"

与简单规则一样好（即，您可以保留 [simp] 属性）。您遇到的循环的原因是您的引理

(*BAD*)
lemma add_zero [simp]:
  "add x 0 = add 0 x"

由于在 simpset（Isabelle 行话，表示 simp 和 auto 等方法使用的所有简化规则集）允许对于无限推导：

add 0 0 = add 0 0 = add 0 0 = ...

我建议将其替换为

lemma add_zero [simp]:
  "add x 0 = x"

那么你所有的证明（前提是它们以正确的顺序陈述）在某种意义上应该是"automatic"

apply (induction ...)
apply auto
done

可以简写为

by (induction ...) (auto)

Double function in Isabelle