author  paulson 
Wed, 07 May 1997 16:29:06 +0200  
changeset 3128  d01d4c0c4b44 
parent 3108  335efc3f5632 
child 3950  e9d5bcae8351 
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 
9 
tactic {\tt hyp_subst_tac} performs substitution even in the assumptions. 

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. 
104  18 
Chapter~\ref{simpchap} discusses Isabelle's rewriting tactics. 
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 
104  52 
\(\Var{a}=\Var{b}\Imp\Var{b}=\Var{a}\), then {\tt ssubst} is just 
53 
\hbox{\tt sym RS subst}. Many logics with equality include the rules {\tt 

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

323  55 
(for the usual equality laws). Examples include {\tt FOL} and {\tt HOL}, 
56 
but not {\tt 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} 
26b62963806c
Documented stac, and updated the documentation of hyp_subst_tac
paulson
parents:
332
diff
changeset

68 
Now {\tt stac~eqth} is like {\tt resolve_tac [eqth RS ssubst]} but with the 
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. \] 

323  77 
Calling {\tt 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 
323  79 
work out a solution. First apply {\tt eresolve_tac\ts[subst]\ts\(i\)}, 
104  80 
replacing~$a$ by~$c$: 
81 
\[ \List{c=b} \Imp c=b \] 

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 
112 
{\tt bound_hyp_subst_tac}; alternatively, call \ttindex{cut_facts_tac} to 

113 
insert the atomic premises as objectlevel assumptions. 

104  114 

115 

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

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

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

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

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

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

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

323  123 
argument signature~{\tt 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 
26b62963806c
Documented stac, and updated the documentation of hyp_subst_tac
paulson
parents:
332
diff
changeset

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

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

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

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

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

133 
val sym : thm (* a=b ==> b=a *) 
104  134 
end; 
135 
\end{ttbox} 

136 
Thus, the functor requires the following items: 

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

138 
\item[Simplifier] should be an instance of the simplifier (see 
26b62963806c
Documented stac, and updated the documentation of hyp_subst_tac
paulson
parents:
332
diff
changeset

139 
Chapter~\ref{simpchap}). 
104  140 

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

141 
\item[\ttindexbold{dest_eq}] should return the pair~$(t,u)$ when 
26b62963806c
Documented stac, and updated the documentation of hyp_subst_tac
paulson
parents:
332
diff
changeset

142 
applied to the \ML{} term that represents~$t=u$. For other terms, it 
26b62963806c
Documented stac, and updated the documentation of hyp_subst_tac
paulson
parents:
332
diff
changeset

143 
should raise exception~\xdx{Match}. 
104  144 

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

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

146 
in~\S\ref{sec:settingupsimp}. 
104  147 

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

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

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

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

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

156 

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

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

158 
$\Var{a}=\Var{b}\Imp\Var{b}=\Var{a}$. 
323  159 
\end{ttdescription} 
2038
26b62963806c
Documented stac, and updated the documentation of hyp_subst_tac
paulson
parents:
332
diff
changeset

160 
% 
323  161 
The functor resides in file {\tt Provers/hypsubst.ML} in the Isabelle 
104  162 
distribution directory. It is not sensitive to the precise formalization 
163 
of the objectlogic. It is not concerned with the names of the equality 

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

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

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

167 
\begin{ttbox} 

286  168 
fun dest_eq (Const("Trueprop",_) $ (Const("op =",_)$t$u)) = (t,u) 
104  169 
\end{ttbox} 
148  170 
Here {\tt Trueprop} is the coercion from type~$o$ to type~$prop$, while 
104  171 
\hbox{\tt op =} is the internal name of the infix operator~{\tt=}. 
172 
Patternmatching expresses the function concisely, using wildcards~({\tt_}) 

332  173 
for the types. 
104  174 

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

175 
The tactic {\tt hyp_subst_tac} works as follows. First, it identifies a 
26b62963806c
Documented stac, and updated the documentation of hyp_subst_tac
paulson
parents:
332
diff
changeset

176 
suitable equality assumption, possibly reorienting it using~{\tt sym}. Then 
26b62963806c
Documented stac, and updated the documentation of hyp_subst_tac
paulson
parents:
332
diff
changeset

177 
it moves other assumptions into the conclusion of the goal, by repeatedly 
26b62963806c
Documented stac, and updated the documentation of hyp_subst_tac
paulson
parents:
332
diff
changeset

178 
caling {\tt eresolve_tac\ts[rev_mp]}. Then, it uses {\tt asm_full_simp_tac} 
26b62963806c
Documented stac, and updated the documentation of hyp_subst_tac
paulson
parents:
332
diff
changeset

179 
or {\tt ssubst} to substitute throughout the subgoal. (If the equality 
26b62963806c
Documented stac, and updated the documentation of hyp_subst_tac
paulson
parents:
332
diff
changeset

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

181 
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

182 
by calling \hbox{\tt resolve_tac\ts[imp_intr]}. 
104  183 

323  184 
\index{equality)}\index{tactics!substitution)} 