%

 \begin{isabellebody}%

 \def\isabellecontext{simp}%

 %

 \isadelimtheory

 %

 \endisadelimtheory

 %

 \isatagtheory

 %

 \endisatagtheory

 {\isafoldtheory}%

 %

 \isadelimtheory

 %

 \endisadelimtheory

 %

 \isamarkupsection{Simplification%

 }

 \isamarkuptrue%

 %

 \begin{isamarkuptext}%

 \label{sec:simplification-II}\index{simplification|(}

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

 \isamarkuptrue%

 %

 \isamarkupsubsection{Advanced Features%

 }

 \isamarkuptrue%

 %

 \isamarkupsubsubsection{Congruence Rules%

 }

 \isamarkuptrue%

 %

 \begin{isamarkuptext}%

 \label{sec:simp-cong}

 While simplifying the conclusion $Q$

 of $P \Imp Q$, it is legal to 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\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ xs\ {\isaliteral{40}{\isacharat}}\ xs\ {\isaliteral{3D}{\isacharequal}}\ xs} simplifies to \isa{True} because we may use \isa{xs\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}} when simplifying \isa{xs\ {\isaliteral{40}{\isacharat}}\ xs\ {\isaliteral{3D}{\isacharequal}}\ xs}. The generation of contextual information during simplification is

 controlled by so-called \bfindex{congruence rules}. This is the one for

 \isa{{\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}}:

 \begin{isabelle}%

 \ \ \ \ \ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}P\ {\isaliteral{3D}{\isacharequal}}\ P{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\ P{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Q\ {\isaliteral{3D}{\isacharequal}}\ Q{\isaliteral{27}{\isacharprime}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}P\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ Q{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}P{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ Q{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}%

 \end{isabelle}

 It should be read as follows:

 In order to simplify \isa{P\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ Q} to \isa{P{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ Q{\isaliteral{27}{\isacharprime}}},

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

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

 Here are some more examples.  The congruence rules for bounded

 quantifiers supply contextual information about the bound variable:

 \begin{isabelle}%

 \ \ \ \ \ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}A\ {\isaliteral{3D}{\isacharequal}}\ B{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ x\ {\isaliteral{3D}{\isacharequal}}\ Q\ x{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline

 \isaindent{\ \ \ \ \ }{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{5C3C696E3E}{\isasymin}}A{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{5C3C696E3E}{\isasymin}}B{\isaliteral{2E}{\isachardot}}\ Q\ x{\isaliteral{29}{\isacharparenright}}%

 \end{isabelle}

 One congruence rule for conditional expressions supplies contextual

 information for simplifying the \isa{then} and \isa{else} cases:

 \begin{isabelle}%

 \ \ \ \ \ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}b\ {\isaliteral{3D}{\isacharequal}}\ c{\isaliteral{3B}{\isacharsemicolon}}\ c\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ x\ {\isaliteral{3D}{\isacharequal}}\ u{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ c\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ y\ {\isaliteral{3D}{\isacharequal}}\ v{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline

 \isaindent{\ \ \ \ \ }{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}if\ b\ then\ x\ else\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ c\ then\ u\ else\ v{\isaliteral{29}{\isacharparenright}}%

 \end{isabelle}

 An alternative congruence rule for conditional expressions

 actually \emph{prevents} simplification of some arguments:

 \begin{isabelle}%

 \ \ \ \ \ b\ {\isaliteral{3D}{\isacharequal}}\ c\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}if\ b\ then\ x\ else\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ c\ then\ x\ else\ y{\isaliteral{29}{\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 evaluation of

 \isa{case} expressions.

 You can declare your own congruence rules with the attribute \attrdx{cong},

 either globally, in the usual manner,

 \begin{quote}

 \isacommand{declare} \textit{theorem-name} \isa{{\isaliteral{5B}{\isacharbrackleft}}cong{\isaliteral{5D}{\isacharbrackright}}}

 \end{quote}

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

 \begin{quote}

 \isa{cong{\isaliteral{3A}{\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{\isaliteral{5F}{\isacharunderscore}}cong}

 \begin{isabelle}%

 \ \ \ \ \ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}P\ {\isaliteral{3D}{\isacharequal}}\ P{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\ P{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Q\ {\isaliteral{3D}{\isacharequal}}\ Q{\isaliteral{27}{\isacharprime}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}P\ {\isaliteral{5C3C616E643E}{\isasymand}}\ Q{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}P{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ Q{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}%

 \end{isabelle}

 \par\noindent

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

 \end{warn}%

 \end{isamarkuptext}%

 \isamarkuptrue%

 %

 \isamarkupsubsubsection{Permutative Rewrite Rules%

 }

 \isamarkuptrue%

 %

 \begin{isamarkuptext}%

 \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\ {\isaliteral{2B}{\isacharplus}}\ y\ {\isaliteral{3D}{\isacharequal}}\ y\ {\isaliteral{2B}{\isacharplus}}\ x}.  Other examples

 include \isa{x\ {\isaliteral{2D}{\isacharminus}}\ y\ {\isaliteral{2D}{\isacharminus}}\ z\ {\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{2D}{\isacharminus}}\ z\ {\isaliteral{2D}{\isacharminus}}\ y} in arithmetic and \isa{insert\ x\ {\isaliteral{28}{\isacharparenleft}}insert\ y\ A{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ insert\ y\ {\isaliteral{28}{\isacharparenleft}}insert\ x\ A{\isaliteral{29}{\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 with respect to a fixed

 lexicographic ordering on terms. For example, commutativity rewrites

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

 smaller than \isa{b\ {\isaliteral{2B}{\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{{\isaliteral{2B}{\isacharplus}}} and \isa{{\isaliteral{2A}{\isacharasterisk}}} on numbers is rarely

 necessary because the built-in arithmetic prover often succeeds without

 such tricks.%

 \end{isamarkuptext}%

 \isamarkuptrue%

 %

 \isamarkupsubsection{How the Simplifier Works%

 }

 \isamarkuptrue%

 %

 \begin{isamarkuptext}%

 \label{sec:SimpHow}

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

 \isamarkuptrue%

 %

 \isamarkupsubsubsection{Higher-Order Patterns%

 }

 \isamarkuptrue%

 %

 \begin{isamarkuptext}%

 \index{simplification rule|(}

 So far we have pretended the simplifier can deal with arbitrary

 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{patterns!higher-order}. 

 This restricts where

 unknowns may occur.  Higher-order patterns are terms in $\beta$-normal

 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{{\isaliteral{3F}{\isacharquery}}a\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{3F}{\isacharquery}}b\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{3F}{\isacharquery}}c\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{3F}{\isacharquery}}a\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{3F}{\isacharquery}}b\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{3F}{\isacharquery}}c{\isaliteral{29}{\isacharparenright}}}, are acceptable: if an unknown is

 of base type, it cannot have any arguments. Additionally, the rule

 \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ {\isaliteral{3F}{\isacharquery}}P\ x\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{3F}{\isacharquery}}Q\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ {\isaliteral{3F}{\isacharquery}}P\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ {\isaliteral{3F}{\isacharquery}}Q\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}} is also acceptable, in

 both directions: all arguments of the unknowns \isa{{\isaliteral{3F}{\isacharquery}}P} and

 \isa{{\isaliteral{3F}{\isacharquery}}Q} are distinct bound variables.

 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{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{3F}{\isacharquery}}f\ {\isaliteral{3F}{\isacharquery}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ range\ {\isaliteral{3F}{\isacharquery}}f{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ True} rewrites

 \isa{g\ a\ {\isaliteral{5C3C696E3E}{\isasymin}}\ range\ g} to \isa{True}, but will fail to match

 \isa{g{\isaliteral{28}{\isacharparenleft}}h\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ range{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ g{\isaliteral{28}{\isacharparenleft}}h\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}}.  However, you can

 eliminate the offending subterms --- those that are not patterns ---

 by adding new variables and conditions.

 In our example, we eliminate \isa{{\isaliteral{3F}{\isacharquery}}f\ {\isaliteral{3F}{\isacharquery}}x} and obtain

  \isa{{\isaliteral{3F}{\isacharquery}}y\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{3F}{\isacharquery}}f\ {\isaliteral{3F}{\isacharquery}}x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{3F}{\isacharquery}}y\ {\isaliteral{5C3C696E3E}{\isasymin}}\ range\ {\isaliteral{3F}{\isacharquery}}f{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\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

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

 \isamarkuptrue%

 %

 \isamarkupsubsubsection{The Preprocessor%

 }

 \isamarkuptrue%

 %

 \begin{isamarkuptext}%

 \label{sec:simp-preprocessor}

 When a 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, \isa{f\ x\ {\isaliteral{3D}{\isacharequal}}\ g\ x\ {\isaliteral{5C3C616E643E}{\isasymand}}\ h\ x\ {\isaliteral{3D}{\isacharequal}}\ k\ x} becomes the two separate

 simplification rules \isa{f\ x\ {\isaliteral{3D}{\isacharequal}}\ g\ x} and \isa{h\ x\ {\isaliteral{3D}{\isacharequal}}\ k\ x}. In

 general, the input theorem is converted as follows:

 \begin{eqnarray}

 \neg P &\mapsto& P = \hbox{\isa{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 =\isa{True}$.

 For example, the formula 

 \begin{center}\isa{{\isaliteral{28}{\isacharparenleft}}p\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ t\ {\isaliteral{3D}{\isacharequal}}\ u\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ r{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ s}\end{center}

 is converted into the three rules

 \begin{center}

 \isa{p\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ t\ {\isaliteral{3D}{\isacharequal}}\ u},\quad  \isa{p\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ r\ {\isaliteral{3D}{\isacharequal}}\ False},\quad  \isa{s\ {\isaliteral{3D}{\isacharequal}}\ True}.

 \end{center}

 \index{simplification rule|)}

 \index{simplification|)}%

 \end{isamarkuptext}%

 \isamarkuptrue%

 %

 \isadelimtheory

 %

 \endisadelimtheory

 %

 \isatagtheory

 %

 \endisatagtheory

 {\isafoldtheory}%

 %

 \isadelimtheory

 %

 \endisadelimtheory

 \end{isabellebody}%

 %%% Local Variables:

 %%% mode: latex

 %%% TeX-master: "root"

 %%% End: