Isabelle应用dec_induct规则生成非预期子目标的问题咨询

子目标不符合预期的核心原因 #

你遇到的问题本质是高阶逻辑合一的歧义导致的：
dec_induct规则的结论是?P ?j，你当前要证明的目标是P a，Isabelle的通用合一算法在匹配这两个命题时，存在两种合法的合一方案：

1. 你预期的方案：将模式变量?P实例化为谓词P，?j实例化为项a
2. 更通用的退化方案：将模式变量?P实例化为常值函数λ_. P a，此时?P作用在任意参数上的结果都是P a，?j完全没有被约束

rule是通用的规则应用方法，不会主动猜测你的证明意图，默认会选择后者完成合一，因此所有?P相关的位置都被替换为P a，?j仍为自由变量，最终得到你看到的三个无效子目标。

让规则按预期工作的方法 #

你只需要在应用规则时手动指定需要绑定的模式变量，消除合一歧义即可，写法如下：

proof (rule dec_induct[where ?j = a and ?P = P])

该写法强制将?j绑定到你的目标参数a，?P绑定到目标谓词P，合一就会按照你预期的逻辑执行，最终生成你想要的三个子目标。
如果你想简化写法，也可以只绑定?j，此时合一算法会自动推导出?P的正确实例：

proof (rule dec_induct[where ?j = a])

补充说明 #

induct方法不会出现该问题，是因为它是专门针对归纳规则设计的专用方法，会自动分析目标的结构，选择正确的合一实例，不需要手动消除歧义。而rule作为底层通用方法，只会执行最基础的合一操作，遇到高阶合一场景时需要你提供足够的约束信息。

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