doc-src/Ref/tactic.tex
author haftmann
Thu, 12 Nov 2009 15:49:01 +0100
changeset 33633 9f7280e0c231
parent 30184 37969710e61f
child 46257 3ba3681d8930
permissions -rw-r--r--
explicit code lemmas produce nices code
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
30184
37969710e61f removed parts of the manual that are clearly obsolete, or covered by
wenzelm
parents: 17818
diff changeset
     1
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     2
\chapter{Tactics} \label{tactics}
30184
37969710e61f removed parts of the manual that are clearly obsolete, or covered by
wenzelm
parents: 17818
diff changeset
     3
\index{tactics|(}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     4
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     5
\section{Other basic tactics}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     6
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     7
\subsection{Inserting premises and facts}\label{cut_facts_tac}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
     8
\index{tactics!for inserting facts}\index{assumptions!inserting}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     9
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    10
cut_facts_tac : thm list -> int -> tactic
286
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
    11
cut_inst_tac  : (string*string)list -> thm -> int -> tactic
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
    12
subgoal_tac   : string -> int -> tactic
9523
232b09dba0fe subgoals_tac: fixed spelling;
wenzelm
parents: 8136
diff changeset
    13
subgoals_tac  : string list -> int -> tactic
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    14
\end{ttbox}
2039
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    15
These tactics add assumptions to a subgoal.
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
    16
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    17
\item[\ttindexbold{cut_facts_tac} {\it thms} {\it i}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    18
  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
    19
  been inserted as assumptions, they become subject to tactics such as {\tt
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
    20
    eresolve_tac} and {\tt rewrite_goals_tac}.  Only rules with no premises
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
    21
  are inserted: Isabelle cannot use assumptions that contain $\Imp$
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
    22
  or~$\Forall$.  Sometimes the theorems are premises of a rule being
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
    23
  derived, returned by~{\tt goal}; instead of calling this tactic, you
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
    24
  could state the goal with an outermost meta-quantifier.
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
    25
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
    26
\item[\ttindexbold{cut_inst_tac} {\it insts} {\it thm} {\it i}]
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
    27
  instantiates the {\it thm} with the instantiations {\it insts}, as
7491
95a4af0e10a7 added ftac, eatac, datac, fatac
oheimb
parents: 6618
diff changeset
    28
  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
    29
  new assumption to subgoal~$i$. 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    30
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    31
\item[\ttindexbold{subgoal_tac} {\it formula} {\it i}] 
9568
20c410fb5104 fixed spelling;
wenzelm
parents: 9523
diff changeset
    32
adds the {\it formula} as an assumption to subgoal~$i$, and inserts the same
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    33
{\it formula} as a new subgoal, $i+1$.
457
8577bc1c4e1b documented subgoals_tac
lcp
parents: 332
diff changeset
    34
8577bc1c4e1b documented subgoals_tac
lcp
parents: 332
diff changeset
    35
\item[\ttindexbold{subgoals_tac} {\it formulae} {\it i}] 
8577bc1c4e1b documented subgoals_tac
lcp
parents: 332
diff changeset
    36
  uses {\tt subgoal_tac} to add the members of the list of {\it
8577bc1c4e1b documented subgoals_tac
lcp
parents: 332
diff changeset
    37
    formulae} as assumptions to subgoal~$i$. 
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
    38
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    39
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    40
2039
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    41
\subsection{``Putting off'' a subgoal}
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    42
\begin{ttbox} 
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    43
defer_tac : int -> tactic
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    44
\end{ttbox}
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    45
\begin{ttdescription}
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    46
\item[\ttindexbold{defer_tac} {\it i}] 
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    47
  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
    48
  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
    49
  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
    50
  of the script.
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    51
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    52
  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
    53
  contains type unknowns. 
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    54
\end{ttdescription}
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    55
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    56
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
    57
\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
    58
\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
    59
\index{definitions}
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    60
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    61
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
    62
constant or a constant applied to a list of variables, for example $\it
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
    63
sqr(n)\equiv n\times n$.  Conditional definitions, $\phi\Imp t\equiv u$,
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
    64
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
    65
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
    66
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
    67
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
    68
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    69
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
    70
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
    71
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
    72
easiest way of handling definitions.
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    73
\begin{ttbox} 
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    74
rewrite_goals_tac : thm list -> tactic
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    75
rewrite_tac       : thm list -> tactic
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    76
fold_goals_tac    : thm list -> tactic
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    77
fold_tac          : thm list -> tactic
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    78
\end{ttbox}
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    79
\begin{ttdescription}
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    80
\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
    81
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
    82
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
    83
particular subgoal.
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    84
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    85
\item[\ttindexbold{rewrite_tac} {\it defs}]  
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    86
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
    87
--- not normally desirable!
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    88
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    89
\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
    90
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
    91
leaving the main goal unchanged.
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    92
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    93
\item[\ttindexbold{fold_tac} {\it defs}]  
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    94
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
    95
\end{ttdescription}
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
    96
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
    97
\begin{warn}
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
    98
  These tactics only cope with definitions expressed as meta-level
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
    99
  equalities ($\equiv$).  More general equivalences are handled by the
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   100
  simplifier, provided that it is set up appropriately for your logic
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   101
  (see Chapter~\ref{chap:simplification}).
7264fa2ff2ec several minor updates;
wenzelm
parents: 4276
diff changeset
   102
\end{warn}
2039
79c86b966257 Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents: 1212
diff changeset
   103
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   104
\subsection{Theorems useful with tactics}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   105
\index{theorems!of pure theory}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   106
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   107
asm_rl: thm 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   108
cut_rl: thm 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   109
\end{ttbox}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   110
\begin{ttdescription}
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   111
\item[\tdx{asm_rl}] 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   112
is $\psi\Imp\psi$.  Under elim-resolution it does proof by assumption, and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   113
\hbox{\tt eresolve_tac (asm_rl::{\it thms}) {\it i}} is equivalent to
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   114
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   115
assume_tac {\it i}  ORELSE  eresolve_tac {\it thms} {\it i}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   116
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   117
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   118
\item[\tdx{cut_rl}] 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   119
is $\List{\psi\Imp\theta,\psi}\Imp\theta$.  It is useful for inserting
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   120
assumptions; it underlies {\tt forward_tac}, {\tt cut_facts_tac}
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   121
and {\tt subgoal_tac}.
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   122
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   123
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   124
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   125
\section{Obscure tactics}
1212
7059356e18e0 added rotate_tac
nipkow
parents: 457
diff changeset
   126
2612
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   127
\subsection{Manipulating assumptions}
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   128
\index{assumptions!rotating}
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   129
\begin{ttbox} 
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   130
thin_tac   : string -> int -> tactic
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   131
rotate_tac : int -> int -> tactic
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   132
\end{ttbox}
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   133
\begin{ttdescription}
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   134
\item[\ttindexbold{thin_tac} {\it formula} $i$]  
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   135
\index{assumptions!deleting}
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   136
deletes the specified assumption from subgoal $i$.  Often the assumption
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   137
can be abbreviated, replacing subformul{\ae} by unknowns; the first matching
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   138
assumption will be deleted.  Removing useless assumptions from a subgoal
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   139
increases its readability and can make search tactics run faster.
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   140
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   141
\item[\ttindexbold{rotate_tac} $n$ $i$]  
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   142
\index{assumptions!rotating}
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   143
rotates the assumptions of subgoal $i$ by $n$ positions: from right to left
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   144
if $n$ is positive, and from left to right if $n$ is negative.  This is 
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   145
sometimes necessary in connection with \ttindex{asm_full_simp_tac}, which 
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   146
processes assumptions from left to right.
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   147
\end{ttdescription}
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   148
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   149
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   150
\subsection{Tidying the proof state}
3400
80c979e0d42f Documented the new distinct_subgoals_tac
paulson
parents: 3108
diff changeset
   151
\index{duplicate subgoals!removing}
2612
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   152
\index{parameters!removing unused}
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   153
\index{flex-flex constraints}
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   154
\begin{ttbox} 
3400
80c979e0d42f Documented the new distinct_subgoals_tac
paulson
parents: 3108
diff changeset
   155
distinct_subgoals_tac : tactic
80c979e0d42f Documented the new distinct_subgoals_tac
paulson
parents: 3108
diff changeset
   156
prune_params_tac      : tactic
80c979e0d42f Documented the new distinct_subgoals_tac
paulson
parents: 3108
diff changeset
   157
flexflex_tac          : tactic
2612
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   158
\end{ttbox}
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   159
\begin{ttdescription}
9695
ec7d7f877712 proper setup of iman.sty/extra.sty/ttbox.sty;
wenzelm
parents: 9568
diff changeset
   160
\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
   161
  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
   162
  essentially type constraints.)
3400
80c979e0d42f Documented the new distinct_subgoals_tac
paulson
parents: 3108
diff changeset
   163
2612
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   164
\item[\ttindexbold{prune_params_tac}]  
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   165
  removes unused parameters from all subgoals of the proof state.  It works
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   166
  by rewriting with the theorem $(\Forall x. V)\equiv V$.  This tactic can
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   167
  make the proof state more readable.  It is used with
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   168
  \ttindex{rule_by_tactic} to simplify the resulting theorem.
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   169
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   170
\item[\ttindexbold{flexflex_tac}]  
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   171
  removes all flex-flex pairs from the proof state by applying the trivial
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   172
  unifier.  This drastic step loses information, and should only be done as
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   173
  the last step of a proof.
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   174
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   175
  Flex-flex constraints arise from difficult cases of higher-order
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   176
  unification.  To prevent this, use \ttindex{res_inst_tac} to instantiate
7491
95a4af0e10a7 added ftac, eatac, datac, fatac
oheimb
parents: 6618
diff changeset
   177
  some variables in a rule~({\S}\ref{res_inst_tac}).  Normally flex-flex
2612
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   178
  constraints can be ignored; they often disappear as unknowns get
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   179
  instantiated.
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   180
\end{ttdescription}
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   181
28232396b60e Documented thin_tac
paulson
parents: 2039
diff changeset
   182
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   183
\subsection{Composition: resolution without lifting}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   184
\index{tactics!for composition}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   185
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   186
compose_tac: (bool * thm * int) -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   187
\end{ttbox}
332
01b87a921967 final Springer copy
lcp
parents: 323
diff changeset
   188
{\bf Composing} two rules means resolving them without prior lifting or
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   189
renaming of unknowns.  This low-level operation, which underlies the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   190
resolution tactics, may occasionally be useful for special effects.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   191
A typical application is \ttindex{res_inst_tac}, which lifts and instantiates a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   192
rule, then passes the result to {\tt compose_tac}.
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   193
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   194
\item[\ttindexbold{compose_tac} ($flag$, $rule$, $m$) $i$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   195
refines subgoal~$i$ using $rule$, without lifting.  The $rule$ is taken to
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   196
have the form $\List{\psi@1; \ldots; \psi@m} \Imp \psi$, where $\psi$ need
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   197
not be atomic; thus $m$ determines the number of new subgoals.  If
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   198
$flag$ is {\tt true} then it performs elim-resolution --- it solves the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   199
first premise of~$rule$ by assumption and deletes that assumption.
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   200
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   201
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   202
4276
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3950
diff changeset
   203
\section{*Managing lots of rules}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   204
These operations are not intended for interactive use.  They are concerned
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   205
with the processing of large numbers of rules in automatic proof
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   206
strategies.  Higher-order resolution involving a long list of rules is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   207
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
   208
resolution, and can also detect whether a subgoal is too flexible,
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   209
with too many rules applicable.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   210
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   211
\subsection{Combined resolution and elim-resolution} \label{biresolve_tac}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   212
\index{tactics!resolution}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   213
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   214
biresolve_tac   : (bool*thm)list -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   215
bimatch_tac     : (bool*thm)list -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   216
subgoals_of_brl : bool*thm -> int
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   217
lessb           : (bool*thm) * (bool*thm) -> bool
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   218
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   219
{\bf Bi-resolution} takes a list of $\it (flag,rule)$ pairs.  For each
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   220
pair, it applies resolution if the flag is~{\tt false} and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   221
elim-resolution if the flag is~{\tt true}.  A single tactic call handles a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   222
mixture of introduction and elimination rules.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   223
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   224
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   225
\item[\ttindexbold{biresolve_tac} {\it brls} {\it i}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   226
refines the proof state by resolution or elim-resolution on each rule, as
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   227
indicated by its flag.  It affects subgoal~$i$ of the proof state.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   228
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   229
\item[\ttindexbold{bimatch_tac}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   230
is like {\tt biresolve_tac}, but performs matching: unknowns in the
7491
95a4af0e10a7 added ftac, eatac, datac, fatac
oheimb
parents: 6618
diff changeset
   231
proof state are never updated (see~{\S}\ref{match_tac}).
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   232
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   233
\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
   234
returns the number of new subgoals that bi-res\-o\-lu\-tion would yield for the
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   235
pair (if applied to a suitable subgoal).  This is $n$ if the flag is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   236
{\tt false} and $n-1$ if the flag is {\tt true}, where $n$ is the number
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   237
of premises of the rule.  Elim-resolution yields one fewer subgoal than
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   238
ordinary resolution because it solves the major premise by assumption.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   239
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   240
\item[\ttindexbold{lessb} ({\it brl1},{\it brl2})] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   241
returns the result of 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   242
\begin{ttbox}
332
01b87a921967 final Springer copy
lcp
parents: 323
diff changeset
   243
subgoals_of_brl{\it brl1} < subgoals_of_brl{\it brl2}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   244
\end{ttbox}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   245
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   246
Note that \hbox{\tt sort lessb {\it brls}} sorts a list of $\it
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   247
(flag,rule)$ pairs by the number of new subgoals they will yield.  Thus,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   248
those that yield the fewest subgoals should be tried first.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   249
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   250
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   251
\subsection{Discrimination nets for fast resolution}\label{filt_resolve_tac}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   252
\index{discrimination nets|bold}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   253
\index{tactics!resolution}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   254
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   255
net_resolve_tac  : thm list -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   256
net_match_tac    : thm list -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   257
net_biresolve_tac: (bool*thm) list -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   258
net_bimatch_tac  : (bool*thm) list -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   259
filt_resolve_tac : thm list -> int -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   260
could_unify      : term*term->bool
8136
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 7491
diff changeset
   261
filter_thms      : (term*term->bool) -> int*term*thm list -> thm{\ts}list
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   262
\end{ttbox}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   263
The module {\tt Net} implements a discrimination net data structure for
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   264
fast selection of rules \cite[Chapter 14]{charniak80}.  A term is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   265
classified by the symbol list obtained by flattening it in preorder.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   266
The flattening takes account of function applications, constants, and free
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   267
and bound variables; it identifies all unknowns and also regards
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   268
\index{lambda abs@$\lambda$-abstractions}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   269
$\lambda$-abstractions as unknowns, since they could $\eta$-contract to
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   270
anything.  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   271
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   272
A discrimination net serves as a polymorphic dictionary indexed by terms.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   273
The module provides various functions for inserting and removing items from
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   274
nets.  It provides functions for returning all items whose term could match
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   275
or unify with a target term.  The matching and unification tests are
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   276
overly lax (due to the identifications mentioned above) but they serve as
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   277
useful filters.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   278
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   279
A net can store introduction rules indexed by their conclusion, and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   280
elimination rules indexed by their major premise.  Isabelle provides
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   281
several functions for `compiling' long lists of rules into fast
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   282
resolution tactics.  When supplied with a list of theorems, these functions
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   283
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
   284
goal.  To avoid repeatedly constructing the nets, use currying: bind the
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   285
resulting tactics to \ML{} identifiers.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   286
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   287
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   288
\item[\ttindexbold{net_resolve_tac} {\it thms}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   289
builds a discrimination net to obtain the effect of a similar call to {\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   290
resolve_tac}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   291
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   292
\item[\ttindexbold{net_match_tac} {\it thms}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   293
builds a discrimination net to obtain the effect of a similar call to {\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   294
match_tac}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   295
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   296
\item[\ttindexbold{net_biresolve_tac} {\it brls}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   297
builds a discrimination net to obtain the effect of a similar call to {\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   298
biresolve_tac}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   299
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   300
\item[\ttindexbold{net_bimatch_tac} {\it brls}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   301
builds a discrimination net to obtain the effect of a similar call to {\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   302
bimatch_tac}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   303
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   304
\item[\ttindexbold{filt_resolve_tac} {\it thms} {\it maxr} {\it i}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   305
uses discrimination nets to extract the {\it thms} that are applicable to
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   306
subgoal~$i$.  If more than {\it maxr\/} theorems are applicable then the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   307
tactic fails.  Otherwise it calls {\tt resolve_tac}.  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   308
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   309
This tactic helps avoid runaway instantiation of unknowns, for example in
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   310
type inference.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   311
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   312
\item[\ttindexbold{could_unify} ({\it t},{\it u})] 
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   313
returns {\tt false} if~$t$ and~$u$ are `obviously' non-unifiable, and
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   314
otherwise returns~{\tt true}.  It assumes all variables are distinct,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   315
reporting that {\tt ?a=?a} may unify with {\tt 0=1}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   316
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   317
\item[\ttindexbold{filter_thms} $could\; (limit,prem,thms)$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   318
returns the list of potentially resolvable rules (in {\it thms\/}) for the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   319
subgoal {\it prem}, using the predicate {\it could\/} to compare the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   320
conclusion of the subgoal with the conclusion of each rule.  The resulting list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   321
is no longer than {\it limit}.
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   322
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   323
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   324
\index{tactics|)}
5371
e27558a68b8d emacs local vars;
wenzelm
parents: 4607
diff changeset
   325
e27558a68b8d emacs local vars;
wenzelm
parents: 4607
diff changeset
   326
e27558a68b8d emacs local vars;
wenzelm
parents: 4607
diff changeset
   327
%%% Local Variables: 
e27558a68b8d emacs local vars;
wenzelm
parents: 4607
diff changeset
   328
%%% mode: latex
e27558a68b8d emacs local vars;
wenzelm
parents: 4607
diff changeset
   329
%%% TeX-master: "ref"
e27558a68b8d emacs local vars;
wenzelm
parents: 4607
diff changeset
   330
%%% End: