author  wenzelm 
Sun, 29 Jan 2012 22:12:25 +0100  
changeset 46278  408e3acfdbb9 
parent 46277  aea65ff733b4 
child 46295  2548a85b0e02 
permissions  rwrr 
30184
37969710e61f
removed parts of the manual that are clearly obsolete, or covered by
wenzelm
parents:
17818
diff
changeset

1 

104  2 
\chapter{Tactics} \label{tactics} 
30184
37969710e61f
removed parts of the manual that are clearly obsolete, or covered by
wenzelm
parents:
17818
diff
changeset

3 
\index{tactics(} 
104  4 

5 
\section{Other basic tactics} 

6 

7 
\subsection{Inserting premises and facts}\label{cut_facts_tac} 

323  8 
\index{tactics!for inserting facts}\index{assumptions!inserting} 
104  9 
\begin{ttbox} 
10 
cut_facts_tac : thm list > int > tactic 

286  11 
cut_inst_tac : (string*string)list > thm > int > tactic 
104  12 
\end{ttbox} 
2039
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

13 
These tactics add assumptions to a subgoal. 
323  14 
\begin{ttdescription} 
104  15 
\item[\ttindexbold{cut_facts_tac} {\it thms} {\it i}] 
16 
adds the {\it thms} as new assumptions to subgoal~$i$. Once they have 

286  17 
been inserted as assumptions, they become subject to tactics such as {\tt 
18 
eresolve_tac} and {\tt rewrite_goals_tac}. Only rules with no premises 

19 
are inserted: Isabelle cannot use assumptions that contain $\Imp$ 

20 
or~$\Forall$. Sometimes the theorems are premises of a rule being 

21 
derived, returned by~{\tt goal}; instead of calling this tactic, you 

22 
could state the goal with an outermost metaquantifier. 

23 

24 
\item[\ttindexbold{cut_inst_tac} {\it insts} {\it thm} {\it i}] 

25 
instantiates the {\it thm} with the instantiations {\it insts}, as 

7491  26 
described in {\S}\ref{res_inst_tac}. It adds the resulting theorem as a 
286  27 
new assumption to subgoal~$i$. 
104  28 

323  29 
\end{ttdescription} 
104  30 

31 

4317  32 
\subsection{Definitions and metalevel rewriting} \label{sec:rewrite_goals} 
2039
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

33 
\index{tactics!metarewritingbold}\index{metarewritingbold} 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

34 
\index{definitions} 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

35 

79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

36 
Definitions in Isabelle have the form $t\equiv u$, where $t$ is typically a 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

37 
constant or a constant applied to a list of variables, for example $\it 
4317  38 
sqr(n)\equiv n\times n$. Conditional definitions, $\phi\Imp t\equiv u$, 
39 
are also supported. {\bf Unfolding} the definition ${t\equiv u}$ means using 

2039
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

40 
it as a rewrite rule, replacing~$t$ by~$u$ throughout a theorem. {\bf 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

41 
Folding} $t\equiv u$ means replacing~$u$ by~$t$. Rewriting continues until 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

42 
no rewrites are applicable to any subterm. 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

43 

79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

44 
There are rules for unfolding and folding definitions; Isabelle does not do 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

45 
this automatically. The corresponding tactics rewrite the proof state, 
46257  46 
yielding a single next state. 
2039
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

47 
\begin{ttbox} 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

48 
rewrite_goals_tac : thm list > tactic 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

49 
fold_goals_tac : thm list > tactic 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

50 
\end{ttbox} 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

51 
\begin{ttdescription} 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

52 
\item[\ttindexbold{rewrite_goals_tac} {\it defs}] 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

53 
unfolds the {\it defs} throughout the subgoals of the proof state, while 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

54 
leaving the main goal unchanged. Use \ttindex{SELECT_GOAL} to restrict it to a 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

55 
particular subgoal. 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

56 

79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

57 
\item[\ttindexbold{fold_goals_tac} {\it defs}] 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

58 
folds the {\it defs} throughout the subgoals of the proof state, while 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

59 
leaving the main goal unchanged. 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

60 
\end{ttdescription} 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

61 

4317  62 
\begin{warn} 
63 
These tactics only cope with definitions expressed as metalevel 

64 
equalities ($\equiv$). More general equivalences are handled by the 

65 
simplifier, provided that it is set up appropriately for your logic 

66 
(see Chapter~\ref{chap:simplification}). 

67 
\end{warn} 

2039
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

68 

1212  69 

104  70 
\subsection{Composition: resolution without lifting} 
323  71 
\index{tactics!for composition} 
104  72 
\begin{ttbox} 
73 
compose_tac: (bool * thm * int) > int > tactic 

74 
\end{ttbox} 

332  75 
{\bf Composing} two rules means resolving them without prior lifting or 
104  76 
renaming of unknowns. This lowlevel operation, which underlies the 
77 
resolution tactics, may occasionally be useful for special effects. 

78 
A typical application is \ttindex{res_inst_tac}, which lifts and instantiates a 

79 
rule, then passes the result to {\tt compose_tac}. 

323  80 
\begin{ttdescription} 
104  81 
\item[\ttindexbold{compose_tac} ($flag$, $rule$, $m$) $i$] 
82 
refines subgoal~$i$ using $rule$, without lifting. The $rule$ is taken to 

83 
have the form $\List{\psi@1; \ldots; \psi@m} \Imp \psi$, where $\psi$ need 

323  84 
not be atomic; thus $m$ determines the number of new subgoals. If 
104  85 
$flag$ is {\tt true} then it performs elimresolution  it solves the 
86 
first premise of~$rule$ by assumption and deletes that assumption. 

323  87 
\end{ttdescription} 
104  88 

89 

4276  90 
\section{*Managing lots of rules} 
104  91 
These operations are not intended for interactive use. They are concerned 
92 
with the processing of large numbers of rules in automatic proof 

93 
strategies. Higherorder resolution involving a long list of rules is 

94 
slow. Filtering techniques can shorten the list of rules given to 

2039
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

95 
resolution, and can also detect whether a subgoal is too flexible, 
104  96 
with too many rules applicable. 
97 

98 
\subsection{Combined resolution and elimresolution} \label{biresolve_tac} 

99 
\index{tactics!resolution} 

100 
\begin{ttbox} 

101 
biresolve_tac : (bool*thm)list > int > tactic 

102 
bimatch_tac : (bool*thm)list > int > tactic 

103 
subgoals_of_brl : bool*thm > int 

104 
lessb : (bool*thm) * (bool*thm) > bool 

105 
\end{ttbox} 

106 
{\bf Biresolution} takes a list of $\it (flag,rule)$ pairs. For each 

107 
pair, it applies resolution if the flag is~{\tt false} and 

108 
elimresolution if the flag is~{\tt true}. A single tactic call handles a 

109 
mixture of introduction and elimination rules. 

110 

323  111 
\begin{ttdescription} 
104  112 
\item[\ttindexbold{biresolve_tac} {\it brls} {\it i}] 
113 
refines the proof state by resolution or elimresolution on each rule, as 

114 
indicated by its flag. It affects subgoal~$i$ of the proof state. 

115 

116 
\item[\ttindexbold{bimatch_tac}] 

117 
is like {\tt biresolve_tac}, but performs matching: unknowns in the 

7491  118 
proof state are never updated (see~{\S}\ref{match_tac}). 
104  119 

120 
\item[\ttindexbold{subgoals_of_brl}({\it flag},{\it rule})] 

4597
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4317
diff
changeset

121 
returns the number of new subgoals that bires\o\lu\tion would yield for the 
104  122 
pair (if applied to a suitable subgoal). This is $n$ if the flag is 
123 
{\tt false} and $n1$ if the flag is {\tt true}, where $n$ is the number 

124 
of premises of the rule. Elimresolution yields one fewer subgoal than 

125 
ordinary resolution because it solves the major premise by assumption. 

126 

127 
\item[\ttindexbold{lessb} ({\it brl1},{\it brl2})] 

128 
returns the result of 

129 
\begin{ttbox} 

332  130 
subgoals_of_brl{\it brl1} < subgoals_of_brl{\it brl2} 
104  131 
\end{ttbox} 
323  132 
\end{ttdescription} 
104  133 
Note that \hbox{\tt sort lessb {\it brls}} sorts a list of $\it 
134 
(flag,rule)$ pairs by the number of new subgoals they will yield. Thus, 

135 
those that yield the fewest subgoals should be tried first. 

136 

137 

323  138 
\subsection{Discrimination nets for fast resolution}\label{filt_resolve_tac} 
104  139 
\index{discrimination netsbold} 
140 
\index{tactics!resolution} 

141 
\begin{ttbox} 

142 
net_resolve_tac : thm list > int > tactic 

143 
net_match_tac : thm list > int > tactic 

144 
net_biresolve_tac: (bool*thm) list > int > tactic 

145 
net_bimatch_tac : (bool*thm) list > int > tactic 

146 
filt_resolve_tac : thm list > int > int > tactic 

147 
could_unify : term*term>bool 

8136  148 
filter_thms : (term*term>bool) > int*term*thm list > thm{\ts}list 
104  149 
\end{ttbox} 
323  150 
The module {\tt Net} implements a discrimination net data structure for 
104  151 
fast selection of rules \cite[Chapter 14]{charniak80}. A term is 
152 
classified by the symbol list obtained by flattening it in preorder. 

153 
The flattening takes account of function applications, constants, and free 

154 
and bound variables; it identifies all unknowns and also regards 

323  155 
\index{lambda abs@$\lambda$abstractions} 
104  156 
$\lambda$abstractions as unknowns, since they could $\eta$contract to 
157 
anything. 

158 

159 
A discrimination net serves as a polymorphic dictionary indexed by terms. 

160 
The module provides various functions for inserting and removing items from 

161 
nets. It provides functions for returning all items whose term could match 

162 
or unify with a target term. The matching and unification tests are 

163 
overly lax (due to the identifications mentioned above) but they serve as 

164 
useful filters. 

165 

166 
A net can store introduction rules indexed by their conclusion, and 

167 
elimination rules indexed by their major premise. Isabelle provides 

323  168 
several functions for `compiling' long lists of rules into fast 
104  169 
resolution tactics. When supplied with a list of theorems, these functions 
170 
build a discrimination net; the net is used when the tactic is applied to a 

332  171 
goal. To avoid repeatedly constructing the nets, use currying: bind the 
104  172 
resulting tactics to \ML{} identifiers. 
173 

323  174 
\begin{ttdescription} 
104  175 
\item[\ttindexbold{net_resolve_tac} {\it thms}] 
176 
builds a discrimination net to obtain the effect of a similar call to {\tt 

177 
resolve_tac}. 

178 

179 
\item[\ttindexbold{net_match_tac} {\it thms}] 

180 
builds a discrimination net to obtain the effect of a similar call to {\tt 

181 
match_tac}. 

182 

183 
\item[\ttindexbold{net_biresolve_tac} {\it brls}] 

184 
builds a discrimination net to obtain the effect of a similar call to {\tt 

185 
biresolve_tac}. 

186 

187 
\item[\ttindexbold{net_bimatch_tac} {\it brls}] 

188 
builds a discrimination net to obtain the effect of a similar call to {\tt 

189 
bimatch_tac}. 

190 

191 
\item[\ttindexbold{filt_resolve_tac} {\it thms} {\it maxr} {\it i}] 

192 
uses discrimination nets to extract the {\it thms} that are applicable to 

193 
subgoal~$i$. If more than {\it maxr\/} theorems are applicable then the 

194 
tactic fails. Otherwise it calls {\tt resolve_tac}. 

195 

196 
This tactic helps avoid runaway instantiation of unknowns, for example in 

197 
type inference. 

198 

199 
\item[\ttindexbold{could_unify} ({\it t},{\it u})] 

323  200 
returns {\tt false} if~$t$ and~$u$ are `obviously' nonunifiable, and 
104  201 
otherwise returns~{\tt true}. It assumes all variables are distinct, 
202 
reporting that {\tt ?a=?a} may unify with {\tt 0=1}. 

203 

204 
\item[\ttindexbold{filter_thms} $could\; (limit,prem,thms)$] 

205 
returns the list of potentially resolvable rules (in {\it thms\/}) for the 

206 
subgoal {\it prem}, using the predicate {\it could\/} to compare the 

207 
conclusion of the subgoal with the conclusion of each rule. The resulting list 

208 
is no longer than {\it limit}. 

323  209 
\end{ttdescription} 
104  210 

211 
\index{tactics)} 

5371  212 

213 

214 
%%% Local Variables: 

215 
%%% mode: latex 

216 
%%% TeXmaster: "ref" 

217 
%%% End: 