author  paulson 
Thu, 26 Sep 1996 17:13:18 +0200  
changeset 2038  26b62963806c 
parent 332  01b87a921967 
child 3108  335efc3f5632 
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 

104  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} 

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

40 
subgoal~$i$, use 

41 
\begin{ttbox} 

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

323  47 
If \tdx{sym} denotes the symmetry rule 
104  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} 

323  51 
(for the usual equality laws). Examples include {\tt FOL} and {\tt HOL}, 
52 
but not {\tt CTT} (Constructive Type Theory). 

104  53 

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

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

56 
\begin{ttbox} 

332  57 
eresolve_tac [subst] \(i\) {\rm or} eresolve_tac [ssubst] \(i\){\it.} 
104  58 
\end{ttbox} 
59 

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

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

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

62 
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

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

64 
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

65 
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

66 

104  67 

68 
\section{Substitution in the hypotheses} 

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

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

323  73 
Calling {\tt eresolve_tac\ts[ssubst]\ts\(i\)} simply discards the 
104  74 
assumption~$c=a$, since $c$ does not occur in~$a=b$. Of course, we can 
323  75 
work out a solution. First apply {\tt eresolve_tac\ts[subst]\ts\(i\)}, 
104  76 
replacing~$a$ by~$c$: 
77 
\[ \List{c=b} \Imp c=b \] 

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

79 
nothing more sophisticated than substitution in the assumptions. 

323  80 
Objectlogics that include the rule~$(subst)$ provide tactics for this 
104  81 
purpose: 
82 
\begin{ttbox} 

323  83 
hyp_subst_tac : int > tactic 
84 
bound_hyp_subst_tac : int > tactic 

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

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

91 

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

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

94 
Uses for this are discussed below. 

95 
\end{ttdescription} 

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

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

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

100 
in the subgoal! 

101 

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

102 
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

103 
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

104 
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

105 
premises of a rule being derived: the substitution affects objectlevel 
104  106 
assumptions, not metalevel assumptions. For instance, replacing~$a$ 
323  107 
by~$b$ could make the premise~$P(a)$ worthless. To avoid this problem, use 
108 
{\tt bound_hyp_subst_tac}; alternatively, call \ttindex{cut_facts_tac} to 

109 
insert the atomic premises as objectlevel assumptions. 

104  110 

111 

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

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

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

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

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

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

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

323  119 
argument signature~{\tt HYPSUBST_DATA}: 
104  120 
\begin{ttbox} 
121 
signature HYPSUBST_DATA = 

122 
sig 

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

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

124 
val dest_eq : term > term*term 
26b62963806c
Documented stac, and updated the documentation of hyp_subst_tac
paulson
parents:
332
diff
changeset

125 
val eq_reflection : thm (* a=b ==> a==b *) 
26b62963806c
Documented stac, and updated the documentation of hyp_subst_tac
paulson
parents:
332
diff
changeset

126 
val imp_intr : thm (* (P ==> Q) ==> P>Q *) 
26b62963806c
Documented stac, and updated the documentation of hyp_subst_tac
paulson
parents:
332
diff
changeset

127 
val rev_mp : thm (* [ P; P>Q ] ==> Q *) 
26b62963806c
Documented stac, and updated the documentation of hyp_subst_tac
paulson
parents:
332
diff
changeset

128 
val subst : thm (* [ a=b; P(a) ] ==> P(b) *) 
26b62963806c
Documented stac, and updated the documentation of hyp_subst_tac
paulson
parents:
332
diff
changeset

129 
val sym : thm (* a=b ==> b=a *) 
104  130 
end; 
131 
\end{ttbox} 

132 
Thus, the functor requires the following items: 

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

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

135 
Chapter~\ref{simpchap}). 
104  136 

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

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

138 
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

139 
should raise exception~\xdx{Match}. 
104  140 

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

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

142 
in~\S\ref{sec:settingupsimp}. 
104  143 

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

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

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

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

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

152 

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

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

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

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

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

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

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

163 
\begin{ttbox} 

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

332  169 
for the types. 
104  170 

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

171 
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

172 
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

173 
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

174 
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

175 
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

176 
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

177 
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

178 
by calling \hbox{\tt resolve_tac\ts[imp_intr]}. 
104  179 

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