--- 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|)}
--- /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: