
diff -r f3ff2549cdc8 -r 23a118849801 doc-src/TutorialI/Advanced/simp.thy
--- a/doc-src/TutorialI/Advanced/simp.thy	Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/Advanced/simp.thy	Thu Aug 09 18:12:15 2001 +0200
@@ -5,10 +5,9 @@
 section{*Simplification*}
 
 text{*\label{sec:simplification-II}\index{simplification|(}
-This section discusses some additional nifty features not covered so far and
-gives a short introduction to the simplification process itself. The latter
-is helpful to understand why a particular rule does or does not apply in some
-situation.
+This section describes features not covered until now.  It also
+outlines the simplification process itself, which can be helpful
+when the simplifier does not do what you expect of it.
 *}
 
 subsection{*Advanced Features*}
@@ -16,9 +15,10 @@
 subsubsection{*Congruence Rules*}
 
 text{*\label{sec:simp-cong}
-It is hardwired into the simplifier that while simplifying the conclusion $Q$
-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
+While simplifying the conclusion $Q$
+of $P \Imp Q$, it is legal use the assumption $P$.
+For $\Imp$ this policy is hardwired, but 
+contextual information can also be made available for other
 operators. For example, @{prop"xs = [] --> xs@xs = xs"} simplifies to @{term
 True} because we may use @{prop"xs = []"} when simplifying @{prop"xs@xs =
 xs"}. The generation of contextual information during simplification is
@@ -33,11 +33,11 @@
 Here are some more examples.  The congruence rules for bounded
 quantifiers supply contextual information about the bound variable:
 @{thm[display,eta_contract=false,margin=60]ball_cong[no_vars]}
-The congruence rule for conditional expressions supplies contextual
+One congruence rule for conditional expressions supplies contextual
 information for simplifying the @{text then} and @{text else} cases:
 @{thm[display]if_cong[no_vars]}
-A congruence rule can also \emph{prevent} simplification of some arguments.
-Here is an alternative congruence rule for conditional expressions:
+An alternative congruence rule for conditional expressions
+actually \emph{prevents} simplification of some arguments:
 @{thm[display]if_weak_cong[no_vars]}
 Only the first argument is simplified; the others remain unchanged.
 This makes simplification much faster and is faithful to the evaluation
@@ -67,11 +67,8 @@
 subsubsection{*Permutative Rewrite Rules*}
 
 text{*
-\index{rewrite rule!permutative|bold}
-\index{rewriting!ordered|bold}
-\index{ordered rewriting|bold}
-\index{simplification!ordered|bold}
-An equation is a \bfindex{permutative rewrite rule} if the left-hand
+\index{rewrite rules!permutative|bold}%
+An equation is a \textbf{permutative rewrite rule} if the left-hand
 side and right-hand side are the same up to renaming of variables.  The most
 common permutative rule is commutativity: @{prop"x+y = y+x"}.  Other examples
 include @{prop"(x-y)-z = (x-z)-y"} in arithmetic and @{prop"insert x (insert
@@ -110,45 +107,48 @@
 such tricks.
 *}
 
-subsection{*How it Works*}
+subsection{*How the Simplifier Works*}
 
 text{*\label{sec:SimpHow}
-Roughly speaking, the simplifier proceeds bottom-up (subterms are simplified
-first) and a conditional equation is only applied if its condition could be
-proved (again by simplification). Below we explain some special features of the rewriting process.
+Roughly speaking, the simplifier proceeds bottom-up: subterms are simplified
+first.  A conditional equation is only applied if its condition can be
+proved, again by simplification.  Below we explain some special features of
+the rewriting process. 
 *}
 
 subsubsection{*Higher-Order Patterns*}
 
 text{*\index{simplification rule|(}
 So far we have pretended the simplifier can deal with arbitrary
-rewrite rules. This is not quite true.  Due to efficiency (and
-potentially also computability) reasons, the simplifier expects the
+rewrite rules. This is not quite true.  For reasons of feasibility,
+the simplifier expects the
 left-hand side of each rule to be a so-called \emph{higher-order
-pattern}~\cite{nipkow-patterns}\indexbold{higher-order
-pattern}\indexbold{pattern, higher-order}. This restricts where
+pattern}~\cite{nipkow-patterns}\indexbold{patterns!higher-order}. 
+This restricts where
 unknowns may occur.  Higher-order patterns are terms in $\beta$-normal
-form (this will always be the case unless you have done something
-strange) where each occurrence of an unknown is of the form
+form.  (This means there are no subterms of the form $(\lambda x. M)(N)$.)  
+Each occurrence of an unknown is of the form
 $\Var{f}~x@1~\dots~x@n$, where the $x@i$ are distinct bound
 variables. Thus all ordinary rewrite rules, where all unknowns are
-of base type, for example @{thm add_assoc}, are OK: if an unknown is
+of base type, for example @{thm add_assoc}, are acceptable: if an unknown is
 of base type, it cannot have any arguments. Additionally, the rule
-@{text"(\<forall>x. ?P x \<and> ?Q x) = ((\<forall>x. ?P x) \<and> (\<forall>x. ?Q x))"} is also OK, in
+@{text"(\<forall>x. ?P x \<and> ?Q x) = ((\<forall>x. ?P x) \<and> (\<forall>x. ?Q x))"} is also acceptable, in
 both directions: all arguments of the unknowns @{text"?P"} and
 @{text"?Q"} are distinct bound variables.
 
-If the left-hand side is not a higher-order pattern, not all is lost
-and the simplifier will still try to apply the rule, but only if it
-matches \emph{directly}, i.e.\ without much $\lambda$-calculus hocus
-pocus. For example, @{text"?f ?x \<in> range ?f = True"} rewrites
+If the left-hand side is not a higher-order pattern, all is not lost.
+The simplifier will still try to apply the rule provided it
+matches directly: without much $\lambda$-calculus hocus
+pocus.  For example, @{text"(?f ?x \<in> range ?f) = True"} rewrites
 @{term"g a \<in> range g"} to @{term True}, but will fail to match
 @{text"g(h b) \<in> range(\<lambda>x. g(h x))"}.  However, you can
-replace the offending subterms (in our case @{text"?f ?x"}, which
-is not a pattern) by adding new variables and conditions: @{text"?y =
-?f ?x \<Longrightarrow> ?y \<in> range ?f = True"} is fine
+eliminate the offending subterms --- those that are not patterns ---
+by adding new variables and conditions.
+In our example, we eliminate @{text"?f ?x"} and obtain
+ @{text"?y =
+?f ?x \<Longrightarrow> (?y \<in> range ?f) = True"}, which is fine
 as a conditional rewrite rule since conditions can be arbitrary
-terms. However, this trick is not a panacea because the newly
+terms.  However, this trick is not a panacea because the newly
 introduced conditions may be hard to solve.
   
 There is no restriction on the form of the right-hand




