# HG changeset patch # User nipkow # Date 969041235 -7200 # Node ID c0f7fb6e538e3f44aa483cf2399e46712cb456fe # Parent 4281ccea43f007c9b93e3882be4fcb4c0140c7c7 *** empty log message *** diff -r 4281ccea43f0 -r c0f7fb6e538e doc-src/TutorialI/Advanced/advanced.tex --- a/doc-src/TutorialI/Advanced/advanced.tex Fri Sep 15 19:59:05 2000 +0200 +++ b/doc-src/TutorialI/Advanced/advanced.tex Fri Sep 15 20:07:15 2000 +0200 @@ -9,18 +9,18 @@ \emph{congruence rules}, introduced in the section on simplification, is required for parts of the section on recursion. -\input{document/simp.tex} +\input{Advanced/document/simp.tex} \section{Advanced forms of recursion} \label{sec:advanced-recdef} \index{*recdef|(} -\input{../Recdef/document/Nested0.tex} -\input{../Recdef/document/Nested1.tex} -\input{../Recdef/document/Nested2.tex} +\input{Recdef/document/Nested0.tex} +\input{Recdef/document/Nested1.tex} +\input{Recdef/document/Nested2.tex} \index{*recdef|)} \section{Advanced induction techniques} \label{sec:advanced-ind} \index{induction|(} -\input{../Misc/document/AdvancedInd.tex} +\input{Misc/document/AdvancedInd.tex} \index{induction|)} diff -r 4281ccea43f0 -r c0f7fb6e538e doc-src/TutorialI/Advanced/document/simp.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/TutorialI/Advanced/document/simp.tex Fri Sep 15 20:07:15 2000 +0200 @@ -0,0 +1,145 @@ +% +\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 operators. (Associativity by itself is not +permutative.) When dealing with an AC-operator~$f$, keep the +following points in mind: +\begin{itemize}\index{associative-commutative operators} + +\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% +\end{isamarkuptext}% +% +\isamarkupsubsubsection{Higher-order patterns} +% +\isamarkupsubsubsection{Local assumptions} +% +\isamarkupsubsubsection{The preprocessor} +% +\begin{isamarkuptext}% +\index{simplification|)}% +\end{isamarkuptext}% +\end{isabellebody}% +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "root" +%%% End: