isabelle - 如何在 Isabelle 中证明这个简单的定理？

Question

我定义了一个非常简单的函数 replace将 1 替换为 0，同时保留其他输入值。我想证明函数的输出不能为1。如何实现？

这是代码。

theory Question
  imports Main
begin
fun replace :: "nat ⇒ nat" where
"replace (Suc 0) = 0" |
"replace x = x"

theorem no1: "replace x ≠ (Suc 0)"
  sorry
end

谢谢!

Answer 1

有几种方法可以证明您要证明的陈述。

您可以尝试使用 sledgehammer自动找到证明，例如

theorem no1: "replace x ≠ (Suc 0)"
  by sledgehammer
  (*using replace.elims by blast*)

一旦找到证明，就可以删除命令sledgehammer的显式调用。 .

也许，一种更好的方式来说明 sledgehammer 发现的证明将是

theorem no1': "replace x ≠ (Suc 0)"
  by (auto elim: replace.elims)

您也可以尝试提供更专业的证明。例如，

theorem no1: "replace x ≠ (Suc 0)"
  by (cases x rule: replace.cases) simp_all

这个证明着眼于不同情况下 x 的值可以有，然后使用 simplifier(结合函数定义期间命令 fun 提供的 simp 规则)来完成证明。您可以看到命令 fun 生成的所有定理通过输入 print_theorems紧接在 replace 的规范之后，例如

fun replace :: "nat ⇒ nat" where
  "replace (Suc 0) = 0" |
  "replace x = x"

print_theorems 

当然，还有其他方法可以证明您要证明的结果。提高找到此类证明的能力的一种好方法是阅读 Isabelle 上的文档和教程。我自己学习伊莎贝尔的起点是这本书 "Concrete Semantics"作者:托比亚斯·尼普科夫 (Tobias Nipkow) 和格温·克莱因 (Gerwin Klein)。