proof - 未能细化任何待定目标

Question

我正在尝试证明 Isabelle 中的定理，但我陷入了这一步:

theorem exists_prime_factor: " (n > Suc 0) ⟶ (∃xs::nat list. prod_list xs = n ∧ all_prime xs)"
proof (induct n rule: less_induct)
    case (less k)
    assume HI: "⋀y::nat. (y < k ⟹ Suc 0 < y ⟶ (∃xs. prod_list xs = y ∧ all_prime xs))"
    then show ?case
    proof -
      show "(Suc 0 < k) ⟶ (∃xs. prod_list xs = k ∧ all_prime xs)"
        proof -     
          assume "Suc 0 < k" then show "(∃xs. prod_list xs = k ∧ all_prime xs)" sorry

在最后一个目标中，我需要证明一个含义。像往常一样，我假设前提并尝试展示结论。然而，当我写最后一行时，我得到“无法完善任何待定目标”。是因为我之前应用的归纳原理吗？因为如果没有这种归纳，我就可以像往常一样使用蕴涵引入规则(假设前提然后得出结论)。

有人知道会发生什么吗？

非常感谢。

Answer 1

“问题”确实与证明有关。该声明打开了一个新的子证明，而不对目标应用任何证明方法。如果您编写的 proof 没有 -，则将隐式应用证明方法 rule，这在这种情况下可以发挥作用。

证明规则选择最直接的规则来应用于您的目标。在这种情况下，这相当于proof (rule impI)，因为您要证明的对象级语句的形式为“a --> b”。 impI 是蕴涵的引入规则。它允许您将 "a --> b" 形式的对象级含义提升为元逻辑 "a"==> "b"。

您的目标需要采用"a"==> "b" 形式，才能继续采用assume "a"[...] show "b 形式的子证明“。