doc-src/Ref/tactic.tex
author lcp
Mon, 21 Mar 1994 11:02:57 +0100
changeset 286 e7efbf03562b
parent 104 d8205bb279a7
child 323 361a71713176
permissions -rw-r--r--
first draft of Springer book
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     1
%% $Id$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     2
\chapter{Tactics} \label{tactics}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     3
\index{tactics|(}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     4
Tactics have type \ttindexbold{tactic}.  They are essentially
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     5
functions from theorems to theorem sequences, where the theorems represent
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     6
states of a backward proof.  Tactics seldom need to be coded from scratch,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     7
as functions; the basic tactics suffice for most proofs.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     8
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     9
\section{Resolution and assumption tactics}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    10
{\bf Resolution} is Isabelle's basic mechanism for refining a subgoal using
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    11
a rule.  {\bf Elim-resolution} is particularly suited for elimination
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    12
rules, while {\bf destruct-resolution} is particularly suited for
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    13
destruction rules.  The {\tt r}, {\tt e}, {\tt d} naming convention is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    14
maintained for several different kinds of resolution tactics, as well as
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    15
the shortcuts in the subgoal module.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    16
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    17
All the tactics in this section act on a subgoal designated by a positive
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    18
integer~$i$.  They fail (by returning the empty sequence) if~$i$ is out of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    19
range.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    20
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    21
\subsection{Resolution tactics}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    22
\index{tactics!resolution|bold}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    23
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    24
resolve_tac  : thm list -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    25
eresolve_tac : thm list -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    26
dresolve_tac : thm list -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    27
forward_tac  : thm list -> int -> tactic 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    28
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    29
These perform resolution on a list of theorems, $thms$, representing a list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    30
of object-rules.  When generating next states, they take each of the rules
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    31
in the order given.  Each rule may yield several next states, or none:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    32
higher-order resolution may yield multiple resolvents.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    33
\begin{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    34
\item[\ttindexbold{resolve_tac} {\it thms} {\it i}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    35
refines the proof state using the object-rules, which should normally be
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    36
introduction rules.  It resolves an object-rule's conclusion with
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    37
subgoal~$i$ of the proof state.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    38
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    39
\item[\ttindexbold{eresolve_tac} {\it thms} {\it i}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    40
refines the proof state by elim-resolution with the object-rules, which
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    41
should normally be elimination rules.  It resolves with a rule, solves
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    42
its first premise by assumption, and finally {\bf deletes} that assumption
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    43
from any new subgoals.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    44
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    45
\item[\ttindexbold{dresolve_tac} {\it thms} {\it i}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    46
performs destruct-resolution with the object-rules, which normally should
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    47
be destruction rules.  This replaces an assumption by the result of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    48
applying one of the rules.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    49
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    50
\item[\ttindexbold{forward_tac}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    51
is like \ttindex{dresolve_tac} except that the selected assumption is not
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    52
deleted.  It applies a rule to an assumption, adding the result as a new
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    53
assumption.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    54
\end{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    55
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    56
\subsection{Assumption tactics}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    57
\index{tactics!assumption|bold}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    58
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    59
assume_tac    : int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    60
eq_assume_tac : int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    61
\end{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    62
\begin{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    63
\item[\ttindexbold{assume_tac} {\it i}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    64
attempts to solve subgoal~$i$ by assumption.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    65
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    66
\item[\ttindexbold{eq_assume_tac}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    67
is like {\tt assume_tac} but does not use unification.  It succeeds (with a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    68
{\bf unique} next state) if one of the assumptions is identical to the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    69
subgoal's conclusion.  Since it does not instantiate variables, it cannot
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    70
make other subgoals unprovable.  It is intended to be called from proof
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    71
strategies, not interactively.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    72
\end{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    73
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    74
\subsection{Matching tactics} \label{match_tac}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    75
\index{tactics!matching|bold}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    76
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    77
match_tac  : thm list -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    78
ematch_tac : thm list -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    79
dmatch_tac : thm list -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    80
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    81
These are just like the resolution tactics except that they never
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    82
instantiate unknowns in the proof state.  Flexible subgoals are not updated
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    83
willy-nilly, but are left alone.  Matching --- strictly speaking --- means
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    84
treating the unknowns in the proof state as constants; these tactics merely
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    85
discard unifiers that would update the proof state.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    86
\begin{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    87
\item[\ttindexbold{match_tac} {\it thms} {\it i}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    88
refines the proof state using the object-rules, matching an object-rule's
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    89
conclusion with subgoal~$i$ of the proof state.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    90
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    91
\item[\ttindexbold{ematch_tac}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    92
is like {\tt match_tac}, but performs elim-resolution.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    93
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    94
\item[\ttindexbold{dmatch_tac}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    95
is like {\tt match_tac}, but performs destruct-resolution.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    96
\end{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    97
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    98
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    99
\subsection{Resolution with instantiation} \label{res_inst_tac}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   100
\index{tactics!instantiation|bold}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   101
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   102
res_inst_tac  : (string*string)list -> thm -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   103
eres_inst_tac : (string*string)list -> thm -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   104
dres_inst_tac : (string*string)list -> thm -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   105
forw_inst_tac : (string*string)list -> thm -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   106
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   107
These tactics are designed for applying rules such as substitution and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   108
induction, which cause difficulties for higher-order unification.  The
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   109
tactics accept explicit instantiations for schematic variables in the rule
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   110
--- typically, in the rule's conclusion.  Each instantiation is a pair
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   111
{\tt($v$,$e$)}, where $v$ can be a type variable or ordinary variable:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   112
\begin{itemize}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   113
\item If $v$ is the {\bf type variable} {\tt'a}, then
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   114
the rule must contain a schematic type variable \verb$?'a$ of some
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   115
sort~$s$, and $e$ should be a type of sort $s$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   116
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   117
\item If $v$ is the {\bf variable} {\tt P}, then
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   118
the rule must contain a schematic variable \verb$?P$ of some type~$\tau$,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   119
and $e$ should be a term of some type~$\sigma$ such that $\tau$ and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   120
$\sigma$ are unifiable.  If the unification of $\tau$ and $\sigma$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   121
instantiates any schematic type variables in $\tau$, these instantiations
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   122
are recorded for application to the rule.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   123
\end{itemize}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   124
Types are instantiated before terms.  Because type instantiations are
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   125
inferred from term instantiations, explicit type instantiations are seldom
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   126
necessary --- if \verb$?t$ has type \verb$?'a$, then the instantiation list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   127
\verb$[("'a","bool"),("t","True")]$ may be simplified to
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   128
\verb$[("t","True")]$.  Type unknowns in the proof state may cause
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   129
failure because the tactics cannot instantiate them.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   130
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   131
The instantiation tactics act on a given subgoal.  Terms in the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   132
instantiations are type-checked in the context of that subgoal --- in
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   133
particular, they may refer to that subgoal's parameters.  Any unknowns in
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   134
the terms receive subscripts and are lifted over the parameters; thus, you
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   135
may not refer to unknowns in the subgoal.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   136
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   137
\begin{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   138
\item[\ttindexbold{res_inst_tac} {\it insts} {\it thm} {\it i}]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   139
instantiates the rule {\it thm} with the instantiations {\it insts}, as
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   140
described above, and then performs resolution on subgoal~$i$.  Resolution
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   141
typically causes further instantiations; you need not give explicit
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   142
instantiations for every variable in the rule.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   143
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   144
\item[\ttindexbold{eres_inst_tac}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   145
is like {\tt res_inst_tac}, but performs elim-resolution.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   146
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   147
\item[\ttindexbold{dres_inst_tac}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   148
is like {\tt res_inst_tac}, but performs destruct-resolution.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   149
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   150
\item[\ttindexbold{forw_inst_tac}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   151
is like {\tt dres_inst_tac} except that the selected assumption is not
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   152
deleted.  It applies the instantiated rule to an assumption, adding the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   153
result as a new assumption.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   154
\end{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   155
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   156
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   157
\section{Other basic tactics}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   158
\subsection{Definitions and meta-level rewriting}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   159
\index{tactics!meta-rewriting|bold}\index{rewriting!meta-level}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   160
Definitions in Isabelle have the form $t\equiv u$, where typically $t$ is a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   161
constant or a constant applied to a list of variables, for example $\it
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   162
sqr(n)\equiv n\times n$.  (Conditional definitions, $\phi\Imp t\equiv u$,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   163
are not supported.)  {\bf Unfolding} the definition $t\equiv u$ means using
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   164
it as a rewrite rule, replacing~$t$ by~$u$ throughout a theorem.  {\bf
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   165
Folding} $t\equiv u$ means replacing~$u$ by~$t$.  Rewriting continues until
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   166
no rewrites are applicable to any subterm.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   167
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   168
There are rules for unfolding and folding definitions; Isabelle does not do
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   169
this automatically.  The corresponding tactics rewrite the proof state,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   170
yielding a unique result.  See also the {\tt goalw} command, which is the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   171
easiest way of handling definitions.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   172
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   173
rewrite_goals_tac : thm list -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   174
rewrite_tac       : thm list -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   175
fold_goals_tac    : thm list -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   176
fold_tac          : thm list -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   177
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   178
\begin{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   179
\item[\ttindexbold{rewrite_goals_tac} {\it defs}]  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   180
unfolds the {\it defs} throughout the subgoals of the proof state, while
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   181
leaving the main goal unchanged.  Use \ttindex{SELECT_GOAL} to restrict it to a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   182
particular subgoal.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   183
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   184
\item[\ttindexbold{rewrite_tac} {\it defs}]  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   185
unfolds the {\it defs} throughout the proof state, including the main goal
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   186
--- not normally desirable!
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   187
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   188
\item[\ttindexbold{fold_goals_tac} {\it defs}]  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   189
folds the {\it defs} throughout the subgoals of the proof state, while
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   190
leaving the main goal unchanged.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   191
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   192
\item[\ttindexbold{fold_tac} {\it defs}]  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   193
folds the {\it defs} throughout the proof state.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   194
\end{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   195
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   196
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   197
\subsection{Tactic shortcuts}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   198
\index{shortcuts!for tactics|bold}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   199
\index{tactics!resolution}\index{tactics!assumption}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   200
\index{tactics!meta-rewriting}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   201
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   202
rtac     : thm -> int ->tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   203
etac     : thm -> int ->tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   204
dtac     : thm -> int ->tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   205
atac     : int ->tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   206
ares_tac : thm list -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   207
rewtac   : thm -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   208
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   209
These abbreviate common uses of tactics.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   210
\begin{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   211
\item[\ttindexbold{rtac} {\it thm} {\it i}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   212
abbreviates \hbox{\tt resolve_tac [{\it thm}] {\it i}}, doing resolution.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   213
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   214
\item[\ttindexbold{etac} {\it thm} {\it i}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   215
abbreviates \hbox{\tt eresolve_tac [{\it thm}] {\it i}}, doing elim-resolution.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   216
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   217
\item[\ttindexbold{dtac} {\it thm} {\it i}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   218
abbreviates \hbox{\tt dresolve_tac [{\it thm}] {\it i}}, doing
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   219
destruct-resolution.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   220
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   221
\item[\ttindexbold{atac} {\it i}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   222
is a synonym for \hbox{\tt assume_tac {\it i}}, doing proof by assumption.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   223
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   224
\item[\ttindexbold{ares_tac} {\it thms} {\it i}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   225
tries proof by assumption and resolution; it abbreviates
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   226
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   227
assume_tac {\it i} ORELSE resolve_tac {\it thms} {\it i}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   228
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   229
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   230
\item[\ttindexbold{rewtac} {\it def}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   231
abbreviates \hbox{\tt rewrite_goals_tac [{\it def}]}, unfolding a definition.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   232
\end{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   233
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   234
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   235
\subsection{Inserting premises and facts}\label{cut_facts_tac}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   236
\index{tactics!for inserting facts|bold}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   237
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   238
cut_facts_tac : thm list -> int -> tactic
286
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   239
cut_inst_tac  : (string*string)list -> thm -> int -> tactic
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   240
subgoal_tac   : string -> int -> tactic
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   241
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   242
These tactics add assumptions --- which must be proved, sooner or later ---
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   243
to a given subgoal.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   244
\begin{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   245
\item[\ttindexbold{cut_facts_tac} {\it thms} {\it i}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   246
  adds the {\it thms} as new assumptions to subgoal~$i$.  Once they have
286
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   247
  been inserted as assumptions, they become subject to tactics such as {\tt
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   248
    eresolve_tac} and {\tt rewrite_goals_tac}.  Only rules with no premises
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   249
  are inserted: Isabelle cannot use assumptions that contain $\Imp$
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   250
  or~$\Forall$.  Sometimes the theorems are premises of a rule being
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   251
  derived, returned by~{\tt goal}; instead of calling this tactic, you
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   252
  could state the goal with an outermost meta-quantifier.
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   253
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   254
\item[\ttindexbold{cut_inst_tac} {\it insts} {\it thm} {\it i}]
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   255
  instantiates the {\it thm} with the instantiations {\it insts}, as
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   256
  described in \S\ref{res_inst_tac}.  It adds the resulting theorem as a
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   257
  new assumption to subgoal~$i$. 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   258
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   259
\item[\ttindexbold{subgoal_tac} {\it formula} {\it i}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   260
adds the {\it formula} as a assumption to subgoal~$i$, and inserts the same
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   261
{\it formula} as a new subgoal, $i+1$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   262
\end{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   263
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   264
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   265
\subsection{Theorems useful with tactics}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   266
\index{theorems!of pure theory|bold}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   267
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   268
asm_rl: thm 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   269
cut_rl: thm 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   270
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   271
\begin{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   272
\item[\ttindexbold{asm_rl}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   273
is $\psi\Imp\psi$.  Under elim-resolution it does proof by assumption, and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   274
\hbox{\tt eresolve_tac (asm_rl::{\it thms}) {\it i}} is equivalent to
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   275
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   276
assume_tac {\it i}  ORELSE  eresolve_tac {\it thms} {\it i}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   277
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   278
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   279
\item[\ttindexbold{cut_rl}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   280
is $\List{\psi\Imp\theta,\psi}\Imp\theta$.  It is useful for inserting
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   281
assumptions; it underlies \ttindex{forward_tac}, \ttindex{cut_facts_tac}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   282
and \ttindex{subgoal_tac}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   283
\end{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   284
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   285
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   286
\section{Obscure tactics}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   287
\subsection{Tidying the proof state}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   288
\index{parameters!removing unused|bold}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   289
\index{flex-flex constraints}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   290
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   291
prune_params_tac : tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   292
flexflex_tac     : tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   293
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   294
\begin{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   295
\item[\ttindexbold{prune_params_tac}]  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   296
  removes unused parameters from all subgoals of the proof state.  It works
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   297
  by rewriting with the theorem $(\Forall x. V)\equiv V$.  This tactic can
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   298
  make the proof state more readable.  It is used with
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   299
  \ttindex{rule_by_tactic} to simplify the resulting theorem.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   300
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   301
\item[\ttindexbold{flexflex_tac}]  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   302
  removes all flex-flex pairs from the proof state by applying the trivial
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   303
  unifier.  This drastic step loses information, and should only be done as
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   304
  the last step of a proof.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   305
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   306
  Flex-flex constraints arise from difficult cases of higher-order
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   307
  unification.  To prevent this, use \ttindex{res_inst_tac} to instantiate
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   308
  some variables in a rule~(\S\ref{res_inst_tac}).  Normally flex-flex
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   309
  constraints can be ignored; they often disappear as unknowns get
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   310
  instantiated.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   311
\end{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   312
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   313
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   314
\subsection{Renaming parameters in a goal} \index{parameters!renaming|bold}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   315
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   316
rename_tac        : string -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   317
rename_last_tac   : string -> string list -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   318
Logic.set_rename_prefix : string -> unit
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   319
Logic.auto_rename       : bool ref      \hfill{\bf initially false}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   320
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   321
When creating a parameter, Isabelle chooses its name by matching variable
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   322
names via the object-rule.  Given the rule $(\forall I)$ formalized as
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   323
$\left(\Forall x. P(x)\right) \Imp \forall x.P(x)$, Isabelle will note that
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   324
the $\Forall$-bound variable in the premise has the same name as the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   325
$\forall$-bound variable in the conclusion.  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   326
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   327
Sometimes there is insufficient information and Isabelle chooses an
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   328
arbitrary name.  The renaming tactics let you override Isabelle's choice.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   329
Because renaming parameters has no logical effect on the proof state, the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   330
{\tt by} command prints the needless message {\tt Warning:\ same as previous
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   331
level}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   332
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   333
Alternatively, you can suppress the naming mechanism described above and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   334
have Isabelle generate uniform names for parameters.  These names have the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   335
form $p${\tt a}, $p${\tt b}, $p${\tt c},~\ldots, where $p$ is any desired
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   336
prefix.  They are ugly but predictable.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   337
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   338
\begin{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   339
\item[\ttindexbold{rename_tac} {\it str} {\it i}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   340
interprets the string {\it str} as a series of blank-separated variable
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   341
names, and uses them to rename the parameters of subgoal~$i$.  The names
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   342
must be distinct.  If there are fewer names than parameters, then the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   343
tactic renames the innermost parameters and may modify the remaining ones
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   344
to ensure that all the parameters are distinct.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   345
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   346
\item[\ttindexbold{rename_last_tac} {\it prefix} {\it suffixes} {\it i}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   347
generates a list of names by attaching each of the {\it suffixes\/} to the 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   348
{\it prefix}.  It is intended for coding structural induction tactics,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   349
where several of the new parameters should have related names.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   350
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   351
\item[\ttindexbold{Logic.set_rename_prefix} {\it prefix};] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   352
sets the prefix for uniform renaming to~{\it prefix}.  The default prefix
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   353
is {\tt"k"}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   354
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   355
\item[\ttindexbold{Logic.auto_rename} \tt:= true;] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   356
makes Isabelle generate uniform names for parameters. 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   357
\end{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   358
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   359
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   360
\subsection{Composition: resolution without lifting}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   361
\index{tactics!for composition|bold}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   362
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   363
compose_tac: (bool * thm * int) -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   364
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   365
{\bf Composing} two rules means to resolve them without prior lifting or
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   366
renaming of unknowns.  This low-level operation, which underlies the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   367
resolution tactics, may occasionally be useful for special effects.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   368
A typical application is \ttindex{res_inst_tac}, which lifts and instantiates a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   369
rule, then passes the result to {\tt compose_tac}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   370
\begin{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   371
\item[\ttindexbold{compose_tac} ($flag$, $rule$, $m$) $i$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   372
refines subgoal~$i$ using $rule$, without lifting.  The $rule$ is taken to
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   373
have the form $\List{\psi@1; \ldots; \psi@m} \Imp \psi$, where $\psi$ need
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   374
{\bf not} be atomic; thus $m$ determines the number of new subgoals.  If
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   375
$flag$ is {\tt true} then it performs elim-resolution --- it solves the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   376
first premise of~$rule$ by assumption and deletes that assumption.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   377
\end{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   378
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   379
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   380
\section{Managing lots of rules}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   381
These operations are not intended for interactive use.  They are concerned
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   382
with the processing of large numbers of rules in automatic proof
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   383
strategies.  Higher-order resolution involving a long list of rules is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   384
slow.  Filtering techniques can shorten the list of rules given to
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   385
resolution, and can also detect whether a given subgoal is too flexible,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   386
with too many rules applicable.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   387
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   388
\subsection{Combined resolution and elim-resolution} \label{biresolve_tac}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   389
\index{tactics!resolution}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   390
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   391
biresolve_tac   : (bool*thm)list -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   392
bimatch_tac     : (bool*thm)list -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   393
subgoals_of_brl : bool*thm -> int
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   394
lessb           : (bool*thm) * (bool*thm) -> bool
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   395
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   396
{\bf Bi-resolution} takes a list of $\it (flag,rule)$ pairs.  For each
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   397
pair, it applies resolution if the flag is~{\tt false} and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   398
elim-resolution if the flag is~{\tt true}.  A single tactic call handles a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   399
mixture of introduction and elimination rules.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   400
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   401
\begin{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   402
\item[\ttindexbold{biresolve_tac} {\it brls} {\it i}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   403
refines the proof state by resolution or elim-resolution on each rule, as
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   404
indicated by its flag.  It affects subgoal~$i$ of the proof state.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   405
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   406
\item[\ttindexbold{bimatch_tac}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   407
is like {\tt biresolve_tac}, but performs matching: unknowns in the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   408
proof state are never updated (see~\S\ref{match_tac}).
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   409
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   410
\item[\ttindexbold{subgoals_of_brl}({\it flag},{\it rule})] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   411
returns the number of new subgoals that bi-resolution would yield for the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   412
pair (if applied to a suitable subgoal).  This is $n$ if the flag is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   413
{\tt false} and $n-1$ if the flag is {\tt true}, where $n$ is the number
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   414
of premises of the rule.  Elim-resolution yields one fewer subgoal than
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   415
ordinary resolution because it solves the major premise by assumption.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   416
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   417
\item[\ttindexbold{lessb} ({\it brl1},{\it brl2})] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   418
returns the result of 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   419
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   420
subgoals_of_brl {\it brl1} < subgoals_of_brl {\it brl2}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   421
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   422
Note that \hbox{\tt sort lessb {\it brls}} sorts a list of $\it
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   423
(flag,rule)$ pairs by the number of new subgoals they will yield.  Thus,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   424
those that yield the fewest subgoals should be tried first.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   425
\end{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   426
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   427
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   428
\subsection{Discrimination nets for fast resolution}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   429
\index{discrimination nets|bold}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   430
\index{tactics!resolution}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   431
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   432
net_resolve_tac  : thm list -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   433
net_match_tac    : thm list -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   434
net_biresolve_tac: (bool*thm) list -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   435
net_bimatch_tac  : (bool*thm) list -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   436
filt_resolve_tac : thm list -> int -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   437
could_unify      : term*term->bool
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   438
filter_thms      : (term*term->bool) -> int*term*thm list -> thm list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   439
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   440
The module \ttindex{Net} implements a discrimination net data structure for
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   441
fast selection of rules \cite[Chapter 14]{charniak80}.  A term is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   442
classified by the symbol list obtained by flattening it in preorder.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   443
The flattening takes account of function applications, constants, and free
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   444
and bound variables; it identifies all unknowns and also regards
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   445
$\lambda$-abstractions as unknowns, since they could $\eta$-contract to
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   446
anything.  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   447
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   448
A discrimination net serves as a polymorphic dictionary indexed by terms.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   449
The module provides various functions for inserting and removing items from
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   450
nets.  It provides functions for returning all items whose term could match
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   451
or unify with a target term.  The matching and unification tests are
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   452
overly lax (due to the identifications mentioned above) but they serve as
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   453
useful filters.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   454
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   455
A net can store introduction rules indexed by their conclusion, and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   456
elimination rules indexed by their major premise.  Isabelle provides
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   457
several functions for ``compiling'' long lists of rules into fast
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   458
resolution tactics.  When supplied with a list of theorems, these functions
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   459
build a discrimination net; the net is used when the tactic is applied to a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   460
goal.  To avoid repreatedly constructing the nets, use currying: bind the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   461
resulting tactics to \ML{} identifiers.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   462
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   463
\begin{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   464
\item[\ttindexbold{net_resolve_tac} {\it thms}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   465
builds a discrimination net to obtain the effect of a similar call to {\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   466
resolve_tac}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   467
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   468
\item[\ttindexbold{net_match_tac} {\it thms}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   469
builds a discrimination net to obtain the effect of a similar call to {\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   470
match_tac}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   471
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   472
\item[\ttindexbold{net_biresolve_tac} {\it brls}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   473
builds a discrimination net to obtain the effect of a similar call to {\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   474
biresolve_tac}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   475
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   476
\item[\ttindexbold{net_bimatch_tac} {\it brls}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   477
builds a discrimination net to obtain the effect of a similar call to {\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   478
bimatch_tac}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   479
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   480
\item[\ttindexbold{filt_resolve_tac} {\it thms} {\it maxr} {\it i}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   481
uses discrimination nets to extract the {\it thms} that are applicable to
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   482
subgoal~$i$.  If more than {\it maxr\/} theorems are applicable then the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   483
tactic fails.  Otherwise it calls {\tt resolve_tac}.  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   484
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   485
This tactic helps avoid runaway instantiation of unknowns, for example in
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   486
type inference.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   487
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   488
\item[\ttindexbold{could_unify} ({\it t},{\it u})] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   489
returns {\tt false} if~$t$ and~$u$ are ``obviously'' non-unifiable, and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   490
otherwise returns~{\tt true}.  It assumes all variables are distinct,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   491
reporting that {\tt ?a=?a} may unify with {\tt 0=1}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   492
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   493
\item[\ttindexbold{filter_thms} $could\; (limit,prem,thms)$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   494
returns the list of potentially resolvable rules (in {\it thms\/}) for the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   495
subgoal {\it prem}, using the predicate {\it could\/} to compare the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   496
conclusion of the subgoal with the conclusion of each rule.  The resulting list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   497
is no longer than {\it limit}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   498
\end{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   499
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   500
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   501
\section{Programming tools for proof strategies}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   502
Do not consider using the primitives discussed in this section unless you
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   503
really need to code tactics from scratch,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   504
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   505
\subsection{Operations on type {\tt tactic}}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   506
\index{tactics!primitives for coding|bold}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   507
A tactic maps theorems to theorem sequences (lazy lists).  The type
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   508
constructor for sequences is called \ttindex{Sequence.seq}.  To simplify the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   509
types of tactics and tacticals, Isabelle defines a type of tactics:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   510
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   511
datatype tactic = Tactic of thm -> thm Sequence.seq
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   512
\end{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   513
{\tt Tactic} and {\tt tapply} convert between tactics and functions.  The
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   514
other operations provide means for coding tactics in a clean style.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   515
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   516
tapply    : tactic * thm -> thm Sequence.seq
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   517
Tactic    :     (thm -> thm Sequence.seq) -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   518
PRIMITIVE :                  (thm -> thm) -> tactic  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   519
STATE     :               (thm -> tactic) -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   520
SUBGOAL   : ((term*int) -> tactic) -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   521
\end{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   522
\begin{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   523
\item[\ttindexbold{tapply} {\it tac} {\it thm}]  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   524
returns the result of applying the tactic, as a function, to {\it thm}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   525
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   526
\item[\ttindexbold{Tactic} {\it f}]  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   527
packages {\it f} as a tactic.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   528
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   529
\item[\ttindexbold{PRIMITIVE} $f$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   530
applies $f$ to the proof state and returns the result as a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   531
one-element sequence.  This packages the meta-rule~$f$ as a tactic.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   532
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   533
\item[\ttindexbold{STATE} $f$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   534
applies $f$ to the proof state and then applies the resulting tactic to the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   535
same state.  It supports the following style, where the tactic body is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   536
expressed at a high level, but may peek at the proof state:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   537
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   538
STATE (fn state => {\it some tactic})
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   539
\end{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   540
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   541
\item[\ttindexbold{SUBGOAL} $f$ $i$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   542
extracts subgoal~$i$ from the proof state as a term~$t$, and computes a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   543
tactic by calling~$f(t,i)$.  It applies the resulting tactic to the same
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   544
state.  The tactic body is expressed at a high level, but may peek at a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   545
particular subgoal:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   546
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   547
SUBGOAL (fn (t,i) => {\it some tactic})
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   548
\end{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   549
\end{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   550
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   551
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   552
\subsection{Tracing}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   553
\index{tactics!tracing|bold}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   554
\index{tracing!of tactics}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   555
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   556
pause_tac: tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   557
print_tac: tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   558
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   559
These violate the functional behaviour of tactics by printing information
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   560
when they are applied to a proof state.  Their output may be difficult to
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   561
interpret.  Note that certain of the searching tacticals, such as {\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   562
REPEAT}, have built-in tracing options.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   563
\begin{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   564
\item[\ttindexbold{pause_tac}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   565
prints {\tt** Press RETURN to continue:} and then reads a line from the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   566
terminal.  If this line is blank then it returns the proof state unchanged;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   567
otherwise it fails (which may terminate a repetition).
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   568
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   569
\item[\ttindexbold{print_tac}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   570
returns the proof state unchanged, with the side effect of printing it at
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   571
the terminal.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   572
\end{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   573
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   574
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   575
\subsection{Sequences}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   576
\index{sequences (lazy lists)|bold}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   577
The module \ttindex{Sequence} declares a type of lazy lists.  It uses
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   578
Isabelle's type \ttindexbold{option} to represent the possible presence
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   579
(\ttindexbold{Some}) or absence (\ttindexbold{None}) of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   580
a value:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   581
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   582
datatype 'a option = None  |  Some of 'a;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   583
\end{ttbox}
286
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   584
For clarity, the module name {\tt Sequence} is omitted from the signature
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   585
specifications below; for instance, {\tt null} appears instead of {\tt
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   586
  Sequence.null}.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   587
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   588
\subsubsection{Basic operations on sequences}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   589
\begin{ttbox} 
286
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   590
null   : 'a seq
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   591
seqof  : (unit -> ('a * 'a seq) option) -> 'a seq
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   592
single : 'a -> 'a seq
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   593
pull   : 'a seq -> ('a * 'a seq) option
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   594
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   595
\begin{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   596
\item[{\tt Sequence.null}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   597
is the empty sequence.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   598
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   599
\item[\tt Sequence.seqof (fn()=> Some($x$,$s$))] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   600
constructs the sequence with head~$x$ and tail~$s$, neither of which is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   601
evaluated.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   602
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   603
\item[{\tt Sequence.single} $x$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   604
constructs the sequence containing the single element~$x$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   605
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   606
\item[{\tt Sequence.pull} $s$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   607
returns {\tt None} if the sequence is empty and {\tt Some($x$,$s'$)} if the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   608
sequence has head~$x$ and tail~$s'$.  Warning: calling \hbox{Sequence.pull
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   609
$s$} again will {\bf recompute} the value of~$x$; it is not stored!
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   610
\end{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   611
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   612
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   613
\subsubsection{Converting between sequences and lists}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   614
\begin{ttbox} 
286
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   615
chop      : int * 'a seq -> 'a list * 'a seq
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   616
list_of_s : 'a seq -> 'a list
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   617
s_of_list : 'a list -> 'a seq
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   618
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   619
\begin{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   620
\item[{\tt Sequence.chop} ($n$, $s$)] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   621
returns the first~$n$ elements of~$s$ as a list, paired with the remaining
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   622
elements of~$s$.  If $s$ has fewer than~$n$ elements, then so will the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   623
list.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   624
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   625
\item[{\tt Sequence.list_of_s} $s$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   626
returns the elements of~$s$, which must be finite, as a list.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   627
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   628
\item[{\tt Sequence.s_of_list} $l$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   629
creates a sequence containing the elements of~$l$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   630
\end{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   631
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   632
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   633
\subsubsection{Combining sequences}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   634
\begin{ttbox} 
286
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   635
append     : 'a seq * 'a seq -> 'a seq
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   636
interleave : 'a seq * 'a seq -> 'a seq
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   637
flats      : 'a seq seq -> 'a seq
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   638
maps       : ('a -> 'b) -> 'a seq -> 'b seq
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   639
filters    : ('a -> bool) -> 'a seq -> 'a seq
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   640
\end{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   641
\begin{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   642
\item[{\tt Sequence.append} ($s@1$, $s@2$)] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   643
concatenates $s@1$ to $s@2$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   644
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   645
\item[{\tt Sequence.interleave} ($s@1$, $s@2$)] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   646
joins $s@1$ with $s@2$ by interleaving their elements.  The result contains
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   647
all the elements of the sequences, even if both are infinite.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   648
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   649
\item[{\tt Sequence.flats} $ss$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   650
concatenates a sequence of sequences.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   651
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   652
\item[{\tt Sequence.maps} $f$ $s$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   653
applies $f$ to every element of~$s=x@1,x@2,\ldots$, yielding the sequence
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   654
$f(x@1),f(x@2),\ldots$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   655
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   656
\item[{\tt Sequence.filters} $p$ $s$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   657
returns the sequence consisting of all elements~$x$ of~$s$ such that $p(x)$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   658
is {\tt true}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   659
\end{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   660
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   661
\index{tactics|)}