Isabelle中如何为auto添加消除规则且无需全局声明？能否加入simp？

背景定义 #

以下是《Concrete Semantics》第3.1节中的算术表达式及相关函数定义：

算术表达式与常量折叠函数 #

type_synonym vname = string
datatype aexp = N int | V vname | Plus aexp aexp

fun asimp_const :: "aexp ⇒ aexp" where
  "asimp_const (N n) = N n"
| "asimp_const (V x) = V x"
| "asimp_const (Plus a1 a2) =
    (case (asimp_const a1, asimp_const a2)
      of (N n1, N n2) ⇒ N (n1 + n2)
       | (b1, b2) ⇒ Plus b1 b2)"

asimp_const 会将 Plus (N n1) (N n2) 这类子表达式折叠为 N (n1 + n2)，完成常量合并操作。

最优性检查函数 #

fun optimal :: "aexp ⇒ bool" where
  "optimal (N n) = True"
| "optimal (V x) = True"
| "optimal (Plus a1 a2) = (case (a1, a2)
    of (N n1, N n2) ⇒ False
     | (b1, b2) ⇒ optimal b1 ∧ optimal b2)"

optimal 用于检查表达式中是否不存在 Plus (N n1) (N n2) 这类可折叠的常量加法子表达式。

原证明情况 #

要证明引理 optimal (asimp_const a)，初始分步证明需要显式调用消除规则：

lemma "optimal (asimp_const a)"
  apply (induct a)
  apply simp
  apply simp
  by (erule optimal.elims; erule optimal.elims; simp)

若全局声明 optimal.elims 为强制消除规则，证明可简化为：

declare optimal.elims [elim!]

lemma "optimal (asimp_const a)"
  by (induct a; auto)

问题与解答 #

1. 能否在不全局声明的前提下，将 optimal.elims 添加到 auto 中？ #

可以，但需要配合拆分规则使用。因为 optimal 和 asimp_const 的定义中都用到了元组模式匹配（case (a1,a2)），auto 默认不会自动拆分元组结构，导致消除规则无法匹配生效。

正确写法需显式指定元组拆分规则 prod.split，同时将 optimal.elims 作为消除规则传入 auto：

lemma "optimal (asimp_const a)"
  by (induct a; auto elim: optimal.elims split: prod.split)

若使用 auto elim!: optimal.elims 陷入停滞，是因为 elim! 会强制优先应用消除规则，引发不必要的分支遍历。配合 split: prod.split 后，auto 能正确识别元组模式，elim: optimal.elims 即可正常工作，无需全局声明。

2. 能否将消除规则添加到 simp 而非 auto 中？ #

不行。simp 是重写规则集，仅处理等式形式的重写（如 f x = g x），用于简化表达式；而 optimal.elims 是消除规则，本质是对 optimal 谓词做 case 分析的推理规则，作用是消解目标中的断言，两者规则类型和作用机制完全不同，无法将消除规则直接添加到 simp 规则集中。

如果想通过类似 simp 的方式实现效果，可手动编写针对 optimal 的重写规则，但需要覆盖所有 case，不如直接使用消除规则简洁可靠。

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