1.1 --- a/doc-src/Intro/advanced.tex Wed Apr 06 16:36:34 1994 +0200
1.2 +++ b/doc-src/Intro/advanced.tex Fri Apr 15 11:35:44 1994 +0200
1.3 @@ -28,30 +28,30 @@
1.4 A mathematical development goes through a progression of stages. Each
1.5 stage defines some concepts and derives rules about them. We shall see how
1.6 to derive rules, perhaps involving definitions, using Isabelle. The
1.7 -following section will explain how to declare types, constants, axioms and
1.8 +following section will explain how to declare types, constants, rules and
1.9 definitions.
1.10
1.11
1.12 \subsection{Deriving a rule using tactics and meta-level assumptions}
1.13 \label{deriving-example}
1.14 -\index{examples!of deriving rules}
1.15 +\index{examples!of deriving rules}\index{assumptions!of main goal}
1.16
1.17 The subgoal module supports the derivation of rules, as discussed in
1.18 \S\ref{deriving}. The \ttindex{goal} command, when supplied a goal of the
1.19 form $\List{\theta@1; \ldots; \theta@k} \Imp \phi$, creates $\phi\Imp\phi$
1.20 as the initial proof state and returns a list consisting of the theorems
1.21 ${\theta@i\;[\theta@i]}$, for $i=1$, \ldots,~$k$. These meta-assumptions
1.22 -are also recorded internally, allowing \ttindex{result} to discharge them
1.23 +are also recorded internally, allowing {\tt result} to discharge them
1.24 in the original order.
1.25
1.26 Let us derive $\conj$ elimination using Isabelle.
1.27 -Until now, calling \ttindex{goal} has returned an empty list, which we have
1.28 +Until now, calling {\tt goal} has returned an empty list, which we have
1.29 thrown away. In this example, the list contains the two premises of the
1.30 rule. We bind them to the \ML\ identifiers {\tt major} and {\tt
1.31 minor}:\footnote{Some ML compilers will print a message such as {\em
1.32 binding not exhaustive}. This warns that {\tt goal} must return a
1.33 2-element list. Otherwise, the pattern-match will fail; ML will
1.34 -raise exception \ttindex{Match}.}
1.35 +raise exception \xdx{Match}.}
1.36 \begin{ttbox}
1.37 val [major,minor] = goal FOL.thy
1.38 "[| P&Q; [| P; Q |] ==> R |] ==> R";
1.39 @@ -104,9 +104,8 @@
1.40
1.41
1.42 \subsection{Definitions and derived rules} \label{definitions}
1.43 -\index{rules!derived}
1.44 -\index{Isabelle!definitions in}
1.45 -\index{definitions!reasoning about|bold}
1.46 +\index{rules!derived}\index{definitions!and derived rules|(}
1.47 +
1.48 Definitions are expressed as meta-level equalities. Let us define negation
1.49 and the if-and-only-if connective:
1.50 \begin{eqnarray*}
1.51 @@ -114,8 +113,7 @@
1.52 \Var{P}\bimp \Var{Q} & \equiv &
1.53 (\Var{P}\imp \Var{Q}) \conj (\Var{Q}\imp \Var{P})
1.54 \end{eqnarray*}
1.55 -\index{rewriting!meta-level|bold}
1.56 -\index{unfolding|bold}\index{folding|bold}
1.57 +\index{meta-rewriting}
1.58 Isabelle permits {\bf meta-level rewriting} using definitions such as
1.59 these. {\bf Unfolding} replaces every instance
1.60 of $\neg \Var{P}$ by the corresponding instance of $\Var{P}\imp\bot$. For
1.61 @@ -147,7 +145,7 @@
1.62
1.63
1.64 \subsection{Deriving the $\neg$ introduction rule}
1.65 -To derive $(\neg I)$, we may call \ttindex{goal} with the appropriate
1.66 +To derive $(\neg I)$, we may call {\tt goal} with the appropriate
1.67 formula. Again, {\tt goal} returns a list consisting of the rule's
1.68 premises. We bind this one-element list to the \ML\ identifier {\tt
1.69 prems}.
1.70 @@ -158,7 +156,7 @@
1.71 {\out 1. ~P}
1.72 {\out val prems = ["P ==> False [P ==> False]"] : thm list}
1.73 \end{ttbox}
1.74 -Calling \ttindex{rewrite_goals_tac} with \ttindex{not_def}, which is the
1.75 +Calling \ttindex{rewrite_goals_tac} with \tdx{not_def}, which is the
1.76 definition of negation, unfolds that definition in the subgoals. It leaves
1.77 the main goal alone.
1.78 \begin{ttbox}
1.79 @@ -169,7 +167,7 @@
1.80 {\out ~P}
1.81 {\out 1. P --> False}
1.82 \end{ttbox}
1.83 -Using \ttindex{impI} and the premise, we reduce subgoal~1 to a triviality:
1.84 +Using \tdx{impI} and the premise, we reduce subgoal~1 to a triviality:
1.85 \begin{ttbox}
1.86 by (resolve_tac [impI] 1);
1.87 {\out Level 2}
1.88 @@ -191,10 +189,10 @@
1.89 val notI = result();
1.90 {\out val notI = "(?P ==> False) ==> ~?P" : thm}
1.91 \end{ttbox}
1.92 -\indexbold{*notI}
1.93 +\indexbold{*notI theorem}
1.94
1.95 There is a simpler way of conducting this proof. The \ttindex{goalw}
1.96 -command starts a backward proof, as does \ttindex{goal}, but it also
1.97 +command starts a backward proof, as does {\tt goal}, but it also
1.98 unfolds definitions. Thus there is no need to call
1.99 \ttindex{rewrite_goals_tac}:
1.100 \begin{ttbox}
1.101 @@ -211,8 +209,8 @@
1.102 Let us derive the rule $(\neg E)$. The proof follows that of~{\tt conjE}
1.103 above, with an additional step to unfold negation in the major premise.
1.104 Although the {\tt goalw} command is best for this, let us
1.105 -try~\ttindex{goal} to see another way of unfolding definitions. After
1.106 -binding the premises to \ML\ identifiers, we apply \ttindex{FalseE}:
1.107 +try~{\tt goal} to see another way of unfolding definitions. After
1.108 +binding the premises to \ML\ identifiers, we apply \tdx{FalseE}:
1.109 \begin{ttbox}
1.110 val [major,minor] = goal FOL.thy "[| ~P; P |] ==> R";
1.111 {\out Level 0}
1.112 @@ -257,7 +255,7 @@
1.113 val notE = result();
1.114 {\out val notE = "[| ~?P; ?P |] ==> ?R" : thm}
1.115 \end{ttbox}
1.116 -\indexbold{*notE}
1.117 +\indexbold{*notE theorem}
1.118
1.119 \medskip
1.120 Again, there is a simpler way of conducting this proof. Recall that
1.121 @@ -282,8 +280,9 @@
1.122 {\out R}
1.123 {\out No subgoals!}
1.124 \end{ttbox}
1.125 +\index{definitions!and derived rules|)}
1.126
1.127 -\goodbreak\medskip
1.128 +\goodbreak\medskip\index{*"!"! symbol!in main goal}
1.129 Finally, here is a trick that is sometimes useful. If the goal
1.130 has an outermost meta-quantifier, then \ttindex{goal} and \ttindex{goalw}
1.131 do not return the rule's premises in the list of theorems; instead, the
1.132 @@ -297,8 +296,8 @@
1.133 val it = [] : thm list
1.134 \end{ttbox}
1.135 The proof continues as before. But instead of referring to \ML\
1.136 -identifiers, we refer to assumptions using \ttindex{eresolve_tac} or
1.137 -\ttindex{assume_tac}:
1.138 +identifiers, we refer to assumptions using {\tt eresolve_tac} or
1.139 +{\tt assume_tac}:
1.140 \begin{ttbox}
1.141 by (resolve_tac [FalseE] 1);
1.142 {\out Level 1}
1.143 @@ -329,6 +328,7 @@
1.144
1.145 \section{Defining theories}\label{sec:defining-theories}
1.146 \index{theories!defining|(}
1.147 +
1.148 Isabelle makes no distinction between simple extensions of a logic --- like
1.149 defining a type~$bool$ with constants~$true$ and~$false$ --- and defining
1.150 an entire logic. A theory definition has the form
1.151 @@ -350,7 +350,8 @@
1.152 default sort for type variables. A constant declaration can specify an
1.153 associated concrete syntax. The translations section specifies rewrite
1.154 rules on abstract syntax trees, for defining notations and abbreviations.
1.155 -The {\ML} section contains code to perform arbitrary syntactic
1.156 +\index{*ML section}
1.157 +The {\tt ML} section contains code to perform arbitrary syntactic
1.158 transformations. The main declaration forms are discussed below.
1.159 The full syntax can be found in \iflabelundefined{app:TheorySyntax}{the
1.160 appendix of the {\it Reference Manual}}{App.\ts\ref{app:TheorySyntax}}.
1.161 @@ -358,7 +359,7 @@
1.162 All the declaration parts can be omitted. In the simplest case, $T$ is
1.163 just the union of $S@1$,~\ldots,~$S@n$. New theories always extend one
1.164 or more other theories, inheriting their types, constants, syntax, etc.
1.165 -The theory \ttindexbold{Pure} contains nothing but Isabelle's meta-logic.
1.166 +The theory \thydx{Pure} contains nothing but Isabelle's meta-logic.
1.167
1.168 Each theory definition must reside in a separate file, whose name is
1.169 determined as follows: the theory name, say {\tt ListFn}, is converted to
1.170 @@ -388,7 +389,8 @@
1.171
1.172
1.173 \subsection{Declaring constants and rules}
1.174 -\indexbold{constants!declaring}\indexbold{rules!declaring}
1.175 +\indexbold{constants!declaring}\index{rules!declaring}
1.176 +
1.177 Most theories simply declare constants and rules. The {\bf constant
1.178 declaration part} has the form
1.179 \begin{ttbox}
1.180 @@ -414,6 +416,7 @@
1.181 $rule@n$ are expressions of type~$prop$. Each rule {\em must\/} be
1.182 enclosed in quotation marks.
1.183
1.184 +\indexbold{definitions}
1.185 {\bf Definitions} are rules of the form $t\equiv u$. Normally definitions
1.186 should be conservative, serving only as abbreviations. As of this writing,
1.187 Isabelle does not provide a separate declaration part for definitions; it
1.188 @@ -544,9 +547,11 @@
1.189 negate :: "signal => signal"
1.190 \end{ttbox}
1.191
1.192 -\subsection{Infixes and Mixfixes}
1.193 -\indexbold{infix operators}\index{examples!of theories}
1.194 -The constant declaration part of the theory
1.195 +\subsection{Infix and Mixfix operators}
1.196 +\index{infixes}\index{examples!of theories}
1.197 +
1.198 +Infix or mixfix syntax may be attached to constants. Consider the
1.199 +following theory:
1.200 \begin{ttbox}
1.201 Gate2 = FOL +
1.202 consts "~&" :: "[o,o] => o" (infixl 35)
1.203 @@ -555,55 +560,63 @@
1.204 xor_def "P # Q == P & ~Q | ~P & Q"
1.205 end
1.206 \end{ttbox}
1.207 -declares two left-associating infix operators: $\nand$ of precedence~35 and
1.208 -$\xor$ of precedence~30. Hence $P \xor Q \xor R$ is parsed as $(P\xor
1.209 -Q) \xor R$ and $P \xor Q \nand R$ as $P \xor (Q \nand R)$. Note the
1.210 -quotation marks in \verb|"~&"| and \verb|"#"|.
1.211 +The constant declaration part declares two left-associating infix operators
1.212 +with their priorities, or precedences; they are $\nand$ of priority~35 and
1.213 +$\xor$ of priority~30. Hence $P \xor Q \xor R$ is parsed as $(P\xor Q)
1.214 +\xor R$ and $P \xor Q \nand R$ as $P \xor (Q \nand R)$. Note the quotation
1.215 +marks in \verb|"~&"| and \verb|"#"|.
1.216
1.217 The constants \hbox{\verb|op ~&|} and \hbox{\verb|op #|} are declared
1.218 automatically, just as in \ML. Hence you may write propositions like
1.219 \verb|op #(True) == op ~&(True)|, which asserts that the functions $\lambda
1.220 Q.True \xor Q$ and $\lambda Q.True \nand Q$ are identical.
1.221
1.222 -\indexbold{mixfix operators}
1.223 -{\bf Mixfix} operators may have arbitrary context-free syntaxes. For example
1.224 +\bigskip\index{mixfix declarations}
1.225 +{\bf Mixfix} operators may have arbitrary context-free syntaxes. Let us
1.226 +add a line to the constant declaration part:
1.227 \begin{ttbox}
1.228 If :: "[o,o,o] => o" ("if _ then _ else _")
1.229 \end{ttbox}
1.230 -declares a constant $If$ of type $[o,o,o] \To o$ with concrete syntax {\tt
1.231 +This declares a constant $If$ of type $[o,o,o] \To o$ with concrete syntax {\tt
1.232 if~$P$ then~$Q$ else~$R$} as well as {\tt If($P$,$Q$,$R$)}. Underscores
1.233 -denote argument positions. Pretty-printing information can be specified in
1.234 -order to improve the layout of formulae with mixfix operations. For
1.235 -details, see {\em Isabelle's Object-Logics}.
1.236 +denote argument positions.
1.237
1.238 -Mixfix declarations can be annotated with precedences, just like
1.239 +The declaration above does not allow the {\tt if}-{\tt then}-{\tt else}
1.240 +construct to be split across several lines, even if it is too long to fit
1.241 +on one line. Pretty-printing information can be added to specify the
1.242 +layout of mixfix operators. For details, see
1.243 +\iflabelundefined{Defining-Logics}%
1.244 + {the {\it Reference Manual}, chapter `Defining Logics'}%
1.245 + {Chap.\ts\ref{Defining-Logics}}.
1.246 +
1.247 +Mixfix declarations can be annotated with priorities, just like
1.248 infixes. The example above is just a shorthand for
1.249 \begin{ttbox}
1.250 If :: "[o,o,o] => o" ("if _ then _ else _" [0,0,0] 1000)
1.251 \end{ttbox}
1.252 -The numeric components determine precedences. The list of integers
1.253 -defines, for each argument position, the minimal precedence an expression
1.254 -at that position must have. The final integer is the precedence of the
1.255 +The numeric components determine priorities. The list of integers
1.256 +defines, for each argument position, the minimal priority an expression
1.257 +at that position must have. The final integer is the priority of the
1.258 construct itself. In the example above, any argument expression is
1.259 -acceptable because precedences are non-negative, and conditionals may
1.260 -appear everywhere because 1000 is the highest precedence. On the other
1.261 -hand,
1.262 +acceptable because priorities are non-negative, and conditionals may
1.263 +appear everywhere because 1000 is the highest priority. On the other
1.264 +hand, the declaration
1.265 \begin{ttbox}
1.266 If :: "[o,o,o] => o" ("if _ then _ else _" [100,0,0] 99)
1.267 \end{ttbox}
1.268 defines concrete syntax for a conditional whose first argument cannot have
1.269 -the form {\tt if~$P$ then~$Q$ else~$R$} because it must have a precedence
1.270 -of at least~100. Since expressions put in parentheses have maximal
1.271 -precedence, we may of course write
1.272 +the form {\tt if~$P$ then~$Q$ else~$R$} because it must have a priority
1.273 +of at least~100. We may of course write
1.274 \begin{quote}\tt
1.275 if (if $P$ then $Q$ else $R$) then $S$ else $T$
1.276 \end{quote}
1.277 +because expressions in parentheses have maximal priority.
1.278
1.279 Binary type constructors, like products and sums, may also be declared as
1.280 infixes. The type declaration below introduces a type constructor~$*$ with
1.281 infix notation $\alpha*\beta$, together with the mixfix notation
1.282 ${<}\_,\_{>}$ for pairs.
1.283 -\index{examples!of theories}
1.284 +\index{examples!of theories}\index{mixfix declarations}
1.285 \begin{ttbox}
1.286 Prod = FOL +
1.287 types ('a,'b) "*" (infixl 20)
1.288 @@ -643,7 +656,7 @@
1.289 types with the constants ${+} :: [\alpha,\alpha]\To \alpha$ and $0,1 {::}
1.290 \alpha$, for $\alpha{::}arith$. We introduce $arith$ as a subclass of
1.291 $term$ and add the three polymorphic constants of this class.
1.292 -\index{examples!of theories}
1.293 +\index{examples!of theories}\index{constants!overloaded}
1.294 \begin{ttbox}
1.295 Arith = FOL +
1.296 classes arith < term
1.297 @@ -696,7 +709,7 @@
1.298 Section\ts\ref{sec:logical-syntax} has formalized a first-order logic,
1.299 including a type~$nat$ and the constants $0::nat$ and $Suc::nat\To nat$.
1.300 Let us introduce the Peano axioms for mathematical induction and the
1.301 -freeness of $0$ and~$Suc$:
1.302 +freeness of $0$ and~$Suc$:\index{axioms!Peano}
1.303 \[ \vcenter{\infer[(induct)]{P[n/x]}{P[0/x] & \infer*{P[Suc(x)/x]}{[P]}}}
1.304 \qquad \parbox{4.5cm}{provided $x$ is not free in any assumption except~$P$}
1.305 \]
1.306 @@ -748,12 +761,12 @@
1.307
1.308 \subsection{Declaring the theory to Isabelle}
1.309 \index{examples!of theories}
1.310 -Let us create the theory \ttindexbold{Nat} starting from theory~\verb$FOL$,
1.311 +Let us create the theory \thydx{Nat} starting from theory~\verb$FOL$,
1.312 which contains only classical logic with no natural numbers. We declare
1.313 the 0-place type constructor $nat$ and the associated constants. Note that
1.314 the constant~0 requires a mixfix annotation because~0 is not a legal
1.315 identifier, and could not otherwise be written in terms:
1.316 -\begin{ttbox}
1.317 +\begin{ttbox}\index{mixfix declarations}
1.318 Nat = FOL +
1.319 types nat
1.320 arities nat :: term
1.321 @@ -811,8 +824,9 @@
1.322
1.323
1.324 \section{Refinement with explicit instantiation}
1.325 -\index{refinement!with instantiation|bold}
1.326 -\index{instantiation!explicit|bold}
1.327 +\index{resolution!with instantiation}
1.328 +\index{instantiation|(}
1.329 +
1.330 In order to employ mathematical induction, we need to refine a subgoal by
1.331 the rule~$(induct)$. The conclusion of this rule is $\Var{P}(\Var{n})$,
1.332 which is highly ambiguous in higher-order unification. It matches every
1.333 @@ -825,12 +839,12 @@
1.334 a rule. But it also accepts explicit instantiations for the rule's
1.335 schematic variables.
1.336 \begin{description}
1.337 -\item[\ttindexbold{res_inst_tac} {\it insts} {\it thm} {\it i}]
1.338 +\item[\ttindex{res_inst_tac} {\it insts} {\it thm} {\it i}]
1.339 instantiates the rule {\it thm} with the instantiations {\it insts}, and
1.340 then performs resolution on subgoal~$i$.
1.341
1.342 -\item[\ttindexbold{eres_inst_tac}]
1.343 -and \ttindexbold{dres_inst_tac} are similar, but perform elim-resolution
1.344 +\item[\ttindex{eres_inst_tac}]
1.345 +and \ttindex{dres_inst_tac} are similar, but perform elim-resolution
1.346 and destruct-resolution, respectively.
1.347 \end{description}
1.348 The list {\it insts} consists of pairs $[(v@1,e@1), \ldots, (v@n,e@n)]$,
1.349 @@ -844,7 +858,7 @@
1.350 whenever the type of~$e@i$ is an instance of the type of~$\Var{v@i}$.
1.351
1.352 \subsection{A simple proof by induction}
1.353 -\index{proof!by induction}\index{examples!of induction}
1.354 +\index{examples!of induction}
1.355 Let us prove that no natural number~$k$ equals its own successor. To
1.356 use~$(induct)$, we instantiate~$\Var{n}$ to~$k$; Isabelle finds a good
1.357 instantiation for~$\Var{P}$.
1.358 @@ -863,8 +877,8 @@
1.359 We should check that Isabelle has correctly applied induction. Subgoal~1
1.360 is the base case, with $k$ replaced by~0. Subgoal~2 is the inductive step,
1.361 with $k$ replaced by~$Suc(x)$ and with an induction hypothesis for~$x$.
1.362 -The rest of the proof demonstrates~\ttindex{notI}, \ttindex{notE} and the
1.363 -other rules of~\ttindex{Nat.thy}. The base case holds by~\ttindex{Suc_neq_0}:
1.364 +The rest of the proof demonstrates~\tdx{notI}, \tdx{notE} and the
1.365 +other rules of theory {\tt Nat}. The base case holds by~\ttindex{Suc_neq_0}:
1.366 \begin{ttbox}
1.367 by (resolve_tac [notI] 1);
1.368 {\out Level 2}
1.369 @@ -949,23 +963,26 @@
1.370 \end{ttbox}
1.371 Inspecting subgoal~1 reveals that induction has been applied to just the
1.372 second occurrence of~$n$. This perfectly legitimate induction is useless
1.373 -here. The main goal admits fourteen different applications of induction.
1.374 -The number is exponential in the size of the formula.
1.375 +here.
1.376 +
1.377 +The main goal admits fourteen different applications of induction. The
1.378 +number is exponential in the size of the formula.
1.379
1.380 \subsection{Proving that addition is associative}
1.381 -Let us invoke the induction rule properly properly,
1.382 -using~\ttindex{res_inst_tac}. At the same time, we shall have a glimpse at
1.383 -Isabelle's rewriting tactics, which are described in the {\em Reference
1.384 - Manual}.
1.385 +Let us invoke the induction rule properly properly, using~{\tt
1.386 + res_inst_tac}. At the same time, we shall have a glimpse at Isabelle's
1.387 +simplification tactics, which are described in
1.388 +\iflabelundefined{simp-chap}%
1.389 + {the {\em Reference Manual}}{Chap.\ts\ref{simp-chap}}.
1.390
1.391 -\index{rewriting!object-level}\index{examples!of rewriting}
1.392 +\index{simplification}\index{examples!of simplification}
1.393
1.394 -Isabelle's rewriting tactics repeatedly applies equations to a subgoal,
1.395 -simplifying or proving it. For efficiency, the rewriting rules must be
1.396 -packaged into a \bfindex{simplification set}, or {\bf simpset}. We take
1.397 -the standard simpset for first-order logic and insert the equations
1.398 -for~{\tt add} proved in the previous section, namely $0+n=n$ and ${\tt
1.399 - Suc}(m)+n={\tt Suc}(m+n)$:
1.400 +Isabelle's simplification tactics repeatedly apply equations to a subgoal,
1.401 +perhaps proving it. For efficiency, the rewrite rules must be
1.402 +packaged into a {\bf simplification set},\index{simplification sets}
1.403 +or {\bf simpset}. We take the standard simpset for first-order logic and
1.404 +insert the equations for~{\tt add} proved in the previous section, namely
1.405 +$0+n=n$ and ${\tt Suc}(m)+n={\tt Suc}(m+n)$:
1.406 \begin{ttbox}
1.407 val add_ss = FOL_ss addrews [add_0, add_Suc];
1.408 \end{ttbox}
1.409 @@ -1004,6 +1021,7 @@
1.410 {\out k + m + n = k + (m + n)}
1.411 {\out No subgoals!}
1.412 \end{ttbox}
1.413 +\index{instantiation|)}
1.414
1.415
1.416 \section{A Prolog interpreter}
1.417 @@ -1037,9 +1055,9 @@
1.418 \]
1.419
1.420 \index{examples!of theories}
1.421 -Theory \ttindex{Prolog} extends first-order logic in order to make use
1.422 +Theory \thydx{Prolog} extends first-order logic in order to make use
1.423 of the class~$term$ and the type~$o$. The interpreter does not use the
1.424 -rules of~\ttindex{FOL}.
1.425 +rules of~{\tt FOL}.
1.426 \begin{ttbox}
1.427 Prolog = FOL +
1.428 types 'a list
1.429 @@ -1103,7 +1121,7 @@
1.430 \end{ttbox}
1.431
1.432
1.433 -\subsection{Backtracking}\index{backtracking}
1.434 +\subsection{Backtracking}\index{backtracking!Prolog style}
1.435 Prolog backtracking can answer questions that have multiple solutions.
1.436 Which lists $x$ and $y$ can be appended to form the list $[a,b,c,d]$? This
1.437 question has five solutions. Using \ttindex{REPEAT} to apply the rules, we
1.438 @@ -1196,11 +1214,12 @@
1.439 {\out rev(c : b : a : Nil, a : b : c : Nil)}
1.440 {\out No subgoals!}
1.441 \end{ttbox}
1.442 -\ttindex{REPEAT} stops when it cannot continue, regardless of which state
1.443 -is reached. The tactical \ttindex{DEPTH_FIRST} searches for a satisfactory
1.444 -state, as specified by an \ML{} predicate. Below,
1.445 +\ttindex{REPEAT} goes wrong because it is only a repetition tactical, not a
1.446 +search tactical. {\tt REPEAT} stops when it cannot continue, regardless of
1.447 +which state is reached. The tactical \ttindex{DEPTH_FIRST} searches for a
1.448 +satisfactory state, as specified by an \ML{} predicate. Below,
1.449 \ttindex{has_fewer_prems} specifies that the proof state should have no
1.450 -subgoals.
1.451 +subgoals.
1.452 \begin{ttbox}
1.453 val prolog_tac = DEPTH_FIRST (has_fewer_prems 1)
1.454 (resolve_tac rules 1);