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