Isabelle中如何在apply风格证明内正确使用using语句？

问题根源 #

你遇到的Undefined fact: "Cons.IH"报错，核心原因是Cons.IH是Isar风格下执行proof (induction xs)进入Cons分支后，系统自动生成的归纳假设事实。你之前将归纳步骤单独拆成独立lemma时，没有执行归纳流程，上下文里根本没有这个事实，自然调用失败。

正确的apply风格完整证明 #

完整的目标lemma不需要拆分，直接按归纳+分支讨论的逻辑写apply链即可，此时归纳假设会自动进入上下文供auto调用：

lemma "map f (intersperse a xs) = intersperse (f a) (map f xs)"
  apply (induction xs)
   apply simp (* 处理空表基例 *)
  apply (cases xs) (* 对Cons分支的剩余列表做 case 拆分 *)
   apply simp (* 剩余列表为空的分支 *)
  apply auto (* 剩余列表非空的分支，自动匹配归纳假设完成证明 *)
done

单独测试归纳步骤的写法 #

如果你确实需要单独验证归纳步骤的推导，可以手动将归纳假设作为前提写入lemma，替代自动生成的Cons.IH：

lemma 
  assumes IH: "map f (intersperse a xs) = intersperse (f a) (map f xs)"
  shows "map f (intersperse a (x # xs)) = intersperse (f a) (map f (x # xs))"
  apply (cases xs)
   apply simp
  apply (auto simp add: IH)
done

apply风格引入事实的通用语法 #

你问的using语句对应apply风格的用法，常用有两种：

• 事实可以直接放在apply命令前，作为上下文传入：using 事实名 apply (证明方法)
• 也可以作为证明方法的参数传入：apply (证明方法 规则参数: 事实名)，比如simp add: 事实名、auto intro: 事实名等。

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