doc-src/IsarImplementation/Thy/Tactic.thy
author wenzelm
Fri Aug 12 22:10:49 2011 +0200 (2011-08-12)
changeset 44163 32e0c150c010
parent 40800 330eb65c9469
child 46258 89ee3bc580a8
permissions -rw-r--r--
normalized theory dependencies wrt. file_store;
     1 theory Tactic
     2 imports Base
     3 begin
     4 
     5 chapter {* Tactical reasoning *}
     6 
     7 text {* 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.  *}
    14 
    15 
    16 section {* Goals \label{sec:tactical-goals} *}
    17 
    18 text {*
    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)"}]{@{text "#C"}}{@{text "C"}} \qquad
    57   \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"}}
    58   \]
    59 *}
    60 
    61 text %mlref {*
    62   \begin{mldecls}
    63   @{index_ML Goal.init: "cterm -> thm"} \\
    64   @{index_ML Goal.finish: "Proof.context -> thm -> thm"} \\
    65   @{index_ML Goal.protect: "thm -> thm"} \\
    66   @{index_ML Goal.conclude: "thm -> thm"} \\
    67   \end{mldecls}
    68 
    69   \begin{description}
    70 
    71   \item @{ML "Goal.init"}~@{text C} initializes a tactical goal from
    72   the well-formed proposition @{text C}.
    73 
    74   \item @{ML "Goal.finish"}~@{text "ctxt thm"} checks whether theorem
    75   @{text "thm"} is a solved goal (no subgoals), and concludes the
    76   result by removing the goal protection.  The context is only
    77   required for printing error messages.
    78 
    79   \item @{ML "Goal.protect"}~@{text "thm"} protects the full statement
    80   of theorem @{text "thm"}.
    81 
    82   \item @{ML "Goal.conclude"}~@{text "thm"} removes the goal
    83   protection, even if there are pending subgoals.
    84 
    85   \end{description}
    86 *}
    87 
    88 
    89 section {* Tactics\label{sec:tactics} *}
    90 
    91 text {* A @{text "tactic"} is a function @{text "goal \<rightarrow> goal\<^sup>*\<^sup>*"} that
    92   maps a given goal state (represented as a theorem, cf.\
    93   \secref{sec:tactical-goals}) to a lazy sequence of potential
    94   successor states.  The underlying sequence implementation is lazy
    95   both in head and tail, and is purely functional in \emph{not}
    96   supporting memoing.\footnote{The lack of memoing and the strict
    97   nature of SML requires some care when working with low-level
    98   sequence operations, to avoid duplicate or premature evaluation of
    99   results.  It also means that modified runtime behavior, such as
   100   timeout, is very hard to achieve for general tactics.}
   101 
   102   An \emph{empty result sequence} means that the tactic has failed: in
   103   a compound tactic expression other tactics might be tried instead,
   104   or the whole refinement step might fail outright, producing a
   105   toplevel error message in the end.  When implementing tactics from
   106   scratch, one should take care to observe the basic protocol of
   107   mapping regular error conditions to an empty result; only serious
   108   faults should emerge as exceptions.
   109 
   110   By enumerating \emph{multiple results}, a tactic can easily express
   111   the potential outcome of an internal search process.  There are also
   112   combinators for building proof tools that involve search
   113   systematically, see also \secref{sec:tacticals}.
   114 
   115   \medskip As explained before, a goal state essentially consists of a
   116   list of subgoals that imply the main goal (conclusion).  Tactics may
   117   operate on all subgoals or on a particularly specified subgoal, but
   118   must not change the main conclusion (apart from instantiating
   119   schematic goal variables).
   120 
   121   Tactics with explicit \emph{subgoal addressing} are of the form
   122   @{text "int \<rightarrow> tactic"} and may be applied to a particular subgoal
   123   (counting from 1).  If the subgoal number is out of range, the
   124   tactic should fail with an empty result sequence, but must not raise
   125   an exception!
   126 
   127   Operating on a particular subgoal means to replace it by an interval
   128   of zero or more subgoals in the same place; other subgoals must not
   129   be affected, apart from instantiating schematic variables ranging
   130   over the whole goal state.
   131 
   132   A common pattern of composing tactics with subgoal addressing is to
   133   try the first one, and then the second one only if the subgoal has
   134   not been solved yet.  Special care is required here to avoid bumping
   135   into unrelated subgoals that happen to come after the original
   136   subgoal.  Assuming that there is only a single initial subgoal is a
   137   very common error when implementing tactics!
   138 
   139   Tactics with internal subgoal addressing should expose the subgoal
   140   index as @{text "int"} argument in full generality; a hardwired
   141   subgoal 1 is not acceptable.
   142   
   143   \medskip The main well-formedness conditions for proper tactics are
   144   summarized as follows.
   145 
   146   \begin{itemize}
   147 
   148   \item General tactic failure is indicated by an empty result, only
   149   serious faults may produce an exception.
   150 
   151   \item The main conclusion must not be changed, apart from
   152   instantiating schematic variables.
   153 
   154   \item A tactic operates either uniformly on all subgoals, or
   155   specifically on a selected subgoal (without bumping into unrelated
   156   subgoals).
   157 
   158   \item Range errors in subgoal addressing produce an empty result.
   159 
   160   \end{itemize}
   161 
   162   Some of these conditions are checked by higher-level goal
   163   infrastructure (\secref{sec:struct-goals}); others are not checked
   164   explicitly, and violating them merely results in ill-behaved tactics
   165   experienced by the user (e.g.\ tactics that insist in being
   166   applicable only to singleton goals, or prevent composition via
   167   standard tacticals).
   168 *}
   169 
   170 text %mlref {*
   171   \begin{mldecls}
   172   @{index_ML_type tactic: "thm -> thm Seq.seq"} \\
   173   @{index_ML no_tac: tactic} \\
   174   @{index_ML all_tac: tactic} \\
   175   @{index_ML print_tac: "string -> tactic"} \\[1ex]
   176   @{index_ML PRIMITIVE: "(thm -> thm) -> tactic"} \\[1ex]
   177   @{index_ML SUBGOAL: "(term * int -> tactic) -> int -> tactic"} \\
   178   @{index_ML CSUBGOAL: "(cterm * int -> tactic) -> int -> tactic"} \\
   179   \end{mldecls}
   180 
   181   \begin{description}
   182 
   183   \item Type @{ML_type tactic} represents tactics.  The
   184   well-formedness conditions described above need to be observed.  See
   185   also @{file "~~/src/Pure/General/seq.ML"} for the underlying
   186   implementation of lazy sequences.
   187 
   188   \item Type @{ML_type "int -> tactic"} represents tactics with
   189   explicit subgoal addressing, with well-formedness conditions as
   190   described above.
   191 
   192   \item @{ML no_tac} is a tactic that always fails, returning the
   193   empty sequence.
   194 
   195   \item @{ML all_tac} is a tactic that always succeeds, returning a
   196   singleton sequence with unchanged goal state.
   197 
   198   \item @{ML print_tac}~@{text "message"} is like @{ML all_tac}, but
   199   prints a message together with the goal state on the tracing
   200   channel.
   201 
   202   \item @{ML PRIMITIVE}~@{text rule} turns a primitive inference rule
   203   into a tactic with unique result.  Exception @{ML THM} is considered
   204   a regular tactic failure and produces an empty result; other
   205   exceptions are passed through.
   206 
   207   \item @{ML SUBGOAL}~@{text "(fn (subgoal, i) => tactic)"} is the
   208   most basic form to produce a tactic with subgoal addressing.  The
   209   given abstraction over the subgoal term and subgoal number allows to
   210   peek at the relevant information of the full goal state.  The
   211   subgoal range is checked as required above.
   212 
   213   \item @{ML CSUBGOAL} is similar to @{ML SUBGOAL}, but passes the
   214   subgoal as @{ML_type cterm} instead of raw @{ML_type term}.  This
   215   avoids expensive re-certification in situations where the subgoal is
   216   used directly for primitive inferences.
   217 
   218   \end{description}
   219 *}
   220 
   221 
   222 subsection {* Resolution and assumption tactics \label{sec:resolve-assume-tac} *}
   223 
   224 text {* \emph{Resolution} is the most basic mechanism for refining a
   225   subgoal using a theorem as object-level rule.
   226   \emph{Elim-resolution} is particularly suited for elimination rules:
   227   it resolves with a rule, proves its first premise by assumption, and
   228   finally deletes that assumption from any new subgoals.
   229   \emph{Destruct-resolution} is like elim-resolution, but the given
   230   destruction rules are first turned into canonical elimination
   231   format.  \emph{Forward-resolution} is like destruct-resolution, but
   232   without deleting the selected assumption.  The @{text "r/e/d/f"}
   233   naming convention is maintained for several different kinds of
   234   resolution rules and tactics.
   235 
   236   Assumption tactics close a subgoal by unifying some of its premises
   237   against its conclusion.
   238 
   239   \medskip All the tactics in this section operate on a subgoal
   240   designated by a positive integer.  Other subgoals might be affected
   241   indirectly, due to instantiation of schematic variables.
   242 
   243   There are various sources of non-determinism, the tactic result
   244   sequence enumerates all possibilities of the following choices (if
   245   applicable):
   246 
   247   \begin{enumerate}
   248 
   249   \item selecting one of the rules given as argument to the tactic;
   250 
   251   \item selecting a subgoal premise to eliminate, unifying it against
   252   the first premise of the rule;
   253 
   254   \item unifying the conclusion of the subgoal to the conclusion of
   255   the rule.
   256 
   257   \end{enumerate}
   258 
   259   Recall that higher-order unification may produce multiple results
   260   that are enumerated here.
   261 *}
   262 
   263 text %mlref {*
   264   \begin{mldecls}
   265   @{index_ML resolve_tac: "thm list -> int -> tactic"} \\
   266   @{index_ML eresolve_tac: "thm list -> int -> tactic"} \\
   267   @{index_ML dresolve_tac: "thm list -> int -> tactic"} \\
   268   @{index_ML forward_tac: "thm list -> int -> tactic"} \\[1ex]
   269   @{index_ML assume_tac: "int -> tactic"} \\
   270   @{index_ML eq_assume_tac: "int -> tactic"} \\[1ex]
   271   @{index_ML match_tac: "thm list -> int -> tactic"} \\
   272   @{index_ML ematch_tac: "thm list -> int -> tactic"} \\
   273   @{index_ML dmatch_tac: "thm list -> int -> tactic"} \\
   274   \end{mldecls}
   275 
   276   \begin{description}
   277 
   278   \item @{ML resolve_tac}~@{text "thms i"} refines the goal state
   279   using the given theorems, which should normally be introduction
   280   rules.  The tactic resolves a rule's conclusion with subgoal @{text
   281   i}, replacing it by the corresponding versions of the rule's
   282   premises.
   283 
   284   \item @{ML eresolve_tac}~@{text "thms i"} performs elim-resolution
   285   with the given theorems, which should normally be elimination rules.
   286 
   287   \item @{ML dresolve_tac}~@{text "thms i"} performs
   288   destruct-resolution with the given theorems, which should normally
   289   be destruction rules.  This replaces an assumption by the result of
   290   applying one of the rules.
   291 
   292   \item @{ML forward_tac} is like @{ML dresolve_tac} except that the
   293   selected assumption is not deleted.  It applies a rule to an
   294   assumption, adding the result as a new assumption.
   295 
   296   \item @{ML assume_tac}~@{text i} attempts to solve subgoal @{text i}
   297   by assumption (modulo higher-order unification).
   298 
   299   \item @{ML eq_assume_tac} is similar to @{ML assume_tac}, but checks
   300   only for immediate @{text "\<alpha>"}-convertibility instead of using
   301   unification.  It succeeds (with a unique next state) if one of the
   302   assumptions is equal to the subgoal's conclusion.  Since it does not
   303   instantiate variables, it cannot make other subgoals unprovable.
   304 
   305   \item @{ML match_tac}, @{ML ematch_tac}, and @{ML dmatch_tac} are
   306   similar to @{ML resolve_tac}, @{ML eresolve_tac}, and @{ML
   307   dresolve_tac}, respectively, but do not instantiate schematic
   308   variables in the goal state.
   309 
   310   Flexible subgoals are not updated at will, but are left alone.
   311   Strictly speaking, matching means to treat the unknowns in the goal
   312   state as constants; these tactics merely discard unifiers that would
   313   update the goal state.
   314 
   315   \end{description}
   316 *}
   317 
   318 
   319 subsection {* Explicit instantiation within a subgoal context *}
   320 
   321 text {* The main resolution tactics (\secref{sec:resolve-assume-tac})
   322   use higher-order unification, which works well in many practical
   323   situations despite its daunting theoretical properties.
   324   Nonetheless, there are important problem classes where unguided
   325   higher-order unification is not so useful.  This typically involves
   326   rules like universal elimination, existential introduction, or
   327   equational substitution.  Here the unification problem involves
   328   fully flexible @{text "?P ?x"} schemes, which are hard to manage
   329   without further hints.
   330 
   331   By providing a (small) rigid term for @{text "?x"} explicitly, the
   332   remaining unification problem is to assign a (large) term to @{text
   333   "?P"}, according to the shape of the given subgoal.  This is
   334   sufficiently well-behaved in most practical situations.
   335 
   336   \medskip Isabelle provides separate versions of the standard @{text
   337   "r/e/d/f"} resolution tactics that allow to provide explicit
   338   instantiations of unknowns of the given rule, wrt.\ terms that refer
   339   to the implicit context of the selected subgoal.
   340 
   341   An instantiation consists of a list of pairs of the form @{text
   342   "(?x, t)"}, where @{text ?x} is a schematic variable occurring in
   343   the given rule, and @{text t} is a term from the current proof
   344   context, augmented by the local goal parameters of the selected
   345   subgoal; cf.\ the @{text "focus"} operation described in
   346   \secref{sec:variables}.
   347 
   348   Entering the syntactic context of a subgoal is a brittle operation,
   349   because its exact form is somewhat accidental, and the choice of
   350   bound variable names depends on the presence of other local and
   351   global names.  Explicit renaming of subgoal parameters prior to
   352   explicit instantiation might help to achieve a bit more robustness.
   353 
   354   Type instantiations may be given as well, via pairs like @{text
   355   "(?'a, \<tau>)"}.  Type instantiations are distinguished from term
   356   instantiations by the syntactic form of the schematic variable.
   357   Types are instantiated before terms are.  Since term instantiation
   358   already performs simple type-inference, so explicit type
   359   instantiations are seldom necessary.
   360 *}
   361 
   362 text %mlref {*
   363   \begin{mldecls}
   364   @{index_ML res_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\
   365   @{index_ML eres_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\
   366   @{index_ML dres_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\
   367   @{index_ML forw_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\[1ex]
   368   @{index_ML rename_tac: "string list -> int -> tactic"} \\
   369   \end{mldecls}
   370 
   371   \begin{description}
   372 
   373   \item @{ML res_inst_tac}~@{text "ctxt insts thm i"} instantiates the
   374   rule @{text thm} with the instantiations @{text insts}, as described
   375   above, and then performs resolution on subgoal @{text i}.
   376   
   377   \item @{ML eres_inst_tac} is like @{ML res_inst_tac}, but performs
   378   elim-resolution.
   379 
   380   \item @{ML dres_inst_tac} is like @{ML res_inst_tac}, but performs
   381   destruct-resolution.
   382 
   383   \item @{ML forw_inst_tac} is like @{ML dres_inst_tac} except that
   384   the selected assumption is not deleted.
   385 
   386   \item @{ML rename_tac}~@{text "names i"} renames the innermost
   387   parameters of subgoal @{text i} according to the provided @{text
   388   names} (which need to be distinct indentifiers).
   389 
   390   \end{description}
   391 
   392   For historical reasons, the above instantiation tactics take
   393   unparsed string arguments, which makes them hard to use in general
   394   ML code.  The slightly more advanced @{ML Subgoal.FOCUS} combinator
   395   of \secref{sec:struct-goals} allows to refer to internal goal
   396   structure with explicit context management.
   397 *}
   398 
   399 
   400 section {* Tacticals \label{sec:tacticals} *}
   401 
   402 text {*
   403   A \emph{tactical} is a functional combinator for building up complex
   404   tactics from simpler ones.  Typical tactical perform sequential
   405   composition, disjunction (choice), iteration, or goal addressing.
   406   Various search strategies may be expressed via tacticals.
   407 
   408   \medskip FIXME
   409 
   410   \medskip The chapter on tacticals in \cite{isabelle-ref} is still
   411   applicable, despite a few outdated details.  *}
   412 
   413 end