doc-src/IsarRef/Thy/document/ML_Tactic.tex
author wenzelm
Fri Oct 29 11:49:56 2010 +0200 (2010-10-29)
changeset 40255 9ffbc25e1606
parent 30172 afdf7808cfd0
child 40406 313a24b66a8d
permissions -rw-r--r--
eliminated obsolete \_ escapes in rail environments;
     1 %
     2 \begin{isabellebody}%
     3 \def\isabellecontext{ML{\isacharunderscore}Tactic}%
     4 %
     5 \isadelimtheory
     6 %
     7 \endisadelimtheory
     8 %
     9 \isatagtheory
    10 \isacommand{theory}\isamarkupfalse%
    11 \ ML{\isacharunderscore}Tactic\isanewline
    12 \isakeyword{imports}\ Main\isanewline
    13 \isakeyword{begin}%
    14 \endisatagtheory
    15 {\isafoldtheory}%
    16 %
    17 \isadelimtheory
    18 %
    19 \endisadelimtheory
    20 %
    21 \isamarkupchapter{ML tactic expressions%
    22 }
    23 \isamarkuptrue%
    24 %
    25 \begin{isamarkuptext}%
    26 Isar Proof methods closely resemble traditional tactics, when used
    27   in unstructured sequences of \hyperlink{command.apply}{\mbox{\isa{\isacommand{apply}}}} commands.
    28   Isabelle/Isar provides emulations for all major ML tactics of
    29   classic Isabelle --- mostly for the sake of easy porting of existing
    30   developments, as actual Isar proof texts would demand much less
    31   diversity of proof methods.
    32 
    33   Unlike tactic expressions in ML, Isar proof methods provide proper
    34   concrete syntax for additional arguments, options, modifiers etc.
    35   Thus a typical method text is usually more concise than the
    36   corresponding ML tactic.  Furthermore, the Isar versions of classic
    37   Isabelle tactics often cover several variant forms by a single
    38   method with separate options to tune the behavior.  For example,
    39   method \hyperlink{method.simp}{\mbox{\isa{simp}}} replaces all of \verb|simp_tac|~/ \verb|asm_simp_tac|~/ \verb|full_simp_tac|~/ \verb|asm_full_simp_tac|, there
    40   is also concrete syntax for augmenting the Simplifier context (the
    41   current ``simpset'') in a convenient way.%
    42 \end{isamarkuptext}%
    43 \isamarkuptrue%
    44 %
    45 \isamarkupsection{Resolution tactics%
    46 }
    47 \isamarkuptrue%
    48 %
    49 \begin{isamarkuptext}%
    50 Classic Isabelle provides several variant forms of tactics for
    51   single-step rule applications (based on higher-order resolution).
    52   The space of resolution tactics has the following main dimensions.
    53 
    54   \begin{enumerate}
    55 
    56   \item The ``mode'' of resolution: intro, elim, destruct, or forward
    57   (e.g.\ \verb|resolve_tac|, \verb|eresolve_tac|, \verb|dresolve_tac|,
    58   \verb|forward_tac|).
    59 
    60   \item Optional explicit instantiation (e.g.\ \verb|resolve_tac| vs.\
    61   \verb|res_inst_tac|).
    62 
    63   \item Abbreviations for singleton arguments (e.g.\ \verb|resolve_tac|
    64   vs.\ \verb|rtac|).
    65 
    66   \end{enumerate}
    67 
    68   Basically, the set of Isar tactic emulations \hyperlink{method.rule-tac}{\mbox{\isa{rule{\isacharunderscore}tac}}},
    69   \hyperlink{method.erule-tac}{\mbox{\isa{erule{\isacharunderscore}tac}}}, \hyperlink{method.drule-tac}{\mbox{\isa{drule{\isacharunderscore}tac}}}, \hyperlink{method.frule-tac}{\mbox{\isa{frule{\isacharunderscore}tac}}} (see
    70   \secref{sec:tactics}) would be sufficient to cover the four modes,
    71   either with or without instantiation, and either with single or
    72   multiple arguments.  Although it is more convenient in most cases to
    73   use the plain \hyperlink{method.rule}{\mbox{\isa{rule}}} method (see
    74   \secref{sec:pure-meth-att}), or any of its ``improper'' variants
    75   \hyperlink{method.erule}{\mbox{\isa{erule}}}, \hyperlink{method.drule}{\mbox{\isa{drule}}}, \hyperlink{method.frule}{\mbox{\isa{frule}}} (see
    76   \secref{sec:misc-meth-att}).  Note that explicit goal addressing is
    77   only supported by the actual \hyperlink{method.rule-tac}{\mbox{\isa{rule{\isacharunderscore}tac}}} version.
    78 
    79   With this in mind, plain resolution tactics correspond to Isar
    80   methods as follows.
    81 
    82   \medskip
    83   \begin{tabular}{lll}
    84     \verb|rtac|~\isa{{\isachardoublequote}a\ {\isadigit{1}}{\isachardoublequote}} & & \isa{{\isachardoublequote}rule\ a{\isachardoublequote}} \\
    85     \verb|resolve_tac|~\isa{{\isachardoublequote}{\isacharbrackleft}a\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}\ {\isadigit{1}}{\isachardoublequote}} & & \isa{{\isachardoublequote}rule\ a\isactrlsub {\isadigit{1}}\ {\isasymdots}{\isachardoublequote}} \\
    86     \verb|res_inst_tac|~\isa{{\isachardoublequote}ctxt\ {\isacharbrackleft}{\isacharparenleft}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ t\isactrlsub {\isadigit{1}}{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}\ a\ {\isadigit{1}}{\isachardoublequote}} & &
    87     \isa{{\isachardoublequote}rule{\isacharunderscore}tac\ x\isactrlsub {\isadigit{1}}\ {\isacharequal}\ t\isactrlsub {\isadigit{1}}\ {\isasymAND}\ {\isasymdots}\ {\isasymIN}\ a{\isachardoublequote}} \\[0.5ex]
    88     \verb|rtac|~\isa{{\isachardoublequote}a\ i{\isachardoublequote}} & & \isa{{\isachardoublequote}rule{\isacharunderscore}tac\ {\isacharbrackleft}i{\isacharbrackright}\ a{\isachardoublequote}} \\
    89     \verb|resolve_tac|~\isa{{\isachardoublequote}{\isacharbrackleft}a\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}\ i{\isachardoublequote}} & & \isa{{\isachardoublequote}rule{\isacharunderscore}tac\ {\isacharbrackleft}i{\isacharbrackright}\ a\isactrlsub {\isadigit{1}}\ {\isasymdots}{\isachardoublequote}} \\
    90     \verb|res_inst_tac|~\isa{{\isachardoublequote}ctxt\ {\isacharbrackleft}{\isacharparenleft}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ t\isactrlsub {\isadigit{1}}{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}\ a\ i{\isachardoublequote}} & &
    91     \isa{{\isachardoublequote}rule{\isacharunderscore}tac\ {\isacharbrackleft}i{\isacharbrackright}\ x\isactrlsub {\isadigit{1}}\ {\isacharequal}\ t\isactrlsub {\isadigit{1}}\ {\isasymAND}\ {\isasymdots}\ {\isasymIN}\ a{\isachardoublequote}} \\
    92   \end{tabular}
    93   \medskip
    94 
    95   Note that explicit goal addressing may be usually avoided by
    96   changing the order of subgoals with \hyperlink{command.defer}{\mbox{\isa{\isacommand{defer}}}} or \hyperlink{command.prefer}{\mbox{\isa{\isacommand{prefer}}}} (see \secref{sec:tactic-commands}).%
    97 \end{isamarkuptext}%
    98 \isamarkuptrue%
    99 %
   100 \isamarkupsection{Simplifier tactics%
   101 }
   102 \isamarkuptrue%
   103 %
   104 \begin{isamarkuptext}%
   105 The main Simplifier tactics \verb|simp_tac| and variants (cf.\
   106   \cite{isabelle-ref}) are all covered by the \hyperlink{method.simp}{\mbox{\isa{simp}}} and
   107   \hyperlink{method.simp-all}{\mbox{\isa{simp{\isacharunderscore}all}}} methods (see \secref{sec:simplifier}).  Note that
   108   there is no individual goal addressing available, simplification
   109   acts either on the first goal (\hyperlink{method.simp}{\mbox{\isa{simp}}}) or all goals
   110   (\hyperlink{method.simp-all}{\mbox{\isa{simp{\isacharunderscore}all}}}).
   111 
   112   \medskip
   113   \begin{tabular}{lll}
   114     \verb|asm_full_simp_tac|~\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}simpset{\isacharbraceright}\ {\isadigit{1}}{\isachardoublequote}} & & \hyperlink{method.simp}{\mbox{\isa{simp}}} \\
   115     \verb|ALLGOALS|~(\verb|asm_full_simp_tac|~\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}simpset{\isacharbraceright}{\isachardoublequote}}) & & \hyperlink{method.simp-all}{\mbox{\isa{simp{\isacharunderscore}all}}} \\[0.5ex]
   116     \verb|simp_tac|~\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}simpset{\isacharbraceright}\ {\isadigit{1}}{\isachardoublequote}} & & \hyperlink{method.simp}{\mbox{\isa{simp}}}~\isa{{\isachardoublequote}{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isachardoublequote}} \\
   117     \verb|asm_simp_tac|~\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}simpset{\isacharbraceright}\ {\isadigit{1}}{\isachardoublequote}} & & \hyperlink{method.simp}{\mbox{\isa{simp}}}~\isa{{\isachardoublequote}{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}simp{\isacharparenright}{\isachardoublequote}} \\
   118     \verb|full_simp_tac|~\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}simpset{\isacharbraceright}\ {\isadigit{1}}{\isachardoublequote}} & & \hyperlink{method.simp}{\mbox{\isa{simp}}}~\isa{{\isachardoublequote}{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}{\isachardoublequote}} \\
   119     \verb|asm_lr_simp_tac|~\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}simpset{\isacharbraceright}\ {\isadigit{1}}{\isachardoublequote}} & & \hyperlink{method.simp}{\mbox{\isa{simp}}}~\isa{{\isachardoublequote}{\isacharparenleft}asm{\isacharunderscore}lr{\isacharparenright}{\isachardoublequote}} \\
   120   \end{tabular}
   121   \medskip%
   122 \end{isamarkuptext}%
   123 \isamarkuptrue%
   124 %
   125 \isamarkupsection{Classical Reasoner tactics%
   126 }
   127 \isamarkuptrue%
   128 %
   129 \begin{isamarkuptext}%
   130 The Classical Reasoner provides a rather large number of variations
   131   of automated tactics, such as \verb|blast_tac|, \verb|fast_tac|, \verb|clarify_tac| etc.\ (see \cite{isabelle-ref}).  The corresponding
   132   Isar methods usually share the same base name, such as \hyperlink{method.blast}{\mbox{\isa{blast}}}, \hyperlink{method.fast}{\mbox{\isa{fast}}}, \hyperlink{method.clarify}{\mbox{\isa{clarify}}} etc.\ (see
   133   \secref{sec:classical}).%
   134 \end{isamarkuptext}%
   135 \isamarkuptrue%
   136 %
   137 \isamarkupsection{Miscellaneous tactics%
   138 }
   139 \isamarkuptrue%
   140 %
   141 \begin{isamarkuptext}%
   142 There are a few additional tactics defined in various theories of
   143   Isabelle/HOL, some of these also in Isabelle/FOL or Isabelle/ZF.
   144   The most common ones of these may be ported to Isar as follows.
   145 
   146   \medskip
   147   \begin{tabular}{lll}
   148     \verb|stac|~\isa{{\isachardoublequote}a\ {\isadigit{1}}{\isachardoublequote}} & & \isa{{\isachardoublequote}subst\ a{\isachardoublequote}} \\
   149     \verb|hyp_subst_tac|~\isa{{\isadigit{1}}} & & \isa{hypsubst} \\
   150     \verb|strip_tac|~\isa{{\isadigit{1}}} & \isa{{\isachardoublequote}{\isasymapprox}{\isachardoublequote}} & \isa{{\isachardoublequote}intro\ strip{\isachardoublequote}} \\
   151     \verb|split_all_tac|~\isa{{\isadigit{1}}} & & \isa{{\isachardoublequote}simp\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}simp{\isacharparenright}\ only{\isacharcolon}\ split{\isacharunderscore}tupled{\isacharunderscore}all{\isachardoublequote}} \\
   152       & \isa{{\isachardoublequote}{\isasymapprox}{\isachardoublequote}} & \isa{{\isachardoublequote}simp\ only{\isacharcolon}\ split{\isacharunderscore}tupled{\isacharunderscore}all{\isachardoublequote}} \\
   153       & \isa{{\isachardoublequote}{\isasymlless}{\isachardoublequote}} & \isa{{\isachardoublequote}clarify{\isachardoublequote}} \\
   154   \end{tabular}%
   155 \end{isamarkuptext}%
   156 \isamarkuptrue%
   157 %
   158 \isamarkupsection{Tacticals%
   159 }
   160 \isamarkuptrue%
   161 %
   162 \begin{isamarkuptext}%
   163 Classic Isabelle provides a huge amount of tacticals for combination
   164   and modification of existing tactics.  This has been greatly reduced
   165   in Isar, providing the bare minimum of combinators only: ``\isa{{\isachardoublequote}{\isacharcomma}{\isachardoublequote}}'' (sequential composition), ``\isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}}'' (alternative
   166   choices), ``\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}}'' (try), ``\isa{{\isachardoublequote}{\isacharplus}{\isachardoublequote}}'' (repeat at least
   167   once).  These are usually sufficient in practice; if all fails,
   168   arbitrary ML tactic code may be invoked via the \hyperlink{method.tactic}{\mbox{\isa{tactic}}}
   169   method (see \secref{sec:tactics}).
   170 
   171   \medskip Common ML tacticals may be expressed directly in Isar as
   172   follows:
   173 
   174   \medskip
   175   \begin{tabular}{lll}
   176     \isa{{\isachardoublequote}tac\isactrlsub {\isadigit{1}}{\isachardoublequote}}~\verb|THEN|~\isa{{\isachardoublequote}tac\isactrlsub {\isadigit{2}}{\isachardoublequote}} & & \isa{{\isachardoublequote}meth\isactrlsub {\isadigit{1}}{\isacharcomma}\ meth\isactrlsub {\isadigit{2}}{\isachardoublequote}} \\
   177     \isa{{\isachardoublequote}tac\isactrlsub {\isadigit{1}}{\isachardoublequote}}~\verb|ORELSE|~\isa{{\isachardoublequote}tac\isactrlsub {\isadigit{2}}{\isachardoublequote}} & & \isa{{\isachardoublequote}meth\isactrlsub {\isadigit{1}}\ {\isacharbar}\ meth\isactrlsub {\isadigit{2}}{\isachardoublequote}} \\
   178     \verb|TRY|~\isa{tac} & & \isa{{\isachardoublequote}meth{\isacharquery}{\isachardoublequote}} \\
   179     \verb|REPEAT1|~\isa{tac} & & \isa{{\isachardoublequote}meth{\isacharplus}{\isachardoublequote}} \\
   180     \verb|REPEAT|~\isa{tac} & & \isa{{\isachardoublequote}{\isacharparenleft}meth{\isacharplus}{\isacharparenright}{\isacharquery}{\isachardoublequote}} \\
   181     \verb|EVERY|~\isa{{\isachardoublequote}{\isacharbrackleft}tac\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}{\isachardoublequote}} & & \isa{{\isachardoublequote}meth\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isachardoublequote}} \\
   182     \verb|FIRST|~\isa{{\isachardoublequote}{\isacharbrackleft}tac\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}{\isachardoublequote}} & & \isa{{\isachardoublequote}meth\isactrlsub {\isadigit{1}}\ {\isacharbar}\ {\isasymdots}{\isachardoublequote}} \\
   183   \end{tabular}
   184   \medskip
   185 
   186   \medskip \verb|CHANGED| (see \cite{isabelle-ref}) is usually not
   187   required in Isar, since most basic proof methods already fail unless
   188   there is an actual change in the goal state.  Nevertheless, ``\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}}''  (try) may be used to accept \emph{unchanged} results as
   189   well.
   190 
   191   \medskip \verb|ALLGOALS|, \verb|SOMEGOAL| etc.\ (see
   192   \cite{isabelle-ref}) are not available in Isar, since there is no
   193   direct goal addressing.  Nevertheless, some basic methods address
   194   all goals internally, notably \hyperlink{method.simp-all}{\mbox{\isa{simp{\isacharunderscore}all}}} (see
   195   \secref{sec:simplifier}).  Also note that \verb|ALLGOALS| can be
   196   often replaced by ``\isa{{\isachardoublequote}{\isacharplus}{\isachardoublequote}}'' (repeat at least once), although
   197   this usually has a different operational behavior, such as solving
   198   goals in a different order.
   199 
   200   \medskip Iterated resolution, such as \verb|REPEAT (FIRSTGOAL|\isasep\isanewline%
   201 \verb|  (resolve_tac \<dots>))|, is usually better expressed using the \hyperlink{method.intro}{\mbox{\isa{intro}}} and \hyperlink{method.elim}{\mbox{\isa{elim}}} methods of Isar (see
   202   \secref{sec:classical}).%
   203 \end{isamarkuptext}%
   204 \isamarkuptrue%
   205 %
   206 \isadelimtheory
   207 %
   208 \endisadelimtheory
   209 %
   210 \isatagtheory
   211 \isacommand{end}\isamarkupfalse%
   212 %
   213 \endisatagtheory
   214 {\isafoldtheory}%
   215 %
   216 \isadelimtheory
   217 %
   218 \endisadelimtheory
   219 \isanewline
   220 \end{isabellebody}%
   221 %%% Local Variables:
   222 %%% mode: latex
   223 %%% TeX-master: "root"
   224 %%% End: