伊莎贝尔在处理两个理论文件时“无法应用证明方法”

问题描述

我有我在 Isabelle src/HOL 中复制的理论文件 Test_Func.thy，它定义了函数 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 发行版中（相反，我最好保持原样，以确保您的开发可以在其他机器上使用，而无需触及 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。