doc-src/Ref/tactic.tex
author wenzelm
Sun, 29 Jan 2012 22:12:25 +0100
changeset 46278 408e3acfdbb9
parent 46277 aea65ff733b4
child 46295 2548a85b0e02
permissions -rw-r--r--
updated hint about asm_rl;
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: 17818
diff changeset
     1
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     2
\chapter{Tactics} \label{tactics}
30184
37969710e61f removed parts of the manual that are clearly obsolete, or covered by
wenzelm
parents: 17818
diff changeset
     3
\index{tactics|(}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     4
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     5
\section{Other basic tactics}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     6
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     7
\subsection{Inserting premises and facts}\label{cut_facts_tac}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
     8
\index{tactics!for inserting facts}\index{assumptions!inserting}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     9
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    10
cut_facts_tac : thm list -> int -> tactic
286
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
    11
cut_inst_tac  : (string*string)list -> thm -> int -> tactic
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    12
\end{ttbox}
2039
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    13
These tactics add assumptions to a subgoal.
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
    14
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    15
\item[\ttindexbold{cut_facts_tac} {\it thms} {\it i}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    16
  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
    17
  been inserted as assumptions, they become subject to tactics such as {\tt
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
    18
    eresolve_tac} and {\tt rewrite_goals_tac}.  Only rules with no premises
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
    19
  are inserted: Isabelle cannot use assumptions that contain $\Imp$
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
    20
  or~$\Forall$.  Sometimes the theorems are premises of a rule being
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
    21
  derived, returned by~{\tt goal}; instead of calling this tactic, you
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
    22
  could state the goal with an outermost meta-quantifier.
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
    23
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
    24
\item[\ttindexbold{cut_inst_tac} {\it insts} {\it thm} {\it i}]
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
    25
  instantiates the {\it thm} with the instantiations {\it insts}, as
7491
95a4af0e10a7 added ftac, eatac, datac, fatac
oheimb
parents: 6618
diff changeset
    26
  described in {\S}\ref{res_inst_tac}.  It adds the resulting theorem as a
286
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
    27
  new assumption to subgoal~$i$. 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    28
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
    29
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    30
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    31
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
    32
\subsection{Definitions and meta-level rewriting} \label{sec:rewrite_goals}
2039
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    33
\index{tactics!meta-rewriting|bold}\index{meta-rewriting|bold}
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    34
\index{definitions}
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    35
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    36
Definitions in Isabelle have the form $t\equiv u$, where $t$ is typically a
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    37
constant or a constant applied to a list of variables, for example $\it
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
    38
sqr(n)\equiv n\times n$.  Conditional definitions, $\phi\Imp t\equiv u$,
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
    39
are also supported.  {\bf Unfolding} the definition ${t\equiv u}$ means using
2039
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    40
it as a rewrite rule, replacing~$t$ by~$u$ throughout a theorem.  {\bf
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    41
Folding} $t\equiv u$ means replacing~$u$ by~$t$.  Rewriting continues until
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    42
no rewrites are applicable to any subterm.
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    43
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    44
There are rules for unfolding and folding definitions; Isabelle does not do
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    45
this automatically.  The corresponding tactics rewrite the proof state,
46257
3ba3681d8930 removed obscure/outdated material;
wenzelm
parents: 30184
diff changeset
    46
yielding a single next state.
2039
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    47
\begin{ttbox} 
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    48
rewrite_goals_tac : thm list -> tactic
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    49
fold_goals_tac    : thm list -> tactic
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    50
\end{ttbox}
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    51
\begin{ttdescription}
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    52
\item[\ttindexbold{rewrite_goals_tac} {\it defs}]  
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    53
unfolds the {\it defs} throughout the subgoals of the proof state, while
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    54
leaving the main goal unchanged.  Use \ttindex{SELECT_GOAL} to restrict it to a
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    55
particular subgoal.
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    56
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    57
\item[\ttindexbold{fold_goals_tac} {\it defs}]  
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    58
folds the {\it defs} throughout the subgoals of the proof state, while
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    59
leaving the main goal unchanged.
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    60
\end{ttdescription}
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    61
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
    62
\begin{warn}
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
    63
  These tactics only cope with definitions expressed as meta-level
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
    64
  equalities ($\equiv$).  More general equivalences are handled by the
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
    65
  simplifier, provided that it is set up appropriately for your logic
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
    66
  (see Chapter~\ref{chap:simplification}).
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
    67
\end{warn}
2039
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    68
1212
7059356e18e0 added rotate_tac
nipkow
parents: 457
diff changeset
    69
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    70
\subsection{Composition: resolution without lifting}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
    71
\index{tactics!for composition}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    72
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    73
compose_tac: (bool * thm * int) -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    74
\end{ttbox}
332
01b87a921967 final Springer copy
lcp
parents: 323
diff changeset
    75
{\bf Composing} two rules means resolving them without prior lifting or
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    76
renaming of unknowns.  This low-level operation, which underlies the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    77
resolution tactics, may occasionally be useful for special effects.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    78
A typical application is \ttindex{res_inst_tac}, which lifts and instantiates a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    79
rule, then passes the result to {\tt compose_tac}.
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
    80
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    81
\item[\ttindexbold{compose_tac} ($flag$, $rule$, $m$) $i$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    82
refines subgoal~$i$ using $rule$, without lifting.  The $rule$ is taken to
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    83
have the form $\List{\psi@1; \ldots; \psi@m} \Imp \psi$, where $\psi$ need
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
    84
not be atomic; thus $m$ determines the number of new subgoals.  If
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    85
$flag$ is {\tt true} then it performs elim-resolution --- it solves the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    86
first premise of~$rule$ by assumption and deletes that assumption.
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
    87
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    88
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    89
4276
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3950
diff changeset
    90
\section{*Managing lots of rules}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    91
These operations are not intended for interactive use.  They are concerned
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    92
with the processing of large numbers of rules in automatic proof
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    93
strategies.  Higher-order resolution involving a long list of rules is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    94
slow.  Filtering techniques can shorten the list of rules given to
2039
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    95
resolution, and can also detect whether a subgoal is too flexible,
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    96
with too many rules applicable.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    97
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    98
\subsection{Combined resolution and elim-resolution} \label{biresolve_tac}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    99
\index{tactics!resolution}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   100
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   101
biresolve_tac   : (bool*thm)list -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   102
bimatch_tac     : (bool*thm)list -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   103
subgoals_of_brl : bool*thm -> int
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   104
lessb           : (bool*thm) * (bool*thm) -> bool
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   105
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   106
{\bf Bi-resolution} takes a list of $\it (flag,rule)$ pairs.  For each
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   107
pair, it applies resolution if the flag is~{\tt false} and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   108
elim-resolution if the flag is~{\tt true}.  A single tactic call handles a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   109
mixture of introduction and elimination rules.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   110
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   111
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   112
\item[\ttindexbold{biresolve_tac} {\it brls} {\it i}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   113
refines the proof state by resolution or elim-resolution on each rule, as
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   114
indicated by its flag.  It affects subgoal~$i$ of the proof state.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   115
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   116
\item[\ttindexbold{bimatch_tac}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   117
is like {\tt biresolve_tac}, but performs matching: unknowns in the
7491
95a4af0e10a7 added ftac, eatac, datac, fatac
oheimb
parents: 6618
diff changeset
   118
proof state are never updated (see~{\S}\ref{match_tac}).
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   119
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   120
\item[\ttindexbold{subgoals_of_brl}({\it flag},{\it rule})] 
4597
a0bdee64194c Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents: 4317
diff changeset
   121
returns the number of new subgoals that bi-res\-o\-lu\-tion would yield for the
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   122
pair (if applied to a suitable subgoal).  This is $n$ if the flag is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   123
{\tt false} and $n-1$ if the flag is {\tt true}, where $n$ is the number
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   124
of premises of the rule.  Elim-resolution yields one fewer subgoal than
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   125
ordinary resolution because it solves the major premise by assumption.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   126
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   127
\item[\ttindexbold{lessb} ({\it brl1},{\it brl2})] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   128
returns the result of 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   129
\begin{ttbox}
332
01b87a921967 final Springer copy
lcp
parents: 323
diff changeset
   130
subgoals_of_brl{\it brl1} < subgoals_of_brl{\it brl2}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   131
\end{ttbox}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   132
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   133
Note that \hbox{\tt sort lessb {\it brls}} sorts a list of $\it
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   134
(flag,rule)$ pairs by the number of new subgoals they will yield.  Thus,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   135
those that yield the fewest subgoals should be tried first.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   136
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   137
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   138
\subsection{Discrimination nets for fast resolution}\label{filt_resolve_tac}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   139
\index{discrimination nets|bold}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   140
\index{tactics!resolution}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   141
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   142
net_resolve_tac  : thm list -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   143
net_match_tac    : thm list -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   144
net_biresolve_tac: (bool*thm) list -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   145
net_bimatch_tac  : (bool*thm) list -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   146
filt_resolve_tac : thm list -> int -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   147
could_unify      : term*term->bool
8136
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 7491
diff changeset
   148
filter_thms      : (term*term->bool) -> int*term*thm list -> thm{\ts}list
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   149
\end{ttbox}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   150
The module {\tt Net} implements a discrimination net data structure for
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   151
fast selection of rules \cite[Chapter 14]{charniak80}.  A term is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   152
classified by the symbol list obtained by flattening it in preorder.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   153
The flattening takes account of function applications, constants, and free
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   154
and bound variables; it identifies all unknowns and also regards
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   155
\index{lambda abs@$\lambda$-abstractions}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   156
$\lambda$-abstractions as unknowns, since they could $\eta$-contract to
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   157
anything.  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   158
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   159
A discrimination net serves as a polymorphic dictionary indexed by terms.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   160
The module provides various functions for inserting and removing items from
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   161
nets.  It provides functions for returning all items whose term could match
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   162
or unify with a target term.  The matching and unification tests are
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   163
overly lax (due to the identifications mentioned above) but they serve as
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   164
useful filters.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   165
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   166
A net can store introduction rules indexed by their conclusion, and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   167
elimination rules indexed by their major premise.  Isabelle provides
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   168
several functions for `compiling' long lists of rules into fast
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   169
resolution tactics.  When supplied with a list of theorems, these functions
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   170
build a discrimination net; the net is used when the tactic is applied to a
332
01b87a921967 final Springer copy
lcp
parents: 323
diff changeset
   171
goal.  To avoid repeatedly constructing the nets, use currying: bind the
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   172
resulting tactics to \ML{} identifiers.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   173
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   174
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   175
\item[\ttindexbold{net_resolve_tac} {\it thms}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   176
builds a discrimination net to obtain the effect of a similar call to {\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   177
resolve_tac}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   178
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   179
\item[\ttindexbold{net_match_tac} {\it thms}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   180
builds a discrimination net to obtain the effect of a similar call to {\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   181
match_tac}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   182
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   183
\item[\ttindexbold{net_biresolve_tac} {\it brls}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   184
builds a discrimination net to obtain the effect of a similar call to {\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   185
biresolve_tac}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   186
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   187
\item[\ttindexbold{net_bimatch_tac} {\it brls}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   188
builds a discrimination net to obtain the effect of a similar call to {\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   189
bimatch_tac}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   190
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   191
\item[\ttindexbold{filt_resolve_tac} {\it thms} {\it maxr} {\it i}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   192
uses discrimination nets to extract the {\it thms} that are applicable to
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   193
subgoal~$i$.  If more than {\it maxr\/} theorems are applicable then the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   194
tactic fails.  Otherwise it calls {\tt resolve_tac}.  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   195
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   196
This tactic helps avoid runaway instantiation of unknowns, for example in
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   197
type inference.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   198
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   199
\item[\ttindexbold{could_unify} ({\it t},{\it u})] 
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   200
returns {\tt false} if~$t$ and~$u$ are `obviously' non-unifiable, and
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   201
otherwise returns~{\tt true}.  It assumes all variables are distinct,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   202
reporting that {\tt ?a=?a} may unify with {\tt 0=1}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   203
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   204
\item[\ttindexbold{filter_thms} $could\; (limit,prem,thms)$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   205
returns the list of potentially resolvable rules (in {\it thms\/}) for the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   206
subgoal {\it prem}, using the predicate {\it could\/} to compare the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   207
conclusion of the subgoal with the conclusion of each rule.  The resulting list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   208
is no longer than {\it limit}.
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   209
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   210
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   211
\index{tactics|)}
5371
e27558a68b8d emacs local vars;
wenzelm
parents: 4607
diff changeset
   212
e27558a68b8d emacs local vars;
wenzelm
parents: 4607
diff changeset
   213
e27558a68b8d emacs local vars;
wenzelm
parents: 4607
diff changeset
   214
%%% Local Variables: 
e27558a68b8d emacs local vars;
wenzelm
parents: 4607
diff changeset
   215
%%% mode: latex
e27558a68b8d emacs local vars;
wenzelm
parents: 4607
diff changeset
   216
%%% TeX-master: "ref"
e27558a68b8d emacs local vars;
wenzelm
parents: 4607
diff changeset
   217
%%% End: