doc-src/IsarImplementation/Thy/document/Tactic.tex
author wenzelm
Sun, 29 Jan 2012 22:12:25 +0100
changeset 46278 408e3acfdbb9
parent 46277 aea65ff733b4
permissions -rw-r--r--
updated hint about asm_rl;
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
46278
408e3acfdbb9 updated hint about asm_rl;
wenzelm
parents: 46277
diff changeset
   341
  with the given theorems, which are normally be elimination rules.
408e3acfdbb9 updated hint about asm_rl;
wenzelm
parents: 46277
diff changeset
   342
408e3acfdbb9 updated hint about asm_rl;
wenzelm
parents: 46277
diff changeset
   343
  Note that \verb|eresolve_tac [asm_rl]| is equivalent to \verb|assume_tac|, which facilitates mixing of assumption steps with
408e3acfdbb9 updated hint about asm_rl;
wenzelm
parents: 46277
diff changeset
   344
  genuine eliminations.
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   345
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   346
  \item \verb|dresolve_tac|~\isa{thms\ i} performs
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   347
  destruct-resolution with the given theorems, which should normally
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   348
  be destruction rules.  This replaces an assumption by the result of
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   349
  applying one of the rules.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   350
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   351
  \item \verb|forward_tac| is like \verb|dresolve_tac| except that the
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   352
  selected assumption is not deleted.  It applies a rule to an
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   353
  assumption, adding the result as a new assumption.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   354
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   355
  \item \verb|assume_tac|~\isa{i} attempts to solve subgoal \isa{i}
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   356
  by assumption (modulo higher-order unification).
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   357
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   358
  \item \verb|eq_assume_tac| is similar to \verb|assume_tac|, but checks
40406
313a24b66a8d updated generated files;
wenzelm
parents: 39885
diff changeset
   359
  only for immediate \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}}-convertibility instead of using
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   360
  unification.  It succeeds (with a unique next state) if one of the
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   361
  assumptions is equal to the subgoal's conclusion.  Since it does not
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   362
  instantiate variables, it cannot make other subgoals unprovable.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   363
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   364
  \item \verb|match_tac|, \verb|ematch_tac|, and \verb|dmatch_tac| are
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   365
  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
   366
  variables in the goal state.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   367
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   368
  Flexible subgoals are not updated at will, but are left alone.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   369
  Strictly speaking, matching means to treat the unknowns in the goal
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   370
  state as constants; these tactics merely discard unifiers that would
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   371
  update the goal state.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   372
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   373
  \end{description}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   374
\end{isamarkuptext}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   375
\isamarkuptrue%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   376
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   377
\endisatagmlref
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   378
{\isafoldmlref}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   379
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   380
\isadelimmlref
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   381
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   382
\endisadelimmlref
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   383
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   384
\isamarkupsubsection{Explicit instantiation within a subgoal context%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   385
}
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   386
\isamarkuptrue%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   387
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   388
\begin{isamarkuptext}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   389
The main resolution tactics (\secref{sec:resolve-assume-tac})
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   390
  use higher-order unification, which works well in many practical
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   391
  situations despite its daunting theoretical properties.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   392
  Nonetheless, there are important problem classes where unguided
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   393
  higher-order unification is not so useful.  This typically involves
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   394
  rules like universal elimination, existential introduction, or
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   395
  equational substitution.  Here the unification problem involves
40406
313a24b66a8d updated generated files;
wenzelm
parents: 39885
diff changeset
   396
  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
   397
  without further hints.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   398
40406
313a24b66a8d updated generated files;
wenzelm
parents: 39885
diff changeset
   399
  By providing a (small) rigid term for \isa{{\isaliteral{3F}{\isacharquery}}x} explicitly, the
313a24b66a8d updated generated files;
wenzelm
parents: 39885
diff changeset
   400
  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
   401
  sufficiently well-behaved in most practical situations.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   402
40406
313a24b66a8d updated generated files;
wenzelm
parents: 39885
diff changeset
   403
  \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
   404
  instantiations of unknowns of the given rule, wrt.\ terms that refer
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   405
  to the implicit context of the selected subgoal.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   406
40406
313a24b66a8d updated generated files;
wenzelm
parents: 39885
diff changeset
   407
  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
   408
  the given rule, and \isa{t} is a term from the current proof
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   409
  context, augmented by the local goal parameters of the selected
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   410
  subgoal; cf.\ the \isa{focus} operation described in
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   411
  \secref{sec:variables}.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   412
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   413
  Entering the syntactic context of a subgoal is a brittle operation,
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   414
  because its exact form is somewhat accidental, and the choice of
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   415
  bound variable names depends on the presence of other local and
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   416
  global names.  Explicit renaming of subgoal parameters prior to
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   417
  explicit instantiation might help to achieve a bit more robustness.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   418
40406
313a24b66a8d updated generated files;
wenzelm
parents: 39885
diff changeset
   419
  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
   420
  instantiations by the syntactic form of the schematic variable.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   421
  Types are instantiated before terms are.  Since term instantiation
35001
31f8d9eaceff updated generated files;
wenzelm
parents: 32201
diff changeset
   422
  already performs simple type-inference, so explicit type
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   423
  instantiations are seldom necessary.%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   424
\end{isamarkuptext}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   425
\isamarkuptrue%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   426
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   427
\isadelimmlref
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   428
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   429
\endisadelimmlref
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   430
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   431
\isatagmlref
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   432
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   433
\begin{isamarkuptext}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   434
\begin{mldecls}
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   435
  \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
   436
  \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
   437
  \indexdef{}{ML}{dres\_inst\_tac}\verb|dres_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic| \\
46271
e1b5460f1725 updated subgoal_tac;
wenzelm
parents: 46270
diff changeset
   438
  \indexdef{}{ML}{forw\_inst\_tac}\verb|forw_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic| \\
e1b5460f1725 updated subgoal_tac;
wenzelm
parents: 46270
diff changeset
   439
  \indexdef{}{ML}{subgoal\_tac}\verb|subgoal_tac: Proof.context -> string -> int -> tactic| \\
46277
aea65ff733b4 updated thin_tac;
wenzelm
parents: 46276
diff changeset
   440
  \indexdef{}{ML}{thin\_tac}\verb|thin_tac: Proof.context -> string -> int -> tactic| \\
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   441
  \indexdef{}{ML}{rename\_tac}\verb|rename_tac: string list -> int -> tactic| \\
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   442
  \end{mldecls}
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   443
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   444
  \begin{description}
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   445
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   446
  \item \verb|res_inst_tac|~\isa{ctxt\ insts\ thm\ i} instantiates the
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   447
  rule \isa{thm} with the instantiations \isa{insts}, as described
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   448
  above, and then performs resolution on subgoal \isa{i}.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   449
  
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   450
  \item \verb|eres_inst_tac| is like \verb|res_inst_tac|, but performs
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   451
  elim-resolution.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   452
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   453
  \item \verb|dres_inst_tac| is like \verb|res_inst_tac|, but performs
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   454
  destruct-resolution.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   455
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   456
  \item \verb|forw_inst_tac| is like \verb|dres_inst_tac| except that
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   457
  the selected assumption is not deleted.
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   458
46271
e1b5460f1725 updated subgoal_tac;
wenzelm
parents: 46270
diff changeset
   459
  \item \verb|subgoal_tac|~\isa{ctxt\ {\isaliteral{5C3C7068693E}{\isasymphi}}\ i} adds the proposition
e1b5460f1725 updated subgoal_tac;
wenzelm
parents: 46270
diff changeset
   460
  \isa{{\isaliteral{5C3C7068693E}{\isasymphi}}} as local premise to subgoal \isa{i}, and poses the
e1b5460f1725 updated subgoal_tac;
wenzelm
parents: 46270
diff changeset
   461
  same as a new subgoal \isa{i\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}} (in the original context).
e1b5460f1725 updated subgoal_tac;
wenzelm
parents: 46270
diff changeset
   462
46277
aea65ff733b4 updated thin_tac;
wenzelm
parents: 46276
diff changeset
   463
  \item \verb|thin_tac|~\isa{ctxt\ {\isaliteral{5C3C7068693E}{\isasymphi}}\ i} deletes the specified
aea65ff733b4 updated thin_tac;
wenzelm
parents: 46276
diff changeset
   464
  premise from subgoal \isa{i}.  Note that \isa{{\isaliteral{5C3C7068693E}{\isasymphi}}} may contain
aea65ff733b4 updated thin_tac;
wenzelm
parents: 46276
diff changeset
   465
  schematic variables, to abbreviate the intended proposition; the
aea65ff733b4 updated thin_tac;
wenzelm
parents: 46276
diff changeset
   466
  first matching subgoal premise will be deleted.  Removing useless
aea65ff733b4 updated thin_tac;
wenzelm
parents: 46276
diff changeset
   467
  premises from a subgoal increases its readability and can make
aea65ff733b4 updated thin_tac;
wenzelm
parents: 46276
diff changeset
   468
  search tactics run faster.
aea65ff733b4 updated thin_tac;
wenzelm
parents: 46276
diff changeset
   469
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   470
  \item \verb|rename_tac|~\isa{names\ i} renames the innermost
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   471
  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
   472
35001
31f8d9eaceff updated generated files;
wenzelm
parents: 32201
diff changeset
   473
  \end{description}
31f8d9eaceff updated generated files;
wenzelm
parents: 32201
diff changeset
   474
31f8d9eaceff updated generated files;
wenzelm
parents: 32201
diff changeset
   475
  For historical reasons, the above instantiation tactics take
31f8d9eaceff updated generated files;
wenzelm
parents: 32201
diff changeset
   476
  unparsed string arguments, which makes them hard to use in general
31f8d9eaceff updated generated files;
wenzelm
parents: 32201
diff changeset
   477
  ML code.  The slightly more advanced \verb|Subgoal.FOCUS| combinator
31f8d9eaceff updated generated files;
wenzelm
parents: 32201
diff changeset
   478
  of \secref{sec:struct-goals} allows to refer to internal goal
31f8d9eaceff updated generated files;
wenzelm
parents: 32201
diff changeset
   479
  structure with explicit context management.%
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   480
\end{isamarkuptext}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   481
\isamarkuptrue%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   482
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   483
\endisatagmlref
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   484
{\isafoldmlref}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   485
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   486
\isadelimmlref
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   487
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   488
\endisadelimmlref
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   489
%
46274
67139209b548 updated rotate_tac;
wenzelm
parents: 46271
diff changeset
   490
\isamarkupsubsection{Rearranging goal states%
67139209b548 updated rotate_tac;
wenzelm
parents: 46271
diff changeset
   491
}
67139209b548 updated rotate_tac;
wenzelm
parents: 46271
diff changeset
   492
\isamarkuptrue%
67139209b548 updated rotate_tac;
wenzelm
parents: 46271
diff changeset
   493
%
67139209b548 updated rotate_tac;
wenzelm
parents: 46271
diff changeset
   494
\begin{isamarkuptext}%
67139209b548 updated rotate_tac;
wenzelm
parents: 46271
diff changeset
   495
In rare situations there is a need to rearrange goal states:
67139209b548 updated rotate_tac;
wenzelm
parents: 46271
diff changeset
   496
  either the overall collection of subgoals, or the local structure of
67139209b548 updated rotate_tac;
wenzelm
parents: 46271
diff changeset
   497
  a subgoal.  Various administrative tactics allow to operate on the
67139209b548 updated rotate_tac;
wenzelm
parents: 46271
diff changeset
   498
  concrete presentation these conceptual sets of formulae.%
67139209b548 updated rotate_tac;
wenzelm
parents: 46271
diff changeset
   499
\end{isamarkuptext}%
67139209b548 updated rotate_tac;
wenzelm
parents: 46271
diff changeset
   500
\isamarkuptrue%
67139209b548 updated rotate_tac;
wenzelm
parents: 46271
diff changeset
   501
%
67139209b548 updated rotate_tac;
wenzelm
parents: 46271
diff changeset
   502
\isadelimmlref
67139209b548 updated rotate_tac;
wenzelm
parents: 46271
diff changeset
   503
%
67139209b548 updated rotate_tac;
wenzelm
parents: 46271
diff changeset
   504
\endisadelimmlref
67139209b548 updated rotate_tac;
wenzelm
parents: 46271
diff changeset
   505
%
67139209b548 updated rotate_tac;
wenzelm
parents: 46271
diff changeset
   506
\isatagmlref
67139209b548 updated rotate_tac;
wenzelm
parents: 46271
diff changeset
   507
%
67139209b548 updated rotate_tac;
wenzelm
parents: 46271
diff changeset
   508
\begin{isamarkuptext}%
67139209b548 updated rotate_tac;
wenzelm
parents: 46271
diff changeset
   509
\begin{mldecls}
67139209b548 updated rotate_tac;
wenzelm
parents: 46271
diff changeset
   510
  \indexdef{}{ML}{rotate\_tac}\verb|rotate_tac: int -> int -> tactic| \\
46276
8f1f33faf24e updated distinct_subgoals_tac, flexflex_tac;
wenzelm
parents: 46274
diff changeset
   511
  \indexdef{}{ML}{distinct\_subgoals\_tac}\verb|distinct_subgoals_tac: tactic| \\
8f1f33faf24e updated distinct_subgoals_tac, flexflex_tac;
wenzelm
parents: 46274
diff changeset
   512
  \indexdef{}{ML}{flexflex\_tac}\verb|flexflex_tac: tactic| \\
46274
67139209b548 updated rotate_tac;
wenzelm
parents: 46271
diff changeset
   513
  \end{mldecls}
67139209b548 updated rotate_tac;
wenzelm
parents: 46271
diff changeset
   514
67139209b548 updated rotate_tac;
wenzelm
parents: 46271
diff changeset
   515
  \begin{description}
67139209b548 updated rotate_tac;
wenzelm
parents: 46271
diff changeset
   516
67139209b548 updated rotate_tac;
wenzelm
parents: 46271
diff changeset
   517
  \item \verb|rotate_tac|~\isa{n\ i} rotates the premises of subgoal
67139209b548 updated rotate_tac;
wenzelm
parents: 46271
diff changeset
   518
  \isa{i} by \isa{n} positions: from right to left if \isa{n} is
67139209b548 updated rotate_tac;
wenzelm
parents: 46271
diff changeset
   519
  positive, and from left to right if \isa{n} is negative.
67139209b548 updated rotate_tac;
wenzelm
parents: 46271
diff changeset
   520
46276
8f1f33faf24e updated distinct_subgoals_tac, flexflex_tac;
wenzelm
parents: 46274
diff changeset
   521
  \item \verb|distinct_subgoals_tac| removes duplicate subgoals from a
8f1f33faf24e updated distinct_subgoals_tac, flexflex_tac;
wenzelm
parents: 46274
diff changeset
   522
  proof state.  This is potentially inefficient.
8f1f33faf24e updated distinct_subgoals_tac, flexflex_tac;
wenzelm
parents: 46274
diff changeset
   523
8f1f33faf24e updated distinct_subgoals_tac, flexflex_tac;
wenzelm
parents: 46274
diff changeset
   524
  \item \verb|flexflex_tac| removes all flex-flex pairs from the proof
8f1f33faf24e updated distinct_subgoals_tac, flexflex_tac;
wenzelm
parents: 46274
diff changeset
   525
  state by applying the trivial unifier.  This drastic step loses
8f1f33faf24e updated distinct_subgoals_tac, flexflex_tac;
wenzelm
parents: 46274
diff changeset
   526
  information.  It is already part of the Isar infrastructure for
8f1f33faf24e updated distinct_subgoals_tac, flexflex_tac;
wenzelm
parents: 46274
diff changeset
   527
  facts resulting from goals, and rarely needs to be invoked manually.
8f1f33faf24e updated distinct_subgoals_tac, flexflex_tac;
wenzelm
parents: 46274
diff changeset
   528
8f1f33faf24e updated distinct_subgoals_tac, flexflex_tac;
wenzelm
parents: 46274
diff changeset
   529
  Flex-flex constraints arise from difficult cases of higher-order
8f1f33faf24e updated distinct_subgoals_tac, flexflex_tac;
wenzelm
parents: 46274
diff changeset
   530
  unification.  To prevent this, use \verb|res_inst_tac| to instantiate
8f1f33faf24e updated distinct_subgoals_tac, flexflex_tac;
wenzelm
parents: 46274
diff changeset
   531
  some variables in a rule.  Normally flex-flex constraints can be
8f1f33faf24e updated distinct_subgoals_tac, flexflex_tac;
wenzelm
parents: 46274
diff changeset
   532
  ignored; they often disappear as unknowns get instantiated.
8f1f33faf24e updated distinct_subgoals_tac, flexflex_tac;
wenzelm
parents: 46274
diff changeset
   533
46274
67139209b548 updated rotate_tac;
wenzelm
parents: 46271
diff changeset
   534
  \end{description}%
67139209b548 updated rotate_tac;
wenzelm
parents: 46271
diff changeset
   535
\end{isamarkuptext}%
67139209b548 updated rotate_tac;
wenzelm
parents: 46271
diff changeset
   536
\isamarkuptrue%
67139209b548 updated rotate_tac;
wenzelm
parents: 46271
diff changeset
   537
%
67139209b548 updated rotate_tac;
wenzelm
parents: 46271
diff changeset
   538
\endisatagmlref
67139209b548 updated rotate_tac;
wenzelm
parents: 46271
diff changeset
   539
{\isafoldmlref}%
67139209b548 updated rotate_tac;
wenzelm
parents: 46271
diff changeset
   540
%
67139209b548 updated rotate_tac;
wenzelm
parents: 46271
diff changeset
   541
\isadelimmlref
67139209b548 updated rotate_tac;
wenzelm
parents: 46271
diff changeset
   542
%
67139209b548 updated rotate_tac;
wenzelm
parents: 46271
diff changeset
   543
\endisadelimmlref
67139209b548 updated rotate_tac;
wenzelm
parents: 46271
diff changeset
   544
%
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   545
\isamarkupsection{Tacticals \label{sec:tacticals}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   546
}
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   547
\isamarkuptrue%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   548
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   549
\begin{isamarkuptext}%
46258
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   550
A \emph{tactical} is a functional combinator for building up
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   551
  complex tactics from simpler ones.  Common tacticals perform
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   552
  sequential composition, disjunctive choice, iteration, or goal
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   553
  addressing.  Various search strategies may be expressed via
46269
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   554
  tacticals.%
46258
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   555
\end{isamarkuptext}%
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   556
\isamarkuptrue%
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   557
%
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   558
\isamarkupsubsection{Combining tactics%
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
\isamarkuptrue%
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   561
%
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   562
\begin{isamarkuptext}%
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   563
Sequential composition and alternative choices are the most
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   564
  basic ways to combine tactics, similarly to ``\verb|,|'' and
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   565
  ``\verb||\verb,|,\verb||'' in Isar method notation.  This corresponds to
46262
912b42e64fde tuned ML infixes;
wenzelm
parents: 46260
diff changeset
   566
  \verb|THEN| and \verb|ORELSE| in ML, but there are further
912b42e64fde tuned ML infixes;
wenzelm
parents: 46260
diff changeset
   567
  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
   568
  subgoal addressing.%
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   569
\end{isamarkuptext}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   570
\isamarkuptrue%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
   571
%
46258
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   572
\isadelimmlref
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   573
%
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   574
\endisadelimmlref
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   575
%
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   576
\isatagmlref
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   577
%
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   578
\begin{isamarkuptext}%
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   579
\begin{mldecls}
46262
912b42e64fde tuned ML infixes;
wenzelm
parents: 46260
diff changeset
   580
  \indexdef{}{ML infix}{THEN}\verb|infix THEN: tactic * tactic -> tactic| \\
912b42e64fde tuned ML infixes;
wenzelm
parents: 46260
diff changeset
   581
  \indexdef{}{ML infix}{ORELSE}\verb|infix ORELSE: tactic * tactic -> tactic| \\
912b42e64fde tuned ML infixes;
wenzelm
parents: 46260
diff changeset
   582
  \indexdef{}{ML infix}{APPEND}\verb|infix APPEND: tactic * tactic -> tactic| \\
46258
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   583
  \indexdef{}{ML}{EVERY}\verb|EVERY: tactic list -> tactic| \\
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   584
  \indexdef{}{ML}{FIRST}\verb|FIRST: tactic list -> tactic| \\[0.5ex]
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   585
46262
912b42e64fde tuned ML infixes;
wenzelm
parents: 46260
diff changeset
   586
  \indexdef{}{ML infix}{THEN'}\verb|infix THEN': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic| \\
912b42e64fde tuned ML infixes;
wenzelm
parents: 46260
diff changeset
   587
  \indexdef{}{ML infix}{ORELSE'}\verb|infix ORELSE': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic| \\
912b42e64fde tuned ML infixes;
wenzelm
parents: 46260
diff changeset
   588
  \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
   589
  \indexdef{}{ML}{EVERY'}\verb|EVERY': ('a -> tactic) list -> 'a -> tactic| \\
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   590
  \indexdef{}{ML}{FIRST'}\verb|FIRST': ('a -> tactic) list -> 'a -> tactic| \\
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   591
  \end{mldecls}
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   592
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   593
  \begin{description}
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   594
46262
912b42e64fde tuned ML infixes;
wenzelm
parents: 46260
diff changeset
   595
  \item \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}}~\verb|THEN|~\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} is the sequential
46269
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   596
  composition of \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}.  Applied to a goal
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   597
  state, it returns all states reachable in two steps by applying
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   598
  \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} followed by \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}.  First, it applies \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} to the goal state, getting a sequence of possible next
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   599
  states; then, it applies \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} to each of these and
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   600
  concatenates the results to produce again one flat sequence of
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   601
  states.
46258
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   602
46262
912b42e64fde tuned ML infixes;
wenzelm
parents: 46260
diff changeset
   603
  \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
   604
  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
   605
  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
   606
  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
   607
  from the result.
46258
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   608
46262
912b42e64fde tuned ML infixes;
wenzelm
parents: 46260
diff changeset
   609
  \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
   610
  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
   611
  \verb|ORELSE| there is \emph{no commitment} to either tactic, so
912b42e64fde tuned ML infixes;
wenzelm
parents: 46260
diff changeset
   612
  \verb|APPEND| helps to avoid incompleteness during search, at
912b42e64fde tuned ML infixes;
wenzelm
parents: 46260
diff changeset
   613
  the cost of potential inefficiencies.
46258
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   614
46262
912b42e64fde tuned ML infixes;
wenzelm
parents: 46260
diff changeset
   615
  \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
   616
  Note that \verb|EVERY []| is the same as \verb|all_tac|: it always
912b42e64fde tuned ML infixes;
wenzelm
parents: 46260
diff changeset
   617
  succeeds.
46258
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   618
46262
912b42e64fde tuned ML infixes;
wenzelm
parents: 46260
diff changeset
   619
  \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
   620
  always fails.
46258
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   621
46264
wenzelm
parents: 46263
diff changeset
   622
  \item \verb|THEN'| is the lifted version of \verb|THEN|, for
46266
a9694a4e39e5 removed some obscure material;
wenzelm
parents: 46264
diff changeset
   623
  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
   624
46264
wenzelm
parents: 46263
diff changeset
   625
  The other primed tacticals work analogously.
46258
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   626
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   627
  \end{description}%
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   628
\end{isamarkuptext}%
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   629
\isamarkuptrue%
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   630
%
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   631
\endisatagmlref
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   632
{\isafoldmlref}%
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   633
%
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   634
\isadelimmlref
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   635
%
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   636
\endisadelimmlref
89ee3bc580a8 updated THEN, ORELSE, APPEND, and derivatives;
wenzelm
parents: 40802
diff changeset
   637
%
46259
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   638
\isamarkupsubsection{Repetition tacticals%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   639
}
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   640
\isamarkuptrue%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   641
%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   642
\begin{isamarkuptext}%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   643
These tacticals provide further control over repetition of
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   644
  tactics, beyond the stylized forms of ``\verb|?|''  and
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   645
  ``\verb|+|'' in Isar method expressions.%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   646
\end{isamarkuptext}%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   647
\isamarkuptrue%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   648
%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   649
\isadelimmlref
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   650
%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   651
\endisadelimmlref
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   652
%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   653
\isatagmlref
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   654
%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   655
\begin{isamarkuptext}%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   656
\begin{mldecls}
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   657
  \indexdef{}{ML}{TRY}\verb|TRY: tactic -> tactic| \\
46266
a9694a4e39e5 removed some obscure material;
wenzelm
parents: 46264
diff changeset
   658
  \indexdef{}{ML}{REPEAT}\verb|REPEAT: tactic -> tactic| \\
a9694a4e39e5 removed some obscure material;
wenzelm
parents: 46264
diff changeset
   659
  \indexdef{}{ML}{REPEAT1}\verb|REPEAT1: tactic -> tactic| \\
46259
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   660
  \indexdef{}{ML}{REPEAT\_DETERM}\verb|REPEAT_DETERM: tactic -> tactic| \\
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   661
  \indexdef{}{ML}{REPEAT\_DETERM\_N}\verb|REPEAT_DETERM_N: int -> tactic -> tactic| \\
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   662
  \end{mldecls}
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   663
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   664
  \begin{description}
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   665
46269
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   666
  \item \verb|TRY|~\isa{tac} applies \isa{tac} to the goal
46259
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   667
  state and returns the resulting sequence, if non-empty; otherwise it
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   668
  returns the original state.  Thus, it applies \isa{tac} at most
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   669
  once.
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   670
46266
a9694a4e39e5 removed some obscure material;
wenzelm
parents: 46264
diff changeset
   671
  Note that for tactics with subgoal addressing, the combinator can be
a9694a4e39e5 removed some obscure material;
wenzelm
parents: 46264
diff changeset
   672
  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
   673
46269
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   674
  \item \verb|REPEAT|~\isa{tac} applies \isa{tac} to the goal
46259
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   675
  state and, recursively, to each element of the resulting sequence.
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   676
  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
   677
  possible (including zero times), and allows backtracking over each
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   678
  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
   679
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   680
  \item \verb|REPEAT1|~\isa{tac} is like \verb|REPEAT|~\isa{tac}
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   681
  but it always applies \isa{tac} at least once, failing if this
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   682
  is impossible.
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   683
46266
a9694a4e39e5 removed some obscure material;
wenzelm
parents: 46264
diff changeset
   684
  \item \verb|REPEAT_DETERM|~\isa{tac} applies \isa{tac} to the
46269
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   685
  goal state and, recursively, to the head of the resulting sequence.
46266
a9694a4e39e5 removed some obscure material;
wenzelm
parents: 46264
diff changeset
   686
  It returns the first state to make \isa{tac} fail.  It is
a9694a4e39e5 removed some obscure material;
wenzelm
parents: 46264
diff changeset
   687
  deterministic, discarding alternative outcomes.
a9694a4e39e5 removed some obscure material;
wenzelm
parents: 46264
diff changeset
   688
a9694a4e39e5 removed some obscure material;
wenzelm
parents: 46264
diff changeset
   689
  \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
   690
  by \isa{n} (where \verb|~1| means \isa{{\isaliteral{5C3C696E66696E6974793E}{\isasyminfinity}}}).
46259
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   691
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   692
  \end{description}%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   693
\end{isamarkuptext}%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   694
\isamarkuptrue%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   695
%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   696
\endisatagmlref
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   697
{\isafoldmlref}%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   698
%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   699
\isadelimmlref
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   700
%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   701
\endisadelimmlref
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   702
%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   703
\isadelimmlex
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   704
%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   705
\endisadelimmlex
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   706
%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   707
\isatagmlex
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   708
%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   709
\begin{isamarkuptext}%
46260
wenzelm
parents: 46259
diff changeset
   710
The basic tactics and tacticals considered above follow
wenzelm
parents: 46259
diff changeset
   711
  some algebraic laws:
wenzelm
parents: 46259
diff changeset
   712
wenzelm
parents: 46259
diff changeset
   713
  \begin{itemize}
wenzelm
parents: 46259
diff changeset
   714
46262
912b42e64fde tuned ML infixes;
wenzelm
parents: 46260
diff changeset
   715
  \item \verb|all_tac| is the identity element of the tactical \verb|THEN|.
46260
wenzelm
parents: 46259
diff changeset
   716
46262
912b42e64fde tuned ML infixes;
wenzelm
parents: 46260
diff changeset
   717
  \item \verb|no_tac| is the identity element of \verb|ORELSE| and
912b42e64fde tuned ML infixes;
wenzelm
parents: 46260
diff changeset
   718
  \verb|APPEND|.  Also, it is a zero element for \verb|THEN|,
912b42e64fde tuned ML infixes;
wenzelm
parents: 46260
diff changeset
   719
  which means that \isa{tac}~\verb|THEN|~\verb|no_tac| is
912b42e64fde tuned ML infixes;
wenzelm
parents: 46260
diff changeset
   720
  equivalent to \verb|no_tac|.
46260
wenzelm
parents: 46259
diff changeset
   721
wenzelm
parents: 46259
diff changeset
   722
  \item \verb|TRY| and \verb|REPEAT| can be expressed as (recursive)
wenzelm
parents: 46259
diff changeset
   723
  functions over more basic combinators (ignoring some internal
wenzelm
parents: 46259
diff changeset
   724
  implementation tricks):
wenzelm
parents: 46259
diff changeset
   725
wenzelm
parents: 46259
diff changeset
   726
  \end{itemize}%
46259
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   727
\end{isamarkuptext}%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   728
\isamarkuptrue%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   729
%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   730
\endisatagmlex
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   731
{\isafoldmlex}%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   732
%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   733
\isadelimmlex
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   734
%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   735
\endisadelimmlex
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   736
%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   737
\isadelimML
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   738
%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   739
\endisadelimML
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   740
%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   741
\isatagML
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   742
\isacommand{ML}\isamarkupfalse%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   743
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   744
\ \ 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
   745
\ \ 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
   746
{\isaliteral{2A7D}{\isacharverbatimclose}}%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   747
\endisatagML
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   748
{\isafoldML}%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   749
%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   750
\isadelimML
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   751
%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   752
\endisadelimML
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   753
%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   754
\begin{isamarkuptext}%
46262
912b42e64fde tuned ML infixes;
wenzelm
parents: 46260
diff changeset
   755
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
   756
  \verb|APPEND|, it applies \isa{tac} as many times as
46259
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   757
  possible in each outcome.
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   758
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   759
  \begin{warn}
46269
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   760
  Note the explicit abstraction over the goal state in the ML
46260
wenzelm
parents: 46259
diff changeset
   761
  definition of \verb|REPEAT|.  Recursive tacticals must be coded in
wenzelm
parents: 46259
diff changeset
   762
  this awkward fashion to avoid infinite recursion of eager functional
wenzelm
parents: 46259
diff changeset
   763
  evaluation in Standard ML.  The following attempt would make \verb|REPEAT|~\isa{tac} loop:
46259
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   764
  \end{warn}%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   765
\end{isamarkuptext}%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   766
\isamarkuptrue%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   767
%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   768
\isadelimML
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   769
%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   770
\endisadelimML
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   771
%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   772
\isatagML
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   773
\isacommand{ML}\isamarkupfalse%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   774
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
46260
wenzelm
parents: 46259
diff changeset
   775
\ \ {\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
   776
\ \ 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
   777
{\isaliteral{2A7D}{\isacharverbatimclose}}%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   778
\endisatagML
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   779
{\isafoldML}%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   780
%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   781
\isadelimML
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   782
%
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   783
\endisadelimML
46263
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   784
%
46267
bc9479cada96 moved HEADGOAL;
wenzelm
parents: 46266
diff changeset
   785
\isamarkupsubsection{Applying tactics to subgoal ranges%
46263
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   786
}
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   787
\isamarkuptrue%
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   788
%
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   789
\begin{isamarkuptext}%
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   790
Tactics with explicit subgoal addressing
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   791
  \verb|int -> tactic| can be used together with tacticals that
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   792
  act like ``subgoal quantifiers'': guided by success of the body
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   793
  tactic a certain range of subgoals is covered.  Thus the body tactic
46267
bc9479cada96 moved HEADGOAL;
wenzelm
parents: 46266
diff changeset
   794
  is applied to \emph{all} subgoals, \emph{some} subgoal etc.
46263
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   795
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   796
  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
   797
  these tacticals address subgoal ranges counting downwards from
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   798
  \isa{n} towards \isa{{\isadigit{1}}}.  This has the fortunate effect that
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   799
  newly emerging subgoals are concatenated in the result, without
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   800
  interfering each other.  Nonetheless, there might be situations
46266
a9694a4e39e5 removed some obscure material;
wenzelm
parents: 46264
diff changeset
   801
  where a different order is desired.%
46263
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   802
\end{isamarkuptext}%
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   803
\isamarkuptrue%
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   804
%
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   805
\isadelimmlref
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   806
%
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   807
\endisadelimmlref
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   808
%
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   809
\isatagmlref
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   810
%
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   811
\begin{isamarkuptext}%
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   812
\begin{mldecls}
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   813
  \indexdef{}{ML}{ALLGOALS}\verb|ALLGOALS: (int -> tactic) -> tactic| \\
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   814
  \indexdef{}{ML}{SOMEGOAL}\verb|SOMEGOAL: (int -> tactic) -> tactic| \\
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   815
  \indexdef{}{ML}{FIRSTGOAL}\verb|FIRSTGOAL: (int -> tactic) -> tactic| \\
46267
bc9479cada96 moved HEADGOAL;
wenzelm
parents: 46266
diff changeset
   816
  \indexdef{}{ML}{HEADGOAL}\verb|HEADGOAL: (int -> tactic) -> tactic| \\
46263
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   817
  \indexdef{}{ML}{REPEAT\_SOME}\verb|REPEAT_SOME: (int -> tactic) -> tactic| \\
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   818
  \indexdef{}{ML}{REPEAT\_FIRST}\verb|REPEAT_FIRST: (int -> tactic) -> tactic| \\
46267
bc9479cada96 moved HEADGOAL;
wenzelm
parents: 46266
diff changeset
   819
  \indexdef{}{ML}{RANGE}\verb|RANGE: (int -> tactic) list -> int -> tactic| \\
46263
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   820
  \end{mldecls}
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   821
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   822
  \begin{description}
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   823
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   824
  \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
   825
  applies the \isa{tac} to all the subgoals, counting downwards.
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   826
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   827
  \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
   828
  applies \isa{tac} to one subgoal, counting downwards.
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   829
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   830
  \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
   831
  applies \isa{tac} to one subgoal, counting upwards.
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   832
46267
bc9479cada96 moved HEADGOAL;
wenzelm
parents: 46266
diff changeset
   833
  \item \verb|HEADGOAL|~\isa{tac} is equivalent to \isa{tac\ {\isadigit{1}}}.
bc9479cada96 moved HEADGOAL;
wenzelm
parents: 46266
diff changeset
   834
  It applies \isa{tac} unconditionally to the first subgoal.
bc9479cada96 moved HEADGOAL;
wenzelm
parents: 46266
diff changeset
   835
46263
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   836
  \item \verb|REPEAT_SOME|~\isa{tac} applies \isa{tac} once or
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   837
  more to a subgoal, counting downwards.
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   838
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   839
  \item \verb|REPEAT_FIRST|~\isa{tac} applies \isa{tac} once or
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   840
  more to a subgoal, counting upwards.
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   841
46267
bc9479cada96 moved HEADGOAL;
wenzelm
parents: 46266
diff changeset
   842
  \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
   843
  \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
   844
  corresponding range of subgoals, counting downwards.
bc9479cada96 moved HEADGOAL;
wenzelm
parents: 46266
diff changeset
   845
46263
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   846
  \end{description}%
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   847
\end{isamarkuptext}%
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   848
\isamarkuptrue%
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   849
%
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   850
\endisatagmlref
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   851
{\isafoldmlref}%
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   852
%
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   853
\isadelimmlref
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   854
%
a87e06a18a5c updated "subgoal quantifiers";
wenzelm
parents: 46262
diff changeset
   855
\endisadelimmlref
46259
6fab37137dcb updated repetition tacticals;
wenzelm
parents: 46258
diff changeset
   856
%
46269
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   857
\isamarkupsubsection{Control and search tacticals%
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   858
}
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   859
\isamarkuptrue%
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   860
%
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   861
\begin{isamarkuptext}%
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   862
A predicate on theorems \verb|thm -> bool| can test
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   863
  whether a goal state enjoys some desirable property --- such as
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   864
  having no subgoals.  Tactics that search for satisfactory goal
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   865
  states are easy to express.  The main search procedures,
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   866
  depth-first, breadth-first and best-first, are provided as
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   867
  tacticals.  They generate the search tree by repeatedly applying a
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   868
  given tactic.%
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   869
\end{isamarkuptext}%
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   870
\isamarkuptrue%
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   871
%
46270
4ab175c85d57 tuned sectioning;
wenzelm
parents: 46269
diff changeset
   872
\isadelimmlref
4ab175c85d57 tuned sectioning;
wenzelm
parents: 46269
diff changeset
   873
%
4ab175c85d57 tuned sectioning;
wenzelm
parents: 46269
diff changeset
   874
\endisadelimmlref
4ab175c85d57 tuned sectioning;
wenzelm
parents: 46269
diff changeset
   875
%
4ab175c85d57 tuned sectioning;
wenzelm
parents: 46269
diff changeset
   876
\isatagmlref
4ab175c85d57 tuned sectioning;
wenzelm
parents: 46269
diff changeset
   877
%
4ab175c85d57 tuned sectioning;
wenzelm
parents: 46269
diff changeset
   878
\begin{isamarkuptext}%
4ab175c85d57 tuned sectioning;
wenzelm
parents: 46269
diff changeset
   879
%
4ab175c85d57 tuned sectioning;
wenzelm
parents: 46269
diff changeset
   880
\end{isamarkuptext}%
4ab175c85d57 tuned sectioning;
wenzelm
parents: 46269
diff changeset
   881
\isamarkuptrue%
4ab175c85d57 tuned sectioning;
wenzelm
parents: 46269
diff changeset
   882
%
4ab175c85d57 tuned sectioning;
wenzelm
parents: 46269
diff changeset
   883
\endisatagmlref
4ab175c85d57 tuned sectioning;
wenzelm
parents: 46269
diff changeset
   884
{\isafoldmlref}%
4ab175c85d57 tuned sectioning;
wenzelm
parents: 46269
diff changeset
   885
%
4ab175c85d57 tuned sectioning;
wenzelm
parents: 46269
diff changeset
   886
\isadelimmlref
4ab175c85d57 tuned sectioning;
wenzelm
parents: 46269
diff changeset
   887
%
4ab175c85d57 tuned sectioning;
wenzelm
parents: 46269
diff changeset
   888
\endisadelimmlref
4ab175c85d57 tuned sectioning;
wenzelm
parents: 46269
diff changeset
   889
%
46269
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   890
\isamarkupsubsubsection{Filtering a tactic's results%
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   891
}
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   892
\isamarkuptrue%
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   893
%
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   894
\begin{isamarkuptext}%
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   895
\begin{mldecls}
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   896
  \indexdef{}{ML}{FILTER}\verb|FILTER: (thm -> bool) -> tactic -> tactic| \\
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   897
  \indexdef{}{ML}{CHANGED}\verb|CHANGED: tactic -> tactic| \\
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   898
  \end{mldecls}
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   899
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   900
  \begin{description}
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   901
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   902
  \item \verb|FILTER|~\isa{sat\ tac} applies \isa{tac} to the
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   903
  goal state and returns a sequence consisting of those result goal
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   904
  states that are satisfactory in the sense of \isa{sat}.
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   905
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   906
  \item \verb|CHANGED|~\isa{tac} applies \isa{tac} to the goal
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   907
  state and returns precisely those states that differ from the
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   908
  original state (according to \verb|Thm.eq_thm|).  Thus \verb|CHANGED|~\isa{tac} always has some effect on the state.
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   909
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   910
  \end{description}%
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   911
\end{isamarkuptext}%
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   912
\isamarkuptrue%
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   913
%
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   914
\isamarkupsubsubsection{Depth-first search%
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   915
}
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   916
\isamarkuptrue%
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   917
%
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   918
\begin{isamarkuptext}%
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   919
\begin{mldecls}
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   920
  \indexdef{}{ML}{DEPTH\_FIRST}\verb|DEPTH_FIRST: (thm -> bool) -> tactic -> tactic| \\
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   921
  \indexdef{}{ML}{DEPTH\_SOLVE}\verb|DEPTH_SOLVE: tactic -> tactic| \\
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   922
  \indexdef{}{ML}{DEPTH\_SOLVE\_1}\verb|DEPTH_SOLVE_1: tactic -> tactic| \\
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   923
  \end{mldecls}
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   924
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   925
  \begin{description}
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   926
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   927
  \item \verb|DEPTH_FIRST|~\isa{sat\ tac} returns the goal state if
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   928
  \isa{sat} returns true.  Otherwise it applies \isa{tac},
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   929
  then recursively searches from each element of the resulting
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   930
  sequence.  The code uses a stack for efficiency, in effect applying
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   931
  \isa{tac}~\verb|THEN|~\verb|DEPTH_FIRST|~\isa{sat\ tac} to
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   932
  the state.
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   933
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   934
  \item \verb|DEPTH_SOLVE|\isa{tac} uses \verb|DEPTH_FIRST| to
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   935
  search for states having no subgoals.
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   936
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   937
  \item \verb|DEPTH_SOLVE_1|~\isa{tac} uses \verb|DEPTH_FIRST| to
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   938
  search for states having fewer subgoals than the given state.  Thus,
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   939
  it insists upon solving at least one subgoal.
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   940
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   941
  \end{description}%
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   942
\end{isamarkuptext}%
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   943
\isamarkuptrue%
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   944
%
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   945
\isamarkupsubsubsection{Other search strategies%
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   946
}
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   947
\isamarkuptrue%
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   948
%
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   949
\begin{isamarkuptext}%
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   950
\begin{mldecls}
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   951
  \indexdef{}{ML}{BREADTH\_FIRST}\verb|BREADTH_FIRST: (thm -> bool) -> tactic -> tactic| \\
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   952
  \indexdef{}{ML}{BEST\_FIRST}\verb|BEST_FIRST: (thm -> bool) * (thm -> int) -> tactic -> tactic| \\
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   953
  \indexdef{}{ML}{THEN\_BEST\_FIRST}\verb|THEN_BEST_FIRST: tactic -> (thm -> bool) * (thm -> int) -> tactic -> tactic| \\
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   954
  \end{mldecls}
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   955
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   956
  These search strategies will find a solution if one exists.
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   957
  However, they do not enumerate all solutions; they terminate after
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   958
  the first satisfactory result from \isa{tac}.
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   959
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   960
  \begin{description}
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   961
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   962
  \item \verb|BREADTH_FIRST|~\isa{sat\ tac} uses breadth-first
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   963
  search to find states for which \isa{sat} is true.  For most
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   964
  applications, it is too slow.
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   965
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   966
  \item \verb|BEST_FIRST|~\isa{{\isaliteral{28}{\isacharparenleft}}sat{\isaliteral{2C}{\isacharcomma}}\ dist{\isaliteral{29}{\isacharparenright}}\ tac} does a heuristic
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   967
  search, using \isa{dist} to estimate the distance from a
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   968
  satisfactory state (in the sense of \isa{sat}).  It maintains a
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   969
  list of states ordered by distance.  It applies \isa{tac} to the
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   970
  head of this list; if the result contains any satisfactory states,
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   971
  then it returns them.  Otherwise, \verb|BEST_FIRST| adds the new
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   972
  states to the list, and continues.
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   973
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   974
  The distance function is typically \verb|size_of_thm|, which computes
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   975
  the size of the state.  The smaller the state, the fewer and simpler
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   976
  subgoals it has.
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   977
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   978
  \item \verb|THEN_BEST_FIRST|~\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{0}}\ {\isaliteral{28}{\isacharparenleft}}sat{\isaliteral{2C}{\isacharcomma}}\ dist{\isaliteral{29}{\isacharparenright}}\ tac} is like
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   979
  \verb|BEST_FIRST|, except that the priority queue initially contains
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   980
  the result of applying \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{0}}} to the goal state.  This
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   981
  tactical permits separate tactics for starting the search and
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   982
  continuing the search.
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   983
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   984
  \end{description}%
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   985
\end{isamarkuptext}%
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   986
\isamarkuptrue%
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   987
%
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   988
\isamarkupsubsubsection{Auxiliary tacticals for searching%
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   989
}
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   990
\isamarkuptrue%
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   991
%
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   992
\begin{isamarkuptext}%
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   993
\begin{mldecls}
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   994
  \indexdef{}{ML}{COND}\verb|COND: (thm -> bool) -> tactic -> tactic -> tactic| \\
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   995
  \indexdef{}{ML}{IF\_UNSOLVED}\verb|IF_UNSOLVED: tactic -> tactic| \\
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   996
  \indexdef{}{ML}{SOLVE}\verb|SOLVE: tactic -> tactic| \\
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   997
  \indexdef{}{ML}{DETERM}\verb|DETERM: tactic -> tactic| \\
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   998
  \end{mldecls}
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
   999
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
  1000
  \begin{description}
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
  1001
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
  1002
  \item \verb|COND|~\isa{sat\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} applies \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} to
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
  1003
  the goal state if it satisfies predicate \isa{sat}, and applies
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
  1004
  \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}.  It is a conditional tactical in that only one of
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
  1005
  \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} is applied to a goal state.
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
  1006
  However, both \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} are evaluated
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
  1007
  because ML uses eager evaluation.
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
  1008
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
  1009
  \item \verb|IF_UNSOLVED|~\isa{tac} applies \isa{tac} to the
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
  1010
  goal state if it has any subgoals, and simply returns the goal state
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
  1011
  otherwise.  Many common tactics, such as \verb|resolve_tac|, fail if
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
  1012
  applied to a goal state that has no subgoals.
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
  1013
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
  1014
  \item \verb|SOLVE|~\isa{tac} applies \isa{tac} to the goal
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
  1015
  state and then fails iff there are subgoals left.
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
  1016
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
  1017
  \item \verb|DETERM|~\isa{tac} applies \isa{tac} to the goal
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
  1018
  state and returns the head of the resulting sequence.  \verb|DETERM|
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
  1019
  limits the search space by making its argument deterministic.
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
  1020
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
  1021
  \end{description}%
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
  1022
\end{isamarkuptext}%
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
  1023
\isamarkuptrue%
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
  1024
%
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
  1025
\isamarkupsubsubsection{Predicates and functions useful for searching%
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
  1026
}
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
  1027
\isamarkuptrue%
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
  1028
%
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
  1029
\begin{isamarkuptext}%
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
  1030
\begin{mldecls}
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
  1031
  \indexdef{}{ML}{has\_fewer\_prems}\verb|has_fewer_prems: int -> thm -> bool| \\
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
  1032
  \indexdef{}{ML}{Thm.eq\_thm}\verb|Thm.eq_thm: thm * thm -> bool| \\
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
  1033
  \indexdef{}{ML}{Thm.eq\_thm\_prop}\verb|Thm.eq_thm_prop: thm * thm -> bool| \\
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
  1034
  \indexdef{}{ML}{size\_of\_thm}\verb|size_of_thm: thm -> int| \\
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
  1035
  \end{mldecls}
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
  1036
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
  1037
  \begin{description}
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
  1038
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
  1039
  \item \verb|has_fewer_prems|~\isa{n\ thm} reports whether \isa{thm} has fewer than \isa{n} premises.
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
  1040
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
  1041
  \item \verb|Thm.eq_thm|~\isa{{\isaliteral{28}{\isacharparenleft}}thm\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ thm\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}} reports whether \isa{thm\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and \isa{thm\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} are equal.  Both theorems must have
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
  1042
  compatible background theories.  Both theorems must have the same
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
  1043
  conclusions, the same set of hypotheses, and the same set of sort
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
  1044
  hypotheses.  Names of bound variables are ignored as usual.
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
  1045
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
  1046
  \item \verb|Thm.eq_thm_prop|~\isa{{\isaliteral{28}{\isacharparenleft}}thm\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ thm\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}} reports whether
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
  1047
  the propositions of \isa{thm\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and \isa{thm\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} are equal.
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
  1048
  Names of bound variables are ignored.
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
  1049
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
  1050
  \item \verb|size_of_thm|~\isa{thm} computes the size of \isa{thm}, namely the number of variables, constants and abstractions
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
  1051
  in its conclusion.  It may serve as a distance function for
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
  1052
  \verb|BEST_FIRST|.
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
  1053
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
  1054
  \end{description}%
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
  1055
\end{isamarkuptext}%
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
  1056
\isamarkuptrue%
e75181672150 updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents: 46267
diff changeset
  1057
%
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
  1058
\isadelimtheory
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
  1059
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
  1060
\endisadelimtheory
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
  1061
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
  1062
\isatagtheory
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
  1063
\isacommand{end}\isamarkupfalse%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
  1064
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
  1065
\endisatagtheory
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
  1066
{\isafoldtheory}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
  1067
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
  1068
\isadelimtheory
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
  1069
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
  1070
\endisadelimtheory
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
  1071
\isanewline
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
  1072
\end{isabellebody}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
  1073
%%% Local Variables:
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
  1074
%%% mode: latex
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
  1075
%%% TeX-master: "root"
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset
  1076
%%% End: