*** empty log message ***
Wed, 29 Mar 2000 15:09:51 +0200
changeset 8604 c99e0024050c
parent 8603 805910de7be0
child 8605 625fbbe5c6b4
*** empty log message ***
--- a/doc-src/HOL/HOL.tex	Wed Mar 29 14:23:27 2000 +0200
+++ b/doc-src/HOL/HOL.tex	Wed Mar 29 15:09:51 2000 +0200
@@ -936,6 +936,14 @@
   including \ttindex{conj_cong} in a simpset, \verb$addcongs [conj_cong]$.
+\begin{warn}\index{simplification!of \texttt{if}}\label{if-simp}%
+  By default only the condition of an \ttindex{if} is simplified but not the
+  \texttt{then} and \texttt{else} parts. Of course the latter are simplified
+  once the condition simplifies to \texttt{True} or \texttt{False}. To ensure
+  full simplification of all parts of a conditional you must remove
+  \ttindex{if_weak_cong} from the simpset, \verb$delcongs [if_weak_cong]$.
 If the simplifier cannot use a certain rewrite rule --- either because
 of nontermination or because its left-hand side is too flexible ---
 then you might try \texttt{stac}:
@@ -2135,6 +2143,16 @@
 This theorem can be added to a simpset via \ttindex{addsplits}
+\begin{warn}\index{simplification!of \texttt{case}}%
+  By default only the selector expression ($e$ above) in a
+  \texttt{case}-construct is simplified, in analogy with \texttt{if} (see
+  page~\pageref{if-simp}). Only if that reduces to a constructor is one of
+  the arms of the \texttt{case}-construct exposed and simplified. To ensure
+  full simplification of all parts of a \texttt{case}-construct for datatype
+  $t$, remove $t$\texttt{.}\ttindexbold{case_weak_cong} from the simpset, for
+  example by \texttt{delcongs [thm "$t$.weak_case_cong"]}.
 \subsubsection{The function \cdx{size}}\label{sec:HOL:size}
 Theory \texttt{Arith} declares a generic function \texttt{size} of type