Table of Contents

`drule`

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

Assume we have a subgoal

and we want to use `drule`

with rule

Then, `drule`

does the following:

- Unify and 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 .

Note that `drule`

is almost the same as `frule`

. The only difference is that `frule`

keeps the assumption “used” by the used rule while `drule`

drops it. This is useful if is needed to prove the new subgoals; `drule`

is unsafe because of this.

Assume we have the goal

Applying `apply (drule mp)`

yields new goals

which can both be solved by `Assumption`

. Note that `apply (drule(2) mp)`

is a shortcut for this and immediately solves the goal.

With `drule_tac`

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

apply (drule_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 `drule(k)`

which forces Isabelle to apply `assumption`

times after the rule application.