summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

doc-src/TutorialI/fp.tex

changeset 9844 | 8016321c7de1 |

parent 9792 | bbefb6ce5cb2 |

child 9933 | 9feb1e0c4cb3 |

--- a/doc-src/TutorialI/fp.tex Tue Sep 05 13:12:00 2000 +0200 +++ b/doc-src/TutorialI/fp.tex Tue Sep 05 13:53:39 2000 +0200 @@ -370,11 +370,7 @@ Section~\S\ref{sec:Simplification} explains how definitions are used in proofs. -\begin{warn}% -A common mistake when writing definitions is to introduce extra free -variables on the right-hand side as in the following fictitious definition: -\input{Misc/document/prime_def.tex}% -\end{warn} +\input{Misc/document/prime_def.tex} \chapter{More Functional Programming} @@ -425,181 +421,17 @@ to as \bfindex{rewrite rules}. ``Rewriting'' is more honest than ``simplification'' because the terms do not necessarily become simpler in the process. -\subsubsection{Simplification rules} -\indexbold{simplification rules} - -To facilitate simplification, theorems can be declared to be simplification -rules (with the help of the attribute \isa{[simp]}\index{*simp - (attribute)}), in which case proofs by simplification make use of these -rules automatically. In addition the constructs \isacommand{datatype} and -\isacommand{primrec} (and a few others) invisibly declare useful -simplification rules. Explicit definitions are \emph{not} declared -simplification rules automatically! - -Not merely equations but pretty much any theorem can become a simplification -rule. The simplifier will try to make sense of it. For example, a theorem -\isasymnot$P$ is automatically turned into \isa{$P$ = False}. The details -are explained in \S\ref{sec:SimpHow}. - -The simplification attribute of theorems can be turned on and off as follows: -\begin{ttbox} -lemmas [simp] = \(list of theorem names\); -lemmas [simp del] = \(list of theorem names\); -\end{ttbox} -As a rule of thumb, equations that really simplify (like \isa{rev(rev xs) = - xs} and \mbox{\isa{xs \at\ [] = xs}}) should be made simplification -rules. Those of a more specific nature (e.g.\ distributivity laws, which -alter the structure of terms considerably) should only be used selectively, -i.e.\ they should not be default simplification rules. Conversely, it may -also happen that a simplification rule needs to be disabled in certain -proofs. Frequent changes in the simplification status of a theorem may -indicate a badly designed theory. -\begin{warn} - Simplification may not terminate, for example if both $f(x) = g(x)$ and - $g(x) = f(x)$ are simplification rules. It is the user's responsibility not - to include simplification rules that can lead to nontermination, either on - their own or in combination with other simplification rules. -\end{warn} - -\subsubsection{The simplification method} -\index{*simp (method)|bold} - -The general format of the simplification method is -\begin{ttbox} -simp \(list of modifiers\) -\end{ttbox} -where the list of \emph{modifiers} helps to fine tune the behaviour and may -be empty. Most if not all of the proofs seen so far could have been performed -with \isa{simp} instead of \isa{auto}, except that \isa{simp} attacks -only the first subgoal and may thus need to be repeated---use \isaindex{simp_all} -to simplify all subgoals. -Note that \isa{simp} fails if nothing changes. - -\subsubsection{Adding and deleting simplification rules} - -If a certain theorem is merely needed in a few proofs by simplification, -we do not need to make it a global simplification rule. Instead we can modify -the set of simplification rules used in a simplification step by adding rules -to it and/or deleting rules from it. The two modifiers for this are -\begin{ttbox} -add: \(list of theorem names\) -del: \(list of theorem names\) -\end{ttbox} -In case you want to use only a specific list of theorems and ignore all -others: -\begin{ttbox} -only: \(list of theorem names\) -\end{ttbox} - - -\subsubsection{Assumptions} -\index{simplification!with/of assumptions} - -{\makeatother\input{Misc/document/asm_simp.tex}} - -\subsubsection{Rewriting with definitions} -\index{simplification!with definitions} - -\input{Misc/document/def_rewr.tex} - -\begin{warn} - If you have defined $f\,x\,y~\isasymequiv~t$ then you can only expand - occurrences of $f$ with at least two arguments. Thus it is safer to define - $f$~\isasymequiv~\isasymlambda$x\,y.\;t$. -\end{warn} - -\input{Misc/document/let_rewr.tex} - -\subsubsection{Conditional equations} - -\input{Misc/document/cond_rewr.tex} - - -\subsubsection{Automatic case splits} -\indexbold{case splits} -\index{*split|(} - -{\makeatother\input{Misc/document/case_splits.tex}} -\index{*split|)} - -\begin{warn} - The simplifier merely simplifies the condition of an \isa{if} but not the - \isa{then} or \isa{else} parts. The latter are simplified only after the - condition reduces to \isa{True} or \isa{False}, or after splitting. The - same is true for \isaindex{case}-expressions: only the selector is - simplified at first, until either the expression reduces to one of the - cases or it is split. -\end{warn} - -\subsubsection{Arithmetic} -\index{arithmetic} - -The simplifier routinely solves a small class of linear arithmetic formulae -(over type \isa{nat} and other numeric types): it only takes into account -assumptions and conclusions that are (possibly negated) (in)equalities -(\isa{=}, \isasymle, \isa{<}) and it only knows about addition. Thus - -\input{Misc/document/arith1.tex}% -is proved by simplification, whereas the only slightly more complex - -\input{Misc/document/arith4.tex}% -is not proved by simplification and requires \isa{arith}. - -\subsubsection{Tracing} -\indexbold{tracing the simplifier} - -{\makeatother\input{Misc/document/trace_simp.tex}} +\input{Misc/document/simp.tex} \index{simplification|)} -\section{Induction heuristics} -\label{sec:InductionHeuristics} - -The purpose of this section is to illustrate some simple heuristics for -inductive proofs. The first one we have already mentioned in our initial -example: -\begin{quote} -\emph{Theorems about recursive functions are proved by induction.} -\end{quote} -In case the function has more than one argument -\begin{quote} -\emph{Do induction on argument number $i$ if the function is defined by -recursion in argument number $i$.} -\end{quote} -When we look at the proof of {\makeatother\isa{(xs @ ys) @ zs = xs @ (ys @ - zs)}} in \S\ref{sec:intro-proof} we find (a) \isa{\at} is recursive in -the first argument, (b) \isa{xs} occurs only as the first argument of -\isa{\at}, and (c) both \isa{ys} and \isa{zs} occur at least once as -the second argument of \isa{\at}. Hence it is natural to perform induction -on \isa{xs}. - -The key heuristic, and the main point of this section, is to -generalize the goal before induction. The reason is simple: if the goal is -too specific, the induction hypothesis is too weak to allow the induction -step to go through. Let us now illustrate the idea with an example. - -{\makeatother\input{Misc/document/Itrev.tex}} - -A final point worth mentioning is the orientation of the equation we just -proved: the more complex notion (\isa{itrev}) is on the left-hand -side, the simpler \isa{rev} on the right-hand side. This constitutes -another, albeit weak heuristic that is not restricted to induction: -\begin{quote} - \emph{The right-hand side of an equation should (in some sense) be simpler - than the left-hand side.} -\end{quote} -This heuristic is tricky to apply because it is not obvious that -\isa{rev xs \at\ ys} is simpler than \isa{itrev xs ys}. But see what -happens if you try to prove \isa{rev xs \at\ ys = itrev xs ys}! +\input{Misc/document/Itrev.tex} \begin{exercise} \input{Misc/document/Tree2.tex}% \end{exercise} -\section{Case study: compiling expressions} -\label{sec:ExprCompiler} - -{\makeatother\input{CodeGen/document/CodeGen.tex}} +\input{CodeGen/document/CodeGen.tex} \section{Advanced datatypes}