Table of Contents

`rule`

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

Assume we have a subgoal

and we want to use `rule`

with rule

Then, `rule`

does the following:

- Unify and . The application fails if there is no unifier; otherwise, let be this unifier.
- Remove the old subgoal and create one new subgoal

for each .

Assume we have a goal

Applying `apply (rule disjI1)`

yields the new subgoal

which can obviously be solved by one application of `Assumption`

. Note that `apply (rule(1) disjI)`

is a shortcut for this and immediately solves the goal.

With `rule_tac`

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

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

This means that the variable `?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 `rule(k)`

which forces Isabelle to apply `assumption`

times after the rule application.