%

 \begin{isabellebody}%

 \def\isabellecontext{simp}%

 %

 \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.%

 \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 \isasymImp Q$ it is legal to make uses of the assumptions $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

 \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}%

 \end{isabelle}

 It should be read as follows:

 In order to simplify \isa{P\ {\isasymlongrightarrow}\ Q} to \isa{P{\isacharprime}\ {\isasymlongrightarrow}\ Q{\isacharprime}},

 simplify \isa{P} to \isa{P{\isacharprime}}

 and assume \isa{P{\isacharprime}} when simplifying \isa{Q} to \isa{Q{\isacharprime}}.

 Here are some more examples.  The congruence rules for bounded

 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

 \ \ \ \ \ {\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:

 \begin{isabelle}%

 \ \ \ \ \ {\isasymlbrakk}b\ {\isacharequal}\ c{\isacharsemicolon}\ c\ {\isasymLongrightarrow}\ x\ {\isacharequal}\ u{\isacharsemicolon}\ {\isasymnot}\ c\ {\isasymLongrightarrow}\ y\ {\isacharequal}\ v{\isasymrbrakk}\isanewline

 \ \ \ \ \ {\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:

 \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

 strategy in programming languages, which is why this is the default

 congruence rule for \isa{if}. Analogous rules control the evaluaton of

 \isa{case} expressions.

 You can delare your own congruence rules with the attribute \isa{cong},

 either globally, in the usual manner,

 \begin{quote}

 \isacommand{declare} \textit{theorem-name} \isa{{\isacharbrackleft}cong{\isacharbrackright}}

 \end{quote}

 or locally in a \isa{simp} call by adding the modifier

 \begin{quote}

 \isa{cong{\isacharcolon}} \textit{list of theorem names}

 \end{quote}

 The effect is reversed by \isa{cong\ del} instead of \isa{cong}.

 \begin{warn}

 The congruence rule \isa{conj{\isacharunderscore}cong}

 \begin{isabelle}%

 \ \ \ \ \ {\isasymlbrakk}P\ {\isacharequal}\ P{\isacharprime}{\isacharsemicolon}\ P{\isacharprime}\ {\isasymLongrightarrow}\ Q\ {\isacharequal}\ Q{\isacharprime}{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}P\ {\isasymand}\ Q{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}P{\isacharprime}\ {\isasymand}\ Q{\isacharprime}{\isacharparenright}%

 \end{isabelle}

 is occasionally useful but not a default rule; you have to use it explicitly.

 \end{warn}%

 \end{isamarkuptext}%

 %

 \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

 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

 \bfindex{ordered rewriting}: a permutative rewrite

 rule is only applied if the term becomes ``smaller'' (w.r.t.\ some fixed

 lexicographic ordering on terms). For example, commutativity rewrites

 \isa{b\ {\isacharplus}\ a} to \isa{a\ {\isacharplus}\ b}, but then stops because \isa{a\ {\isacharplus}\ b} is strictly

 smaller than \isa{b\ {\isacharplus}\ a}.  Permutative rewrite rules can be turned into

 simplification rules in the usual manner via the \isa{simp} attribute; the

 simplifier recognizes their special status automatically.

 Permutative rewrite rules are most effective in the case of

 associative-commutative functions.  (Associativity by itself is not

 permutative.)  When dealing with an AC-function~$f$, keep the

 following points in mind:

 \begin{itemize}\index{associative-commutative function}

 \item The associative law must always be oriented from left to right,

   namely $f(f(x,y),z) = f(x,f(y,z))$.  The opposite orientation, if

   used with commutativity, can lead to nontermination.

 \item To complete your set of rewrite rules, you must add not just

   associativity~(A) and commutativity~(C) but also a derived rule, {\bf

     left-com\-mut\-ativ\-ity} (LC): $f(x,f(y,z)) = f(y,f(x,z))$.

 \end{itemize}

 Ordered rewriting with the combination of A, C, and LC sorts a term

 lexicographically:

 \[\def\maps#1{~\stackrel{#1}{\leadsto}~}

  f(f(b,c),a) \maps{A} f(b,f(c,a)) \maps{C} f(b,f(a,c)) \maps{LC} f(a,f(b,c)) \]

 Note that ordered rewriting for \isa{{\isacharplus}} and \isa{{\isacharasterisk}} on numbers is rarely

 necessary because the builtin arithmetic capabilities often take care of

 this.%

 \end{isamarkuptext}%

 %

 \isamarkupsubsection{How it 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.%

 \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

 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

 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

 $\Var{f}~x@1~\dots~x@n$, where the $x@i$ are distinct bound

 variables. Thus all ``standard'' 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, 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

 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 ``directly'', i.e.\ without much $\lambda$-calculus hocus

 pocus. For example, \isa{{\isacharquery}f\ {\isacharquery}x\ {\isasymin}\ range\ {\isacharquery}f\ {\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

 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, which has to take place

 before the rule can actually be applied.

 There is basically no restriction on the form of the right-hand

 sides.  They may not contain extraneous term or type variables, though.%

 \end{isamarkuptext}%

 %

 \isamarkupsubsubsection{The preprocessor}

 %

 \begin{isamarkuptext}%

 When some theorem is declared a simplification rule, it need not be a

 conditional equation already.  The simplifier will turn it into a set of

 conditional equations automatically.  For example, given \isa{f\ x\ {\isacharequal}\ g\ x\ {\isasymand}\ h\ x\ {\isacharequal}\ k\ x} the simplifier will turn this into the two separate

 simplifiction rules \isa{f\ x\ {\isacharequal}\ g\ x} and \isa{h\ x\ {\isacharequal}\ k\ x}. In

 general, the input theorem is converted as follows:

 \begin{eqnarray}

 \neg P &\mapsto& P = False \nonumber\\

 P \longrightarrow Q &\mapsto& P \Longrightarrow Q \nonumber\\

 P \land Q &\mapsto& P,\ Q \nonumber\\

 \forall x.~P~x &\mapsto& P~\Var{x}\nonumber\\

 \forall x \in A.\ P~x &\mapsto& \Var{x} \in A \Longrightarrow P~\Var{x} \nonumber\\

 \isa{if}\ P\ \isa{then}\ Q\ \isa{else}\ R &\mapsto&

  P \Longrightarrow Q,\ \neg P \Longrightarrow R \nonumber

 \end{eqnarray}

 Once this conversion process is finished, all remaining non-equations

 $P$ are turned into trivial equations $P = True$.

 For example, the formula \isa{{\isacharparenleft}p\ {\isasymlongrightarrow}\ q\ {\isasymand}\ r{\isacharparenright}\ {\isasymand}\ s} is converted into the three rules

 \begin{center}

 \isa{p\ {\isasymLongrightarrow}\ q\ {\isacharequal}\ True},\quad  \isa{p\ {\isasymLongrightarrow}\ r\ {\isacharequal}\ True},\quad  \isa{s\ {\isacharequal}\ True}.

 \end{center}

 \index{simplification rule|)}

 \index{simplification|)}%

 \end{isamarkuptext}%

 \end{isabellebody}%

 %%% Local Variables:

 %%% mode: latex

 %%% TeX-master: "root"

 %%% End: