doc-src/Ref/tctical.tex

 
 
 \subsection{Repetition tacticals}
 \index{tacticals!repetition}
 \begin{ttbox} 
-TRY           : tactic -> tactic
-REPEAT_DETERM : tactic -> tactic
-REPEAT        : tactic -> tactic
-REPEAT1       : tactic -> tactic
-trace_REPEAT  : bool ref \hfill{\bf initially false}
+TRY             : tactic -> tactic
+REPEAT_DETERM   : tactic -> tactic
+REPEAT_DETERM_N : int -> tactic -> tactic
+REPEAT          : tactic -> tactic
+REPEAT1         : tactic -> tactic
+DETERM_UNTIL    : (thm -> bool) -> tactic -> tactic
+trace_REPEAT    : bool ref \hfill{\bf initially false}
 \end{ttbox}
 \begin{ttdescription}
 \item[\ttindexbold{TRY} {\it tac}] 
 applies {\it tac\/} to the proof state and returns the resulting sequence,
 if non-empty; otherwise it returns the original state.  Thus, it applies

 
 \item[\ttindexbold{REPEAT_DETERM} {\it tac}] 
 applies {\it tac\/} to the proof state and, recursively, to the head of the
 resulting sequence.  It returns the first state to make {\it tac\/} fail.
 It is deterministic, discarding alternative outcomes.
+
+\item[\ttindexbold{REPEAT_DETERM_N} {\it n} {\it tac}] 
+is like \hbox{\tt REPEAT_DETERM {\it tac}} but the number of repititions
+is bound by {\it n} (unless negative).
 
 \item[\ttindexbold{REPEAT} {\it tac}] 
 applies {\it tac\/} to the proof state and, recursively, to each element of
 the resulting sequence.  The resulting sequence consists of those states
 that make {\it tac\/} fail.  Thus, it applies {\it tac\/} as many times as

 
 \item[\ttindexbold{REPEAT1} {\it tac}] 
 is like \hbox{\tt REPEAT {\it tac}} but it always applies {\it tac\/} at
 least once, failing if this is impossible.
 
+\item[\ttindexbold{DETERM_UNTIL} {\it p} {\it tac}] 
+applies {\it tac\/} to the proof state and, recursively, to the head of the
+resulting sequence, until the predicate {\it p} (applied on the proof state)
+yields {\it true}. It fails if {\it tac\/} fails on any of the intermediate 
+states. It is deterministic, discarding alternative outcomes.
+
 \item[set \ttindexbold{trace_REPEAT};] 
 enables an interactive tracing mode for the tacticals {\tt REPEAT_DETERM}
 and {\tt REPEAT}.  To view the tracing options, type {\tt h} at the prompt.
 \end{ttdescription}
 

 
 \subsection{Auxiliary tacticals for searching}
 \index{tacticals!conditional}
 \index{tacticals!deterministic}
 \begin{ttbox} 
-COND        : (thm->bool) -> tactic -> tactic -> tactic
-IF_UNSOLVED : tactic -> tactic
-SOLVE       : tactic -> tactic
-DETERM      : tactic -> tactic
+COND                : (thm->bool) -> tactic -> tactic -> tactic
+IF_UNSOLVED         : tactic -> tactic
+SOLVE               : tactic -> tactic
+DETERM              : tactic -> tactic
+DETERM_UNTIL_SOLVED : tactic -> tactic
 \end{ttbox}
 \begin{ttdescription}
 \item[\ttindexbold{COND} {\it p} $tac@1$ $tac@2$] 
 applies $tac@1$ to the proof state if it satisfies~$p$, and applies $tac@2$
 otherwise.  It is a conditional tactical in that only one of $tac@1$ and

 
 \item[\ttindexbold{DETERM} {\it tac}] 
 applies {\it tac\/} to the proof state and returns the head of the
 resulting sequence.  {\tt DETERM} limits the search space by making its
 argument deterministic.
+
+\item[\ttindexbold{DETERM_UNTIL_SOLVED} {\it tac}] 
+forces repeated deterministic application of {\it tac\/} to the proof state 
+until the goal is solved completely.
 \end{ttdescription}
 
 
 \subsection{Predicates and functions useful for searching}
 \index{theorems!size of}