How to add an elimination rule to auto?

Here are arithmetic expressions from the "Concrete Semantics" (section 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 folds Plus (N n1) (N n2) subexpressions to N (n1 + n2).

The following function checks that an expression doesn't contain any 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)"

I'm trying to prove the following lemma:

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

The problem is that I have to apply optimal.elims explicitly.

I can declare optimal.elims as an elimination rule and then the proof reduces to the following:

declare optimal.elims [elim!]

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

But is it possible to add optimal.elims to auto without declaring it as an elimintation rule?

The following doesn't apply optimal.elims:

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

And the following is stuck:

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

Can I add elimination rules to simp instead of auto?

Solution

The last variant, that is, auto elim!: actually works. However, by using elim! you are forcing auto to assume that optimal.elims are safe rules. A better alternative to explicitly pass optimal.elims as elimination rules for this specific case is fastforce elim:.

Regarding your last question, simp will usually not work with introduction/elimination rules but only with simplification rules.