summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

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}