104

1 
%% $Id$


2 
\chapter{Substitution Tactics} \label{substitution}

323

3 
\index{tactics!substitution(}\index{equality(}


4 

104

5 
Replacing equals by equals is a basic form of reasoning. Isabelle supports


6 
several kinds of equality reasoning. {\bf Substitution} means to replace


7 
free occurrences of~$t$ by~$u$ in a subgoal. This is easily done, given an


8 
equality $t=u$, provided the logic possesses the appropriate rule 


9 
unless you want to substitute even in the assumptions. The tactic

323

10 
{\tt hyp_subst_tac} performs substitution in the assumptions, but it

104

11 
works via objectlevel implication, and therefore must be specially set up


12 
for each suitable objectlogic.


13 


14 
Substitution should not be confused with objectlevel {\bf rewriting}.


15 
Given equalities of the form $t=u$, rewriting replaces instances of~$t$ by


16 
corresponding instances of~$u$, and continues until it reaches a normal


17 
form. Substitution handles `oneoff' replacements by particular


18 
equalities, while rewriting handles general equalities.


19 
Chapter~\ref{simpchap} discusses Isabelle's rewriting tactics.


20 


21 

323

22 
\section{Substitution rules}


23 
\index{substitution!rules}\index{*subst theorem}


24 
Many logics include a substitution rule of the form

104

25 
$$ \List{\Var{a}=\Var{b}; \Var{P}(\Var{a})} \Imp


26 
\Var{P}(\Var{b}) \eqno(subst)$$


27 
In backward proof, this may seem difficult to use: the conclusion


28 
$\Var{P}(\Var{b})$ admits far too many unifiers. But, if the theorem {\tt


29 
eqth} asserts $t=u$, then \hbox{\tt eqth RS subst} is the derived rule


30 
\[ \Var{P}(t) \Imp \Var{P}(u). \]


31 
Provided $u$ is not an unknown, resolution with this rule is


32 
wellbehaved.\footnote{Unifying $\Var{P}(u)$ with a formula~$Q$


33 
expresses~$Q$ in terms of its dependence upon~$u$. There are still $2^k$


34 
unifiers, if $Q$ has $k$ occurrences of~$u$, but Isabelle ensures that


35 
the first unifier includes all the occurrences.} To replace $u$ by~$t$ in


36 
subgoal~$i$, use


37 
\begin{ttbox}


38 
resolve_tac [eqth RS subst] \(i\) {\it.}


39 
\end{ttbox}


40 
To replace $t$ by~$u$ in


41 
subgoal~$i$, use


42 
\begin{ttbox}


43 
resolve_tac [eqth RS ssubst] \(i\) {\it,}


44 
\end{ttbox}

323

45 
where \tdxbold{ssubst} is the `swapped' substitution rule

104

46 
$$ \List{\Var{a}=\Var{b}; \Var{P}(\Var{b})} \Imp


47 
\Var{P}(\Var{a}). \eqno(ssubst)$$

323

48 
If \tdx{sym} denotes the symmetry rule

104

49 
\(\Var{a}=\Var{b}\Imp\Var{b}=\Var{a}\), then {\tt ssubst} is just


50 
\hbox{\tt sym RS subst}. Many logics with equality include the rules {\tt


51 
subst} and {\tt ssubst}, as well as {\tt refl}, {\tt sym} and {\tt trans}

323

52 
(for the usual equality laws). Examples include {\tt FOL} and {\tt HOL},


53 
but not {\tt CTT} (Constructive Type Theory).

104

54 


55 
Elimresolution is wellbehaved with assumptions of the form $t=u$.


56 
To replace $u$ by~$t$ or $t$ by~$u$ in subgoal~$i$, use


57 
\begin{ttbox}


58 
eresolve_tac [subst] \(i\) {\it or} eresolve_tac [ssubst] \(i\) {\it.}


59 
\end{ttbox}


60 


61 


62 
\section{Substitution in the hypotheses}

323

63 
\index{assumptions!substitution in}

104

64 
Substitution rules, like other rules of natural deduction, do not affect


65 
the assumptions. This can be inconvenient. Consider proving the subgoal


66 
\[ \List{c=a; c=b} \Imp a=b. \]

323

67 
Calling {\tt eresolve_tac\ts[ssubst]\ts\(i\)} simply discards the

104

68 
assumption~$c=a$, since $c$ does not occur in~$a=b$. Of course, we can

323

69 
work out a solution. First apply {\tt eresolve_tac\ts[subst]\ts\(i\)},

104

70 
replacing~$a$ by~$c$:


71 
\[ \List{c=b} \Imp c=b \]


72 
Equality reasoning can be difficult, but this trivial proof requires


73 
nothing more sophisticated than substitution in the assumptions.

323

74 
Objectlogics that include the rule~$(subst)$ provide tactics for this

104

75 
purpose:


76 
\begin{ttbox}

323

77 
hyp_subst_tac : int > tactic


78 
bound_hyp_subst_tac : int > tactic

104

79 
\end{ttbox}

323

80 
\begin{ttdescription}

104

81 
\item[\ttindexbold{hyp_subst_tac} {\it i}]

323

82 
selects an equality assumption of the form $t=u$ or $u=t$, where $t$ is a


83 
free variable or parameter. Deleting this assumption, it replaces $t$


84 
by~$u$ throughout subgoal~$i$, including the other assumptions.


85 


86 
\item[\ttindexbold{bound_hyp_subst_tac} {\it i}]


87 
is similar but only substitutes for parameters (bound variables).


88 
Uses for this are discussed below.


89 
\end{ttdescription}

104

90 
The term being replaced must be a free variable or parameter. Substitution


91 
for constants is usually unhelpful, since they may appear in other


92 
theorems. For instance, the best way to use the assumption $0=1$ is to


93 
contradict a theorem that states $0\not=1$, rather than to replace 0 by~1


94 
in the subgoal!


95 


96 
Replacing a free variable causes similar problems if they appear in the


97 
premises of a rule being derived  the substitution affects objectlevel


98 
assumptions, not metalevel assumptions. For instance, replacing~$a$

323

99 
by~$b$ could make the premise~$P(a)$ worthless. To avoid this problem, use


100 
{\tt bound_hyp_subst_tac}; alternatively, call \ttindex{cut_facts_tac} to


101 
insert the atomic premises as objectlevel assumptions.

104

102 


103 


104 
\section{Setting up {\tt hyp_subst_tac}}


105 
Many Isabelle objectlogics, such as {\tt FOL}, {\tt HOL} and their


106 
descendants, come with {\tt hyp_subst_tac} already defined. A few others,


107 
such as {\tt CTT}, do not support this tactic because they lack the


108 
rule~$(subst)$. When defining a new logic that includes a substitution


109 
rule and implication, you must set up {\tt hyp_subst_tac} yourself. It


110 
is packaged as the \ML{} functor \ttindex{HypsubstFun}, which takes the

323

111 
argument signature~{\tt HYPSUBST_DATA}:

104

112 
\begin{ttbox}


113 
signature HYPSUBST_DATA =


114 
sig


115 
val subst : thm


116 
val sym : thm


117 
val rev_cut_eq : thm


118 
val imp_intr : thm


119 
val rev_mp : thm


120 
val dest_eq : term > term*term


121 
end;


122 
\end{ttbox}


123 
Thus, the functor requires the following items:

323

124 
\begin{ttdescription}


125 
\item[\tdxbold{subst}] should be the substitution rule

104

126 
$\List{\Var{a}=\Var{b};\; \Var{P}(\Var{a})} \Imp \Var{P}(\Var{b})$.


127 

323

128 
\item[\tdxbold{sym}] should be the symmetry rule

104

129 
$\Var{a}=\Var{b}\Imp\Var{b}=\Var{a}$.


130 

323

131 
\item[\tdxbold{rev_cut_eq}] should have the form

104

132 
$\List{\Var{a}=\Var{b};\; \Var{a}=\Var{b}\Imp\Var{R}} \Imp \Var{R}$.


133 

323

134 
\item[\tdxbold{imp_intr}] should be the implies introduction

104

135 
rule $(\Var{P}\Imp\Var{Q})\Imp \Var{P}\imp\Var{Q}$.


136 

323

137 
\item[\tdxbold{rev_mp}] should be the `reversed' implies elimination

104

138 
rule $\List{\Var{P}; \;\Var{P}\imp\Var{Q}} \Imp \Var{Q}$.


139 


140 
\item[\ttindexbold{dest_eq}] should return the pair~$(t,u)$ when


141 
applied to the \ML{} term that represents~$t=u$. For other terms, it

323

142 
should raise exception~\xdx{Match}.


143 
\end{ttdescription}


144 
The functor resides in file {\tt Provers/hypsubst.ML} in the Isabelle

104

145 
distribution directory. It is not sensitive to the precise formalization


146 
of the objectlogic. It is not concerned with the names of the equality


147 
and implication symbols, or the types of formula and terms. Coding the


148 
function {\tt dest_eq} requires knowledge of Isabelle's representation of


149 
terms. For {\tt FOL} it is defined by


150 
\begin{ttbox}

286

151 
fun dest_eq (Const("Trueprop",_) $ (Const("op =",_)$t$u)) = (t,u)

104

152 
\end{ttbox}

148

153 
Here {\tt Trueprop} is the coercion from type~$o$ to type~$prop$, while

104

154 
\hbox{\tt op =} is the internal name of the infix operator~{\tt=}.


155 
Patternmatching expresses the function concisely, using wildcards~({\tt_})


156 
to hide the types.


157 

323

158 
Here is how {\tt hyp_subst_tac} works. Given a subgoal of the form


159 
\[ \List{P@1; \cdots ; t=u; \cdots ; P@n} \Imp Q, \] it locates a suitable


160 
equality assumption and moves it to the last position using elimresolution


161 
on {\tt rev_cut_eq} (possibly reorienting it using~{\tt sym}):

104

162 
\[ \List{P@1; \cdots ; P@n; t=u} \Imp Q \]

323

163 
Using $n$ calls of {\tt eresolve_tac\ts[rev_mp]}, it creates the subgoal

104

164 
\[ \List{t=u} \Imp P@1\imp \cdots \imp P@n \imp Q \]

323

165 
By {\tt eresolve_tac\ts[ssubst]}, it replaces~$t$ by~$u$ throughout:

104

166 
\[ P'@1\imp \cdots \imp P'@n \imp Q' \]

323

167 
Finally, using $n$ calls of \hbox{\tt resolve_tac\ts[imp_intr]}, it restores

104

168 
$P'@1$, \ldots, $P'@n$ as assumptions:


169 
\[ \List{P'@n; \cdots ; P'@1} \Imp Q' \]


170 

323

171 
\index{equality)}\index{tactics!substitution)}
