src/Doc/Implementation/Tactic.thy
author wenzelm
Sun Nov 09 17:04:14 2014 +0100 (2014-11-09)
changeset 58957 c9e744ea8a38
parent 58956 a816aa3ff391
child 58963 26bf09b95dda
permissions -rw-r--r--
proper context for match_tac etc.;
     1 theory Tactic
     2 imports Base
     3 begin
     4 
     5 chapter \<open>Tactical reasoning\<close>
     6 
     7 text \<open>Tactical reasoning works by refining an initial claim in a
     8   backwards fashion, until a solved form is reached.  A @{text "goal"}
     9   consists of several subgoals that need to be solved in order to
    10   achieve the main statement; zero subgoals means that the proof may
    11   be finished.  A @{text "tactic"} is a refinement operation that maps
    12   a goal to a lazy sequence of potential successors.  A @{text
    13   "tactical"} is a combinator for composing tactics.\<close>
    14 
    15 
    16 section \<open>Goals \label{sec:tactical-goals}\<close>
    17 
    18 text \<open>
    19   Isabelle/Pure represents a goal as a theorem stating that the
    20   subgoals imply the main goal: @{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow>
    21   C"}.  The outermost goal structure is that of a Horn Clause: i.e.\
    22   an iterated implication without any quantifiers\footnote{Recall that
    23   outermost @{text "\<And>x. \<phi>[x]"} is always represented via schematic
    24   variables in the body: @{text "\<phi>[?x]"}.  These variables may get
    25   instantiated during the course of reasoning.}.  For @{text "n = 0"}
    26   a goal is called ``solved''.
    27 
    28   The structure of each subgoal @{text "A\<^sub>i"} is that of a
    29   general Hereditary Harrop Formula @{text "\<And>x\<^sub>1 \<dots>
    30   \<And>x\<^sub>k. H\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> H\<^sub>m \<Longrightarrow> B"}.  Here @{text
    31   "x\<^sub>1, \<dots>, x\<^sub>k"} are goal parameters, i.e.\
    32   arbitrary-but-fixed entities of certain types, and @{text
    33   "H\<^sub>1, \<dots>, H\<^sub>m"} are goal hypotheses, i.e.\ facts that may
    34   be assumed locally.  Together, this forms the goal context of the
    35   conclusion @{text B} to be established.  The goal hypotheses may be
    36   again arbitrary Hereditary Harrop Formulas, although the level of
    37   nesting rarely exceeds 1--2 in practice.
    38 
    39   The main conclusion @{text C} is internally marked as a protected
    40   proposition, which is represented explicitly by the notation @{text
    41   "#C"} here.  This ensures that the decomposition into subgoals and
    42   main conclusion is well-defined for arbitrarily structured claims.
    43 
    44   \medskip Basic goal management is performed via the following
    45   Isabelle/Pure rules:
    46 
    47   \[
    48   \infer[@{text "(init)"}]{@{text "C \<Longrightarrow> #C"}}{} \qquad
    49   \infer[@{text "(finish)"}]{@{text "C"}}{@{text "#C"}}
    50   \]
    51 
    52   \medskip The following low-level variants admit general reasoning
    53   with protected propositions:
    54 
    55   \[
    56   \infer[@{text "(protect n)"}]{@{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> #C"}}{@{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> C"}}
    57   \]
    58   \[
    59   \infer[@{text "(conclude)"}]{@{text "A \<Longrightarrow> \<dots> \<Longrightarrow> C"}}{@{text "A \<Longrightarrow> \<dots> \<Longrightarrow> #C"}}
    60   \]
    61 \<close>
    62 
    63 text %mlref \<open>
    64   \begin{mldecls}
    65   @{index_ML Goal.init: "cterm -> thm"} \\
    66   @{index_ML Goal.finish: "Proof.context -> thm -> thm"} \\
    67   @{index_ML Goal.protect: "int -> thm -> thm"} \\
    68   @{index_ML Goal.conclude: "thm -> thm"} \\
    69   \end{mldecls}
    70 
    71   \begin{description}
    72 
    73   \item @{ML "Goal.init"}~@{text C} initializes a tactical goal from
    74   the well-formed proposition @{text C}.
    75 
    76   \item @{ML "Goal.finish"}~@{text "ctxt thm"} checks whether theorem
    77   @{text "thm"} is a solved goal (no subgoals), and concludes the
    78   result by removing the goal protection.  The context is only
    79   required for printing error messages.
    80 
    81   \item @{ML "Goal.protect"}~@{text "n thm"} protects the statement
    82   of theorem @{text "thm"}.  The parameter @{text n} indicates the
    83   number of premises to be retained.
    84 
    85   \item @{ML "Goal.conclude"}~@{text "thm"} removes the goal
    86   protection, even if there are pending subgoals.
    87 
    88   \end{description}
    89 \<close>
    90 
    91 
    92 section \<open>Tactics\label{sec:tactics}\<close>
    93 
    94 text \<open>A @{text "tactic"} is a function @{text "goal \<rightarrow> goal\<^sup>*\<^sup>*"} that
    95   maps a given goal state (represented as a theorem, cf.\
    96   \secref{sec:tactical-goals}) to a lazy sequence of potential
    97   successor states.  The underlying sequence implementation is lazy
    98   both in head and tail, and is purely functional in \emph{not}
    99   supporting memoing.\footnote{The lack of memoing and the strict
   100   nature of ML requires some care when working with low-level
   101   sequence operations, to avoid duplicate or premature evaluation of
   102   results.  It also means that modified runtime behavior, such as
   103   timeout, is very hard to achieve for general tactics.}
   104 
   105   An \emph{empty result sequence} means that the tactic has failed: in
   106   a compound tactic expression other tactics might be tried instead,
   107   or the whole refinement step might fail outright, producing a
   108   toplevel error message in the end.  When implementing tactics from
   109   scratch, one should take care to observe the basic protocol of
   110   mapping regular error conditions to an empty result; only serious
   111   faults should emerge as exceptions.
   112 
   113   By enumerating \emph{multiple results}, a tactic can easily express
   114   the potential outcome of an internal search process.  There are also
   115   combinators for building proof tools that involve search
   116   systematically, see also \secref{sec:tacticals}.
   117 
   118   \medskip As explained before, a goal state essentially consists of a
   119   list of subgoals that imply the main goal (conclusion).  Tactics may
   120   operate on all subgoals or on a particularly specified subgoal, but
   121   must not change the main conclusion (apart from instantiating
   122   schematic goal variables).
   123 
   124   Tactics with explicit \emph{subgoal addressing} are of the form
   125   @{text "int \<rightarrow> tactic"} and may be applied to a particular subgoal
   126   (counting from 1).  If the subgoal number is out of range, the
   127   tactic should fail with an empty result sequence, but must not raise
   128   an exception!
   129 
   130   Operating on a particular subgoal means to replace it by an interval
   131   of zero or more subgoals in the same place; other subgoals must not
   132   be affected, apart from instantiating schematic variables ranging
   133   over the whole goal state.
   134 
   135   A common pattern of composing tactics with subgoal addressing is to
   136   try the first one, and then the second one only if the subgoal has
   137   not been solved yet.  Special care is required here to avoid bumping
   138   into unrelated subgoals that happen to come after the original
   139   subgoal.  Assuming that there is only a single initial subgoal is a
   140   very common error when implementing tactics!
   141 
   142   Tactics with internal subgoal addressing should expose the subgoal
   143   index as @{text "int"} argument in full generality; a hardwired
   144   subgoal 1 is not acceptable.
   145   
   146   \medskip The main well-formedness conditions for proper tactics are
   147   summarized as follows.
   148 
   149   \begin{itemize}
   150 
   151   \item General tactic failure is indicated by an empty result, only
   152   serious faults may produce an exception.
   153 
   154   \item The main conclusion must not be changed, apart from
   155   instantiating schematic variables.
   156 
   157   \item A tactic operates either uniformly on all subgoals, or
   158   specifically on a selected subgoal (without bumping into unrelated
   159   subgoals).
   160 
   161   \item Range errors in subgoal addressing produce an empty result.
   162 
   163   \end{itemize}
   164 
   165   Some of these conditions are checked by higher-level goal
   166   infrastructure (\secref{sec:struct-goals}); others are not checked
   167   explicitly, and violating them merely results in ill-behaved tactics
   168   experienced by the user (e.g.\ tactics that insist in being
   169   applicable only to singleton goals, or prevent composition via
   170   standard tacticals such as @{ML REPEAT}).
   171 \<close>
   172 
   173 text %mlref \<open>
   174   \begin{mldecls}
   175   @{index_ML_type tactic: "thm -> thm Seq.seq"} \\
   176   @{index_ML no_tac: tactic} \\
   177   @{index_ML all_tac: tactic} \\
   178   @{index_ML print_tac: "Proof.context -> string -> tactic"} \\[1ex]
   179   @{index_ML PRIMITIVE: "(thm -> thm) -> tactic"} \\[1ex]
   180   @{index_ML SUBGOAL: "(term * int -> tactic) -> int -> tactic"} \\
   181   @{index_ML CSUBGOAL: "(cterm * int -> tactic) -> int -> tactic"} \\
   182   @{index_ML SELECT_GOAL: "tactic -> int -> tactic"} \\
   183   @{index_ML PREFER_GOAL: "tactic -> int -> tactic"} \\
   184   \end{mldecls}
   185 
   186   \begin{description}
   187 
   188   \item Type @{ML_type tactic} represents tactics.  The
   189   well-formedness conditions described above need to be observed.  See
   190   also @{file "~~/src/Pure/General/seq.ML"} for the underlying
   191   implementation of lazy sequences.
   192 
   193   \item Type @{ML_type "int -> tactic"} represents tactics with
   194   explicit subgoal addressing, with well-formedness conditions as
   195   described above.
   196 
   197   \item @{ML no_tac} is a tactic that always fails, returning the
   198   empty sequence.
   199 
   200   \item @{ML all_tac} is a tactic that always succeeds, returning a
   201   singleton sequence with unchanged goal state.
   202 
   203   \item @{ML print_tac}~@{text "ctxt message"} is like @{ML all_tac}, but
   204   prints a message together with the goal state on the tracing
   205   channel.
   206 
   207   \item @{ML PRIMITIVE}~@{text rule} turns a primitive inference rule
   208   into a tactic with unique result.  Exception @{ML THM} is considered
   209   a regular tactic failure and produces an empty result; other
   210   exceptions are passed through.
   211 
   212   \item @{ML SUBGOAL}~@{text "(fn (subgoal, i) => tactic)"} is the
   213   most basic form to produce a tactic with subgoal addressing.  The
   214   given abstraction over the subgoal term and subgoal number allows to
   215   peek at the relevant information of the full goal state.  The
   216   subgoal range is checked as required above.
   217 
   218   \item @{ML CSUBGOAL} is similar to @{ML SUBGOAL}, but passes the
   219   subgoal as @{ML_type cterm} instead of raw @{ML_type term}.  This
   220   avoids expensive re-certification in situations where the subgoal is
   221   used directly for primitive inferences.
   222 
   223   \item @{ML SELECT_GOAL}~@{text "tac i"} confines a tactic to the
   224   specified subgoal @{text "i"}.  This rearranges subgoals and the
   225   main goal protection (\secref{sec:tactical-goals}), while retaining
   226   the syntactic context of the overall goal state (concerning
   227   schematic variables etc.).
   228 
   229   \item @{ML PREFER_GOAL}~@{text "tac i"} rearranges subgoals to put
   230   @{text "i"} in front.  This is similar to @{ML SELECT_GOAL}, but
   231   without changing the main goal protection.
   232 
   233   \end{description}
   234 \<close>
   235 
   236 
   237 subsection \<open>Resolution and assumption tactics \label{sec:resolve-assume-tac}\<close>
   238 
   239 text \<open>\emph{Resolution} is the most basic mechanism for refining a
   240   subgoal using a theorem as object-level rule.
   241   \emph{Elim-resolution} is particularly suited for elimination rules:
   242   it resolves with a rule, proves its first premise by assumption, and
   243   finally deletes that assumption from any new subgoals.
   244   \emph{Destruct-resolution} is like elim-resolution, but the given
   245   destruction rules are first turned into canonical elimination
   246   format.  \emph{Forward-resolution} is like destruct-resolution, but
   247   without deleting the selected assumption.  The @{text "r/e/d/f"}
   248   naming convention is maintained for several different kinds of
   249   resolution rules and tactics.
   250 
   251   Assumption tactics close a subgoal by unifying some of its premises
   252   against its conclusion.
   253 
   254   \medskip All the tactics in this section operate on a subgoal
   255   designated by a positive integer.  Other subgoals might be affected
   256   indirectly, due to instantiation of schematic variables.
   257 
   258   There are various sources of non-determinism, the tactic result
   259   sequence enumerates all possibilities of the following choices (if
   260   applicable):
   261 
   262   \begin{enumerate}
   263 
   264   \item selecting one of the rules given as argument to the tactic;
   265 
   266   \item selecting a subgoal premise to eliminate, unifying it against
   267   the first premise of the rule;
   268 
   269   \item unifying the conclusion of the subgoal to the conclusion of
   270   the rule.
   271 
   272   \end{enumerate}
   273 
   274   Recall that higher-order unification may produce multiple results
   275   that are enumerated here.
   276 \<close>
   277 
   278 text %mlref \<open>
   279   \begin{mldecls}
   280   @{index_ML resolve_tac: "thm list -> int -> tactic"} \\
   281   @{index_ML eresolve_tac: "thm list -> int -> tactic"} \\
   282   @{index_ML dresolve_tac: "thm list -> int -> tactic"} \\
   283   @{index_ML forward_tac: "thm list -> int -> tactic"} \\
   284   @{index_ML biresolve_tac: "(bool * thm) list -> int -> tactic"} \\[1ex]
   285   @{index_ML assume_tac: "int -> tactic"} \\
   286   @{index_ML eq_assume_tac: "int -> tactic"} \\[1ex]
   287   @{index_ML match_tac: "Proof.context -> thm list -> int -> tactic"} \\
   288   @{index_ML ematch_tac: "Proof.context -> thm list -> int -> tactic"} \\
   289   @{index_ML dmatch_tac: "Proof.context -> thm list -> int -> tactic"} \\
   290   @{index_ML bimatch_tac: "Proof.context -> (bool * thm) list -> int -> tactic"} \\
   291   \end{mldecls}
   292 
   293   \begin{description}
   294 
   295   \item @{ML resolve_tac}~@{text "thms i"} refines the goal state
   296   using the given theorems, which should normally be introduction
   297   rules.  The tactic resolves a rule's conclusion with subgoal @{text
   298   i}, replacing it by the corresponding versions of the rule's
   299   premises.
   300 
   301   \item @{ML eresolve_tac}~@{text "thms i"} performs elim-resolution
   302   with the given theorems, which are normally be elimination rules.
   303 
   304   Note that @{ML "eresolve_tac [asm_rl]"} is equivalent to @{ML
   305   assume_tac}, which facilitates mixing of assumption steps with
   306   genuine eliminations.
   307 
   308   \item @{ML dresolve_tac}~@{text "thms i"} performs
   309   destruct-resolution with the given theorems, which should normally
   310   be destruction rules.  This replaces an assumption by the result of
   311   applying one of the rules.
   312 
   313   \item @{ML forward_tac} is like @{ML dresolve_tac} except that the
   314   selected assumption is not deleted.  It applies a rule to an
   315   assumption, adding the result as a new assumption.
   316 
   317   \item @{ML biresolve_tac}~@{text "brls i"} refines the proof state
   318   by resolution or elim-resolution on each rule, as indicated by its
   319   flag.  It affects subgoal @{text "i"} of the proof state.
   320 
   321   For each pair @{text "(flag, rule)"}, it applies resolution if the
   322   flag is @{text "false"} and elim-resolution if the flag is @{text
   323   "true"}.  A single tactic call handles a mixture of introduction and
   324   elimination rules, which is useful to organize the search process
   325   systematically in proof tools.
   326 
   327   \item @{ML assume_tac}~@{text i} attempts to solve subgoal @{text i}
   328   by assumption (modulo higher-order unification).
   329 
   330   \item @{ML eq_assume_tac} is similar to @{ML assume_tac}, but checks
   331   only for immediate @{text "\<alpha>"}-convertibility instead of using
   332   unification.  It succeeds (with a unique next state) if one of the
   333   assumptions is equal to the subgoal's conclusion.  Since it does not
   334   instantiate variables, it cannot make other subgoals unprovable.
   335 
   336   \item @{ML match_tac}, @{ML ematch_tac}, @{ML dmatch_tac}, and @{ML
   337   bimatch_tac} are similar to @{ML resolve_tac}, @{ML eresolve_tac},
   338   @{ML dresolve_tac}, and @{ML biresolve_tac}, respectively, but do
   339   not instantiate schematic variables in the goal state.%
   340 \footnote{Strictly speaking, matching means to treat the unknowns in the goal
   341   state as constants, but these tactics merely discard unifiers that would
   342   update the goal state. In rare situations (where the conclusion and 
   343   goal state have flexible terms at the same position), the tactic
   344   will fail even though an acceptable unifier exists.}
   345   These tactics were written for a specific application within the classical reasoner.
   346 
   347   Flexible subgoals are not updated at will, but are left alone.
   348   \end{description}
   349 \<close>
   350 
   351 
   352 subsection \<open>Explicit instantiation within a subgoal context\<close>
   353 
   354 text \<open>The main resolution tactics (\secref{sec:resolve-assume-tac})
   355   use higher-order unification, which works well in many practical
   356   situations despite its daunting theoretical properties.
   357   Nonetheless, there are important problem classes where unguided
   358   higher-order unification is not so useful.  This typically involves
   359   rules like universal elimination, existential introduction, or
   360   equational substitution.  Here the unification problem involves
   361   fully flexible @{text "?P ?x"} schemes, which are hard to manage
   362   without further hints.
   363 
   364   By providing a (small) rigid term for @{text "?x"} explicitly, the
   365   remaining unification problem is to assign a (large) term to @{text
   366   "?P"}, according to the shape of the given subgoal.  This is
   367   sufficiently well-behaved in most practical situations.
   368 
   369   \medskip Isabelle provides separate versions of the standard @{text
   370   "r/e/d/f"} resolution tactics that allow to provide explicit
   371   instantiations of unknowns of the given rule, wrt.\ terms that refer
   372   to the implicit context of the selected subgoal.
   373 
   374   An instantiation consists of a list of pairs of the form @{text
   375   "(?x, t)"}, where @{text ?x} is a schematic variable occurring in
   376   the given rule, and @{text t} is a term from the current proof
   377   context, augmented by the local goal parameters of the selected
   378   subgoal; cf.\ the @{text "focus"} operation described in
   379   \secref{sec:variables}.
   380 
   381   Entering the syntactic context of a subgoal is a brittle operation,
   382   because its exact form is somewhat accidental, and the choice of
   383   bound variable names depends on the presence of other local and
   384   global names.  Explicit renaming of subgoal parameters prior to
   385   explicit instantiation might help to achieve a bit more robustness.
   386 
   387   Type instantiations may be given as well, via pairs like @{text
   388   "(?'a, \<tau>)"}.  Type instantiations are distinguished from term
   389   instantiations by the syntactic form of the schematic variable.
   390   Types are instantiated before terms are.  Since term instantiation
   391   already performs simple type-inference, so explicit type
   392   instantiations are seldom necessary.
   393 \<close>
   394 
   395 text %mlref \<open>
   396   \begin{mldecls}
   397   @{index_ML res_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\
   398   @{index_ML eres_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\
   399   @{index_ML dres_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\
   400   @{index_ML forw_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\
   401   @{index_ML subgoal_tac: "Proof.context -> string -> int -> tactic"} \\
   402   @{index_ML thin_tac: "Proof.context -> string -> int -> tactic"} \\
   403   @{index_ML rename_tac: "string list -> int -> tactic"} \\
   404   \end{mldecls}
   405 
   406   \begin{description}
   407 
   408   \item @{ML res_inst_tac}~@{text "ctxt insts thm i"} instantiates the
   409   rule @{text thm} with the instantiations @{text insts}, as described
   410   above, and then performs resolution on subgoal @{text i}.
   411   
   412   \item @{ML eres_inst_tac} is like @{ML res_inst_tac}, but performs
   413   elim-resolution.
   414 
   415   \item @{ML dres_inst_tac} is like @{ML res_inst_tac}, but performs
   416   destruct-resolution.
   417 
   418   \item @{ML forw_inst_tac} is like @{ML dres_inst_tac} except that
   419   the selected assumption is not deleted.
   420 
   421   \item @{ML subgoal_tac}~@{text "ctxt \<phi> i"} adds the proposition
   422   @{text "\<phi>"} as local premise to subgoal @{text "i"}, and poses the
   423   same as a new subgoal @{text "i + 1"} (in the original context).
   424 
   425   \item @{ML thin_tac}~@{text "ctxt \<phi> i"} deletes the specified
   426   premise from subgoal @{text i}.  Note that @{text \<phi>} may contain
   427   schematic variables, to abbreviate the intended proposition; the
   428   first matching subgoal premise will be deleted.  Removing useless
   429   premises from a subgoal increases its readability and can make
   430   search tactics run faster.
   431 
   432   \item @{ML rename_tac}~@{text "names i"} renames the innermost
   433   parameters of subgoal @{text i} according to the provided @{text
   434   names} (which need to be distinct identifiers).
   435 
   436   \end{description}
   437 
   438   For historical reasons, the above instantiation tactics take
   439   unparsed string arguments, which makes them hard to use in general
   440   ML code.  The slightly more advanced @{ML Subgoal.FOCUS} combinator
   441   of \secref{sec:struct-goals} allows to refer to internal goal
   442   structure with explicit context management.
   443 \<close>
   444 
   445 
   446 subsection \<open>Rearranging goal states\<close>
   447 
   448 text \<open>In rare situations there is a need to rearrange goal states:
   449   either the overall collection of subgoals, or the local structure of
   450   a subgoal.  Various administrative tactics allow to operate on the
   451   concrete presentation these conceptual sets of formulae.\<close>
   452 
   453 text %mlref \<open>
   454   \begin{mldecls}
   455   @{index_ML rotate_tac: "int -> int -> tactic"} \\
   456   @{index_ML distinct_subgoals_tac: tactic} \\
   457   @{index_ML flexflex_tac: "Proof.context -> tactic"} \\
   458   \end{mldecls}
   459 
   460   \begin{description}
   461 
   462   \item @{ML rotate_tac}~@{text "n i"} rotates the premises of subgoal
   463   @{text i} by @{text n} positions: from right to left if @{text n} is
   464   positive, and from left to right if @{text n} is negative.
   465 
   466   \item @{ML distinct_subgoals_tac} removes duplicate subgoals from a
   467   proof state.  This is potentially inefficient.
   468 
   469   \item @{ML flexflex_tac} removes all flex-flex pairs from the proof
   470   state by applying the trivial unifier.  This drastic step loses
   471   information.  It is already part of the Isar infrastructure for
   472   facts resulting from goals, and rarely needs to be invoked manually.
   473 
   474   Flex-flex constraints arise from difficult cases of higher-order
   475   unification.  To prevent this, use @{ML res_inst_tac} to instantiate
   476   some variables in a rule.  Normally flex-flex constraints can be
   477   ignored; they often disappear as unknowns get instantiated.
   478 
   479   \end{description}
   480 \<close>
   481 
   482 
   483 subsection \<open>Raw composition: resolution without lifting\<close>
   484 
   485 text \<open>
   486   Raw composition of two rules means resolving them without prior
   487   lifting or renaming of unknowns.  This low-level operation, which
   488   underlies the resolution tactics, may occasionally be useful for
   489   special effects.  Schematic variables are not renamed by default, so
   490   beware of clashes!
   491 \<close>
   492 
   493 text %mlref \<open>
   494   \begin{mldecls}
   495   @{index_ML compose_tac: "Proof.context -> (bool * thm * int) -> int -> tactic"} \\
   496   @{index_ML Drule.compose: "thm * int * thm -> thm"} \\
   497   @{index_ML_op COMP: "thm * thm -> thm"} \\
   498   \end{mldecls}
   499 
   500   \begin{description}
   501 
   502   \item @{ML compose_tac}~@{text "ctxt (flag, rule, m) i"} refines subgoal
   503   @{text "i"} using @{text "rule"}, without lifting.  The @{text
   504   "rule"} is taken to have the form @{text "\<psi>\<^sub>1 \<Longrightarrow> \<dots> \<psi>\<^sub>m \<Longrightarrow> \<psi>"}, where
   505   @{text "\<psi>"} need not be atomic; thus @{text "m"} determines the
   506   number of new subgoals.  If @{text "flag"} is @{text "true"} then it
   507   performs elim-resolution --- it solves the first premise of @{text
   508   "rule"} by assumption and deletes that assumption.
   509 
   510   \item @{ML Drule.compose}~@{text "(thm\<^sub>1, i, thm\<^sub>2)"} uses @{text "thm\<^sub>1"},
   511   regarded as an atomic formula, to solve premise @{text "i"} of
   512   @{text "thm\<^sub>2"}.  Let @{text "thm\<^sub>1"} and @{text "thm\<^sub>2"} be @{text
   513   "\<psi>"} and @{text "\<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> \<phi>"}.  The unique @{text "s"} that
   514   unifies @{text "\<psi>"} and @{text "\<phi>\<^sub>i"} yields the theorem @{text "(\<phi>\<^sub>1 \<Longrightarrow>
   515   \<dots> \<phi>\<^sub>i\<^sub>-\<^sub>1 \<Longrightarrow> \<phi>\<^sub>i\<^sub>+\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> \<phi>)s"}.  Multiple results are considered as
   516   error (exception @{ML THM}).
   517 
   518   \item @{text "thm\<^sub>1 COMP thm\<^sub>2"} is the same as @{text "Drule.compose
   519   (thm\<^sub>1, 1, thm\<^sub>2)"}.
   520 
   521   \end{description}
   522 
   523   \begin{warn}
   524   These low-level operations are stepping outside the structure
   525   imposed by regular rule resolution.  Used without understanding of
   526   the consequences, they may produce results that cause problems with
   527   standard rules and tactics later on.
   528   \end{warn}
   529 \<close>
   530 
   531 
   532 section \<open>Tacticals \label{sec:tacticals}\<close>
   533 
   534 text \<open>A \emph{tactical} is a functional combinator for building up
   535   complex tactics from simpler ones.  Common tacticals perform
   536   sequential composition, disjunctive choice, iteration, or goal
   537   addressing.  Various search strategies may be expressed via
   538   tacticals.
   539 \<close>
   540 
   541 
   542 subsection \<open>Combining tactics\<close>
   543 
   544 text \<open>Sequential composition and alternative choices are the most
   545   basic ways to combine tactics, similarly to ``@{verbatim ","}'' and
   546   ``@{verbatim "|"}'' in Isar method notation.  This corresponds to
   547   @{ML_op "THEN"} and @{ML_op "ORELSE"} in ML, but there are further
   548   possibilities for fine-tuning alternation of tactics such as @{ML_op
   549   "APPEND"}.  Further details become visible in ML due to explicit
   550   subgoal addressing.
   551 \<close>
   552 
   553 text %mlref \<open>
   554   \begin{mldecls}
   555   @{index_ML_op "THEN": "tactic * tactic -> tactic"} \\
   556   @{index_ML_op "ORELSE": "tactic * tactic -> tactic"} \\
   557   @{index_ML_op "APPEND": "tactic * tactic -> tactic"} \\
   558   @{index_ML "EVERY": "tactic list -> tactic"} \\
   559   @{index_ML "FIRST": "tactic list -> tactic"} \\[0.5ex]
   560 
   561   @{index_ML_op "THEN'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\
   562   @{index_ML_op "ORELSE'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\
   563   @{index_ML_op "APPEND'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\
   564   @{index_ML "EVERY'": "('a -> tactic) list -> 'a -> tactic"} \\
   565   @{index_ML "FIRST'": "('a -> tactic) list -> 'a -> tactic"} \\
   566   \end{mldecls}
   567 
   568   \begin{description}
   569 
   570   \item @{text "tac\<^sub>1"}~@{ML_op THEN}~@{text "tac\<^sub>2"} is the sequential
   571   composition of @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"}.  Applied to a goal
   572   state, it returns all states reachable in two steps by applying
   573   @{text "tac\<^sub>1"} followed by @{text "tac\<^sub>2"}.  First, it applies @{text
   574   "tac\<^sub>1"} to the goal state, getting a sequence of possible next
   575   states; then, it applies @{text "tac\<^sub>2"} to each of these and
   576   concatenates the results to produce again one flat sequence of
   577   states.
   578 
   579   \item @{text "tac\<^sub>1"}~@{ML_op ORELSE}~@{text "tac\<^sub>2"} makes a choice
   580   between @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"}.  Applied to a state, it
   581   tries @{text "tac\<^sub>1"} and returns the result if non-empty; if @{text
   582   "tac\<^sub>1"} fails then it uses @{text "tac\<^sub>2"}.  This is a deterministic
   583   choice: if @{text "tac\<^sub>1"} succeeds then @{text "tac\<^sub>2"} is excluded
   584   from the result.
   585 
   586   \item @{text "tac\<^sub>1"}~@{ML_op APPEND}~@{text "tac\<^sub>2"} concatenates the
   587   possible results of @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"}.  Unlike
   588   @{ML_op "ORELSE"} there is \emph{no commitment} to either tactic, so
   589   @{ML_op "APPEND"} helps to avoid incompleteness during search, at
   590   the cost of potential inefficiencies.
   591 
   592   \item @{ML EVERY}~@{text "[tac\<^sub>1, \<dots>, tac\<^sub>n]"} abbreviates @{text
   593   "tac\<^sub>1"}~@{ML_op THEN}~@{text "\<dots>"}~@{ML_op THEN}~@{text "tac\<^sub>n"}.
   594   Note that @{ML "EVERY []"} is the same as @{ML all_tac}: it always
   595   succeeds.
   596 
   597   \item @{ML FIRST}~@{text "[tac\<^sub>1, \<dots>, tac\<^sub>n]"} abbreviates @{text
   598   "tac\<^sub>1"}~@{ML_op ORELSE}~@{text "\<dots>"}~@{ML_op "ORELSE"}~@{text
   599   "tac\<^sub>n"}.  Note that @{ML "FIRST []"} is the same as @{ML no_tac}: it
   600   always fails.
   601 
   602   \item @{ML_op "THEN'"} is the lifted version of @{ML_op "THEN"}, for
   603   tactics with explicit subgoal addressing.  So @{text
   604   "(tac\<^sub>1"}~@{ML_op THEN'}~@{text "tac\<^sub>2) i"} is the same as @{text
   605   "(tac\<^sub>1 i"}~@{ML_op THEN}~@{text "tac\<^sub>2 i)"}.
   606 
   607   The other primed tacticals work analogously.
   608 
   609   \end{description}
   610 \<close>
   611 
   612 
   613 subsection \<open>Repetition tacticals\<close>
   614 
   615 text \<open>These tacticals provide further control over repetition of
   616   tactics, beyond the stylized forms of ``@{verbatim "?"}''  and
   617   ``@{verbatim "+"}'' in Isar method expressions.\<close>
   618 
   619 text %mlref \<open>
   620   \begin{mldecls}
   621   @{index_ML "TRY": "tactic -> tactic"} \\
   622   @{index_ML "REPEAT": "tactic -> tactic"} \\
   623   @{index_ML "REPEAT1": "tactic -> tactic"} \\
   624   @{index_ML "REPEAT_DETERM": "tactic -> tactic"} \\
   625   @{index_ML "REPEAT_DETERM_N": "int -> tactic -> tactic"} \\
   626   \end{mldecls}
   627 
   628   \begin{description}
   629 
   630   \item @{ML TRY}~@{text "tac"} applies @{text "tac"} to the goal
   631   state and returns the resulting sequence, if non-empty; otherwise it
   632   returns the original state.  Thus, it applies @{text "tac"} at most
   633   once.
   634 
   635   Note that for tactics with subgoal addressing, the combinator can be
   636   applied via functional composition: @{ML "TRY"}~@{ML_op o}~@{text
   637   "tac"}.  There is no need for @{verbatim TRY'}.
   638 
   639   \item @{ML REPEAT}~@{text "tac"} applies @{text "tac"} to the goal
   640   state and, recursively, to each element of the resulting sequence.
   641   The resulting sequence consists of those states that make @{text
   642   "tac"} fail.  Thus, it applies @{text "tac"} as many times as
   643   possible (including zero times), and allows backtracking over each
   644   invocation of @{text "tac"}.  @{ML REPEAT} is more general than @{ML
   645   REPEAT_DETERM}, but requires more space.
   646 
   647   \item @{ML REPEAT1}~@{text "tac"} is like @{ML REPEAT}~@{text "tac"}
   648   but it always applies @{text "tac"} at least once, failing if this
   649   is impossible.
   650 
   651   \item @{ML REPEAT_DETERM}~@{text "tac"} applies @{text "tac"} to the
   652   goal state and, recursively, to the head of the resulting sequence.
   653   It returns the first state to make @{text "tac"} fail.  It is
   654   deterministic, discarding alternative outcomes.
   655 
   656   \item @{ML REPEAT_DETERM_N}~@{text "n tac"} is like @{ML
   657   REPEAT_DETERM}~@{text "tac"} but the number of repetitions is bound
   658   by @{text "n"} (where @{ML "~1"} means @{text "\<infinity>"}).
   659 
   660   \end{description}
   661 \<close>
   662 
   663 text %mlex \<open>The basic tactics and tacticals considered above follow
   664   some algebraic laws:
   665 
   666   \begin{itemize}
   667 
   668   \item @{ML all_tac} is the identity element of the tactical @{ML_op
   669   "THEN"}.
   670 
   671   \item @{ML no_tac} is the identity element of @{ML_op "ORELSE"} and
   672   @{ML_op "APPEND"}.  Also, it is a zero element for @{ML_op "THEN"},
   673   which means that @{text "tac"}~@{ML_op THEN}~@{ML no_tac} is
   674   equivalent to @{ML no_tac}.
   675 
   676   \item @{ML TRY} and @{ML REPEAT} can be expressed as (recursive)
   677   functions over more basic combinators (ignoring some internal
   678   implementation tricks):
   679 
   680   \end{itemize}
   681 \<close>
   682 
   683 ML \<open>
   684   fun TRY tac = tac ORELSE all_tac;
   685   fun REPEAT tac st = ((tac THEN REPEAT tac) ORELSE all_tac) st;
   686 \<close>
   687 
   688 text \<open>If @{text "tac"} can return multiple outcomes then so can @{ML
   689   REPEAT}~@{text "tac"}.  @{ML REPEAT} uses @{ML_op "ORELSE"} and not
   690   @{ML_op "APPEND"}, it applies @{text "tac"} as many times as
   691   possible in each outcome.
   692 
   693   \begin{warn}
   694   Note the explicit abstraction over the goal state in the ML
   695   definition of @{ML REPEAT}.  Recursive tacticals must be coded in
   696   this awkward fashion to avoid infinite recursion of eager functional
   697   evaluation in Standard ML.  The following attempt would make @{ML
   698   REPEAT}~@{text "tac"} loop:
   699   \end{warn}
   700 \<close>
   701 
   702 ML \<open>
   703   (*BAD -- does not terminate!*)
   704   fun REPEAT tac = (tac THEN REPEAT tac) ORELSE all_tac;
   705 \<close>
   706 
   707 
   708 subsection \<open>Applying tactics to subgoal ranges\<close>
   709 
   710 text \<open>Tactics with explicit subgoal addressing
   711   @{ML_type "int -> tactic"} can be used together with tacticals that
   712   act like ``subgoal quantifiers'': guided by success of the body
   713   tactic a certain range of subgoals is covered.  Thus the body tactic
   714   is applied to \emph{all} subgoals, \emph{some} subgoal etc.
   715 
   716   Suppose that the goal state has @{text "n \<ge> 0"} subgoals.  Many of
   717   these tacticals address subgoal ranges counting downwards from
   718   @{text "n"} towards @{text "1"}.  This has the fortunate effect that
   719   newly emerging subgoals are concatenated in the result, without
   720   interfering each other.  Nonetheless, there might be situations
   721   where a different order is desired.\<close>
   722 
   723 text %mlref \<open>
   724   \begin{mldecls}
   725   @{index_ML ALLGOALS: "(int -> tactic) -> tactic"} \\
   726   @{index_ML SOMEGOAL: "(int -> tactic) -> tactic"} \\
   727   @{index_ML FIRSTGOAL: "(int -> tactic) -> tactic"} \\
   728   @{index_ML HEADGOAL: "(int -> tactic) -> tactic"} \\
   729   @{index_ML REPEAT_SOME: "(int -> tactic) -> tactic"} \\
   730   @{index_ML REPEAT_FIRST: "(int -> tactic) -> tactic"} \\
   731   @{index_ML RANGE: "(int -> tactic) list -> int -> tactic"} \\
   732   \end{mldecls}
   733 
   734   \begin{description}
   735 
   736   \item @{ML ALLGOALS}~@{text "tac"} is equivalent to @{text "tac
   737   n"}~@{ML_op THEN}~@{text "\<dots>"}~@{ML_op THEN}~@{text "tac 1"}.  It
   738   applies the @{text tac} to all the subgoals, counting downwards.
   739 
   740   \item @{ML SOMEGOAL}~@{text "tac"} is equivalent to @{text "tac
   741   n"}~@{ML_op ORELSE}~@{text "\<dots>"}~@{ML_op ORELSE}~@{text "tac 1"}.  It
   742   applies @{text "tac"} to one subgoal, counting downwards.
   743 
   744   \item @{ML FIRSTGOAL}~@{text "tac"} is equivalent to @{text "tac
   745   1"}~@{ML_op ORELSE}~@{text "\<dots>"}~@{ML_op ORELSE}~@{text "tac n"}.  It
   746   applies @{text "tac"} to one subgoal, counting upwards.
   747 
   748   \item @{ML HEADGOAL}~@{text "tac"} is equivalent to @{text "tac 1"}.
   749   It applies @{text "tac"} unconditionally to the first subgoal.
   750 
   751   \item @{ML REPEAT_SOME}~@{text "tac"} applies @{text "tac"} once or
   752   more to a subgoal, counting downwards.
   753 
   754   \item @{ML REPEAT_FIRST}~@{text "tac"} applies @{text "tac"} once or
   755   more to a subgoal, counting upwards.
   756 
   757   \item @{ML RANGE}~@{text "[tac\<^sub>1, \<dots>, tac\<^sub>k] i"} is equivalent to
   758   @{text "tac\<^sub>k (i + k - 1)"}~@{ML_op THEN}~@{text "\<dots>"}~@{ML_op
   759   THEN}~@{text "tac\<^sub>1 i"}.  It applies the given list of tactics to the
   760   corresponding range of subgoals, counting downwards.
   761 
   762   \end{description}
   763 \<close>
   764 
   765 
   766 subsection \<open>Control and search tacticals\<close>
   767 
   768 text \<open>A predicate on theorems @{ML_type "thm -> bool"} can test
   769   whether a goal state enjoys some desirable property --- such as
   770   having no subgoals.  Tactics that search for satisfactory goal
   771   states are easy to express.  The main search procedures,
   772   depth-first, breadth-first and best-first, are provided as
   773   tacticals.  They generate the search tree by repeatedly applying a
   774   given tactic.\<close>
   775 
   776 
   777 text %mlref ""
   778 
   779 subsubsection \<open>Filtering a tactic's results\<close>
   780 
   781 text \<open>
   782   \begin{mldecls}
   783   @{index_ML FILTER: "(thm -> bool) -> tactic -> tactic"} \\
   784   @{index_ML CHANGED: "tactic -> tactic"} \\
   785   \end{mldecls}
   786 
   787   \begin{description}
   788 
   789   \item @{ML FILTER}~@{text "sat tac"} applies @{text "tac"} to the
   790   goal state and returns a sequence consisting of those result goal
   791   states that are satisfactory in the sense of @{text "sat"}.
   792 
   793   \item @{ML CHANGED}~@{text "tac"} applies @{text "tac"} to the goal
   794   state and returns precisely those states that differ from the
   795   original state (according to @{ML Thm.eq_thm}).  Thus @{ML
   796   CHANGED}~@{text "tac"} always has some effect on the state.
   797 
   798   \end{description}
   799 \<close>
   800 
   801 
   802 subsubsection \<open>Depth-first search\<close>
   803 
   804 text \<open>
   805   \begin{mldecls}
   806   @{index_ML DEPTH_FIRST: "(thm -> bool) -> tactic -> tactic"} \\
   807   @{index_ML DEPTH_SOLVE: "tactic -> tactic"} \\
   808   @{index_ML DEPTH_SOLVE_1: "tactic -> tactic"} \\
   809   \end{mldecls}
   810 
   811   \begin{description}
   812 
   813   \item @{ML DEPTH_FIRST}~@{text "sat tac"} returns the goal state if
   814   @{text "sat"} returns true.  Otherwise it applies @{text "tac"},
   815   then recursively searches from each element of the resulting
   816   sequence.  The code uses a stack for efficiency, in effect applying
   817   @{text "tac"}~@{ML_op THEN}~@{ML DEPTH_FIRST}~@{text "sat tac"} to
   818   the state.
   819 
   820   \item @{ML DEPTH_SOLVE}@{text "tac"} uses @{ML DEPTH_FIRST} to
   821   search for states having no subgoals.
   822 
   823   \item @{ML DEPTH_SOLVE_1}~@{text "tac"} uses @{ML DEPTH_FIRST} to
   824   search for states having fewer subgoals than the given state.  Thus,
   825   it insists upon solving at least one subgoal.
   826 
   827   \end{description}
   828 \<close>
   829 
   830 
   831 subsubsection \<open>Other search strategies\<close>
   832 
   833 text \<open>
   834   \begin{mldecls}
   835   @{index_ML BREADTH_FIRST: "(thm -> bool) -> tactic -> tactic"} \\
   836   @{index_ML BEST_FIRST: "(thm -> bool) * (thm -> int) -> tactic -> tactic"} \\
   837   @{index_ML THEN_BEST_FIRST: "tactic -> (thm -> bool) * (thm -> int) -> tactic -> tactic"} \\
   838   \end{mldecls}
   839 
   840   These search strategies will find a solution if one exists.
   841   However, they do not enumerate all solutions; they terminate after
   842   the first satisfactory result from @{text "tac"}.
   843 
   844   \begin{description}
   845 
   846   \item @{ML BREADTH_FIRST}~@{text "sat tac"} uses breadth-first
   847   search to find states for which @{text "sat"} is true.  For most
   848   applications, it is too slow.
   849 
   850   \item @{ML BEST_FIRST}~@{text "(sat, dist) tac"} does a heuristic
   851   search, using @{text "dist"} to estimate the distance from a
   852   satisfactory state (in the sense of @{text "sat"}).  It maintains a
   853   list of states ordered by distance.  It applies @{text "tac"} to the
   854   head of this list; if the result contains any satisfactory states,
   855   then it returns them.  Otherwise, @{ML BEST_FIRST} adds the new
   856   states to the list, and continues.
   857 
   858   The distance function is typically @{ML size_of_thm}, which computes
   859   the size of the state.  The smaller the state, the fewer and simpler
   860   subgoals it has.
   861 
   862   \item @{ML THEN_BEST_FIRST}~@{text "tac\<^sub>0 (sat, dist) tac"} is like
   863   @{ML BEST_FIRST}, except that the priority queue initially contains
   864   the result of applying @{text "tac\<^sub>0"} to the goal state.  This
   865   tactical permits separate tactics for starting the search and
   866   continuing the search.
   867 
   868   \end{description}
   869 \<close>
   870 
   871 
   872 subsubsection \<open>Auxiliary tacticals for searching\<close>
   873 
   874 text \<open>
   875   \begin{mldecls}
   876   @{index_ML COND: "(thm -> bool) -> tactic -> tactic -> tactic"} \\
   877   @{index_ML IF_UNSOLVED: "tactic -> tactic"} \\
   878   @{index_ML SOLVE: "tactic -> tactic"} \\
   879   @{index_ML DETERM: "tactic -> tactic"} \\
   880   \end{mldecls}
   881 
   882   \begin{description}
   883 
   884   \item @{ML COND}~@{text "sat tac\<^sub>1 tac\<^sub>2"} applies @{text "tac\<^sub>1"} to
   885   the goal state if it satisfies predicate @{text "sat"}, and applies
   886   @{text "tac\<^sub>2"}.  It is a conditional tactical in that only one of
   887   @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"} is applied to a goal state.
   888   However, both @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"} are evaluated
   889   because ML uses eager evaluation.
   890 
   891   \item @{ML IF_UNSOLVED}~@{text "tac"} applies @{text "tac"} to the
   892   goal state if it has any subgoals, and simply returns the goal state
   893   otherwise.  Many common tactics, such as @{ML resolve_tac}, fail if
   894   applied to a goal state that has no subgoals.
   895 
   896   \item @{ML SOLVE}~@{text "tac"} applies @{text "tac"} to the goal
   897   state and then fails iff there are subgoals left.
   898 
   899   \item @{ML DETERM}~@{text "tac"} applies @{text "tac"} to the goal
   900   state and returns the head of the resulting sequence.  @{ML DETERM}
   901   limits the search space by making its argument deterministic.
   902 
   903   \end{description}
   904 \<close>
   905 
   906 
   907 subsubsection \<open>Predicates and functions useful for searching\<close>
   908 
   909 text \<open>
   910   \begin{mldecls}
   911   @{index_ML has_fewer_prems: "int -> thm -> bool"} \\
   912   @{index_ML Thm.eq_thm: "thm * thm -> bool"} \\
   913   @{index_ML Thm.eq_thm_prop: "thm * thm -> bool"} \\
   914   @{index_ML size_of_thm: "thm -> int"} \\
   915   \end{mldecls}
   916 
   917   \begin{description}
   918 
   919   \item @{ML has_fewer_prems}~@{text "n thm"} reports whether @{text
   920   "thm"} has fewer than @{text "n"} premises.
   921 
   922   \item @{ML Thm.eq_thm}~@{text "(thm\<^sub>1, thm\<^sub>2)"} reports whether @{text
   923   "thm\<^sub>1"} and @{text "thm\<^sub>2"} are equal.  Both theorems must have the
   924   same conclusions, the same set of hypotheses, and the same set of sort
   925   hypotheses.  Names of bound variables are ignored as usual.
   926 
   927   \item @{ML Thm.eq_thm_prop}~@{text "(thm\<^sub>1, thm\<^sub>2)"} reports whether
   928   the propositions of @{text "thm\<^sub>1"} and @{text "thm\<^sub>2"} are equal.
   929   Names of bound variables are ignored.
   930 
   931   \item @{ML size_of_thm}~@{text "thm"} computes the size of @{text
   932   "thm"}, namely the number of variables, constants and abstractions
   933   in its conclusion.  It may serve as a distance function for
   934   @{ML BEST_FIRST}.
   935 
   936   \end{description}
   937 \<close>
   938 
   939 end