reference:rule_method

**This is an old revision of the document!**

`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 .

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`

.

reference/rule_method.1308736782.txt.gz · Last modified: 2011/06/22 11:59 by 131.246.161.187