wenzelm@30184: lcp@104: \chapter{Tacticals} lcp@104: \index{tacticals|(} lcp@104: Tacticals are operations on tactics. Their implementation makes use of lcp@104: functional programming techniques, especially for sequences. Most of the lcp@104: time, you may forget about this and regard tacticals as high-level control lcp@104: structures. lcp@104: lcp@104: \section{The basic tacticals} lcp@104: \subsection{Joining two tactics} lcp@323: \index{tacticals!joining two tactics} lcp@104: The tacticals {\tt THEN} and {\tt ORELSE}, which provide sequencing and lcp@104: alternation, underlie most of the other control structures in Isabelle. lcp@104: {\tt APPEND} and {\tt INTLEAVE} provide more sophisticated forms of lcp@104: alternation. lcp@104: \begin{ttbox} lcp@104: THEN : tactic * tactic -> tactic \hfill{\bf infix 1} lcp@104: ORELSE : tactic * tactic -> tactic \hfill{\bf infix} lcp@104: APPEND : tactic * tactic -> tactic \hfill{\bf infix} lcp@104: INTLEAVE : tactic * tactic -> tactic \hfill{\bf infix} lcp@104: \end{ttbox} lcp@323: \begin{ttdescription} lcp@323: \item[$tac@1$ \ttindexbold{THEN} $tac@2$] lcp@104: is the sequential composition of the two tactics. Applied to a proof lcp@104: state, it returns all states reachable in two steps by applying $tac@1$ lcp@104: followed by~$tac@2$. First, it applies $tac@1$ to the proof state, getting a lcp@104: sequence of next states; then, it applies $tac@2$ to each of these and lcp@104: concatenates the results. lcp@104: lcp@323: \item[$tac@1$ \ttindexbold{ORELSE} $tac@2$] lcp@104: makes a choice between the two tactics. Applied to a state, it lcp@104: tries~$tac@1$ and returns the result if non-empty; if $tac@1$ fails then it lcp@104: uses~$tac@2$. This is a deterministic choice: if $tac@1$ succeeds then lcp@104: $tac@2$ is excluded. lcp@104: lcp@323: \item[$tac@1$ \ttindexbold{APPEND} $tac@2$] lcp@104: concatenates the results of $tac@1$ and~$tac@2$. By not making a commitment lcp@323: to either tactic, {\tt APPEND} helps avoid incompleteness during lcp@323: search.\index{search} lcp@104: lcp@323: \item[$tac@1$ \ttindexbold{INTLEAVE} $tac@2$] lcp@104: interleaves the results of $tac@1$ and~$tac@2$. Thus, it includes all lcp@104: possible next states, even if one of the tactics returns an infinite lcp@104: sequence. lcp@323: \end{ttdescription} lcp@104: lcp@104: lcp@104: \subsection{Joining a list of tactics} lcp@323: \index{tacticals!joining a list of tactics} lcp@104: \begin{ttbox} lcp@104: EVERY : tactic list -> tactic lcp@104: FIRST : tactic list -> tactic lcp@104: \end{ttbox} lcp@104: {\tt EVERY} and {\tt FIRST} are block structured versions of {\tt THEN} and lcp@104: {\tt ORELSE}\@. lcp@323: \begin{ttdescription} lcp@104: \item[\ttindexbold{EVERY} {$[tac@1,\ldots,tac@n]$}] lcp@104: abbreviates \hbox{\tt$tac@1$ THEN \ldots{} THEN $tac@n$}. It is useful for lcp@104: writing a series of tactics to be executed in sequence. lcp@104: lcp@104: \item[\ttindexbold{FIRST} {$[tac@1,\ldots,tac@n]$}] lcp@104: abbreviates \hbox{\tt$tac@1$ ORELSE \ldots{} ORELSE $tac@n$}. It is useful for lcp@104: writing a series of tactics to be attempted one after another. lcp@323: \end{ttdescription} lcp@104: lcp@104: lcp@104: \subsection{Repetition tacticals} lcp@323: \index{tacticals!repetition} lcp@104: \begin{ttbox} oheimb@8149: TRY : tactic -> tactic oheimb@8149: REPEAT_DETERM : tactic -> tactic oheimb@8149: REPEAT_DETERM_N : int -> tactic -> tactic oheimb@8149: REPEAT : tactic -> tactic oheimb@8149: REPEAT1 : tactic -> tactic oheimb@8149: DETERM_UNTIL : (thm -> bool) -> tactic -> tactic oheimb@8149: trace_REPEAT : bool ref \hfill{\bf initially false} lcp@104: \end{ttbox} lcp@323: \begin{ttdescription} lcp@104: \item[\ttindexbold{TRY} {\it tac}] lcp@104: applies {\it tac\/} to the proof state and returns the resulting sequence, lcp@104: if non-empty; otherwise it returns the original state. Thus, it applies lcp@104: {\it tac\/} at most once. lcp@104: lcp@104: \item[\ttindexbold{REPEAT_DETERM} {\it tac}] lcp@104: applies {\it tac\/} to the proof state and, recursively, to the head of the lcp@104: resulting sequence. It returns the first state to make {\it tac\/} fail. lcp@104: It is deterministic, discarding alternative outcomes. lcp@104: oheimb@8149: \item[\ttindexbold{REPEAT_DETERM_N} {\it n} {\it tac}] oheimb@8149: is like \hbox{\tt REPEAT_DETERM {\it tac}} but the number of repititions oheimb@8149: is bound by {\it n} (unless negative). oheimb@8149: lcp@104: \item[\ttindexbold{REPEAT} {\it tac}] lcp@104: applies {\it tac\/} to the proof state and, recursively, to each element of lcp@104: the resulting sequence. The resulting sequence consists of those states lcp@104: that make {\it tac\/} fail. Thus, it applies {\it tac\/} as many times as lcp@104: possible (including zero times), and allows backtracking over each lcp@104: invocation of {\it tac}. It is more general than {\tt REPEAT_DETERM}, but lcp@104: requires more space. lcp@104: lcp@104: \item[\ttindexbold{REPEAT1} {\it tac}] lcp@104: is like \hbox{\tt REPEAT {\it tac}} but it always applies {\it tac\/} at lcp@104: least once, failing if this is impossible. lcp@104: oheimb@8149: \item[\ttindexbold{DETERM_UNTIL} {\it p} {\it tac}] oheimb@8149: applies {\it tac\/} to the proof state and, recursively, to the head of the oheimb@8149: resulting sequence, until the predicate {\it p} (applied on the proof state) oheimb@8149: yields {\it true}. It fails if {\it tac\/} fails on any of the intermediate oheimb@8149: states. It is deterministic, discarding alternative outcomes. oheimb@8149: wenzelm@4317: \item[set \ttindexbold{trace_REPEAT};] lcp@286: enables an interactive tracing mode for the tacticals {\tt REPEAT_DETERM} lcp@286: and {\tt REPEAT}. To view the tracing options, type {\tt h} at the prompt. lcp@323: \end{ttdescription} lcp@104: lcp@104: lcp@104: \subsection{Identities for tacticals} lcp@323: \index{tacticals!identities for} lcp@104: \begin{ttbox} lcp@104: all_tac : tactic lcp@104: no_tac : tactic lcp@104: \end{ttbox} lcp@323: \begin{ttdescription} lcp@104: \item[\ttindexbold{all_tac}] lcp@104: maps any proof state to the one-element sequence containing that state. lcp@104: Thus, it succeeds for all states. It is the identity element of the lcp@104: tactical \ttindex{THEN}\@. lcp@104: lcp@104: \item[\ttindexbold{no_tac}] lcp@104: maps any proof state to the empty sequence. Thus it succeeds for no state. lcp@104: It is the identity element of \ttindex{ORELSE}, \ttindex{APPEND}, and lcp@104: \ttindex{INTLEAVE}\@. Also, it is a zero element for \ttindex{THEN}, which means that lcp@104: \hbox{\tt$tac$ THEN no_tac} is equivalent to {\tt no_tac}. lcp@323: \end{ttdescription} lcp@104: These primitive tactics are useful when writing tacticals. For example, lcp@104: \ttindexbold{TRY} and \ttindexbold{REPEAT} (ignoring tracing) can be coded lcp@104: as follows: lcp@104: \begin{ttbox} lcp@104: fun TRY tac = tac ORELSE all_tac; lcp@104: wenzelm@3108: fun REPEAT tac = wenzelm@3108: (fn state => ((tac THEN REPEAT tac) ORELSE all_tac) state); lcp@104: \end{ttbox} lcp@104: If $tac$ can return multiple outcomes then so can \hbox{\tt REPEAT $tac$}. lcp@104: Since {\tt REPEAT} uses \ttindex{ORELSE} and not {\tt APPEND} or {\tt lcp@104: INTLEAVE}, it applies $tac$ as many times as possible in each lcp@104: outcome. lcp@104: lcp@104: \begin{warn} lcp@104: Note {\tt REPEAT}'s explicit abstraction over the proof state. Recursive lcp@104: tacticals must be coded in this awkward fashion to avoid infinite lcp@104: recursion. With the following definition, \hbox{\tt REPEAT $tac$} would lcp@332: loop due to \ML's eager evaluation strategy: lcp@104: \begin{ttbox} lcp@104: fun REPEAT tac = (tac THEN REPEAT tac) ORELSE all_tac; lcp@104: \end{ttbox} lcp@104: \par\noindent lcp@104: The built-in {\tt REPEAT} avoids~{\tt THEN}, handling sequences explicitly lcp@104: and using tail recursion. This sacrifices clarity, but saves much space by lcp@104: discarding intermediate proof states. lcp@104: \end{warn} lcp@104: lcp@104: lcp@104: \section{Control and search tacticals} lcp@323: \index{search!tacticals|(} lcp@323: lcp@104: A predicate on theorems, namely a function of type \hbox{\tt thm->bool}, lcp@104: can test whether a proof state enjoys some desirable property --- such as lcp@104: having no subgoals. Tactics that search for satisfactory states are easy lcp@104: to express. The main search procedures, depth-first, breadth-first and lcp@104: best-first, are provided as tacticals. They generate the search tree by lcp@104: repeatedly applying a given tactic. lcp@104: lcp@104: lcp@104: \subsection{Filtering a tactic's results} lcp@323: \index{tacticals!for filtering} lcp@323: \index{tactics!filtering results of} lcp@104: \begin{ttbox} lcp@104: FILTER : (thm -> bool) -> tactic -> tactic lcp@104: CHANGED : tactic -> tactic lcp@104: \end{ttbox} lcp@323: \begin{ttdescription} lcp@1118: \item[\ttindexbold{FILTER} {\it p} $tac$] lcp@104: applies $tac$ to the proof state and returns a sequence consisting of those lcp@104: result states that satisfy~$p$. lcp@104: lcp@104: \item[\ttindexbold{CHANGED} {\it tac}] lcp@104: applies {\it tac\/} to the proof state and returns precisely those states lcp@104: that differ from the original state. Thus, \hbox{\tt CHANGED {\it tac}} lcp@104: always has some effect on the state. lcp@323: \end{ttdescription} lcp@104: lcp@104: lcp@104: \subsection{Depth-first search} lcp@323: \index{tacticals!searching} lcp@104: \index{tracing!of searching tacticals} lcp@104: \begin{ttbox} lcp@104: DEPTH_FIRST : (thm->bool) -> tactic -> tactic lcp@332: DEPTH_SOLVE : tactic -> tactic lcp@332: DEPTH_SOLVE_1 : tactic -> tactic lcp@104: trace_DEPTH_FIRST: bool ref \hfill{\bf initially false} lcp@104: \end{ttbox} lcp@323: \begin{ttdescription} lcp@104: \item[\ttindexbold{DEPTH_FIRST} {\it satp} {\it tac}] lcp@104: returns the proof state if {\it satp} returns true. Otherwise it applies lcp@104: {\it tac}, then recursively searches from each element of the resulting lcp@104: sequence. The code uses a stack for efficiency, in effect applying lcp@104: \hbox{\tt {\it tac} THEN DEPTH_FIRST {\it satp} {\it tac}} to the state. lcp@104: lcp@104: \item[\ttindexbold{DEPTH_SOLVE} {\it tac}] lcp@104: uses {\tt DEPTH_FIRST} to search for states having no subgoals. lcp@104: lcp@104: \item[\ttindexbold{DEPTH_SOLVE_1} {\it tac}] lcp@104: uses {\tt DEPTH_FIRST} to search for states having fewer subgoals than the lcp@104: given state. Thus, it insists upon solving at least one subgoal. lcp@104: wenzelm@4317: \item[set \ttindexbold{trace_DEPTH_FIRST};] lcp@104: enables interactive tracing for {\tt DEPTH_FIRST}. To view the lcp@104: tracing options, type {\tt h} at the prompt. lcp@323: \end{ttdescription} lcp@104: lcp@104: lcp@104: \subsection{Other search strategies} lcp@323: \index{tacticals!searching} lcp@104: \index{tracing!of searching tacticals} lcp@104: \begin{ttbox} lcp@332: BREADTH_FIRST : (thm->bool) -> tactic -> tactic lcp@104: BEST_FIRST : (thm->bool)*(thm->int) -> tactic -> tactic lcp@104: THEN_BEST_FIRST : tactic * ((thm->bool) * (thm->int) * tactic) lcp@104: -> tactic \hfill{\bf infix 1} lcp@104: trace_BEST_FIRST: bool ref \hfill{\bf initially false} lcp@104: \end{ttbox} lcp@104: These search strategies will find a solution if one exists. However, they lcp@104: do not enumerate all solutions; they terminate after the first satisfactory lcp@104: result from {\it tac}. lcp@323: \begin{ttdescription} lcp@104: \item[\ttindexbold{BREADTH_FIRST} {\it satp} {\it tac}] lcp@104: uses breadth-first search to find states for which {\it satp\/} is true. lcp@104: For most applications, it is too slow. lcp@104: lcp@104: \item[\ttindexbold{BEST_FIRST} $(satp,distf)$ {\it tac}] lcp@104: does a heuristic search, using {\it distf\/} to estimate the distance from lcp@104: a satisfactory state. It maintains a list of states ordered by distance. lcp@104: It applies $tac$ to the head of this list; if the result contains any lcp@104: satisfactory states, then it returns them. Otherwise, {\tt BEST_FIRST} lcp@104: adds the new states to the list, and continues. lcp@104: lcp@104: The distance function is typically \ttindex{size_of_thm}, which computes lcp@104: the size of the state. The smaller the state, the fewer and simpler lcp@104: subgoals it has. lcp@104: lcp@104: \item[$tac@0$ \ttindexbold{THEN_BEST_FIRST} $(satp,distf,tac)$] lcp@104: is like {\tt BEST_FIRST}, except that the priority queue initially lcp@104: contains the result of applying $tac@0$ to the proof state. This tactical lcp@104: permits separate tactics for starting the search and continuing the search. lcp@104: wenzelm@4317: \item[set \ttindexbold{trace_BEST_FIRST};] lcp@286: enables an interactive tracing mode for the tactical {\tt BEST_FIRST}. To lcp@286: view the tracing options, type {\tt h} at the prompt. lcp@323: \end{ttdescription} lcp@104: lcp@104: lcp@104: \subsection{Auxiliary tacticals for searching} lcp@104: \index{tacticals!conditional} lcp@104: \index{tacticals!deterministic} lcp@104: \begin{ttbox} oheimb@8149: COND : (thm->bool) -> tactic -> tactic -> tactic oheimb@8149: IF_UNSOLVED : tactic -> tactic oheimb@8149: SOLVE : tactic -> tactic oheimb@8149: DETERM : tactic -> tactic oheimb@8149: DETERM_UNTIL_SOLVED : tactic -> tactic lcp@104: \end{ttbox} lcp@323: \begin{ttdescription} lcp@1118: \item[\ttindexbold{COND} {\it p} $tac@1$ $tac@2$] lcp@104: applies $tac@1$ to the proof state if it satisfies~$p$, and applies $tac@2$ lcp@104: otherwise. It is a conditional tactical in that only one of $tac@1$ and lcp@104: $tac@2$ is applied to a proof state. However, both $tac@1$ and $tac@2$ are lcp@104: evaluated because \ML{} uses eager evaluation. lcp@104: lcp@104: \item[\ttindexbold{IF_UNSOLVED} {\it tac}] lcp@104: applies {\it tac\/} to the proof state if it has any subgoals, and simply lcp@104: returns the proof state otherwise. Many common tactics, such as {\tt lcp@104: resolve_tac}, fail if applied to a proof state that has no subgoals. lcp@104: oheimb@5754: \item[\ttindexbold{SOLVE} {\it tac}] oheimb@5754: applies {\it tac\/} to the proof state and then fails iff there are subgoals oheimb@5754: left. oheimb@5754: lcp@104: \item[\ttindexbold{DETERM} {\it tac}] lcp@104: applies {\it tac\/} to the proof state and returns the head of the lcp@104: resulting sequence. {\tt DETERM} limits the search space by making its lcp@104: argument deterministic. oheimb@8149: oheimb@8149: \item[\ttindexbold{DETERM_UNTIL_SOLVED} {\it tac}] oheimb@8149: forces repeated deterministic application of {\it tac\/} to the proof state oheimb@8149: until the goal is solved completely. lcp@323: \end{ttdescription} lcp@104: lcp@104: lcp@104: \subsection{Predicates and functions useful for searching} lcp@104: \index{theorems!size of} lcp@104: \index{theorems!equality of} lcp@104: \begin{ttbox} lcp@104: has_fewer_prems : int -> thm -> bool lcp@104: eq_thm : thm * thm -> bool wenzelm@13104: eq_thm_prop : thm * thm -> bool lcp@104: size_of_thm : thm -> int lcp@104: \end{ttbox} lcp@323: \begin{ttdescription} lcp@104: \item[\ttindexbold{has_fewer_prems} $n$ $thm$] lcp@104: reports whether $thm$ has fewer than~$n$ premises. By currying, lcp@104: \hbox{\tt has_fewer_prems $n$} is a predicate on theorems; it may lcp@104: be given to the searching tacticals. lcp@104: wenzelm@6569: \item[\ttindexbold{eq_thm} ($thm@1$, $thm@2$)] reports whether $thm@1$ and wenzelm@13104: $thm@2$ are equal. Both theorems must have compatible signatures. Both wenzelm@13104: theorems must have the same conclusions, the same hypotheses (in the same wenzelm@13104: order), and the same set of sort hypotheses. Names of bound variables are wenzelm@13104: ignored. wenzelm@13104: wenzelm@13104: \item[\ttindexbold{eq_thm_prop} ($thm@1$, $thm@2$)] reports whether the wenzelm@13104: propositions of $thm@1$ and $thm@2$ are equal. Names of bound variables are wenzelm@13104: ignored. lcp@104: lcp@104: \item[\ttindexbold{size_of_thm} $thm$] lcp@104: computes the size of $thm$, namely the number of variables, constants and lcp@104: abstractions in its conclusion. It may serve as a distance function for lcp@104: \ttindex{BEST_FIRST}. lcp@323: \end{ttdescription} lcp@323: lcp@323: \index{search!tacticals|)} lcp@104: lcp@104: lcp@104: \section{Tacticals for subgoal numbering} lcp@104: When conducting a backward proof, we normally consider one goal at a time. lcp@104: A tactic can affect the entire proof state, but many tactics --- such as lcp@104: {\tt resolve_tac} and {\tt assume_tac} --- work on a single subgoal. lcp@104: Subgoals are designated by a positive integer, so Isabelle provides lcp@104: tacticals for combining values of type {\tt int->tactic}. lcp@104: lcp@104: lcp@104: \subsection{Restricting a tactic to one subgoal} lcp@104: \index{tactics!restricting to a subgoal} lcp@104: \index{tacticals!for restriction to a subgoal} lcp@104: \begin{ttbox} lcp@104: SELECT_GOAL : tactic -> int -> tactic lcp@104: METAHYPS : (thm list -> tactic) -> int -> tactic lcp@104: \end{ttbox} lcp@323: \begin{ttdescription} lcp@104: \item[\ttindexbold{SELECT_GOAL} {\it tac} $i$] lcp@104: restricts the effect of {\it tac\/} to subgoal~$i$ of the proof state. It lcp@104: fails if there is no subgoal~$i$, or if {\it tac\/} changes the main goal lcp@104: (do not use {\tt rewrite_tac}). It applies {\it tac\/} to a dummy proof lcp@104: state and uses the result to refine the original proof state at lcp@104: subgoal~$i$. If {\it tac\/} returns multiple results then so does lcp@104: \hbox{\tt SELECT_GOAL {\it tac} $i$}. lcp@104: lcp@323: {\tt SELECT_GOAL} works by creating a state of the form $\phi\Imp\phi$, lcp@332: with the one subgoal~$\phi$. If subgoal~$i$ has the form $\psi\Imp\theta$ lcp@332: then $(\psi\Imp\theta)\Imp(\psi\Imp\theta)$ is in fact lcp@332: $\List{\psi\Imp\theta;\; \psi}\Imp\theta$, a proof state with two subgoals. lcp@332: Such a proof state might cause tactics to go astray. Therefore {\tt lcp@332: SELECT_GOAL} inserts a quantifier to create the state lcp@323: \[ (\Forall x.\psi\Imp\theta)\Imp(\Forall x.\psi\Imp\theta). \] lcp@104: lcp@323: \item[\ttindexbold{METAHYPS} {\it tacf} $i$]\index{meta-assumptions} lcp@104: takes subgoal~$i$, of the form lcp@104: \[ \Forall x@1 \ldots x@l. \List{\theta@1; \ldots; \theta@k}\Imp\theta, \] lcp@104: and creates the list $\theta'@1$, \ldots, $\theta'@k$ of meta-level lcp@104: assumptions. In these theorems, the subgoal's parameters ($x@1$, lcp@104: \ldots,~$x@l$) become free variables. It supplies the assumptions to lcp@104: $tacf$ and applies the resulting tactic to the proof state lcp@104: $\theta\Imp\theta$. lcp@104: lcp@104: If the resulting proof state is $\List{\phi@1; \ldots; \phi@n} \Imp \phi$, lcp@104: possibly containing $\theta'@1,\ldots,\theta'@k$ as assumptions, then it is lcp@104: lifted back into the original context, yielding $n$ subgoals. lcp@104: lcp@286: Meta-level assumptions may not contain unknowns. Unknowns in the lcp@286: hypotheses $\theta@1,\ldots,\theta@k$ become free variables in $\theta'@1$, lcp@286: \ldots, $\theta'@k$, and are restored afterwards; the {\tt METAHYPS} call lcp@286: cannot instantiate them. Unknowns in $\theta$ may be instantiated. New lcp@323: unknowns in $\phi@1$, \ldots, $\phi@n$ are lifted over the parameters. lcp@104: lcp@104: Here is a typical application. Calling {\tt hyp_res_tac}~$i$ resolves lcp@104: subgoal~$i$ with one of its own assumptions, which may itself have the form lcp@104: of an inference rule (these are called {\bf higher-level assumptions}). lcp@104: \begin{ttbox} lcp@104: val hyp_res_tac = METAHYPS (fn prems => resolve_tac prems 1); lcp@104: \end{ttbox} lcp@332: The function \ttindex{gethyps} is useful for debugging applications of {\tt lcp@332: METAHYPS}. lcp@323: \end{ttdescription} lcp@104: lcp@104: \begin{warn} lcp@104: {\tt METAHYPS} fails if the context or new subgoals contain type unknowns. lcp@104: In principle, the tactical could treat these like ordinary unknowns. lcp@104: \end{warn} lcp@104: lcp@104: lcp@104: \subsection{Scanning for a subgoal by number} lcp@323: \index{tacticals!scanning for subgoals} lcp@104: \begin{ttbox} lcp@104: ALLGOALS : (int -> tactic) -> tactic lcp@104: TRYALL : (int -> tactic) -> tactic lcp@104: SOMEGOAL : (int -> tactic) -> tactic lcp@104: FIRSTGOAL : (int -> tactic) -> tactic lcp@104: REPEAT_SOME : (int -> tactic) -> tactic lcp@104: REPEAT_FIRST : (int -> tactic) -> tactic lcp@104: trace_goalno_tac : (int -> tactic) -> int -> tactic lcp@104: \end{ttbox} lcp@104: These apply a tactic function of type {\tt int -> tactic} to all the lcp@104: subgoal numbers of a proof state, and join the resulting tactics using lcp@104: \ttindex{THEN} or \ttindex{ORELSE}\@. Thus, they apply the tactic to all the lcp@104: subgoals, or to one subgoal. lcp@104: lcp@104: Suppose that the original proof state has $n$ subgoals. lcp@104: lcp@323: \begin{ttdescription} lcp@104: \item[\ttindexbold{ALLGOALS} {\it tacf}] lcp@104: is equivalent to lcp@104: \hbox{\tt$tacf(n)$ THEN \ldots{} THEN $tacf(1)$}. lcp@104: lcp@323: It applies {\it tacf} to all the subgoals, counting downwards (to lcp@104: avoid problems when subgoals are added or deleted). lcp@104: lcp@104: \item[\ttindexbold{TRYALL} {\it tacf}] lcp@104: is equivalent to lcp@323: \hbox{\tt TRY$(tacf(n))$ THEN \ldots{} THEN TRY$(tacf(1))$}. lcp@104: lcp@104: It attempts to apply {\it tacf} to all the subgoals. For instance, lcp@286: the tactic \hbox{\tt TRYALL assume_tac} attempts to solve all the subgoals by lcp@104: assumption. lcp@104: lcp@104: \item[\ttindexbold{SOMEGOAL} {\it tacf}] lcp@104: is equivalent to lcp@104: \hbox{\tt$tacf(n)$ ORELSE \ldots{} ORELSE $tacf(1)$}. lcp@104: lcp@323: It applies {\it tacf} to one subgoal, counting downwards. For instance, lcp@286: the tactic \hbox{\tt SOMEGOAL assume_tac} solves one subgoal by assumption, lcp@286: failing if this is impossible. lcp@104: lcp@104: \item[\ttindexbold{FIRSTGOAL} {\it tacf}] lcp@104: is equivalent to lcp@104: \hbox{\tt$tacf(1)$ ORELSE \ldots{} ORELSE $tacf(n)$}. lcp@104: lcp@323: It applies {\it tacf} to one subgoal, counting upwards. lcp@104: lcp@104: \item[\ttindexbold{REPEAT_SOME} {\it tacf}] lcp@323: applies {\it tacf} once or more to a subgoal, counting downwards. lcp@104: lcp@104: \item[\ttindexbold{REPEAT_FIRST} {\it tacf}] lcp@323: applies {\it tacf} once or more to a subgoal, counting upwards. lcp@104: lcp@104: \item[\ttindexbold{trace_goalno_tac} {\it tac} {\it i}] lcp@104: applies \hbox{\it tac i\/} to the proof state. If the resulting sequence lcp@104: is non-empty, then it is returned, with the side-effect of printing {\tt lcp@104: Subgoal~$i$ selected}. Otherwise, {\tt trace_goalno_tac} returns the empty lcp@104: sequence and prints nothing. lcp@104: lcp@323: It indicates that `the tactic worked for subgoal~$i$' and is mainly used lcp@104: with {\tt SOMEGOAL} and {\tt FIRSTGOAL}. lcp@323: \end{ttdescription} lcp@104: lcp@104: lcp@104: \subsection{Joining tactic functions} lcp@323: \index{tacticals!joining tactic functions} lcp@104: \begin{ttbox} lcp@104: THEN' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic \hfill{\bf infix 1} lcp@104: ORELSE' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic \hfill{\bf infix} lcp@104: APPEND' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic \hfill{\bf infix} lcp@104: INTLEAVE' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic \hfill{\bf infix} lcp@104: EVERY' : ('a -> tactic) list -> 'a -> tactic lcp@104: FIRST' : ('a -> tactic) list -> 'a -> tactic lcp@104: \end{ttbox} lcp@104: These help to express tactics that specify subgoal numbers. The tactic lcp@104: \begin{ttbox} lcp@104: SOMEGOAL (fn i => resolve_tac rls i ORELSE eresolve_tac erls i) lcp@104: \end{ttbox} lcp@104: can be simplified to lcp@104: \begin{ttbox} lcp@104: SOMEGOAL (resolve_tac rls ORELSE' eresolve_tac erls) lcp@104: \end{ttbox} lcp@104: Note that {\tt TRY'}, {\tt REPEAT'}, {\tt DEPTH_FIRST'}, etc.\ are not lcp@104: provided, because function composition accomplishes the same purpose. lcp@104: The tactic lcp@104: \begin{ttbox} lcp@104: ALLGOALS (fn i => REPEAT (etac exE i ORELSE atac i)) lcp@104: \end{ttbox} lcp@104: can be simplified to lcp@104: \begin{ttbox} lcp@104: ALLGOALS (REPEAT o (etac exE ORELSE' atac)) lcp@104: \end{ttbox} lcp@104: These tacticals are polymorphic; $x$ need not be an integer. lcp@104: \begin{center} \tt lcp@104: \begin{tabular}{r@{\rm\ \ yields\ \ }l} lcp@323: $(tacf@1$~~THEN'~~$tacf@2)(x)$ \index{*THEN'} & lcp@104: $tacf@1(x)$~~THEN~~$tacf@2(x)$ \\ lcp@104: lcp@323: $(tacf@1$ ORELSE' $tacf@2)(x)$ \index{*ORELSE'} & lcp@104: $tacf@1(x)$ ORELSE $tacf@2(x)$ \\ lcp@104: lcp@323: $(tacf@1$ APPEND' $tacf@2)(x)$ \index{*APPEND'} & lcp@104: $tacf@1(x)$ APPEND $tacf@2(x)$ \\ lcp@104: lcp@323: $(tacf@1$ INTLEAVE' $tacf@2)(x)$ \index{*INTLEAVE'} & lcp@104: $tacf@1(x)$ INTLEAVE $tacf@2(x)$ \\ lcp@104: lcp@104: EVERY' $[tacf@1,\ldots,tacf@n] \; (x)$ \index{*EVERY'} & lcp@104: EVERY $[tacf@1(x),\ldots,tacf@n(x)]$ \\ lcp@104: lcp@104: FIRST' $[tacf@1,\ldots,tacf@n] \; (x)$ \index{*FIRST'} & lcp@104: FIRST $[tacf@1(x),\ldots,tacf@n(x)]$ lcp@104: \end{tabular} lcp@104: \end{center} lcp@104: lcp@104: lcp@104: \subsection{Applying a list of tactics to 1} lcp@323: \index{tacticals!joining tactic functions} lcp@104: \begin{ttbox} lcp@104: EVERY1: (int -> tactic) list -> tactic lcp@104: FIRST1: (int -> tactic) list -> tactic lcp@104: \end{ttbox} lcp@104: A common proof style is to treat the subgoals as a stack, always lcp@104: restricting attention to the first subgoal. Such proofs contain long lists lcp@104: of tactics, each applied to~1. These can be simplified using {\tt EVERY1} lcp@104: and {\tt FIRST1}: lcp@104: \begin{center} \tt lcp@104: \begin{tabular}{r@{\rm\ \ abbreviates\ \ }l} lcp@104: EVERY1 $[tacf@1,\ldots,tacf@n]$ \indexbold{*EVERY1} & lcp@104: EVERY $[tacf@1(1),\ldots,tacf@n(1)]$ \\ lcp@104: lcp@104: FIRST1 $[tacf@1,\ldots,tacf@n]$ \indexbold{*FIRST1} & lcp@104: FIRST $[tacf@1(1),\ldots,tacf@n(1)]$ lcp@104: \end{tabular} lcp@104: \end{center} lcp@104: lcp@104: \index{tacticals|)} wenzelm@5371: wenzelm@5371: wenzelm@5371: %%% Local Variables: wenzelm@5371: %%% mode: latex wenzelm@5371: %%% TeX-master: "ref" wenzelm@5371: %%% End: