equal
deleted
inserted
replaced
19 |
19 |
20 |
20 |
21 \section{Substitution rules} |
21 \section{Substitution rules} |
22 \index{substitution!rules}\index{*subst theorem} |
22 \index{substitution!rules}\index{*subst theorem} |
23 Many logics include a substitution rule of the form |
23 Many logics include a substitution rule of the form |
24 $$ \List{\Var{a}=\Var{b}; \Var{P}(\Var{a})} \Imp |
24 $$ |
25 \Var{P}(\Var{b}) \eqno(subst)$$ |
25 \List{\Var{a}=\Var{b}; \Var{P}(\Var{a})} \Imp |
|
26 \Var{P}(\Var{b}) \eqno(subst) |
|
27 $$ |
26 In backward proof, this may seem difficult to use: the conclusion |
28 In backward proof, this may seem difficult to use: the conclusion |
27 $\Var{P}(\Var{b})$ admits far too many unifiers. But, if the theorem {\tt |
29 $\Var{P}(\Var{b})$ admits far too many unifiers. But, if the theorem {\tt |
28 eqth} asserts $t=u$, then \hbox{\tt eqth RS subst} is the derived rule |
30 eqth} asserts $t=u$, then \hbox{\tt eqth RS subst} is the derived rule |
29 \[ \Var{P}(t) \Imp \Var{P}(u). \] |
31 \[ \Var{P}(t) \Imp \Var{P}(u). \] |
30 Provided $u$ is not an unknown, resolution with this rule is |
32 Provided $u$ is not an unknown, resolution with this rule is |
40 subgoal~$i$, use |
42 subgoal~$i$, use |
41 \begin{ttbox} |
43 \begin{ttbox} |
42 resolve_tac [eqth RS ssubst] \(i\){\it,} |
44 resolve_tac [eqth RS ssubst] \(i\){\it,} |
43 \end{ttbox} |
45 \end{ttbox} |
44 where \tdxbold{ssubst} is the `swapped' substitution rule |
46 where \tdxbold{ssubst} is the `swapped' substitution rule |
45 $$ \List{\Var{a}=\Var{b}; \Var{P}(\Var{b})} \Imp |
47 $$ |
46 \Var{P}(\Var{a}). \eqno(ssubst)$$ |
48 \List{\Var{a}=\Var{b}; \Var{P}(\Var{b})} \Imp |
|
49 \Var{P}(\Var{a}). \eqno(ssubst) |
|
50 $$ |
47 If \tdx{sym} denotes the symmetry rule |
51 If \tdx{sym} denotes the symmetry rule |
48 \(\Var{a}=\Var{b}\Imp\Var{b}=\Var{a}\), then {\tt ssubst} is just |
52 \(\Var{a}=\Var{b}\Imp\Var{b}=\Var{a}\), then {\tt ssubst} is just |
49 \hbox{\tt sym RS subst}. Many logics with equality include the rules {\tt |
53 \hbox{\tt sym RS subst}. Many logics with equality include the rules {\tt |
50 subst} and {\tt ssubst}, as well as {\tt refl}, {\tt sym} and {\tt trans} |
54 subst} and {\tt ssubst}, as well as {\tt refl}, {\tt sym} and {\tt trans} |
51 (for the usual equality laws). Examples include {\tt FOL} and {\tt HOL}, |
55 (for the usual equality laws). Examples include {\tt FOL} and {\tt HOL}, |
55 To replace $u$ by~$t$ or $t$ by~$u$ in subgoal~$i$, use |
59 To replace $u$ by~$t$ or $t$ by~$u$ in subgoal~$i$, use |
56 \begin{ttbox} |
60 \begin{ttbox} |
57 eresolve_tac [subst] \(i\) {\rm or} eresolve_tac [ssubst] \(i\){\it.} |
61 eresolve_tac [subst] \(i\) {\rm or} eresolve_tac [ssubst] \(i\){\it.} |
58 \end{ttbox} |
62 \end{ttbox} |
59 |
63 |
60 Logics HOL, FOL and ZF define the tactic \ttindexbold{stac} by |
64 Logics \HOL, {\FOL} and {\ZF} define the tactic \ttindexbold{stac} by |
61 \begin{ttbox} |
65 \begin{ttbox} |
62 fun stac eqth = CHANGED o rtac (eqth RS ssubst); |
66 fun stac eqth = CHANGED o rtac (eqth RS ssubst); |
63 \end{ttbox} |
67 \end{ttbox} |
64 Now {\tt stac~eqth} is like {\tt resolve_tac [eqth RS ssubst]} but with the |
68 Now {\tt stac~eqth} is like {\tt resolve_tac [eqth RS ssubst]} but with the |
65 valuable property of failing if the substitution has no effect. |
69 valuable property of failing if the substitution has no effect. |