--- a/doc-src/Logics/HOL.tex Mon Apr 27 16:47:50 1998 +0200
+++ b/doc-src/Logics/HOL.tex Mon Apr 27 17:52:03 1998 +0200
@@ -414,7 +414,7 @@
%\tdx{if_False} (if False then x else y) = y
\tdx{if_P} P ==> (if P then x else y) = x
\tdx{if_not_P} ~ P ==> (if P then x else y) = y
-\tdx{expand_if} P(if Q then x else y) = ((Q --> P x) & (~Q --> P y))
+\tdx{split_if} P(if Q then x else y) = ((Q --> P x) & (~Q --> P y))
\subcaption{Conditionals}
\end{ttbox}
\caption{More derived rules} \label{hol-lemmas2}
@@ -756,8 +756,8 @@
They also include straightforward constructions on functions: image~({\tt``})
and \texttt{range}.
-%The predicate \cdx{inj_onto} is used for simulating type definitions.
-%The statement ${\tt inj_onto}~f~A$ asserts that $f$ is injective on the
+%The predicate \cdx{inj_on} is used for simulating type definitions.
+%The statement ${\tt inj_on}~f~A$ asserts that $f$ is injective on the
%set~$A$, which specifies a subset of its domain type. In a type
%definition, $f$ is the abstraction function and $A$ is the set of valid
%representations; we should not expect $f$ to be injective outside of~$A$.
@@ -778,13 +778,13 @@
%\tdx{inj_inverseI} (!!x. g(f x) = x) ==> inj f
%\tdx{injD} [| inj f; f x = f y |] ==> x=y
%
-%\tdx{inj_ontoI} (!!x y. [| f x=f y; x:A; y:A |] ==> x=y) ==> inj_onto f A
-%\tdx{inj_ontoD} [| inj_onto f A; f x=f y; x:A; y:A |] ==> x=y
+%\tdx{inj_onI} (!!x y. [| f x=f y; x:A; y:A |] ==> x=y) ==> inj_on f A
+%\tdx{inj_onD} [| inj_on f A; f x=f y; x:A; y:A |] ==> x=y
%
-%\tdx{inj_onto_inverseI}
-% (!!x. x:A ==> g(f x) = x) ==> inj_onto f A
-%\tdx{inj_onto_contraD}
-% [| inj_onto f A; x~=y; x:A; y:A |] ==> ~ f x=f y
+%\tdx{inj_on_inverseI}
+% (!!x. x:A ==> g(f x) = x) ==> inj_on f A
+%\tdx{inj_on_contraD}
+% [| inj_on f A; x~=y; x:A; y:A |] ==> ~ f x=f y
%\end{ttbox}
%\caption{Derived rules involving functions} \label{hol-fun}
%\end{figure}
@@ -871,7 +871,7 @@
\it name &\it meta-type & \it description \\
\cdx{inj}~~\cdx{surj}& $(\alpha\To\beta )\To bool$
& injective/surjective \\
- \cdx{inj_onto} & $[\alpha\To\beta ,\alpha\,set]\To bool$
+ \cdx{inj_on} & $[\alpha\To\beta ,\alpha\,set]\To bool$
& injective over subset\\
\cdx{inv} & $(\alpha\To\beta)\To(\beta\To\alpha)$ & inverse function
\end{tabular}
@@ -879,10 +879,10 @@
\underscoreon
\begin{ttbox}
-\tdx{inj_def} inj f == ! x y. f x=f y --> x=y
-\tdx{surj_def} surj f == ! y. ? x. y=f x
-\tdx{inj_onto_def} inj_onto f A == !x:A. !y:A. f x=f y --> x=y
-\tdx{inv_def} inv f == (\%y. @x. f(x)=y)
+\tdx{inj_def} inj f == ! x y. f x=f y --> x=y
+\tdx{surj_def} surj f == ! y. ? x. y=f x
+\tdx{inj_on_def} inj_on f A == !x:A. !y:A. f x=f y --> x=y
+\tdx{inv_def} inv f == (\%y. @x. f(x)=y)
\end{ttbox}
\caption{Theory \thydx{Fun}} \label{fig:HOL:Fun}
\end{figure}
@@ -946,9 +946,9 @@
\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
+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}:
+expressed by the theorem \tdx{split_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})))
@@ -963,16 +963,24 @@
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
+\ttindexbold{addsplits} of type \texttt{simpset * thm list -> simpset}
+(analogous to \texttt{addsimps}) that adds rules such as $(*)$ to a
simpset, as in
\begin{ttbox}
-by(simp_tac (!simpset addsplits [expand_if]) 1);
+by(simp_tac (!simpset addsplits [split_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} is split acording to \texttt{split_if}, until all occurences of
\texttt{if} have been eliminated.
+It turns out that using \texttt{split_if} is almost always the right thing to
+do. Hence \texttt{split_if} is already included in the default simpset. If
+you want to delete it from a simpset, use \ttindexbold{delsplits}, which is
+the inverse of \texttt{addsplits}:
+\begin{ttbox}
+by(simp_tac (!simpset delsplits [split_if]) 1);
+\end{ttbox}
+
In general, \texttt{addsplits} accepts rules of the form
\[
\Var{P}(c~\Var{x@1}~\dots~\Var{x@n})~=~ rhs
@@ -983,6 +991,14 @@
are splitting rules for \texttt{case} expressions (see~\S\ref{subsec:list}
and~\S\ref{subsec:datatype:basics}).
+Analogous to \texttt{Addsimps} and \texttt{Delsimps}, there are also
+imperative versions of \texttt{addsplits} and \texttt{delsplits}
+\begin{ttbox}
+\ttindexbold{Addsplits}: thm list -> unit
+\ttindexbold{Delsplits}: thm list -> unit
+\end{ttbox}
+for adding splitting rules to, and deleting them from the current simpset.
+
\subsection{Classical reasoning}
\HOL\ derives classical introduction rules for $\disj$ and~$\exists$, as
@@ -1037,7 +1053,7 @@
\tdx{surjective_pairing} p = (fst p,snd p)
\tdx{split} split c (a,b) = c a b
-\tdx{expand_split} R(split c p) = (! x y. p = (x,y) --> R(c x y))
+\tdx{split_split} R(split c p) = (! x y. p = (x,y) --> R(c x y))
\tdx{SigmaI} [| a:A; b:B a |] ==> (a,b) : Sigma A B
\tdx{SigmaE} [| c:Sigma A B; !!x y.[| x:A; y:B x; c=(x,y) |] ==> P |] ==> P
@@ -1136,7 +1152,7 @@
\tdx{sum_case_Inr} sum_case f g (Inr x) = g x
\tdx{surjective_sum} sum_case (\%x. f(Inl x)) (\%y. f(Inr y)) s = f s
-\tdx{expand_sum_case} R(sum_case f g s) = ((! x. s = Inl(x) --> R(f(x))) &
+\tdx{split_sum_case} R(sum_case f g s) = ((! x. s = Inl(x) --> R(f(x))) &
(! y. s = Inr(y) --> R(g(y))))
\end{ttbox}
\caption{Type $\alpha+\beta$}\label{hol-sum}
@@ -1409,7 +1425,7 @@
\end{array}
\]
which can be fed to \ttindex{addsplits} just like
-\texttt{expand_if} (see~\S\ref{subsec:HOL:case:splitting}).
+\texttt{split_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