author wenzelm
Wed Jan 25 18:18:59 2012 +0100 (2012-01-25)
changeset 46258 89ee3bc580a8
parent 40800 330eb65c9469
child 46259 6fab37137dcb
permissions -rw-r--r--
updated THEN, ORELSE, APPEND, and derivatives;
discontinued obscure INTLEAVE;
     1 theory Tactic
     2 imports Base
     3 begin
     5 chapter {* Tactical reasoning *}
     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.  *}
    16 section {* Goals \label{sec:tactical-goals} *}
    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''.
    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)"}]{@{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 *}
    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}
    69   \begin{description}
    71   \item @{ML "Goal.init"}~@{text C} initializes a tactical goal from
    72   the well-formed proposition @{text C}.
    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.
    79   \item @{ML "Goal.protect"}~@{text "thm"} protects the full statement
    80   of theorem @{text "thm"}.
    82   \item @{ML "Goal.conclude"}~@{text "thm"} removes the goal
    83   protection, even if there are pending subgoals.
    85   \end{description}
    86 *}
    89 section {* Tactics\label{sec:tactics} *}
    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.}
   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.
   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}.
   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).
   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!
   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.
   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!
   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.
   143   \medskip The main well-formedness conditions for proper tactics are
   144   summarized as follows.
   146   \begin{itemize}
   148   \item General tactic failure is indicated by an empty result, only
   149   serious faults may produce an exception.
   151   \item The main conclusion must not be changed, apart from
   152   instantiating schematic variables.
   154   \item A tactic operates either uniformly on all subgoals, or
   155   specifically on a selected subgoal (without bumping into unrelated
   156   subgoals).
   158   \item Range errors in subgoal addressing produce an empty result.
   160   \end{itemize}
   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 *}
   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}
   181   \begin{description}
   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.
   188   \item Type @{ML_type "int -> tactic"} represents tactics with
   189   explicit subgoal addressing, with well-formedness conditions as
   190   described above.
   192   \item @{ML no_tac} is a tactic that always fails, returning the
   193   empty sequence.
   195   \item @{ML all_tac} is a tactic that always succeeds, returning a
   196   singleton sequence with unchanged goal state.
   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.
   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.
   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.
   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.
   218   \end{description}
   219 *}
   222 subsection {* Resolution and assumption tactics \label{sec:resolve-assume-tac} *}
   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.
   236   Assumption tactics close a subgoal by unifying some of its premises
   237   against its conclusion.
   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.
   243   There are various sources of non-determinism, the tactic result
   244   sequence enumerates all possibilities of the following choices (if
   245   applicable):
   247   \begin{enumerate}
   249   \item selecting one of the rules given as argument to the tactic;
   251   \item selecting a subgoal premise to eliminate, unifying it against
   252   the first premise of the rule;
   254   \item unifying the conclusion of the subgoal to the conclusion of
   255   the rule.
   257   \end{enumerate}
   259   Recall that higher-order unification may produce multiple results
   260   that are enumerated here.
   261 *}
   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}
   276   \begin{description}
   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.
   284   \item @{ML eresolve_tac}~@{text "thms i"} performs elim-resolution
   285   with the given theorems, which should normally be elimination rules.
   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.
   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.
   296   \item @{ML assume_tac}~@{text i} attempts to solve subgoal @{text i}
   297   by assumption (modulo higher-order unification).
   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.
   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.
   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.
   315   \end{description}
   316 *}
   319 subsection {* Explicit instantiation within a subgoal context *}
   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.
   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.
   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.
   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}.
   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.
   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 *}
   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}
   371   \begin{description}
   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}.
   377   \item @{ML eres_inst_tac} is like @{ML res_inst_tac}, but performs
   378   elim-resolution.
   380   \item @{ML dres_inst_tac} is like @{ML res_inst_tac}, but performs
   381   destruct-resolution.
   383   \item @{ML forw_inst_tac} is like @{ML dres_inst_tac} except that
   384   the selected assumption is not deleted.
   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).
   390   \end{description}
   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 *}
   400 section {* Tacticals \label{sec:tacticals} *}
   402 text {* A \emph{tactical} is a functional combinator for building up
   403   complex tactics from simpler ones.  Common tacticals perform
   404   sequential composition, disjunctive choice, iteration, or goal
   405   addressing.  Various search strategies may be expressed via
   406   tacticals.
   408   \medskip The chapter on tacticals in old \cite{isabelle-ref} is
   409   still applicable for further details.  *}
   412 subsection {* Combining tactics *}
   414 text {* Sequential composition and alternative choices are the most
   415   basic ways to combine tactics, similarly to ``@{verbatim ","}'' and
   416   ``@{verbatim "|"}'' in Isar method notation.  This corresponds to
   417   @{text "THEN"} and @{text "ORELSE"} in ML, but there are further
   418   possibilities for fine-tuning alternation of tactics such as @{text
   419   "APPEND"}.  Further details become visible in ML due to explicit
   420   subgoal addressing.  *}
   422 text %mlref {*
   423   \begin{mldecls}
   424   @{index_ML "op THEN": "tactic * tactic -> tactic"} \\
   425   @{index_ML "op ORELSE": "tactic * tactic -> tactic"} \\
   426   @{index_ML "op APPEND": "tactic * tactic -> tactic"} \\
   427   @{index_ML "EVERY": "tactic list -> tactic"} \\
   428   @{index_ML "FIRST": "tactic list -> tactic"} \\[0.5ex]
   430   @{index_ML "op THEN'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\
   431   @{index_ML "op ORELSE'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\
   432   @{index_ML "op APPEND'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\
   433   @{index_ML "EVERY'": "('a -> tactic) list -> 'a -> tactic"} \\
   434   @{index_ML "FIRST'": "('a -> tactic) list -> 'a -> tactic"} \\
   435   @{index_ML "EVERY1": "(int -> tactic) list -> tactic"} \\
   436   @{index_ML "FIRST1": "(int -> tactic) list -> tactic"} \\[0.5ex]
   437   \end{mldecls}
   439   \begin{description}
   441   \item @{text "tac\<^sub>1 THEN tac\<^sub>2"} is the sequential composition of
   442   @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"}.  Applied to a proof state, it
   443   returns all states reachable in two steps by applying @{text "tac\<^sub>1"}
   444   followed by @{text "tac\<^sub>2"}.  First, it applies @{text "tac\<^sub>1"} to the
   445   proof state, getting a sequence of possible next states; then, it
   446   applies @{text "tac\<^sub>2"} to each of these and concatenates the results
   447   to produce again one flat sequence of states.
   449   \item @{text "tac\<^sub>1 ORELSE tac\<^sub>2"} makes a choice between @{text
   450   "tac\<^sub>1"} and @{text "tac\<^sub>2"}.  Applied to a state, it tries @{text
   451   "tac\<^sub>1"} and returns the result if non-empty; if @{text "tac\<^sub>1"} fails
   452   then it uses @{text "tac\<^sub>2"}.  This is a deterministic choice: if
   453   @{text "tac\<^sub>1"} succeeds then @{text "tac\<^sub>2"} is excluded from the
   454   result.
   456   \item @{text "tac\<^sub>1 APPEND tac\<^sub>2"} concatenates the possible results
   457   of @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"}.  Unlike @{text "ORELSE"} there
   458   is \emph{no commitment} to either tactic, so @{text "APPEND"} helps
   459   to avoid incompleteness during search, at the cost of potential
   460   inefficiencies.
   462   \item @{text "EVERY [tac\<^sub>1, \<dots>, tac\<^sub>n]"} abbreviates @{text "tac\<^sub>1 THEN
   463   \<dots> THEN tac\<^sub>n"}.  Note that @{text "EVERY []"} is the same as @{ML
   464   all_tac}: it always succeeds.
   466   \item @{text "FIRST [tac\<^sub>1, \<dots>, tac\<^sub>n]"} abbreviates @{text "tac\<^sub>1
   467   ORELSE \<dots> ORELSE tac\<^sub>n"}.  Note that @{text "FIRST []"} is the same as
   468   @{ML no_tac}: it always fails.
   470   \item @{text "THEN'"}, @{text "ORELSE'"}, and @{text "APPEND'"} are
   471   lifted versions of @{text "THEN"}, @{text "ORELSE"}, and @{text
   472   "APPEND"}, for tactics with explicit subgoal addressing.  This means
   473   @{text "(tac\<^sub>1 THEN' tac\<^sub>2) i"} is the same as @{text "(tac\<^sub>1 i THEN
   474   tac\<^sub>2 i)"} etc.
   476   \item @{text "EVERY'"} and @{text "FIRST'"} are lifted versions of
   477   @{text "EVERY'"} and @{text "FIRST'"}, for tactics with explicit
   478   subgoal addressing.
   480   \item @{text "EVERY1"} and @{text "FIRST1"} are convenience versions
   481   of @{text "EVERY'"} and @{text "FIRST'"}, applied to subgoal 1.
   483   \end{description}
   484 *}
   486 end