doc-src/Ref/tactic.tex
author wenzelm
Fri, 10 Nov 2000 19:02:37 +0100
changeset 10432 3dfbc913d184
parent 10347 c0cfc4ac12e2
child 17818 38c889d77282
permissions -rw-r--r--
added axclass inverse and consts inverse, divide (infix "/"); moved axclass power to Nat.thy;
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}
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2612
diff changeset
     3
\index{tactics|(} Tactics have type \mltydx{tactic}.  This is just an
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2612
diff changeset
     4
abbreviation for functions from theorems to theorem sequences, where
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2612
diff changeset
     5
the theorems represent states of a backward proof.  Tactics seldom
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2612
diff changeset
     6
need to be coded from scratch, as functions; instead they are
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2612
diff changeset
     7
expressed using basic tactics and tacticals.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     8
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
     9
This chapter only presents the primitive tactics.  Substantial proofs
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
    10
require the power of automatic tools like simplification
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
    11
(Chapter~\ref{chap:simplification}) and classical tableau reasoning
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
    12
(Chapter~\ref{chap:classical}).
2039
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    13
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    14
\section{Resolution and assumption tactics}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    15
{\bf Resolution} is Isabelle's basic mechanism for refining a subgoal using
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    16
a rule.  {\bf Elim-resolution} is particularly suited for elimination
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    17
rules, while {\bf destruct-resolution} is particularly suited for
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    18
destruction rules.  The {\tt r}, {\tt e}, {\tt d} naming convention is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    19
maintained for several different kinds of resolution tactics, as well as
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    20
the shortcuts in the subgoal module.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    21
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    22
All the tactics in this section act on a subgoal designated by a positive
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    23
integer~$i$.  They fail (by returning the empty sequence) if~$i$ is out of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    24
range.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    25
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    26
\subsection{Resolution tactics}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
    27
\index{resolution!tactics}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    28
\index{tactics!resolution|bold}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    29
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    30
resolve_tac  : thm list -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    31
eresolve_tac : thm list -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    32
dresolve_tac : thm list -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    33
forward_tac  : thm list -> int -> tactic 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    34
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    35
These perform resolution on a list of theorems, $thms$, representing a list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    36
of object-rules.  When generating next states, they take each of the rules
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    37
in the order given.  Each rule may yield several next states, or none:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    38
higher-order resolution may yield multiple resolvents.
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
    39
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    40
\item[\ttindexbold{resolve_tac} {\it thms} {\it i}] 
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
    41
  refines the proof state using the rules, which should normally be
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
    42
  introduction rules.  It resolves a rule's conclusion with
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
    43
  subgoal~$i$ of the proof state.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    44
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    45
\item[\ttindexbold{eresolve_tac} {\it thms} {\it i}] 
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
    46
  \index{elim-resolution}
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
    47
  performs elim-resolution with the rules, which should normally be
4607
6759ba6d3cc1 Added reference to rotate_prems
paulson
parents: 4597
diff changeset
    48
  elimination rules.  It resolves with a rule, proves its first premise by
6759ba6d3cc1 Added reference to rotate_prems
paulson
parents: 4597
diff changeset
    49
  assumption, and finally \emph{deletes} that assumption from any new
6759ba6d3cc1 Added reference to rotate_prems
paulson
parents: 4597
diff changeset
    50
  subgoals.  (To rotate a rule's premises,
7491
95a4af0e10a7 added ftac, eatac, datac, fatac
oheimb
parents: 6618
diff changeset
    51
  see \texttt{rotate_prems} in~{\S}\ref{MiscellaneousForwardRules}.)
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    52
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    53
\item[\ttindexbold{dresolve_tac} {\it thms} {\it i}] 
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
    54
  \index{forward proof}\index{destruct-resolution}
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
    55
  performs destruct-resolution with the rules, which normally should
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
    56
  be destruction rules.  This replaces an assumption by the result of
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
    57
  applying one of the rules.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    58
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
    59
\item[\ttindexbold{forward_tac}]\index{forward proof}
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
    60
  is like {\tt dresolve_tac} except that the selected assumption is not
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
    61
  deleted.  It applies a rule to an assumption, adding the result as a new
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
    62
  assumption.
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
    63
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    64
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    65
\subsection{Assumption tactics}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
    66
\index{tactics!assumption|bold}\index{assumptions!tactics for}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    67
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    68
assume_tac    : int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    69
eq_assume_tac : int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    70
\end{ttbox} 
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
    71
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    72
\item[\ttindexbold{assume_tac} {\it i}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    73
attempts to solve subgoal~$i$ by assumption.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    74
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    75
\item[\ttindexbold{eq_assume_tac}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    76
is like {\tt assume_tac} but does not use unification.  It succeeds (with a
4607
6759ba6d3cc1 Added reference to rotate_prems
paulson
parents: 4597
diff changeset
    77
\emph{unique} next state) if one of the assumptions is identical to the
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    78
subgoal's conclusion.  Since it does not instantiate variables, it cannot
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    79
make other subgoals unprovable.  It is intended to be called from proof
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    80
strategies, not interactively.
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
    81
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    82
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    83
\subsection{Matching tactics} \label{match_tac}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
    84
\index{tactics!matching}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    85
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    86
match_tac  : thm list -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    87
ematch_tac : thm list -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    88
dmatch_tac : thm list -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    89
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    90
These are just like the resolution tactics except that they never
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    91
instantiate unknowns in the proof state.  Flexible subgoals are not updated
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    92
willy-nilly, but are left alone.  Matching --- strictly speaking --- means
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    93
treating the unknowns in the proof state as constants; these tactics merely
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    94
discard unifiers that would update the proof state.
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
    95
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    96
\item[\ttindexbold{match_tac} {\it thms} {\it i}] 
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
    97
refines the proof state using the rules, matching a rule's
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    98
conclusion with subgoal~$i$ of the proof state.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    99
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   100
\item[\ttindexbold{ematch_tac}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   101
is like {\tt match_tac}, but performs elim-resolution.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   102
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   103
\item[\ttindexbold{dmatch_tac}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   104
is like {\tt match_tac}, but performs destruct-resolution.
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   105
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   106
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   107
10347
c0cfc4ac12e2 added instantiate_tac
oheimb
parents: 9695
diff changeset
   108
\subsection{Explicit instantiation} \label{res_inst_tac}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   109
\index{tactics!instantiation}\index{instantiation}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   110
\begin{ttbox} 
10347
c0cfc4ac12e2 added instantiate_tac
oheimb
parents: 9695
diff changeset
   111
res_inst_tac    : (string*string)list -> thm -> int -> tactic
c0cfc4ac12e2 added instantiate_tac
oheimb
parents: 9695
diff changeset
   112
eres_inst_tac   : (string*string)list -> thm -> int -> tactic
c0cfc4ac12e2 added instantiate_tac
oheimb
parents: 9695
diff changeset
   113
dres_inst_tac   : (string*string)list -> thm -> int -> tactic
c0cfc4ac12e2 added instantiate_tac
oheimb
parents: 9695
diff changeset
   114
forw_inst_tac   : (string*string)list -> thm -> int -> tactic
c0cfc4ac12e2 added instantiate_tac
oheimb
parents: 9695
diff changeset
   115
instantiate_tac : (string*string)list -> tactic
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   116
\end{ttbox}
10347
c0cfc4ac12e2 added instantiate_tac
oheimb
parents: 9695
diff changeset
   117
The first four of these tactics are designed for applying rules by resolution
c0cfc4ac12e2 added instantiate_tac
oheimb
parents: 9695
diff changeset
   118
such as substitution and induction, which cause difficulties for higher-order 
c0cfc4ac12e2 added instantiate_tac
oheimb
parents: 9695
diff changeset
   119
unification.  The tactics accept explicit instantiations for unknowns 
c0cfc4ac12e2 added instantiate_tac
oheimb
parents: 9695
diff changeset
   120
in the rule ---typically, in the rule's conclusion. The last one, 
c0cfc4ac12e2 added instantiate_tac
oheimb
parents: 9695
diff changeset
   121
{\tt instantiate_tac}, may be used to instantiate unknowns in the proof state,
c0cfc4ac12e2 added instantiate_tac
oheimb
parents: 9695
diff changeset
   122
independently of rule application. 
c0cfc4ac12e2 added instantiate_tac
oheimb
parents: 9695
diff changeset
   123
c0cfc4ac12e2 added instantiate_tac
oheimb
parents: 9695
diff changeset
   124
Each instantiation is a pair {\tt($v$,$e$)}, 
c0cfc4ac12e2 added instantiate_tac
oheimb
parents: 9695
diff changeset
   125
where $v$ is an unknown \emph{without} its leading question mark!
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   126
\begin{itemize}
332
01b87a921967 final Springer copy
lcp
parents: 323
diff changeset
   127
\item If $v$ is the type unknown {\tt'a}, then
01b87a921967 final Springer copy
lcp
parents: 323
diff changeset
   128
the rule must contain a type unknown \verb$?'a$ of some
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   129
sort~$s$, and $e$ should be a type of sort $s$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   130
332
01b87a921967 final Springer copy
lcp
parents: 323
diff changeset
   131
\item If $v$ is the unknown {\tt P}, then
01b87a921967 final Springer copy
lcp
parents: 323
diff changeset
   132
the rule must contain an unknown \verb$?P$ of some type~$\tau$,
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   133
and $e$ should be a term of some type~$\sigma$ such that $\tau$ and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   134
$\sigma$ are unifiable.  If the unification of $\tau$ and $\sigma$
332
01b87a921967 final Springer copy
lcp
parents: 323
diff changeset
   135
instantiates any type unknowns in $\tau$, these instantiations
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   136
are recorded for application to the rule.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   137
\end{itemize}
8136
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 7491
diff changeset
   138
Types are instantiated before terms are.  Because type instantiations are
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   139
inferred from term instantiations, explicit type instantiations are seldom
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   140
necessary --- if \verb$?t$ has type \verb$?'a$, then the instantiation list
8136
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 7491
diff changeset
   141
\texttt{[("'a","bool"), ("t","True")]} may be simplified to
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 7491
diff changeset
   142
\texttt{[("t","True")]}.  Type unknowns in the proof state may cause
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   143
failure because the tactics cannot instantiate them.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   144
10347
c0cfc4ac12e2 added instantiate_tac
oheimb
parents: 9695
diff changeset
   145
The first four instantiation tactics act on a given subgoal.  Terms in the
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   146
instantiations are type-checked in the context of that subgoal --- in
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   147
particular, they may refer to that subgoal's parameters.  Any unknowns in
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   148
the terms receive subscripts and are lifted over the parameters; thus, you
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   149
may not refer to unknowns in the subgoal.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   150
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   151
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   152
\item[\ttindexbold{res_inst_tac} {\it insts} {\it thm} {\it i}]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   153
instantiates the rule {\it thm} with the instantiations {\it insts}, as
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   154
described above, and then performs resolution on subgoal~$i$.  Resolution
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   155
typically causes further instantiations; you need not give explicit
332
01b87a921967 final Springer copy
lcp
parents: 323
diff changeset
   156
instantiations for every unknown in the rule.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   157
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   158
\item[\ttindexbold{eres_inst_tac}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   159
is like {\tt res_inst_tac}, but performs elim-resolution.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   160
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   161
\item[\ttindexbold{dres_inst_tac}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   162
is like {\tt res_inst_tac}, but performs destruct-resolution.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   163
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   164
\item[\ttindexbold{forw_inst_tac}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   165
is like {\tt dres_inst_tac} except that the selected assumption is not
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   166
deleted.  It applies the instantiated rule to an assumption, adding the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   167
result as a new assumption.
10347
c0cfc4ac12e2 added instantiate_tac
oheimb
parents: 9695
diff changeset
   168
c0cfc4ac12e2 added instantiate_tac
oheimb
parents: 9695
diff changeset
   169
\item[\ttindexbold{instantiate_tac} {\it insts}] 
c0cfc4ac12e2 added instantiate_tac
oheimb
parents: 9695
diff changeset
   170
instantiates unknowns in the proof state. This affects the main goal as 
c0cfc4ac12e2 added instantiate_tac
oheimb
parents: 9695
diff changeset
   171
well as all subgoals.
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   172
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   173
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   174
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   175
\section{Other basic tactics}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   176
\subsection{Tactic shortcuts}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   177
\index{shortcuts!for tactics}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   178
\index{tactics!resolution}\index{tactics!assumption}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   179
\index{tactics!meta-rewriting}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   180
\begin{ttbox} 
7491
95a4af0e10a7 added ftac, eatac, datac, fatac
oheimb
parents: 6618
diff changeset
   181
rtac     :      thm ->        int -> tactic
95a4af0e10a7 added ftac, eatac, datac, fatac
oheimb
parents: 6618
diff changeset
   182
etac     :      thm ->        int -> tactic
95a4af0e10a7 added ftac, eatac, datac, fatac
oheimb
parents: 6618
diff changeset
   183
dtac     :      thm ->        int -> tactic
95a4af0e10a7 added ftac, eatac, datac, fatac
oheimb
parents: 6618
diff changeset
   184
ftac     :      thm ->        int -> tactic
95a4af0e10a7 added ftac, eatac, datac, fatac
oheimb
parents: 6618
diff changeset
   185
atac     :                    int -> tactic
95a4af0e10a7 added ftac, eatac, datac, fatac
oheimb
parents: 6618
diff changeset
   186
eatac    :      thm -> int -> int -> tactic
95a4af0e10a7 added ftac, eatac, datac, fatac
oheimb
parents: 6618
diff changeset
   187
datac    :      thm -> int -> int -> tactic
95a4af0e10a7 added ftac, eatac, datac, fatac
oheimb
parents: 6618
diff changeset
   188
fatac    :      thm -> int -> int -> tactic
95a4af0e10a7 added ftac, eatac, datac, fatac
oheimb
parents: 6618
diff changeset
   189
ares_tac :      thm list   -> int -> tactic
95a4af0e10a7 added ftac, eatac, datac, fatac
oheimb
parents: 6618
diff changeset
   190
rewtac   :      thm ->               tactic
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   191
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   192
These abbreviate common uses of tactics.
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   193
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   194
\item[\ttindexbold{rtac} {\it thm} {\it i}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   195
abbreviates \hbox{\tt resolve_tac [{\it thm}] {\it i}}, doing resolution.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   196
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   197
\item[\ttindexbold{etac} {\it thm} {\it i}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   198
abbreviates \hbox{\tt eresolve_tac [{\it thm}] {\it i}}, doing elim-resolution.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   199
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   200
\item[\ttindexbold{dtac} {\it thm} {\it i}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   201
abbreviates \hbox{\tt dresolve_tac [{\it thm}] {\it i}}, doing
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   202
destruct-resolution.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   203
7491
95a4af0e10a7 added ftac, eatac, datac, fatac
oheimb
parents: 6618
diff changeset
   204
\item[\ttindexbold{ftac} {\it thm} {\it i}] 
95a4af0e10a7 added ftac, eatac, datac, fatac
oheimb
parents: 6618
diff changeset
   205
abbreviates \hbox{\tt forward_tac [{\it thm}] {\it i}}, doing
95a4af0e10a7 added ftac, eatac, datac, fatac
oheimb
parents: 6618
diff changeset
   206
destruct-resolution without deleting the assumption.
95a4af0e10a7 added ftac, eatac, datac, fatac
oheimb
parents: 6618
diff changeset
   207
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   208
\item[\ttindexbold{atac} {\it i}] 
332
01b87a921967 final Springer copy
lcp
parents: 323
diff changeset
   209
abbreviates \hbox{\tt assume_tac {\it i}}, doing proof by assumption.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   210
7491
95a4af0e10a7 added ftac, eatac, datac, fatac
oheimb
parents: 6618
diff changeset
   211
\item[\ttindexbold{eatac} {\it thm} {\it j} {\it i}] 
95a4af0e10a7 added ftac, eatac, datac, fatac
oheimb
parents: 6618
diff changeset
   212
performs \hbox{\tt etac {\it thm}} and then {\it j} times \texttt{atac}, 
95a4af0e10a7 added ftac, eatac, datac, fatac
oheimb
parents: 6618
diff changeset
   213
solving additionally {\it j}~premises of the rule {\it thm} by assumption.
95a4af0e10a7 added ftac, eatac, datac, fatac
oheimb
parents: 6618
diff changeset
   214
95a4af0e10a7 added ftac, eatac, datac, fatac
oheimb
parents: 6618
diff changeset
   215
\item[\ttindexbold{datac} {\it thm} {\it j} {\it i}] 
95a4af0e10a7 added ftac, eatac, datac, fatac
oheimb
parents: 6618
diff changeset
   216
performs \hbox{\tt dtac {\it thm}} and then {\it j} times \texttt{atac}, 
95a4af0e10a7 added ftac, eatac, datac, fatac
oheimb
parents: 6618
diff changeset
   217
solving additionally {\it j}~premises of the rule {\it thm} by assumption.
95a4af0e10a7 added ftac, eatac, datac, fatac
oheimb
parents: 6618
diff changeset
   218
95a4af0e10a7 added ftac, eatac, datac, fatac
oheimb
parents: 6618
diff changeset
   219
\item[\ttindexbold{fatac} {\it thm} {\it j} {\it i}] 
95a4af0e10a7 added ftac, eatac, datac, fatac
oheimb
parents: 6618
diff changeset
   220
performs \hbox{\tt ftac {\it thm}} and then {\it j} times \texttt{atac}, 
95a4af0e10a7 added ftac, eatac, datac, fatac
oheimb
parents: 6618
diff changeset
   221
solving additionally {\it j}~premises of the rule {\it thm} by assumption.
95a4af0e10a7 added ftac, eatac, datac, fatac
oheimb
parents: 6618
diff changeset
   222
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   223
\item[\ttindexbold{ares_tac} {\it thms} {\it i}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   224
tries proof by assumption and resolution; it abbreviates
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   225
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   226
assume_tac {\it i} ORELSE resolve_tac {\it thms} {\it i}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   227
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   228
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   229
\item[\ttindexbold{rewtac} {\it def}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   230
abbreviates \hbox{\tt rewrite_goals_tac [{\it def}]}, unfolding a definition.
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   231
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   232
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   233
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   234
\subsection{Inserting premises and facts}\label{cut_facts_tac}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   235
\index{tactics!for inserting facts}\index{assumptions!inserting}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   236
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   237
cut_facts_tac : thm list -> int -> tactic
286
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   238
cut_inst_tac  : (string*string)list -> thm -> int -> tactic
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   239
subgoal_tac   : string -> int -> tactic
9523
232b09dba0fe subgoals_tac: fixed spelling;
wenzelm
parents: 8136
diff changeset
   240
subgoals_tac  : string list -> int -> tactic
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   241
\end{ttbox}
2039
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
   242
These tactics add assumptions to a subgoal.
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   243
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   244
\item[\ttindexbold{cut_facts_tac} {\it thms} {\it i}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   245
  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
   246
  been inserted as assumptions, they become subject to tactics such as {\tt
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   247
    eresolve_tac} and {\tt rewrite_goals_tac}.  Only rules with no premises
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   248
  are inserted: Isabelle cannot use assumptions that contain $\Imp$
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   249
  or~$\Forall$.  Sometimes the theorems are premises of a rule being
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   250
  derived, returned by~{\tt goal}; instead of calling this tactic, you
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   251
  could state the goal with an outermost meta-quantifier.
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   252
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   253
\item[\ttindexbold{cut_inst_tac} {\it insts} {\it thm} {\it i}]
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   254
  instantiates the {\it thm} with the instantiations {\it insts}, as
7491
95a4af0e10a7 added ftac, eatac, datac, fatac
oheimb
parents: 6618
diff changeset
   255
  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
   256
  new assumption to subgoal~$i$. 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   257
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   258
\item[\ttindexbold{subgoal_tac} {\it formula} {\it i}] 
9568
20c410fb5104 fixed spelling;
wenzelm
parents: 9523
diff changeset
   259
adds the {\it formula} as an assumption to subgoal~$i$, and inserts the same
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   260
{\it formula} as a new subgoal, $i+1$.
457
8577bc1c4e1b documented subgoals_tac
lcp
parents: 332
diff changeset
   261
8577bc1c4e1b documented subgoals_tac
lcp
parents: 332
diff changeset
   262
\item[\ttindexbold{subgoals_tac} {\it formulae} {\it i}] 
8577bc1c4e1b documented subgoals_tac
lcp
parents: 332
diff changeset
   263
  uses {\tt subgoal_tac} to add the members of the list of {\it
8577bc1c4e1b documented subgoals_tac
lcp
parents: 332
diff changeset
   264
    formulae} as assumptions to subgoal~$i$. 
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   265
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   266
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   267
2039
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
   268
\subsection{``Putting off'' a subgoal}
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
   269
\begin{ttbox} 
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
   270
defer_tac : int -> tactic
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
   271
\end{ttbox}
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
   272
\begin{ttdescription}
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
   273
\item[\ttindexbold{defer_tac} {\it i}] 
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
   274
  moves subgoal~$i$ to the last position in the proof state.  It can be
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
   275
  useful when correcting a proof script: if the tactic given for subgoal~$i$
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
   276
  fails, calling {\tt defer_tac} instead will let you continue with the rest
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
   277
  of the script.
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
   278
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
   279
  The tactic fails if subgoal~$i$ does not exist or if the proof state
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
   280
  contains type unknowns. 
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
   281
\end{ttdescription}
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
   282
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
   283
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   284
\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
   285
\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
   286
\index{definitions}
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
   287
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
   288
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
   289
constant or a constant applied to a list of variables, for example $\it
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   290
sqr(n)\equiv n\times n$.  Conditional definitions, $\phi\Imp t\equiv u$,
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   291
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
   292
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
   293
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
   294
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
   295
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
   296
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
   297
this automatically.  The corresponding tactics rewrite the proof state,
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
   298
yielding a single next state.  See also the {\tt goalw} command, which is the
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
   299
easiest way of handling definitions.
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
   300
\begin{ttbox} 
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
   301
rewrite_goals_tac : thm list -> tactic
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
   302
rewrite_tac       : thm list -> tactic
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
   303
fold_goals_tac    : thm list -> tactic
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
   304
fold_tac          : thm list -> tactic
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
   305
\end{ttbox}
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
   306
\begin{ttdescription}
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
   307
\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
   308
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
   309
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
   310
particular subgoal.
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
   311
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
   312
\item[\ttindexbold{rewrite_tac} {\it defs}]  
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
   313
unfolds the {\it defs} throughout the proof state, including the main goal
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
   314
--- not normally desirable!
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
   315
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
   316
\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
   317
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
   318
leaving the main goal unchanged.
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
   319
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
   320
\item[\ttindexbold{fold_tac} {\it defs}]  
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
   321
folds the {\it defs} throughout the proof state.
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
   322
\end{ttdescription}
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
   323
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   324
\begin{warn}
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   325
  These tactics only cope with definitions expressed as meta-level
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   326
  equalities ($\equiv$).  More general equivalences are handled by the
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   327
  simplifier, provided that it is set up appropriately for your logic
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   328
  (see Chapter~\ref{chap:simplification}).
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   329
\end{warn}
2039
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
   330
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   331
\subsection{Theorems useful with tactics}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   332
\index{theorems!of pure theory}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   333
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   334
asm_rl: thm 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   335
cut_rl: thm 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   336
\end{ttbox}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   337
\begin{ttdescription}
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   338
\item[\tdx{asm_rl}] 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   339
is $\psi\Imp\psi$.  Under elim-resolution it does proof by assumption, and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   340
\hbox{\tt eresolve_tac (asm_rl::{\it thms}) {\it i}} is equivalent to
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   341
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   342
assume_tac {\it i}  ORELSE  eresolve_tac {\it thms} {\it i}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   343
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   344
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   345
\item[\tdx{cut_rl}] 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   346
is $\List{\psi\Imp\theta,\psi}\Imp\theta$.  It is useful for inserting
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   347
assumptions; it underlies {\tt forward_tac}, {\tt cut_facts_tac}
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   348
and {\tt subgoal_tac}.
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   349
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   350
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   351
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   352
\section{Obscure tactics}
1212
7059356e18e0 added rotate_tac
nipkow
parents: 457
diff changeset
   353
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   354
\subsection{Renaming parameters in a goal} \index{parameters!renaming}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   355
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   356
rename_tac        : string -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   357
rename_last_tac   : string -> string list -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   358
Logic.set_rename_prefix : string -> unit
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   359
Logic.auto_rename       : bool ref      \hfill{\bf initially false}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   360
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   361
When creating a parameter, Isabelle chooses its name by matching variable
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   362
names via the object-rule.  Given the rule $(\forall I)$ formalized as
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   363
$\left(\Forall x. P(x)\right) \Imp \forall x.P(x)$, Isabelle will note that
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   364
the $\Forall$-bound variable in the premise has the same name as the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   365
$\forall$-bound variable in the conclusion.  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   366
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   367
Sometimes there is insufficient information and Isabelle chooses an
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   368
arbitrary name.  The renaming tactics let you override Isabelle's choice.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   369
Because renaming parameters has no logical effect on the proof state, the
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   370
{\tt by} command prints the message {\tt Warning:\ same as previous
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   371
level}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   372
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   373
Alternatively, you can suppress the naming mechanism described above and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   374
have Isabelle generate uniform names for parameters.  These names have the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   375
form $p${\tt a}, $p${\tt b}, $p${\tt c},~\ldots, where $p$ is any desired
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   376
prefix.  They are ugly but predictable.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   377
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   378
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   379
\item[\ttindexbold{rename_tac} {\it str} {\it i}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   380
interprets the string {\it str} as a series of blank-separated variable
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   381
names, and uses them to rename the parameters of subgoal~$i$.  The names
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   382
must be distinct.  If there are fewer names than parameters, then the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   383
tactic renames the innermost parameters and may modify the remaining ones
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   384
to ensure that all the parameters are distinct.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   385
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   386
\item[\ttindexbold{rename_last_tac} {\it prefix} {\it suffixes} {\it i}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   387
generates a list of names by attaching each of the {\it suffixes\/} to the 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   388
{\it prefix}.  It is intended for coding structural induction tactics,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   389
where several of the new parameters should have related names.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   390
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   391
\item[\ttindexbold{Logic.set_rename_prefix} {\it prefix};] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   392
sets the prefix for uniform renaming to~{\it prefix}.  The default prefix
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   393
is {\tt"k"}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   394
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   395
\item[set \ttindexbold{Logic.auto_rename};] 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   396
makes Isabelle generate uniform names for parameters. 
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   397
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   398
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   399
2612
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   400
\subsection{Manipulating assumptions}
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   401
\index{assumptions!rotating}
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   402
\begin{ttbox} 
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   403
thin_tac   : string -> int -> tactic
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   404
rotate_tac : int -> int -> tactic
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   405
\end{ttbox}
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   406
\begin{ttdescription}
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   407
\item[\ttindexbold{thin_tac} {\it formula} $i$]  
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   408
\index{assumptions!deleting}
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   409
deletes the specified assumption from subgoal $i$.  Often the assumption
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   410
can be abbreviated, replacing subformul{\ae} by unknowns; the first matching
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   411
assumption will be deleted.  Removing useless assumptions from a subgoal
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   412
increases its readability and can make search tactics run faster.
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   413
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   414
\item[\ttindexbold{rotate_tac} $n$ $i$]  
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   415
\index{assumptions!rotating}
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   416
rotates the assumptions of subgoal $i$ by $n$ positions: from right to left
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   417
if $n$ is positive, and from left to right if $n$ is negative.  This is 
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   418
sometimes necessary in connection with \ttindex{asm_full_simp_tac}, which 
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   419
processes assumptions from left to right.
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   420
\end{ttdescription}
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   421
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   422
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   423
\subsection{Tidying the proof state}
3400
80c979e0d42f Documented the new distinct_subgoals_tac
paulson
parents: 3108
diff changeset
   424
\index{duplicate subgoals!removing}
2612
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   425
\index{parameters!removing unused}
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   426
\index{flex-flex constraints}
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   427
\begin{ttbox} 
3400
80c979e0d42f Documented the new distinct_subgoals_tac
paulson
parents: 3108
diff changeset
   428
distinct_subgoals_tac : tactic
80c979e0d42f Documented the new distinct_subgoals_tac
paulson
parents: 3108
diff changeset
   429
prune_params_tac      : tactic
80c979e0d42f Documented the new distinct_subgoals_tac
paulson
parents: 3108
diff changeset
   430
flexflex_tac          : tactic
2612
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   431
\end{ttbox}
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   432
\begin{ttdescription}
9695
ec7d7f877712 proper setup of iman.sty/extra.sty/ttbox.sty;
wenzelm
parents: 9568
diff changeset
   433
\item[\ttindexbold{distinct_subgoals_tac}] removes duplicate subgoals from a
ec7d7f877712 proper setup of iman.sty/extra.sty/ttbox.sty;
wenzelm
parents: 9568
diff changeset
   434
  proof state.  (These arise especially in ZF, where the subgoals are
ec7d7f877712 proper setup of iman.sty/extra.sty/ttbox.sty;
wenzelm
parents: 9568
diff changeset
   435
  essentially type constraints.)
3400
80c979e0d42f Documented the new distinct_subgoals_tac
paulson
parents: 3108
diff changeset
   436
2612
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   437
\item[\ttindexbold{prune_params_tac}]  
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   438
  removes unused parameters from all subgoals of the proof state.  It works
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   439
  by rewriting with the theorem $(\Forall x. V)\equiv V$.  This tactic can
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   440
  make the proof state more readable.  It is used with
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   441
  \ttindex{rule_by_tactic} to simplify the resulting theorem.
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   442
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   443
\item[\ttindexbold{flexflex_tac}]  
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   444
  removes all flex-flex pairs from the proof state by applying the trivial
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   445
  unifier.  This drastic step loses information, and should only be done as
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   446
  the last step of a proof.
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   447
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   448
  Flex-flex constraints arise from difficult cases of higher-order
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   449
  unification.  To prevent this, use \ttindex{res_inst_tac} to instantiate
7491
95a4af0e10a7 added ftac, eatac, datac, fatac
oheimb
parents: 6618
diff changeset
   450
  some variables in a rule~({\S}\ref{res_inst_tac}).  Normally flex-flex
2612
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   451
  constraints can be ignored; they often disappear as unknowns get
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   452
  instantiated.
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   453
\end{ttdescription}
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   454
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   455
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   456
\subsection{Composition: resolution without lifting}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   457
\index{tactics!for composition}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   458
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   459
compose_tac: (bool * thm * int) -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   460
\end{ttbox}
332
01b87a921967 final Springer copy
lcp
parents: 323
diff changeset
   461
{\bf Composing} two rules means resolving them without prior lifting or
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   462
renaming of unknowns.  This low-level operation, which underlies the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   463
resolution tactics, may occasionally be useful for special effects.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   464
A typical application is \ttindex{res_inst_tac}, which lifts and instantiates a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   465
rule, then passes the result to {\tt compose_tac}.
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   466
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   467
\item[\ttindexbold{compose_tac} ($flag$, $rule$, $m$) $i$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   468
refines subgoal~$i$ using $rule$, without lifting.  The $rule$ is taken to
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   469
have the form $\List{\psi@1; \ldots; \psi@m} \Imp \psi$, where $\psi$ need
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   470
not be atomic; thus $m$ determines the number of new subgoals.  If
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   471
$flag$ is {\tt true} then it performs elim-resolution --- it solves the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   472
first premise of~$rule$ by assumption and deletes that assumption.
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   473
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   474
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   475
4276
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3950
diff changeset
   476
\section{*Managing lots of rules}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   477
These operations are not intended for interactive use.  They are concerned
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   478
with the processing of large numbers of rules in automatic proof
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   479
strategies.  Higher-order resolution involving a long list of rules is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   480
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
   481
resolution, and can also detect whether a subgoal is too flexible,
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   482
with too many rules applicable.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   483
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   484
\subsection{Combined resolution and elim-resolution} \label{biresolve_tac}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   485
\index{tactics!resolution}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   486
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   487
biresolve_tac   : (bool*thm)list -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   488
bimatch_tac     : (bool*thm)list -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   489
subgoals_of_brl : bool*thm -> int
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   490
lessb           : (bool*thm) * (bool*thm) -> bool
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   491
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   492
{\bf Bi-resolution} takes a list of $\it (flag,rule)$ pairs.  For each
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   493
pair, it applies resolution if the flag is~{\tt false} and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   494
elim-resolution if the flag is~{\tt true}.  A single tactic call handles a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   495
mixture of introduction and elimination rules.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   496
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   497
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   498
\item[\ttindexbold{biresolve_tac} {\it brls} {\it i}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   499
refines the proof state by resolution or elim-resolution on each rule, as
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   500
indicated by its flag.  It affects subgoal~$i$ of the proof state.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   501
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   502
\item[\ttindexbold{bimatch_tac}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   503
is like {\tt biresolve_tac}, but performs matching: unknowns in the
7491
95a4af0e10a7 added ftac, eatac, datac, fatac
oheimb
parents: 6618
diff changeset
   504
proof state are never updated (see~{\S}\ref{match_tac}).
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   505
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   506
\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
   507
returns the number of new subgoals that bi-res\-o\-lu\-tion would yield for the
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   508
pair (if applied to a suitable subgoal).  This is $n$ if the flag is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   509
{\tt false} and $n-1$ if the flag is {\tt true}, where $n$ is the number
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   510
of premises of the rule.  Elim-resolution yields one fewer subgoal than
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   511
ordinary resolution because it solves the major premise by assumption.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   512
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   513
\item[\ttindexbold{lessb} ({\it brl1},{\it brl2})] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   514
returns the result of 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   515
\begin{ttbox}
332
01b87a921967 final Springer copy
lcp
parents: 323
diff changeset
   516
subgoals_of_brl{\it brl1} < subgoals_of_brl{\it brl2}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   517
\end{ttbox}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   518
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   519
Note that \hbox{\tt sort lessb {\it brls}} sorts a list of $\it
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   520
(flag,rule)$ pairs by the number of new subgoals they will yield.  Thus,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   521
those that yield the fewest subgoals should be tried first.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   522
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   523
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   524
\subsection{Discrimination nets for fast resolution}\label{filt_resolve_tac}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   525
\index{discrimination nets|bold}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   526
\index{tactics!resolution}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   527
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   528
net_resolve_tac  : thm list -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   529
net_match_tac    : thm list -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   530
net_biresolve_tac: (bool*thm) list -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   531
net_bimatch_tac  : (bool*thm) list -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   532
filt_resolve_tac : thm list -> int -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   533
could_unify      : term*term->bool
8136
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 7491
diff changeset
   534
filter_thms      : (term*term->bool) -> int*term*thm list -> thm{\ts}list
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   535
\end{ttbox}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   536
The module {\tt Net} implements a discrimination net data structure for
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   537
fast selection of rules \cite[Chapter 14]{charniak80}.  A term is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   538
classified by the symbol list obtained by flattening it in preorder.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   539
The flattening takes account of function applications, constants, and free
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   540
and bound variables; it identifies all unknowns and also regards
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   541
\index{lambda abs@$\lambda$-abstractions}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   542
$\lambda$-abstractions as unknowns, since they could $\eta$-contract to
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   543
anything.  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   544
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   545
A discrimination net serves as a polymorphic dictionary indexed by terms.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   546
The module provides various functions for inserting and removing items from
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   547
nets.  It provides functions for returning all items whose term could match
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   548
or unify with a target term.  The matching and unification tests are
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   549
overly lax (due to the identifications mentioned above) but they serve as
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   550
useful filters.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   551
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   552
A net can store introduction rules indexed by their conclusion, and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   553
elimination rules indexed by their major premise.  Isabelle provides
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   554
several functions for `compiling' long lists of rules into fast
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   555
resolution tactics.  When supplied with a list of theorems, these functions
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   556
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
   557
goal.  To avoid repeatedly constructing the nets, use currying: bind the
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   558
resulting tactics to \ML{} identifiers.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   559
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   560
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   561
\item[\ttindexbold{net_resolve_tac} {\it thms}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   562
builds a discrimination net to obtain the effect of a similar call to {\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   563
resolve_tac}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   564
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   565
\item[\ttindexbold{net_match_tac} {\it thms}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   566
builds a discrimination net to obtain the effect of a similar call to {\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   567
match_tac}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   568
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   569
\item[\ttindexbold{net_biresolve_tac} {\it brls}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   570
builds a discrimination net to obtain the effect of a similar call to {\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   571
biresolve_tac}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   572
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   573
\item[\ttindexbold{net_bimatch_tac} {\it brls}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   574
builds a discrimination net to obtain the effect of a similar call to {\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   575
bimatch_tac}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   576
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   577
\item[\ttindexbold{filt_resolve_tac} {\it thms} {\it maxr} {\it i}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   578
uses discrimination nets to extract the {\it thms} that are applicable to
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   579
subgoal~$i$.  If more than {\it maxr\/} theorems are applicable then the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   580
tactic fails.  Otherwise it calls {\tt resolve_tac}.  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   581
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   582
This tactic helps avoid runaway instantiation of unknowns, for example in
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   583
type inference.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   584
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   585
\item[\ttindexbold{could_unify} ({\it t},{\it u})] 
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   586
returns {\tt false} if~$t$ and~$u$ are `obviously' non-unifiable, and
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   587
otherwise returns~{\tt true}.  It assumes all variables are distinct,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   588
reporting that {\tt ?a=?a} may unify with {\tt 0=1}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   589
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   590
\item[\ttindexbold{filter_thms} $could\; (limit,prem,thms)$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   591
returns the list of potentially resolvable rules (in {\it thms\/}) for the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   592
subgoal {\it prem}, using the predicate {\it could\/} to compare the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   593
conclusion of the subgoal with the conclusion of each rule.  The resulting list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   594
is no longer than {\it limit}.
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   595
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   596
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   597
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   598
\section{Programming tools for proof strategies}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   599
Do not consider using the primitives discussed in this section unless you
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   600
really need to code tactics from scratch.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   601
6618
13293a7d4a57 pdf setup;
wenzelm
parents: 5371
diff changeset
   602
\subsection{Operations on tactics}
3561
329441e7eeee Removal of tactical STATE
paulson
parents: 3400
diff changeset
   603
\index{tactics!primitives for coding} A tactic maps theorems to sequences of
329441e7eeee Removal of tactical STATE
paulson
parents: 3400
diff changeset
   604
theorems.  The type constructor for sequences (lazy lists) is called
4276
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3950
diff changeset
   605
\mltydx{Seq.seq}.  To simplify the types of tactics and tacticals,
3561
329441e7eeee Removal of tactical STATE
paulson
parents: 3400
diff changeset
   606
Isabelle defines a type abbreviation:
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   607
\begin{ttbox} 
4276
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3950
diff changeset
   608
type tactic = thm -> thm Seq.seq
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   609
\end{ttbox} 
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2612
diff changeset
   610
The following operations provide means for coding tactics in a clean style.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   611
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   612
PRIMITIVE :                  (thm -> thm) -> tactic  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   613
SUBGOAL   : ((term*int) -> tactic) -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   614
\end{ttbox} 
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   615
\begin{ttdescription}
3561
329441e7eeee Removal of tactical STATE
paulson
parents: 3400
diff changeset
   616
\item[\ttindexbold{PRIMITIVE} $f$] packages the meta-rule~$f$ as a tactic that
329441e7eeee Removal of tactical STATE
paulson
parents: 3400
diff changeset
   617
  applies $f$ to the proof state and returns the result as a one-element
329441e7eeee Removal of tactical STATE
paulson
parents: 3400
diff changeset
   618
  sequence.  If $f$ raises an exception, then the tactic's result is the empty
329441e7eeee Removal of tactical STATE
paulson
parents: 3400
diff changeset
   619
  sequence.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   620
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   621
\item[\ttindexbold{SUBGOAL} $f$ $i$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   622
extracts subgoal~$i$ from the proof state as a term~$t$, and computes a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   623
tactic by calling~$f(t,i)$.  It applies the resulting tactic to the same
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   624
state.  The tactic body is expressed using tactics and tacticals, but may
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   625
peek at a particular subgoal:
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   626
\begin{ttbox} 
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   627
SUBGOAL (fn (t,i) => {\it tactic-valued expression})
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   628
\end{ttbox} 
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   629
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   630
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   631
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   632
\subsection{Tracing}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   633
\index{tactics!tracing}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   634
\index{tracing!of tactics}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   635
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   636
pause_tac: tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   637
print_tac: tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   638
\end{ttbox}
332
01b87a921967 final Springer copy
lcp
parents: 323
diff changeset
   639
These tactics print tracing information when they are applied to a proof
01b87a921967 final Springer copy
lcp
parents: 323
diff changeset
   640
state.  Their output may be difficult to interpret.  Note that certain of
01b87a921967 final Springer copy
lcp
parents: 323
diff changeset
   641
the searching tacticals, such as {\tt REPEAT}, have built-in tracing
01b87a921967 final Springer copy
lcp
parents: 323
diff changeset
   642
options.
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   643
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   644
\item[\ttindexbold{pause_tac}] 
332
01b87a921967 final Springer copy
lcp
parents: 323
diff changeset
   645
prints {\footnotesize\tt** Press RETURN to continue:} and then reads a line
01b87a921967 final Springer copy
lcp
parents: 323
diff changeset
   646
from the terminal.  If this line is blank then it returns the proof state
01b87a921967 final Springer copy
lcp
parents: 323
diff changeset
   647
unchanged; otherwise it fails (which may terminate a repetition).
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   648
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   649
\item[\ttindexbold{print_tac}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   650
returns the proof state unchanged, with the side effect of printing it at
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   651
the terminal.
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   652
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   653
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   654
4276
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3950
diff changeset
   655
\section{*Sequences}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   656
\index{sequences (lazy lists)|bold}
4276
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3950
diff changeset
   657
The module {\tt Seq} declares a type of lazy lists.  It uses
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   658
Isabelle's type \mltydx{option} to represent the possible presence
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   659
(\ttindexbold{Some}) or absence (\ttindexbold{None}) of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   660
a value:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   661
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   662
datatype 'a option = None  |  Some of 'a;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   663
\end{ttbox}
4276
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3950
diff changeset
   664
The {\tt Seq} structure is supposed to be accessed via fully qualified
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   665
names and should not be \texttt{open}.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   666
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   667
\subsection{Basic operations on sequences}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   668
\begin{ttbox} 
4276
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3950
diff changeset
   669
Seq.empty   : 'a seq
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3950
diff changeset
   670
Seq.make    : (unit -> ('a * 'a seq) option) -> 'a seq
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3950
diff changeset
   671
Seq.single  : 'a -> 'a seq
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3950
diff changeset
   672
Seq.pull    : 'a seq -> ('a * 'a seq) option
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   673
\end{ttbox}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   674
\begin{ttdescription}
4276
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3950
diff changeset
   675
\item[Seq.empty] is the empty sequence.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   676
4276
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3950
diff changeset
   677
\item[\tt Seq.make (fn () => Some ($x$, $xq$))] constructs the
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3950
diff changeset
   678
  sequence with head~$x$ and tail~$xq$, neither of which is evaluated.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   679
4276
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3950
diff changeset
   680
\item[Seq.single $x$] 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   681
constructs the sequence containing the single element~$x$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   682
4276
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3950
diff changeset
   683
\item[Seq.pull $xq$] returns {\tt None} if the sequence is empty and
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3950
diff changeset
   684
  {\tt Some ($x$, $xq'$)} if the sequence has head~$x$ and tail~$xq'$.
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3950
diff changeset
   685
  Warning: calling \hbox{Seq.pull $xq$} again will {\it recompute\/}
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3950
diff changeset
   686
  the value of~$x$; it is not stored!
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   687
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   688
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   689
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   690
\subsection{Converting between sequences and lists}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   691
\begin{ttbox} 
4276
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3950
diff changeset
   692
Seq.chop    : int * 'a seq -> 'a list * 'a seq
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3950
diff changeset
   693
Seq.list_of : 'a seq -> 'a list
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3950
diff changeset
   694
Seq.of_list : 'a list -> 'a seq
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   695
\end{ttbox}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   696
\begin{ttdescription}
4276
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3950
diff changeset
   697
\item[Seq.chop ($n$, $xq$)] returns the first~$n$ elements of~$xq$ as a
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3950
diff changeset
   698
  list, paired with the remaining elements of~$xq$.  If $xq$ has fewer
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3950
diff changeset
   699
  than~$n$ elements, then so will the list.
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3950
diff changeset
   700
  
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3950
diff changeset
   701
\item[Seq.list_of $xq$] returns the elements of~$xq$, which must be
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3950
diff changeset
   702
  finite, as a list.
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3950
diff changeset
   703
  
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3950
diff changeset
   704
\item[Seq.of_list $xs$] creates a sequence containing the elements
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3950
diff changeset
   705
  of~$xs$.
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   706
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   707
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   708
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   709
\subsection{Combining sequences}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   710
\begin{ttbox} 
4276
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3950
diff changeset
   711
Seq.append      : 'a seq * 'a seq -> 'a seq
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3950
diff changeset
   712
Seq.interleave  : 'a seq * 'a seq -> 'a seq
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3950
diff changeset
   713
Seq.flat        : 'a seq seq -> 'a seq
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3950
diff changeset
   714
Seq.map         : ('a -> 'b) -> 'a seq -> 'b seq
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3950
diff changeset
   715
Seq.filter      : ('a -> bool) -> 'a seq -> 'a seq
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   716
\end{ttbox} 
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   717
\begin{ttdescription}
4276
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3950
diff changeset
   718
\item[Seq.append ($xq$, $yq$)] concatenates $xq$ to $yq$.
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3950
diff changeset
   719
  
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3950
diff changeset
   720
\item[Seq.interleave ($xq$, $yq$)] joins $xq$ with $yq$ by
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3950
diff changeset
   721
  interleaving their elements.  The result contains all the elements
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3950
diff changeset
   722
  of the sequences, even if both are infinite.
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3950
diff changeset
   723
  
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3950
diff changeset
   724
\item[Seq.flat $xqq$] concatenates a sequence of sequences.
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3950
diff changeset
   725
  
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3950
diff changeset
   726
\item[Seq.map $f$ $xq$] applies $f$ to every element
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3950
diff changeset
   727
  of~$xq=x@1,x@2,\ldots$, yielding the sequence $f(x@1),f(x@2),\ldots$.
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3950
diff changeset
   728
  
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3950
diff changeset
   729
\item[Seq.filter $p$ $xq$] returns the sequence consisting of all
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3950
diff changeset
   730
  elements~$x$ of~$xq$ such that $p(x)$ is {\tt true}.
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   731
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   732
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   733
\index{tactics|)}
5371
e27558a68b8d emacs local vars;
wenzelm
parents: 4607
diff changeset
   734
e27558a68b8d emacs local vars;
wenzelm
parents: 4607
diff changeset
   735
e27558a68b8d emacs local vars;
wenzelm
parents: 4607
diff changeset
   736
%%% Local Variables: 
e27558a68b8d emacs local vars;
wenzelm
parents: 4607
diff changeset
   737
%%% mode: latex
e27558a68b8d emacs local vars;
wenzelm
parents: 4607
diff changeset
   738
%%% TeX-master: "ref"
e27558a68b8d emacs local vars;
wenzelm
parents: 4607
diff changeset
   739
%%% End: