author  wenzelm 
Wed, 25 Aug 1999 20:49:02 +0200  
changeset 7357  d0e16da40ea2 
parent 6618  13293a7d4a57 
child 8136  8c65f3ca13f2 
permissions  rwrr 
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 
332  6 
several kinds of equality reasoning. {\bf Substitution} means replacing 
104  7 
free occurrences of~$t$ by~$u$ in a subgoal. This is easily done, given an 
332  8 
equality $t=u$, provided the logic possesses the appropriate rule. The 
4596
0c32a609fcad
Updated the description of how to set up hyp_subst_tac
paulson
parents:
4374
diff
changeset

9 
tactic \texttt{hyp_subst_tac} performs substitution even in the assumptions. 
332  10 
But it works via objectlevel implication, and therefore must be specially 
11 
set up for each suitable objectlogic. 

104  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 

332  17 
equalities while rewriting handles general equations. 
3950  18 
Chapter~\ref{chap:simplification} discusses Isabelle's rewriting tactics. 
104  19 

20 

323  21 
\section{Substitution rules} 
22 
\index{substitution!rules}\index{*subst theorem} 

23 
Many logics include a substitution rule of the form 

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

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

27 
$$ 

104  28 
In backward proof, this may seem difficult to use: the conclusion 
29 
$\Var{P}(\Var{b})$ admits far too many unifiers. But, if the theorem {\tt 

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

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

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

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

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

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

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

37 
subgoal~$i$, use 

38 
\begin{ttbox} 

332  39 
resolve_tac [eqth RS subst] \(i\){\it.} 
104  40 
\end{ttbox} 
41 
To replace $t$ by~$u$ in 

42 
subgoal~$i$, use 

43 
\begin{ttbox} 

332  44 
resolve_tac [eqth RS ssubst] \(i\){\it,} 
104  45 
\end{ttbox} 
323  46 
where \tdxbold{ssubst} is the `swapped' substitution rule 
3108  47 
$$ 
48 
\List{\Var{a}=\Var{b}; \Var{P}(\Var{b})} \Imp 

49 
\Var{P}(\Var{a}). \eqno(ssubst) 

50 
$$ 

323  51 
If \tdx{sym} denotes the symmetry rule 
4596
0c32a609fcad
Updated the description of how to set up hyp_subst_tac
paulson
parents:
4374
diff
changeset

52 
\(\Var{a}=\Var{b}\Imp\Var{b}=\Var{a}\), then \texttt{ssubst} is just 
104  53 
\hbox{\tt sym RS subst}. Many logics with equality include the rules {\tt 
4596
0c32a609fcad
Updated the description of how to set up hyp_subst_tac
paulson
parents:
4374
diff
changeset

54 
subst} and \texttt{ssubst}, as well as \texttt{refl}, \texttt{sym} and \texttt{trans} 
0c32a609fcad
Updated the description of how to set up hyp_subst_tac
paulson
parents:
4374
diff
changeset

55 
(for the usual equality laws). Examples include \texttt{FOL} and \texttt{HOL}, 
0c32a609fcad
Updated the description of how to set up hyp_subst_tac
paulson
parents:
4374
diff
changeset

56 
but not \texttt{CTT} (Constructive Type Theory). 
104  57 

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

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

60 
\begin{ttbox} 

332  61 
eresolve_tac [subst] \(i\) {\rm or} eresolve_tac [ssubst] \(i\){\it.} 
104  62 
\end{ttbox} 
63 

3108  64 
Logics \HOL, {\FOL} and {\ZF} define the tactic \ttindexbold{stac} by 
2038
26b62963806c
Documented stac, and updated the documentation of hyp_subst_tac
paulson
parents:
332
diff
changeset

65 
\begin{ttbox} 
26b62963806c
Documented stac, and updated the documentation of hyp_subst_tac
paulson
parents:
332
diff
changeset

66 
fun stac eqth = CHANGED o rtac (eqth RS ssubst); 
26b62963806c
Documented stac, and updated the documentation of hyp_subst_tac
paulson
parents:
332
diff
changeset

67 
\end{ttbox} 
4596
0c32a609fcad
Updated the description of how to set up hyp_subst_tac
paulson
parents:
4374
diff
changeset

68 
Now \texttt{stac~eqth} is like \texttt{resolve_tac [eqth RS ssubst]} but with the 
2038
26b62963806c
Documented stac, and updated the documentation of hyp_subst_tac
paulson
parents:
332
diff
changeset

69 
valuable property of failing if the substitution has no effect. 
26b62963806c
Documented stac, and updated the documentation of hyp_subst_tac
paulson
parents:
332
diff
changeset

70 

104  71 

72 
\section{Substitution in the hypotheses} 

323  73 
\index{assumptions!substitution in} 
104  74 
Substitution rules, like other rules of natural deduction, do not affect 
75 
the assumptions. This can be inconvenient. Consider proving the subgoal 

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

4596
0c32a609fcad
Updated the description of how to set up hyp_subst_tac
paulson
parents:
4374
diff
changeset

77 
Calling \texttt{eresolve_tac\ts[ssubst]\ts\(i\)} simply discards the 
104  78 
assumption~$c=a$, since $c$ does not occur in~$a=b$. Of course, we can 
4596
0c32a609fcad
Updated the description of how to set up hyp_subst_tac
paulson
parents:
4374
diff
changeset

79 
work out a solution. First apply \texttt{eresolve_tac\ts[subst]\ts\(i\)}, 
104  80 
replacing~$a$ by~$c$: 
4374  81 
\[ c=b \Imp c=b \] 
104  82 
Equality reasoning can be difficult, but this trivial proof requires 
83 
nothing more sophisticated than substitution in the assumptions. 

323  84 
Objectlogics that include the rule~$(subst)$ provide tactics for this 
104  85 
purpose: 
86 
\begin{ttbox} 

323  87 
hyp_subst_tac : int > tactic 
88 
bound_hyp_subst_tac : int > tactic 

104  89 
\end{ttbox} 
323  90 
\begin{ttdescription} 
104  91 
\item[\ttindexbold{hyp_subst_tac} {\it i}] 
323  92 
selects an equality assumption of the form $t=u$ or $u=t$, where $t$ is a 
93 
free variable or parameter. Deleting this assumption, it replaces $t$ 

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

95 

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

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

98 
Uses for this are discussed below. 

99 
\end{ttdescription} 

104  100 
The term being replaced must be a free variable or parameter. Substitution 
101 
for constants is usually unhelpful, since they may appear in other 

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

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

104 
in the subgoal! 

105 

2038
26b62963806c
Documented stac, and updated the documentation of hyp_subst_tac
paulson
parents:
332
diff
changeset

106 
Substitution for unknowns, such as $\Var{x}=0$, is a bad idea: we might prove 
26b62963806c
Documented stac, and updated the documentation of hyp_subst_tac
paulson
parents:
332
diff
changeset

107 
the subgoal more easily by instantiating~$\Var{x}$ to~1. 
26b62963806c
Documented stac, and updated the documentation of hyp_subst_tac
paulson
parents:
332
diff
changeset

108 
Substitution for free variables is unhelpful if they appear in the 
26b62963806c
Documented stac, and updated the documentation of hyp_subst_tac
paulson
parents:
332
diff
changeset

109 
premises of a rule being derived: the substitution affects objectlevel 
104  110 
assumptions, not metalevel assumptions. For instance, replacing~$a$ 
323  111 
by~$b$ could make the premise~$P(a)$ worthless. To avoid this problem, use 
4596
0c32a609fcad
Updated the description of how to set up hyp_subst_tac
paulson
parents:
4374
diff
changeset

112 
\texttt{bound_hyp_subst_tac}; alternatively, call \ttindex{cut_facts_tac} to 
323  113 
insert the atomic premises as objectlevel assumptions. 
104  114 

115 

6618  116 
\section{Setting up the package} 
4596
0c32a609fcad
Updated the description of how to set up hyp_subst_tac
paulson
parents:
4374
diff
changeset

117 
Many Isabelle objectlogics, such as \texttt{FOL}, \texttt{HOL} and their 
0c32a609fcad
Updated the description of how to set up hyp_subst_tac
paulson
parents:
4374
diff
changeset

118 
descendants, come with \texttt{hyp_subst_tac} already defined. A few others, 
0c32a609fcad
Updated the description of how to set up hyp_subst_tac
paulson
parents:
4374
diff
changeset

119 
such as \texttt{CTT}, do not support this tactic because they lack the 
104  120 
rule~$(subst)$. When defining a new logic that includes a substitution 
4596
0c32a609fcad
Updated the description of how to set up hyp_subst_tac
paulson
parents:
4374
diff
changeset

121 
rule and implication, you must set up \texttt{hyp_subst_tac} yourself. It 
104  122 
is packaged as the \ML{} functor \ttindex{HypsubstFun}, which takes the 
4596
0c32a609fcad
Updated the description of how to set up hyp_subst_tac
paulson
parents:
4374
diff
changeset

123 
argument signature~\texttt{HYPSUBST_DATA}: 
104  124 
\begin{ttbox} 
125 
signature HYPSUBST_DATA = 

126 
sig 

2038
26b62963806c
Documented stac, and updated the documentation of hyp_subst_tac
paulson
parents:
332
diff
changeset

127 
structure Simplifier : SIMPLIFIER 
4596
0c32a609fcad
Updated the description of how to set up hyp_subst_tac
paulson
parents:
4374
diff
changeset

128 
val dest_Trueprop : term > term 
0c32a609fcad
Updated the description of how to set up hyp_subst_tac
paulson
parents:
4374
diff
changeset

129 
val dest_eq : term > term*term*typ 
0c32a609fcad
Updated the description of how to set up hyp_subst_tac
paulson
parents:
4374
diff
changeset

130 
val dest_imp : term > term*term 
3128
d01d4c0c4b44
New acknowledgements; fixed overfull lines and tables
paulson
parents:
3108
diff
changeset

131 
val eq_reflection : thm (* a=b ==> a==b *) 
d01d4c0c4b44
New acknowledgements; fixed overfull lines and tables
paulson
parents:
3108
diff
changeset

132 
val imp_intr : thm (* (P ==> Q) ==> P>Q *) 
d01d4c0c4b44
New acknowledgements; fixed overfull lines and tables
paulson
parents:
3108
diff
changeset

133 
val rev_mp : thm (* [ P; P>Q ] ==> Q *) 
d01d4c0c4b44
New acknowledgements; fixed overfull lines and tables
paulson
parents:
3108
diff
changeset

134 
val subst : thm (* [ a=b; P(a) ] ==> P(b) *) 
d01d4c0c4b44
New acknowledgements; fixed overfull lines and tables
paulson
parents:
3108
diff
changeset

135 
val sym : thm (* a=b ==> b=a *) 
4596
0c32a609fcad
Updated the description of how to set up hyp_subst_tac
paulson
parents:
4374
diff
changeset

136 
val thin_refl : thm (* [x=x; P] ==> P *) 
104  137 
end; 
138 
\end{ttbox} 

139 
Thus, the functor requires the following items: 

323  140 
\begin{ttdescription} 
2038
26b62963806c
Documented stac, and updated the documentation of hyp_subst_tac
paulson
parents:
332
diff
changeset

141 
\item[Simplifier] should be an instance of the simplifier (see 
3950  142 
Chapter~\ref{chap:simplification}). 
4596
0c32a609fcad
Updated the description of how to set up hyp_subst_tac
paulson
parents:
4374
diff
changeset

143 

0c32a609fcad
Updated the description of how to set up hyp_subst_tac
paulson
parents:
4374
diff
changeset

144 
\item[\ttindexbold{dest_Trueprop}] should coerce a metalevel formula to the 
0c32a609fcad
Updated the description of how to set up hyp_subst_tac
paulson
parents:
4374
diff
changeset

145 
corresponding objectlevel one. Typically, it should return $P$ when 
0c32a609fcad
Updated the description of how to set up hyp_subst_tac
paulson
parents:
4374
diff
changeset

146 
applied to the term $\texttt{Trueprop}\,P$ (see example below). 
0c32a609fcad
Updated the description of how to set up hyp_subst_tac
paulson
parents:
4374
diff
changeset

147 

0c32a609fcad
Updated the description of how to set up hyp_subst_tac
paulson
parents:
4374
diff
changeset

148 
\item[\ttindexbold{dest_eq}] should return the triple~$(t,u,T)$, where $T$ is 
0c32a609fcad
Updated the description of how to set up hyp_subst_tac
paulson
parents:
4374
diff
changeset

149 
the type of~$t$ and~$u$, when applied to the \ML{} term that 
0c32a609fcad
Updated the description of how to set up hyp_subst_tac
paulson
parents:
4374
diff
changeset

150 
represents~$t=u$. For other terms, it should raise an exception. 
0c32a609fcad
Updated the description of how to set up hyp_subst_tac
paulson
parents:
4374
diff
changeset

151 

0c32a609fcad
Updated the description of how to set up hyp_subst_tac
paulson
parents:
4374
diff
changeset

152 
\item[\ttindexbold{dest_imp}] should return the pair~$(P,Q)$ when applied to 
0c32a609fcad
Updated the description of how to set up hyp_subst_tac
paulson
parents:
4374
diff
changeset

153 
the \ML{} term that represents the implication $P\imp Q$. For other terms, 
0c32a609fcad
Updated the description of how to set up hyp_subst_tac
paulson
parents:
4374
diff
changeset

154 
it should raise an exception. 
104  155 

2038
26b62963806c
Documented stac, and updated the documentation of hyp_subst_tac
paulson
parents:
332
diff
changeset

156 
\item[\tdxbold{eq_reflection}] is the theorem discussed 
26b62963806c
Documented stac, and updated the documentation of hyp_subst_tac
paulson
parents:
332
diff
changeset

157 
in~\S\ref{sec:settingupsimp}. 
104  158 

323  159 
\item[\tdxbold{imp_intr}] should be the implies introduction 
104  160 
rule $(\Var{P}\Imp\Var{Q})\Imp \Var{P}\imp\Var{Q}$. 
161 

323  162 
\item[\tdxbold{rev_mp}] should be the `reversed' implies elimination 
104  163 
rule $\List{\Var{P}; \;\Var{P}\imp\Var{Q}} \Imp \Var{Q}$. 
164 

2038
26b62963806c
Documented stac, and updated the documentation of hyp_subst_tac
paulson
parents:
332
diff
changeset

165 
\item[\tdxbold{subst}] should be the substitution rule 
26b62963806c
Documented stac, and updated the documentation of hyp_subst_tac
paulson
parents:
332
diff
changeset

166 
$\List{\Var{a}=\Var{b};\; \Var{P}(\Var{a})} \Imp \Var{P}(\Var{b})$. 
26b62963806c
Documented stac, and updated the documentation of hyp_subst_tac
paulson
parents:
332
diff
changeset

167 

26b62963806c
Documented stac, and updated the documentation of hyp_subst_tac
paulson
parents:
332
diff
changeset

168 
\item[\tdxbold{sym}] should be the symmetry rule 
26b62963806c
Documented stac, and updated the documentation of hyp_subst_tac
paulson
parents:
332
diff
changeset

169 
$\Var{a}=\Var{b}\Imp\Var{b}=\Var{a}$. 
4596
0c32a609fcad
Updated the description of how to set up hyp_subst_tac
paulson
parents:
4374
diff
changeset

170 

0c32a609fcad
Updated the description of how to set up hyp_subst_tac
paulson
parents:
4374
diff
changeset

171 
\item[\tdxbold{thin_refl}] should be the rule 
0c32a609fcad
Updated the description of how to set up hyp_subst_tac
paulson
parents:
4374
diff
changeset

172 
$\List{\Var{a}=\Var{a};\; \Var{P}} \Imp \Var{P}$, which is used to erase 
0c32a609fcad
Updated the description of how to set up hyp_subst_tac
paulson
parents:
4374
diff
changeset

173 
trivial equalities. 
323  174 
\end{ttdescription} 
2038
26b62963806c
Documented stac, and updated the documentation of hyp_subst_tac
paulson
parents:
332
diff
changeset

175 
% 
4596
0c32a609fcad
Updated the description of how to set up hyp_subst_tac
paulson
parents:
4374
diff
changeset

176 
The functor resides in file \texttt{Provers/hypsubst.ML} in the Isabelle 
104  177 
distribution directory. It is not sensitive to the precise formalization 
178 
of the objectlogic. It is not concerned with the names of the equality 

4596
0c32a609fcad
Updated the description of how to set up hyp_subst_tac
paulson
parents:
4374
diff
changeset

179 
and implication symbols, or the types of formula and terms. 
0c32a609fcad
Updated the description of how to set up hyp_subst_tac
paulson
parents:
4374
diff
changeset

180 

0c32a609fcad
Updated the description of how to set up hyp_subst_tac
paulson
parents:
4374
diff
changeset

181 
Coding the functions \texttt{dest_Trueprop}, \texttt{dest_eq} and 
0c32a609fcad
Updated the description of how to set up hyp_subst_tac
paulson
parents:
4374
diff
changeset

182 
\texttt{dest_imp} requires knowledge of Isabelle's representation of terms. 
0c32a609fcad
Updated the description of how to set up hyp_subst_tac
paulson
parents:
4374
diff
changeset

183 
For \texttt{FOL}, they are declared by 
104  184 
\begin{ttbox} 
4596
0c32a609fcad
Updated the description of how to set up hyp_subst_tac
paulson
parents:
4374
diff
changeset

185 
fun dest_Trueprop (Const ("Trueprop", _) $ P) = P 
0c32a609fcad
Updated the description of how to set up hyp_subst_tac
paulson
parents:
4374
diff
changeset

186 
 dest_Trueprop t = raise TERM ("dest_Trueprop", [t]); 
0c32a609fcad
Updated the description of how to set up hyp_subst_tac
paulson
parents:
4374
diff
changeset

187 

0c32a609fcad
Updated the description of how to set up hyp_subst_tac
paulson
parents:
4374
diff
changeset

188 
fun dest_eq (Const("op =",T) $ t $ u) = (t, u, domain_type T) 
0c32a609fcad
Updated the description of how to set up hyp_subst_tac
paulson
parents:
4374
diff
changeset

189 

0c32a609fcad
Updated the description of how to set up hyp_subst_tac
paulson
parents:
4374
diff
changeset

190 
fun dest_imp (Const("op >",_) $ A $ B) = (A, B) 
0c32a609fcad
Updated the description of how to set up hyp_subst_tac
paulson
parents:
4374
diff
changeset

191 
 dest_imp t = raise TERM ("dest_imp", [t]); 
104  192 
\end{ttbox} 
4596
0c32a609fcad
Updated the description of how to set up hyp_subst_tac
paulson
parents:
4374
diff
changeset

193 
Recall that \texttt{Trueprop} is the coercion from type~$o$ to type~$prop$, 
0c32a609fcad
Updated the description of how to set up hyp_subst_tac
paulson
parents:
4374
diff
changeset

194 
while \hbox{\tt op =} is the internal name of the infix operator~\texttt{=}. 
0c32a609fcad
Updated the description of how to set up hyp_subst_tac
paulson
parents:
4374
diff
changeset

195 
Function \ttindexbold{domain_type}, given the function type $S\To T$, returns 
0c32a609fcad
Updated the description of how to set up hyp_subst_tac
paulson
parents:
4374
diff
changeset

196 
the type~$S$. Patternmatching expresses the function concisely, using 
0c32a609fcad
Updated the description of how to set up hyp_subst_tac
paulson
parents:
4374
diff
changeset

197 
wildcards~({\tt_}) for the types. 
104  198 

4596
0c32a609fcad
Updated the description of how to set up hyp_subst_tac
paulson
parents:
4374
diff
changeset

199 
The tactic \texttt{hyp_subst_tac} works as follows. First, it identifies a 
0c32a609fcad
Updated the description of how to set up hyp_subst_tac
paulson
parents:
4374
diff
changeset

200 
suitable equality assumption, possibly reorienting it using~\texttt{sym}. 
0c32a609fcad
Updated the description of how to set up hyp_subst_tac
paulson
parents:
4374
diff
changeset

201 
Then it moves other assumptions into the conclusion of the goal, by repeatedly 
0c32a609fcad
Updated the description of how to set up hyp_subst_tac
paulson
parents:
4374
diff
changeset

202 
calling \texttt{etac~rev_mp}. Then, it uses \texttt{asm_full_simp_tac} or 
0c32a609fcad
Updated the description of how to set up hyp_subst_tac
paulson
parents:
4374
diff
changeset

203 
\texttt{ssubst} to substitute throughout the subgoal. (If the equality 
0c32a609fcad
Updated the description of how to set up hyp_subst_tac
paulson
parents:
4374
diff
changeset

204 
involves unknowns then it must use \texttt{ssubst}.) Then, it deletes the 
2038
26b62963806c
Documented stac, and updated the documentation of hyp_subst_tac
paulson
parents:
332
diff
changeset

205 
equality. Finally, it moves the assumptions back to their original positions 
26b62963806c
Documented stac, and updated the documentation of hyp_subst_tac
paulson
parents:
332
diff
changeset

206 
by calling \hbox{\tt resolve_tac\ts[imp_intr]}. 
104  207 

323  208 
\index{equality)}\index{tactics!substitution)} 
5371  209 

210 

211 
%%% Local Variables: 

212 
%%% mode: latex 

213 
%%% TeXmaster: "ref" 

214 
%%% End: 