允许替换普遍量化变量的引理/规则 (Isabelle)
Posted
技术标签:
【中文标题】允许替换普遍量化变量的引理/规则 (Isabelle)【英文标题】:Lemma/rule to allow substitution in universally quantified variable (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
来证明这一点,但似乎必须有一个快速简单的方法。
【问题讨论】:
【参考方案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
命令为您提供能够解决目标的证明方法列表。
【讨论】:
这很有帮助。不幸的是,我真正想证明的事情稍微复杂一些,并且无法使用它。 您可以尝试一个接一个地剥离量词,只做最少的工作来帮助自动化。以上是关于允许替换普遍量化变量的引理/规则 (Isabelle)的主要内容,如果未能解决你的问题,请参考以下文章