doc-src/Ref/simplifier.tex

   There is basically no restriction on the form of the right-hand
   sides.  They may not contain extraneous term or type variables,
   though.
 \end{warn}
 \index{rewrite rules|)}
-
-
-\subsection{*Congruence rules}\index{congruence rules}\label{sec:simp-congs}
-\begin{ttbox}
-addcongs   : simpset * thm list -> simpset \hfill{\bf infix 4}
-delcongs   : simpset * thm list -> simpset \hfill{\bf infix 4}
-addeqcongs : simpset * thm list -> simpset \hfill{\bf infix 4}
-deleqcongs : simpset * thm list -> simpset \hfill{\bf infix 4}
-\end{ttbox}
-
-Congruence rules are meta-equalities of the form
-\[ \dots \Imp
-   f(\Var{x@1},\ldots,\Var{x@n}) \equiv f(\Var{y@1},\ldots,\Var{y@n}).
-\]
-This governs the simplification of the arguments of~$f$.  For
-example, some arguments can be simplified under additional assumptions:
-\[ \List{\Var{P@1} \bimp \Var{Q@1};\; \Var{Q@1} \Imp \Var{P@2} \bimp \Var{Q@2}}
-   \Imp (\Var{P@1} \imp \Var{P@2}) \equiv (\Var{Q@1} \imp \Var{Q@2})
-\]
-Given this rule, the simplifier assumes $Q@1$ and extracts rewrite
-rules from it when simplifying~$P@2$.  Such local assumptions are
-effective for rewriting formulae such as $x=0\imp y+x=y$.  The local
-assumptions are also provided as theorems to the solver; see
-{\S}~\ref{sec:simp-solver} below.
-
-\begin{ttdescription}
-  
-\item[$ss$ \ttindexbold{addcongs} $thms$] adds congruence rules to the
-  simpset $ss$.  These are derived from $thms$ in an appropriate way,
-  depending on the underlying object-logic.
-  
-\item[$ss$ \ttindexbold{delcongs} $thms$] deletes congruence rules
-  derived from $thms$.
-  
-\item[$ss$ \ttindexbold{addeqcongs} $thms$] adds congruence rules in
-  their internal form (conclusions using meta-equality) to simpset
-  $ss$.  This is the basic mechanism that \texttt{addcongs} is built
-  on.  It should be rarely used directly.
-  
-\item[$ss$ \ttindexbold{deleqcongs} $thms$] deletes congruence rules
-  in internal form from simpset $ss$.
-  
-\end{ttdescription}
-
-\medskip
-
-Here are some more examples.  The congruence rule for bounded
-quantifiers also supplies contextual information, this time about the
-bound variable:
-\begin{eqnarray*}
-  &&\List{\Var{A}=\Var{B};\; 
-          \Forall x. x\in \Var{B} \Imp \Var{P}(x) = \Var{Q}(x)} \Imp{} \\
- &&\qquad\qquad
-    (\forall x\in \Var{A}.\Var{P}(x)) = (\forall x\in \Var{B}.\Var{Q}(x))
-\end{eqnarray*}
-The congruence rule for conditional expressions can supply contextual
-information for simplifying the arms:
-\[ \List{\Var{p}=\Var{q};~ \Var{q} \Imp \Var{a}=\Var{c};~
-         \neg\Var{q} \Imp \Var{b}=\Var{d}} \Imp
-   if(\Var{p},\Var{a},\Var{b}) \equiv if(\Var{q},\Var{c},\Var{d})
-\]
-A congruence rule can also {\em prevent\/} simplification of some arguments.
-Here is an alternative congruence rule for conditional expressions:
-\[ \Var{p}=\Var{q} \Imp
-   if(\Var{p},\Var{a},\Var{b}) \equiv if(\Var{q},\Var{a},\Var{b})
-\]
-Only the first argument is simplified; the others remain unchanged.
-This can make simplification much faster, but may require an extra case split
-to prove the goal.  
 
 
 \subsection{*The subgoaler}\label{sec:simp-subgoaler}
 \begin{ttbox}
 setsubgoaler :