isabelle - 如何在假设中用 ∀ 和 ⟶ 替换 ⋀ 和 ⟹

Question

我是 Isabelle 新手，我对 ⋀ 和 ∀ 之间以及 ⟹ 和 ⟶ 之间的关系有点(实际上，很多)感到困惑。

我有以下目标(这是我最终在真实证明中得到的东西的高度简化版本):

⟦⋀x. P x ⟹ P z; P y⟧ ⟹ P z

我想通过将 x 与 y 特化得到 ⟦P y ⟹ P z 来证明这一点； P y⟧ ⟹ P z，然后使用 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 **] .