Table of Contents

`erule`

is a proof method. It applies a rule if possible.

Assume we have a subgoal

and we want to use `erule`

with rule

Then, `erule`

does the following:

- Unify with and with simultaneously for some . The application fails if there is no unifier for any ; otherwise, let be this unifier.
- Remove the old subgoal and create new ones

for each .

Assume we have the goal

Applying `apply (erule conjE)`

yields the new goal

which can be solved by `Assumption`

. Note that `apply (erule(1) conjE)`

is a shortcut for this and immediately solves the goal.

With `erule_tac`

, you can force schematic variables in the used rule to take specific values. The extended syntax is:

apply (erule_tac ident1="expr1" and ident2="expr1" and ... in rule)

This means that the variables `?ident1`

is replaced by expression `expr1`

and similarly for the others. Note that you have to leave out the question mark marking schematic variables. Find out which variables a rule uses with `thm rule`

.

Oftentimes, a rule application results in several subgoals that can directly be solved by `Assumption`

; see above for an example. Instead of applying `assumption`

by hand, you can apply `erule(k)`

which forces Isabelle to apply `assumption`

times after the rule application.