Isabelle "Failed to apply proof method" 在处理两个理论文件时
Isabelle "Failed to apply proof method" when working with two theory files
我有理论文件 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 发行版（相反，我最好保持原样，以确保您的开发可以在其他机器上使用而无需触及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。
我有理论文件 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 发行版（相反，我最好保持原样，以确保您的开发可以在其他机器上使用而无需触及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。