User Tools

Site Tools


This is an old revision of the document!

rule (method)

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