1.1 --- a/doc-src/TutorialI/fp.tex Tue Sep 05 13:12:00 2000 +0200
1.2 +++ b/doc-src/TutorialI/fp.tex Tue Sep 05 13:53:39 2000 +0200
1.3 @@ -370,11 +370,7 @@
1.4 Section~\S\ref{sec:Simplification} explains how definitions are used
1.5 in proofs.
1.6
1.7 -\begin{warn}%
1.8 -A common mistake when writing definitions is to introduce extra free
1.9 -variables on the right-hand side as in the following fictitious definition:
1.10 -\input{Misc/document/prime_def.tex}%
1.11 -\end{warn}
1.12 +\input{Misc/document/prime_def.tex}
1.13
1.14
1.15 \chapter{More Functional Programming}
1.16 @@ -425,181 +421,17 @@
1.17 to as \bfindex{rewrite rules}. ``Rewriting'' is more honest than ``simplification''
1.18 because the terms do not necessarily become simpler in the process.
1.19
1.20 -\subsubsection{Simplification rules}
1.21 -\indexbold{simplification rules}
1.22 -
1.23 -To facilitate simplification, theorems can be declared to be simplification
1.24 -rules (with the help of the attribute \isa{[simp]}\index{*simp
1.25 - (attribute)}), in which case proofs by simplification make use of these
1.26 -rules automatically. In addition the constructs \isacommand{datatype} and
1.27 -\isacommand{primrec} (and a few others) invisibly declare useful
1.28 -simplification rules. Explicit definitions are \emph{not} declared
1.29 -simplification rules automatically!
1.30 -
1.31 -Not merely equations but pretty much any theorem can become a simplification
1.32 -rule. The simplifier will try to make sense of it. For example, a theorem
1.33 -\isasymnot$P$ is automatically turned into \isa{$P$ = False}. The details
1.34 -are explained in \S\ref{sec:SimpHow}.
1.35 -
1.36 -The simplification attribute of theorems can be turned on and off as follows:
1.37 -\begin{ttbox}
1.38 -lemmas [simp] = \(list of theorem names\);
1.39 -lemmas [simp del] = \(list of theorem names\);
1.40 -\end{ttbox}
1.41 -As a rule of thumb, equations that really simplify (like \isa{rev(rev xs) =
1.42 - xs} and \mbox{\isa{xs \at\ [] = xs}}) should be made simplification
1.43 -rules. Those of a more specific nature (e.g.\ distributivity laws, which
1.44 -alter the structure of terms considerably) should only be used selectively,
1.45 -i.e.\ they should not be default simplification rules. Conversely, it may
1.46 -also happen that a simplification rule needs to be disabled in certain
1.47 -proofs. Frequent changes in the simplification status of a theorem may
1.48 -indicate a badly designed theory.
1.49 -\begin{warn}
1.50 - Simplification may not terminate, for example if both $f(x) = g(x)$ and
1.51 - $g(x) = f(x)$ are simplification rules. It is the user's responsibility not
1.52 - to include simplification rules that can lead to nontermination, either on
1.53 - their own or in combination with other simplification rules.
1.54 -\end{warn}
1.55 -
1.56 -\subsubsection{The simplification method}
1.57 -\index{*simp (method)|bold}
1.58 -
1.59 -The general format of the simplification method is
1.60 -\begin{ttbox}
1.61 -simp \(list of modifiers\)
1.62 -\end{ttbox}
1.63 -where the list of \emph{modifiers} helps to fine tune the behaviour and may
1.64 -be empty. Most if not all of the proofs seen so far could have been performed
1.65 -with \isa{simp} instead of \isa{auto}, except that \isa{simp} attacks
1.66 -only the first subgoal and may thus need to be repeated---use \isaindex{simp_all}
1.67 -to simplify all subgoals.
1.68 -Note that \isa{simp} fails if nothing changes.
1.69 -
1.70 -\subsubsection{Adding and deleting simplification rules}
1.71 -
1.72 -If a certain theorem is merely needed in a few proofs by simplification,
1.73 -we do not need to make it a global simplification rule. Instead we can modify
1.74 -the set of simplification rules used in a simplification step by adding rules
1.75 -to it and/or deleting rules from it. The two modifiers for this are
1.76 -\begin{ttbox}
1.77 -add: \(list of theorem names\)
1.78 -del: \(list of theorem names\)
1.79 -\end{ttbox}
1.80 -In case you want to use only a specific list of theorems and ignore all
1.81 -others:
1.82 -\begin{ttbox}
1.83 -only: \(list of theorem names\)
1.84 -\end{ttbox}
1.85 -
1.86 -
1.87 -\subsubsection{Assumptions}
1.88 -\index{simplification!with/of assumptions}
1.89 -
1.90 -{\makeatother\input{Misc/document/asm_simp.tex}}
1.91 -
1.92 -\subsubsection{Rewriting with definitions}
1.93 -\index{simplification!with definitions}
1.94 -
1.95 -\input{Misc/document/def_rewr.tex}
1.96 -
1.97 -\begin{warn}
1.98 - If you have defined $f\,x\,y~\isasymequiv~t$ then you can only expand
1.99 - occurrences of $f$ with at least two arguments. Thus it is safer to define
1.100 - $f$~\isasymequiv~\isasymlambda$x\,y.\;t$.
1.101 -\end{warn}
1.102 -
1.103 -\input{Misc/document/let_rewr.tex}
1.104 -
1.105 -\subsubsection{Conditional equations}
1.106 -
1.107 -\input{Misc/document/cond_rewr.tex}
1.108 -
1.109 -
1.110 -\subsubsection{Automatic case splits}
1.111 -\indexbold{case splits}
1.112 -\index{*split|(}
1.113 -
1.114 -{\makeatother\input{Misc/document/case_splits.tex}}
1.115 -\index{*split|)}
1.116 -
1.117 -\begin{warn}
1.118 - The simplifier merely simplifies the condition of an \isa{if} but not the
1.119 - \isa{then} or \isa{else} parts. The latter are simplified only after the
1.120 - condition reduces to \isa{True} or \isa{False}, or after splitting. The
1.121 - same is true for \isaindex{case}-expressions: only the selector is
1.122 - simplified at first, until either the expression reduces to one of the
1.123 - cases or it is split.
1.124 -\end{warn}
1.125 -
1.126 -\subsubsection{Arithmetic}
1.127 -\index{arithmetic}
1.128 -
1.129 -The simplifier routinely solves a small class of linear arithmetic formulae
1.130 -(over type \isa{nat} and other numeric types): it only takes into account
1.131 -assumptions and conclusions that are (possibly negated) (in)equalities
1.132 -(\isa{=}, \isasymle, \isa{<}) and it only knows about addition. Thus
1.133 -
1.134 -\input{Misc/document/arith1.tex}%
1.135 -is proved by simplification, whereas the only slightly more complex
1.136 -
1.137 -\input{Misc/document/arith4.tex}%
1.138 -is not proved by simplification and requires \isa{arith}.
1.139 -
1.140 -\subsubsection{Tracing}
1.141 -\indexbold{tracing the simplifier}
1.142 -
1.143 -{\makeatother\input{Misc/document/trace_simp.tex}}
1.144 +\input{Misc/document/simp.tex}
1.145
1.146 \index{simplification|)}
1.147
1.148 -\section{Induction heuristics}
1.149 -\label{sec:InductionHeuristics}
1.150 -
1.151 -The purpose of this section is to illustrate some simple heuristics for
1.152 -inductive proofs. The first one we have already mentioned in our initial
1.153 -example:
1.154 -\begin{quote}
1.155 -\emph{Theorems about recursive functions are proved by induction.}
1.156 -\end{quote}
1.157 -In case the function has more than one argument
1.158 -\begin{quote}
1.159 -\emph{Do induction on argument number $i$ if the function is defined by
1.160 -recursion in argument number $i$.}
1.161 -\end{quote}
1.162 -When we look at the proof of {\makeatother\isa{(xs @ ys) @ zs = xs @ (ys @
1.163 - zs)}} in \S\ref{sec:intro-proof} we find (a) \isa{\at} is recursive in
1.164 -the first argument, (b) \isa{xs} occurs only as the first argument of
1.165 -\isa{\at}, and (c) both \isa{ys} and \isa{zs} occur at least once as
1.166 -the second argument of \isa{\at}. Hence it is natural to perform induction
1.167 -on \isa{xs}.
1.168 -
1.169 -The key heuristic, and the main point of this section, is to
1.170 -generalize the goal before induction. The reason is simple: if the goal is
1.171 -too specific, the induction hypothesis is too weak to allow the induction
1.172 -step to go through. Let us now illustrate the idea with an example.
1.173 -
1.174 -{\makeatother\input{Misc/document/Itrev.tex}}
1.175 -
1.176 -A final point worth mentioning is the orientation of the equation we just
1.177 -proved: the more complex notion (\isa{itrev}) is on the left-hand
1.178 -side, the simpler \isa{rev} on the right-hand side. This constitutes
1.179 -another, albeit weak heuristic that is not restricted to induction:
1.180 -\begin{quote}
1.181 - \emph{The right-hand side of an equation should (in some sense) be simpler
1.182 - than the left-hand side.}
1.183 -\end{quote}
1.184 -This heuristic is tricky to apply because it is not obvious that
1.185 -\isa{rev xs \at\ ys} is simpler than \isa{itrev xs ys}. But see what
1.186 -happens if you try to prove \isa{rev xs \at\ ys = itrev xs ys}!
1.187 +\input{Misc/document/Itrev.tex}
1.188
1.189 \begin{exercise}
1.190 \input{Misc/document/Tree2.tex}%
1.191 \end{exercise}
1.192
1.193 -\section{Case study: compiling expressions}
1.194 -\label{sec:ExprCompiler}
1.195 -
1.196 -{\makeatother\input{CodeGen/document/CodeGen.tex}}
1.197 +\input{CodeGen/document/CodeGen.tex}
1.198
1.199
1.200 \section{Advanced datatypes}