doc-src/Ref/tactic.tex

Reverted to structure representation with records.

%% $Id$
\chapter{Tactics} \label{tactics}
\index{tactics|(} Tactics have type \mltydx{tactic}.  This is just an
abbreviation for functions from theorems to theorem sequences, where
the theorems represent states of a backward proof.  Tactics seldom
need to be coded from scratch, as functions; instead they are
expressed using basic tactics and tacticals.

This chapter only presents the primitive tactics.  Substantial proofs
require the power of automatic tools like simplification
(Chapter~\ref{chap:simplification}) and classical tableau reasoning
(Chapter~\ref{chap:classical}).

\section{Resolution and assumption tactics}
{\bf Resolution} is Isabelle's basic mechanism for refining a subgoal using
a rule.  {\bf Elim-resolution} is particularly suited for elimination
rules, while {\bf destruct-resolution} is particularly suited for
destruction rules.  The {\tt r}, {\tt e}, {\tt d} naming convention is
maintained for several different kinds of resolution tactics, as well as
the shortcuts in the subgoal module.

All the tactics in this section act on a subgoal designated by a positive
integer~$i$.  They fail (by returning the empty sequence) if~$i$ is out of
range.

\subsection{Resolution tactics}
\index{resolution!tactics}
\index{tactics!resolution|bold}
\begin{ttbox} 
resolve_tac  : thm list -> int -> tactic
eresolve_tac : thm list -> int -> tactic
dresolve_tac : thm list -> int -> tactic
forward_tac  : thm list -> int -> tactic 
\end{ttbox}
These perform resolution on a list of theorems, $thms$, representing a list
of object-rules.  When generating next states, they take each of the rules
in the order given.  Each rule may yield several next states, or none:
higher-order resolution may yield multiple resolvents.
\begin{ttdescription}
\item[\ttindexbold{resolve_tac} {\it thms} {\it i}] 
  refines the proof state using the rules, which should normally be
  introduction rules.  It resolves a rule's conclusion with
  subgoal~$i$ of the proof state.

\item[\ttindexbold{eresolve_tac} {\it thms} {\it i}] 
  \index{elim-resolution}
  performs elim-resolution with the rules, which should normally be
  elimination rules.  It resolves with a rule, proves its first premise by
  assumption, and finally \emph{deletes} that assumption from any new
  subgoals.  (To rotate a rule's premises,
  see \texttt{rotate_prems} in~{\S}\ref{MiscellaneousForwardRules}.)

\item[\ttindexbold{dresolve_tac} {\it thms} {\it i}] 
  \index{forward proof}\index{destruct-resolution}
  performs destruct-resolution with the rules, which normally should
  be destruction rules.  This replaces an assumption by the result of
  applying one of the rules.

\item[\ttindexbold{forward_tac}]\index{forward proof}
  is like {\tt dresolve_tac} except that the selected assumption is not
  deleted.  It applies a rule to an assumption, adding the result as a new
  assumption.
\end{ttdescription}

\subsection{Assumption tactics}
\index{tactics!assumption|bold}\index{assumptions!tactics for}
\begin{ttbox} 
assume_tac    : int -> tactic
eq_assume_tac : int -> tactic
\end{ttbox} 
\begin{ttdescription}
\item[\ttindexbold{assume_tac} {\it i}] 
attempts to solve subgoal~$i$ by assumption.

\item[\ttindexbold{eq_assume_tac}] 
is like {\tt assume_tac} but does not use unification.  It succeeds (with a
\emph{unique} next state) if one of the assumptions is identical to the
subgoal's conclusion.  Since it does not instantiate variables, it cannot
make other subgoals unprovable.  It is intended to be called from proof
strategies, not interactively.
\end{ttdescription}

\subsection{Matching tactics} \label{match_tac}
\index{tactics!matching}
\begin{ttbox} 
match_tac  : thm list -> int -> tactic
ematch_tac : thm list -> int -> tactic
dmatch_tac : thm list -> int -> tactic
\end{ttbox}
These are just like the resolution tactics except that they never
instantiate unknowns in the proof state.  Flexible subgoals are not updated
willy-nilly, but are left alone.  Matching --- strictly speaking --- means
treating the unknowns in the proof state as constants; these tactics merely
discard unifiers that would update the proof state.
\begin{ttdescription}
\item[\ttindexbold{match_tac} {\it thms} {\it i}] 
refines the proof state using the rules, matching a rule's
conclusion with subgoal~$i$ of the proof state.

\item[\ttindexbold{ematch_tac}] 
is like {\tt match_tac}, but performs elim-resolution.

\item[\ttindexbold{dmatch_tac}] 
is like {\tt match_tac}, but performs destruct-resolution.
\end{ttdescription}


\subsection{Explicit instantiation} \label{res_inst_tac}
\index{tactics!instantiation}\index{instantiation}
\begin{ttbox} 
res_inst_tac    : (string*string)list -> thm -> int -> tactic
eres_inst_tac   : (string*string)list -> thm -> int -> tactic
dres_inst_tac   : (string*string)list -> thm -> int -> tactic
forw_inst_tac   : (string*string)list -> thm -> int -> tactic
instantiate_tac : (string*string)list -> tactic
\end{ttbox}
The first four of these tactics are designed for applying rules by resolution
such as substitution and induction, which cause difficulties for higher-order 
unification.  The tactics accept explicit instantiations for unknowns 
in the rule ---typically, in the rule's conclusion. The last one, 
{\tt instantiate_tac}, may be used to instantiate unknowns in the proof state,
independently of rule application. 

Each instantiation is a pair {\tt($v$,$e$)}, 
where $v$ is an unknown \emph{without} its leading question mark!
\begin{itemize}
\item If $v$ is the type unknown {\tt'a}, then
the rule must contain a type unknown \verb$?'a$ of some
sort~$s$, and $e$ should be a type of sort $s$.

\item If $v$ is the unknown {\tt P}, then
the rule must contain an unknown \verb$?P$ of some type~$\tau$,
and $e$ should be a term of some type~$\sigma$ such that $\tau$ and
$\sigma$ are unifiable.  If the unification of $\tau$ and $\sigma$
instantiates any type unknowns in $\tau$, these instantiations
are recorded for application to the rule.
\end{itemize}
Types are instantiated before terms are.  Because type instantiations are
inferred from term instantiations, explicit type instantiations are seldom
necessary --- if \verb$?t$ has type \verb$?'a$, then the instantiation list
\texttt{[("'a","bool"), ("t","True")]} may be simplified to
\texttt{[("t","True")]}.  Type unknowns in the proof state may cause
failure because the tactics cannot instantiate them.

The first four instantiation tactics act on a given subgoal.  Terms in the
instantiations are type-checked in the context of that subgoal --- in
particular, they may refer to that subgoal's parameters.  Any unknowns in
the terms receive subscripts and are lifted over the parameters; thus, you
may not refer to unknowns in the subgoal.

\begin{ttdescription}
\item[\ttindexbold{res_inst_tac} {\it insts} {\it thm} {\it i}]
instantiates the rule {\it thm} with the instantiations {\it insts}, as
described above, and then performs resolution on subgoal~$i$.  Resolution
typically causes further instantiations; you need not give explicit
instantiations for every unknown in the rule.

\item[\ttindexbold{eres_inst_tac}] 
is like {\tt res_inst_tac}, but performs elim-resolution.

\item[\ttindexbold{dres_inst_tac}] 
is like {\tt res_inst_tac}, but performs destruct-resolution.

\item[\ttindexbold{forw_inst_tac}] 
is like {\tt dres_inst_tac} except that the selected assumption is not
deleted.  It applies the instantiated rule to an assumption, adding the
result as a new assumption.

\item[\ttindexbold{instantiate_tac} {\it insts}] 
instantiates unknowns in the proof state. This affects the main goal as 
well as all subgoals.
\end{ttdescription}


\section{Other basic tactics}
\subsection{Tactic shortcuts}
\index{shortcuts!for tactics}
\index{tactics!resolution}\index{tactics!assumption}
\index{tactics!meta-rewriting}
\begin{ttbox} 
rtac     :      thm ->        int -> tactic
etac     :      thm ->        int -> tactic
dtac     :      thm ->        int -> tactic
ftac     :      thm ->        int -> tactic
atac     :                    int -> tactic
eatac    :      thm -> int -> int -> tactic
datac    :      thm -> int -> int -> tactic
fatac    :      thm -> int -> int -> tactic
ares_tac :      thm list   -> int -> tactic
rewtac   :      thm ->               tactic
\end{ttbox}
These abbreviate common uses of tactics.
\begin{ttdescription}
\item[\ttindexbold{rtac} {\it thm} {\it i}] 
abbreviates \hbox{\tt resolve_tac [{\it thm}] {\it i}}, doing resolution.

\item[\ttindexbold{etac} {\it thm} {\it i}] 
abbreviates \hbox{\tt eresolve_tac [{\it thm}] {\it i}}, doing elim-resolution.

\item[\ttindexbold{dtac} {\it thm} {\it i}] 
abbreviates \hbox{\tt dresolve_tac [{\it thm}] {\it i}}, doing
destruct-resolution.

\item[\ttindexbold{ftac} {\it thm} {\it i}] 
abbreviates \hbox{\tt forward_tac [{\it thm}] {\it i}}, doing
destruct-resolution without deleting the assumption.

\item[\ttindexbold{atac} {\it i}] 
abbreviates \hbox{\tt assume_tac {\it i}}, doing proof by assumption.

\item[\ttindexbold{eatac} {\it thm} {\it j} {\it i}] 
performs \hbox{\tt etac {\it thm}} and then {\it j} times \texttt{atac}, 
solving additionally {\it j}~premises of the rule {\it thm} by assumption.

\item[\ttindexbold{datac} {\it thm} {\it j} {\it i}] 
performs \hbox{\tt dtac {\it thm}} and then {\it j} times \texttt{atac}, 
solving additionally {\it j}~premises of the rule {\it thm} by assumption.

\item[\ttindexbold{fatac} {\it thm} {\it j} {\it i}] 
performs \hbox{\tt ftac {\it thm}} and then {\it j} times \texttt{atac}, 
solving additionally {\it j}~premises of the rule {\it thm} by assumption.

\item[\ttindexbold{ares_tac} {\it thms} {\it i}] 
tries proof by assumption and resolution; it abbreviates
\begin{ttbox}
assume_tac {\it i} ORELSE resolve_tac {\it thms} {\it i}
\end{ttbox}

\item[\ttindexbold{rewtac} {\it def}] 
abbreviates \hbox{\tt rewrite_goals_tac [{\it def}]}, unfolding a definition.
\end{ttdescription}


\subsection{Inserting premises and facts}\label{cut_facts_tac}
\index{tactics!for inserting facts}\index{assumptions!inserting}
\begin{ttbox} 
cut_facts_tac : thm list -> int -> tactic
cut_inst_tac  : (string*string)list -> thm -> int -> tactic
subgoal_tac   : string -> int -> tactic
subgoals_tac  : string list -> int -> tactic
\end{ttbox}
These tactics add assumptions to a subgoal.
\begin{ttdescription}
\item[\ttindexbold{cut_facts_tac} {\it thms} {\it i}] 
  adds the {\it thms} as new assumptions to subgoal~$i$.  Once they have
  been inserted as assumptions, they become subject to tactics such as {\tt
    eresolve_tac} and {\tt rewrite_goals_tac}.  Only rules with no premises
  are inserted: Isabelle cannot use assumptions that contain $\Imp$
  or~$\Forall$.  Sometimes the theorems are premises of a rule being
  derived, returned by~{\tt goal}; instead of calling this tactic, you
  could state the goal with an outermost meta-quantifier.

\item[\ttindexbold{cut_inst_tac} {\it insts} {\it thm} {\it i}]
  instantiates the {\it thm} with the instantiations {\it insts}, as
  described in {\S}\ref{res_inst_tac}.  It adds the resulting theorem as a
  new assumption to subgoal~$i$. 

\item[\ttindexbold{subgoal_tac} {\it formula} {\it i}] 
adds the {\it formula} as an assumption to subgoal~$i$, and inserts the same
{\it formula} as a new subgoal, $i+1$.

\item[\ttindexbold{subgoals_tac} {\it formulae} {\it i}] 
  uses {\tt subgoal_tac} to add the members of the list of {\it
    formulae} as assumptions to subgoal~$i$. 
\end{ttdescription}