--- a/doc-src/TutorialI/Advanced/document/simp.tex Mon Mar 05 15:47:11 2001 +0100
+++ b/doc-src/TutorialI/Advanced/document/simp.tex Wed Mar 07 15:54:11 2001 +0100
@@ -22,7 +22,7 @@
\begin{isamarkuptext}%
\label{sec:simp-cong}
It is hardwired into the simplifier that while simplifying the conclusion $Q$
-of $P \isasymImp Q$ it is legal to make uses of the assumptions $P$. This
+of $P \Imp Q$ it is legal to make uses of the assumption $P$. This
kind of contextual information can also be made available for other
operators. For example, \isa{xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ xs\ {\isacharat}\ xs\ {\isacharequal}\ xs} simplifies to \isa{True} because we may use \isa{xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}} when simplifying \isa{xs\ {\isacharat}\ xs\ {\isacharequal}\ xs}. The generation of contextual information during simplification is
controlled by so-called \bfindex{congruence rules}. This is the one for
@@ -41,8 +41,8 @@
\ \ \ \ \ {\isasymlbrakk}A\ {\isacharequal}\ B{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ B\ {\isasymLongrightarrow}\ P\ x\ {\isacharequal}\ Q\ x{\isasymrbrakk}\isanewline
\isaindent{\ \ \ \ \ }{\isasymLongrightarrow}\ {\isacharparenleft}{\isasymforall}x{\isasymin}A{\isachardot}\ P\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymforall}x{\isasymin}B{\isachardot}\ Q\ x{\isacharparenright}%
\end{isabelle}
-The congruence rule for conditional expressions supply contextual
-information for simplifying the arms:
+The congruence rule for conditional expressions supplies contextual
+information for simplifying the \isa{then} and \isa{else} cases:
\begin{isabelle}%
\ \ \ \ \ {\isasymlbrakk}b\ {\isacharequal}\ c{\isacharsemicolon}\ c\ {\isasymLongrightarrow}\ x\ {\isacharequal}\ u{\isacharsemicolon}\ {\isasymnot}\ c\ {\isasymLongrightarrow}\ y\ {\isacharequal}\ v{\isasymrbrakk}\isanewline
\isaindent{\ \ \ \ \ }{\isasymLongrightarrow}\ {\isacharparenleft}if\ b\ then\ x\ else\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ c\ then\ u\ else\ v{\isacharparenright}%
@@ -55,7 +55,7 @@
Only the first argument is simplified; the others remain unchanged.
This makes simplification much faster and is faithful to the evaluation
strategy in programming languages, which is why this is the default
-congruence rule for \isa{if}. Analogous rules control the evaluaton of
+congruence rule for \isa{if}. Analogous rules control the evaluation of
\isa{case} expressions.
You can declare your own congruence rules with the attribute \isa{cong},
@@ -122,7 +122,7 @@
Note that ordered rewriting for \isa{{\isacharplus}} and \isa{{\isacharasterisk}} on numbers is rarely
necessary because the built-in arithmetic prover often succeeds without
-such hints.%
+such tricks.%
\end{isamarkuptext}%
%
\isamarkupsubsection{How It Works%
@@ -167,8 +167,7 @@
is not a pattern) by adding new variables and conditions: \isa{{\isacharquery}y\ {\isacharequal}\ {\isacharquery}f\ {\isacharquery}x\ {\isasymLongrightarrow}\ {\isacharquery}y\ {\isasymin}\ range\ {\isacharquery}f\ {\isacharequal}\ True} is fine
as a conditional rewrite rule since conditions can be arbitrary
terms. However, this trick is not a panacea because the newly
-introduced conditions may be hard to prove, as they must be
-before the rule can actually be applied.
+introduced conditions may be hard to solve.
There is no restriction on the form of the right-hand
sides. They may not contain extraneous term or type variables, though.%