wenzelm@30184
|
1 |
|
lcp@104
|
2 |
\chapter{Substitution Tactics} \label{substitution}
|
lcp@323
|
3 |
\index{tactics!substitution|(}\index{equality|(}
|
lcp@323
|
4 |
|
lcp@104
|
5 |
Replacing equals by equals is a basic form of reasoning. Isabelle supports
|
lcp@332
|
6 |
several kinds of equality reasoning. {\bf Substitution} means replacing
|
lcp@104
|
7 |
free occurrences of~$t$ by~$u$ in a subgoal. This is easily done, given an
|
lcp@332
|
8 |
equality $t=u$, provided the logic possesses the appropriate rule. The
|
paulson@4596
|
9 |
tactic \texttt{hyp_subst_tac} performs substitution even in the assumptions.
|
lcp@332
|
10 |
But it works via object-level implication, and therefore must be specially
|
lcp@332
|
11 |
set up for each suitable object-logic.
|
lcp@104
|
12 |
|
lcp@104
|
13 |
Substitution should not be confused with object-level {\bf rewriting}.
|
lcp@104
|
14 |
Given equalities of the form $t=u$, rewriting replaces instances of~$t$ by
|
lcp@104
|
15 |
corresponding instances of~$u$, and continues until it reaches a normal
|
lcp@104
|
16 |
form. Substitution handles `one-off' replacements by particular
|
lcp@332
|
17 |
equalities while rewriting handles general equations.
|
nipkow@3950
|
18 |
Chapter~\ref{chap:simplification} discusses Isabelle's rewriting tactics.
|
lcp@104
|
19 |
|
lcp@104
|
20 |
|
lcp@323
|
21 |
\section{Substitution rules}
|
lcp@323
|
22 |
\index{substitution!rules}\index{*subst theorem}
|
lcp@323
|
23 |
Many logics include a substitution rule of the form
|
wenzelm@3108
|
24 |
$$
|
wenzelm@3108
|
25 |
\List{\Var{a}=\Var{b}; \Var{P}(\Var{a})} \Imp
|
wenzelm@3108
|
26 |
\Var{P}(\Var{b}) \eqno(subst)
|
wenzelm@3108
|
27 |
$$
|
lcp@104
|
28 |
In backward proof, this may seem difficult to use: the conclusion
|
lcp@104
|
29 |
$\Var{P}(\Var{b})$ admits far too many unifiers. But, if the theorem {\tt
|
lcp@104
|
30 |
eqth} asserts $t=u$, then \hbox{\tt eqth RS subst} is the derived rule
|
lcp@104
|
31 |
\[ \Var{P}(t) \Imp \Var{P}(u). \]
|
lcp@104
|
32 |
Provided $u$ is not an unknown, resolution with this rule is
|
lcp@104
|
33 |
well-behaved.\footnote{Unifying $\Var{P}(u)$ with a formula~$Q$
|
lcp@104
|
34 |
expresses~$Q$ in terms of its dependence upon~$u$. There are still $2^k$
|
lcp@104
|
35 |
unifiers, if $Q$ has $k$ occurrences of~$u$, but Isabelle ensures that
|
lcp@104
|
36 |
the first unifier includes all the occurrences.} To replace $u$ by~$t$ in
|
lcp@104
|
37 |
subgoal~$i$, use
|
lcp@104
|
38 |
\begin{ttbox}
|
lcp@332
|
39 |
resolve_tac [eqth RS subst] \(i\){\it.}
|
lcp@104
|
40 |
\end{ttbox}
|
lcp@104
|
41 |
To replace $t$ by~$u$ in
|
lcp@104
|
42 |
subgoal~$i$, use
|
lcp@104
|
43 |
\begin{ttbox}
|
lcp@332
|
44 |
resolve_tac [eqth RS ssubst] \(i\){\it,}
|
lcp@104
|
45 |
\end{ttbox}
|
lcp@323
|
46 |
where \tdxbold{ssubst} is the `swapped' substitution rule
|
wenzelm@3108
|
47 |
$$
|
wenzelm@3108
|
48 |
\List{\Var{a}=\Var{b}; \Var{P}(\Var{b})} \Imp
|
wenzelm@3108
|
49 |
\Var{P}(\Var{a}). \eqno(ssubst)
|
wenzelm@3108
|
50 |
$$
|
lcp@323
|
51 |
If \tdx{sym} denotes the symmetry rule
|
paulson@4596
|
52 |
\(\Var{a}=\Var{b}\Imp\Var{b}=\Var{a}\), then \texttt{ssubst} is just
|
lcp@104
|
53 |
\hbox{\tt sym RS subst}. Many logics with equality include the rules {\tt
|
paulson@4596
|
54 |
subst} and \texttt{ssubst}, as well as \texttt{refl}, \texttt{sym} and \texttt{trans}
|
paulson@4596
|
55 |
(for the usual equality laws). Examples include \texttt{FOL} and \texttt{HOL},
|
paulson@4596
|
56 |
but not \texttt{CTT} (Constructive Type Theory).
|
lcp@104
|
57 |
|
lcp@104
|
58 |
Elim-resolution is well-behaved with assumptions of the form $t=u$.
|
lcp@104
|
59 |
To replace $u$ by~$t$ or $t$ by~$u$ in subgoal~$i$, use
|
lcp@104
|
60 |
\begin{ttbox}
|
lcp@332
|
61 |
eresolve_tac [subst] \(i\) {\rm or} eresolve_tac [ssubst] \(i\){\it.}
|
lcp@104
|
62 |
\end{ttbox}
|
lcp@104
|
63 |
|
wenzelm@9695
|
64 |
Logics HOL, FOL and ZF define the tactic \ttindexbold{stac} by
|
paulson@2038
|
65 |
\begin{ttbox}
|
paulson@2038
|
66 |
fun stac eqth = CHANGED o rtac (eqth RS ssubst);
|
paulson@2038
|
67 |
\end{ttbox}
|
paulson@4596
|
68 |
Now \texttt{stac~eqth} is like \texttt{resolve_tac [eqth RS ssubst]} but with the
|
paulson@2038
|
69 |
valuable property of failing if the substitution has no effect.
|
paulson@2038
|
70 |
|
lcp@104
|
71 |
|
lcp@104
|
72 |
\section{Substitution in the hypotheses}
|
lcp@323
|
73 |
\index{assumptions!substitution in}
|
lcp@104
|
74 |
Substitution rules, like other rules of natural deduction, do not affect
|
lcp@104
|
75 |
the assumptions. This can be inconvenient. Consider proving the subgoal
|
lcp@104
|
76 |
\[ \List{c=a; c=b} \Imp a=b. \]
|
paulson@4596
|
77 |
Calling \texttt{eresolve_tac\ts[ssubst]\ts\(i\)} simply discards the
|
lcp@104
|
78 |
assumption~$c=a$, since $c$ does not occur in~$a=b$. Of course, we can
|
paulson@4596
|
79 |
work out a solution. First apply \texttt{eresolve_tac\ts[subst]\ts\(i\)},
|
lcp@104
|
80 |
replacing~$a$ by~$c$:
|
wenzelm@4374
|
81 |
\[ c=b \Imp c=b \]
|
lcp@104
|
82 |
Equality reasoning can be difficult, but this trivial proof requires
|
lcp@104
|
83 |
nothing more sophisticated than substitution in the assumptions.
|
lcp@323
|
84 |
Object-logics that include the rule~$(subst)$ provide tactics for this
|
lcp@104
|
85 |
purpose:
|
lcp@104
|
86 |
\begin{ttbox}
|
lcp@323
|
87 |
hyp_subst_tac : int -> tactic
|
lcp@323
|
88 |
bound_hyp_subst_tac : int -> tactic
|
lcp@104
|
89 |
\end{ttbox}
|
lcp@323
|
90 |
\begin{ttdescription}
|
lcp@104
|
91 |
\item[\ttindexbold{hyp_subst_tac} {\it i}]
|
lcp@323
|
92 |
selects an equality assumption of the form $t=u$ or $u=t$, where $t$ is a
|
lcp@323
|
93 |
free variable or parameter. Deleting this assumption, it replaces $t$
|
lcp@323
|
94 |
by~$u$ throughout subgoal~$i$, including the other assumptions.
|
lcp@323
|
95 |
|
lcp@323
|
96 |
\item[\ttindexbold{bound_hyp_subst_tac} {\it i}]
|
lcp@323
|
97 |
is similar but only substitutes for parameters (bound variables).
|
lcp@323
|
98 |
Uses for this are discussed below.
|
lcp@323
|
99 |
\end{ttdescription}
|
lcp@104
|
100 |
The term being replaced must be a free variable or parameter. Substitution
|
lcp@104
|
101 |
for constants is usually unhelpful, since they may appear in other
|
lcp@104
|
102 |
theorems. For instance, the best way to use the assumption $0=1$ is to
|
lcp@104
|
103 |
contradict a theorem that states $0\not=1$, rather than to replace 0 by~1
|
lcp@104
|
104 |
in the subgoal!
|
lcp@104
|
105 |
|
paulson@2038
|
106 |
Substitution for unknowns, such as $\Var{x}=0$, is a bad idea: we might prove
|
paulson@2038
|
107 |
the subgoal more easily by instantiating~$\Var{x}$ to~1.
|
paulson@2038
|
108 |
Substitution for free variables is unhelpful if they appear in the
|
paulson@2038
|
109 |
premises of a rule being derived: the substitution affects object-level
|
lcp@104
|
110 |
assumptions, not meta-level assumptions. For instance, replacing~$a$
|
lcp@323
|
111 |
by~$b$ could make the premise~$P(a)$ worthless. To avoid this problem, use
|
paulson@4596
|
112 |
\texttt{bound_hyp_subst_tac}; alternatively, call \ttindex{cut_facts_tac} to
|
lcp@323
|
113 |
insert the atomic premises as object-level assumptions.
|
lcp@104
|
114 |
|
lcp@104
|
115 |
|
wenzelm@6618
|
116 |
\section{Setting up the package}
|
paulson@4596
|
117 |
Many Isabelle object-logics, such as \texttt{FOL}, \texttt{HOL} and their
|
paulson@4596
|
118 |
descendants, come with \texttt{hyp_subst_tac} already defined. A few others,
|
paulson@4596
|
119 |
such as \texttt{CTT}, do not support this tactic because they lack the
|
lcp@104
|
120 |
rule~$(subst)$. When defining a new logic that includes a substitution
|
paulson@4596
|
121 |
rule and implication, you must set up \texttt{hyp_subst_tac} yourself. It
|
lcp@104
|
122 |
is packaged as the \ML{} functor \ttindex{HypsubstFun}, which takes the
|
paulson@4596
|
123 |
argument signature~\texttt{HYPSUBST_DATA}:
|
lcp@104
|
124 |
\begin{ttbox}
|
lcp@104
|
125 |
signature HYPSUBST_DATA =
|
lcp@104
|
126 |
sig
|
paulson@2038
|
127 |
structure Simplifier : SIMPLIFIER
|
paulson@4596
|
128 |
val dest_Trueprop : term -> term
|
haftmann@20975
|
129 |
val dest_eq : term -> (term*term)*typ
|
paulson@4596
|
130 |
val dest_imp : term -> term*term
|
paulson@8136
|
131 |
val eq_reflection : thm (* a=b ==> a==b *)
|
wenzelm@9524
|
132 |
val rev_eq_reflection: thm (* a==b ==> a=b *)
|
paulson@8136
|
133 |
val imp_intr : thm (*(P ==> Q) ==> P-->Q *)
|
paulson@8136
|
134 |
val rev_mp : thm (* [| P; P-->Q |] ==> Q *)
|
paulson@8136
|
135 |
val subst : thm (* [| a=b; P(a) |] ==> P(b) *)
|
paulson@8136
|
136 |
val sym : thm (* a=b ==> b=a *)
|
paulson@8136
|
137 |
val thin_refl : thm (* [|x=x; P|] ==> P *)
|
lcp@104
|
138 |
end;
|
lcp@104
|
139 |
\end{ttbox}
|
lcp@104
|
140 |
Thus, the functor requires the following items:
|
lcp@323
|
141 |
\begin{ttdescription}
|
paulson@2038
|
142 |
\item[Simplifier] should be an instance of the simplifier (see
|
nipkow@3950
|
143 |
Chapter~\ref{chap:simplification}).
|
paulson@4596
|
144 |
|
paulson@4596
|
145 |
\item[\ttindexbold{dest_Trueprop}] should coerce a meta-level formula to the
|
paulson@4596
|
146 |
corresponding object-level one. Typically, it should return $P$ when
|
paulson@4596
|
147 |
applied to the term $\texttt{Trueprop}\,P$ (see example below).
|
paulson@4596
|
148 |
|
haftmann@20975
|
149 |
\item[\ttindexbold{dest_eq}] should return the triple~$((t,u),T)$, where $T$ is
|
paulson@4596
|
150 |
the type of~$t$ and~$u$, when applied to the \ML{} term that
|
paulson@4596
|
151 |
represents~$t=u$. For other terms, it should raise an exception.
|
paulson@4596
|
152 |
|
paulson@4596
|
153 |
\item[\ttindexbold{dest_imp}] should return the pair~$(P,Q)$ when applied to
|
paulson@4596
|
154 |
the \ML{} term that represents the implication $P\imp Q$. For other terms,
|
paulson@4596
|
155 |
it should raise an exception.
|
lcp@104
|
156 |
|
paulson@2038
|
157 |
\item[\tdxbold{eq_reflection}] is the theorem discussed
|
wenzelm@9524
|
158 |
in~\S\ref{sec:setting-up-simp}.
|
wenzelm@9524
|
159 |
|
wenzelm@9524
|
160 |
\item[\tdxbold{rev_eq_reflection}] is the reverse of \texttt{eq_reflection}.
|
lcp@104
|
161 |
|
lcp@323
|
162 |
\item[\tdxbold{imp_intr}] should be the implies introduction
|
lcp@104
|
163 |
rule $(\Var{P}\Imp\Var{Q})\Imp \Var{P}\imp\Var{Q}$.
|
lcp@104
|
164 |
|
lcp@323
|
165 |
\item[\tdxbold{rev_mp}] should be the `reversed' implies elimination
|
lcp@104
|
166 |
rule $\List{\Var{P}; \;\Var{P}\imp\Var{Q}} \Imp \Var{Q}$.
|
lcp@104
|
167 |
|
paulson@2038
|
168 |
\item[\tdxbold{subst}] should be the substitution rule
|
paulson@2038
|
169 |
$\List{\Var{a}=\Var{b};\; \Var{P}(\Var{a})} \Imp \Var{P}(\Var{b})$.
|
paulson@2038
|
170 |
|
paulson@2038
|
171 |
\item[\tdxbold{sym}] should be the symmetry rule
|
paulson@2038
|
172 |
$\Var{a}=\Var{b}\Imp\Var{b}=\Var{a}$.
|
paulson@4596
|
173 |
|
paulson@4596
|
174 |
\item[\tdxbold{thin_refl}] should be the rule
|
paulson@4596
|
175 |
$\List{\Var{a}=\Var{a};\; \Var{P}} \Imp \Var{P}$, which is used to erase
|
paulson@4596
|
176 |
trivial equalities.
|
lcp@323
|
177 |
\end{ttdescription}
|
paulson@2038
|
178 |
%
|
paulson@4596
|
179 |
The functor resides in file \texttt{Provers/hypsubst.ML} in the Isabelle
|
lcp@104
|
180 |
distribution directory. It is not sensitive to the precise formalization
|
lcp@104
|
181 |
of the object-logic. It is not concerned with the names of the equality
|
paulson@4596
|
182 |
and implication symbols, or the types of formula and terms.
|
paulson@4596
|
183 |
|
paulson@4596
|
184 |
Coding the functions \texttt{dest_Trueprop}, \texttt{dest_eq} and
|
paulson@4596
|
185 |
\texttt{dest_imp} requires knowledge of Isabelle's representation of terms.
|
paulson@4596
|
186 |
For \texttt{FOL}, they are declared by
|
lcp@104
|
187 |
\begin{ttbox}
|
paulson@4596
|
188 |
fun dest_Trueprop (Const ("Trueprop", _) $ P) = P
|
paulson@4596
|
189 |
| dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);
|
paulson@4596
|
190 |
|
haftmann@20975
|
191 |
fun dest_eq (Const("op =",T) $ t $ u) = ((t, u), domain_type T)
|
paulson@4596
|
192 |
|
paulson@4596
|
193 |
fun dest_imp (Const("op -->",_) $ A $ B) = (A, B)
|
paulson@4596
|
194 |
| dest_imp t = raise TERM ("dest_imp", [t]);
|
lcp@104
|
195 |
\end{ttbox}
|
paulson@4596
|
196 |
Recall that \texttt{Trueprop} is the coercion from type~$o$ to type~$prop$,
|
paulson@4596
|
197 |
while \hbox{\tt op =} is the internal name of the infix operator~\texttt{=}.
|
paulson@4596
|
198 |
Function \ttindexbold{domain_type}, given the function type $S\To T$, returns
|
paulson@4596
|
199 |
the type~$S$. Pattern-matching expresses the function concisely, using
|
paulson@4596
|
200 |
wildcards~({\tt_}) for the types.
|
lcp@104
|
201 |
|
paulson@4596
|
202 |
The tactic \texttt{hyp_subst_tac} works as follows. First, it identifies a
|
paulson@4596
|
203 |
suitable equality assumption, possibly re-orienting it using~\texttt{sym}.
|
paulson@4596
|
204 |
Then it moves other assumptions into the conclusion of the goal, by repeatedly
|
paulson@4596
|
205 |
calling \texttt{etac~rev_mp}. Then, it uses \texttt{asm_full_simp_tac} or
|
paulson@4596
|
206 |
\texttt{ssubst} to substitute throughout the subgoal. (If the equality
|
paulson@4596
|
207 |
involves unknowns then it must use \texttt{ssubst}.) Then, it deletes the
|
paulson@2038
|
208 |
equality. Finally, it moves the assumptions back to their original positions
|
paulson@2038
|
209 |
by calling \hbox{\tt resolve_tac\ts[imp_intr]}.
|
lcp@104
|
210 |
|
lcp@323
|
211 |
\index{equality|)}\index{tactics!substitution|)}
|
wenzelm@5371
|
212 |
|
wenzelm@5371
|
213 |
|
wenzelm@5371
|
214 |
%%% Local Variables:
|
wenzelm@5371
|
215 |
%%% mode: latex
|
wenzelm@5371
|
216 |
%%% TeX-master: "ref"
|
wenzelm@5371
|
217 |
%%% End:
|