|
1 %% $Id$ |
|
2 \chapter{Substitution Tactics} \label{substitution} |
|
3 \index{substitution|(} |
|
4 Replacing equals by equals is a basic form of reasoning. Isabelle supports |
|
5 several kinds of equality reasoning. {\bf Substitution} means to replace |
|
6 free occurrences of~$t$ by~$u$ in a subgoal. This is easily done, given an |
|
7 equality $t=u$, provided the logic possesses the appropriate rule --- |
|
8 unless you want to substitute even in the assumptions. The tactic |
|
9 \ttindex{hyp_subst_tac} performs substitution in the assumptions, but it |
|
10 works via object-level implication, and therefore must be specially set up |
|
11 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 equalities. |
|
18 Chapter~\ref{simp-chap} discusses Isabelle's rewriting tactics. |
|
19 |
|
20 |
|
21 \section{Simple substitution} |
|
22 \index{substitution!simple} |
|
23 Many logics include a substitution rule of the form\indexbold{*subst} |
|
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 well-behaved.\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} |
|
37 resolve_tac [eqth RS subst] \(i\) {\it.} |
|
38 \end{ttbox} |
|
39 To replace $t$ by~$u$ in |
|
40 subgoal~$i$, use |
|
41 \begin{ttbox} |
|
42 resolve_tac [eqth RS ssubst] \(i\) {\it,} |
|
43 \end{ttbox} |
|
44 where \ttindexbold{ssubst} is the `swapped' substitution rule |
|
45 $$ \List{\Var{a}=\Var{b}; \Var{P}(\Var{b})} \Imp |
|
46 \Var{P}(\Var{a}). \eqno(ssubst)$$ |
|
47 If \ttindex{sym} denotes the symmetry rule |
|
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} |
|
51 (for the usual equality laws). |
|
52 |
|
53 Elim-resolution is well-behaved with assumptions of the form $t=u$. |
|
54 To replace $u$ by~$t$ or $t$ by~$u$ in subgoal~$i$, use |
|
55 \begin{ttbox} |
|
56 eresolve_tac [subst] \(i\) {\it or} eresolve_tac [ssubst] \(i\) {\it.} |
|
57 \end{ttbox} |
|
58 |
|
59 |
|
60 \section{Substitution in the hypotheses} |
|
61 \index{substitution!in hypotheses} |
|
62 Substitution rules, like other rules of natural deduction, do not affect |
|
63 the assumptions. This can be inconvenient. Consider proving the subgoal |
|
64 \[ \List{c=a; c=b} \Imp a=b. \] |
|
65 Calling \hbox{\tt eresolve_tac [ssubst] \(i\)} simply discards the |
|
66 assumption~$c=a$, since $c$ does not occur in~$a=b$. Of course, we can |
|
67 work out a solution. First apply \hbox{\tt eresolve_tac [subst] \(i\)}, |
|
68 replacing~$a$ by~$c$: |
|
69 \[ \List{c=b} \Imp c=b \] |
|
70 Equality reasoning can be difficult, but this trivial proof requires |
|
71 nothing more sophisticated than substitution in the assumptions. |
|
72 Object-logics that include the rule~$(subst)$ provide a tactic for this |
|
73 purpose: |
|
74 \begin{ttbox} |
|
75 hyp_subst_tac : int -> tactic |
|
76 \end{ttbox} |
|
77 \begin{description} |
|
78 \item[\ttindexbold{hyp_subst_tac} {\it i}] |
|
79 selects an equality assumption of the form $t=u$ or $u=t$, where $t$ is a |
|
80 free variable or parameter. Deleting this assumption, it replaces $t$ |
|
81 by~$u$ throughout subgoal~$i$, including the other assumptions. |
|
82 \end{description} |
|
83 The term being replaced must be a free variable or parameter. Substitution |
|
84 for constants is usually unhelpful, since they may appear in other |
|
85 theorems. For instance, the best way to use the assumption $0=1$ is to |
|
86 contradict a theorem that states $0\not=1$, rather than to replace 0 by~1 |
|
87 in the subgoal! |
|
88 |
|
89 Replacing a free variable causes similar problems if they appear in the |
|
90 premises of a rule being derived --- the substitution affects object-level |
|
91 assumptions, not meta-level assumptions. For instance, replacing~$a$ |
|
92 by~$b$ could make the premise~$P(a)$ worthless. To avoid this problem, call |
|
93 \ttindex{cut_facts_tac} to insert the atomic premises as object-level |
|
94 assumptions. |
|
95 |
|
96 |
|
97 \section{Setting up {\tt hyp_subst_tac}} |
|
98 Many Isabelle object-logics, such as {\tt FOL}, {\tt HOL} and their |
|
99 descendants, come with {\tt hyp_subst_tac} already defined. A few others, |
|
100 such as {\tt CTT}, do not support this tactic because they lack the |
|
101 rule~$(subst)$. When defining a new logic that includes a substitution |
|
102 rule and implication, you must set up {\tt hyp_subst_tac} yourself. It |
|
103 is packaged as the \ML{} functor \ttindex{HypsubstFun}, which takes the |
|
104 argument signature~\ttindexbold{HYPSUBST_DATA}: |
|
105 \begin{ttbox} |
|
106 signature HYPSUBST_DATA = |
|
107 sig |
|
108 val subst : thm |
|
109 val sym : thm |
|
110 val rev_cut_eq : thm |
|
111 val imp_intr : thm |
|
112 val rev_mp : thm |
|
113 val dest_eq : term -> term*term |
|
114 end; |
|
115 \end{ttbox} |
|
116 Thus, the functor requires the following items: |
|
117 \begin{description} |
|
118 \item[\ttindexbold{subst}] should be the substitution rule |
|
119 $\List{\Var{a}=\Var{b};\; \Var{P}(\Var{a})} \Imp \Var{P}(\Var{b})$. |
|
120 |
|
121 \item[\ttindexbold{sym}] should be the symmetry rule |
|
122 $\Var{a}=\Var{b}\Imp\Var{b}=\Var{a}$. |
|
123 |
|
124 \item[\ttindexbold{rev_cut_eq}] should have the form |
|
125 $\List{\Var{a}=\Var{b};\; \Var{a}=\Var{b}\Imp\Var{R}} \Imp \Var{R}$. |
|
126 |
|
127 \item[\ttindexbold{imp_intr}] should be the implies introduction |
|
128 rule $(\Var{P}\Imp\Var{Q})\Imp \Var{P}\imp\Var{Q}$. |
|
129 |
|
130 \item[\ttindexbold{rev_mp}] should be the ``reversed'' implies elimination |
|
131 rule $\List{\Var{P}; \;\Var{P}\imp\Var{Q}} \Imp \Var{Q}$. |
|
132 |
|
133 \item[\ttindexbold{dest_eq}] should return the pair~$(t,u)$ when |
|
134 applied to the \ML{} term that represents~$t=u$. For other terms, it |
|
135 should raise exception~\ttindex{Match}. |
|
136 \end{description} |
|
137 The functor resides in {\tt Provers/hypsubst.ML} on the Isabelle |
|
138 distribution directory. It is not sensitive to the precise formalization |
|
139 of the object-logic. It is not concerned with the names of the equality |
|
140 and implication symbols, or the types of formula and terms. Coding the |
|
141 function {\tt dest_eq} requires knowledge of Isabelle's representation of |
|
142 terms. For {\tt FOL} it is defined by |
|
143 \begin{ttbox} |
|
144 fun dest_eq (Const("Trueprop",_) $ (Const("op =",_)$t$u)) = (t,u); |
|
145 \end{ttbox} |
|
146 Here {\tt Trueprop} is the coercion from type'~$o$ to type~$prop$, while |
|
147 \hbox{\tt op =} is the internal name of the infix operator~{\tt=}. |
|
148 Pattern-matching expresses the function concisely, using wildcards~({\tt_}) |
|
149 to hide the types. |
|
150 |
|
151 Given a subgoal of the form |
|
152 \[ \List{P@1; \cdots ; t=u; \cdots ; P@n} \Imp Q, \] |
|
153 \ttindexbold{hyp_subst_tac} locates a suitable equality |
|
154 assumption and moves it to the last position using elim-resolution on {\tt |
|
155 rev_cut_eq} (possibly re-orienting it using~{\tt sym}): |
|
156 \[ \List{P@1; \cdots ; P@n; t=u} \Imp Q \] |
|
157 Using $n$ calls of \hbox{\tt eresolve_tac [rev_mp]}, it creates the subgoal |
|
158 \[ \List{t=u} \Imp P@1\imp \cdots \imp P@n \imp Q \] |
|
159 By \hbox{\tt eresolve_tac [ssubst]}, it replaces~$t$ by~$u$ throughout: |
|
160 \[ P'@1\imp \cdots \imp P'@n \imp Q' \] |
|
161 Finally, using $n$ calls of \hbox{\tt resolve_tac [imp_intr]}, it restores |
|
162 $P'@1$, \ldots, $P'@n$ as assumptions: |
|
163 \[ \List{P'@n; \cdots ; P'@1} \Imp Q' \] |
|
164 |
|
165 \index{substitution|)} |