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

use proper context operations (for fresh names of type and term variables, and for hypothetical definitions), monomorphize theorems (instead of terms, necessary for hypothetical definitions made during lambda lifting)

%
\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\ {\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
\isaindent{\ \ \ \ \ }{\isasymLongrightarrow}\ {\isacharparenleft}{\isasymforall}x{\isasymin}A{\isachardot}\ P\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymforall}x{\isasymin}B{\isachardot}\ Q\ x{\isacharparenright}%
\end{isabelle}
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}
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
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{{\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}
\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\ {\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 with respect to a 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 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{{\isacharquery}a\ {\isacharplus}\ {\isacharquery}b\ {\isacharplus}\ {\isacharquery}c\ {\isacharequal}\ {\isacharquery}a\ {\isacharplus}\ {\isacharparenleft}{\isacharquery}b\ {\isacharplus}\ {\isacharquery}c{\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 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, 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
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
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\ {\isacharequal}\ g\ x\ {\isasymand}\ h\ x\ {\isacharequal}\ k\ x} becomes the two separate
simplification 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 = \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{{\isacharparenleft}p\ {\isasymlongrightarrow}\ t\ {\isacharequal}\ u\ {\isasymand}\ {\isasymnot}\ r{\isacharparenright}\ {\isasymand}\ s}\end{center}
is converted into the three rules
\begin{center}
\isa{p\ {\isasymLongrightarrow}\ t\ {\isacharequal}\ u},\quad  \isa{p\ {\isasymLongrightarrow}\ r\ {\isacharequal}\ False},\quad  \isa{s\ {\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: