Isabelle中如何引用所有由assume关键字创建的当前假设？
2026-10-22
解决方案
Isabelle 目前没有内置和顶层assms完全对等、直接指代当前子证明所有assume假设的关键字，但有三种社区普遍使用的成熟方案可以消除冗余命名：
方案1：通配符统一绑定（最常用轻量方案）
你可以把同一子证明内所有assume的假设都绑定到同一个无意义通配符名称（通常用*），后续直接用该名称调用所有假设，完全不需要为单个假设分配有意义的名称：
lemma foo: ... proof assume *: ... and ... and ... then have ... then have ... using * ... then have ... using * ... then show ... proof assume *: ... and ... and ... then have ... then have ... using * ... ... qed
同一子证明内多次用*绑定assume时，新的假设会自动追加到*对应的事实集合中，不会互相覆盖。
方案2：自定义局部假设集合
如果你的证明层级较多、需要区分不同层级的假设，可以用named_theorems自定义专属的局部假设集合：
lemma foo: ... proof named_theorems local_assms "当前子证明局部假设" assume [local_assms]: ... and [local_assms]: ... and [local_assms]: ... then have ... then have ... using local_assms ... then have ... using local_assms ... ... qed
方案3：自动化方法隐式调用
如果你的证明步骤不需要显式指定假设，assumption、blast、auto、simp_all等内置方法默认会自动遍历所有当前局部假设进行推理，不需要你通过using手动引入：
lemma foo: "P ⟹ Q ⟹ P" proof assume P and Q (* 直接用assumption方法自动匹配假设P完成证明，不需要引用名称 *) then show ?thesis by assumption qed
内容的提问来源于stack exchange，提问作者Luiz Martins
相关产品推荐
相关产品推荐
