summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

doc-src/Ref/substitution.tex

author | wenzelm |

Mon Aug 28 13:52:38 2000 +0200 (2000-08-28) | |

changeset 9695 | ec7d7f877712 |

parent 9524 | 5721615da108 |

child 20975 | 5bfa2e4ed789 |

permissions | -rw-r--r-- |

proper setup of iman.sty/extra.sty/ttbox.sty;

1 %% $Id$

2 \chapter{Substitution Tactics} \label{substitution}

3 \index{tactics!substitution|(}\index{equality|(}

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.

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.

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).

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}

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.

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.

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!

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.

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}).

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).

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.

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.

157 \item[\tdxbold{eq_reflection}] is the theorem discussed

158 in~\S\ref{sec:setting-up-simp}.

160 \item[\tdxbold{rev_eq_reflection}] is the reverse of \texttt{eq_reflection}.

162 \item[\tdxbold{imp_intr}] should be the implies introduction

163 rule $(\Var{P}\Imp\Var{Q})\Imp \Var{P}\imp\Var{Q}$.

165 \item[\tdxbold{rev_mp}] should be the `reversed' implies elimination

166 rule $\List{\Var{P}; \;\Var{P}\imp\Var{Q}} \Imp \Var{Q}$.

168 \item[\tdxbold{subst}] should be the substitution rule

169 $\List{\Var{a}=\Var{b};\; \Var{P}(\Var{a})} \Imp \Var{P}(\Var{b})$.

171 \item[\tdxbold{sym}] should be the symmetry rule

172 $\Var{a}=\Var{b}\Imp\Var{b}=\Var{a}$.

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.

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]);

191 fun dest_eq (Const("op =",T) $ t $ u) = (t, u, domain_type T)

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.

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]}.

211 \index{equality|)}\index{tactics!substitution|)}

214 %%% Local Variables:

215 %%% mode: latex

216 %%% TeX-master: "ref"

217 %%% End: