doc-src/TutorialI/Advanced/document/simp.tex

 \isamarkupsection{Simplification%
 }
 %
 \begin{isamarkuptext}%
 \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.%
 \end{isamarkuptext}%
 %
 \isamarkupsubsection{Advanced Features%
 }
 %
 \isamarkupsubsubsection{Congruence Rules%
 }
 %
 \begin{isamarkuptext}%
 \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, \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
 \isa{{\isasymlongrightarrow}}:
 \begin{isabelle}%
 \ \ \ \ \ {\isasymlbrakk}P\ {\isacharequal}\ P{\isacharprime}{\isacharsemicolon}\ P{\isacharprime}\ {\isasymLongrightarrow}\ Q\ {\isacharequal}\ Q{\isacharprime}{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}P\ {\isasymlongrightarrow}\ Q{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}P{\isacharprime}\ {\isasymlongrightarrow}\ Q{\isacharprime}{\isacharparenright}%

 quantifiers supply contextual information about the bound variable:
 \begin{isabelle}%
 \ \ \ \ \ {\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 supplies contextual
+One 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}%
 \end{isabelle}
-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:
 \begin{isabelle}%
 \ \ \ \ \ b\ {\isacharequal}\ c\ {\isasymLongrightarrow}\ {\isacharparenleft}if\ b\ then\ x\ else\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ c\ then\ x\ else\ y{\isacharparenright}%
 \end{isabelle}
 Only the first argument is simplified; the others remain unchanged.
 This makes simplification much faster and is faithful to the evaluation

 %
 \isamarkupsubsubsection{Permutative Rewrite Rules%
 }
 %
 \begin{isamarkuptext}%
-\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: \isa{x\ {\isacharplus}\ y\ {\isacharequal}\ y\ {\isacharplus}\ x}.  Other examples
 include \isa{x\ {\isacharminus}\ y\ {\isacharminus}\ z\ {\isacharequal}\ x\ {\isacharminus}\ z\ {\isacharminus}\ y} in arithmetic and \isa{insert\ x\ {\isacharparenleft}insert\ y\ A{\isacharparenright}\ {\isacharequal}\ insert\ y\ {\isacharparenleft}insert\ x\ A{\isacharparenright}} for sets. Such rules are problematic because
 once they apply, they can be used forever. The simplifier is aware of this
 danger and treats permutative rules by means of a special strategy, called

 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 tricks.%
 \end{isamarkuptext}%
 %
-\isamarkupsubsection{How it Works%
+\isamarkupsubsection{How the Simplifier Works%
 }
 %
 \begin{isamarkuptext}%
 \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.%
 \end{isamarkuptext}%
 %
 \isamarkupsubsubsection{Higher-Order Patterns%
 }
 %
 \begin{isamarkuptext}%
 \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 \isa{{\isacharquery}m\ {\isacharplus}\ {\isacharquery}n\ {\isacharplus}\ {\isacharquery}k\ {\isacharequal}\ {\isacharquery}m\ {\isacharplus}\ {\isacharparenleft}{\isacharquery}n\ {\isacharplus}\ {\isacharquery}k{\isacharparenright}}, are OK: if an unknown is
+of base type, for example \isa{{\isacharquery}m\ {\isacharplus}\ {\isacharquery}n\ {\isacharplus}\ {\isacharquery}k\ {\isacharequal}\ {\isacharquery}m\ {\isacharplus}\ {\isacharparenleft}{\isacharquery}n\ {\isacharplus}\ {\isacharquery}k{\isacharparenright}}, are acceptable: if an unknown is
 of base type, it cannot have any arguments. Additionally, the rule
-\isa{{\isacharparenleft}{\isasymforall}x{\isachardot}\ {\isacharquery}P\ x\ {\isasymand}\ {\isacharquery}Q\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isacharparenleft}{\isasymforall}x{\isachardot}\ {\isacharquery}P\ x{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}x{\isachardot}\ {\isacharquery}Q\ x{\isacharparenright}{\isacharparenright}} is also OK, in
+\isa{{\isacharparenleft}{\isasymforall}x{\isachardot}\ {\isacharquery}P\ x\ {\isasymand}\ {\isacharquery}Q\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isacharparenleft}{\isasymforall}x{\isachardot}\ {\isacharquery}P\ x{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}x{\isachardot}\ {\isacharquery}Q\ x{\isacharparenright}{\isacharparenright}} is also acceptable, in
 both directions: all arguments of the unknowns \isa{{\isacharquery}P} and
 \isa{{\isacharquery}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, \isa{{\isacharquery}f\ {\isacharquery}x\ {\isasymin}\ range\ {\isacharquery}f\ {\isacharequal}\ 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, \isa{{\isacharparenleft}{\isacharquery}f\ {\isacharquery}x\ {\isasymin}\ range\ {\isacharquery}f{\isacharparenright}\ {\isacharequal}\ True} rewrites
 \isa{g\ a\ {\isasymin}\ range\ g} to \isa{True}, but will fail to match
 \isa{g{\isacharparenleft}h\ b{\isacharparenright}\ {\isasymin}\ range{\isacharparenleft}{\isasymlambda}x{\isachardot}\ g{\isacharparenleft}h\ x{\isacharparenright}{\isacharparenright}}.  However, you can
-replace the offending subterms (in our case \isa{{\isacharquery}f\ {\isacharquery}x}, which
-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
+eliminate the offending subterms --- those that are not patterns ---
+by adding new variables and conditions.
+In our example, we eliminate \isa{{\isacharquery}f\ {\isacharquery}x} and obtain
+ \isa{{\isacharquery}y\ {\isacharequal}\ {\isacharquery}f\ {\isacharquery}x\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isacharquery}y\ {\isasymin}\ range\ {\isacharquery}f{\isacharparenright}\ {\isacharequal}\ 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
 sides.  They may not contain extraneous term or type variables, though.%
 \end{isamarkuptext}%