
wenzelm@30081: theory Tactic
wenzelm@30081: imports Base
wenzelm@30081: begin
wenzelm@18537: 
wenzelm@20452: chapter {* Tactical reasoning *}
wenzelm@18537: 
wenzelm@34997: text {* Tactical reasoning works by refining an initial claim in a
wenzelm@20474:   backwards fashion, until a solved form is reached.  A @{text "goal"}
wenzelm@20474:   consists of several subgoals that need to be solved in order to
wenzelm@20474:   achieve the main statement; zero subgoals means that the proof may
wenzelm@20474:   be finished.  A @{text "tactic"} is a refinement operation that maps
wenzelm@20474:   a goal to a lazy sequence of potential successors.  A @{text
wenzelm@34997:   "tactical"} is a combinator for composing tactics.  *}
wenzelm@18537: 
wenzelm@18537: 
wenzelm@18537: section {* Goals \label{sec:tactical-goals} *}
wenzelm@18537: 
wenzelm@20451: text {*
wenzelm@30084:   Isabelle/Pure represents a goal as a theorem stating that the
wenzelm@30084:   subgoals imply the main goal: @{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow>
wenzelm@30084:   C"}.  The outermost goal structure is that of a Horn Clause: i.e.\
wenzelm@30084:   an iterated implication without any quantifiers\footnote{Recall that
wenzelm@30084:   outermost @{text "\<And>x. \<phi>[x]"} is always represented via schematic
wenzelm@30084:   variables in the body: @{text "\<phi>[?x]"}.  These variables may get
wenzelm@30084:   instantiated during the course of reasoning.}.  For @{text "n = 0"}
wenzelm@30084:   a goal is called ``solved''.
wenzelm@18537: 
wenzelm@30087:   The structure of each subgoal @{text "A\<^sub>i"} is that of a
wenzelm@30087:   general Hereditary Harrop Formula @{text "\<And>x\<^sub>1 \<dots>
wenzelm@30087:   \<And>x\<^sub>k. H\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> H\<^sub>m \<Longrightarrow> B"}.  Here @{text
wenzelm@30087:   "x\<^sub>1, \<dots>, x\<^sub>k"} are goal parameters, i.e.\
wenzelm@30087:   arbitrary-but-fixed entities of certain types, and @{text
wenzelm@30087:   "H\<^sub>1, \<dots>, H\<^sub>m"} are goal hypotheses, i.e.\ facts that may
wenzelm@30087:   be assumed locally.  Together, this forms the goal context of the
wenzelm@30087:   conclusion @{text B} to be established.  The goal hypotheses may be
wenzelm@30087:   again arbitrary Hereditary Harrop Formulas, although the level of
wenzelm@30087:   nesting rarely exceeds 1--2 in practice.
wenzelm@18537: 
wenzelm@20451:   The main conclusion @{text C} is internally marked as a protected
wenzelm@30084:   proposition, which is represented explicitly by the notation @{text
wenzelm@34997:   "#C"} here.  This ensures that the decomposition into subgoals and
wenzelm@34997:   main conclusion is well-defined for arbitrarily structured claims.
wenzelm@18537: 
wenzelm@20451:   \medskip Basic goal management is performed via the following
wenzelm@20451:   Isabelle/Pure rules:
wenzelm@18537: 
wenzelm@18537:   \[
wenzelm@18537:   \infer[@{text "(init)"}]{@{text "C \<Longrightarrow> #C"}}{} \qquad
wenzelm@20547:   \infer[@{text "(finish)"}]{@{text "C"}}{@{text "#C"}}
wenzelm@18537:   \]
wenzelm@18537: 
wenzelm@18537:   \medskip The following low-level variants admit general reasoning
wenzelm@18537:   with protected propositions:
wenzelm@18537: 
wenzelm@18537:   \[
wenzelm@18537:   \infer[@{text "(protect)"}]{@{text "#C"}}{@{text "C"}} \qquad
wenzelm@18537:   \infer[@{text "(conclude)"}]{@{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> C"}}{@{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> #C"}}
wenzelm@18537:   \]
wenzelm@18537: *}
wenzelm@18537: 
wenzelm@18537: text %mlref {*
wenzelm@18537:   \begin{mldecls}
wenzelm@18537:   @{index_ML Goal.init: "cterm -> thm"} \\
wenzelm@32207:   @{index_ML Goal.finish: "Proof.context -> thm -> thm"} \\
wenzelm@18537:   @{index_ML Goal.protect: "thm -> thm"} \\
wenzelm@18537:   @{index_ML Goal.conclude: "thm -> thm"} \\
wenzelm@18537:   \end{mldecls}
wenzelm@18537: 
wenzelm@18537:   \begin{description}
wenzelm@18537: 
wenzelm@20474:   \item @{ML "Goal.init"}~@{text C} initializes a tactical goal from
wenzelm@20474:   the well-formed proposition @{text C}.
wenzelm@18537: 
wenzelm@32207:   \item @{ML "Goal.finish"}~@{text "ctxt thm"} checks whether theorem
wenzelm@20474:   @{text "thm"} is a solved goal (no subgoals), and concludes the
wenzelm@32207:   result by removing the goal protection.  The context is only
wenzelm@32207:   required for printing error messages.
wenzelm@18537: 
wenzelm@20474:   \item @{ML "Goal.protect"}~@{text "thm"} protects the full statement
wenzelm@20474:   of theorem @{text "thm"}.
wenzelm@18537: 
wenzelm@20474:   \item @{ML "Goal.conclude"}~@{text "thm"} removes the goal
wenzelm@20474:   protection, even if there are pending subgoals.
wenzelm@18537: 
wenzelm@18537:   \end{description}
wenzelm@18537: *}
wenzelm@18537: 
wenzelm@18537: 
wenzelm@18537: section {* Tactics *}
wenzelm@18537: 
wenzelm@28781: text {* A @{text "tactic"} is a function @{text "goal \<rightarrow> goal\<^sup>*\<^sup>*"} that
wenzelm@28781:   maps a given goal state (represented as a theorem, cf.\
wenzelm@28781:   \secref{sec:tactical-goals}) to a lazy sequence of potential
wenzelm@28781:   successor states.  The underlying sequence implementation is lazy
wenzelm@28781:   both in head and tail, and is purely functional in \emph{not}
wenzelm@28781:   supporting memoing.\footnote{The lack of memoing and the strict
wenzelm@28781:   nature of SML requires some care when working with low-level
wenzelm@28781:   sequence operations, to avoid duplicate or premature evaluation of
wenzelm@34997:   results.  It also means that modified runtime behavior, such as
wenzelm@34997:   timeout, is very hard to achieve for general tactics.}
wenzelm@18537: 
wenzelm@28781:   An \emph{empty result sequence} means that the tactic has failed: in
wenzelm@34997:   a compound tactic expression other tactics might be tried instead,
wenzelm@28781:   or the whole refinement step might fail outright, producing a
wenzelm@34997:   toplevel error message in the end.  When implementing tactics from
wenzelm@34997:   scratch, one should take care to observe the basic protocol of
wenzelm@34997:   mapping regular error conditions to an empty result; only serious
wenzelm@34997:   faults should emerge as exceptions.
wenzelm@18537: 
wenzelm@28781:   By enumerating \emph{multiple results}, a tactic can easily express
wenzelm@28781:   the potential outcome of an internal search process.  There are also
wenzelm@28781:   combinators for building proof tools that involve search
wenzelm@28781:   systematically, see also \secref{sec:tacticals}.
wenzelm@18537: 
wenzelm@34997:   \medskip As explained before, a goal state essentially consists of a
wenzelm@34997:   list of subgoals that imply the main goal (conclusion).  Tactics may
wenzelm@34997:   operate on all subgoals or on a particularly specified subgoal, but
wenzelm@34997:   must not change the main conclusion (apart from instantiating
wenzelm@34997:   schematic goal variables).
wenzelm@18537: 
wenzelm@28781:   Tactics with explicit \emph{subgoal addressing} are of the form
wenzelm@28781:   @{text "int \<rightarrow> tactic"} and may be applied to a particular subgoal
wenzelm@28781:   (counting from 1).  If the subgoal number is out of range, the
wenzelm@28781:   tactic should fail with an empty result sequence, but must not raise
wenzelm@28781:   an exception!
wenzelm@28781: 
wenzelm@28781:   Operating on a particular subgoal means to replace it by an interval
wenzelm@28781:   of zero or more subgoals in the same place; other subgoals must not
wenzelm@28781:   be affected, apart from instantiating schematic variables ranging
wenzelm@28781:   over the whole goal state.
wenzelm@28781: 
wenzelm@28781:   A common pattern of composing tactics with subgoal addressing is to
wenzelm@28781:   try the first one, and then the second one only if the subgoal has
wenzelm@28781:   not been solved yet.  Special care is required here to avoid bumping
wenzelm@28782:   into unrelated subgoals that happen to come after the original
wenzelm@28782:   subgoal.  Assuming that there is only a single initial subgoal is a
wenzelm@28782:   very common error when implementing tactics!
wenzelm@28782: 
wenzelm@28782:   Tactics with internal subgoal addressing should expose the subgoal
wenzelm@28782:   index as @{text "int"} argument in full generality; a hardwired
wenzelm@34997:   subgoal 1 is not acceptable.
wenzelm@28781:   
wenzelm@28781:   \medskip The main well-formedness conditions for proper tactics are
wenzelm@28781:   summarized as follows.
wenzelm@28781: 
wenzelm@28781:   \begin{itemize}
wenzelm@28781: 
wenzelm@28781:   \item General tactic failure is indicated by an empty result, only
wenzelm@28781:   serious faults may produce an exception.
wenzelm@28781: 
wenzelm@28781:   \item The main conclusion must not be changed, apart from
wenzelm@28781:   instantiating schematic variables.
wenzelm@28781: 
wenzelm@28781:   \item A tactic operates either uniformly on all subgoals, or
wenzelm@28781:   specifically on a selected subgoal (without bumping into unrelated
wenzelm@28781:   subgoals).
wenzelm@28781: 
wenzelm@28781:   \item Range errors in subgoal addressing produce an empty result.
wenzelm@28781: 
wenzelm@28781:   \end{itemize}
wenzelm@28782: 
wenzelm@28782:   Some of these conditions are checked by higher-level goal
wenzelm@34997:   infrastructure (\secref{sec:struct-goals}); others are not checked
wenzelm@28782:   explicitly, and violating them merely results in ill-behaved tactics
wenzelm@28782:   experienced by the user (e.g.\ tactics that insist in being
wenzelm@34997:   applicable only to singleton goals, or prevent composition via
wenzelm@34997:   standard tacticals).
wenzelm@28782: *}
wenzelm@28782: 
wenzelm@28782: text %mlref {*
wenzelm@28782:   \begin{mldecls}
wenzelm@28782:   @{index_ML_type tactic: "thm -> thm Seq.seq"} \\
wenzelm@28783:   @{index_ML no_tac: tactic} \\
wenzelm@28783:   @{index_ML all_tac: tactic} \\
wenzelm@28783:   @{index_ML print_tac: "string -> tactic"} \\[1ex]
wenzelm@28783:   @{index_ML PRIMITIVE: "(thm -> thm) -> tactic"} \\[1ex]
wenzelm@28782:   @{index_ML SUBGOAL: "(term * int -> tactic) -> int -> tactic"} \\
wenzelm@28782:   @{index_ML CSUBGOAL: "(cterm * int -> tactic) -> int -> tactic"} \\
wenzelm@28782:   \end{mldecls}
wenzelm@28782: 
wenzelm@28782:   \begin{description}
wenzelm@28782: 
wenzelm@28782:   \item @{ML_type tactic} represents tactics.  The well-formedness
wenzelm@28782:   conditions described above need to be observed.  See also @{"file"
wenzelm@28782:   "~~/src/Pure/General/seq.ML"} for the underlying implementation of
wenzelm@28782:   lazy sequences.
wenzelm@28782: 
wenzelm@28782:   \item @{ML_type "int -> tactic"} represents tactics with explicit
wenzelm@28782:   subgoal addressing, with well-formedness conditions as described
wenzelm@28782:   above.
wenzelm@28782: 
wenzelm@28783:   \item @{ML no_tac} is a tactic that always fails, returning the
wenzelm@28783:   empty sequence.
wenzelm@28783: 
wenzelm@28783:   \item @{ML all_tac} is a tactic that always succeeds, returning a
wenzelm@28783:   singleton sequence with unchanged goal state.
wenzelm@28783: 
wenzelm@28783:   \item @{ML print_tac}~@{text "message"} is like @{ML all_tac}, but
wenzelm@28783:   prints a message together with the goal state on the tracing
wenzelm@28783:   channel.
wenzelm@28783: 
wenzelm@28782:   \item @{ML PRIMITIVE}~@{text rule} turns a primitive inference rule
wenzelm@28782:   into a tactic with unique result.  Exception @{ML THM} is considered
wenzelm@28782:   a regular tactic failure and produces an empty result; other
wenzelm@28782:   exceptions are passed through.
wenzelm@28782: 
wenzelm@28782:   \item @{ML SUBGOAL}~@{text "(fn (subgoal, i) => tactic)"} is the
wenzelm@28783:   most basic form to produce a tactic with subgoal addressing.  The
wenzelm@28782:   given abstraction over the subgoal term and subgoal number allows to
wenzelm@28782:   peek at the relevant information of the full goal state.  The
wenzelm@28782:   subgoal range is checked as required above.
wenzelm@28782: 
wenzelm@28782:   \item @{ML CSUBGOAL} is similar to @{ML SUBGOAL}, but passes the
wenzelm@28783:   subgoal as @{ML_type cterm} instead of raw @{ML_type term}.  This
wenzelm@28782:   avoids expensive re-certification in situations where the subgoal is
wenzelm@28782:   used directly for primitive inferences.
wenzelm@28782: 
wenzelm@28782:   \end{description}
wenzelm@18537: *}
wenzelm@18537: 
wenzelm@28781: 
wenzelm@28785: subsection {* Resolution and assumption tactics \label{sec:resolve-assume-tac} *}
wenzelm@28783: 
wenzelm@28783: text {* \emph{Resolution} is the most basic mechanism for refining a
wenzelm@28783:   subgoal using a theorem as object-level rule.
wenzelm@28783:   \emph{Elim-resolution} is particularly suited for elimination rules:
wenzelm@28783:   it resolves with a rule, proves its first premise by assumption, and
wenzelm@28783:   finally deletes that assumption from any new subgoals.
wenzelm@28783:   \emph{Destruct-resolution} is like elim-resolution, but the given
wenzelm@28783:   destruction rules are first turned into canonical elimination
wenzelm@28783:   format.  \emph{Forward-resolution} is like destruct-resolution, but
wenzelm@28785:   without deleting the selected assumption.  The @{text "r/e/d/f"}
wenzelm@28785:   naming convention is maintained for several different kinds of
wenzelm@28785:   resolution rules and tactics.
wenzelm@28783: 
wenzelm@28783:   Assumption tactics close a subgoal by unifying some of its premises
wenzelm@28783:   against its conclusion.
wenzelm@28783: 
wenzelm@28783:   \medskip All the tactics in this section operate on a subgoal
wenzelm@28783:   designated by a positive integer.  Other subgoals might be affected
wenzelm@28783:   indirectly, due to instantiation of schematic variables.
wenzelm@28783: 
wenzelm@28783:   There are various sources of non-determinism, the tactic result
wenzelm@28783:   sequence enumerates all possibilities of the following choices (if
wenzelm@28783:   applicable):
wenzelm@28783: 
wenzelm@28783:   \begin{enumerate}
wenzelm@28783: 
wenzelm@28783:   \item selecting one of the rules given as argument to the tactic;
wenzelm@28783: 
wenzelm@28783:   \item selecting a subgoal premise to eliminate, unifying it against
wenzelm@28783:   the first premise of the rule;
wenzelm@28783: 
wenzelm@28783:   \item unifying the conclusion of the subgoal to the conclusion of
wenzelm@28783:   the rule.
wenzelm@28783: 
wenzelm@28783:   \end{enumerate}
wenzelm@28783: 
wenzelm@28783:   Recall that higher-order unification may produce multiple results
wenzelm@28783:   that are enumerated here.
wenzelm@28783: *}
wenzelm@28783: 
wenzelm@28783: text %mlref {*
wenzelm@28783:   \begin{mldecls}
wenzelm@28783:   @{index_ML resolve_tac: "thm list -> int -> tactic"} \\
wenzelm@28783:   @{index_ML eresolve_tac: "thm list -> int -> tactic"} \\
wenzelm@28783:   @{index_ML dresolve_tac: "thm list -> int -> tactic"} \\
wenzelm@28783:   @{index_ML forward_tac: "thm list -> int -> tactic"} \\[1ex]
wenzelm@28783:   @{index_ML assume_tac: "int -> tactic"} \\
wenzelm@28783:   @{index_ML eq_assume_tac: "int -> tactic"} \\[1ex]
wenzelm@28783:   @{index_ML match_tac: "thm list -> int -> tactic"} \\
wenzelm@28783:   @{index_ML ematch_tac: "thm list -> int -> tactic"} \\
wenzelm@28783:   @{index_ML dmatch_tac: "thm list -> int -> tactic"} \\
wenzelm@28783:   \end{mldecls}
wenzelm@28783: 
wenzelm@28783:   \begin{description}
wenzelm@28783: 
wenzelm@28783:   \item @{ML resolve_tac}~@{text "thms i"} refines the goal state
wenzelm@28783:   using the given theorems, which should normally be introduction
wenzelm@28783:   rules.  The tactic resolves a rule's conclusion with subgoal @{text
wenzelm@28783:   i}, replacing it by the corresponding versions of the rule's
wenzelm@28783:   premises.
wenzelm@28783: 
wenzelm@28783:   \item @{ML eresolve_tac}~@{text "thms i"} performs elim-resolution
wenzelm@28783:   with the given theorems, which should normally be elimination rules.
wenzelm@28783: 
wenzelm@28783:   \item @{ML dresolve_tac}~@{text "thms i"} performs
wenzelm@28783:   destruct-resolution with the given theorems, which should normally
wenzelm@28783:   be destruction rules.  This replaces an assumption by the result of
wenzelm@28783:   applying one of the rules.
wenzelm@28783: 
wenzelm@28783:   \item @{ML forward_tac} is like @{ML dresolve_tac} except that the
wenzelm@28783:   selected assumption is not deleted.  It applies a rule to an
wenzelm@28783:   assumption, adding the result as a new assumption.
wenzelm@28783: 
wenzelm@28783:   \item @{ML assume_tac}~@{text i} attempts to solve subgoal @{text i}
wenzelm@28783:   by assumption (modulo higher-order unification).
wenzelm@28783: 
wenzelm@28783:   \item @{ML eq_assume_tac} is similar to @{ML assume_tac}, but checks
wenzelm@28783:   only for immediate @{text "\<alpha>"}-convertibility instead of using
wenzelm@28783:   unification.  It succeeds (with a unique next state) if one of the
wenzelm@28783:   assumptions is equal to the subgoal's conclusion.  Since it does not
wenzelm@28783:   instantiate variables, it cannot make other subgoals unprovable.
wenzelm@28783: 
wenzelm@28783:   \item @{ML match_tac}, @{ML ematch_tac}, and @{ML dmatch_tac} are
wenzelm@28783:   similar to @{ML resolve_tac}, @{ML eresolve_tac}, and @{ML
wenzelm@28783:   dresolve_tac}, respectively, but do not instantiate schematic
wenzelm@28783:   variables in the goal state.
wenzelm@28783: 
wenzelm@28783:   Flexible subgoals are not updated at will, but are left alone.
wenzelm@28783:   Strictly speaking, matching means to treat the unknowns in the goal
wenzelm@28783:   state as constants; these tactics merely discard unifiers that would
wenzelm@28783:   update the goal state.
wenzelm@28783: 
wenzelm@28783:   \end{description}
wenzelm@28783: *}
wenzelm@28783: 
wenzelm@28783: 
wenzelm@28785: subsection {* Explicit instantiation within a subgoal context *}
wenzelm@28785: 
wenzelm@28785: text {* The main resolution tactics (\secref{sec:resolve-assume-tac})
wenzelm@28785:   use higher-order unification, which works well in many practical
wenzelm@28785:   situations despite its daunting theoretical properties.
wenzelm@28785:   Nonetheless, there are important problem classes where unguided
wenzelm@28785:   higher-order unification is not so useful.  This typically involves
wenzelm@28785:   rules like universal elimination, existential introduction, or
wenzelm@28785:   equational substitution.  Here the unification problem involves
wenzelm@28785:   fully flexible @{text "?P ?x"} schemes, which are hard to manage
wenzelm@28785:   without further hints.
wenzelm@28785: 
wenzelm@28785:   By providing a (small) rigid term for @{text "?x"} explicitly, the
wenzelm@28785:   remaining unification problem is to assign a (large) term to @{text
wenzelm@28785:   "?P"}, according to the shape of the given subgoal.  This is
wenzelm@28785:   sufficiently well-behaved in most practical situations.
wenzelm@28785: 
wenzelm@28785:   \medskip Isabelle provides separate versions of the standard @{text
wenzelm@28785:   "r/e/d/f"} resolution tactics that allow to provide explicit
wenzelm@28785:   instantiations of unknowns of the given rule, wrt.\ terms that refer
wenzelm@28785:   to the implicit context of the selected subgoal.
wenzelm@28785: 
wenzelm@28785:   An instantiation consists of a list of pairs of the form @{text
wenzelm@28785:   "(?x, t)"}, where @{text ?x} is a schematic variable occurring in
wenzelm@28785:   the given rule, and @{text t} is a term from the current proof
wenzelm@28785:   context, augmented by the local goal parameters of the selected
wenzelm@28785:   subgoal; cf.\ the @{text "focus"} operation described in
wenzelm@28785:   \secref{sec:variables}.
wenzelm@28785: 
wenzelm@28785:   Entering the syntactic context of a subgoal is a brittle operation,
wenzelm@28785:   because its exact form is somewhat accidental, and the choice of
wenzelm@28785:   bound variable names depends on the presence of other local and
wenzelm@28785:   global names.  Explicit renaming of subgoal parameters prior to
wenzelm@28785:   explicit instantiation might help to achieve a bit more robustness.
wenzelm@28785: 
wenzelm@28785:   Type instantiations may be given as well, via pairs like @{text
wenzelm@28785:   "(?'a, \<tau>)"}.  Type instantiations are distinguished from term
wenzelm@28785:   instantiations by the syntactic form of the schematic variable.
wenzelm@28785:   Types are instantiated before terms are.  Since term instantiation
wenzelm@34997:   already performs simple type-inference, so explicit type
wenzelm@28785:   instantiations are seldom necessary.
wenzelm@28785: *}
wenzelm@28785: 
wenzelm@28785: text %mlref {*
wenzelm@28785:   \begin{mldecls}
wenzelm@28785:   @{index_ML res_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\
wenzelm@28785:   @{index_ML eres_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\
wenzelm@28785:   @{index_ML dres_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\
wenzelm@28785:   @{index_ML forw_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\[1ex]
wenzelm@28785:   @{index_ML rename_tac: "string list -> int -> tactic"} \\
wenzelm@28785:   \end{mldecls}
wenzelm@28785: 
wenzelm@28785:   \begin{description}
wenzelm@28785: 
wenzelm@28785:   \item @{ML res_inst_tac}~@{text "ctxt insts thm i"} instantiates the
wenzelm@28785:   rule @{text thm} with the instantiations @{text insts}, as described
wenzelm@28785:   above, and then performs resolution on subgoal @{text i}.
wenzelm@28785:   
wenzelm@28785:   \item @{ML eres_inst_tac} is like @{ML res_inst_tac}, but performs
wenzelm@28785:   elim-resolution.
wenzelm@28785: 
wenzelm@28785:   \item @{ML dres_inst_tac} is like @{ML res_inst_tac}, but performs
wenzelm@28785:   destruct-resolution.
wenzelm@28785: 
wenzelm@28785:   \item @{ML forw_inst_tac} is like @{ML dres_inst_tac} except that
wenzelm@28785:   the selected assumption is not deleted.
wenzelm@28785: 
wenzelm@28785:   \item @{ML rename_tac}~@{text "names i"} renames the innermost
wenzelm@28785:   parameters of subgoal @{text i} according to the provided @{text
wenzelm@28785:   names} (which need to be distinct indentifiers).
wenzelm@28785: 
wenzelm@28785:   \end{description}
wenzelm@34997: 
wenzelm@34997:   For historical reasons, the above instantiation tactics take
wenzelm@34997:   unparsed string arguments, which makes them hard to use in general
wenzelm@34997:   ML code.  The slightly more advanced @{ML Subgoal.FOCUS} combinator
wenzelm@34997:   of \secref{sec:struct-goals} allows to refer to internal goal
wenzelm@34997:   structure with explicit context management.
wenzelm@28785: *}
wenzelm@28785: 
wenzelm@28785: 
wenzelm@28781: section {* Tacticals \label{sec:tacticals} *}
wenzelm@18537: 
wenzelm@18537: text {*
wenzelm@30084:   A \emph{tactical} is a functional combinator for building up complex
wenzelm@30084:   tactics from simpler ones.  Typical tactical perform sequential
wenzelm@30084:   composition, disjunction (choice), iteration, or goal addressing.
wenzelm@30084:   Various search strategies may be expressed via tacticals.
wenzelm@18537: 
wenzelm@30084:   \medskip FIXME
wenzelm@18537: *}
wenzelm@30273: 
wenzelm@18537: end




