1.1 --- a/doc-src/IsarImplementation/Thy/document/tactic.tex Mon Feb 16 20:25:21 2009 +0100
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,512 +0,0 @@
1.4 -%
1.5 -\begin{isabellebody}%
1.6 -\def\isabellecontext{tactic}%
1.7 -%
1.8 -\isadelimtheory
1.9 -\isanewline
1.10 -\isanewline
1.11 -\isanewline
1.12 -%
1.13 -\endisadelimtheory
1.14 -%
1.15 -\isatagtheory
1.16 -\isacommand{theory}\isamarkupfalse%
1.17 -\ tactic\ \isakeyword{imports}\ base\ \isakeyword{begin}%
1.18 -\endisatagtheory
1.19 -{\isafoldtheory}%
1.20 -%
1.21 -\isadelimtheory
1.22 -%
1.23 -\endisadelimtheory
1.24 -%
1.25 -\isamarkupchapter{Tactical reasoning%
1.26 -}
1.27 -\isamarkuptrue%
1.28 -%
1.29 -\begin{isamarkuptext}%
1.30 -Tactical reasoning works by refining the initial claim in a
1.31 - backwards fashion, until a solved form is reached. A \isa{goal}
1.32 - consists of several subgoals that need to be solved in order to
1.33 - achieve the main statement; zero subgoals means that the proof may
1.34 - be finished. A \isa{tactic} is a refinement operation that maps
1.35 - a goal to a lazy sequence of potential successors. A \isa{tactical} is a combinator for composing tactics.%
1.36 -\end{isamarkuptext}%
1.37 -\isamarkuptrue%
1.38 -%
1.39 -\isamarkupsection{Goals \label{sec:tactical-goals}%
1.40 -}
1.41 -\isamarkuptrue%
1.42 -%
1.43 -\begin{isamarkuptext}%
1.44 -Isabelle/Pure represents a goal\glossary{Tactical goal}{A theorem of
1.45 - \seeglossary{Horn Clause} form stating that a number of subgoals
1.46 - imply the main conclusion, which is marked as a protected
1.47 - proposition.} as a theorem stating that the subgoals imply the main
1.48 - goal: \isa{A\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymLongrightarrow}\ A\isactrlsub n\ {\isasymLongrightarrow}\ C}. The outermost goal
1.49 - structure is that of a Horn Clause\glossary{Horn Clause}{An iterated
1.50 - implication \isa{A\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymLongrightarrow}\ A\isactrlsub n\ {\isasymLongrightarrow}\ C}, without any
1.51 - outermost quantifiers. Strictly speaking, propositions \isa{A\isactrlsub i} need to be atomic in Horn Clauses, but Isabelle admits
1.52 - arbitrary substructure here (nested \isa{{\isasymLongrightarrow}} and \isa{{\isasymAnd}}
1.53 - connectives).}: i.e.\ an iterated implication without any
1.54 - quantifiers\footnote{Recall that outermost \isa{{\isasymAnd}x{\isachardot}\ {\isasymphi}{\isacharbrackleft}x{\isacharbrackright}} is
1.55 - always represented via schematic variables in the body: \isa{{\isasymphi}{\isacharbrackleft}{\isacharquery}x{\isacharbrackright}}. These variables may get instantiated during the course of
1.56 - reasoning.}. For \isa{n\ {\isacharequal}\ {\isadigit{0}}} a goal is called ``solved''.
1.57 -
1.58 - The structure of each subgoal \isa{A\isactrlsub i} is that of a general
1.59 - Hereditary Harrop Formula \isa{{\isasymAnd}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymAnd}x\isactrlsub k{\isachardot}\ H\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymLongrightarrow}\ H\isactrlsub m\ {\isasymLongrightarrow}\ B} in
1.60 - normal form. Here \isa{x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub k} are goal parameters, i.e.\
1.61 - arbitrary-but-fixed entities of certain types, and \isa{H\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ H\isactrlsub m} are goal hypotheses, i.e.\ facts that may be assumed locally.
1.62 - Together, this forms the goal context of the conclusion \isa{B} to
1.63 - be established. The goal hypotheses may be again arbitrary
1.64 - Hereditary Harrop Formulas, although the level of nesting rarely
1.65 - exceeds 1--2 in practice.
1.66 -
1.67 - The main conclusion \isa{C} is internally marked as a protected
1.68 - proposition\glossary{Protected proposition}{An arbitrarily
1.69 - structured proposition \isa{C} which is forced to appear as
1.70 - atomic by wrapping it into a propositional identity operator;
1.71 - notation \isa{{\isacharhash}C}. Protecting a proposition prevents basic
1.72 - inferences from entering into that structure for the time being.},
1.73 - which is represented explicitly by the notation \isa{{\isacharhash}C}. This
1.74 - ensures that the decomposition into subgoals and main conclusion is
1.75 - well-defined for arbitrarily structured claims.
1.76 -
1.77 - \medskip Basic goal management is performed via the following
1.78 - Isabelle/Pure rules:
1.79 -
1.80 - \[
1.81 - \infer[\isa{{\isacharparenleft}init{\isacharparenright}}]{\isa{C\ {\isasymLongrightarrow}\ {\isacharhash}C}}{} \qquad
1.82 - \infer[\isa{{\isacharparenleft}finish{\isacharparenright}}]{\isa{C}}{\isa{{\isacharhash}C}}
1.83 - \]
1.84 -
1.85 - \medskip The following low-level variants admit general reasoning
1.86 - with protected propositions:
1.87 -
1.88 - \[
1.89 - \infer[\isa{{\isacharparenleft}protect{\isacharparenright}}]{\isa{{\isacharhash}C}}{\isa{C}} \qquad
1.90 - \infer[\isa{{\isacharparenleft}conclude{\isacharparenright}}]{\isa{A\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymLongrightarrow}\ A\isactrlsub n\ {\isasymLongrightarrow}\ C}}{\isa{A\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymLongrightarrow}\ A\isactrlsub n\ {\isasymLongrightarrow}\ {\isacharhash}C}}
1.91 - \]%
1.92 -\end{isamarkuptext}%
1.93 -\isamarkuptrue%
1.94 -%
1.95 -\isadelimmlref
1.96 -%
1.97 -\endisadelimmlref
1.98 -%
1.99 -\isatagmlref
1.100 -%
1.101 -\begin{isamarkuptext}%
1.102 -\begin{mldecls}
1.103 - \indexml{Goal.init}\verb|Goal.init: cterm -> thm| \\
1.104 - \indexml{Goal.finish}\verb|Goal.finish: thm -> thm| \\
1.105 - \indexml{Goal.protect}\verb|Goal.protect: thm -> thm| \\
1.106 - \indexml{Goal.conclude}\verb|Goal.conclude: thm -> thm| \\
1.107 - \end{mldecls}
1.108 -
1.109 - \begin{description}
1.110 -
1.111 - \item \verb|Goal.init|~\isa{C} initializes a tactical goal from
1.112 - the well-formed proposition \isa{C}.
1.113 -
1.114 - \item \verb|Goal.finish|~\isa{thm} checks whether theorem
1.115 - \isa{thm} is a solved goal (no subgoals), and concludes the
1.116 - result by removing the goal protection.
1.117 -
1.118 - \item \verb|Goal.protect|~\isa{thm} protects the full statement
1.119 - of theorem \isa{thm}.
1.120 -
1.121 - \item \verb|Goal.conclude|~\isa{thm} removes the goal
1.122 - protection, even if there are pending subgoals.
1.123 -
1.124 - \end{description}%
1.125 -\end{isamarkuptext}%
1.126 -\isamarkuptrue%
1.127 -%
1.128 -\endisatagmlref
1.129 -{\isafoldmlref}%
1.130 -%
1.131 -\isadelimmlref
1.132 -%
1.133 -\endisadelimmlref
1.134 -%
1.135 -\isamarkupsection{Tactics%
1.136 -}
1.137 -\isamarkuptrue%
1.138 -%
1.139 -\begin{isamarkuptext}%
1.140 -A \isa{tactic} is a function \isa{goal\ {\isasymrightarrow}\ goal\isactrlsup {\isacharasterisk}\isactrlsup {\isacharasterisk}} that
1.141 - maps a given goal state (represented as a theorem, cf.\
1.142 - \secref{sec:tactical-goals}) to a lazy sequence of potential
1.143 - successor states. The underlying sequence implementation is lazy
1.144 - both in head and tail, and is purely functional in \emph{not}
1.145 - supporting memoing.\footnote{The lack of memoing and the strict
1.146 - nature of SML requires some care when working with low-level
1.147 - sequence operations, to avoid duplicate or premature evaluation of
1.148 - results.}
1.149 -
1.150 - An \emph{empty result sequence} means that the tactic has failed: in
1.151 - a compound tactic expressions other tactics might be tried instead,
1.152 - or the whole refinement step might fail outright, producing a
1.153 - toplevel error message. When implementing tactics from scratch, one
1.154 - should take care to observe the basic protocol of mapping regular
1.155 - error conditions to an empty result; only serious faults should
1.156 - emerge as exceptions.
1.157 -
1.158 - By enumerating \emph{multiple results}, a tactic can easily express
1.159 - the potential outcome of an internal search process. There are also
1.160 - combinators for building proof tools that involve search
1.161 - systematically, see also \secref{sec:tacticals}.
1.162 -
1.163 - \medskip As explained in \secref{sec:tactical-goals}, a goal state
1.164 - essentially consists of a list of subgoals that imply the main goal
1.165 - (conclusion). Tactics may operate on all subgoals or on a
1.166 - particularly specified subgoal, but must not change the main
1.167 - conclusion (apart from instantiating schematic goal variables).
1.168 -
1.169 - Tactics with explicit \emph{subgoal addressing} are of the form
1.170 - \isa{int\ {\isasymrightarrow}\ tactic} and may be applied to a particular subgoal
1.171 - (counting from 1). If the subgoal number is out of range, the
1.172 - tactic should fail with an empty result sequence, but must not raise
1.173 - an exception!
1.174 -
1.175 - Operating on a particular subgoal means to replace it by an interval
1.176 - of zero or more subgoals in the same place; other subgoals must not
1.177 - be affected, apart from instantiating schematic variables ranging
1.178 - over the whole goal state.
1.179 -
1.180 - A common pattern of composing tactics with subgoal addressing is to
1.181 - try the first one, and then the second one only if the subgoal has
1.182 - not been solved yet. Special care is required here to avoid bumping
1.183 - into unrelated subgoals that happen to come after the original
1.184 - subgoal. Assuming that there is only a single initial subgoal is a
1.185 - very common error when implementing tactics!
1.186 -
1.187 - Tactics with internal subgoal addressing should expose the subgoal
1.188 - index as \isa{int} argument in full generality; a hardwired
1.189 - subgoal 1 inappropriate.
1.190 -
1.191 - \medskip The main well-formedness conditions for proper tactics are
1.192 - summarized as follows.
1.193 -
1.194 - \begin{itemize}
1.195 -
1.196 - \item General tactic failure is indicated by an empty result, only
1.197 - serious faults may produce an exception.
1.198 -
1.199 - \item The main conclusion must not be changed, apart from
1.200 - instantiating schematic variables.
1.201 -
1.202 - \item A tactic operates either uniformly on all subgoals, or
1.203 - specifically on a selected subgoal (without bumping into unrelated
1.204 - subgoals).
1.205 -
1.206 - \item Range errors in subgoal addressing produce an empty result.
1.207 -
1.208 - \end{itemize}
1.209 -
1.210 - Some of these conditions are checked by higher-level goal
1.211 - infrastructure (\secref{sec:results}); others are not checked
1.212 - explicitly, and violating them merely results in ill-behaved tactics
1.213 - experienced by the user (e.g.\ tactics that insist in being
1.214 - applicable only to singleton goals, or disallow composition with
1.215 - basic tacticals).%
1.216 -\end{isamarkuptext}%
1.217 -\isamarkuptrue%
1.218 -%
1.219 -\isadelimmlref
1.220 -%
1.221 -\endisadelimmlref
1.222 -%
1.223 -\isatagmlref
1.224 -%
1.225 -\begin{isamarkuptext}%
1.226 -\begin{mldecls}
1.227 - \indexmltype{tactic}\verb|type tactic = thm -> thm Seq.seq| \\
1.228 - \indexml{no\_tac}\verb|no_tac: tactic| \\
1.229 - \indexml{all\_tac}\verb|all_tac: tactic| \\
1.230 - \indexml{print\_tac}\verb|print_tac: string -> tactic| \\[1ex]
1.231 - \indexml{PRIMITIVE}\verb|PRIMITIVE: (thm -> thm) -> tactic| \\[1ex]
1.232 - \indexml{SUBGOAL}\verb|SUBGOAL: (term * int -> tactic) -> int -> tactic| \\
1.233 - \indexml{CSUBGOAL}\verb|CSUBGOAL: (cterm * int -> tactic) -> int -> tactic| \\
1.234 - \end{mldecls}
1.235 -
1.236 - \begin{description}
1.237 -
1.238 - \item \verb|tactic| represents tactics. The well-formedness
1.239 - conditions described above need to be observed. See also \hyperlink{file.~~/src/Pure/General/seq.ML}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}General{\isacharslash}seq{\isachardot}ML}}}} for the underlying implementation of
1.240 - lazy sequences.
1.241 -
1.242 - \item \verb|int -> tactic| represents tactics with explicit
1.243 - subgoal addressing, with well-formedness conditions as described
1.244 - above.
1.245 -
1.246 - \item \verb|no_tac| is a tactic that always fails, returning the
1.247 - empty sequence.
1.248 -
1.249 - \item \verb|all_tac| is a tactic that always succeeds, returning a
1.250 - singleton sequence with unchanged goal state.
1.251 -
1.252 - \item \verb|print_tac|~\isa{message} is like \verb|all_tac|, but
1.253 - prints a message together with the goal state on the tracing
1.254 - channel.
1.255 -
1.256 - \item \verb|PRIMITIVE|~\isa{rule} turns a primitive inference rule
1.257 - into a tactic with unique result. Exception \verb|THM| is considered
1.258 - a regular tactic failure and produces an empty result; other
1.259 - exceptions are passed through.
1.260 -
1.261 - \item \verb|SUBGOAL|~\isa{{\isacharparenleft}fn\ {\isacharparenleft}subgoal{\isacharcomma}\ i{\isacharparenright}\ {\isacharequal}{\isachargreater}\ tactic{\isacharparenright}} is the
1.262 - most basic form to produce a tactic with subgoal addressing. The
1.263 - given abstraction over the subgoal term and subgoal number allows to
1.264 - peek at the relevant information of the full goal state. The
1.265 - subgoal range is checked as required above.
1.266 -
1.267 - \item \verb|CSUBGOAL| is similar to \verb|SUBGOAL|, but passes the
1.268 - subgoal as \verb|cterm| instead of raw \verb|term|. This
1.269 - avoids expensive re-certification in situations where the subgoal is
1.270 - used directly for primitive inferences.
1.271 -
1.272 - \end{description}%
1.273 -\end{isamarkuptext}%
1.274 -\isamarkuptrue%
1.275 -%
1.276 -\endisatagmlref
1.277 -{\isafoldmlref}%
1.278 -%
1.279 -\isadelimmlref
1.280 -%
1.281 -\endisadelimmlref
1.282 -%
1.283 -\isamarkupsubsection{Resolution and assumption tactics \label{sec:resolve-assume-tac}%
1.284 -}
1.285 -\isamarkuptrue%
1.286 -%
1.287 -\begin{isamarkuptext}%
1.288 -\emph{Resolution} is the most basic mechanism for refining a
1.289 - subgoal using a theorem as object-level rule.
1.290 - \emph{Elim-resolution} is particularly suited for elimination rules:
1.291 - it resolves with a rule, proves its first premise by assumption, and
1.292 - finally deletes that assumption from any new subgoals.
1.293 - \emph{Destruct-resolution} is like elim-resolution, but the given
1.294 - destruction rules are first turned into canonical elimination
1.295 - format. \emph{Forward-resolution} is like destruct-resolution, but
1.296 - without deleting the selected assumption. The \isa{r{\isacharslash}e{\isacharslash}d{\isacharslash}f}
1.297 - naming convention is maintained for several different kinds of
1.298 - resolution rules and tactics.
1.299 -
1.300 - Assumption tactics close a subgoal by unifying some of its premises
1.301 - against its conclusion.
1.302 -
1.303 - \medskip All the tactics in this section operate on a subgoal
1.304 - designated by a positive integer. Other subgoals might be affected
1.305 - indirectly, due to instantiation of schematic variables.
1.306 -
1.307 - There are various sources of non-determinism, the tactic result
1.308 - sequence enumerates all possibilities of the following choices (if
1.309 - applicable):
1.310 -
1.311 - \begin{enumerate}
1.312 -
1.313 - \item selecting one of the rules given as argument to the tactic;
1.314 -
1.315 - \item selecting a subgoal premise to eliminate, unifying it against
1.316 - the first premise of the rule;
1.317 -
1.318 - \item unifying the conclusion of the subgoal to the conclusion of
1.319 - the rule.
1.320 -
1.321 - \end{enumerate}
1.322 -
1.323 - Recall that higher-order unification may produce multiple results
1.324 - that are enumerated here.%
1.325 -\end{isamarkuptext}%
1.326 -\isamarkuptrue%
1.327 -%
1.328 -\isadelimmlref
1.329 -%
1.330 -\endisadelimmlref
1.331 -%
1.332 -\isatagmlref
1.333 -%
1.334 -\begin{isamarkuptext}%
1.335 -\begin{mldecls}
1.336 - \indexml{resolve\_tac}\verb|resolve_tac: thm list -> int -> tactic| \\
1.337 - \indexml{eresolve\_tac}\verb|eresolve_tac: thm list -> int -> tactic| \\
1.338 - \indexml{dresolve\_tac}\verb|dresolve_tac: thm list -> int -> tactic| \\
1.339 - \indexml{forward\_tac}\verb|forward_tac: thm list -> int -> tactic| \\[1ex]
1.340 - \indexml{assume\_tac}\verb|assume_tac: int -> tactic| \\
1.341 - \indexml{eq\_assume\_tac}\verb|eq_assume_tac: int -> tactic| \\[1ex]
1.342 - \indexml{match\_tac}\verb|match_tac: thm list -> int -> tactic| \\
1.343 - \indexml{ematch\_tac}\verb|ematch_tac: thm list -> int -> tactic| \\
1.344 - \indexml{dmatch\_tac}\verb|dmatch_tac: thm list -> int -> tactic| \\
1.345 - \end{mldecls}
1.346 -
1.347 - \begin{description}
1.348 -
1.349 - \item \verb|resolve_tac|~\isa{thms\ i} refines the goal state
1.350 - using the given theorems, which should normally be introduction
1.351 - rules. The tactic resolves a rule's conclusion with subgoal \isa{i}, replacing it by the corresponding versions of the rule's
1.352 - premises.
1.353 -
1.354 - \item \verb|eresolve_tac|~\isa{thms\ i} performs elim-resolution
1.355 - with the given theorems, which should normally be elimination rules.
1.356 -
1.357 - \item \verb|dresolve_tac|~\isa{thms\ i} performs
1.358 - destruct-resolution with the given theorems, which should normally
1.359 - be destruction rules. This replaces an assumption by the result of
1.360 - applying one of the rules.
1.361 -
1.362 - \item \verb|forward_tac| is like \verb|dresolve_tac| except that the
1.363 - selected assumption is not deleted. It applies a rule to an
1.364 - assumption, adding the result as a new assumption.
1.365 -
1.366 - \item \verb|assume_tac|~\isa{i} attempts to solve subgoal \isa{i}
1.367 - by assumption (modulo higher-order unification).
1.368 -
1.369 - \item \verb|eq_assume_tac| is similar to \verb|assume_tac|, but checks
1.370 - only for immediate \isa{{\isasymalpha}}-convertibility instead of using
1.371 - unification. It succeeds (with a unique next state) if one of the
1.372 - assumptions is equal to the subgoal's conclusion. Since it does not
1.373 - instantiate variables, it cannot make other subgoals unprovable.
1.374 -
1.375 - \item \verb|match_tac|, \verb|ematch_tac|, and \verb|dmatch_tac| are
1.376 - similar to \verb|resolve_tac|, \verb|eresolve_tac|, and \verb|dresolve_tac|, respectively, but do not instantiate schematic
1.377 - variables in the goal state.
1.378 -
1.379 - Flexible subgoals are not updated at will, but are left alone.
1.380 - Strictly speaking, matching means to treat the unknowns in the goal
1.381 - state as constants; these tactics merely discard unifiers that would
1.382 - update the goal state.
1.383 -
1.384 - \end{description}%
1.385 -\end{isamarkuptext}%
1.386 -\isamarkuptrue%
1.387 -%
1.388 -\endisatagmlref
1.389 -{\isafoldmlref}%
1.390 -%
1.391 -\isadelimmlref
1.392 -%
1.393 -\endisadelimmlref
1.394 -%
1.395 -\isamarkupsubsection{Explicit instantiation within a subgoal context%
1.396 -}
1.397 -\isamarkuptrue%
1.398 -%
1.399 -\begin{isamarkuptext}%
1.400 -The main resolution tactics (\secref{sec:resolve-assume-tac})
1.401 - use higher-order unification, which works well in many practical
1.402 - situations despite its daunting theoretical properties.
1.403 - Nonetheless, there are important problem classes where unguided
1.404 - higher-order unification is not so useful. This typically involves
1.405 - rules like universal elimination, existential introduction, or
1.406 - equational substitution. Here the unification problem involves
1.407 - fully flexible \isa{{\isacharquery}P\ {\isacharquery}x} schemes, which are hard to manage
1.408 - without further hints.
1.409 -
1.410 - By providing a (small) rigid term for \isa{{\isacharquery}x} explicitly, the
1.411 - remaining unification problem is to assign a (large) term to \isa{{\isacharquery}P}, according to the shape of the given subgoal. This is
1.412 - sufficiently well-behaved in most practical situations.
1.413 -
1.414 - \medskip Isabelle provides separate versions of the standard \isa{r{\isacharslash}e{\isacharslash}d{\isacharslash}f} resolution tactics that allow to provide explicit
1.415 - instantiations of unknowns of the given rule, wrt.\ terms that refer
1.416 - to the implicit context of the selected subgoal.
1.417 -
1.418 - An instantiation consists of a list of pairs of the form \isa{{\isacharparenleft}{\isacharquery}x{\isacharcomma}\ t{\isacharparenright}}, where \isa{{\isacharquery}x} is a schematic variable occurring in
1.419 - the given rule, and \isa{t} is a term from the current proof
1.420 - context, augmented by the local goal parameters of the selected
1.421 - subgoal; cf.\ the \isa{focus} operation described in
1.422 - \secref{sec:variables}.
1.423 -
1.424 - Entering the syntactic context of a subgoal is a brittle operation,
1.425 - because its exact form is somewhat accidental, and the choice of
1.426 - bound variable names depends on the presence of other local and
1.427 - global names. Explicit renaming of subgoal parameters prior to
1.428 - explicit instantiation might help to achieve a bit more robustness.
1.429 -
1.430 - Type instantiations may be given as well, via pairs like \isa{{\isacharparenleft}{\isacharquery}{\isacharprime}a{\isacharcomma}\ {\isasymtau}{\isacharparenright}}. Type instantiations are distinguished from term
1.431 - instantiations by the syntactic form of the schematic variable.
1.432 - Types are instantiated before terms are. Since term instantiation
1.433 - already performs type-inference as expected, explicit type
1.434 - instantiations are seldom necessary.%
1.435 -\end{isamarkuptext}%
1.436 -\isamarkuptrue%
1.437 -%
1.438 -\isadelimmlref
1.439 -%
1.440 -\endisadelimmlref
1.441 -%
1.442 -\isatagmlref
1.443 -%
1.444 -\begin{isamarkuptext}%
1.445 -\begin{mldecls}
1.446 - \indexml{res\_inst\_tac}\verb|res_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic| \\
1.447 - \indexml{eres\_inst\_tac}\verb|eres_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic| \\
1.448 - \indexml{dres\_inst\_tac}\verb|dres_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic| \\
1.449 - \indexml{forw\_inst\_tac}\verb|forw_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic| \\[1ex]
1.450 - \indexml{rename\_tac}\verb|rename_tac: string list -> int -> tactic| \\
1.451 - \end{mldecls}
1.452 -
1.453 - \begin{description}
1.454 -
1.455 - \item \verb|res_inst_tac|~\isa{ctxt\ insts\ thm\ i} instantiates the
1.456 - rule \isa{thm} with the instantiations \isa{insts}, as described
1.457 - above, and then performs resolution on subgoal \isa{i}.
1.458 -
1.459 - \item \verb|eres_inst_tac| is like \verb|res_inst_tac|, but performs
1.460 - elim-resolution.
1.461 -
1.462 - \item \verb|dres_inst_tac| is like \verb|res_inst_tac|, but performs
1.463 - destruct-resolution.
1.464 -
1.465 - \item \verb|forw_inst_tac| is like \verb|dres_inst_tac| except that
1.466 - the selected assumption is not deleted.
1.467 -
1.468 - \item \verb|rename_tac|~\isa{names\ i} renames the innermost
1.469 - parameters of subgoal \isa{i} according to the provided \isa{names} (which need to be distinct indentifiers).
1.470 -
1.471 - \end{description}%
1.472 -\end{isamarkuptext}%
1.473 -\isamarkuptrue%
1.474 -%
1.475 -\endisatagmlref
1.476 -{\isafoldmlref}%
1.477 -%
1.478 -\isadelimmlref
1.479 -%
1.480 -\endisadelimmlref
1.481 -%
1.482 -\isamarkupsection{Tacticals \label{sec:tacticals}%
1.483 -}
1.484 -\isamarkuptrue%
1.485 -%
1.486 -\begin{isamarkuptext}%
1.487 -FIXME
1.488 -
1.489 -\glossary{Tactical}{A functional combinator for building up complex
1.490 -tactics from simpler ones. Typical tactical perform sequential
1.491 -composition, disjunction (choice), iteration, or goal addressing.
1.492 -Various search strategies may be expressed via tacticals.}%
1.493 -\end{isamarkuptext}%
1.494 -\isamarkuptrue%
1.495 -%
1.496 -\isadelimtheory
1.497 -%
1.498 -\endisadelimtheory
1.499 -%
1.500 -\isatagtheory
1.501 -\isacommand{end}\isamarkupfalse%
1.502 -%
1.503 -\endisatagtheory
1.504 -{\isafoldtheory}%
1.505 -%
1.506 -\isadelimtheory
1.507 -%
1.508 -\endisadelimtheory
1.509 -\isanewline
1.510 -\isanewline
1.511 -\end{isabellebody}%
1.512 -%%% Local Variables:
1.513 -%%% mode: latex
1.514 -%%% TeX-master: "root"
1.515 -%%% End: