Documented exhaust_tac.
Thu, 22 May 1997 10:49:33 +0200
changeset 3287 078be5581967
parent 3286 321f49dae373
child 3288 f38eb5eb9fac
Documented exhaust_tac.
--- 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
 case $e$ of [] => $a$  |  \(x\)\#\(xs\) => b
@@ -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}.
+In some cases, induction is overkill and a case distinction over all
+constructors of the datatype suffices:
+\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.
 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 @@