author paulson Thu, 26 Sep 1996 17:14:02 +0200 changeset 2039 79c86b966257 parent 2038 26b62963806c child 2040 6db93e6f1b11
Documented defer_tac and moved back the obsolete tactics like fold_tac
 doc-src/Ref/tactic.tex file | annotate | diff | comparison | revisions
--- a/doc-src/Ref/tactic.tex	Thu Sep 26 17:13:18 1996 +0200
+++ b/doc-src/Ref/tactic.tex	Thu Sep 26 17:14:02 1996 +0200
@@ -6,6 +6,10 @@
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 simplification (Chapter~\ref{simp-chap}) and classical 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
@@ -159,47 +163,6 @@

\section{Other basic tactics}
-\subsection{Definitions and meta-level rewriting}
-\index{tactics!meta-rewriting|bold}\index{meta-rewriting|bold}
-\index{definitions}
-
-Definitions in Isabelle have the form $t\equiv u$, where $t$ is typically a
-constant or a constant applied to a list of variables, for example $\it -sqr(n)\equiv n\times n$.  (Conditional definitions, $\phi\Imp t\equiv u$,
-are not supported.)  {\bf Unfolding} the definition ${t\equiv u}$ means using
-it as a rewrite rule, replacing~$t$ by~$u$ throughout a theorem.  {\bf
-Folding} $t\equiv u$ means replacing~$u$ by~$t$.  Rewriting continues until
-no rewrites are applicable to any subterm.
-
-There are rules for unfolding and folding definitions; Isabelle does not do
-this automatically.  The corresponding tactics rewrite the proof state,
-yielding a single next state.  See also the {\tt goalw} command, which is the
-easiest way of handling definitions.
-\begin{ttbox}
-rewrite_goals_tac : thm list -> tactic
-rewrite_tac       : thm list -> tactic
-fold_goals_tac    : thm list -> tactic
-fold_tac          : thm list -> tactic
-\end{ttbox}
-\begin{ttdescription}
-\item[\ttindexbold{rewrite_goals_tac} {\it defs}]
-unfolds the {\it defs} throughout the subgoals of the proof state, while
-leaving the main goal unchanged.  Use \ttindex{SELECT_GOAL} to restrict it to a
-particular subgoal.
-
-\item[\ttindexbold{rewrite_tac} {\it defs}]
-unfolds the {\it defs} throughout the proof state, including the main goal
---- not normally desirable!
-
-\item[\ttindexbold{fold_goals_tac} {\it defs}]
-folds the {\it defs} throughout the subgoals of the proof state, while
-leaving the main goal unchanged.
-
-\item[\ttindexbold{fold_tac} {\it defs}]
-folds the {\it defs} throughout the proof state.
-\end{ttdescription}
-
-
\subsection{Tactic shortcuts}
\index{shortcuts!for tactics}
\index{tactics!resolution}\index{tactics!assumption}
@@ -246,7 +209,7 @@
subgoal_tac   : string -> int -> tactic
subgoal_tacs  : string list -> int -> tactic
\end{ttbox}
-These tactics add assumptions to a given subgoal.
+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
@@ -272,6 +235,63 @@
\end{ttdescription}

+\subsection{Putting off'' a subgoal}
+\begin{ttbox}
+defer_tac : int -> tactic
+\end{ttbox}
+\begin{ttdescription}
+\item[\ttindexbold{defer_tac} {\it i}]
+  moves subgoal~$i$ to the last position in the proof state.  It can be
+  useful when correcting a proof script: if the tactic given for subgoal~$i$
+  fails, calling {\tt defer_tac} instead will let you continue with the rest
+  of the script.
+
+  The tactic fails if subgoal~$i$ does not exist or if the proof state
+  contains type unknowns.
+\end{ttdescription}
+
+
+\subsection{Definitions and meta-level rewriting}
+\index{tactics!meta-rewriting|bold}\index{meta-rewriting|bold}
+\index{definitions}
+
+Definitions in Isabelle have the form $t\equiv u$, where $t$ is typically a
+constant or a constant applied to a list of variables, for example $\it +sqr(n)\equiv n\times n$.  (Conditional definitions, $\phi\Imp t\equiv u$,
+are not supported.)  {\bf Unfolding} the definition ${t\equiv u}$ means using
+it as a rewrite rule, replacing~$t$ by~$u$ throughout a theorem.  {\bf
+Folding} $t\equiv u$ means replacing~$u$ by~$t$.  Rewriting continues until
+no rewrites are applicable to any subterm.
+
+There are rules for unfolding and folding definitions; Isabelle does not do
+this automatically.  The corresponding tactics rewrite the proof state,
+yielding a single next state.  See also the {\tt goalw} command, which is the
+easiest way of handling definitions.
+\begin{ttbox}
+rewrite_goals_tac : thm list -> tactic
+rewrite_tac       : thm list -> tactic
+fold_goals_tac    : thm list -> tactic
+fold_tac          : thm list -> tactic
+\end{ttbox}
+\begin{ttdescription}
+\item[\ttindexbold{rewrite_goals_tac} {\it defs}]
+unfolds the {\it defs} throughout the subgoals of the proof state, while
+leaving the main goal unchanged.  Use \ttindex{SELECT_GOAL} to restrict it to a
+particular subgoal.
+
+\item[\ttindexbold{rewrite_tac} {\it defs}]
+unfolds the {\it defs} throughout the proof state, including the main goal
+--- not normally desirable!
+
+\item[\ttindexbold{fold_goals_tac} {\it defs}]
+folds the {\it defs} throughout the subgoals of the proof state, while
+leaving the main goal unchanged.
+
+\item[\ttindexbold{fold_tac} {\it defs}]
+folds the {\it defs} throughout the proof state.
+\end{ttdescription}
+
+
\subsection{Theorems useful with tactics}
\index{theorems!of pure theory}
\begin{ttbox}
@@ -406,7 +426,7 @@
with the processing of large numbers of rules in automatic proof
strategies.  Higher-order resolution involving a long list of rules is
slow.  Filtering techniques can shorten the list of rules given to
-resolution, and can also detect whether a given subgoal is too flexible,
+resolution, and can also detect whether a subgoal is too flexible,
with too many rules applicable.

\subsection{Combined resolution and elim-resolution} \label{biresolve_tac}