Documented `addsplits'
Mon, 20 Oct 1997 17:21:54 +0200
changeset 3959 033633d9a032
parent 3958 78a8e9a1c2f9
child 3960 7a38fae985f9
Documented `addsplits'
--- 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 @@
 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
+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
 \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}
+\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})))
+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
+by(simp_tac (!simpset addsplits [expand_if]) 1);
+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}
 \subsection{Classical reasoning}
@@ -1345,6 +1385,7 @@
 \subsection{The type constructor for lists, \textit{list}}
 \index{list@{\textit{list}} type|(}
 Figure~\ref{hol-list} presents the theory \thydx{List}: the basic list
@@ -1356,7 +1397,18 @@
 case $e$ of [] => $a$  |  \(x\)\#\(xs\) => b
-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}
+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)))
+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 @@
 The general \HOL\ \texttt{datatype} definition is of the following form: