author nipkow Thu, 22 May 1997 10:49:33 +0200 changeset 3287 078be5581967 parent 3286 321f49dae373 child 3288 f38eb5eb9fac
Documented exhaust_tac.
 doc-src/Logics/HOL.tex file | annotate | diff | comparison | revisions doc-src/Logics/logics.tex file | annotate | diff | comparison | revisions
--- a/doc-src/Logics/HOL.tex	Thu May 22 10:40:08 1997 +0200
+++ b/doc-src/Logics/HOL.tex	Thu May 22 10:49:33 1997 +0200
@@ -1377,9 +1377,9 @@
Figure~\ref{hol-list} presents the theory \thydx{List}: the basic list
operations with their types and syntax. Type $\alpha \; list$ is
defined as a {\tt datatype} with the constructors {\tt[]} and {\tt\#}.
-As a result the generic induction tactic \ttindex{induct_tac} also
-performs structural induction over lists. A \sdx{case} construct of
-the form
+As a result the generic structural induction and case analysis tactics
+\texttt{induct\_tac} and \texttt{exhaust\_tac} also become available for
+lists. A \sdx{case} construct of the form
\begin{center}\tt
case $e$ of [] => $a$  |  $$x$$\#$$xs$$ => b
\end{center}
@@ -1637,6 +1637,19 @@
applies structural induction on variable $x$ to subgoal $i$, provided the
type of $x$ is a datatype or type {\tt nat}.
\end{ttdescription}
+In some cases, induction is overkill and a case distinction over all
+constructors of the datatype suffices:
+\begin{ttdescription}
+\item[\ttindexbold{exhaust_tac} {\tt"}$u${\tt"} $i$]
+ performs an exhaustive case analysis for an arbitrary term $u$ whose type
+ must be a datatyp or type {\tt nat}. If the datatype has $n$ constructors
+ $C@1$, \dots $C@n$, subgoal $i$ is replaced by $n$ new subgoals which
+ contain the additional assumption $u = C@j~x@1~\dots~x@{k@j}$ for
+ $j=1,\dots,n$.
+
+Note that in contrast to induction, exhaustion is possible even if $u$
+mentions identifiers that occur in the assumptions of the subgoal.
+\end{ttdescription}

For the technically minded, we give a more detailed description.
Reading the theory file produces a structure which, in addition to the
--- a/doc-src/Logics/logics.tex	Thu May 22 10:40:08 1997 +0200
+++ b/doc-src/Logics/logics.tex	Thu May 22 10:49:33 1997 +0200
@@ -1,7 +1,8 @@
\documentclass[12pt]{report}
-\usepackage{a4,latexsym,proof}
+\usepackage{a4,latexsym}

\makeatletter
+\input{../proof.sty}
\input{../rail.sty}
\input{../iman.sty}
\input{../extra.sty}