# HG changeset patch
# User nipkow
# Date 877360914 -7200
# Node ID 033633d9a0323953a57068214f009148f284d91c
# Parent  78a8e9a1c2f9fe265192a159ab8c4aed15a1ff9c
Documented `addsplits'

diff -r 78a8e9a1c2f9 -r 033633d9a032 doc-src/Logics/HOL.tex
--- a/doc-src/Logics/HOL.tex	Mon Oct 20 17:08:18 1997 +0200
+++ b/doc-src/Logics/HOL.tex	Mon Oct 20 17:21:54 1997 +0200
@@ -260,9 +260,9 @@
 \begin{warn}
 Both \texttt{if} and \texttt{case} constructs have as low a priority as
 quantifiers, which requires additional enclosing parentheses in the context
-of most other operations.  For example, instead of $f~x = if \dots then \dots
-else \dots$ you need to write $f~x = (if \dots then \dots else
-\dots)$.
+of most other operations.  For example, instead of $f~x = {\tt if\dots
+then\dots else}\dots$ you need to write $f~x = ({\tt if\dots then\dots
+else\dots})$.
 \end{warn}
 
 \section{Rules of inference}
@@ -942,6 +942,46 @@
   for an equality throughout a subgoal and its hypotheses.  This tactic uses
   \HOL's general substitution rule.
 
+\subsubsection{Case splitting}
+\label{subsec:HOL:case:splitting}
+
+\HOL{} also provides convenient means for case splitting during
+  rewriting. Goals containing a subterm of the form {\tt if}~$b$~{\tt
+then\dots else\dots} often require a case distinction on $b$. This is
+expressed by the theorem \tdx{expand_if}:
+$$
+\Var{P}(\mbox{\tt if}~\Var{b}~{\tt then}~\Var{x}~\mbox{\tt else}~\Var{y})~=~
+((\Var{b} \to \Var{P}(\Var{x})) \land (\neg \Var{b} \to \Var{P}(\Var{y})))
+\eqno{(*)}
+$$
+For example, a simple instance of $(*)$ is
+\[
+x \in (\mbox{\tt if}~x \in A~{\tt then}~A~\mbox{\tt else}~\{x\})~=~
+((x \in A \to x \in A) \land (x \notin A \to x \in \{x\}))
+\]
+Because $(*)$ is too general as a rewrite rule for the simplifier (the
+left-hand side is not a higher-order pattern in the sense of
+\iflabelundefined{chap:simplification}{the {\em Reference Manual\/}}%
+{Chap.\ts\ref{chap:simplification}}), there is a special infix function 
+\ttindexbold{addsplits} (analogous to \texttt{addsimps}) of type
+\texttt{simpset * thm list -> simpset} that adds rules such as $(*)$ to a
+simpset, as in
+\begin{ttbox}
+by(simp_tac (!simpset addsplits [expand_if]) 1);
+\end{ttbox}
+The effect is that after each round of simplification, one occurrence of
+\texttt{if} is split acording to \texttt{expand_if}, until all occurences of
+\texttt{if} have been eliminated.
+
+In general, \texttt{addsplits} accepts rules of the form
+\[
+\Var{P}(c~\Var{x@1}~\dots~\Var{x@n})~=~ rhs
+\]
+where $c$ is a constant and $rhs$ is arbitrary. Note that $(*)$ is of the
+right form because internally the left-hand side is
+$\Var{P}(\mathtt{If}~\Var{b}~\Var{x}~~\Var{y})$. Important further examples
+are splitting rules for \texttt{case} expressions (see~\S\ref{subsec:list}
+and~\S\ref{subsec:datatype:basics}).
 
 \subsection{Classical reasoning}
 
@@ -1345,6 +1385,7 @@
 
 
 \subsection{The type constructor for lists, \textit{list}}
+\label{subsec:list}
 \index{list@{\textit{list}} type|(}
 
 Figure~\ref{hol-list} presents the theory \thydx{List}: the basic list
@@ -1356,7 +1397,18 @@
 \begin{center}\tt
 case $e$ of [] => $a$  |  \(x\)\#\(xs\) => b
 \end{center}
-is defined by translation.  For details see~\S\ref{sec:HOL:datatype}.
+is defined by translation.  For details see~\S\ref{sec:HOL:datatype}. There
+is also a case splitting rule \tdx{expand_list_case}
+\[
+\begin{array}{l}
+P(\mathtt{case}~e~\mathtt{of}~\texttt{[] =>}~a ~\texttt{|}~
+               x\texttt{\#}xs~\texttt{=>}~f~x~xs) ~= \\
+((e = \texttt{[]} \to P(a)) \land
+ (\forall x~ xs. e = x\texttt{\#}xs \to P(f~x~xs)))
+\end{array}
+\]
+which can be fed to \ttindex{addsplits} just like
+\texttt{expand_if} (see~\S\ref{subsec:HOL:case:splitting}).
 
 {\tt List} provides a basic library of list processing functions defined by
 primitive recursion (see~\S\ref{sec:HOL:primrec}).  The recursion equations
@@ -1484,6 +1536,7 @@
 
 
 \subsection{Basics}
+\label{subsec:datatype:basics}
 
 The general \HOL\ \texttt{datatype} definition is of the following form:
 \[