一次实例化多个口头量词

Question

有没有办法一次做多个

apply (erule_tac x=... in allE)

？有时，当我的假设中有多个

forall

时，Isabelle 会在

erule_tac

之后对它们重新排序，这使得证明非常烦人。

例如。

lemma "forall x y. P x y ==> P a b"
  apply (erule_tac x=a in allE)
  apply (erule_tac x=b in allE) (* how can I do these two rules in one rule *)?
  done

Answer 1

对于具体问题，

allE

只有一个

x

，所以你不能同时进行多个实例化。 方法是手动引入

lemma all2E: ‹∀x y. P x y ⟹ (P x y ⟹ R) ⟹ R› by blast

。 然后，您可以在证明中写下

apply (erule_tac x=a and y=b in all2E)

。 （或者，有一个 HOL 引理

spec2

接近我们在这种情况下需要的。）

通常，在证明步骤中实例化多个变量的便捷且稳定的方法是在事实上使用

[of ...]

修饰符属性而不是

rule_tac

。 在这种情况下，这将显示为

apply (erule all2E[of _ a b])

。 （在最小的例子中，也可以省略实例化。Isabelle 会找到它们来完成证明。）

为了更清晰的证明，我通常更喜欢命名我的假设和事实，并在它们上实例化变量（而不是在上面的规则上）。 在此示例中，将显示为：

lemma
  assumes P_univ: ‹∀ x y. P x y›
  shows ‹P a b›
  using P_univ[rule_format, of a b] .

（需要

[rule_format]

将

x,y

转为元变量，可以在外层实例化。）