Isabelle 在处理两个理论文件时“无法应用证明方法”答案

【问题标题】：Isabelle "Failed to apply proof method" when working with two theory filesIsabelle 在处理两个理论文件时“无法应用证明方法”
【发布时间】：2021-05-05 22:05:25
【问题描述】：

我有理论文件 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 也发生了同样的事情。

【问题讨论】：

标签： isabelle isar

【解决方案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。

【讨论】：