author lcp Wed, 09 Nov 1994 15:47:11 +0100 changeset 698 23734672dc12 parent 697 40f72ab196f8 child 699 2da262e85c4d
updated discussion of congruence rules in first section
--- a/doc-src/Ref/simplifier.tex	Wed Nov 09 13:50:59 1994 +0100
+++ b/doc-src/Ref/simplifier.tex	Wed Nov 09 15:47:11 1994 +0100
@@ -69,8 +69,11 @@
\]
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 congruence rule for bounded
-quantifiers can also supply contextual information:
+rewriting formulae such as $x=0\imp y+x=y$.  The local assumptions are also
+provided as theorems to the solver; see page~\pageref{sec:simp-solver} below.
+
+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{} \\
@@ -83,8 +86,7 @@
\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 suppress simplification of certain arguments.
+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})
@@ -121,7 +123,7 @@
simplification only if that fails; here {\tt prems_of_ss} extracts the
current premises from a simpset.

-\subsection{*The solver}
+\subsection{*The solver}\label{sec:simp-solver}
The solver is a tactic that attempts to solve a subgoal after
simplification.  Typically it just proves trivial subgoals such as {\tt
True} and $t=t$.  It could use sophisticated means such as {\tt
@@ -157,8 +159,8 @@
\begin{warn}
If the simplifier aborts with the message {\tt Failed congruence proof!},
then the subgoaler or solver has failed to prove a premise of a
-  congruence rule.  This should never occur and indicates that the
-  subgoaler or solver is faulty.
+  congruence rule.  This should never occur; it indicates that some
+  congruence rule, or possibly the subgoaler or solver, is faulty.
\end{warn}