Isabelle：能否一次性执行多条erule_tac allE规则以实例化全称量词？

针对你提出的一次性执行多条erule_tac x=... in allE的需求，有几种直接的解决方式，能避免拆分操作带来的量词顺序调整问题：

1. 单条erule_tac绑定多个变量 #

最直接的方式是在erule_tac中用and连接多个变量的赋值，一次性匹配外层的多层全称量词：

lemma "forall x y. P x y ==> P a b"
  apply (erule_tac x=a and y=b in allE)
  done

这种写法会直接消解两层全称量词，全程保持量词的原始顺序，无需分步操作。

2. 借助规则组合的结构化证明（Isar风格） #

如果偏好Isar结构化证明，可以通过直接组合allE规则完成，同样是一次性消解：

lemma "∀x y. P x y ⟹ P a b"
proof -
  assume hyp: "∀x y. P x y"
  from hyp have "P a b" by (rule allE[of _ a], rule allE[of _ b])
  show ?thesis .
qed

3. 自动化策略快速完成 #

如果不需要手动控制变量绑定细节，也可以用自动化策略直接完成证明：

lemma "forall x y. P x y ==> P a b"
  apply fastforce
  done

需要注意的是，使用多变量绑定的erule_tac时，变量赋值的顺序要和原假设中全称量词的顺序对应，这样就能确保消解过程不会打乱量词结构。

内容的提问来源于stack exchange，提问作者Mathieu Paturel