有没有办法一次做多个
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
对于具体问题,
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
转为元变量,可以在外层实例化。)