src/Doc/Implementation/Tactic.thy
 author wenzelm Sun Nov 09 17:04:14 2014 +0100 (2014-11-09) changeset 58957 c9e744ea8a38 parent 58956 a816aa3ff391 child 58963 26bf09b95dda permissions -rw-r--r--
proper context for match_tac etc.;
     1 theory Tactic

     2 imports Base

     3 begin

     4

     5 chapter \<open>Tactical reasoning\<close>

     6

     7 text \<open>Tactical reasoning works by refining an initial claim in a

     8   backwards fashion, until a solved form is reached.  A @{text "goal"}

     9   consists of several subgoals that need to be solved in order to

    10   achieve the main statement; zero subgoals means that the proof may

    11   be finished.  A @{text "tactic"} is a refinement operation that maps

    12   a goal to a lazy sequence of potential successors.  A @{text

    13   "tactical"} is a combinator for composing tactics.\<close>

    14

    15

    16 section \<open>Goals \label{sec:tactical-goals}\<close>

    17

    18 text \<open>

    19   Isabelle/Pure represents a goal as a theorem stating that the

    20   subgoals imply the main goal: @{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow>

    21   C"}.  The outermost goal structure is that of a Horn Clause: i.e.\

    22   an iterated implication without any quantifiers\footnote{Recall that

    23   outermost @{text "\<And>x. \<phi>[x]"} is always represented via schematic

    24   variables in the body: @{text "\<phi>[?x]"}.  These variables may get

    25   instantiated during the course of reasoning.}.  For @{text "n = 0"}

    26   a goal is called solved''.

    27

    28   The structure of each subgoal @{text "A\<^sub>i"} is that of a

    29   general Hereditary Harrop Formula @{text "\<And>x\<^sub>1 \<dots>

    30   \<And>x\<^sub>k. H\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> H\<^sub>m \<Longrightarrow> B"}.  Here @{text

    31   "x\<^sub>1, \<dots>, x\<^sub>k"} are goal parameters, i.e.\

    32   arbitrary-but-fixed entities of certain types, and @{text

    33   "H\<^sub>1, \<dots>, H\<^sub>m"} are goal hypotheses, i.e.\ facts that may

    34   be assumed locally.  Together, this forms the goal context of the

    35   conclusion @{text B} to be established.  The goal hypotheses may be

    36   again arbitrary Hereditary Harrop Formulas, although the level of

    37   nesting rarely exceeds 1--2 in practice.

    38

    39   The main conclusion @{text C} is internally marked as a protected

    40   proposition, which is represented explicitly by the notation @{text

    41   "#C"} here.  This ensures that the decomposition into subgoals and

    42   main conclusion is well-defined for arbitrarily structured claims.

    43

    44   \medskip Basic goal management is performed via the following

    45   Isabelle/Pure rules:

    46

    47   $  48 \infer[@{text "(init)"}]{@{text "C \<Longrightarrow> #C"}}{} \qquad   49 \infer[@{text "(finish)"}]{@{text "C"}}{@{text "#C"}}   50$

    51

    52   \medskip The following low-level variants admit general reasoning

    53   with protected propositions:

    54

    55   $  56 \infer[@{text "(protect n)"}]{@{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> #C"}}{@{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> C"}}   57$

    58   $  59 \infer[@{text "(conclude)"}]{@{text "A \<Longrightarrow> \<dots> \<Longrightarrow> C"}}{@{text "A \<Longrightarrow> \<dots> \<Longrightarrow> #C"}}   60$

    61 \<close>

    62

    63 text %mlref \<open>

    64   \begin{mldecls}

    65   @{index_ML Goal.init: "cterm -> thm"} \\

    66   @{index_ML Goal.finish: "Proof.context -> thm -> thm"} \\

    67   @{index_ML Goal.protect: "int -> thm -> thm"} \\

    68   @{index_ML Goal.conclude: "thm -> thm"} \\

    69   \end{mldecls}

    70

    71   \begin{description}

    72

    73   \item @{ML "Goal.init"}~@{text C} initializes a tactical goal from

    74   the well-formed proposition @{text C}.

    75

    76   \item @{ML "Goal.finish"}~@{text "ctxt thm"} checks whether theorem

    77   @{text "thm"} is a solved goal (no subgoals), and concludes the

    78   result by removing the goal protection.  The context is only

    79   required for printing error messages.

    80

    81   \item @{ML "Goal.protect"}~@{text "n thm"} protects the statement

    82   of theorem @{text "thm"}.  The parameter @{text n} indicates the

    83   number of premises to be retained.

    84

    85   \item @{ML "Goal.conclude"}~@{text "thm"} removes the goal

    86   protection, even if there are pending subgoals.

    87

    88   \end{description}

    89 \<close>

    90

    91

    92 section \<open>Tactics\label{sec:tactics}\<close>

    93

    94 text \<open>A @{text "tactic"} is a function @{text "goal \<rightarrow> goal\<^sup>*\<^sup>*"} that

    95   maps a given goal state (represented as a theorem, cf.\

    96   \secref{sec:tactical-goals}) to a lazy sequence of potential

    97   successor states.  The underlying sequence implementation is lazy

    98   both in head and tail, and is purely functional in \emph{not}

    99   supporting memoing.\footnote{The lack of memoing and the strict

   100   nature of ML requires some care when working with low-level

   101   sequence operations, to avoid duplicate or premature evaluation of

   102   results.  It also means that modified runtime behavior, such as

   103   timeout, is very hard to achieve for general tactics.}

   104

   105   An \emph{empty result sequence} means that the tactic has failed: in

   106   a compound tactic expression other tactics might be tried instead,

   107   or the whole refinement step might fail outright, producing a

   108   toplevel error message in the end.  When implementing tactics from

   109   scratch, one should take care to observe the basic protocol of

   110   mapping regular error conditions to an empty result; only serious

   111   faults should emerge as exceptions.

   112

   113   By enumerating \emph{multiple results}, a tactic can easily express

   114   the potential outcome of an internal search process.  There are also

   115   combinators for building proof tools that involve search

   116   systematically, see also \secref{sec:tacticals}.

   117

   118   \medskip As explained before, a goal state essentially consists of a

   119   list of subgoals that imply the main goal (conclusion).  Tactics may

   120   operate on all subgoals or on a particularly specified subgoal, but

   121   must not change the main conclusion (apart from instantiating

   122   schematic goal variables).

   123

   124   Tactics with explicit \emph{subgoal addressing} are of the form

   125   @{text "int \<rightarrow> tactic"} and may be applied to a particular subgoal

   126   (counting from 1).  If the subgoal number is out of range, the

   127   tactic should fail with an empty result sequence, but must not raise

   128   an exception!

   129

   130   Operating on a particular subgoal means to replace it by an interval

   131   of zero or more subgoals in the same place; other subgoals must not

   132   be affected, apart from instantiating schematic variables ranging

   133   over the whole goal state.

   134

   135   A common pattern of composing tactics with subgoal addressing is to

   136   try the first one, and then the second one only if the subgoal has

   137   not been solved yet.  Special care is required here to avoid bumping

   138   into unrelated subgoals that happen to come after the original

   139   subgoal.  Assuming that there is only a single initial subgoal is a

   140   very common error when implementing tactics!

   141

   142   Tactics with internal subgoal addressing should expose the subgoal

   143   index as @{text "int"} argument in full generality; a hardwired

   144   subgoal 1 is not acceptable.

   145

   146   \medskip The main well-formedness conditions for proper tactics are

   147   summarized as follows.

   148

   149   \begin{itemize}

   150

   151   \item General tactic failure is indicated by an empty result, only

   152   serious faults may produce an exception.

   153

   154   \item The main conclusion must not be changed, apart from

   155   instantiating schematic variables.

   156

   157   \item A tactic operates either uniformly on all subgoals, or

   158   specifically on a selected subgoal (without bumping into unrelated

   159   subgoals).

   160

   161   \item Range errors in subgoal addressing produce an empty result.

   162

   163   \end{itemize}

   164

   165   Some of these conditions are checked by higher-level goal

   166   infrastructure (\secref{sec:struct-goals}); others are not checked

   167   explicitly, and violating them merely results in ill-behaved tactics

   168   experienced by the user (e.g.\ tactics that insist in being

   169   applicable only to singleton goals, or prevent composition via

   170   standard tacticals such as @{ML REPEAT}).

   171 \<close>

   172

   173 text %mlref \<open>

   174   \begin{mldecls}

   175   @{index_ML_type tactic: "thm -> thm Seq.seq"} \\

   176   @{index_ML no_tac: tactic} \\

   177   @{index_ML all_tac: tactic} \\

   178   @{index_ML print_tac: "Proof.context -> string -> tactic"} \\[1ex]

   179   @{index_ML PRIMITIVE: "(thm -> thm) -> tactic"} \\[1ex]

   180   @{index_ML SUBGOAL: "(term * int -> tactic) -> int -> tactic"} \\

   181   @{index_ML CSUBGOAL: "(cterm * int -> tactic) -> int -> tactic"} \\

   182   @{index_ML SELECT_GOAL: "tactic -> int -> tactic"} \\

   183   @{index_ML PREFER_GOAL: "tactic -> int -> tactic"} \\

   184   \end{mldecls}

   185

   186   \begin{description}

   187

   188   \item Type @{ML_type tactic} represents tactics.  The

   189   well-formedness conditions described above need to be observed.  See

   190   also @{file "~~/src/Pure/General/seq.ML"} for the underlying

   191   implementation of lazy sequences.

   192

   193   \item Type @{ML_type "int -> tactic"} represents tactics with

   194   explicit subgoal addressing, with well-formedness conditions as

   195   described above.

   196

   197   \item @{ML no_tac} is a tactic that always fails, returning the

   198   empty sequence.

   199

   200   \item @{ML all_tac} is a tactic that always succeeds, returning a

   201   singleton sequence with unchanged goal state.

   202

   203   \item @{ML print_tac}~@{text "ctxt message"} is like @{ML all_tac}, but

   204   prints a message together with the goal state on the tracing

   205   channel.

   206

   207   \item @{ML PRIMITIVE}~@{text rule} turns a primitive inference rule

   208   into a tactic with unique result.  Exception @{ML THM} is considered

   209   a regular tactic failure and produces an empty result; other

   210   exceptions are passed through.

   211

   212   \item @{ML SUBGOAL}~@{text "(fn (subgoal, i) => tactic)"} is the

   213   most basic form to produce a tactic with subgoal addressing.  The

   214   given abstraction over the subgoal term and subgoal number allows to

   215   peek at the relevant information of the full goal state.  The

   216   subgoal range is checked as required above.

   217

   218   \item @{ML CSUBGOAL} is similar to @{ML SUBGOAL}, but passes the

   219   subgoal as @{ML_type cterm} instead of raw @{ML_type term}.  This

   220   avoids expensive re-certification in situations where the subgoal is

   221   used directly for primitive inferences.

   222

   223   \item @{ML SELECT_GOAL}~@{text "tac i"} confines a tactic to the

   224   specified subgoal @{text "i"}.  This rearranges subgoals and the

   225   main goal protection (\secref{sec:tactical-goals}), while retaining

   226   the syntactic context of the overall goal state (concerning

   227   schematic variables etc.).

   228

   229   \item @{ML PREFER_GOAL}~@{text "tac i"} rearranges subgoals to put

   230   @{text "i"} in front.  This is similar to @{ML SELECT_GOAL}, but

   231   without changing the main goal protection.

   232

   233   \end{description}

   234 \<close>

   235

   236

   237 subsection \<open>Resolution and assumption tactics \label{sec:resolve-assume-tac}\<close>

   238

   239 text \<open>\emph{Resolution} is the most basic mechanism for refining a

   240   subgoal using a theorem as object-level rule.

   241   \emph{Elim-resolution} is particularly suited for elimination rules:

   242   it resolves with a rule, proves its first premise by assumption, and

   243   finally deletes that assumption from any new subgoals.

   244   \emph{Destruct-resolution} is like elim-resolution, but the given

   245   destruction rules are first turned into canonical elimination

   246   format.  \emph{Forward-resolution} is like destruct-resolution, but

   247   without deleting the selected assumption.  The @{text "r/e/d/f"}

   248   naming convention is maintained for several different kinds of

   249   resolution rules and tactics.

   250

   251   Assumption tactics close a subgoal by unifying some of its premises

   252   against its conclusion.

   253

   254   \medskip All the tactics in this section operate on a subgoal

   255   designated by a positive integer.  Other subgoals might be affected

   256   indirectly, due to instantiation of schematic variables.

   257

   258   There are various sources of non-determinism, the tactic result

   259   sequence enumerates all possibilities of the following choices (if

   260   applicable):

   261

   262   \begin{enumerate}

   263

   264   \item selecting one of the rules given as argument to the tactic;

   265

   266   \item selecting a subgoal premise to eliminate, unifying it against

   267   the first premise of the rule;

   268

   269   \item unifying the conclusion of the subgoal to the conclusion of

   270   the rule.

   271

   272   \end{enumerate}

   273

   274   Recall that higher-order unification may produce multiple results

   275   that are enumerated here.

   276 \<close>

   277

   278 text %mlref \<open>

   279   \begin{mldecls}

   280   @{index_ML resolve_tac: "thm list -> int -> tactic"} \\

   281   @{index_ML eresolve_tac: "thm list -> int -> tactic"} \\

   282   @{index_ML dresolve_tac: "thm list -> int -> tactic"} \\

   283   @{index_ML forward_tac: "thm list -> int -> tactic"} \\

   284   @{index_ML biresolve_tac: "(bool * thm) list -> int -> tactic"} \\[1ex]

   285   @{index_ML assume_tac: "int -> tactic"} \\

   286   @{index_ML eq_assume_tac: "int -> tactic"} \\[1ex]

   287   @{index_ML match_tac: "Proof.context -> thm list -> int -> tactic"} \\

   288   @{index_ML ematch_tac: "Proof.context -> thm list -> int -> tactic"} \\

   289   @{index_ML dmatch_tac: "Proof.context -> thm list -> int -> tactic"} \\

   290   @{index_ML bimatch_tac: "Proof.context -> (bool * thm) list -> int -> tactic"} \\

   291   \end{mldecls}

   292

   293   \begin{description}

   294

   295   \item @{ML resolve_tac}~@{text "thms i"} refines the goal state

   296   using the given theorems, which should normally be introduction

   297   rules.  The tactic resolves a rule's conclusion with subgoal @{text

   298   i}, replacing it by the corresponding versions of the rule's

   299   premises.

   300

   301   \item @{ML eresolve_tac}~@{text "thms i"} performs elim-resolution

   302   with the given theorems, which are normally be elimination rules.

   303

   304   Note that @{ML "eresolve_tac [asm_rl]"} is equivalent to @{ML

   305   assume_tac}, which facilitates mixing of assumption steps with

   306   genuine eliminations.

   307

   308   \item @{ML dresolve_tac}~@{text "thms i"} performs

   309   destruct-resolution with the given theorems, which should normally

   310   be destruction rules.  This replaces an assumption by the result of

   311   applying one of the rules.

   312

   313   \item @{ML forward_tac} is like @{ML dresolve_tac} except that the

   314   selected assumption is not deleted.  It applies a rule to an

   315   assumption, adding the result as a new assumption.

   316

   317   \item @{ML biresolve_tac}~@{text "brls i"} refines the proof state

   318   by resolution or elim-resolution on each rule, as indicated by its

   319   flag.  It affects subgoal @{text "i"} of the proof state.

   320

   321   For each pair @{text "(flag, rule)"}, it applies resolution if the

   322   flag is @{text "false"} and elim-resolution if the flag is @{text

   323   "true"}.  A single tactic call handles a mixture of introduction and

   324   elimination rules, which is useful to organize the search process

   325   systematically in proof tools.

   326

   327   \item @{ML assume_tac}~@{text i} attempts to solve subgoal @{text i}

   328   by assumption (modulo higher-order unification).

   329

   330   \item @{ML eq_assume_tac} is similar to @{ML assume_tac}, but checks

   331   only for immediate @{text "\<alpha>"}-convertibility instead of using

   332   unification.  It succeeds (with a unique next state) if one of the

   333   assumptions is equal to the subgoal's conclusion.  Since it does not

   334   instantiate variables, it cannot make other subgoals unprovable.

   335

   336   \item @{ML match_tac}, @{ML ematch_tac}, @{ML dmatch_tac}, and @{ML

   337   bimatch_tac} are similar to @{ML resolve_tac}, @{ML eresolve_tac},

   338   @{ML dresolve_tac}, and @{ML biresolve_tac}, respectively, but do

   339   not instantiate schematic variables in the goal state.%

   340 \footnote{Strictly speaking, matching means to treat the unknowns in the goal

   341   state as constants, but these tactics merely discard unifiers that would

   342   update the goal state. In rare situations (where the conclusion and

   343   goal state have flexible terms at the same position), the tactic

   344   will fail even though an acceptable unifier exists.}

   345   These tactics were written for a specific application within the classical reasoner.

   346

   347   Flexible subgoals are not updated at will, but are left alone.

   348   \end{description}

   349 \<close>

   350

   351

   352 subsection \<open>Explicit instantiation within a subgoal context\<close>

   353

   354 text \<open>The main resolution tactics (\secref{sec:resolve-assume-tac})

   355   use higher-order unification, which works well in many practical

   356   situations despite its daunting theoretical properties.

   357   Nonetheless, there are important problem classes where unguided

   358   higher-order unification is not so useful.  This typically involves

   359   rules like universal elimination, existential introduction, or

   360   equational substitution.  Here the unification problem involves

   361   fully flexible @{text "?P ?x"} schemes, which are hard to manage

   362   without further hints.

   363

   364   By providing a (small) rigid term for @{text "?x"} explicitly, the

   365   remaining unification problem is to assign a (large) term to @{text

   366   "?P"}, according to the shape of the given subgoal.  This is

   367   sufficiently well-behaved in most practical situations.

   368

   369   \medskip Isabelle provides separate versions of the standard @{text

   370   "r/e/d/f"} resolution tactics that allow to provide explicit

   371   instantiations of unknowns of the given rule, wrt.\ terms that refer

   372   to the implicit context of the selected subgoal.

   373

   374   An instantiation consists of a list of pairs of the form @{text

   375   "(?x, t)"}, where @{text ?x} is a schematic variable occurring in

   376   the given rule, and @{text t} is a term from the current proof

   377   context, augmented by the local goal parameters of the selected

   378   subgoal; cf.\ the @{text "focus"} operation described in

   379   \secref{sec:variables}.

   380

   381   Entering the syntactic context of a subgoal is a brittle operation,

   382   because its exact form is somewhat accidental, and the choice of

   383   bound variable names depends on the presence of other local and

   384   global names.  Explicit renaming of subgoal parameters prior to

   385   explicit instantiation might help to achieve a bit more robustness.

   386

   387   Type instantiations may be given as well, via pairs like @{text

   388   "(?'a, \<tau>)"}.  Type instantiations are distinguished from term

   389   instantiations by the syntactic form of the schematic variable.

   390   Types are instantiated before terms are.  Since term instantiation

   391   already performs simple type-inference, so explicit type

   392   instantiations are seldom necessary.

   393 \<close>

   394

   395 text %mlref \<open>

   396   \begin{mldecls}

   397   @{index_ML res_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\

   398   @{index_ML eres_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\

   399   @{index_ML dres_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\

   400   @{index_ML forw_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\

   401   @{index_ML subgoal_tac: "Proof.context -> string -> int -> tactic"} \\

   402   @{index_ML thin_tac: "Proof.context -> string -> int -> tactic"} \\

   403   @{index_ML rename_tac: "string list -> int -> tactic"} \\

   404   \end{mldecls}

   405

   406   \begin{description}

   407

   408   \item @{ML res_inst_tac}~@{text "ctxt insts thm i"} instantiates the

   409   rule @{text thm} with the instantiations @{text insts}, as described

   410   above, and then performs resolution on subgoal @{text i}.

   411

   412   \item @{ML eres_inst_tac} is like @{ML res_inst_tac}, but performs

   413   elim-resolution.

   414

   415   \item @{ML dres_inst_tac} is like @{ML res_inst_tac}, but performs

   416   destruct-resolution.

   417

   418   \item @{ML forw_inst_tac} is like @{ML dres_inst_tac} except that

   419   the selected assumption is not deleted.

   420

   421   \item @{ML subgoal_tac}~@{text "ctxt \<phi> i"} adds the proposition

   422   @{text "\<phi>"} as local premise to subgoal @{text "i"}, and poses the

   423   same as a new subgoal @{text "i + 1"} (in the original context).

   424

   425   \item @{ML thin_tac}~@{text "ctxt \<phi> i"} deletes the specified

   426   premise from subgoal @{text i}.  Note that @{text \<phi>} may contain

   427   schematic variables, to abbreviate the intended proposition; the

   428   first matching subgoal premise will be deleted.  Removing useless

   429   premises from a subgoal increases its readability and can make

   430   search tactics run faster.

   431

   432   \item @{ML rename_tac}~@{text "names i"} renames the innermost

   433   parameters of subgoal @{text i} according to the provided @{text

   434   names} (which need to be distinct identifiers).

   435

   436   \end{description}

   437

   438   For historical reasons, the above instantiation tactics take

   439   unparsed string arguments, which makes them hard to use in general

   440   ML code.  The slightly more advanced @{ML Subgoal.FOCUS} combinator

   441   of \secref{sec:struct-goals} allows to refer to internal goal

   442   structure with explicit context management.

   443 \<close>

   444

   445

   446 subsection \<open>Rearranging goal states\<close>

   447

   448 text \<open>In rare situations there is a need to rearrange goal states:

   449   either the overall collection of subgoals, or the local structure of

   450   a subgoal.  Various administrative tactics allow to operate on the

   451   concrete presentation these conceptual sets of formulae.\<close>

   452

   453 text %mlref \<open>

   454   \begin{mldecls}

   455   @{index_ML rotate_tac: "int -> int -> tactic"} \\

   456   @{index_ML distinct_subgoals_tac: tactic} \\

   457   @{index_ML flexflex_tac: "Proof.context -> tactic"} \\

   458   \end{mldecls}

   459

   460   \begin{description}

   461

   462   \item @{ML rotate_tac}~@{text "n i"} rotates the premises of subgoal

   463   @{text i} by @{text n} positions: from right to left if @{text n} is

   464   positive, and from left to right if @{text n} is negative.

   465

   466   \item @{ML distinct_subgoals_tac} removes duplicate subgoals from a

   467   proof state.  This is potentially inefficient.

   468

   469   \item @{ML flexflex_tac} removes all flex-flex pairs from the proof

   470   state by applying the trivial unifier.  This drastic step loses

   471   information.  It is already part of the Isar infrastructure for

   472   facts resulting from goals, and rarely needs to be invoked manually.

   473

   474   Flex-flex constraints arise from difficult cases of higher-order

   475   unification.  To prevent this, use @{ML res_inst_tac} to instantiate

   476   some variables in a rule.  Normally flex-flex constraints can be

   477   ignored; they often disappear as unknowns get instantiated.

   478

   479   \end{description}

   480 \<close>

   481

   482

   483 subsection \<open>Raw composition: resolution without lifting\<close>

   484

   485 text \<open>

   486   Raw composition of two rules means resolving them without prior

   487   lifting or renaming of unknowns.  This low-level operation, which

   488   underlies the resolution tactics, may occasionally be useful for

   489   special effects.  Schematic variables are not renamed by default, so

   490   beware of clashes!

   491 \<close>

   492

   493 text %mlref \<open>

   494   \begin{mldecls}

   495   @{index_ML compose_tac: "Proof.context -> (bool * thm * int) -> int -> tactic"} \\

   496   @{index_ML Drule.compose: "thm * int * thm -> thm"} \\

   497   @{index_ML_op COMP: "thm * thm -> thm"} \\

   498   \end{mldecls}

   499

   500   \begin{description}

   501

   502   \item @{ML compose_tac}~@{text "ctxt (flag, rule, m) i"} refines subgoal

   503   @{text "i"} using @{text "rule"}, without lifting.  The @{text

   504   "rule"} is taken to have the form @{text "\<psi>\<^sub>1 \<Longrightarrow> \<dots> \<psi>\<^sub>m \<Longrightarrow> \<psi>"}, where

   505   @{text "\<psi>"} need not be atomic; thus @{text "m"} determines the

   506   number of new subgoals.  If @{text "flag"} is @{text "true"} then it

   507   performs elim-resolution --- it solves the first premise of @{text

   508   "rule"} by assumption and deletes that assumption.

   509

   510   \item @{ML Drule.compose}~@{text "(thm\<^sub>1, i, thm\<^sub>2)"} uses @{text "thm\<^sub>1"},

   511   regarded as an atomic formula, to solve premise @{text "i"} of

   512   @{text "thm\<^sub>2"}.  Let @{text "thm\<^sub>1"} and @{text "thm\<^sub>2"} be @{text

   513   "\<psi>"} and @{text "\<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> \<phi>"}.  The unique @{text "s"} that

   514   unifies @{text "\<psi>"} and @{text "\<phi>\<^sub>i"} yields the theorem @{text "(\<phi>\<^sub>1 \<Longrightarrow>

   515   \<dots> \<phi>\<^sub>i\<^sub>-\<^sub>1 \<Longrightarrow> \<phi>\<^sub>i\<^sub>+\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> \<phi>)s"}.  Multiple results are considered as

   516   error (exception @{ML THM}).

   517

   518   \item @{text "thm\<^sub>1 COMP thm\<^sub>2"} is the same as @{text "Drule.compose

   519   (thm\<^sub>1, 1, thm\<^sub>2)"}.

   520

   521   \end{description}

   522

   523   \begin{warn}

   524   These low-level operations are stepping outside the structure

   525   imposed by regular rule resolution.  Used without understanding of

   526   the consequences, they may produce results that cause problems with

   527   standard rules and tactics later on.

   528   \end{warn}

   529 \<close>

   530

   531

   532 section \<open>Tacticals \label{sec:tacticals}\<close>

   533

   534 text \<open>A \emph{tactical} is a functional combinator for building up

   535   complex tactics from simpler ones.  Common tacticals perform

   536   sequential composition, disjunctive choice, iteration, or goal

   537   addressing.  Various search strategies may be expressed via

   538   tacticals.

   539 \<close>

   540

   541

   542 subsection \<open>Combining tactics\<close>

   543

   544 text \<open>Sequential composition and alternative choices are the most

   545   basic ways to combine tactics, similarly to @{verbatim ","}'' and

   546   @{verbatim "|"}'' in Isar method notation.  This corresponds to

   547   @{ML_op "THEN"} and @{ML_op "ORELSE"} in ML, but there are further

   548   possibilities for fine-tuning alternation of tactics such as @{ML_op

   549   "APPEND"}.  Further details become visible in ML due to explicit

   550   subgoal addressing.

   551 \<close>

   552

   553 text %mlref \<open>

   554   \begin{mldecls}

   555   @{index_ML_op "THEN": "tactic * tactic -> tactic"} \\

   556   @{index_ML_op "ORELSE": "tactic * tactic -> tactic"} \\

   557   @{index_ML_op "APPEND": "tactic * tactic -> tactic"} \\

   558   @{index_ML "EVERY": "tactic list -> tactic"} \\

   559   @{index_ML "FIRST": "tactic list -> tactic"} \\[0.5ex]

   560

   561   @{index_ML_op "THEN'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\

   562   @{index_ML_op "ORELSE'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\

   563   @{index_ML_op "APPEND'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\

   564   @{index_ML "EVERY'": "('a -> tactic) list -> 'a -> tactic"} \\

   565   @{index_ML "FIRST'": "('a -> tactic) list -> 'a -> tactic"} \\

   566   \end{mldecls}

   567

   568   \begin{description}

   569

   570   \item @{text "tac\<^sub>1"}~@{ML_op THEN}~@{text "tac\<^sub>2"} is the sequential

   571   composition of @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"}.  Applied to a goal

   572   state, it returns all states reachable in two steps by applying

   573   @{text "tac\<^sub>1"} followed by @{text "tac\<^sub>2"}.  First, it applies @{text

   574   "tac\<^sub>1"} to the goal state, getting a sequence of possible next

   575   states; then, it applies @{text "tac\<^sub>2"} to each of these and

   576   concatenates the results to produce again one flat sequence of

   577   states.

   578

   579   \item @{text "tac\<^sub>1"}~@{ML_op ORELSE}~@{text "tac\<^sub>2"} makes a choice

   580   between @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"}.  Applied to a state, it

   581   tries @{text "tac\<^sub>1"} and returns the result if non-empty; if @{text

   582   "tac\<^sub>1"} fails then it uses @{text "tac\<^sub>2"}.  This is a deterministic

   583   choice: if @{text "tac\<^sub>1"} succeeds then @{text "tac\<^sub>2"} is excluded

   584   from the result.

   585

   586   \item @{text "tac\<^sub>1"}~@{ML_op APPEND}~@{text "tac\<^sub>2"} concatenates the

   587   possible results of @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"}.  Unlike

   588   @{ML_op "ORELSE"} there is \emph{no commitment} to either tactic, so

   589   @{ML_op "APPEND"} helps to avoid incompleteness during search, at

   590   the cost of potential inefficiencies.

   591

   592   \item @{ML EVERY}~@{text "[tac\<^sub>1, \<dots>, tac\<^sub>n]"} abbreviates @{text

   593   "tac\<^sub>1"}~@{ML_op THEN}~@{text "\<dots>"}~@{ML_op THEN}~@{text "tac\<^sub>n"}.

   594   Note that @{ML "EVERY []"} is the same as @{ML all_tac}: it always

   595   succeeds.

   596

   597   \item @{ML FIRST}~@{text "[tac\<^sub>1, \<dots>, tac\<^sub>n]"} abbreviates @{text

   598   "tac\<^sub>1"}~@{ML_op ORELSE}~@{text "\<dots>"}~@{ML_op "ORELSE"}~@{text

   599   "tac\<^sub>n"}.  Note that @{ML "FIRST []"} is the same as @{ML no_tac}: it

   600   always fails.

   601

   602   \item @{ML_op "THEN'"} is the lifted version of @{ML_op "THEN"}, for

   603   tactics with explicit subgoal addressing.  So @{text

   604   "(tac\<^sub>1"}~@{ML_op THEN'}~@{text "tac\<^sub>2) i"} is the same as @{text

   605   "(tac\<^sub>1 i"}~@{ML_op THEN}~@{text "tac\<^sub>2 i)"}.

   606

   607   The other primed tacticals work analogously.

   608

   609   \end{description}

   610 \<close>

   611

   612

   613 subsection \<open>Repetition tacticals\<close>

   614

   615 text \<open>These tacticals provide further control over repetition of

   616   tactics, beyond the stylized forms of @{verbatim "?"}''  and

   617   @{verbatim "+"}'' in Isar method expressions.\<close>

   618

   619 text %mlref \<open>

   620   \begin{mldecls}

   621   @{index_ML "TRY": "tactic -> tactic"} \\

   622   @{index_ML "REPEAT": "tactic -> tactic"} \\

   623   @{index_ML "REPEAT1": "tactic -> tactic"} \\

   624   @{index_ML "REPEAT_DETERM": "tactic -> tactic"} \\

   625   @{index_ML "REPEAT_DETERM_N": "int -> tactic -> tactic"} \\

   626   \end{mldecls}

   627

   628   \begin{description}

   629

   630   \item @{ML TRY}~@{text "tac"} applies @{text "tac"} to the goal

   631   state and returns the resulting sequence, if non-empty; otherwise it

   632   returns the original state.  Thus, it applies @{text "tac"} at most

   633   once.

   634

   635   Note that for tactics with subgoal addressing, the combinator can be

   636   applied via functional composition: @{ML "TRY"}~@{ML_op o}~@{text

   637   "tac"}.  There is no need for @{verbatim TRY'}.

   638

   639   \item @{ML REPEAT}~@{text "tac"} applies @{text "tac"} to the goal

   640   state and, recursively, to each element of the resulting sequence.

   641   The resulting sequence consists of those states that make @{text

   642   "tac"} fail.  Thus, it applies @{text "tac"} as many times as

   643   possible (including zero times), and allows backtracking over each

   644   invocation of @{text "tac"}.  @{ML REPEAT} is more general than @{ML

   645   REPEAT_DETERM}, but requires more space.

   646

   647   \item @{ML REPEAT1}~@{text "tac"} is like @{ML REPEAT}~@{text "tac"}

   648   but it always applies @{text "tac"} at least once, failing if this

   649   is impossible.

   650

   651   \item @{ML REPEAT_DETERM}~@{text "tac"} applies @{text "tac"} to the

   652   goal state and, recursively, to the head of the resulting sequence.

   653   It returns the first state to make @{text "tac"} fail.  It is

   654   deterministic, discarding alternative outcomes.

   655

   656   \item @{ML REPEAT_DETERM_N}~@{text "n tac"} is like @{ML

   657   REPEAT_DETERM}~@{text "tac"} but the number of repetitions is bound

   658   by @{text "n"} (where @{ML "~1"} means @{text "\<infinity>"}).

   659

   660   \end{description}

   661 \<close>

   662

   663 text %mlex \<open>The basic tactics and tacticals considered above follow

   664   some algebraic laws:

   665

   666   \begin{itemize}

   667

   668   \item @{ML all_tac} is the identity element of the tactical @{ML_op

   669   "THEN"}.

   670

   671   \item @{ML no_tac} is the identity element of @{ML_op "ORELSE"} and

   672   @{ML_op "APPEND"}.  Also, it is a zero element for @{ML_op "THEN"},

   673   which means that @{text "tac"}~@{ML_op THEN}~@{ML no_tac} is

   674   equivalent to @{ML no_tac}.

   675

   676   \item @{ML TRY} and @{ML REPEAT} can be expressed as (recursive)

   677   functions over more basic combinators (ignoring some internal

   678   implementation tricks):

   679

   680   \end{itemize}

   681 \<close>

   682

   683 ML \<open>

   684   fun TRY tac = tac ORELSE all_tac;

   685   fun REPEAT tac st = ((tac THEN REPEAT tac) ORELSE all_tac) st;

   686 \<close>

   687

   688 text \<open>If @{text "tac"} can return multiple outcomes then so can @{ML

   689   REPEAT}~@{text "tac"}.  @{ML REPEAT} uses @{ML_op "ORELSE"} and not

   690   @{ML_op "APPEND"}, it applies @{text "tac"} as many times as

   691   possible in each outcome.

   692

   693   \begin{warn}

   694   Note the explicit abstraction over the goal state in the ML

   695   definition of @{ML REPEAT}.  Recursive tacticals must be coded in

   696   this awkward fashion to avoid infinite recursion of eager functional

   697   evaluation in Standard ML.  The following attempt would make @{ML

   698   REPEAT}~@{text "tac"} loop:

   699   \end{warn}

   700 \<close>

   701

   702 ML \<open>

   703   (*BAD -- does not terminate!*)

   704   fun REPEAT tac = (tac THEN REPEAT tac) ORELSE all_tac;

   705 \<close>

   706

   707

   708 subsection \<open>Applying tactics to subgoal ranges\<close>

   709

   710 text \<open>Tactics with explicit subgoal addressing

   711   @{ML_type "int -> tactic"} can be used together with tacticals that

   712   act like subgoal quantifiers'': guided by success of the body

   713   tactic a certain range of subgoals is covered.  Thus the body tactic

   714   is applied to \emph{all} subgoals, \emph{some} subgoal etc.

   715

   716   Suppose that the goal state has @{text "n \<ge> 0"} subgoals.  Many of

   717   these tacticals address subgoal ranges counting downwards from

   718   @{text "n"} towards @{text "1"}.  This has the fortunate effect that

   719   newly emerging subgoals are concatenated in the result, without

   720   interfering each other.  Nonetheless, there might be situations

   721   where a different order is desired.\<close>

   722

   723 text %mlref \<open>

   724   \begin{mldecls}

   725   @{index_ML ALLGOALS: "(int -> tactic) -> tactic"} \\

   726   @{index_ML SOMEGOAL: "(int -> tactic) -> tactic"} \\

   727   @{index_ML FIRSTGOAL: "(int -> tactic) -> tactic"} \\

   728   @{index_ML HEADGOAL: "(int -> tactic) -> tactic"} \\

   729   @{index_ML REPEAT_SOME: "(int -> tactic) -> tactic"} \\

   730   @{index_ML REPEAT_FIRST: "(int -> tactic) -> tactic"} \\

   731   @{index_ML RANGE: "(int -> tactic) list -> int -> tactic"} \\

   732   \end{mldecls}

   733

   734   \begin{description}

   735

   736   \item @{ML ALLGOALS}~@{text "tac"} is equivalent to @{text "tac

   737   n"}~@{ML_op THEN}~@{text "\<dots>"}~@{ML_op THEN}~@{text "tac 1"}.  It

   738   applies the @{text tac} to all the subgoals, counting downwards.

   739

   740   \item @{ML SOMEGOAL}~@{text "tac"} is equivalent to @{text "tac

   741   n"}~@{ML_op ORELSE}~@{text "\<dots>"}~@{ML_op ORELSE}~@{text "tac 1"}.  It

   742   applies @{text "tac"} to one subgoal, counting downwards.

   743

   744   \item @{ML FIRSTGOAL}~@{text "tac"} is equivalent to @{text "tac

   745   1"}~@{ML_op ORELSE}~@{text "\<dots>"}~@{ML_op ORELSE}~@{text "tac n"}.  It

   746   applies @{text "tac"} to one subgoal, counting upwards.

   747

   748   \item @{ML HEADGOAL}~@{text "tac"} is equivalent to @{text "tac 1"}.

   749   It applies @{text "tac"} unconditionally to the first subgoal.

   750

   751   \item @{ML REPEAT_SOME}~@{text "tac"} applies @{text "tac"} once or

   752   more to a subgoal, counting downwards.

   753

   754   \item @{ML REPEAT_FIRST}~@{text "tac"} applies @{text "tac"} once or

   755   more to a subgoal, counting upwards.

   756

   757   \item @{ML RANGE}~@{text "[tac\<^sub>1, \<dots>, tac\<^sub>k] i"} is equivalent to

   758   @{text "tac\<^sub>k (i + k - 1)"}~@{ML_op THEN}~@{text "\<dots>"}~@{ML_op

   759   THEN}~@{text "tac\<^sub>1 i"}.  It applies the given list of tactics to the

   760   corresponding range of subgoals, counting downwards.

   761

   762   \end{description}

   763 \<close>

   764

   765

   766 subsection \<open>Control and search tacticals\<close>

   767

   768 text \<open>A predicate on theorems @{ML_type "thm -> bool"} can test

   769   whether a goal state enjoys some desirable property --- such as

   770   having no subgoals.  Tactics that search for satisfactory goal

   771   states are easy to express.  The main search procedures,

   772   depth-first, breadth-first and best-first, are provided as

   773   tacticals.  They generate the search tree by repeatedly applying a

   774   given tactic.\<close>

   775

   776

   777 text %mlref ""

   778

   779 subsubsection \<open>Filtering a tactic's results\<close>

   780

   781 text \<open>

   782   \begin{mldecls}

   783   @{index_ML FILTER: "(thm -> bool) -> tactic -> tactic"} \\

   784   @{index_ML CHANGED: "tactic -> tactic"} \\

   785   \end{mldecls}

   786

   787   \begin{description}

   788

   789   \item @{ML FILTER}~@{text "sat tac"} applies @{text "tac"} to the

   790   goal state and returns a sequence consisting of those result goal

   791   states that are satisfactory in the sense of @{text "sat"}.

   792

   793   \item @{ML CHANGED}~@{text "tac"} applies @{text "tac"} to the goal

   794   state and returns precisely those states that differ from the

   795   original state (according to @{ML Thm.eq_thm}).  Thus @{ML

   796   CHANGED}~@{text "tac"} always has some effect on the state.

   797

   798   \end{description}

   799 \<close>

   800

   801

   802 subsubsection \<open>Depth-first search\<close>

   803

   804 text \<open>

   805   \begin{mldecls}

   806   @{index_ML DEPTH_FIRST: "(thm -> bool) -> tactic -> tactic"} \\

   807   @{index_ML DEPTH_SOLVE: "tactic -> tactic"} \\

   808   @{index_ML DEPTH_SOLVE_1: "tactic -> tactic"} \\

   809   \end{mldecls}

   810

   811   \begin{description}

   812

   813   \item @{ML DEPTH_FIRST}~@{text "sat tac"} returns the goal state if

   814   @{text "sat"} returns true.  Otherwise it applies @{text "tac"},

   815   then recursively searches from each element of the resulting

   816   sequence.  The code uses a stack for efficiency, in effect applying

   817   @{text "tac"}~@{ML_op THEN}~@{ML DEPTH_FIRST}~@{text "sat tac"} to

   818   the state.

   819

   820   \item @{ML DEPTH_SOLVE}@{text "tac"} uses @{ML DEPTH_FIRST} to

   821   search for states having no subgoals.

   822

   823   \item @{ML DEPTH_SOLVE_1}~@{text "tac"} uses @{ML DEPTH_FIRST} to

   824   search for states having fewer subgoals than the given state.  Thus,

   825   it insists upon solving at least one subgoal.

   826

   827   \end{description}

   828 \<close>

   829

   830

   831 subsubsection \<open>Other search strategies\<close>

   832

   833 text \<open>

   834   \begin{mldecls}

   835   @{index_ML BREADTH_FIRST: "(thm -> bool) -> tactic -> tactic"} \\

   836   @{index_ML BEST_FIRST: "(thm -> bool) * (thm -> int) -> tactic -> tactic"} \\

   837   @{index_ML THEN_BEST_FIRST: "tactic -> (thm -> bool) * (thm -> int) -> tactic -> tactic"} \\

   838   \end{mldecls}

   839

   840   These search strategies will find a solution if one exists.

   841   However, they do not enumerate all solutions; they terminate after

   842   the first satisfactory result from @{text "tac"}.

   843

   844   \begin{description}

   845

   846   \item @{ML BREADTH_FIRST}~@{text "sat tac"} uses breadth-first

   847   search to find states for which @{text "sat"} is true.  For most

   848   applications, it is too slow.

   849

   850   \item @{ML BEST_FIRST}~@{text "(sat, dist) tac"} does a heuristic

   851   search, using @{text "dist"} to estimate the distance from a

   852   satisfactory state (in the sense of @{text "sat"}).  It maintains a

   853   list of states ordered by distance.  It applies @{text "tac"} to the

   854   head of this list; if the result contains any satisfactory states,

   855   then it returns them.  Otherwise, @{ML BEST_FIRST} adds the new

   856   states to the list, and continues.

   857

   858   The distance function is typically @{ML size_of_thm}, which computes

   859   the size of the state.  The smaller the state, the fewer and simpler

   860   subgoals it has.

   861

   862   \item @{ML THEN_BEST_FIRST}~@{text "tac\<^sub>0 (sat, dist) tac"} is like

   863   @{ML BEST_FIRST}, except that the priority queue initially contains

   864   the result of applying @{text "tac\<^sub>0"} to the goal state.  This

   865   tactical permits separate tactics for starting the search and

   866   continuing the search.

   867

   868   \end{description}

   869 \<close>

   870

   871

   872 subsubsection \<open>Auxiliary tacticals for searching\<close>

   873

   874 text \<open>

   875   \begin{mldecls}

   876   @{index_ML COND: "(thm -> bool) -> tactic -> tactic -> tactic"} \\

   877   @{index_ML IF_UNSOLVED: "tactic -> tactic"} \\

   878   @{index_ML SOLVE: "tactic -> tactic"} \\

   879   @{index_ML DETERM: "tactic -> tactic"} \\

   880   \end{mldecls}

   881

   882   \begin{description}

   883

   884   \item @{ML COND}~@{text "sat tac\<^sub>1 tac\<^sub>2"} applies @{text "tac\<^sub>1"} to

   885   the goal state if it satisfies predicate @{text "sat"}, and applies

   886   @{text "tac\<^sub>2"}.  It is a conditional tactical in that only one of

   887   @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"} is applied to a goal state.

   888   However, both @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"} are evaluated

   889   because ML uses eager evaluation.

   890

   891   \item @{ML IF_UNSOLVED}~@{text "tac"} applies @{text "tac"} to the

   892   goal state if it has any subgoals, and simply returns the goal state

   893   otherwise.  Many common tactics, such as @{ML resolve_tac}, fail if

   894   applied to a goal state that has no subgoals.

   895

   896   \item @{ML SOLVE}~@{text "tac"} applies @{text "tac"} to the goal

   897   state and then fails iff there are subgoals left.

   898

   899   \item @{ML DETERM}~@{text "tac"} applies @{text "tac"} to the goal

   900   state and returns the head of the resulting sequence.  @{ML DETERM}

   901   limits the search space by making its argument deterministic.

   902

   903   \end{description}

   904 \<close>

   905

   906

   907 subsubsection \<open>Predicates and functions useful for searching\<close>

   908

   909 text \<open>

   910   \begin{mldecls}

   911   @{index_ML has_fewer_prems: "int -> thm -> bool"} \\

   912   @{index_ML Thm.eq_thm: "thm * thm -> bool"} \\

   913   @{index_ML Thm.eq_thm_prop: "thm * thm -> bool"} \\

   914   @{index_ML size_of_thm: "thm -> int"} \\

   915   \end{mldecls}

   916

   917   \begin{description}

   918

   919   \item @{ML has_fewer_prems}~@{text "n thm"} reports whether @{text

   920   "thm"} has fewer than @{text "n"} premises.

   921

   922   \item @{ML Thm.eq_thm}~@{text "(thm\<^sub>1, thm\<^sub>2)"} reports whether @{text

   923   "thm\<^sub>1"} and @{text "thm\<^sub>2"} are equal.  Both theorems must have the

   924   same conclusions, the same set of hypotheses, and the same set of sort

   925   hypotheses.  Names of bound variables are ignored as usual.

   926

   927   \item @{ML Thm.eq_thm_prop}~@{text "(thm\<^sub>1, thm\<^sub>2)"} reports whether

   928   the propositions of @{text "thm\<^sub>1"} and @{text "thm\<^sub>2"} are equal.

   929   Names of bound variables are ignored.

   930

   931   \item @{ML size_of_thm}~@{text "thm"} computes the size of @{text

   932   "thm"}, namely the number of variables, constants and abstractions

   933   in its conclusion.  It may serve as a distance function for

   934   @{ML BEST_FIRST}.

   935

   936   \end{description}

   937 \<close>

   938

   939 end