如何在Isabelle中完全控制替换操作并消除统一歧义？

一、替换命令的核心差异与稳定用法 #

• apply(subst xx)：基于定理/前提xx执行正向替换，默认匹配目标中最左侧的可替换项，歧义场景下需额外指定约束
• apply(rule subst)：调用基础替换规则subst: "s = t ⟹ P s ⟹ P t"，需手动匹配上下文，适合复杂替换但需精确控制
• apply(subst_tac xx)：战术级别的实例化替换，支持通过显式变量绑定实现精细控制

二、消歧义与精准指定的实用技巧 #

1. 指定替换位置：通过subst xx at n（n为目标中的匹配项位置）明确替换目标，例如subst eq_thm at 3会替换目标中第3个符合eq_thm的项
2. 显式绑定变量：使用subst_tac [P="λx. ...", s="a", t="b"] xx直接绑定规则中的自由变量，彻底消除项统一的歧义
3. 选择特定等式来源：
   • 若要使用前提中的某个等式，用subst (asm) eq_name
   • 若要使用已证明的定理，用subst (thm) eq_name

三、arg_cong的erule_tac正确调用方式 #

你定义的arg_cong规则为：

lemma arg_cong: "x = y ⟹ f x = f y"
  by (iprover intro: refl elim: subst)

使用erule_tac时必须显式绑定高阶变量f以及等式两侧的x和y，正确格式如下：

apply(erule_tac f="λz. <你的函数表达式>" and x="<左匹配项>" and y="<右匹配项>" in arg_cong)

示例：若目标为g c = g d且前提存在c = d，可执行：

apply(erule_tac f="λz. g z" and x="c" and y="d" in arg_cong)

你遇到的Failed to apply proof method错误，本质是变量实例化不匹配——要么f未绑定到正确的高阶函数，要么x/y与前提中的等式无法统一。

推荐学习资料 #

• 《Programming and Proving in Isabelle/HOL》：官方实战导向教程，包含大量替换与项统一的案例
• 《Isabelle/HOL Reference Manual》：搜索subst章节，可获取所有替换战术的参数细节与约束说明
• Isle教程：深入讲解项统一的底层逻辑，帮助理解歧义产生的根源

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