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
     5 chapter \<open>Tactical reasoning\<close>
     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>
    16 section \<open>Goals \label{sec:tactical-goals}\<close>
    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''.
    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.
    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.
    44   \medskip Basic goal management is performed via the following
    45   Isabelle/Pure rules:
    47   \[
    48   \infer[@{text "(init)"}]{@{text "C \<Longrightarrow> #C"}}{} \qquad
    49   \infer[@{text "(finish)"}]{@{text "C"}}{@{text "#C"}}
    50   \]
    52   \medskip The following low-level variants admit general reasoning
    53   with protected propositions:
    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>
    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}
    71   \begin{description}
    73   \item @{ML "Goal.init"}~@{text C} initializes a tactical goal from
    74   the well-formed proposition @{text C}.
    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.
    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.
    85   \item @{ML "Goal.conclude"}~@{text "thm"} removes the goal
    86   protection, even if there are pending subgoals.
    88   \end{description}
    89 \<close>
    92 section \<open>Tactics\label{sec:tactics}\<close>
    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.}
   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.
   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}.
   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).
   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!
   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.
   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!
   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.
   146   \medskip The main well-formedness conditions for proper tactics are
   147   summarized as follows.
   149   \begin{itemize}
   151   \item General tactic failure is indicated by an empty result, only
   152   serious faults may produce an exception.
   154   \item The main conclusion must not be changed, apart from
   155   instantiating schematic variables.
   157   \item A tactic operates either uniformly on all subgoals, or
   158   specifically on a selected subgoal (without bumping into unrelated
   159   subgoals).
   161   \item Range errors in subgoal addressing produce an empty result.
   163   \end{itemize}
   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>
   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}
   186   \begin{description}
   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.
   193   \item Type @{ML_type "int -> tactic"} represents tactics with
   194   explicit subgoal addressing, with well-formedness conditions as
   195   described above.
   197   \item @{ML no_tac} is a tactic that always fails, returning the
   198   empty sequence.
   200   \item @{ML all_tac} is a tactic that always succeeds, returning a
   201   singleton sequence with unchanged goal state.
   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.
   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.
   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.
   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.
   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.).
   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.
   233   \end{description}
   234 \<close>
   237 subsection \<open>Resolution and assumption tactics \label{sec:resolve-assume-tac}\<close>
   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.
   251   Assumption tactics close a subgoal by unifying some of its premises
   252   against its conclusion.
   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.
   258   There are various sources of non-determinism, the tactic result
   259   sequence enumerates all possibilities of the following choices (if
   260   applicable):
   262   \begin{enumerate}
   264   \item selecting one of the rules given as argument to the tactic;
   266   \item selecting a subgoal premise to eliminate, unifying it against
   267   the first premise of the rule;
   269   \item unifying the conclusion of the subgoal to the conclusion of
   270   the rule.
   272   \end{enumerate}
   274   Recall that higher-order unification may produce multiple results
   275   that are enumerated here.
   276 \<close>
   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}
   293   \begin{description}
   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.
   301   \item @{ML eresolve_tac}~@{text "thms i"} performs elim-resolution
   302   with the given theorems, which are normally be elimination rules.
   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.
   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.
   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.
   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.
   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.
   327   \item @{ML assume_tac}~@{text i} attempts to solve subgoal @{text i}
   328   by assumption (modulo higher-order unification).
   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.
   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.
   347   Flexible subgoals are not updated at will, but are left alone.
   348   \end{description}
   349 \<close>
   352 subsection \<open>Explicit instantiation within a subgoal context\<close>
   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.
   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.
   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.
   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}.
   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.
   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>
   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}
   406   \begin{description}
   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}.
   412   \item @{ML eres_inst_tac} is like @{ML res_inst_tac}, but performs
   413   elim-resolution.
   415   \item @{ML dres_inst_tac} is like @{ML res_inst_tac}, but performs
   416   destruct-resolution.
   418   \item @{ML forw_inst_tac} is like @{ML dres_inst_tac} except that
   419   the selected assumption is not deleted.
   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).
   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.
   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).
   436   \end{description}
   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>
   446 subsection \<open>Rearranging goal states\<close>
   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>
   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}
   460   \begin{description}
   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.
   466   \item @{ML distinct_subgoals_tac} removes duplicate subgoals from a
   467   proof state.  This is potentially inefficient.
   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.
   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.
   479   \end{description}
   480 \<close>
   483 subsection \<open>Raw composition: resolution without lifting\<close>
   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>
   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}
   500   \begin{description}
   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.
   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}).
   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)"}.
   521   \end{description}
   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>
   532 section \<open>Tacticals \label{sec:tacticals}\<close>
   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>
   542 subsection \<open>Combining tactics\<close>
   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>
   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]
   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}
   568   \begin{description}
   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.
   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.
   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.
   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.
   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.
   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)"}.
   607   The other primed tacticals work analogously.
   609   \end{description}
   610 \<close>
   613 subsection \<open>Repetition tacticals\<close>
   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>
   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}
   628   \begin{description}
   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.
   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'}.
   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.
   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.
   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.
   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>"}).
   660   \end{description}
   661 \<close>
   663 text %mlex \<open>The basic tactics and tacticals considered above follow
   664   some algebraic laws:
   666   \begin{itemize}
   668   \item @{ML all_tac} is the identity element of the tactical @{ML_op
   669   "THEN"}.
   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}.
   676   \item @{ML TRY} and @{ML REPEAT} can be expressed as (recursive)
   677   functions over more basic combinators (ignoring some internal
   678   implementation tricks):
   680   \end{itemize}
   681 \<close>
   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>
   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.
   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>
   702 ML \<open>
   703   (*BAD -- does not terminate!*)
   704   fun REPEAT tac = (tac THEN REPEAT tac) ORELSE all_tac;
   705 \<close>
   708 subsection \<open>Applying tactics to subgoal ranges\<close>
   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.
   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>
   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}
   734   \begin{description}
   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.
   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.
   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.
   748   \item @{ML HEADGOAL}~@{text "tac"} is equivalent to @{text "tac 1"}.
   749   It applies @{text "tac"} unconditionally to the first subgoal.
   751   \item @{ML REPEAT_SOME}~@{text "tac"} applies @{text "tac"} once or
   752   more to a subgoal, counting downwards.
   754   \item @{ML REPEAT_FIRST}~@{text "tac"} applies @{text "tac"} once or
   755   more to a subgoal, counting upwards.
   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.
   762   \end{description}
   763 \<close>
   766 subsection \<open>Control and search tacticals\<close>
   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>
   777 text %mlref ""
   779 subsubsection \<open>Filtering a tactic's results\<close>
   781 text \<open>
   782   \begin{mldecls}
   783   @{index_ML FILTER: "(thm -> bool) -> tactic -> tactic"} \\
   784   @{index_ML CHANGED: "tactic -> tactic"} \\
   785   \end{mldecls}
   787   \begin{description}
   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"}.
   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.
   798   \end{description}
   799 \<close>
   802 subsubsection \<open>Depth-first search\<close>
   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}
   811   \begin{description}
   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.
   820   \item @{ML DEPTH_SOLVE}@{text "tac"} uses @{ML DEPTH_FIRST} to
   821   search for states having no subgoals.
   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.
   827   \end{description}
   828 \<close>
   831 subsubsection \<open>Other search strategies\<close>
   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}
   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"}.
   844   \begin{description}
   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.
   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.
   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.
   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.
   868   \end{description}
   869 \<close>
   872 subsubsection \<open>Auxiliary tacticals for searching\<close>
   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}
   882   \begin{description}
   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.
   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.
   896   \item @{ML SOLVE}~@{text "tac"} applies @{text "tac"} to the goal
   897   state and then fails iff there are subgoals left.
   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.
   903   \end{description}
   904 \<close>
   907 subsubsection \<open>Predicates and functions useful for searching\<close>
   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}
   917   \begin{description}
   919   \item @{ML has_fewer_prems}~@{text "n thm"} reports whether @{text
   920   "thm"} has fewer than @{text "n"} premises.
   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.
   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.
   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}.
   936   \end{description}
   937 \<close>
   939 end