我如何有效证明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