doc-src/IsarImplementation/Thy/document/Tactic.tex
author wenzelm
Thu, 26 Jan 2012 21:16:11 +0100
changeset 46267 bc9479cada96
parent 46266 a9694a4e39e5
child 46269 e75181672150
permissions -rw-r--r--
moved HEADGOAL; added RANGE;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
     1
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
     2
\begin{isabellebody}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
     3
\def\isabellecontext{Tactic}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
     4
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
     5
\isadelimtheory
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
     6
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
     7
\endisadelimtheory
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
     8
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
     9
\isatagtheory
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    10
\isacommand{theory}\isamarkupfalse%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    11
\ Tactic\isanewline
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    12
\isakeyword{imports}\ Base\isanewline
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    13
\isakeyword{begin}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    14
\endisatagtheory
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    15
{\isafoldtheory}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    16
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    17
\isadelimtheory
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    18
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    19
\endisadelimtheory
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    20
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    21
\isamarkupchapter{Tactical reasoning%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    22
}
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    23
\isamarkuptrue%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    24
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    25
\begin{isamarkuptext}%
35001
31f8d9eaceff updated generated files;
wenzelm
parents: 32201
diff changeset
    26
Tactical reasoning works by refining an initial claim in a
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    27
  backwards fashion, until a solved form is reached.  A \isa{goal}
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    28
  consists of several subgoals that need to be solved in order to
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    29
  achieve the main statement; zero subgoals means that the proof may
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    30
  be finished.  A \isa{tactic} is a refinement operation that maps
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    31
  a goal to a lazy sequence of potential successors.  A \isa{tactical} is a combinator for composing tactics.%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    32
\end{isamarkuptext}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    33
\isamarkuptrue%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    34
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    35
\isamarkupsection{Goals \label{sec:tactical-goals}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    36
}
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    37
\isamarkuptrue%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    38
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    39
\begin{isamarkuptext}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    40
Isabelle/Pure represents a goal as a theorem stating that the
40406
313a24b66a8d updated generated files;
wenzelm
parents: 39885
diff changeset
    41
  subgoals imply the main goal: \isa{A\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C}.  The outermost goal structure is that of a Horn Clause: i.e.\
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    42
  an iterated implication without any quantifiers\footnote{Recall that
40406
313a24b66a8d updated generated files;
wenzelm
parents: 39885
diff changeset
    43
  outermost \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}} is always represented via schematic
313a24b66a8d updated generated files;
wenzelm
parents: 39885
diff changeset
    44
  variables in the body: \isa{{\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}x{\isaliteral{5D}{\isacharbrackright}}}.  These variables may get
313a24b66a8d updated generated files;
wenzelm
parents: 39885
diff changeset
    45
  instantiated during the course of reasoning.}.  For \isa{n\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}}
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    46
  a goal is called ``solved''.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    47
40406
313a24b66a8d updated generated files;
wenzelm
parents: 39885
diff changeset
    48
  The structure of each subgoal \isa{A\isaliteral{5C3C5E7375623E}{}\isactrlsub i} is that of a
313a24b66a8d updated generated files;
wenzelm
parents: 39885
diff changeset
    49
  general Hereditary Harrop Formula \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub k{\isaliteral{2E}{\isachardot}}\ H\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ H\isaliteral{5C3C5E7375623E}{}\isactrlsub m\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B}.  Here \isa{x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub k} are goal parameters, i.e.\
313a24b66a8d updated generated files;
wenzelm
parents: 39885
diff changeset
    50
  arbitrary-but-fixed entities of certain types, and \isa{H\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ H\isaliteral{5C3C5E7375623E}{}\isactrlsub m} are goal hypotheses, i.e.\ facts that may
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    51
  be assumed locally.  Together, this forms the goal context of the
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    52
  conclusion \isa{B} to be established.  The goal hypotheses may be
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    53
  again arbitrary Hereditary Harrop Formulas, although the level of
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    54
  nesting rarely exceeds 1--2 in practice.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    55
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    56
  The main conclusion \isa{C} is internally marked as a protected
40406
313a24b66a8d updated generated files;
wenzelm
parents: 39885
diff changeset
    57
  proposition, which is represented explicitly by the notation \isa{{\isaliteral{23}{\isacharhash}}C} here.  This ensures that the decomposition into subgoals and
35001
31f8d9eaceff updated generated files;
wenzelm
parents: 32201
diff changeset
    58
  main conclusion is well-defined for arbitrarily structured claims.
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    59
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    60
  \medskip Basic goal management is performed via the following
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    61
  Isabelle/Pure rules:
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    62
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    63
  \[
40406
313a24b66a8d updated generated files;
wenzelm
parents: 39885
diff changeset
    64
  \infer[\isa{{\isaliteral{28}{\isacharparenleft}}init{\isaliteral{29}{\isacharparenright}}}]{\isa{C\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{23}{\isacharhash}}C}}{} \qquad
313a24b66a8d updated generated files;
wenzelm
parents: 39885
diff changeset
    65
  \infer[\isa{{\isaliteral{28}{\isacharparenleft}}finish{\isaliteral{29}{\isacharparenright}}}]{\isa{C}}{\isa{{\isaliteral{23}{\isacharhash}}C}}
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    66
  \]
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    67
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    68
  \medskip The following low-level variants admit general reasoning
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    69
  with protected propositions:
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    70
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    71
  \[
40406
313a24b66a8d updated generated files;
wenzelm
parents: 39885
diff changeset
    72
  \infer[\isa{{\isaliteral{28}{\isacharparenleft}}protect{\isaliteral{29}{\isacharparenright}}}]{\isa{{\isaliteral{23}{\isacharhash}}C}}{\isa{C}} \qquad
313a24b66a8d updated generated files;
wenzelm
parents: 39885
diff changeset
    73
  \infer[\isa{{\isaliteral{28}{\isacharparenleft}}conclude{\isaliteral{29}{\isacharparenright}}}]{\isa{A\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C}}{\isa{A\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{23}{\isacharhash}}C}}
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    74
  \]%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    75
\end{isamarkuptext}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    76
\isamarkuptrue%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    77
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    78
\isadelimmlref
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    79
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    80
\endisadelimmlref
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    81
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    82
\isatagmlref
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    83
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    84
\begin{isamarkuptext}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    85
\begin{mldecls}
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    86
  \indexdef{}{ML}{Goal.init}\verb|Goal.init: cterm -> thm| \\
32201
3689b647356d updated Variable.focus, SUBPROOF, Obtain.result, Goal.finish;
wenzelm
parents: 30296
diff changeset
    87
  \indexdef{}{ML}{Goal.finish}\verb|Goal.finish: Proof.context -> thm -> thm| \\
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    88
  \indexdef{}{ML}{Goal.protect}\verb|Goal.protect: thm -> thm| \\
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    89
  \indexdef{}{ML}{Goal.conclude}\verb|Goal.conclude: thm -> thm| \\
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    90
  \end{mldecls}
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    91
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    92
  \begin{description}
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    93
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    94
  \item \verb|Goal.init|~\isa{C} initializes a tactical goal from
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    95
  the well-formed proposition \isa{C}.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    96
32201
3689b647356d updated Variable.focus, SUBPROOF, Obtain.result, Goal.finish;
wenzelm
parents: 30296
diff changeset
    97
  \item \verb|Goal.finish|~\isa{ctxt\ thm} checks whether theorem
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
    98
  \isa{thm} is a solved goal (no subgoals), and concludes the
32201
3689b647356d updated Variable.focus, SUBPROOF, Obtain.result, Goal.finish;
wenzelm
parents: 30296
diff changeset
    99
  result by removing the goal protection.  The context is only
3689b647356d updated Variable.focus, SUBPROOF, Obtain.result, Goal.finish;
wenzelm
parents: 30296
diff changeset
   100
  required for printing error messages.
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   101
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   102
  \item \verb|Goal.protect|~\isa{thm} protects the full statement
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   103
  of theorem \isa{thm}.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   104
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   105
  \item \verb|Goal.conclude|~\isa{thm} removes the goal
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   106
  protection, even if there are pending subgoals.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   107
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   108
  \end{description}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   109
\end{isamarkuptext}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   110
\isamarkuptrue%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   111
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   112
\endisatagmlref
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   113
{\isafoldmlref}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   114
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   115
\isadelimmlref
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   116
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   117
\endisadelimmlref
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   118
%
39885
6a3f7941c3a0 cumulative update of generated files (since bf164c153d10);
wenzelm
parents: 35001
diff changeset
   119
\isamarkupsection{Tactics\label{sec:tactics}%
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   120
}
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   121
\isamarkuptrue%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   122
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   123
\begin{isamarkuptext}%
40406
313a24b66a8d updated generated files;
wenzelm
parents: 39885
diff changeset
   124
A \isa{tactic} is a function \isa{goal\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ goal\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}} that
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   125
  maps a given goal state (represented as a theorem, cf.\
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   126
  \secref{sec:tactical-goals}) to a lazy sequence of potential
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   127
  successor states.  The underlying sequence implementation is lazy
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   128
  both in head and tail, and is purely functional in \emph{not}
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   129
  supporting memoing.\footnote{The lack of memoing and the strict
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   130
  nature of SML requires some care when working with low-level
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   131
  sequence operations, to avoid duplicate or premature evaluation of
35001
31f8d9eaceff updated generated files;
wenzelm
parents: 32201
diff changeset
   132
  results.  It also means that modified runtime behavior, such as
31f8d9eaceff updated generated files;
wenzelm
parents: 32201
diff changeset
   133
  timeout, is very hard to achieve for general tactics.}
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   134
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   135
  An \emph{empty result sequence} means that the tactic has failed: in
35001
31f8d9eaceff updated generated files;
wenzelm
parents: 32201
diff changeset
   136
  a compound tactic expression other tactics might be tried instead,
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   137
  or the whole refinement step might fail outright, producing a
35001
31f8d9eaceff updated generated files;
wenzelm
parents: 32201
diff changeset
   138
  toplevel error message in the end.  When implementing tactics from
31f8d9eaceff updated generated files;
wenzelm
parents: 32201
diff changeset
   139
  scratch, one should take care to observe the basic protocol of
31f8d9eaceff updated generated files;
wenzelm
parents: 32201
diff changeset
   140
  mapping regular error conditions to an empty result; only serious
31f8d9eaceff updated generated files;
wenzelm
parents: 32201
diff changeset
   141
  faults should emerge as exceptions.
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   142
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   143
  By enumerating \emph{multiple results}, a tactic can easily express
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   144
  the potential outcome of an internal search process.  There are also
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   145
  combinators for building proof tools that involve search
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   146
  systematically, see also \secref{sec:tacticals}.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   147
35001
31f8d9eaceff updated generated files;
wenzelm
parents: 32201
diff changeset
   148
  \medskip As explained before, a goal state essentially consists of a
31f8d9eaceff updated generated files;
wenzelm
parents: 32201
diff changeset
   149
  list of subgoals that imply the main goal (conclusion).  Tactics may
31f8d9eaceff updated generated files;
wenzelm
parents: 32201
diff changeset
   150
  operate on all subgoals or on a particularly specified subgoal, but
31f8d9eaceff updated generated files;
wenzelm
parents: 32201
diff changeset
   151
  must not change the main conclusion (apart from instantiating
31f8d9eaceff updated generated files;
wenzelm
parents: 32201
diff changeset
   152
  schematic goal variables).
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   153
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   154
  Tactics with explicit \emph{subgoal addressing} are of the form
40406
313a24b66a8d updated generated files;
wenzelm
parents: 39885
diff changeset
   155
  \isa{int\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ tactic} and may be applied to a particular subgoal
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   156
  (counting from 1).  If the subgoal number is out of range, the
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   157
  tactic should fail with an empty result sequence, but must not raise
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   158
  an exception!
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   159
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   160
  Operating on a particular subgoal means to replace it by an interval
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   161
  of zero or more subgoals in the same place; other subgoals must not
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   162
  be affected, apart from instantiating schematic variables ranging
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   163
  over the whole goal state.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   164
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   165
  A common pattern of composing tactics with subgoal addressing is to
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   166
  try the first one, and then the second one only if the subgoal has
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   167
  not been solved yet.  Special care is required here to avoid bumping
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   168
  into unrelated subgoals that happen to come after the original
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   169
  subgoal.  Assuming that there is only a single initial subgoal is a
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   170
  very common error when implementing tactics!
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   171
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   172
  Tactics with internal subgoal addressing should expose the subgoal
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   173
  index as \isa{int} argument in full generality; a hardwired
35001
31f8d9eaceff updated generated files;
wenzelm
parents: 32201
diff changeset
   174
  subgoal 1 is not acceptable.
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   175
  
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   176
  \medskip The main well-formedness conditions for proper tactics are
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   177
  summarized as follows.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   178
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   179
  \begin{itemize}
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   180
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   181
  \item General tactic failure is indicated by an empty result, only
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   182
  serious faults may produce an exception.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   183
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   184
  \item The main conclusion must not be changed, apart from
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   185
  instantiating schematic variables.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   186
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   187
  \item A tactic operates either uniformly on all subgoals, or
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   188
  specifically on a selected subgoal (without bumping into unrelated
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   189
  subgoals).
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   190
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   191
  \item Range errors in subgoal addressing produce an empty result.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   192
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   193
  \end{itemize}
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   194
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   195
  Some of these conditions are checked by higher-level goal
35001
31f8d9eaceff updated generated files;
wenzelm
parents: 32201
diff changeset
   196
  infrastructure (\secref{sec:struct-goals}); others are not checked
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   197
  explicitly, and violating them merely results in ill-behaved tactics
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   198
  experienced by the user (e.g.\ tactics that insist in being
35001
31f8d9eaceff updated generated files;
wenzelm
parents: 32201
diff changeset
   199
  applicable only to singleton goals, or prevent composition via
46260
wenzelm
parents: 46259
diff changeset
   200
  standard tacticals such as \verb|REPEAT|).%
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   201
\end{isamarkuptext}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   202
\isamarkuptrue%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   203
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   204
\isadelimmlref
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   205
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   206
\endisadelimmlref
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   207
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   208
\isatagmlref
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   209
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   210
\begin{isamarkuptext}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   211
\begin{mldecls}
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   212
  \indexdef{}{ML type}{tactic}\verb|type tactic = thm -> thm Seq.seq| \\
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   213
  \indexdef{}{ML}{no\_tac}\verb|no_tac: tactic| \\
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   214
  \indexdef{}{ML}{all\_tac}\verb|all_tac: tactic| \\
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   215
  \indexdef{}{ML}{print\_tac}\verb|print_tac: string -> tactic| \\[1ex]
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   216
  \indexdef{}{ML}{PRIMITIVE}\verb|PRIMITIVE: (thm -> thm) -> tactic| \\[1ex]
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   217
  \indexdef{}{ML}{SUBGOAL}\verb|SUBGOAL: (term * int -> tactic) -> int -> tactic| \\
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   218
  \indexdef{}{ML}{CSUBGOAL}\verb|CSUBGOAL: (cterm * int -> tactic) -> int -> tactic| \\
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   219
  \end{mldecls}
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   220
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   221
  \begin{description}
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   222
39885
6a3f7941c3a0 cumulative update of generated files (since bf164c153d10);
wenzelm
parents: 35001
diff changeset
   223
  \item Type \verb|tactic| represents tactics.  The
6a3f7941c3a0 cumulative update of generated files (since bf164c153d10);
wenzelm
parents: 35001
diff changeset
   224
  well-formedness conditions described above need to be observed.  See
40802
3cd23f676c5b updated generated files;
wenzelm
parents: 40406
diff changeset
   225
  also \verb|~~/src/Pure/General/seq.ML| for the underlying
39885
6a3f7941c3a0 cumulative update of generated files (since bf164c153d10);
wenzelm
parents: 35001
diff changeset
   226
  implementation of lazy sequences.
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   227
39885
6a3f7941c3a0 cumulative update of generated files (since bf164c153d10);
wenzelm
parents: 35001
diff changeset
   228
  \item Type \verb|int -> tactic| represents tactics with
6a3f7941c3a0 cumulative update of generated files (since bf164c153d10);
wenzelm
parents: 35001
diff changeset
   229
  explicit subgoal addressing, with well-formedness conditions as
6a3f7941c3a0 cumulative update of generated files (since bf164c153d10);
wenzelm
parents: 35001
diff changeset
   230
  described above.
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   231
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   232
  \item \verb|no_tac| is a tactic that always fails, returning the
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   233
  empty sequence.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   234
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   235
  \item \verb|all_tac| is a tactic that always succeeds, returning a
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   236
  singleton sequence with unchanged goal state.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   237
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   238
  \item \verb|print_tac|~\isa{message} is like \verb|all_tac|, but
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   239
  prints a message together with the goal state on the tracing
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   240
  channel.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   241
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   242
  \item \verb|PRIMITIVE|~\isa{rule} turns a primitive inference rule
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   243
  into a tactic with unique result.  Exception \verb|THM| is considered
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   244
  a regular tactic failure and produces an empty result; other
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   245
  exceptions are passed through.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   246
40406
313a24b66a8d updated generated files;
wenzelm
parents: 39885
diff changeset
   247
  \item \verb|SUBGOAL|~\isa{{\isaliteral{28}{\isacharparenleft}}fn\ {\isaliteral{28}{\isacharparenleft}}subgoal{\isaliteral{2C}{\isacharcomma}}\ i{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ tactic{\isaliteral{29}{\isacharparenright}}} is the
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   248
  most basic form to produce a tactic with subgoal addressing.  The
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   249
  given abstraction over the subgoal term and subgoal number allows to
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   250
  peek at the relevant information of the full goal state.  The
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   251
  subgoal range is checked as required above.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   252
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   253
  \item \verb|CSUBGOAL| is similar to \verb|SUBGOAL|, but passes the
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   254
  subgoal as \verb|cterm| instead of raw \verb|term|.  This
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   255
  avoids expensive re-certification in situations where the subgoal is
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   256
  used directly for primitive inferences.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   257
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   258
  \end{description}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   259
\end{isamarkuptext}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   260
\isamarkuptrue%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   261
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   262
\endisatagmlref
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   263
{\isafoldmlref}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   264
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   265
\isadelimmlref
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   266
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   267
\endisadelimmlref
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   268
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   269
\isamarkupsubsection{Resolution and assumption tactics \label{sec:resolve-assume-tac}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   270
}
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   271
\isamarkuptrue%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   272
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   273
\begin{isamarkuptext}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   274
\emph{Resolution} is the most basic mechanism for refining a
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   275
  subgoal using a theorem as object-level rule.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   276
  \emph{Elim-resolution} is particularly suited for elimination rules:
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   277
  it resolves with a rule, proves its first premise by assumption, and
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   278
  finally deletes that assumption from any new subgoals.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   279
  \emph{Destruct-resolution} is like elim-resolution, but the given
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   280
  destruction rules are first turned into canonical elimination
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   281
  format.  \emph{Forward-resolution} is like destruct-resolution, but
40406
313a24b66a8d updated generated files;
wenzelm
parents: 39885
diff changeset
   282
  without deleting the selected assumption.  The \isa{r{\isaliteral{2F}{\isacharslash}}e{\isaliteral{2F}{\isacharslash}}d{\isaliteral{2F}{\isacharslash}}f}
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   283
  naming convention is maintained for several different kinds of
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   284
  resolution rules and tactics.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   285
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   286
  Assumption tactics close a subgoal by unifying some of its premises
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   287
  against its conclusion.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   288
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   289
  \medskip All the tactics in this section operate on a subgoal
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   290
  designated by a positive integer.  Other subgoals might be affected
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   291
  indirectly, due to instantiation of schematic variables.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   292
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   293
  There are various sources of non-determinism, the tactic result
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   294
  sequence enumerates all possibilities of the following choices (if
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   295
  applicable):
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   297
  \begin{enumerate}
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   298
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   299
  \item selecting one of the rules given as argument to the tactic;
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   300
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   301
  \item selecting a subgoal premise to eliminate, unifying it against
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   302
  the first premise of the rule;
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   303
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   304
  \item unifying the conclusion of the subgoal to the conclusion of
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   305
  the rule.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   306
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   307
  \end{enumerate}
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   308
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   309
  Recall that higher-order unification may produce multiple results
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   310
  that are enumerated here.%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   311
\end{isamarkuptext}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   312
\isamarkuptrue%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   313
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   314
\isadelimmlref
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   315
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   316
\endisadelimmlref
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   317
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   318
\isatagmlref
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   319
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   320
\begin{isamarkuptext}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   321
\begin{mldecls}
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   322
  \indexdef{}{ML}{resolve\_tac}\verb|resolve_tac: thm list -> int -> tactic| \\
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   323
  \indexdef{}{ML}{eresolve\_tac}\verb|eresolve_tac: thm list -> int -> tactic| \\
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   324
  \indexdef{}{ML}{dresolve\_tac}\verb|dresolve_tac: thm list -> int -> tactic| \\
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   325
  \indexdef{}{ML}{forward\_tac}\verb|forward_tac: thm list -> int -> tactic| \\[1ex]
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   326
  \indexdef{}{ML}{assume\_tac}\verb|assume_tac: int -> tactic| \\
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   327
  \indexdef{}{ML}{eq\_assume\_tac}\verb|eq_assume_tac: int -> tactic| \\[1ex]
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   328
  \indexdef{}{ML}{match\_tac}\verb|match_tac: thm list -> int -> tactic| \\
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   329
  \indexdef{}{ML}{ematch\_tac}\verb|ematch_tac: thm list -> int -> tactic| \\
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   330
  \indexdef{}{ML}{dmatch\_tac}\verb|dmatch_tac: thm list -> int -> tactic| \\
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   331
  \end{mldecls}
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   332
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   333
  \begin{description}
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   334
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   335
  \item \verb|resolve_tac|~\isa{thms\ i} refines the goal state
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   336
  using the given theorems, which should normally be introduction
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   337
  rules.  The tactic resolves a rule's conclusion with subgoal \isa{i}, replacing it by the corresponding versions of the rule's
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   338
  premises.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   339
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   340
  \item \verb|eresolve_tac|~\isa{thms\ i} performs elim-resolution
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   341
  with the given theorems, which should normally be elimination rules.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   342
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   343
  \item \verb|dresolve_tac|~\isa{thms\ i} performs
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   344
  destruct-resolution with the given theorems, which should normally
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   345
  be destruction rules.  This replaces an assumption by the result of
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   346
  applying one of the rules.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   347
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   348
  \item \verb|forward_tac| is like \verb|dresolve_tac| except that the
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   349
  selected assumption is not deleted.  It applies a rule to an
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   350
  assumption, adding the result as a new assumption.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   351
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   352
  \item \verb|assume_tac|~\isa{i} attempts to solve subgoal \isa{i}
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   353
  by assumption (modulo higher-order unification).
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   354
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   355
  \item \verb|eq_assume_tac| is similar to \verb|assume_tac|, but checks
40406
313a24b66a8d updated generated files;
wenzelm
parents: 39885
diff changeset
   356
  only for immediate \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}}-convertibility instead of using
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   357
  unification.  It succeeds (with a unique next state) if one of the
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   358
  assumptions is equal to the subgoal's conclusion.  Since it does not
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   359
  instantiate variables, it cannot make other subgoals unprovable.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   360
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   361
  \item \verb|match_tac|, \verb|ematch_tac|, and \verb|dmatch_tac| are
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   362
  similar to \verb|resolve_tac|, \verb|eresolve_tac|, and \verb|dresolve_tac|, respectively, but do not instantiate schematic
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   363
  variables in the goal state.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   364
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   365
  Flexible subgoals are not updated at will, but are left alone.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   366
  Strictly speaking, matching means to treat the unknowns in the goal
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   367
  state as constants; these tactics merely discard unifiers that would
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   368
  update the goal state.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   369
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   370
  \end{description}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   371
\end{isamarkuptext}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   372
\isamarkuptrue%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   373
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   374
\endisatagmlref
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   375
{\isafoldmlref}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   376
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   377
\isadelimmlref
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   378
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   379
\endisadelimmlref
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   380
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   381
\isamarkupsubsection{Explicit instantiation within a subgoal context%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   382
}
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   383
\isamarkuptrue%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   384
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   385
\begin{isamarkuptext}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   386
The main resolution tactics (\secref{sec:resolve-assume-tac})
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   387
  use higher-order unification, which works well in many practical
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   388
  situations despite its daunting theoretical properties.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   389
  Nonetheless, there are important problem classes where unguided
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   390
  higher-order unification is not so useful.  This typically involves
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   391
  rules like universal elimination, existential introduction, or
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   392
  equational substitution.  Here the unification problem involves
40406
313a24b66a8d updated generated files;
wenzelm
parents: 39885
diff changeset
   393
  fully flexible \isa{{\isaliteral{3F}{\isacharquery}}P\ {\isaliteral{3F}{\isacharquery}}x} schemes, which are hard to manage
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   394
  without further hints.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   395
40406
313a24b66a8d updated generated files;
wenzelm
parents: 39885
diff changeset
   396
  By providing a (small) rigid term for \isa{{\isaliteral{3F}{\isacharquery}}x} explicitly, the
313a24b66a8d updated generated files;
wenzelm
parents: 39885
diff changeset
   397
  remaining unification problem is to assign a (large) term to \isa{{\isaliteral{3F}{\isacharquery}}P}, according to the shape of the given subgoal.  This is
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   398
  sufficiently well-behaved in most practical situations.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   399
40406
313a24b66a8d updated generated files;
wenzelm
parents: 39885
diff changeset
   400
  \medskip Isabelle provides separate versions of the standard \isa{r{\isaliteral{2F}{\isacharslash}}e{\isaliteral{2F}{\isacharslash}}d{\isaliteral{2F}{\isacharslash}}f} resolution tactics that allow to provide explicit
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   401
  instantiations of unknowns of the given rule, wrt.\ terms that refer
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   402
  to the implicit context of the selected subgoal.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   403
40406
313a24b66a8d updated generated files;
wenzelm
parents: 39885
diff changeset
   404
  An instantiation consists of a list of pairs of the form \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{3F}{\isacharquery}}x{\isaliteral{2C}{\isacharcomma}}\ t{\isaliteral{29}{\isacharparenright}}}, where \isa{{\isaliteral{3F}{\isacharquery}}x} is a schematic variable occurring in
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   405
  the given rule, and \isa{t} is a term from the current proof
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   406
  context, augmented by the local goal parameters of the selected
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   407
  subgoal; cf.\ the \isa{focus} operation described in
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   408
  \secref{sec:variables}.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   409
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   410
  Entering the syntactic context of a subgoal is a brittle operation,
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   411
  because its exact form is somewhat accidental, and the choice of
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   412
  bound variable names depends on the presence of other local and
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   413
  global names.  Explicit renaming of subgoal parameters prior to
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   414
  explicit instantiation might help to achieve a bit more robustness.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   415
40406
313a24b66a8d updated generated files;
wenzelm
parents: 39885
diff changeset
   416
  Type instantiations may be given as well, via pairs like \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{29}{\isacharparenright}}}.  Type instantiations are distinguished from term
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   417
  instantiations by the syntactic form of the schematic variable.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   418
  Types are instantiated before terms are.  Since term instantiation
35001
31f8d9eaceff updated generated files;
wenzelm
parents: 32201
diff changeset
   419
  already performs simple type-inference, so explicit type
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   420
  instantiations are seldom necessary.%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   421
\end{isamarkuptext}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   422
\isamarkuptrue%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   423
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   424
\isadelimmlref
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   425
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   426
\endisadelimmlref
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   427
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   428
\isatagmlref
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   429
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   430
\begin{isamarkuptext}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   431
\begin{mldecls}
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   432
  \indexdef{}{ML}{res\_inst\_tac}\verb|res_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic| \\
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   433
  \indexdef{}{ML}{eres\_inst\_tac}\verb|eres_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic| \\
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   434
  \indexdef{}{ML}{dres\_inst\_tac}\verb|dres_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic| \\
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   435
  \indexdef{}{ML}{forw\_inst\_tac}\verb|forw_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic| \\[1ex]
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   436
  \indexdef{}{ML}{rename\_tac}\verb|rename_tac: string list -> int -> tactic| \\
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   437
  \end{mldecls}
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   438
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   439
  \begin{description}
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   440
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   441
  \item \verb|res_inst_tac|~\isa{ctxt\ insts\ thm\ i} instantiates the
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   442
  rule \isa{thm} with the instantiations \isa{insts}, as described
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   443
  above, and then performs resolution on subgoal \isa{i}.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   444
  
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   445
  \item \verb|eres_inst_tac| is like \verb|res_inst_tac|, but performs
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   446
  elim-resolution.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   447
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   448
  \item \verb|dres_inst_tac| is like \verb|res_inst_tac|, but performs
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   449
  destruct-resolution.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   450
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   451
  \item \verb|forw_inst_tac| is like \verb|dres_inst_tac| except that
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   452
  the selected assumption is not deleted.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   453
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   454
  \item \verb|rename_tac|~\isa{names\ i} renames the innermost
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   455
  parameters of subgoal \isa{i} according to the provided \isa{names} (which need to be distinct indentifiers).
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   456
35001
31f8d9eaceff updated generated files;
wenzelm
parents: 32201
diff changeset
   457
  \end{description}
31f8d9eaceff updated generated files;
wenzelm
parents: 32201
diff changeset
   458
31f8d9eaceff updated generated files;
wenzelm
parents: 32201
diff changeset
   459
  For historical reasons, the above instantiation tactics take
31f8d9eaceff updated generated files;
wenzelm
parents: 32201
diff changeset
   460
  unparsed string arguments, which makes them hard to use in general
31f8d9eaceff updated generated files;
wenzelm
parents: 32201
diff changeset
   461
  ML code.  The slightly more advanced \verb|Subgoal.FOCUS| combinator
31f8d9eaceff updated generated files;
wenzelm
parents: 32201
diff changeset
   462
  of \secref{sec:struct-goals} allows to refer to internal goal
31f8d9eaceff updated generated files;
wenzelm
parents: 32201
diff changeset
   463
  structure with explicit context management.%
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   464
\end{isamarkuptext}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   465
\isamarkuptrue%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   466
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   467
\endisatagmlref
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   468
{\isafoldmlref}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   469
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   470
\isadelimmlref
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   471
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   472
\endisadelimmlref
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   473
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   474
\isamarkupsection{Tacticals \label{sec:tacticals}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   475
}
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   476
\isamarkuptrue%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   477
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   478
\begin{isamarkuptext}%
46258
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   479
A \emph{tactical} is a functional combinator for building up
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   480
  complex tactics from simpler ones.  Common tacticals perform
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   481
  sequential composition, disjunctive choice, iteration, or goal
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   482
  addressing.  Various search strategies may be expressed via
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   483
  tacticals.
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   484
46258
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   485
  \medskip The chapter on tacticals in old \cite{isabelle-ref} is
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   486
  still applicable for further details.%
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   487
\end{isamarkuptext}%
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   488
\isamarkuptrue%
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   489
%
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   490
\isamarkupsubsection{Combining tactics%
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   491
}
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   492
\isamarkuptrue%
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   493
%
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   494
\begin{isamarkuptext}%
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   495
Sequential composition and alternative choices are the most
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   496
  basic ways to combine tactics, similarly to ``\verb|,|'' and
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   497
  ``\verb||\verb,|,\verb||'' in Isar method notation.  This corresponds to
46262
912b42e64fde tuned ML infixes;
wenzelm
parents: 46260
diff changeset
   498
  \verb|THEN| and \verb|ORELSE| in ML, but there are further
912b42e64fde tuned ML infixes;
wenzelm
parents: 46260
diff changeset
   499
  possibilities for fine-tuning alternation of tactics such as \verb|APPEND|.  Further details become visible in ML due to explicit
46258
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   500
  subgoal addressing.%
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   501
\end{isamarkuptext}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   502
\isamarkuptrue%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   503
%
46258
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   504
\isadelimmlref
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   505
%
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   506
\endisadelimmlref
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   507
%
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   508
\isatagmlref
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   509
%
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   510
\begin{isamarkuptext}%
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   511
\begin{mldecls}
46262
912b42e64fde tuned ML infixes;
wenzelm
parents: 46260
diff changeset
   512
  \indexdef{}{ML infix}{THEN}\verb|infix THEN: tactic * tactic -> tactic| \\
912b42e64fde tuned ML infixes;
wenzelm
parents: 46260
diff changeset
   513
  \indexdef{}{ML infix}{ORELSE}\verb|infix ORELSE: tactic * tactic -> tactic| \\
912b42e64fde tuned ML infixes;
wenzelm
parents: 46260
diff changeset
   514
  \indexdef{}{ML infix}{APPEND}\verb|infix APPEND: tactic * tactic -> tactic| \\
46258
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   515
  \indexdef{}{ML}{EVERY}\verb|EVERY: tactic list -> tactic| \\
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   516
  \indexdef{}{ML}{FIRST}\verb|FIRST: tactic list -> tactic| \\[0.5ex]
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   517
46262
912b42e64fde tuned ML infixes;
wenzelm
parents: 46260
diff changeset
   518
  \indexdef{}{ML infix}{THEN'}\verb|infix THEN': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic| \\
912b42e64fde tuned ML infixes;
wenzelm
parents: 46260
diff changeset
   519
  \indexdef{}{ML infix}{ORELSE'}\verb|infix ORELSE': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic| \\
912b42e64fde tuned ML infixes;
wenzelm
parents: 46260
diff changeset
   520
  \indexdef{}{ML infix}{APPEND'}\verb|infix APPEND': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic| \\
46258
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   521
  \indexdef{}{ML}{EVERY'}\verb|EVERY': ('a -> tactic) list -> 'a -> tactic| \\
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   522
  \indexdef{}{ML}{FIRST'}\verb|FIRST': ('a -> tactic) list -> 'a -> tactic| \\
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   523
  \end{mldecls}
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   524
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   525
  \begin{description}
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   526
46262
912b42e64fde tuned ML infixes;
wenzelm
parents: 46260
diff changeset
   527
  \item \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}}~\verb|THEN|~\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} is the sequential
912b42e64fde tuned ML infixes;
wenzelm
parents: 46260
diff changeset
   528
  composition of \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}.  Applied to a
912b42e64fde tuned ML infixes;
wenzelm
parents: 46260
diff changeset
   529
  proof state, it returns all states reachable in two steps by
912b42e64fde tuned ML infixes;
wenzelm
parents: 46260
diff changeset
   530
  applying \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} followed by \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}.  First, it
912b42e64fde tuned ML infixes;
wenzelm
parents: 46260
diff changeset
   531
  applies \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} to the proof state, getting a sequence of
912b42e64fde tuned ML infixes;
wenzelm
parents: 46260
diff changeset
   532
  possible next states; then, it applies \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} to each of
912b42e64fde tuned ML infixes;
wenzelm
parents: 46260
diff changeset
   533
  these and concatenates the results to produce again one flat
912b42e64fde tuned ML infixes;
wenzelm
parents: 46260
diff changeset
   534
  sequence of states.
46258
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   535
46262
912b42e64fde tuned ML infixes;
wenzelm
parents: 46260
diff changeset
   536
  \item \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}}~\verb|ORELSE|~\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} makes a choice
912b42e64fde tuned ML infixes;
wenzelm
parents: 46260
diff changeset
   537
  between \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}.  Applied to a state, it
912b42e64fde tuned ML infixes;
wenzelm
parents: 46260
diff changeset
   538
  tries \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and returns the result if non-empty; if \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} fails then it uses \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}.  This is a deterministic
912b42e64fde tuned ML infixes;
wenzelm
parents: 46260
diff changeset
   539
  choice: if \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} succeeds then \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} is excluded
912b42e64fde tuned ML infixes;
wenzelm
parents: 46260
diff changeset
   540
  from the result.
46258
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   541
46262
912b42e64fde tuned ML infixes;
wenzelm
parents: 46260
diff changeset
   542
  \item \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}}~\verb|APPEND|~\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} concatenates the
912b42e64fde tuned ML infixes;
wenzelm
parents: 46260
diff changeset
   543
  possible results of \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}.  Unlike
912b42e64fde tuned ML infixes;
wenzelm
parents: 46260
diff changeset
   544
  \verb|ORELSE| there is \emph{no commitment} to either tactic, so
912b42e64fde tuned ML infixes;
wenzelm
parents: 46260
diff changeset
   545
  \verb|APPEND| helps to avoid incompleteness during search, at
912b42e64fde tuned ML infixes;
wenzelm
parents: 46260
diff changeset
   546
  the cost of potential inefficiencies.
46258
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   547
46262
912b42e64fde tuned ML infixes;
wenzelm
parents: 46260
diff changeset
   548
  \item \verb|EVERY|~\isa{{\isaliteral{5B}{\isacharbrackleft}}tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{5D}{\isacharbrackright}}} abbreviates \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}}~\verb|THEN|~\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}~\verb|THEN|~\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub n}.
912b42e64fde tuned ML infixes;
wenzelm
parents: 46260
diff changeset
   549
  Note that \verb|EVERY []| is the same as \verb|all_tac|: it always
912b42e64fde tuned ML infixes;
wenzelm
parents: 46260
diff changeset
   550
  succeeds.
46258
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   551
46262
912b42e64fde tuned ML infixes;
wenzelm
parents: 46260
diff changeset
   552
  \item \verb|FIRST|~\isa{{\isaliteral{5B}{\isacharbrackleft}}tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{5D}{\isacharbrackright}}} abbreviates \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}}~\verb|ORELSE|~\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}~\verb|ORELSE|~\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub n}.  Note that \verb|FIRST []| is the same as \verb|no_tac|: it
912b42e64fde tuned ML infixes;
wenzelm
parents: 46260
diff changeset
   553
  always fails.
46258
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   554
46264
wenzelm
parents: 46263
diff changeset
   555
  \item \verb|THEN'| is the lifted version of \verb|THEN|, for
46266
a9694a4e39e5 removed some obscure material;
wenzelm
parents: 46264
diff changeset
   556
  tactics with explicit subgoal addressing.  So \isa{{\isaliteral{28}{\isacharparenleft}}tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}}~\verb|THEN'|~\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ i} is the same as \isa{{\isaliteral{28}{\isacharparenleft}}tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ i}~\verb|THEN|~\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}\ i{\isaliteral{29}{\isacharparenright}}}.
46258
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   557
46264
wenzelm
parents: 46263
diff changeset
   558
  The other primed tacticals work analogously.
46258
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   559
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   560
  \end{description}%
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   561
\end{isamarkuptext}%
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   562
\isamarkuptrue%
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   563
%
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   564
\endisatagmlref
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   565
{\isafoldmlref}%
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   566
%
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   567
\isadelimmlref
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   568
%
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   569
\endisadelimmlref
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   570
%
46259
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   571
\isamarkupsubsection{Repetition tacticals%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   572
}
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   573
\isamarkuptrue%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   574
%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   575
\begin{isamarkuptext}%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   576
These tacticals provide further control over repetition of
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   577
  tactics, beyond the stylized forms of ``\verb|?|''  and
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   578
  ``\verb|+|'' in Isar method expressions.%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   579
\end{isamarkuptext}%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   580
\isamarkuptrue%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   581
%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   582
\isadelimmlref
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   583
%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   584
\endisadelimmlref
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   585
%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   586
\isatagmlref
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   587
%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   588
\begin{isamarkuptext}%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   589
\begin{mldecls}
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   590
  \indexdef{}{ML}{TRY}\verb|TRY: tactic -> tactic| \\
46266
a9694a4e39e5 removed some obscure material;
wenzelm
parents: 46264
diff changeset
   591
  \indexdef{}{ML}{REPEAT}\verb|REPEAT: tactic -> tactic| \\
a9694a4e39e5 removed some obscure material;
wenzelm
parents: 46264
diff changeset
   592
  \indexdef{}{ML}{REPEAT1}\verb|REPEAT1: tactic -> tactic| \\
46259
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   593
  \indexdef{}{ML}{REPEAT\_DETERM}\verb|REPEAT_DETERM: tactic -> tactic| \\
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   594
  \indexdef{}{ML}{REPEAT\_DETERM\_N}\verb|REPEAT_DETERM_N: int -> tactic -> tactic| \\
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   595
  \end{mldecls}
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   596
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   597
  \begin{description}
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   598
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   599
  \item \verb|TRY|~\isa{tac} applies \isa{tac} to the proof
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   600
  state and returns the resulting sequence, if non-empty; otherwise it
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   601
  returns the original state.  Thus, it applies \isa{tac} at most
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   602
  once.
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   603
46266
a9694a4e39e5 removed some obscure material;
wenzelm
parents: 46264
diff changeset
   604
  Note that for tactics with subgoal addressing, the combinator can be
a9694a4e39e5 removed some obscure material;
wenzelm
parents: 46264
diff changeset
   605
  applied via functional composition: \verb|TRY|~\verb|o|~\isa{tac}.  There is no need for \verb|TRY'|.
46259
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   606
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   607
  \item \verb|REPEAT|~\isa{tac} applies \isa{tac} to the proof
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   608
  state and, recursively, to each element of the resulting sequence.
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   609
  The resulting sequence consists of those states that make \isa{tac} fail.  Thus, it applies \isa{tac} as many times as
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   610
  possible (including zero times), and allows backtracking over each
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   611
  invocation of \isa{tac}.  \verb|REPEAT| is more general than \verb|REPEAT_DETERM|, but requires more space.
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   612
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   613
  \item \verb|REPEAT1|~\isa{tac} is like \verb|REPEAT|~\isa{tac}
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   614
  but it always applies \isa{tac} at least once, failing if this
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   615
  is impossible.
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   616
46266
a9694a4e39e5 removed some obscure material;
wenzelm
parents: 46264
diff changeset
   617
  \item \verb|REPEAT_DETERM|~\isa{tac} applies \isa{tac} to the
a9694a4e39e5 removed some obscure material;
wenzelm
parents: 46264
diff changeset
   618
  proof state and, recursively, to the head of the resulting sequence.
a9694a4e39e5 removed some obscure material;
wenzelm
parents: 46264
diff changeset
   619
  It returns the first state to make \isa{tac} fail.  It is
a9694a4e39e5 removed some obscure material;
wenzelm
parents: 46264
diff changeset
   620
  deterministic, discarding alternative outcomes.
a9694a4e39e5 removed some obscure material;
wenzelm
parents: 46264
diff changeset
   621
a9694a4e39e5 removed some obscure material;
wenzelm
parents: 46264
diff changeset
   622
  \item \verb|REPEAT_DETERM_N|~\isa{n\ tac} is like \verb|REPEAT_DETERM|~\isa{tac} but the number of repetitions is bound
a9694a4e39e5 removed some obscure material;
wenzelm
parents: 46264
diff changeset
   623
  by \isa{n} (where \verb|~1| means \isa{{\isaliteral{5C3C696E66696E6974793E}{\isasyminfinity}}}).
46259
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   624
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   625
  \end{description}%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   626
\end{isamarkuptext}%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   627
\isamarkuptrue%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   628
%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   629
\endisatagmlref
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   630
{\isafoldmlref}%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   631
%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   632
\isadelimmlref
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   633
%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   634
\endisadelimmlref
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   635
%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   636
\isadelimmlex
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   637
%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   638
\endisadelimmlex
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   639
%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   640
\isatagmlex
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   641
%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   642
\begin{isamarkuptext}%
46260
wenzelm
parents: 46259
diff changeset
   643
The basic tactics and tacticals considered above follow
wenzelm
parents: 46259
diff changeset
   644
  some algebraic laws:
wenzelm
parents: 46259
diff changeset
   645
wenzelm
parents: 46259
diff changeset
   646
  \begin{itemize}
wenzelm
parents: 46259
diff changeset
   647
46262
912b42e64fde tuned ML infixes;
wenzelm
parents: 46260
diff changeset
   648
  \item \verb|all_tac| is the identity element of the tactical \verb|THEN|.
46260
wenzelm
parents: 46259
diff changeset
   649
46262
912b42e64fde tuned ML infixes;
wenzelm
parents: 46260
diff changeset
   650
  \item \verb|no_tac| is the identity element of \verb|ORELSE| and
912b42e64fde tuned ML infixes;
wenzelm
parents: 46260
diff changeset
   651
  \verb|APPEND|.  Also, it is a zero element for \verb|THEN|,
912b42e64fde tuned ML infixes;
wenzelm
parents: 46260
diff changeset
   652
  which means that \isa{tac}~\verb|THEN|~\verb|no_tac| is
912b42e64fde tuned ML infixes;
wenzelm
parents: 46260
diff changeset
   653
  equivalent to \verb|no_tac|.
46260
wenzelm
parents: 46259
diff changeset
   654
wenzelm
parents: 46259
diff changeset
   655
  \item \verb|TRY| and \verb|REPEAT| can be expressed as (recursive)
wenzelm
parents: 46259
diff changeset
   656
  functions over more basic combinators (ignoring some internal
wenzelm
parents: 46259
diff changeset
   657
  implementation tricks):
wenzelm
parents: 46259
diff changeset
   658
wenzelm
parents: 46259
diff changeset
   659
  \end{itemize}%
46259
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   660
\end{isamarkuptext}%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   661
\isamarkuptrue%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   662
%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   663
\endisatagmlex
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   664
{\isafoldmlex}%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   665
%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   666
\isadelimmlex
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   667
%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   668
\endisadelimmlex
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   669
%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   670
\isadelimML
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   671
%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   672
\endisadelimML
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   673
%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   674
\isatagML
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   675
\isacommand{ML}\isamarkupfalse%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   676
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   677
\ \ fun\ TRY\ tac\ {\isaliteral{3D}{\isacharequal}}\ tac\ ORELSE\ all{\isaliteral{5F}{\isacharunderscore}}tac{\isaliteral{3B}{\isacharsemicolon}}\isanewline
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   678
\ \ fun\ REPEAT\ tac\ st\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}tac\ THEN\ REPEAT\ tac{\isaliteral{29}{\isacharparenright}}\ ORELSE\ all{\isaliteral{5F}{\isacharunderscore}}tac{\isaliteral{29}{\isacharparenright}}\ st{\isaliteral{3B}{\isacharsemicolon}}\isanewline
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   679
{\isaliteral{2A7D}{\isacharverbatimclose}}%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   680
\endisatagML
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   681
{\isafoldML}%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   682
%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   683
\isadelimML
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   684
%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   685
\endisadelimML
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   686
%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   687
\begin{isamarkuptext}%
46262
912b42e64fde tuned ML infixes;
wenzelm
parents: 46260
diff changeset
   688
If \isa{tac} can return multiple outcomes then so can \verb|REPEAT|~\isa{tac}.  \verb|REPEAT| uses \verb|ORELSE| and not
912b42e64fde tuned ML infixes;
wenzelm
parents: 46260
diff changeset
   689
  \verb|APPEND|, it applies \isa{tac} as many times as
46259
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   690
  possible in each outcome.
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   691
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   692
  \begin{warn}
46260
wenzelm
parents: 46259
diff changeset
   693
  Note the explicit abstraction over the proof state in the ML
wenzelm
parents: 46259
diff changeset
   694
  definition of \verb|REPEAT|.  Recursive tacticals must be coded in
wenzelm
parents: 46259
diff changeset
   695
  this awkward fashion to avoid infinite recursion of eager functional
wenzelm
parents: 46259
diff changeset
   696
  evaluation in Standard ML.  The following attempt would make \verb|REPEAT|~\isa{tac} loop:
46259
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   697
  \end{warn}%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   698
\end{isamarkuptext}%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   699
\isamarkuptrue%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   700
%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   701
\isadelimML
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   702
%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   703
\endisadelimML
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   704
%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   705
\isatagML
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   706
\isacommand{ML}\isamarkupfalse%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   707
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
46260
wenzelm
parents: 46259
diff changeset
   708
\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}BAD\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}\ does\ not\ terminate{\isaliteral{21}{\isacharbang}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm
parents: 46259
diff changeset
   709
\ \ fun\ REPEAT\ tac\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}tac\ THEN\ REPEAT\ tac{\isaliteral{29}{\isacharparenright}}\ ORELSE\ all{\isaliteral{5F}{\isacharunderscore}}tac{\isaliteral{3B}{\isacharsemicolon}}\isanewline
46259
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   710
{\isaliteral{2A7D}{\isacharverbatimclose}}%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   711
\endisatagML
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   712
{\isafoldML}%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   713
%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   714
\isadelimML
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   715
%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   716
\endisadelimML
46263
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   717
%
46267
bc9479cada96 moved HEADGOAL;
wenzelm
parents: 46266
diff changeset
   718
\isamarkupsubsection{Applying tactics to subgoal ranges%
46263
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   719
}
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   720
\isamarkuptrue%
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   721
%
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   722
\begin{isamarkuptext}%
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   723
Tactics with explicit subgoal addressing
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   724
  \verb|int -> tactic| can be used together with tacticals that
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   725
  act like ``subgoal quantifiers'': guided by success of the body
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   726
  tactic a certain range of subgoals is covered.  Thus the body tactic
46267
bc9479cada96 moved HEADGOAL;
wenzelm
parents: 46266
diff changeset
   727
  is applied to \emph{all} subgoals, \emph{some} subgoal etc.
46263
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   728
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   729
  Suppose that the goal state has \isa{n\ {\isaliteral{5C3C67653E}{\isasymge}}\ {\isadigit{0}}} subgoals.  Many of
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   730
  these tacticals address subgoal ranges counting downwards from
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   731
  \isa{n} towards \isa{{\isadigit{1}}}.  This has the fortunate effect that
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   732
  newly emerging subgoals are concatenated in the result, without
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   733
  interfering each other.  Nonetheless, there might be situations
46266
a9694a4e39e5 removed some obscure material;
wenzelm
parents: 46264
diff changeset
   734
  where a different order is desired.%
46263
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   735
\end{isamarkuptext}%
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   736
\isamarkuptrue%
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   737
%
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   738
\isadelimmlref
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   739
%
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   740
\endisadelimmlref
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   741
%
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   742
\isatagmlref
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   743
%
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   744
\begin{isamarkuptext}%
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   745
\begin{mldecls}
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   746
  \indexdef{}{ML}{ALLGOALS}\verb|ALLGOALS: (int -> tactic) -> tactic| \\
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   747
  \indexdef{}{ML}{SOMEGOAL}\verb|SOMEGOAL: (int -> tactic) -> tactic| \\
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   748
  \indexdef{}{ML}{FIRSTGOAL}\verb|FIRSTGOAL: (int -> tactic) -> tactic| \\
46267
bc9479cada96 moved HEADGOAL;
wenzelm
parents: 46266
diff changeset
   749
  \indexdef{}{ML}{HEADGOAL}\verb|HEADGOAL: (int -> tactic) -> tactic| \\
46263
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   750
  \indexdef{}{ML}{REPEAT\_SOME}\verb|REPEAT_SOME: (int -> tactic) -> tactic| \\
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   751
  \indexdef{}{ML}{REPEAT\_FIRST}\verb|REPEAT_FIRST: (int -> tactic) -> tactic| \\
46267
bc9479cada96 moved HEADGOAL;
wenzelm
parents: 46266
diff changeset
   752
  \indexdef{}{ML}{RANGE}\verb|RANGE: (int -> tactic) list -> int -> tactic| \\
46263
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   753
  \end{mldecls}
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   754
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   755
  \begin{description}
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   756
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   757
  \item \verb|ALLGOALS|~\isa{tac} is equivalent to \isa{tac\ n}~\verb|THEN|~\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}~\verb|THEN|~\isa{tac\ {\isadigit{1}}}.  It
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   758
  applies the \isa{tac} to all the subgoals, counting downwards.
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   759
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   760
  \item \verb|SOMEGOAL|~\isa{tac} is equivalent to \isa{tac\ n}~\verb|ORELSE|~\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}~\verb|ORELSE|~\isa{tac\ {\isadigit{1}}}.  It
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   761
  applies \isa{tac} to one subgoal, counting downwards.
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   762
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   763
  \item \verb|FIRSTGOAL|~\isa{tac} is equivalent to \isa{tac\ {\isadigit{1}}}~\verb|ORELSE|~\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}~\verb|ORELSE|~\isa{tac\ n}.  It
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   764
  applies \isa{tac} to one subgoal, counting upwards.
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   765
46267
bc9479cada96 moved HEADGOAL;
wenzelm
parents: 46266
diff changeset
   766
  \item \verb|HEADGOAL|~\isa{tac} is equivalent to \isa{tac\ {\isadigit{1}}}.
bc9479cada96 moved HEADGOAL;
wenzelm
parents: 46266
diff changeset
   767
  It applies \isa{tac} unconditionally to the first subgoal.
bc9479cada96 moved HEADGOAL;
wenzelm
parents: 46266
diff changeset
   768
46263
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   769
  \item \verb|REPEAT_SOME|~\isa{tac} applies \isa{tac} once or
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   770
  more to a subgoal, counting downwards.
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   771
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   772
  \item \verb|REPEAT_FIRST|~\isa{tac} applies \isa{tac} once or
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   773
  more to a subgoal, counting upwards.
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   774
46267
bc9479cada96 moved HEADGOAL;
wenzelm
parents: 46266
diff changeset
   775
  \item \verb|RANGE|~\isa{{\isaliteral{5B}{\isacharbrackleft}}tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub k{\isaliteral{5D}{\isacharbrackright}}\ i} is equivalent to
bc9479cada96 moved HEADGOAL;
wenzelm
parents: 46266
diff changeset
   776
  \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub k\ {\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{2B}{\isacharplus}}\ k\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}}~\verb|THEN|~\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}~\verb|THEN|~\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ i}.  It applies the given list of tactics to the
bc9479cada96 moved HEADGOAL;
wenzelm
parents: 46266
diff changeset
   777
  corresponding range of subgoals, counting downwards.
bc9479cada96 moved HEADGOAL;
wenzelm
parents: 46266
diff changeset
   778
46263
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   779
  \end{description}%
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   780
\end{isamarkuptext}%
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   781
\isamarkuptrue%
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   782
%
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   783
\endisatagmlref
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   784
{\isafoldmlref}%
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   785
%
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   786
\isadelimmlref
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   787
%
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   788
\endisadelimmlref
46259
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   789
%
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   790
\isadelimtheory
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   791
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   792
\endisadelimtheory
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   793
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   794
\isatagtheory
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   795
\isacommand{end}\isamarkupfalse%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   796
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   797
\endisatagtheory
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   798
{\isafoldtheory}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   799
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   800
\isadelimtheory
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   801
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   802
\endisadelimtheory
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   803
\isanewline
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   804
\end{isabellebody}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   805
%%% Local Variables:
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   806
%%% mode: latex
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   807
%%% TeX-master: "root"
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   808
%%% End: