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

问题描述

说我想证明Isabelle/Isar中的引理∃ n m k . [n, m, k] = [2, 3, 5].如果我按照第45页Isabelle/HOL教程中的建议进行操作，我的证明如下所示:

Say I want to prove the lemma ∃ n m k . [n, m, k] = [2, 3, 5] in Isabelle/Isar. If I go ahead as suggested in the Isabelle/HOL tutorial on page 45, my proof looks as follows:

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

当然，这太冗长了.我该如何证明上述命题，以使证明简洁明了?

Of course, this is way too verbose. How can I prove propositions like the above one such that the proofs are concise and readable?

推荐答案

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

Multiple existential quantifiers can be introduced in a single step by applying the single-quantifier introduction rule several times. For example, the proof method (rule exI)+ introduces all outermost existential quantifiers.

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

或者，您可以先声明实例化的属性，然后使用自动证明方法进行实例化.通常blast在这里可以很好地工作，因为它不会调用简化程序.在您的示例中，由于数字超载，您将不得不添加类型注释.

Alternatively, you can first state the instantiated property and then use an automatic proof method to do the instantiations. Usually blast works well here because it does not invoke the simplfier. In your example, you will have to add type annotations because numbers are overloaded.

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

这篇关于如何在Isabelle/Isar中有效地证明具有多个变量的存在命题?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！