如何在 Isabelle/Isar 中有效地证明具有多个变量的存在命题？

Question

假设我想在 Isabelle/Isar 中证明引理 ∃ n m k . [n, m, k] = [2, 3, 5]。如果我按照第 45 页的 Isabelle/HOL 教程中的建议继续，我的证明如下所示：

lemma "∃ n m k . [n, m, k] = [2, 3, 5]"
proof
  show "∃ m k . [2, m, k] = [2, 3, 5]"
  proof
    show "∃ k . [2, 3, k] = [2, 3, 5]"
    proof
      show "[2, 3, 5] = [2, 3, 5]" by simp
    qed
  qed
qed

当然，这太冗长了。如何证明上述命题，使证明简洁易读？

Answer 1

通过多次应用单量词引入规则，可以在一个步骤中引入多个存在量词。例如，证明方法(rule exI)+ 引入了所有最外层的存在量词。

lemma "∃n m k. [n, m, k] = [2, 3, 5]"
proof(rule exI)+
  show "[2, 3, 5] = [2, 3, 5]" by simp
qed

或者，您可以先声明实例化的属性，然后使用自动证明方法进行实例化。通常blast 在这里工作得很好，因为它不会调用简化器。在您的示例中，您必须添加类型注释，因为数字已重载。

lemma "∃n m k :: nat. [n, m, k] = [2, 3, 5]"
proof -
  have "[2, 3, 5 :: nat] = [2, 3, 5]" by simp
  then show ?thesis by blast
qed