Isabelle/HOL Support Wiki

This page is read only. You can view the source, but not change it. Ask your administrator if you think this is wrong.
===== drule =====
''drule'' is a proof method. It applies a [[rule (calculus)|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 ''drule'' with rule

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

Then, ''drule'' does the following:
  * [[unification|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_{j-1}); U(A_{j+1}); \dots ; U(A_m)\ ; U(Q) |] \Longrightarrow U(C)$
    * $\quad\bigwedge x_1 \dots x_k : [|\ U(A_1); \dots ; U(A_{j-1}); U(A_{j+1}); \dots ; U(A_m)\ |] \Longrightarrow U(P_k)$ \\ for each $k = 2, \dots, n$.

Note that ''drule'' is almost the same as ''[[frule]]''. 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.

==== Example ====
Assume we have the goal

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

Applying  ''apply (drule mp)'' yields new goals

$\quad A \Longrightarrow A$

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

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 variable|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 [[#Example|above]] for an example. Instead of applying ''assumption'' by hand, you can apply ''drule(k)'' which forces Isabelle to apply ''assumption'' $k$ times after the rule application.

==== Relatives ====
  * ''[[rule]]''
  * ''[[erule]]''
  * ''[[frule]]''
Isabelle/HOL Support Wiki

User Tools

Site Tools

Page Tools
