为何对引理应用less_induct归纳规则时抛出THM 0异常？

待证明的引理 #

我正在证明下述关于二进制数相加语义的引理：

lemma (in th2) addMeaningF_2: "∀m. m ≤ n ⟹ (m = (len x + len y) ⟹ (evalBinNum_1 (addBinNum x y) = plus (evalBinNum_1 x) (evalBinNum_1 y)))"

执行操作与报错 #

尝试对该引理应用强归纳：apply(induction n rule: less_induct)，抛出如下错误：

exception THM 0 raised (line 755 of "drule.ML"):
  infer_instantiate_types: type ?'a of variable ?a
  cannot be unified with type 'b of term n
  (⋀x. (⋀y. y < x ⟹ ?P y) ⟹ ?P x) ⟹ ?P ?a

补充上下文 #

Locale定义 #

locale th2 = th1 +
  fixes 
    plus :: "'a ⇒ 'a ⇒ 'a"
  assumes
     arith_1: "plus n zero = n"
    and plus_suc: "plus n (suc m) = suc ( plus n m)"

递归函数定义 #

len用于获取二进制数长度，evalBinNum_1用于计算二进制数的值，其中evalBinNum_1的定义如下：

fun (in th2) evalBinNum_1 :: "BinNum ⇒ 'a"
  where 
    "evalBinNum_1 Zero = zero"|
    "evalBinNum_1 One = suc(zero)"|
    "evalBinNum_1 (JoinZero x) = plus (evalBinNum_1 x) (evalBinNum_1 x)"|
    "evalBinNum_1 (JoinOne x) = plus (plus (evalBinNum_1 x) (evalBinNum_1 x)) (suc zero)"

报错原因 #

核心问题是类型不匹配：

• less_induct（强归纳/良基归纳）规则默认要求归纳变量属于带有良基<关系的类型（通常是自然数nat），该规则中的变量类型为?'a。
• 引理里的n属于泛型类型'a（从th2 locale的plus定义和arith_1假设可推导），而'a是未指定具体结构的泛型类型，没有默认的良基小于关系，导致Isabelle无法将less_induct的?'a与引理中n的'a类型统一。
• 额外矛盾点：len函数返回的是二进制数的长度，逻辑上应为自然数类型，但你将其与泛型类型'a的n做≤比较，进一步加剧了类型混淆，触发类型统一失败的异常。

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