author  obua 
Fri, 16 Sep 2005 21:02:15 +0200  
changeset 17440  df77edc4f5d0 
parent 9695  ec7d7f877712 
child 20975  5bfa2e4ed789 
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 

9695  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 
8136  131 
val eq_reflection : thm (* a=b ==> a==b *) 
9524  132 
val rev_eq_reflection: thm (* a==b ==> a=b *) 
8136  133 
val imp_intr : thm (*(P ==> Q) ==> P>Q *) 
134 
val rev_mp : thm (* [ P; P>Q ] ==> Q *) 

135 
val subst : thm (* [ a=b; P(a) ] ==> P(b) *) 

136 
val sym : thm (* a=b ==> b=a *) 

137 
val thin_refl : thm (* [x=x; P] ==> P *) 

104  138 
end; 
139 
\end{ttbox} 

140 
Thus, the functor requires the following items: 

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

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

144 

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

145 
\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

146 
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

147 
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

148 

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

149 
\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

150 
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

151 
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

152 

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

153 
\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

154 
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

155 
it should raise an exception. 
104  156 

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

157 
\item[\tdxbold{eq_reflection}] is the theorem discussed 
9524  158 
in~\S\ref{sec:settingupsimp}. 
159 

160 
\item[\tdxbold{rev_eq_reflection}] is the reverse of \texttt{eq_reflection}. 

104  161 

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

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

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

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

169 
$\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

170 

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

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

172 
$\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

173 

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

174 
\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

175 
$\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

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

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

179 
The functor resides in file \texttt{Provers/hypsubst.ML} in the Isabelle 
104  180 
distribution directory. It is not sensitive to the precise formalization 
181 
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

182 
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

183 

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

184 
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

185 
\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

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

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

189 
 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

190 

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

191 
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

192 

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

193 
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

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

196 
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

197 
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

198 
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

199 
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

200 
wildcards~({\tt_}) for the types. 
104  201 

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

202 
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

203 
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

204 
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

205 
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

206 
\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

207 
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

208 
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

209 
by calling \hbox{\tt resolve_tac\ts[imp_intr]}. 
104  210 

323  211 
\index{equality)}\index{tactics!substitution)} 
5371  212 

213 

214 
%%% Local Variables: 

215 
%%% mode: latex 

216 
%%% TeXmaster: "ref" 

217 
%%% End: 