doc-src/IsarImplementation/Thy/Tactic.thy
 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

     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 {* 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.

   407

   408   \medskip The chapter on tacticals in old \cite{isabelle-ref} is

   409   still applicable for further details.  *}

   410

   411

   412 subsection {* Combining tactics *}

   413

   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.  *}

   421

   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]

   429

   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}

   438

   439   \begin{description}

   440

   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.

   448

   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.

   455

   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.

   461

   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.

   465

   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.

   469

   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.

   475

   476   \item @{text "EVERY'"} and @{text "FIRST'"} are lifted versions of

   477   @{text "EVERY'"} and @{text "FIRST'"}, for tactics with explicit

   478   subgoal addressing.

   479

   480   \item @{text "EVERY1"} and @{text "FIRST1"} are convenience versions

   481   of @{text "EVERY'"} and @{text "FIRST'"}, applied to subgoal 1.

   482

   483   \end{description}

   484 *}

   485

   486 end