Isabelle/HOL Support Wiki

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

Assume we have a subgoal

$\quad\bigwedge x_1 \dots x_k : [|\ A_1; \dots ; A_m\ |] \Longrightarrow C$

and we want to use frule with rule

$\quad[|\ P_1; \dots ; P_n\ |] \Longrightarrow Q$

Then, frule does the following:

• Unify $P_1$ and $A_j$ for some $j$. The application fails if there is no unifier for any $j$; otherwise, let $U$ be this unifier.
• Remove the old subgoal and create new ones:
  • $\quad\bigwedge x_1 \dots x_k : [|\ U(A_1); \dots ; U(A_m)\ ; U(Q) |] \Longrightarrow U(C)$
  • $\quad\bigwedge x_1 \dots x_k : [|\ U(A_1); \dots ; U(A_m)\ |] \Longrightarrow U(P_k)$
    for each $k = 2, \dots, n$.

Note that frule is almost the same as drule. The only difference is that frule keeps the assumption “used” by the used rule $A_j$ while drule drops it. This is useful if $A_j$ is needed to prove the new subgoals; drule is unsafe because of this. However, frule tends to clutter your assumption set unnecessarily if $A_j$ is no longer needed.

Assume we have the goal

$\quad[|\ A \longrightarrow B; A\ |] \Longrightarrow B$

Applying apply (drule mp) yields new goals

$\quad [|\ A \longrightarrow B; A\ |] \Longrightarrow A$

$\quad[|\ A \longrightarrow B; A; B\ |] \Longrightarrow B$

which can both be solved by Assumption. Note that apply (frule(2) mp) is a shortcut for this and immediately solves the goal.

With 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 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 frule(k) which forces Isabelle to apply assumption $k$ times after the rule application.

• Rule
• drule
• erule