
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 objectlevel implication, and therefore must be specially set up 

11 for each suitable objectlogic. 

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 

17 equalities, while rewriting handles general equalities. 

18 Chapter~\ref{simpchap} 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 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} 

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 Elimresolution is wellbehaved 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 Objectlogics 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 objectlevel 

91 assumptions, not metalevel 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 objectlevel 

94 assumptions. 

95 

96 

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

98 Many Isabelle objectlogics, 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 objectlogic. 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 Patternmatching 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 elimresolution on {\tt 

155 rev_cut_eq} (possibly reorienting 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)} 