104

1 
%% $Id$


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


3 
\index{substitution(}


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


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


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


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


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


9 
\ttindex{hyp_subst_tac} performs substitution in the assumptions, but it


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


11 
for each suitable objectlogic.


12 


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


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


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


16 
form. Substitution handles `oneoff' replacements by particular


17 
equalities, while rewriting handles general equalities.


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


19 


20 


21 
\section{Simple substitution}


22 
\index{substitution!simple}


23 
Many logics include a substitution rule of the form\indexbold{*subst}


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


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


26 
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


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


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


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


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


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


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


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


35 
subgoal~$i$, use


36 
\begin{ttbox}


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


38 
\end{ttbox}


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


40 
subgoal~$i$, use


41 
\begin{ttbox}


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


43 
\end{ttbox}


44 
where \ttindexbold{ssubst} is the `swapped' substitution rule


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


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


47 
If \ttindex{sym} denotes the symmetry rule


48 
\(\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


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


51 
(for the usual equality laws).


52 


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


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


55 
\begin{ttbox}


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


57 
\end{ttbox}


58 


59 


60 
\section{Substitution in the hypotheses}


61 
\index{substitution!in hypotheses}


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


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


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


65 
Calling \hbox{\tt eresolve_tac [ssubst] \(i\)} simply discards the


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


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


68 
replacing~$a$ by~$c$:


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


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


71 
nothing more sophisticated than substitution in the assumptions.


72 
Objectlogics that include the rule~$(subst)$ provide a tactic for this


73 
purpose:


74 
\begin{ttbox}


75 
hyp_subst_tac : int > tactic


76 
\end{ttbox}


77 
\begin{description}


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


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


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


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


82 
\end{description}


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


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


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


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


87 
in the subgoal!


88 


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


90 
premises of a rule being derived  the substitution affects objectlevel


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


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


93 
\ttindex{cut_facts_tac} to insert the atomic premises as objectlevel


94 
assumptions.


95 


96 


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


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


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


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


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


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


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


104 
argument signature~\ttindexbold{HYPSUBST_DATA}:


105 
\begin{ttbox}


106 
signature HYPSUBST_DATA =


107 
sig


108 
val subst : thm


109 
val sym : thm


110 
val rev_cut_eq : thm


111 
val imp_intr : thm


112 
val rev_mp : thm


113 
val dest_eq : term > term*term


114 
end;


115 
\end{ttbox}


116 
Thus, the functor requires the following items:


117 
\begin{description}


118 
\item[\ttindexbold{subst}] should be the substitution rule


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


120 


121 
\item[\ttindexbold{sym}] should be the symmetry rule


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


123 


124 
\item[\ttindexbold{rev_cut_eq}] should have the form


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


126 


127 
\item[\ttindexbold{imp_intr}] should be the implies introduction


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


129 


130 
\item[\ttindexbold{rev_mp}] should be the ``reversed'' implies elimination


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


132 


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


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


135 
should raise exception~\ttindex{Match}.


136 
\end{description}


137 
The functor resides in {\tt Provers/hypsubst.ML} on the Isabelle


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


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


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


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


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


143 
\begin{ttbox}

286

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

104

145 
\end{ttbox}

148

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

104

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


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


149 
to hide the types.


150 


151 
Given a subgoal of the form


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


153 
\ttindexbold{hyp_subst_tac} locates a suitable equality


154 
assumption and moves it to the last position using elimresolution on {\tt


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


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


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


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


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


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


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


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


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


164 


165 
\index{substitution)}
