如何在 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 的值可能具有的不同情况，然后使用简化器（结合函数定义期间命令 fun 提供的简化规则）来完成证明。您可以通过在 replace 的指定后立即键入 print_theorems 来查看命令 fun 生成的所有定理，例如

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

print_theorems

当然，还有其他方法可以证明你要证明的结果。提高找到此类证明的能力的一种好方法是阅读有关 Isabelle 的文档和教程。我自己学习伊莎贝尔的起点是 "Concrete Semantics" Tobias Nipkow 和 Gerwin Klein 的书。

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

How to prove this simple theorem in Isabelle?

formal-verification

isabelle