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