0

我已经与 Isabelle/HOL 合作了几个月，但我一直无法弄清楚使用_tac的确切意图。

具体来说，我说的是case与case_tac和induct与indut_tac （尽管一般来说了解tac的含义会很好，因为我也在使用其他方法，例如cut_tac）。

我注意到我不能使用带有 ⋀ 绑定变量的 apply 来使用案例或归纳，但如果它是结构化证明，我可以。为什么？

一个例子：

    lemma "¬(∀x. ¬(P x)) ⟹ ∃x. P x"
  apply (rule ccontr)
  apply (erule notE)
  apply (rule allI)
  apply (case_tac "P x")
  apply (erule notE)
  apply (erule exI)
  apply assumption
  done

另一方面，我注意到 induct 和 induct_tac 之间的另一个区别是我可以对后者使用双重感应，但不能对前者使用。再说一次，我不知道为什么。

提前致谢。

4

1 回答 1

2

*是-scripts_tac中使用的内置策略。apply特别是，case_tac并且induct_tac已基本被Isabelle/Isar 中的cases和证明方法所取代。induction正如您所提到的，case_tac并且induct_tac可以处理 ⋀-bound 变量。然而，这是相当脆弱的，因为它们的名称通常是自动生成的，并且可能会在 Isabelle 更改时更改（当然，您可以使用rename_tac选择固定名称）。这就是如今结构化证明方法优于非结构化策略脚本的原因之一。现在，回到您的示例：为了能够使用cases，您可以按如下方式引入结构化块：

lemma "¬(∀x. ¬(P x)) ⟹ ∃x. P x"
  apply (rule ccontr)
  apply (erule notE)
  proof (intro allI)
    fix x
    assume "∄x. P x"
    then show "¬ P x"
      apply (cases "P x")
      apply (erule notE)
      apply (erule exI)
      apply assumption
      done
  qed

如您所见，结构化证明通常很冗长，但比线性脚本更具可读性apply。

如果您仍然对“双重感应”问题感到好奇，那么非常欢迎举个例子。最后，如果您想了解更多关于使用 Isabelle/Isar 语言环境进行结构化证明的信息，我强烈建议您阅读有关 Isabelle/HOL 的教程和The Isabelle/Isar 参考手册以获取更多详细信息。

于 2021-06-06T00:55:47.380 回答