User Tools

Site Tools


reference:drule

This is an old revision of the document!


drule

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

Definition

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 .

Example

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.

Non-Example

Variants

drule_tac

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.

drule(k)

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.

Relatives

reference/drule.1308738573.txt.gz · Last modified: 2011/06/22 12:29 by 131.246.161.187