doc-src/TutorialI/fp.tex
 author nipkow Wed Jan 24 12:29:10 2001 +0100 (2001-01-24) changeset 10971 6852682eaf16 parent 10885 90695f46440b child 10978 5eebea8f359f permissions -rw-r--r--
*** empty log message ***
 nipkow@8743  1 \chapter{Functional Programming in HOL}  nipkow@8743  2 nipkow@8743  3 Although on the surface this chapter is mainly concerned with how to write  nipkow@8743  4 functional programs in HOL and how to verify them, most of the  nipkow@8743  5 constructs and proof procedures introduced are general purpose and recur in  nipkow@8743  6 any specification or verification task.  nipkow@8743  7 nipkow@9541  8 The dedicated functional programmer should be warned: HOL offers only  nipkow@9541  9 \emph{total functional programming} --- all functions in HOL must be total;  nipkow@9541  10 lazy data structures are not directly available. On the positive side,  nipkow@9541  11 functions in HOL need not be computable: HOL is a specification language that  nipkow@9541  12 goes well beyond what can be expressed as a program. However, for the time  nipkow@9541  13 being we concentrate on the computable.  nipkow@8743  14 paulson@10885  15 \section{An Introductory Theory}  nipkow@8743  16 \label{sec:intro-theory}  nipkow@8743  17 nipkow@8743  18 Functional programming needs datatypes and functions. Both of them can be  nipkow@8743  19 defined in a theory with a syntax reminiscent of languages like ML or  nipkow@8743  20 Haskell. As an example consider the theory in figure~\ref{fig:ToyList}.  nipkow@8743  21 We will now examine it line by line.  nipkow@8743  22 nipkow@8743  23 \begin{figure}[htbp]  nipkow@8743  24 \begin{ttbox}\makeatother  nipkow@8743  25 \input{ToyList2/ToyList1}\end{ttbox}  nipkow@8743  26 \caption{A theory of lists}  nipkow@8743  27 \label{fig:ToyList}  nipkow@8743  28 \end{figure}  nipkow@8743  29 nipkow@8743  30 {\makeatother\input{ToyList/document/ToyList.tex}}  nipkow@8743  31 paulson@10795  32 The complete proof script is shown in Fig.\ts\ref{fig:ToyList-proofs}. The  paulson@10795  33 concatenation of Figs.\ts\ref{fig:ToyList} and~\ref{fig:ToyList-proofs}  nipkow@8743  34 constitutes the complete theory \texttt{ToyList} and should reside in file  nipkow@8743  35 \texttt{ToyList.thy}. It is good practice to present all declarations and  nipkow@8743  36 definitions at the beginning of a theory to facilitate browsing.  nipkow@8743  37 nipkow@8743  38 \begin{figure}[htbp]  nipkow@8743  39 \begin{ttbox}\makeatother  nipkow@8743  40 \input{ToyList2/ToyList2}\end{ttbox}  nipkow@8743  41 \caption{Proofs about lists}  nipkow@8743  42 \label{fig:ToyList-proofs}  nipkow@8743  43 \end{figure}  nipkow@8743  44 nipkow@8743  45 \subsubsection*{Review}  nipkow@8743  46 nipkow@8743  47 This is the end of our toy proof. It should have familiarized you with  nipkow@8743  48 \begin{itemize}  nipkow@8743  49 \item the standard theorem proving procedure:  nipkow@8743  50 state a goal (lemma or theorem); proceed with proof until a separate lemma is  nipkow@8743  51 required; prove that lemma; come back to the original goal.  nipkow@8743  52 \item a specific procedure that works well for functional programs:  nipkow@8743  53 induction followed by all-out simplification via \isa{auto}.  nipkow@8743  54 \item a basic repertoire of proof commands.  nipkow@8743  55 \end{itemize}  nipkow@8743  56 nipkow@8743  57 paulson@10885  58 \section{Some Helpful Commands}  nipkow@8743  59 \label{sec:commands-and-hints}  nipkow@8743  60 nipkow@8743  61 This section discusses a few basic commands for manipulating the proof state  nipkow@8743  62 and can be skipped by casual readers.  nipkow@8743  63 nipkow@8743  64 There are two kinds of commands used during a proof: the actual proof  nipkow@8743  65 commands and auxiliary commands for examining the proof state and controlling  nipkow@8743  66 the display. Simple proof commands are of the form  nipkow@8743  67 \isacommand{apply}\isa{(method)}\indexbold{apply} where \bfindex{method} is a  nipkow@8743  68 synonym for theorem proving function''. Typical examples are  nipkow@8743  69 \isa{induct_tac} and \isa{auto}. Further methods are introduced throughout  nipkow@8743  70 the tutorial. Unless stated otherwise you may assume that a method attacks  nipkow@8743  71 merely the first subgoal. An exception is \isa{auto} which tries to solve all  nipkow@8743  72 subgoals.  nipkow@8743  73 nipkow@8743  74 The most useful auxiliary commands are:  nipkow@8743  75 \begin{description}  nipkow@8743  76 \item[Undoing:] \isacommand{undo}\indexbold{*undo} undoes the effect of the  nipkow@8743  77  last command; \isacommand{undo} can be undone by  nipkow@8743  78  \isacommand{redo}\indexbold{*redo}. Both are only needed at the shell  nipkow@8743  79  level and should not occur in the final theory.  nipkow@8743  80 \item[Printing the current state:] \isacommand{pr}\indexbold{*pr} redisplays  nipkow@8743  81  the current proof state, for example when it has disappeared off the  nipkow@8743  82  screen.  nipkow@8743  83 \item[Limiting the number of subgoals:] \isacommand{pr}~$n$ tells Isabelle to  nipkow@8743  84  print only the first $n$ subgoals from now on and redisplays the current  nipkow@8743  85  proof state. This is helpful when there are many subgoals.  nipkow@8743  86 \item[Modifying the order of subgoals:]  nipkow@8743  87 \isacommand{defer}\indexbold{*defer} moves the first subgoal to the end and  nipkow@8743  88 \isacommand{prefer}\indexbold{*prefer}~$n$ moves subgoal $n$ to the front.  nipkow@8743  89 \item[Printing theorems:]  nipkow@8743  90  \isacommand{thm}\indexbold{*thm}~\textit{name}$@1$~\dots~\textit{name}$@n$  nipkow@8743  91  prints the named theorems.  nipkow@8743  92 \item[Displaying types:] We have already mentioned the flag  nipkow@8743  93  \ttindex{show_types} above. It can also be useful for detecting typos in  nipkow@8743  94  formulae early on. For example, if \texttt{show_types} is set and the goal  nipkow@8743  95  \isa{rev(rev xs) = xs} is started, Isabelle prints the additional output  nipkow@8743  96 \par\noindent  nipkow@8743  97 \begin{isabelle}%  nipkow@8743  98 Variables:\isanewline  nipkow@8743  99 ~~xs~::~'a~list  nipkow@8743  100 \end{isabelle}%  nipkow@8743  101 \par\noindent  nipkow@8743  102 which tells us that Isabelle has correctly inferred that  nipkow@8743  103 \isa{xs} is a variable of list type. On the other hand, had we  nipkow@8743  104 made a typo as in \isa{rev(re xs) = xs}, the response  nipkow@8743  105 \par\noindent  nipkow@8743  106 \begin{isabelle}%  nipkow@8743  107 Variables:\isanewline  nipkow@8743  108 ~~re~::~'a~list~{\isasymRightarrow}~'a~list\isanewline  nipkow@8743  109 ~~xs~::~'a~list%  nipkow@8743  110 \end{isabelle}%  nipkow@8743  111 \par\noindent  nipkow@8743  112 would have alerted us because of the unexpected variable \isa{re}.  nipkow@8743  113 \item[Reading terms and types:] \isacommand{term}\indexbold{*term}  nipkow@8743  114  \textit{string} reads, type-checks and prints the given string as a term in  nipkow@8743  115  the current context; the inferred type is output as well.  nipkow@8743  116  \isacommand{typ}\indexbold{*typ} \textit{string} reads and prints the given  nipkow@8743  117  string as a type in the current context.  nipkow@8743  118 \item[(Re)loading theories:] When you start your interaction you must open a  nipkow@8771  119  named theory with the line \isa{\isacommand{theory}~T~=~\dots~:}. Isabelle  nipkow@8771  120  automatically loads all the required parent theories from their respective  nipkow@8771  121  files (which may take a moment, unless the theories are already loaded and  nipkow@9541  122  the files have not been modified).  nipkow@8743  123   nipkow@8743  124  If you suddenly discover that you need to modify a parent theory of your  nipkow@10971  125  current theory, you must first abandon your current theory\indexbold{abandon  nipkow@9494  126  theory}\indexbold{theory!abandon} (at the shell  nipkow@8743  127  level type \isacommand{kill}\indexbold{*kill}). After the parent theory has  nipkow@10971  128  been modified, you go back to your original theory. When its first line  nipkow@10971  129  \isa{\isacommand{theory}~T~=~\dots~:} is processed, the  nipkow@8743  130  modified parent is reloaded automatically.  nipkow@9541  131   nipkow@9541  132  The only time when you need to load a theory by hand is when you simply  nipkow@9541  133  want to check if it loads successfully without wanting to make use of the  nipkow@9541  134  theory itself. This you can do by typing  nipkow@9541  135  \isa{\isacommand{use\_thy}\indexbold{*use_thy}~"T"}.  nipkow@8743  136 \end{description}  nipkow@8743  137 Further commands are found in the Isabelle/Isar Reference Manual.  nipkow@8743  138 nipkow@8771  139 We now examine Isabelle's functional programming constructs systematically,  nipkow@8771  140 starting with inductive datatypes.  nipkow@8771  141 nipkow@8743  142 nipkow@8743  143 \section{Datatypes}  nipkow@8743  144 \label{sec:datatype}  nipkow@8743  145 nipkow@8743  146 Inductive datatypes are part of almost every non-trivial application of HOL.  nipkow@8743  147 First we take another look at a very important example, the datatype of  nipkow@8743  148 lists, before we turn to datatypes in general. The section closes with a  nipkow@8743  149 case study.  nipkow@8743  150 nipkow@8743  151 nipkow@8743  152 \subsection{Lists}  nipkow@8743  153 \indexbold{*list}  nipkow@8743  154 nipkow@8743  155 Lists are one of the essential datatypes in computing. Readers of this  nipkow@8743  156 tutorial and users of HOL need to be familiar with their basic operations.  nipkow@8771  157 Theory \isa{ToyList} is only a small fragment of HOL's predefined theory  nipkow@8771  158 \isa{List}\footnote{\url{http://isabelle.in.tum.de/library/HOL/List.html}}.  nipkow@8743  159 The latter contains many further operations. For example, the functions  nipkow@8771  160 \isaindexbold{hd} (head'') and \isaindexbold{tl} (tail'') return the first  nipkow@8743  161 element and the remainder of a list. (However, pattern-matching is usually  paulson@10795  162 preferable to \isa{hd} and \isa{tl}.)  nipkow@10800  163 Also available are higher-order functions like \isa{map} and \isa{filter}.  paulson@10795  164 Theory \isa{List} also contains  nipkow@8743  165 more syntactic sugar: \isa{[}$x@1$\isa{,}\dots\isa{,}$x@n$\isa{]} abbreviates  nipkow@8743  166 $x@1$\isa{\#}\dots\isa{\#}$x@n$\isa{\#[]}. In the rest of the tutorial we  nipkow@8743  167 always use HOL's predefined lists.  nipkow@8743  168 nipkow@8743  169 paulson@10885  170 \subsection{The General Format}  nipkow@8743  171 \label{sec:general-datatype}  nipkow@8743  172 nipkow@8743  173 The general HOL \isacommand{datatype} definition is of the form  nipkow@8743  174 $ nipkow@8743  175 \isacommand{datatype}~(\alpha@1, \dots, \alpha@n) \, t ~=~  nipkow@8743  176 C@1~\tau@{11}~\dots~\tau@{1k@1} ~\mid~ \dots ~\mid~  nipkow@8743  177 C@m~\tau@{m1}~\dots~\tau@{mk@m}  nipkow@8743  178 $  nipkow@8771  179 where $\alpha@i$ are distinct type variables (the parameters), $C@i$ are distinct  nipkow@8743  180 constructor names and $\tau@{ij}$ are types; it is customary to capitalize  nipkow@8743  181 the first letter in constructor names. There are a number of  nipkow@8743  182 restrictions (such as that the type should not be empty) detailed  nipkow@8743  183 elsewhere~\cite{isabelle-HOL}. Isabelle notifies you if you violate them.  nipkow@8743  184 nipkow@8743  185 Laws about datatypes, such as \isa{[] \isasymnoteq~x\#xs} and  nipkow@8743  186 \isa{(x\#xs = y\#ys) = (x=y \isasymand~xs=ys)}, are used automatically  nipkow@8743  187 during proofs by simplification. The same is true for the equations in  nipkow@8743  188 primitive recursive function definitions.  nipkow@8743  189 nipkow@9644  190 Every datatype $t$ comes equipped with a \isa{size} function from $t$ into  nipkow@10538  191 the natural numbers (see~{\S}\ref{sec:nat} below). For lists, \isa{size} is  nipkow@9644  192 just the length, i.e.\ \isa{size [] = 0} and \isa{size(x \# xs) = size xs +  nipkow@10237  193  1}. In general, \isaindexbold{size} returns \isa{0} for all constructors  nipkow@10237  194 that do not have an argument of type $t$, and for all other constructors  nipkow@10237  195 \isa{1 +} the sum of the sizes of all arguments of type $t$. Note that because  nipkow@9644  196 \isa{size} is defined on every datatype, it is overloaded; on lists  nipkow@10237  197 \isa{size} is also called \isaindexbold{length}, which is not overloaded.  paulson@10795  198 Isabelle will always show \isa{size} on lists as \isa{length}.  nipkow@9644  199 nipkow@9644  200 paulson@10885  201 \subsection{Primitive Recursion}  nipkow@8743  202 nipkow@8743  203 Functions on datatypes are usually defined by recursion. In fact, most of the  nipkow@8743  204 time they are defined by what is called \bfindex{primitive recursion}.  nipkow@8743  205 The keyword \isacommand{primrec}\indexbold{*primrec} is followed by a list of  nipkow@8743  206 equations  nipkow@8743  207 $f \, x@1 \, \dots \, (C \, y@1 \, \dots \, y@k)\, \dots \, x@n = r$  nipkow@8743  208 such that $C$ is a constructor of the datatype $t$ and all recursive calls of  nipkow@8743  209 $f$ in $r$ are of the form $f \, \dots \, y@i \, \dots$ for some $i$. Thus  nipkow@8743  210 Isabelle immediately sees that $f$ terminates because one (fixed!) argument  nipkow@10654  211 becomes smaller with every recursive call. There must be at most one equation  nipkow@8743  212 for each constructor. Their order is immaterial.  nipkow@8771  213 A more general method for defining total recursive functions is introduced in  nipkow@10538  214 {\S}\ref{sec:recdef}.  nipkow@8743  215 nipkow@9493  216 \begin{exercise}\label{ex:Tree}  nipkow@8743  217 \input{Misc/document/Tree.tex}%  nipkow@8743  218 \end{exercise}  nipkow@8743  219 nipkow@9721  220 \input{Misc/document/case_exprs.tex}  nipkow@8743  221 nipkow@8743  222 \input{Ifexpr/document/Ifexpr.tex}  nipkow@8743  223 paulson@10885  224 \section{Some Basic Types}  nipkow@8743  225 nipkow@8743  226 paulson@10885  227 \subsection{Natural Numbers}  nipkow@9644  228 \label{sec:nat}  nipkow@8743  229 \index{arithmetic|(}  nipkow@8743  230 nipkow@8743  231 \input{Misc/document/fakenat.tex}  nipkow@8743  232 \input{Misc/document/natsum.tex}  nipkow@8743  233 nipkow@8743  234 \index{arithmetic|)}  nipkow@8743  235 nipkow@8743  236 nipkow@10396  237 \subsection{Pairs}  nipkow@9541  238 \input{Misc/document/pairs.tex}  nipkow@8743  239 nipkow@10608  240 \subsection{Datatype {\tt\slshape option}}  nipkow@10543  241 \label{sec:option}  nipkow@10543  242 \input{Misc/document/Option2.tex}  nipkow@10543  243 nipkow@8743  244 \section{Definitions}  nipkow@8743  245 \label{sec:Definitions}  nipkow@8743  246 nipkow@8743  247 A definition is simply an abbreviation, i.e.\ a new name for an existing  nipkow@8743  248 construction. In particular, definitions cannot be recursive. Isabelle offers  nipkow@8743  249 definitions on the level of types and terms. Those on the type level are  nipkow@8743  250 called type synonyms, those on the term level are called (constant)  nipkow@8743  251 definitions.  nipkow@8743  252 nipkow@8743  253 paulson@10885  254 \subsection{Type Synonyms}  nipkow@8771  255 \indexbold{type synonym}  nipkow@8743  256 paulson@10795  257 Type synonyms are similar to those found in ML\@. Their syntax is fairly self  nipkow@8743  258 explanatory:  nipkow@8743  259 nipkow@8743  260 \input{Misc/document/types.tex}%  nipkow@8743  261 nipkow@8743  262 Note that pattern-matching is not allowed, i.e.\ each definition must be of  nipkow@8743  263 the form $f\,x@1\,\dots\,x@n~\isasymequiv~t$.  nipkow@10538  264 Section~{\S}\ref{sec:Simplification} explains how definitions are used  nipkow@8743  265 in proofs.  nipkow@8743  266 nipkow@9844  267 \input{Misc/document/prime_def.tex}  nipkow@8743  268 nipkow@8743  269 nipkow@8743  270 \chapter{More Functional Programming}  nipkow@8743  271 nipkow@8743  272 The purpose of this chapter is to deepen the reader's understanding of the  nipkow@8771  273 concepts encountered so far and to introduce advanced forms of datatypes and  nipkow@8771  274 recursive functions. The first two sections give a structured presentation of  nipkow@10538  275 theorem proving by simplification ({\S}\ref{sec:Simplification}) and discuss  nipkow@10538  276 important heuristics for induction ({\S}\ref{sec:InductionHeuristics}). They can  nipkow@8771  277 be skipped by readers less interested in proofs. They are followed by a case  nipkow@10538  278 study, a compiler for expressions ({\S}\ref{sec:ExprCompiler}). Advanced  nipkow@8771  279 datatypes, including those involving function spaces, are covered in  nipkow@10538  280 {\S}\ref{sec:advanced-datatypes}, which closes with another case study, search  nipkow@8771  281 trees (tries''). Finally we introduce \isacommand{recdef}, a very general  nipkow@8771  282 form of recursive function definition which goes well beyond what  nipkow@10538  283 \isacommand{primrec} allows ({\S}\ref{sec:recdef}).  nipkow@8743  284 nipkow@8743  285 nipkow@8743  286 \section{Simplification}  nipkow@8743  287 \label{sec:Simplification}  nipkow@8743  288 \index{simplification|(}  nipkow@8743  289 paulson@10795  290 So far we have proved our theorems by \isa{auto}, which simplifies  nipkow@9541  291 \emph{all} subgoals. In fact, \isa{auto} can do much more than that, except  nipkow@9541  292 that it did not need to so far. However, when you go beyond toy examples, you  nipkow@9541  293 need to understand the ingredients of \isa{auto}. This section covers the  nipkow@10971  294 method that \isa{auto} always applies first, simplification.  nipkow@8743  295 nipkow@8743  296 Simplification is one of the central theorem proving tools in Isabelle and  nipkow@8743  297 many other systems. The tool itself is called the \bfindex{simplifier}. The  nipkow@9754  298 purpose of this section is introduce the many features of the simplifier.  nipkow@10971  299 Anybody intending to perform proofs in HOL should read this section. Later on  nipkow@10538  300 ({\S}\ref{sec:simplification-II}) we explain some more advanced features and a  nipkow@9754  301 little bit of how the simplifier works. The serious student should read that  nipkow@9754  302 section as well, in particular in order to understand what happened if things  nipkow@9754  303 do not simplify as expected.  nipkow@8743  304 paulson@10885  305 \subsubsection{What is Simplification?}  nipkow@9458  306 nipkow@8743  307 In its most basic form, simplification means repeated application of  nipkow@8743  308 equations from left to right. For example, taking the rules for \isa{\at}  nipkow@8743  309 and applying them to the term \isa{[0,1] \at\ []} results in a sequence of  nipkow@8743  310 simplification steps:  nipkow@8743  311 \begin{ttbox}\makeatother  nipkow@8743  312 (0#1#[]) @ [] $$\leadsto$$ 0#((1#[]) @ []) $$\leadsto$$ 0#(1#([] @ [])) $$\leadsto$$ 0#1#[]  nipkow@8743  313 \end{ttbox}  nipkow@9933  314 This is also known as \bfindex{term rewriting}\indexbold{rewriting} and the  nipkow@9933  315 equations are referred to as \textbf{rewrite rules}\indexbold{rewrite rule}.  nipkow@9933  316 Rewriting'' is more honest than simplification'' because the terms do not  nipkow@9933  317 necessarily become simpler in the process.  nipkow@8743  318 nipkow@9844  319 \input{Misc/document/simp.tex}  nipkow@8743  320 nipkow@8743  321 \index{simplification|)}  nipkow@8743  322 nipkow@9844  323 \input{Misc/document/Itrev.tex}  nipkow@8743  324 nipkow@9493  325 \begin{exercise}  nipkow@9493  326 \input{Misc/document/Tree2.tex}%  nipkow@9493  327 \end{exercise}  nipkow@8743  328 nipkow@9844  329 \input{CodeGen/document/CodeGen.tex}  nipkow@8743  330 nipkow@8743  331 paulson@10885  332 \section{Advanced Datatypes}  nipkow@8743  333 \label{sec:advanced-datatypes}  nipkow@8743  334 \index{*datatype|(}  nipkow@8743  335 \index{*primrec|(}  nipkow@8743  336 %|)  nipkow@8743  337 nipkow@8743  338 This section presents advanced forms of \isacommand{datatype}s.  nipkow@8743  339 paulson@10885  340 \subsection{Mutual Recursion}  nipkow@8743  341 \label{sec:datatype-mut-rec}  nipkow@8743  342 nipkow@8743  343 \input{Datatype/document/ABexpr.tex}  nipkow@8743  344 paulson@10885  345 \subsection{Nested Recursion}  nipkow@9644  346 \label{sec:nested-datatype}  nipkow@8743  347 nipkow@9644  348 {\makeatother\input{Datatype/document/Nested.tex}}  nipkow@8743  349 nipkow@8743  350 paulson@10885  351 \subsection{The Limits of Nested Recursion}  nipkow@8743  352 nipkow@8743  353 How far can we push nested recursion? By the unfolding argument above, we can  nipkow@8743  354 reduce nested to mutual recursion provided the nested recursion only involves  nipkow@8743  355 previously defined datatypes. This does not include functions:  nipkow@9792  356 \begin{isabelle}  nipkow@9792  357 \isacommand{datatype} t = C "t \isasymRightarrow\ bool"  nipkow@9792  358 \end{isabelle}  paulson@10795  359 This declaration is a real can of worms.  paulson@10795  360 In HOL it must be ruled out because it requires a type  nipkow@8743  361 \isa{t} such that \isa{t} and its power set \isa{t \isasymFun\ bool} have the  nipkow@10971  362 same cardinality --- an impossibility. For the same reason it is not possible  nipkow@8743  363 to allow recursion involving the type \isa{set}, which is isomorphic to  nipkow@8743  364 \isa{t \isasymFun\ bool}.  nipkow@8743  365 nipkow@8743  366 Fortunately, a limited form of recursion  nipkow@8743  367 involving function spaces is permitted: the recursive type may occur on the  nipkow@8743  368 right of a function arrow, but never on the left. Hence the above can of worms  nipkow@8743  369 is ruled out but the following example of a potentially infinitely branching tree is  nipkow@8743  370 accepted:  nipkow@8771  371 \smallskip  nipkow@8743  372 nipkow@8743  373 \input{Datatype/document/Fundata.tex}  nipkow@8743  374 \bigskip  nipkow@8743  375 nipkow@9792  376 If you need nested recursion on the left of a function arrow, there are  nipkow@9792  377 alternatives to pure HOL: LCF~\cite{paulson87} is a logic where types like  nipkow@9792  378 \begin{isabelle}  nipkow@9792  379 \isacommand{datatype} lam = C "lam \isasymrightarrow\ lam"  nipkow@9792  380 \end{isabelle}  paulson@10795  381 do indeed make sense. Note the different arrow,  paulson@10795  382 \isa{\isasymrightarrow} instead of \isa{\isasymRightarrow},  nipkow@10971  383 expressing the type of \emph{continuous} functions.  paulson@10795  384 There is even a version of LCF on top of HOL,  nipkow@9792  385 called HOLCF~\cite{MuellerNvOS99}.  nipkow@8743  386 nipkow@8743  387 \index{*primrec|)}  nipkow@8743  388 \index{*datatype|)}  nipkow@8743  389 paulson@10885  390 \subsection{Case Study: Tries}  nipkow@10543  391 \label{sec:Trie}  nipkow@8743  392 nipkow@8743  393 Tries are a classic search tree data structure~\cite{Knuth3-75} for fast  nipkow@8743  394 indexing with strings. Figure~\ref{fig:trie} gives a graphical example of a  nipkow@8743  395 trie containing the words all'', an'', ape'', can'', car'' and  nipkow@8743  396 cat''. When searching a string in a trie, the letters of the string are  nipkow@8743  397 examined sequentially. Each letter determines which subtrie to search next.  nipkow@8743  398 In this case study we model tries as a datatype, define a lookup and an  nipkow@8743  399 update function, and prove that they behave as expected.  nipkow@8743  400 nipkow@8743  401 \begin{figure}[htbp]  nipkow@8743  402 \begin{center}  nipkow@8743  403 \unitlength1mm  nipkow@8743  404 \begin{picture}(60,30)  nipkow@8743  405 \put( 5, 0){\makebox(0,0)[b]{l}}  nipkow@8743  406 \put(25, 0){\makebox(0,0)[b]{e}}  nipkow@8743  407 \put(35, 0){\makebox(0,0)[b]{n}}  nipkow@8743  408 \put(45, 0){\makebox(0,0)[b]{r}}  nipkow@8743  409 \put(55, 0){\makebox(0,0)[b]{t}}  nipkow@8743  410 %  nipkow@8743  411 \put( 5, 9){\line(0,-1){5}}  nipkow@8743  412 \put(25, 9){\line(0,-1){5}}  nipkow@8743  413 \put(44, 9){\line(-3,-2){9}}  nipkow@8743  414 \put(45, 9){\line(0,-1){5}}  nipkow@8743  415 \put(46, 9){\line(3,-2){9}}  nipkow@8743  416 %  nipkow@8743  417 \put( 5,10){\makebox(0,0)[b]{l}}  nipkow@8743  418 \put(15,10){\makebox(0,0)[b]{n}}  nipkow@8743  419 \put(25,10){\makebox(0,0)[b]{p}}  nipkow@8743  420 \put(45,10){\makebox(0,0)[b]{a}}  nipkow@8743  421 %  nipkow@8743  422 \put(14,19){\line(-3,-2){9}}  nipkow@8743  423 \put(15,19){\line(0,-1){5}}  nipkow@8743  424 \put(16,19){\line(3,-2){9}}  nipkow@8743  425 \put(45,19){\line(0,-1){5}}  nipkow@8743  426 %  nipkow@8743  427 \put(15,20){\makebox(0,0)[b]{a}}  nipkow@8743  428 \put(45,20){\makebox(0,0)[b]{c}}  nipkow@8743  429 %  nipkow@8743  430 \put(30,30){\line(-3,-2){13}}  nipkow@8743  431 \put(30,30){\line(3,-2){13}}  nipkow@8743  432 \end{picture}  nipkow@8743  433 \end{center}  nipkow@8743  434 \caption{A sample trie}  nipkow@8743  435 \label{fig:trie}  nipkow@8743  436 \end{figure}  nipkow@8743  437 nipkow@8743  438 Proper tries associate some value with each string. Since the  nipkow@8743  439 information is stored only in the final node associated with the string, many  nipkow@10543  440 nodes do not carry any value. This distinction is modeled with the help  nipkow@10543  441 of the predefined datatype \isa{option} (see {\S}\ref{sec:option}).  nipkow@8743  442 \input{Trie/document/Trie.tex}  nipkow@8743  443 nipkow@8743  444 \begin{exercise}  nipkow@8743  445  Write an improved version of \isa{update} that does not suffer from the  nipkow@8743  446  space leak in the version above. Prove the main theorem for your improved  nipkow@8743  447  \isa{update}.  nipkow@8743  448 \end{exercise}  nipkow@8743  449 nipkow@8743  450 \begin{exercise}  nipkow@8743  451  Write a function to \emph{delete} entries from a trie. An easy solution is  nipkow@8743  452  a clever modification of \isa{update} which allows both insertion and  nipkow@8743  453  deletion with a single function. Prove (a modified version of) the main  nipkow@8743  454  theorem above. Optimize you function such that it shrinks tries after  nipkow@8743  455  deletion, if possible.  nipkow@8743  456 \end{exercise}  nipkow@8743  457 paulson@10885  458 \section{Total Recursive Functions}  nipkow@8743  459 \label{sec:recdef}  nipkow@8743  460 \index{*recdef|(}  nipkow@8743  461 nipkow@8743  462 Although many total functions have a natural primitive recursive definition,  nipkow@8743  463 this is not always the case. Arbitrary total recursive functions can be  nipkow@8743  464 defined by means of \isacommand{recdef}: you can use full pattern-matching,  nipkow@8743  465 recursion need not involve datatypes, and termination is proved by showing  nipkow@8743  466 that the arguments of all recursive calls are smaller in a suitable (user  nipkow@10522  467 supplied) sense. In this section we ristrict ourselves to measure functions;  nipkow@10538  468 more advanced termination proofs are discussed in {\S}\ref{sec:beyond-measure}.  nipkow@8743  469 paulson@10885  470 \subsection{Defining Recursive Functions}  nipkow@10654  471 \label{sec:recdef-examples}  nipkow@8743  472 \input{Recdef/document/examples.tex}  nipkow@8743  473 paulson@10885  474 \subsection{Proving Termination}  nipkow@8743  475 nipkow@8743  476 \input{Recdef/document/termination.tex}  nipkow@8743  477 paulson@10885  478 \subsection{Simplification with Recdef}  paulson@10181  479 \label{sec:recdef-simplification}  nipkow@8743  480 nipkow@8743  481 \input{Recdef/document/simplification.tex}  nipkow@8743  482 nipkow@8743  483 \subsection{Induction}  nipkow@8743  484 \index{induction!recursion|(}  nipkow@8743  485 \index{recursion induction|(}  nipkow@8743  486 nipkow@8743  487 \input{Recdef/document/Induction.tex}  nipkow@9644  488 \label{sec:recdef-induction}  nipkow@8743  489 nipkow@8743  490 \index{induction!recursion|)}  nipkow@8743  491 \index{recursion induction|)}  nipkow@8743  492 \index{*recdef|)}