允许替换普遍量化变量的引理/规则 (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)"?如果没有,我将不胜感激有关如何证明此类目标的一般建议。

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

【问题讨论】:

【参考方案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)的主要内容,如果未能解决你的问题,请参考以下文章

如何在 Isabelle 中创建适当的引理来证明这个引理?

如何在 Isabelle/HOL 的引理之外获取见证实例

构建有用的引理

Polya定理与Burnside引理

我们如何使用抽水引理证明这种语言是不规则的?

如何在 terraform 中创建允许/拒绝防火墙规则条件?