This is an old revision of the document!
Table of Contents
rule (method)
rule is a proof method. It applies a rule if possible.
Definition
Assume we have a subgoal
$\quad\bigwedge x_1 \dots x_k : [|\ A_1; \dots ; A_m\ |] \Longrightarrow C$
and we want to use rule with rule
$\quad[|\ P_1; \dots ; P_n\ |] \Longrightarrow Q$
Then, rule does the following:
- Unify $C$ and $Q$. The application fails if there is no unifier; otherwise, let $U$ be this unifier.
- Remove the old subgoal and create one new subgoal
$\quad\bigwedge x_1 \dots x_k : [|\ U(A_1); \dots ; U(A_m)\ |] \Longrightarrow U(P_k)$
for each $k = 1, \dots, n$.
Example
Non-Example
Variants
rule_tac
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.
rule(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 rule(k) which forces Isabelle to apply assumption $k$ times after the rule application.