# HG changeset patch # User paulson # Date 843750842 -7200 # Node ID 79c86b966257d1567f83e10d779d37065369ada1 # Parent 26b62963806c5768c58bbca87a7ce34894f3f45f Documented defer_tac and moved back the obsolete tactics like fold_tac diff -r 26b62963806c -r 79c86b966257 doc-src/Ref/tactic.tex --- 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}