frule is a proof method. It applies a rule if possible.
Assume we have a subgoal
and we want to use
frule with rule
frule does the following:
frule is almost the same as
drule. 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. However,
frule tends to clutter your assumption set unnecessarily if is no longer needed.
Assume we have the goal
apply (drule mp) yields new goals
which can both be solved by
Assumption. Note that
apply (frule(2) mp) is a shortcut for this and immediately solves the goal.
frule_tac, you can force schematic variables in the used rule to take specific values. The extended syntax is:
apply (frule_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
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
frule(k) which forces Isabelle to apply
assumption times after the rule application.