如何在假设中用∀和replace代替⋀和.

Question

我是一个Isabelle新手,我对⋀和∀之间以及⟹和between之间的关系感到困惑(实际上,很多).

我有以下目标(这是一个高度简化的版本,我最终得到了一个真实的证明):

??x. P x ? P z; P y? ? P z

我想通过专业化x与y得到⟦Py⟹Pz来证明; Py⟧⟧Pz,然后使用modus ponens.这有助于证明非常相似:

??x. P x ? P z; P y? ? P z

但我无法让它为上述目标而努力.

有没有办法将前一个目标转变为后者？如果没有,这是因为它们在逻辑上是不同的陈述,在这种情况下有人可以帮我理解差异吗？

Answer 1

通过以下证明可以显示这两个前提!!x. P x ==> P y和ALL x. P x --> P y逻辑上等同

lemma
  "(?x. P x ? P y) ? (Trueprop (?x. P x ? P y))"
  by (simp add: atomize_imp atomize_all)

当我为你的示例证明尝试相同的推理时,我遇到了一个问题.我打算做以下证明

lemma
  "??x. P x ? P z; P y? ? P z"
apply (subst (asm) atomize_imp)
apply (unfold atomize_all)
apply (drule spec [of _ y])
apply (erule rev_mp)
apply assumption
done

但是unfold atomize_all我得到了

Failed to apply proof method:

当尝试显式实例化引理时,我得到一个更明确的错误消息,即

apply (unfold atomize_all [of "?x. P x ? P z"])

产量

Type unification failed: Variable 'a::{} not of sort type

我发现这很奇怪,因为据我所知,每个类型变量应该是排序的type.我们可以通过添加显式排序约束来解决此问题:

lemma
  "??x::_::type. P x ? P z; P y? ? P z"

然后证明工作如上所示.

长话短说.我通常使用Isar结构化证明而不是apply脚本.然后经常避免这些问题.对于你的陈述我实际上会这样做

lemma
  "??x. P x ? P z; P y? ? P z"
proof -
  assume *: "?x. P x ? P z"
    and **: "P y"
  from * [OF **] show ?thesis .
qed

或许更惯用

lemma
  assumes *: "?x. P x ? P z"
    and **: "P y"
  shows "P z"
  using * [OF **] .