0

我有理论文件 Test_Func.thy，我在 Isabelle src/HOL 中复制了它，它定义了函数 add_123：

theory Test_Func
  imports Main
begin

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

end

然后我有 Test_1.thy 文件，其中包含导入和引理：

theory Test_1
imports Main "HOL.Test_Func" 
begin
lemma add_02: "add_123 m 0 = m"
  apply(simp)
  done

end

奇怪的是，apply(simp)还是apply(auto)失败了Failed to apply proof method。没有关于未定义函数或不可见函数的错误消息，但是当函数定义和关于它的引理被分成两个文件时，这种简单的证明不起作用。

所以 - 这个问题可能有不同的问题和不同的解决方案 - 也许是因为我没有导入理论文件的经验，或者我对战术选择和应用感到困惑。

我在 Isabelle 2021 的 jEdit 中观察到这一点，但在不同的设置中，我可以看到 Isabelle 2020 也发生了同样的事情。

4

1 回答 1

1

不需要将理论文件放入 Isabelle 发行版中（相反，我最好保持原样，以确保您的开发可以在其他机器上使用而无需接触 Isabelle 安装）。

证明失败的问题在于不同的领域： 的定义add_123对第一个参数是归纳的，并且没有直接规则如何处理 中指定的表达式lemma_02。（例如，lemma add_01: "add_123 0 m = m"可以证明您使用的方式，因为它匹配定义中指定的第一个案例。）

解决方案是对第一个参数使用归纳证明：

apply (induction m)
apply simp_all
done

或者，简而言之by (induction m) simp_all。

于 2021-05-06T06:33:49.843 回答