author nipkow Sun, 02 Nov 1997 13:47:58 +0100 changeset 4067 207a7811faa9 parent 4066 7b508ac609f7 child 4068 99224854a0ac
Documented split_t_case' thm genearted by datatype.
 doc-src/Logics/HOL.tex file | annotate | diff | comparison | revisions
--- a/doc-src/Logics/HOL.tex	Sat Nov 01 13:03:00 1997 +0100
+++ b/doc-src/Logics/HOL.tex	Sun Nov 02 13:47:58 1997 +0100
@@ -1398,7 +1398,7 @@
case $e$ of [] => $a$  |  $$x$$\#$$xs$$ => b
\end{center}
is defined by translation.  For details see~\S\ref{sec:HOL:datatype}. There
-is also a case splitting rule \tdx{expand_list_case}
+is also a case splitting rule \tdx{split_list_case}
$\begin{array}{l} P(\mathtt{case}~e~\mathtt{of}~\texttt{[] =>}~a ~\texttt{|}~ @@ -1631,6 +1631,22 @@ Violating this restriction results in strange error messages. \end{warn} +To perform case distinction on a goal containing a \texttt{case}-construct, +the theorem \texttt{split_}t\texttt{_case} is provided: +\[ +\begin{array}{@{}rcl@{}} +P(t_\mathtt{case}~f@1~\dots~f@m~e) &=& +((\forall x@1 \dots x@{k@1}. e = C@1~x@1\dots x@{k@1} \to + P(f@1~~x@1\dots x@{k@1})) \\ +&& ~\land~ \dots ~\land \\ +&&~ (\forall x@1 \dots x@{k@m}. e = C@m~x@1\dots x@{k@m} \to + P(f@m~~x@1\dots x@{k@m}))) +\end{array} +$
+where $t$\texttt{_case} is the internal name of the \texttt{case}-construct.
+(see~\S\ref{subsec:HOL:case:splitting}).
+
\subsubsection{The function \cdx{size}}\label{sec:HOL:size}

Theory \texttt{Arith} declares an overloaded function \texttt{size} of type
@@ -1698,7 +1714,7 @@
\end{ttdescription}
\begin{warn}
Induction is only allowed on a free variable that should not occur among
-  the premises of the subgoal.  Exhaustion is works for arbitrary terms.
+  the premises of the subgoal.  Exhaustion works for arbitrary terms.
\end{warn}
\bigskip
`