如何在汽车上添加消去规则？

Question

以下是“具体语义”中的算术表达式(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)。

下面的函数检查表达式是否不包含任何Plus (N n1) (N 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)"

我试图证明以下引理：

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

问题是我必须显式地应用optimal.elims。

我可以将optimal.elims声明为消除规则，然后证明如下：

declare optimal.elims [elim!]

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

但是，是否可以将optimal.elims添加到auto中而不将其声明为消除规则？

以下内容不适用于optimal.elims

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

以下是卡住的地方：

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

我可以将消除规则添加到simp而不是auto中吗？

Answer 1

最后一个变体，即auto elim!:实际上可以工作。但是，通过使用elim!，您将迫使auto假定optimal.elims是安全规则。对于这种特殊情况，显式传递optimal.elims作为消除规则的一个更好的替代方法是fastforce elim:。

关于最后一个问题，simp通常不会使用导入/消除规则，而只适用于简化规则。