Differences

This shows you the differences between two versions of the page.

--- reference:drule [2011/06/22 12:20] – created 131.246.161.187
+++ reference:drule [2011/07/06 12:08] (current) – 131.246.161.187
@@ Line 7: / Line 7: @@
 $\quad\bigwedge x_1 \dots x_k : [|\ A_1; \dots ; A_m\ |] \Longrightarrow C$
-and we want to use ''rule'' with rule
+and we want to use ''drule'' with rule
 $\quad[|\ P_1; \dots ; P_n\ |] \Longrightarrow Q$
@@ Line 14: / Line 14: @@
   * [[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)\ ; 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$.
+    * $\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 ====