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