允许替换普遍量化变量的引理/规则 (Isabelle)

【问题标题】：Lemma/rule to allow substitution in universally quantified variable (Isabelle)允许替换普遍量化变量的引理/规则 (Isabelle)
【发布时间】：2016-11-22 16:08:05
【问题描述】：

我有一个类似于"\<forall>x. \<exists>y.\<forall>(z::real). P x y z" 的目标。是否有一条规则可以立即让我得出结论"\<forall>x. \<exists>y.\<forall>(z::real). P x y (z-2)"？如果没有，我将不胜感激有关如何证明此类目标的一般建议。

我知道我可以通过大量使用allI、exI、allE、exE 来证明这一点，但似乎必须有一个快速简单的方法。

【问题讨论】：

标签： isabelle quantifiers

【解决方案1】：

Isabelle2016-1-RC2 中的以下作品：

lemma
  assumes "∀x. ∃y.∀(z::real). P x y z"
  shows "∀x. ∃y.∀(z::real). P x y (z-2)"
using assms by force

您可以使用try0 命令为您提供能够解决目标的证明方法列表。

【讨论】：

这很有帮助。不幸的是，我真正想证明的事情稍微复杂一些，并且无法使用它。
您可以尝试一个接一个地剥离量词，只做最少的工作来帮助自动化。