doc-src/Ref/tctical.tex
author haftmann
Thu, 12 Nov 2009 15:49:01 +0100
changeset 33633 9f7280e0c231
parent 30184 37969710e61f
child 46257 3ba3681d8930
permissions -rw-r--r--
explicit code lemmas produce nices code
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
30184
37969710e61f removed parts of the manual that are clearly obsolete, or covered by
wenzelm
parents: 13104
diff changeset
     1
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     2
\chapter{Tacticals}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     3
\index{tacticals|(}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     4
Tacticals are operations on tactics.  Their implementation makes use of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     5
functional programming techniques, especially for sequences.  Most of the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     6
time, you may forget about this and regard tacticals as high-level control
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     7
structures.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     8
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     9
\section{The basic tacticals}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    10
\subsection{Joining two tactics}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
    11
\index{tacticals!joining two tactics}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    12
The tacticals {\tt THEN} and {\tt ORELSE}, which provide sequencing and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    13
alternation, underlie most of the other control structures in Isabelle.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    14
{\tt APPEND} and {\tt INTLEAVE} provide more sophisticated forms of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    15
alternation.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    16
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    17
THEN     : tactic * tactic -> tactic                 \hfill{\bf infix 1}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    18
ORELSE   : tactic * tactic -> tactic                 \hfill{\bf infix}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    19
APPEND   : tactic * tactic -> tactic                 \hfill{\bf infix}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    20
INTLEAVE : tactic * tactic -> tactic                 \hfill{\bf infix}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    21
\end{ttbox}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
    22
\begin{ttdescription}
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
    23
\item[$tac@1$ \ttindexbold{THEN} $tac@2$] 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    24
is the sequential composition of the two tactics.  Applied to a proof
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    25
state, it returns all states reachable in two steps by applying $tac@1$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    26
followed by~$tac@2$.  First, it applies $tac@1$ to the proof state, getting a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    27
sequence of next states; then, it applies $tac@2$ to each of these and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    28
concatenates the results.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    29
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
    30
\item[$tac@1$ \ttindexbold{ORELSE} $tac@2$] 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    31
makes a choice between the two tactics.  Applied to a state, it
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    32
tries~$tac@1$ and returns the result if non-empty; if $tac@1$ fails then it
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    33
uses~$tac@2$.  This is a deterministic choice: if $tac@1$ succeeds then
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    34
$tac@2$ is excluded.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    35
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
    36
\item[$tac@1$ \ttindexbold{APPEND} $tac@2$] 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    37
concatenates the results of $tac@1$ and~$tac@2$.  By not making a commitment
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
    38
to either tactic, {\tt APPEND} helps avoid incompleteness during
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
    39
search.\index{search}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    40
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
    41
\item[$tac@1$ \ttindexbold{INTLEAVE} $tac@2$] 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    42
interleaves the results of $tac@1$ and~$tac@2$.  Thus, it includes all
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    43
possible next states, even if one of the tactics returns an infinite
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    44
sequence.
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
    45
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    46
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    47
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    48
\subsection{Joining a list of tactics}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
    49
\index{tacticals!joining a list of tactics}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    50
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    51
EVERY : tactic list -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    52
FIRST : tactic list -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    53
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    54
{\tt EVERY} and {\tt FIRST} are block structured versions of {\tt THEN} and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    55
{\tt ORELSE}\@.
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
    56
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    57
\item[\ttindexbold{EVERY} {$[tac@1,\ldots,tac@n]$}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    58
abbreviates \hbox{\tt$tac@1$ THEN \ldots{} THEN $tac@n$}.  It is useful for
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    59
writing a series of tactics to be executed in sequence.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    60
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    61
\item[\ttindexbold{FIRST} {$[tac@1,\ldots,tac@n]$}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    62
abbreviates \hbox{\tt$tac@1$ ORELSE \ldots{} ORELSE $tac@n$}.  It is useful for
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    63
writing a series of tactics to be attempted one after another.
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
    64
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    65
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    66
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    67
\subsection{Repetition tacticals}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
    68
\index{tacticals!repetition}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    69
\begin{ttbox} 
8149
941afb897532 added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents: 6569
diff changeset
    70
TRY             : tactic -> tactic
941afb897532 added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents: 6569
diff changeset
    71
REPEAT_DETERM   : tactic -> tactic
941afb897532 added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents: 6569
diff changeset
    72
REPEAT_DETERM_N : int -> tactic -> tactic
941afb897532 added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents: 6569
diff changeset
    73
REPEAT          : tactic -> tactic
941afb897532 added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents: 6569
diff changeset
    74
REPEAT1         : tactic -> tactic
941afb897532 added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents: 6569
diff changeset
    75
DETERM_UNTIL    : (thm -> bool) -> tactic -> tactic
941afb897532 added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents: 6569
diff changeset
    76
trace_REPEAT    : bool ref \hfill{\bf initially false}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    77
\end{ttbox}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
    78
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    79
\item[\ttindexbold{TRY} {\it tac}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    80
applies {\it tac\/} to the proof state and returns the resulting sequence,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    81
if non-empty; otherwise it returns the original state.  Thus, it applies
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    82
{\it tac\/} at most once.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    83
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    84
\item[\ttindexbold{REPEAT_DETERM} {\it tac}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    85
applies {\it tac\/} to the proof state and, recursively, to the head of the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    86
resulting sequence.  It returns the first state to make {\it tac\/} fail.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    87
It is deterministic, discarding alternative outcomes.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    88
8149
941afb897532 added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents: 6569
diff changeset
    89
\item[\ttindexbold{REPEAT_DETERM_N} {\it n} {\it tac}] 
941afb897532 added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents: 6569
diff changeset
    90
is like \hbox{\tt REPEAT_DETERM {\it tac}} but the number of repititions
941afb897532 added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents: 6569
diff changeset
    91
is bound by {\it n} (unless negative).
941afb897532 added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents: 6569
diff changeset
    92
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    93
\item[\ttindexbold{REPEAT} {\it tac}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    94
applies {\it tac\/} to the proof state and, recursively, to each element of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    95
the resulting sequence.  The resulting sequence consists of those states
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    96
that make {\it tac\/} fail.  Thus, it applies {\it tac\/} as many times as
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    97
possible (including zero times), and allows backtracking over each
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    98
invocation of {\it tac}.  It is more general than {\tt REPEAT_DETERM}, but
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    99
requires more space.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   100
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   101
\item[\ttindexbold{REPEAT1} {\it tac}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   102
is like \hbox{\tt REPEAT {\it tac}} but it always applies {\it tac\/} at
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   103
least once, failing if this is impossible.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   104
8149
941afb897532 added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents: 6569
diff changeset
   105
\item[\ttindexbold{DETERM_UNTIL} {\it p} {\it tac}] 
941afb897532 added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents: 6569
diff changeset
   106
applies {\it tac\/} to the proof state and, recursively, to the head of the
941afb897532 added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents: 6569
diff changeset
   107
resulting sequence, until the predicate {\it p} (applied on the proof state)
941afb897532 added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents: 6569
diff changeset
   108
yields {\it true}. It fails if {\it tac\/} fails on any of the intermediate 
941afb897532 added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents: 6569
diff changeset
   109
states. It is deterministic, discarding alternative outcomes.
941afb897532 added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents: 6569
diff changeset
   110
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 3108
diff changeset
   111
\item[set \ttindexbold{trace_REPEAT};] 
286
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   112
enables an interactive tracing mode for the tacticals {\tt REPEAT_DETERM}
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   113
and {\tt REPEAT}.  To view the tracing options, type {\tt h} at the prompt.
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   114
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   115
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   116
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   117
\subsection{Identities for tacticals}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   118
\index{tacticals!identities for}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   119
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   120
all_tac : tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   121
no_tac  : tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   122
\end{ttbox}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   123
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   124
\item[\ttindexbold{all_tac}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   125
maps any proof state to the one-element sequence containing that state.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   126
Thus, it succeeds for all states.  It is the identity element of the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   127
tactical \ttindex{THEN}\@.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   128
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   129
\item[\ttindexbold{no_tac}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   130
maps any proof state to the empty sequence.  Thus it succeeds for no state.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   131
It is the identity element of \ttindex{ORELSE}, \ttindex{APPEND}, and 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   132
\ttindex{INTLEAVE}\@.  Also, it is a zero element for \ttindex{THEN}, which means that
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   133
\hbox{\tt$tac$ THEN no_tac} is equivalent to {\tt no_tac}.
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   134
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   135
These primitive tactics are useful when writing tacticals.  For example,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   136
\ttindexbold{TRY} and \ttindexbold{REPEAT} (ignoring tracing) can be coded
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   137
as follows: 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   138
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   139
fun TRY tac = tac ORELSE all_tac;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   140
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1118
diff changeset
   141
fun REPEAT tac =
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1118
diff changeset
   142
     (fn state => ((tac THEN REPEAT tac) ORELSE all_tac) state);
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   143
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   144
If $tac$ can return multiple outcomes then so can \hbox{\tt REPEAT $tac$}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   145
Since {\tt REPEAT} uses \ttindex{ORELSE} and not {\tt APPEND} or {\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   146
INTLEAVE}, it applies $tac$ as many times as possible in each
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   147
outcome.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   148
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   149
\begin{warn}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   150
Note {\tt REPEAT}'s explicit abstraction over the proof state.  Recursive
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   151
tacticals must be coded in this awkward fashion to avoid infinite
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   152
recursion.  With the following definition, \hbox{\tt REPEAT $tac$} would
332
01b87a921967 final Springer copy
lcp
parents: 323
diff changeset
   153
loop due to \ML's eager evaluation strategy:
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   154
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   155
fun REPEAT tac = (tac THEN REPEAT tac) ORELSE all_tac;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   156
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   157
\par\noindent
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   158
The built-in {\tt REPEAT} avoids~{\tt THEN}, handling sequences explicitly
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   159
and using tail recursion.  This sacrifices clarity, but saves much space by
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   160
discarding intermediate proof states.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   161
\end{warn}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   162
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   163
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   164
\section{Control and search tacticals}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   165
\index{search!tacticals|(}
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   166
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   167
A predicate on theorems, namely a function of type \hbox{\tt thm->bool},
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   168
can test whether a proof state enjoys some desirable property --- such as
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   169
having no subgoals.  Tactics that search for satisfactory states are easy
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   170
to express.  The main search procedures, depth-first, breadth-first and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   171
best-first, are provided as tacticals.  They generate the search tree by
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   172
repeatedly applying a given tactic.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   173
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   174
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   175
\subsection{Filtering a tactic's results}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   176
\index{tacticals!for filtering}
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   177
\index{tactics!filtering results of}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   178
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   179
FILTER  : (thm -> bool) -> tactic -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   180
CHANGED : tactic -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   181
\end{ttbox}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   182
\begin{ttdescription}
1118
93ba05d8ccdc Indexing of FILTER and COND
lcp
parents: 332
diff changeset
   183
\item[\ttindexbold{FILTER} {\it p} $tac$] 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   184
applies $tac$ to the proof state and returns a sequence consisting of those
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   185
result states that satisfy~$p$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   186
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   187
\item[\ttindexbold{CHANGED} {\it tac}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   188
applies {\it tac\/} to the proof state and returns precisely those states
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   189
that differ from the original state.  Thus, \hbox{\tt CHANGED {\it tac}}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   190
always has some effect on the state.
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   191
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   192
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   193
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   194
\subsection{Depth-first search}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   195
\index{tacticals!searching}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   196
\index{tracing!of searching tacticals}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   197
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   198
DEPTH_FIRST   : (thm->bool) -> tactic -> tactic
332
01b87a921967 final Springer copy
lcp
parents: 323
diff changeset
   199
DEPTH_SOLVE   :                tactic -> tactic
01b87a921967 final Springer copy
lcp
parents: 323
diff changeset
   200
DEPTH_SOLVE_1 :                tactic -> tactic
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   201
trace_DEPTH_FIRST: bool ref \hfill{\bf initially false}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   202
\end{ttbox}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   203
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   204
\item[\ttindexbold{DEPTH_FIRST} {\it satp} {\it tac}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   205
returns the proof state if {\it satp} returns true.  Otherwise it applies
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   206
{\it tac}, then recursively searches from each element of the resulting
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   207
sequence.  The code uses a stack for efficiency, in effect applying
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   208
\hbox{\tt {\it tac} THEN DEPTH_FIRST {\it satp} {\it tac}} to the state.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   209
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   210
\item[\ttindexbold{DEPTH_SOLVE} {\it tac}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   211
uses {\tt DEPTH_FIRST} to search for states having no subgoals.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   212
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   213
\item[\ttindexbold{DEPTH_SOLVE_1} {\it tac}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   214
uses {\tt DEPTH_FIRST} to search for states having fewer subgoals than the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   215
given state.  Thus, it insists upon solving at least one subgoal.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   216
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 3108
diff changeset
   217
\item[set \ttindexbold{trace_DEPTH_FIRST};] 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   218
enables interactive tracing for {\tt DEPTH_FIRST}.  To view the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   219
tracing options, type {\tt h} at the prompt.
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   220
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   221
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   222
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   223
\subsection{Other search strategies}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   224
\index{tacticals!searching}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   225
\index{tracing!of searching tacticals}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   226
\begin{ttbox} 
332
01b87a921967 final Springer copy
lcp
parents: 323
diff changeset
   227
BREADTH_FIRST   :            (thm->bool) -> tactic -> tactic
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   228
BEST_FIRST      : (thm->bool)*(thm->int) -> tactic -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   229
THEN_BEST_FIRST : tactic * ((thm->bool) * (thm->int) * tactic)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   230
                  -> tactic                    \hfill{\bf infix 1}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   231
trace_BEST_FIRST: bool ref \hfill{\bf initially false}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   232
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   233
These search strategies will find a solution if one exists.  However, they
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   234
do not enumerate all solutions; they terminate after the first satisfactory
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   235
result from {\it tac}.
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   236
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   237
\item[\ttindexbold{BREADTH_FIRST} {\it satp} {\it tac}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   238
uses breadth-first search to find states for which {\it satp\/} is true.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   239
For most applications, it is too slow.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   240
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   241
\item[\ttindexbold{BEST_FIRST} $(satp,distf)$ {\it tac}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   242
does a heuristic search, using {\it distf\/} to estimate the distance from
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   243
a satisfactory state.  It maintains a list of states ordered by distance.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   244
It applies $tac$ to the head of this list; if the result contains any
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   245
satisfactory states, then it returns them.  Otherwise, {\tt BEST_FIRST}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   246
adds the new states to the list, and continues.  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   247
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   248
The distance function is typically \ttindex{size_of_thm}, which computes
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   249
the size of the state.  The smaller the state, the fewer and simpler
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   250
subgoals it has.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   251
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   252
\item[$tac@0$ \ttindexbold{THEN_BEST_FIRST} $(satp,distf,tac)$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   253
is like {\tt BEST_FIRST}, except that the priority queue initially
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   254
contains the result of applying $tac@0$ to the proof state.  This tactical
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   255
permits separate tactics for starting the search and continuing the search.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   256
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 3108
diff changeset
   257
\item[set \ttindexbold{trace_BEST_FIRST};] 
286
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   258
enables an interactive tracing mode for the tactical {\tt BEST_FIRST}.  To
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   259
view the tracing options, type {\tt h} at the prompt.
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   260
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   261
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   262
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   263
\subsection{Auxiliary tacticals for searching}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   264
\index{tacticals!conditional}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   265
\index{tacticals!deterministic}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   266
\begin{ttbox} 
8149
941afb897532 added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents: 6569
diff changeset
   267
COND                : (thm->bool) -> tactic -> tactic -> tactic
941afb897532 added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents: 6569
diff changeset
   268
IF_UNSOLVED         : tactic -> tactic
941afb897532 added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents: 6569
diff changeset
   269
SOLVE               : tactic -> tactic
941afb897532 added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents: 6569
diff changeset
   270
DETERM              : tactic -> tactic
941afb897532 added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents: 6569
diff changeset
   271
DETERM_UNTIL_SOLVED : tactic -> tactic
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   272
\end{ttbox}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   273
\begin{ttdescription}
1118
93ba05d8ccdc Indexing of FILTER and COND
lcp
parents: 332
diff changeset
   274
\item[\ttindexbold{COND} {\it p} $tac@1$ $tac@2$] 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   275
applies $tac@1$ to the proof state if it satisfies~$p$, and applies $tac@2$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   276
otherwise.  It is a conditional tactical in that only one of $tac@1$ and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   277
$tac@2$ is applied to a proof state.  However, both $tac@1$ and $tac@2$ are
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   278
evaluated because \ML{} uses eager evaluation.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   279
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   280
\item[\ttindexbold{IF_UNSOLVED} {\it tac}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   281
applies {\it tac\/} to the proof state if it has any subgoals, and simply
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   282
returns the proof state otherwise.  Many common tactics, such as {\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   283
resolve_tac}, fail if applied to a proof state that has no subgoals.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   284
5754
98744e38ded1 added SOLVE tactical
oheimb
parents: 5371
diff changeset
   285
\item[\ttindexbold{SOLVE} {\it tac}] 
98744e38ded1 added SOLVE tactical
oheimb
parents: 5371
diff changeset
   286
applies {\it tac\/} to the proof state and then fails iff there are subgoals
98744e38ded1 added SOLVE tactical
oheimb
parents: 5371
diff changeset
   287
left.
98744e38ded1 added SOLVE tactical
oheimb
parents: 5371
diff changeset
   288
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   289
\item[\ttindexbold{DETERM} {\it tac}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   290
applies {\it tac\/} to the proof state and returns the head of the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   291
resulting sequence.  {\tt DETERM} limits the search space by making its
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   292
argument deterministic.
8149
941afb897532 added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents: 6569
diff changeset
   293
941afb897532 added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents: 6569
diff changeset
   294
\item[\ttindexbold{DETERM_UNTIL_SOLVED} {\it tac}] 
941afb897532 added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents: 6569
diff changeset
   295
forces repeated deterministic application of {\it tac\/} to the proof state 
941afb897532 added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents: 6569
diff changeset
   296
until the goal is solved completely.
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   297
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   298
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   299
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   300
\subsection{Predicates and functions useful for searching}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   301
\index{theorems!size of}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   302
\index{theorems!equality of}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   303
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   304
has_fewer_prems : int -> thm -> bool
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   305
eq_thm          : thm * thm -> bool
13104
df7aac8543c9 clarified eq_thm;
wenzelm
parents: 8149
diff changeset
   306
eq_thm_prop     : thm * thm -> bool
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   307
size_of_thm     : thm -> int
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   308
\end{ttbox}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   309
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   310
\item[\ttindexbold{has_fewer_prems} $n$ $thm$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   311
reports whether $thm$ has fewer than~$n$ premises.  By currying,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   312
\hbox{\tt has_fewer_prems $n$} is a predicate on theorems; it may 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   313
be given to the searching tacticals.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   314
6569
wenzelm
parents: 5754
diff changeset
   315
\item[\ttindexbold{eq_thm} ($thm@1$, $thm@2$)] reports whether $thm@1$ and
13104
df7aac8543c9 clarified eq_thm;
wenzelm
parents: 8149
diff changeset
   316
  $thm@2$ are equal.  Both theorems must have compatible signatures.  Both
df7aac8543c9 clarified eq_thm;
wenzelm
parents: 8149
diff changeset
   317
  theorems must have the same conclusions, the same hypotheses (in the same
df7aac8543c9 clarified eq_thm;
wenzelm
parents: 8149
diff changeset
   318
  order), and the same set of sort hypotheses.  Names of bound variables are
df7aac8543c9 clarified eq_thm;
wenzelm
parents: 8149
diff changeset
   319
  ignored.
df7aac8543c9 clarified eq_thm;
wenzelm
parents: 8149
diff changeset
   320
  
df7aac8543c9 clarified eq_thm;
wenzelm
parents: 8149
diff changeset
   321
\item[\ttindexbold{eq_thm_prop} ($thm@1$, $thm@2$)] reports whether the
df7aac8543c9 clarified eq_thm;
wenzelm
parents: 8149
diff changeset
   322
  propositions of $thm@1$ and $thm@2$ are equal.  Names of bound variables are
df7aac8543c9 clarified eq_thm;
wenzelm
parents: 8149
diff changeset
   323
  ignored.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   324
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   325
\item[\ttindexbold{size_of_thm} $thm$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   326
computes the size of $thm$, namely the number of variables, constants and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   327
abstractions in its conclusion.  It may serve as a distance function for 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   328
\ttindex{BEST_FIRST}. 
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   329
\end{ttdescription}
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   330
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   331
\index{search!tacticals|)}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   332
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   333
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   334
\section{Tacticals for subgoal numbering}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   335
When conducting a backward proof, we normally consider one goal at a time.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   336
A tactic can affect the entire proof state, but many tactics --- such as
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   337
{\tt resolve_tac} and {\tt assume_tac} --- work on a single subgoal.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   338
Subgoals are designated by a positive integer, so Isabelle provides
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   339
tacticals for combining values of type {\tt int->tactic}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   340
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   341
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   342
\subsection{Restricting a tactic to one subgoal}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   343
\index{tactics!restricting to a subgoal}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   344
\index{tacticals!for restriction to a subgoal}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   345
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   346
SELECT_GOAL : tactic -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   347
METAHYPS    : (thm list -> tactic) -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   348
\end{ttbox}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   349
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   350
\item[\ttindexbold{SELECT_GOAL} {\it tac} $i$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   351
restricts the effect of {\it tac\/} to subgoal~$i$ of the proof state.  It
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   352
fails if there is no subgoal~$i$, or if {\it tac\/} changes the main goal
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   353
(do not use {\tt rewrite_tac}).  It applies {\it tac\/} to a dummy proof
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   354
state and uses the result to refine the original proof state at
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   355
subgoal~$i$.  If {\it tac\/} returns multiple results then so does 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   356
\hbox{\tt SELECT_GOAL {\it tac} $i$}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   357
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   358
{\tt SELECT_GOAL} works by creating a state of the form $\phi\Imp\phi$,
332
01b87a921967 final Springer copy
lcp
parents: 323
diff changeset
   359
with the one subgoal~$\phi$.  If subgoal~$i$ has the form $\psi\Imp\theta$
01b87a921967 final Springer copy
lcp
parents: 323
diff changeset
   360
then $(\psi\Imp\theta)\Imp(\psi\Imp\theta)$ is in fact
01b87a921967 final Springer copy
lcp
parents: 323
diff changeset
   361
$\List{\psi\Imp\theta;\; \psi}\Imp\theta$, a proof state with two subgoals.
01b87a921967 final Springer copy
lcp
parents: 323
diff changeset
   362
Such a proof state might cause tactics to go astray.  Therefore {\tt
01b87a921967 final Springer copy
lcp
parents: 323
diff changeset
   363
  SELECT_GOAL} inserts a quantifier to create the state
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   364
\[ (\Forall x.\psi\Imp\theta)\Imp(\Forall x.\psi\Imp\theta). \]
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   365
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   366
\item[\ttindexbold{METAHYPS} {\it tacf} $i$]\index{meta-assumptions}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   367
takes subgoal~$i$, of the form 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   368
\[ \Forall x@1 \ldots x@l. \List{\theta@1; \ldots; \theta@k}\Imp\theta, \]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   369
and creates the list $\theta'@1$, \ldots, $\theta'@k$ of meta-level
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   370
assumptions.  In these theorems, the subgoal's parameters ($x@1$,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   371
\ldots,~$x@l$) become free variables.  It supplies the assumptions to
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   372
$tacf$ and applies the resulting tactic to the proof state
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   373
$\theta\Imp\theta$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   374
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   375
If the resulting proof state is $\List{\phi@1; \ldots; \phi@n} \Imp \phi$,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   376
possibly containing $\theta'@1,\ldots,\theta'@k$ as assumptions, then it is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   377
lifted back into the original context, yielding $n$ subgoals.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   378
286
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   379
Meta-level assumptions may not contain unknowns.  Unknowns in the
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   380
hypotheses $\theta@1,\ldots,\theta@k$ become free variables in $\theta'@1$,
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   381
\ldots, $\theta'@k$, and are restored afterwards; the {\tt METAHYPS} call
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   382
cannot instantiate them.  Unknowns in $\theta$ may be instantiated.  New
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   383
unknowns in $\phi@1$, \ldots, $\phi@n$ are lifted over the parameters.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   384
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   385
Here is a typical application.  Calling {\tt hyp_res_tac}~$i$ resolves
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   386
subgoal~$i$ with one of its own assumptions, which may itself have the form
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   387
of an inference rule (these are called {\bf higher-level assumptions}).  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   388
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   389
val hyp_res_tac = METAHYPS (fn prems => resolve_tac prems 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   390
\end{ttbox} 
332
01b87a921967 final Springer copy
lcp
parents: 323
diff changeset
   391
The function \ttindex{gethyps} is useful for debugging applications of {\tt
01b87a921967 final Springer copy
lcp
parents: 323
diff changeset
   392
  METAHYPS}. 
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   393
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   394
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   395
\begin{warn}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   396
{\tt METAHYPS} fails if the context or new subgoals contain type unknowns.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   397
In principle, the tactical could treat these like ordinary unknowns.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   398
\end{warn}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   399
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   400
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   401
\subsection{Scanning for a subgoal by number}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   402
\index{tacticals!scanning for subgoals}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   403
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   404
ALLGOALS         : (int -> tactic) -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   405
TRYALL           : (int -> tactic) -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   406
SOMEGOAL         : (int -> tactic) -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   407
FIRSTGOAL        : (int -> tactic) -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   408
REPEAT_SOME      : (int -> tactic) -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   409
REPEAT_FIRST     : (int -> tactic) -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   410
trace_goalno_tac : (int -> tactic) -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   411
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   412
These apply a tactic function of type {\tt int -> tactic} to all the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   413
subgoal numbers of a proof state, and join the resulting tactics using
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   414
\ttindex{THEN} or \ttindex{ORELSE}\@.  Thus, they apply the tactic to all the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   415
subgoals, or to one subgoal.  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   416
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   417
Suppose that the original proof state has $n$ subgoals.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   418
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   419
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   420
\item[\ttindexbold{ALLGOALS} {\it tacf}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   421
is equivalent to
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   422
\hbox{\tt$tacf(n)$ THEN \ldots{} THEN $tacf(1)$}.  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   423
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   424
It applies {\it tacf} to all the subgoals, counting downwards (to
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   425
avoid problems when subgoals are added or deleted).
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   426
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   427
\item[\ttindexbold{TRYALL} {\it tacf}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   428
is equivalent to
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   429
\hbox{\tt TRY$(tacf(n))$ THEN \ldots{} THEN TRY$(tacf(1))$}.  
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   430
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   431
It attempts to apply {\it tacf} to all the subgoals.  For instance,
286
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   432
the tactic \hbox{\tt TRYALL assume_tac} attempts to solve all the subgoals by
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   433
assumption.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   434
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   435
\item[\ttindexbold{SOMEGOAL} {\it tacf}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   436
is equivalent to
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   437
\hbox{\tt$tacf(n)$ ORELSE \ldots{} ORELSE $tacf(1)$}.  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   438
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   439
It applies {\it tacf} to one subgoal, counting downwards.  For instance,
286
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   440
the tactic \hbox{\tt SOMEGOAL assume_tac} solves one subgoal by assumption,
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   441
failing if this is impossible.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   442
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   443
\item[\ttindexbold{FIRSTGOAL} {\it tacf}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   444
is equivalent to
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   445
\hbox{\tt$tacf(1)$ ORELSE \ldots{} ORELSE $tacf(n)$}.  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   446
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   447
It applies {\it tacf} to one subgoal, counting upwards.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   448
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   449
\item[\ttindexbold{REPEAT_SOME} {\it tacf}] 
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   450
applies {\it tacf} once or more to a subgoal, counting downwards.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   451
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   452
\item[\ttindexbold{REPEAT_FIRST} {\it tacf}] 
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   453
applies {\it tacf} once or more to a subgoal, counting upwards.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   454
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   455
\item[\ttindexbold{trace_goalno_tac} {\it tac} {\it i}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   456
applies \hbox{\it tac i\/} to the proof state.  If the resulting sequence
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   457
is non-empty, then it is returned, with the side-effect of printing {\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   458
Subgoal~$i$ selected}.  Otherwise, {\tt trace_goalno_tac} returns the empty
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   459
sequence and prints nothing.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   460
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   461
It indicates that `the tactic worked for subgoal~$i$' and is mainly used
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   462
with {\tt SOMEGOAL} and {\tt FIRSTGOAL}.
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   463
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   464
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   465
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   466
\subsection{Joining tactic functions}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   467
\index{tacticals!joining tactic functions}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   468
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   469
THEN'     : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic \hfill{\bf infix 1}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   470
ORELSE'   : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic \hfill{\bf infix}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   471
APPEND'   : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic \hfill{\bf infix}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   472
INTLEAVE' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic \hfill{\bf infix}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   473
EVERY'    : ('a -> tactic) list -> 'a -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   474
FIRST'    : ('a -> tactic) list -> 'a -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   475
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   476
These help to express tactics that specify subgoal numbers.  The tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   477
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   478
SOMEGOAL (fn i => resolve_tac rls i  ORELSE  eresolve_tac erls i)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   479
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   480
can be simplified to
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   481
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   482
SOMEGOAL (resolve_tac rls  ORELSE'  eresolve_tac erls)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   483
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   484
Note that {\tt TRY'}, {\tt REPEAT'}, {\tt DEPTH_FIRST'}, etc.\ are not
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   485
provided, because function composition accomplishes the same purpose.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   486
The tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   487
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   488
ALLGOALS (fn i => REPEAT (etac exE i  ORELSE  atac i))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   489
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   490
can be simplified to
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   491
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   492
ALLGOALS (REPEAT o (etac exE  ORELSE'  atac))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   493
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   494
These tacticals are polymorphic; $x$ need not be an integer.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   495
\begin{center} \tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   496
\begin{tabular}{r@{\rm\ \ yields\ \ }l}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   497
    $(tacf@1$~~THEN'~~$tacf@2)(x)$ \index{*THEN'} &
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   498
    $tacf@1(x)$~~THEN~~$tacf@2(x)$ \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   499
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   500
    $(tacf@1$ ORELSE' $tacf@2)(x)$ \index{*ORELSE'} &
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   501
    $tacf@1(x)$ ORELSE $tacf@2(x)$ \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   502
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   503
    $(tacf@1$ APPEND' $tacf@2)(x)$ \index{*APPEND'} &
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   504
    $tacf@1(x)$ APPEND $tacf@2(x)$ \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   505
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   506
    $(tacf@1$ INTLEAVE' $tacf@2)(x)$ \index{*INTLEAVE'} &
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   507
    $tacf@1(x)$ INTLEAVE $tacf@2(x)$ \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   508
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   509
    EVERY' $[tacf@1,\ldots,tacf@n] \; (x)$ \index{*EVERY'} &
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   510
    EVERY $[tacf@1(x),\ldots,tacf@n(x)]$ \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   511
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   512
    FIRST' $[tacf@1,\ldots,tacf@n] \; (x)$ \index{*FIRST'} &
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   513
    FIRST $[tacf@1(x),\ldots,tacf@n(x)]$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   514
\end{tabular}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   515
\end{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   516
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   517
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   518
\subsection{Applying a list of tactics to 1}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   519
\index{tacticals!joining tactic functions}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   520
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   521
EVERY1: (int -> tactic) list -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   522
FIRST1: (int -> tactic) list -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   523
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   524
A common proof style is to treat the subgoals as a stack, always
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   525
restricting attention to the first subgoal.  Such proofs contain long lists
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   526
of tactics, each applied to~1.  These can be simplified using {\tt EVERY1}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   527
and {\tt FIRST1}:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   528
\begin{center} \tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   529
\begin{tabular}{r@{\rm\ \ abbreviates\ \ }l}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   530
    EVERY1 $[tacf@1,\ldots,tacf@n]$ \indexbold{*EVERY1} &
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   531
    EVERY $[tacf@1(1),\ldots,tacf@n(1)]$ \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   532
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   533
    FIRST1 $[tacf@1,\ldots,tacf@n]$ \indexbold{*FIRST1} &
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   534
    FIRST $[tacf@1(1),\ldots,tacf@n(1)]$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   535
\end{tabular}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   536
\end{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   537
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   538
\index{tacticals|)}
5371
e27558a68b8d emacs local vars;
wenzelm
parents: 4317
diff changeset
   539
e27558a68b8d emacs local vars;
wenzelm
parents: 4317
diff changeset
   540
e27558a68b8d emacs local vars;
wenzelm
parents: 4317
diff changeset
   541
%%% Local Variables: 
e27558a68b8d emacs local vars;
wenzelm
parents: 4317
diff changeset
   542
%%% mode: latex
e27558a68b8d emacs local vars;
wenzelm
parents: 4317
diff changeset
   543
%%% TeX-master: "ref"
e27558a68b8d emacs local vars;
wenzelm
parents: 4317
diff changeset
   544
%%% End: