# HG changeset patch # User paulson # Date 990199123 -7200 # Node ID d666f11ca2d41cb427ba4dee6e9549e179806194 # Parent b28bbb153603378a9b506cb321780c2f5077d277 minor suggestions by Tanja Vos diff -r b28bbb153603 -r d666f11ca2d4 doc-src/TutorialI/Datatype/ABexpr.thy --- a/doc-src/TutorialI/Datatype/ABexpr.thy Fri May 18 16:45:55 2001 +0200 +++ b/doc-src/TutorialI/Datatype/ABexpr.thy Fri May 18 17:18:43 2001 +0200 @@ -27,8 +27,9 @@ text{*\noindent Type @{text"aexp"} is similar to @{text"expr"} in \S\ref{sec:ExprCompiler}, -except that we have fixed the values to be of type @{typ"nat"} and that we -have fixed the two binary operations @{text Sum} and @{term"Diff"}. Boolean +except that we have added an @{text IF} constructor, +fixed the values to be of type @{typ"nat"} and declared the two binary +operations @{text Sum} and @{term"Diff"}. Boolean expressions can be arithmetic comparisons, conjunctions and negations. The semantics is fixed via two evaluation functions *} diff -r b28bbb153603 -r d666f11ca2d4 doc-src/TutorialI/Datatype/Fundata.thy --- a/doc-src/TutorialI/Datatype/Fundata.thy Fri May 18 16:45:55 2001 +0200 +++ b/doc-src/TutorialI/Datatype/Fundata.thy Fri May 18 17:18:43 2001 +0200 @@ -32,7 +32,7 @@ Isabelle because the termination proof is not as obvious since @{term"map_bt"} is only partially applied. -The following lemma has a canonical proof: *} +The following lemma has a simple proof by induction: *} lemma "map_bt (g o f) T = map_bt g (map_bt f T)"; apply(induct_tac T, simp_all) diff -r b28bbb153603 -r d666f11ca2d4 doc-src/TutorialI/Datatype/Nested.thy --- a/doc-src/TutorialI/Datatype/Nested.thy Fri May 18 16:45:55 2001 +0200 +++ b/doc-src/TutorialI/Datatype/Nested.thy Fri May 18 17:18:43 2001 +0200 @@ -120,7 +120,9 @@ could derive a new induction principle as well (see \S\ref{sec:derive-ind}), but simpler is to stop using \isacommand{primrec} and to define functions with \isacommand{recdef} instead. -The details are explained in \S\ref{sec:nested-recdef} below. +Simple uses of \isacommand{recdef} are described in \S\ref{sec:recdef} below, +and later (\S\ref{sec:nested-recdef}) we shall see how \isacommand{recdef} can +handle nested recursion. Of course, you may also combine mutual and nested recursion of datatypes. For example, constructor @{text Sum} in \S\ref{sec:datatype-mut-rec} could take a list of diff -r b28bbb153603 -r d666f11ca2d4 doc-src/TutorialI/Datatype/document/ABexpr.tex --- a/doc-src/TutorialI/Datatype/document/ABexpr.tex Fri May 18 16:45:55 2001 +0200 +++ b/doc-src/TutorialI/Datatype/document/ABexpr.tex Fri May 18 17:18:43 2001 +0200 @@ -26,8 +26,9 @@ \begin{isamarkuptext}% \noindent Type \isa{aexp} is similar to \isa{expr} in \S\ref{sec:ExprCompiler}, -except that we have fixed the values to be of type \isa{nat} and that we -have fixed the two binary operations \isa{Sum} and \isa{Diff}. Boolean +except that we have added an \isa{IF} constructor, +fixed the values to be of type \isa{nat} and declared the two binary +operations \isa{Sum} and \isa{Diff}. Boolean expressions can be arithmetic comparisons, conjunctions and negations. The semantics is fixed via two evaluation functions% \end{isamarkuptext}% diff -r b28bbb153603 -r d666f11ca2d4 doc-src/TutorialI/Datatype/document/Fundata.tex --- a/doc-src/TutorialI/Datatype/document/Fundata.tex Fri May 18 16:45:55 2001 +0200 +++ b/doc-src/TutorialI/Datatype/document/Fundata.tex Fri May 18 17:18:43 2001 +0200 @@ -33,7 +33,7 @@ Isabelle because the termination proof is not as obvious since \isa{map{\isacharunderscore}bt} is only partially applied. -The following lemma has a canonical proof:% +The following lemma has a simple proof by induction:% \end{isamarkuptext}% \isacommand{lemma}\ {\isachardoublequote}map{\isacharunderscore}bt\ {\isacharparenleft}g\ o\ f{\isacharparenright}\ T\ {\isacharequal}\ map{\isacharunderscore}bt\ g\ {\isacharparenleft}map{\isacharunderscore}bt\ f\ T{\isacharparenright}{\isachardoublequote}\isanewline \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ T{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline diff -r b28bbb153603 -r d666f11ca2d4 doc-src/TutorialI/Datatype/document/Nested.tex --- a/doc-src/TutorialI/Datatype/document/Nested.tex Fri May 18 16:45:55 2001 +0200 +++ b/doc-src/TutorialI/Datatype/document/Nested.tex Fri May 18 17:18:43 2001 +0200 @@ -118,7 +118,9 @@ could derive a new induction principle as well (see \S\ref{sec:derive-ind}), but simpler is to stop using \isacommand{primrec} and to define functions with \isacommand{recdef} instead. -The details are explained in \S\ref{sec:nested-recdef} below. +Simple uses of \isacommand{recdef} are described in \S\ref{sec:recdef} below, +and later (\S\ref{sec:nested-recdef}) we shall see how \isacommand{recdef} can +handle nested recursion. Of course, you may also combine mutual and nested recursion of datatypes. For example, constructor \isa{Sum} in \S\ref{sec:datatype-mut-rec} could take a list of diff -r b28bbb153603 -r d666f11ca2d4 doc-src/TutorialI/Misc/document/simp.tex --- a/doc-src/TutorialI/Misc/document/simp.tex Fri May 18 16:45:55 2001 +0200 +++ b/doc-src/TutorialI/Misc/document/simp.tex Fri May 18 17:18:43 2001 +0200 @@ -25,13 +25,16 @@ \isacommand{declare} \textit{theorem-name}\isa{{\isacharbrackleft}simp{\isacharbrackright}}\\ \isacommand{declare} \textit{theorem-name}\isa{{\isacharbrackleft}simp\ del{\isacharbrackright}} \end{quote} -As a rule of thumb, equations that really simplify (like \isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs} and \isa{xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ 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. +Only equations that really simplify, like \isa{rev\ +{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs} and +\isa{xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ +{\isacharequal}\ xs}, should be declared as default simplification rules. +More specific ones should only be used selectively and should +not be made default. Distributivity laws, for example, alter +the structure of terms and can produce an exponential blow-up instead of +simplification. A default simplification rule may +need to be disabled in certain proofs. Frequent changes in the simplification +status of a theorem may indicate an unwise use of defaults. \begin{warn} Simplification may run forever, for example if both $f(x) = g(x)$ and $g(x) = f(x)$ are simplification rules. It is the user's responsibility not @@ -50,7 +53,8 @@ \isa{simp} \textit{list of modifiers} \end{quote} where the list of \emph{modifiers} fine tunes the behaviour and may -be empty. Most if not all of the proofs seen so far could have been performed +be empty. Specific modifiers are discussed below. 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. @@ -73,6 +77,11 @@ others: \begin{quote} \isa{only{\isacharcolon}} \textit{list of theorem names} +\end{quote} +In this example, we invoke the simplifier, adding two distributive +laws: +\begin{quote} +\isacommand{apply}\isa{{\isacharparenleft}simp\ add{\isacharcolon}\ mod{\isacharunderscore}mult{\isacharunderscore}distrib\ add{\isacharunderscore}mult{\isacharunderscore}distrib{\isacharparenright}} \end{quote}% \end{isamarkuptext}% % @@ -123,7 +132,7 @@ Both \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}simp{\isacharparenright}} and \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}} run forever on the problematic subgoal above. Note that only one of the modifiers is allowed, and it must precede all -other arguments. +other modifiers. \begin{warn} Assumptions are simplified in a left-to-right fashion. If an @@ -259,7 +268,8 @@ simplifier performs it automatically. Try \isacommand{apply}\isa{{\isacharparenleft}simp{\isacharparenright}} on the initial goal above. -This splitting idea generalizes from \isa{if} to \isaindex{case}:% +This splitting idea generalizes from \isa{if} to \isaindex{case}. +Let us simplify a case analysis over lists:% \end{isamarkuptxt}% \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ zs\ {\isacharbar}\ y{\isacharhash}ys\ {\isasymRightarrow}\ y{\isacharhash}{\isacharparenleft}ys{\isacharat}zs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ xs{\isacharat}zs{\isachardoublequote}\isanewline \isacommand{apply}{\isacharparenleft}split\ list{\isachardot}split{\isacharparenright}% @@ -386,7 +396,13 @@ [a] = [] == False \end{ttbox} -In more complicated cases, the trace can be quite lenghty, especially since +The trace lists each rule being applied, both in its general form and the +instance being used. For conditional rules, the trace lists the rule +it is trying to rewrite and gives the result of attempting to prove +each of the rule's conditions. Many other hints about the simplifier's +actions will appear. + +In more complicated cases, the trace can be quite lengthy, especially since invocations of the simplifier are often nested (e.g.\ when solving conditions of rewrite rules). Thus it is advisable to reset it:% \end{isamarkuptext}% diff -r b28bbb153603 -r d666f11ca2d4 doc-src/TutorialI/Misc/simp.thy --- a/doc-src/TutorialI/Misc/simp.thy Fri May 18 16:45:55 2001 +0200 +++ b/doc-src/TutorialI/Misc/simp.thy Fri May 18 17:18:43 2001 +0200 @@ -23,14 +23,16 @@ \isacommand{declare} \textit{theorem-name}@{text"[simp]"}\\ \isacommand{declare} \textit{theorem-name}@{text"[simp del]"} \end{quote} -As a rule of thumb, equations that really simplify (like @{prop"rev(rev xs) = - xs"} and @{prop"xs @ [] = 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. +Only equations that really simplify, like \isa{rev\ +{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs} and +\isa{xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ +{\isacharequal}\ xs}, should be declared as default simplification rules. +More specific ones should only be used selectively and should +not be made default. Distributivity laws, for example, alter +the structure of terms and can produce an exponential blow-up instead of +simplification. A default simplification rule may +need to be disabled in certain proofs. Frequent changes in the simplification +status of a theorem may indicate an unwise use of defaults. \begin{warn} Simplification may run forever, for example if both $f(x) = g(x)$ and $g(x) = f(x)$ are simplification rules. It is the user's responsibility not @@ -47,7 +49,8 @@ @{text simp} \textit{list of modifiers} \end{quote} where the list of \emph{modifiers} fine tunes the behaviour and may -be empty. Most if not all of the proofs seen so far could have been performed +be empty. Specific modifiers are discussed below. Most if not all of the +proofs seen so far could have been performed with @{text simp} instead of \isa{auto}, except that @{text simp} attacks only the first subgoal and may thus need to be repeated --- use \isaindex{simp_all} to simplify all subgoals. @@ -70,6 +73,11 @@ \begin{quote} @{text"only:"} \textit{list of theorem names} \end{quote} +In this example, we invoke the simplifier, adding two distributive +laws: +\begin{quote} +\isacommand{apply}@{text"(simp add: mod_mult_distrib add_mult_distrib)"} +\end{quote} *} subsection{*Assumptions*} @@ -120,7 +128,7 @@ Both @{text"(no_asm_simp)"} and @{text"(no_asm_use)"} run forever on the problematic subgoal above. Note that only one of the modifiers is allowed, and it must precede all -other arguments. +other modifiers. \begin{warn} Assumptions are simplified in a left-to-right fashion. If an @@ -258,11 +266,12 @@ simplifier performs it automatically. Try \isacommand{apply}@{text"(simp)"} on the initial goal above. -This splitting idea generalizes from @{text"if"} to \isaindex{case}: +This splitting idea generalizes from @{text"if"} to \isaindex{case}. +Let us simplify a case analysis over lists: *}(*<*)by simp(*>*) lemma "(case xs of [] \ zs | y#ys \ y#(ys@zs)) = xs@zs"; apply(split list.split); - + txt{* @{subgoals[display,indent=0]} In contrast to @{text"if"}-expressions, the simplifier does not split @@ -396,7 +405,13 @@ [a] = [] == False \end{ttbox} -In more complicated cases, the trace can be quite lenghty, especially since +The trace lists each rule being applied, both in its general form and the +instance being used. For conditional rules, the trace lists the rule +it is trying to rewrite and gives the result of attempting to prove +each of the rule's conditions. Many other hints about the simplifier's +actions will appear. + +In more complicated cases, the trace can be quite lengthy, especially since invocations of the simplifier are often nested (e.g.\ when solving conditions of rewrite rules). Thus it is advisable to reset it: *} diff -r b28bbb153603 -r d666f11ca2d4 doc-src/TutorialI/Recdef/document/termination.tex --- a/doc-src/TutorialI/Recdef/document/termination.tex Fri May 18 16:45:55 2001 +0200 +++ b/doc-src/TutorialI/Recdef/document/termination.tex Fri May 18 17:18:43 2001 +0200 @@ -3,10 +3,10 @@ \def\isabellecontext{termination}% % \begin{isamarkuptext}% -When a function is defined via \isacommand{recdef}, Isabelle tries to prove -its termination with the help of the user-supplied measure. All of the above -examples are simple enough that Isabelle can prove automatically that the -measure of the argument goes down in each recursive call. As a result, +When a function~$f$ is defined via \isacommand{recdef}, Isabelle tries to prove +its termination with the help of the user-supplied measure. Each of the examples +above is simple enough that Isabelle can automatically prove that the +argument's measure decreases in each recursive call. As a result, $f$\isa{{\isachardot}simps} will contain the defining equations (or variants derived from them) as theorems. For example, look (via \isacommand{thm}) at \isa{sep{\isachardot}simps} and \isa{sep{\isadigit{1}}{\isachardot}simps} to see that they define diff -r b28bbb153603 -r d666f11ca2d4 doc-src/TutorialI/Recdef/termination.thy --- a/doc-src/TutorialI/Recdef/termination.thy Fri May 18 16:45:55 2001 +0200 +++ b/doc-src/TutorialI/Recdef/termination.thy Fri May 18 17:18:43 2001 +0200 @@ -3,10 +3,10 @@ (*>*) text{* -When a function is defined via \isacommand{recdef}, Isabelle tries to prove -its termination with the help of the user-supplied measure. All of the above -examples are simple enough that Isabelle can prove automatically that the -measure of the argument goes down in each recursive call. As a result, +When a function~$f$ is defined via \isacommand{recdef}, Isabelle tries to prove +its termination with the help of the user-supplied measure. Each of the examples +above is simple enough that Isabelle can automatically prove that the +argument's measure decreases in each recursive call. As a result, $f$@{text".simps"} will contain the defining equations (or variants derived from them) as theorems. For example, look (via \isacommand{thm}) at @{thm[source]sep.simps} and @{thm[source]sep1.simps} to see that they define diff -r b28bbb153603 -r d666f11ca2d4 doc-src/TutorialI/Trie/Trie.thy --- a/doc-src/TutorialI/Trie/Trie.thy Fri May 18 16:45:55 2001 +0200 +++ b/doc-src/TutorialI/Trie/Trie.thy Fri May 18 17:18:43 2001 +0200 @@ -24,7 +24,8 @@ primrec "alist(Trie ov al) = al"; text{*\noindent -Association lists come with a generic lookup function: +Association lists come with a generic lookup function. Its result +involves type @{text option} because a lookup can fail: *}; consts assoc :: "('key * 'val)list \ 'key \ 'val option"; diff -r b28bbb153603 -r d666f11ca2d4 doc-src/TutorialI/Trie/document/Trie.tex --- a/doc-src/TutorialI/Trie/document/Trie.tex Fri May 18 16:45:55 2001 +0200 +++ b/doc-src/TutorialI/Trie/document/Trie.tex Fri May 18 17:18:43 2001 +0200 @@ -23,7 +23,8 @@ \isacommand{primrec}\ {\isachardoublequote}alist{\isacharparenleft}Trie\ ov\ al{\isacharparenright}\ {\isacharequal}\ al{\isachardoublequote}% \begin{isamarkuptext}% \noindent -Association lists come with a generic lookup function:% +Association lists come with a generic lookup function. Its result +involves type \isa{option} because a lookup can fail:% \end{isamarkuptext}% \isacommand{consts}\ \ \ assoc\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}key\ {\isacharasterisk}\ {\isacharprime}val{\isacharparenright}list\ {\isasymRightarrow}\ {\isacharprime}key\ {\isasymRightarrow}\ {\isacharprime}val\ option{\isachardoublequote}\isanewline \isacommand{primrec}\ {\isachardoublequote}assoc\ {\isacharbrackleft}{\isacharbrackright}\ x\ {\isacharequal}\ None{\isachardoublequote}\isanewline diff -r b28bbb153603 -r d666f11ca2d4 doc-src/TutorialI/fp.tex --- a/doc-src/TutorialI/fp.tex Fri May 18 16:45:55 2001 +0200 +++ b/doc-src/TutorialI/fp.tex Fri May 18 17:18:43 2001 +0200 @@ -1,54 +1,4 @@ -\chapter{Functional Programming in HOL} - -Although on the surface this chapter is mainly concerned with how to write -functional programs in HOL and how to verify them, most of the constructs and -proof procedures introduced are general purpose and recur in any specification -or verification task. In fact, we really should speak of functional -\emph{modelling} rather than \emph{programming}: our primary aim is not -to write programs but to design abstract models of systems. HOL is -a specification language that goes well beyond what can be expressed as a -program. However, for the time being we concentrate on the computable. - -The dedicated functional programmer should be warned: HOL offers only -\emph{total functional programming} --- all functions in HOL must be total, -i.e.\ they must terminate for all inputs; lazy data structures are not -directly available. - -\section{An Introductory Theory} -\label{sec:intro-theory} - -Functional programming needs datatypes and functions. Both of them can be -defined in a theory with a syntax reminiscent of languages like ML or -Haskell. As an example consider the theory in figure~\ref{fig:ToyList}. -We will now examine it line by line. - -\begin{figure}[htbp] -\begin{ttbox}\makeatother -\input{ToyList2/ToyList1}\end{ttbox} -\caption{A theory of lists} -\label{fig:ToyList} -\end{figure} - -{\makeatother\input{ToyList/document/ToyList.tex}} - -The complete proof script is shown in Fig.\ts\ref{fig:ToyList-proofs}. The -concatenation of Figs.\ts\ref{fig:ToyList} and~\ref{fig:ToyList-proofs} -constitutes the complete theory \texttt{ToyList} and should reside in file -\texttt{ToyList.thy}. It is good practice to present all declarations and -definitions at the beginning of a theory to facilitate browsing. - -\begin{figure}[htbp] -\begin{ttbox}\makeatother -\input{ToyList2/ToyList2}\end{ttbox} -\caption{Proofs about lists} -\label{fig:ToyList-proofs} -\end{figure} - -\subsubsection*{Review} - -This is the end of our toy proof. It should have familiarized you with -\begin{itemize} -\item the standard theorem proving procedure: +\chapter{Functional Programming in HOL} Although on the surface this chapter is mainly concerned with how to write functional programs in HOL and how to verify them, most of the constructs and proof procedures introduced are general purpose and recur in any specification or verification task. In fact, we really should speak of functional \emph{modelling} rather than \emph{programming}: our primary aim is not to write programs but to design abstract models of systems. HOL is a specification language that goes well beyond what can be expressed as a program. However, for the time being we concentrate on the computable. The dedicated functional programmer should be warned: HOL offers only \emph{total functional programming} --- all functions in HOL must be total, i.e.\ they must terminate for all inputs; lazy data structures are not directly available. \section{An Introductory Theory} \label{sec:intro-theory} Functional programming needs datatypes and functions. Both of them can be defined in a theory with a syntax reminiscent of languages like ML or Haskell. As an example consider the theory in figure~\ref{fig:ToyList}. We will now examine it line by line. \begin{figure}[htbp] \begin{ttbox}\makeatother \input{ToyList2/ToyList1}\end{ttbox} \caption{A theory of lists} \label{fig:ToyList} \end{figure} {\makeatother\input{ToyList/document/ToyList.tex}} The complete proof script is shown in Fig.\ts\ref{fig:ToyList-proofs}. The concatenation of Figs.\ts\ref{fig:ToyList} and~\ref{fig:ToyList-proofs} constitutes the complete theory \texttt{ToyList} and should reside in file \texttt{ToyList.thy}. It is good practice to present all declarations and definitions at the beginning of a theory to facilitate browsing. \begin{figure}[htbp] \begin{ttbox}\makeatother \input{ToyList2/ToyList2}\end{ttbox} \caption{Proofs about lists} \label{fig:ToyList-proofs} \end{figure} \subsubsection*{Review} This is the end of our toy proof. It should have familiarized you with \begin{itemize} \item the standard theorem proving procedure: state a goal (lemma or theorem); proceed with proof until a separate lemma is required; prove that lemma; come back to the original goal. \item a specific procedure that works well for functional programs: @@ -374,58 +324,7 @@ {\makeatother\input{Datatype/document/Nested.tex}} -\subsection{The Limits of Nested Recursion} - -How far can we push nested recursion? By the unfolding argument above, we can -reduce nested to mutual recursion provided the nested recursion only involves -previously defined datatypes. This does not include functions: -\begin{isabelle} -\isacommand{datatype} t = C "t \isasymRightarrow\ bool" -\end{isabelle} -This declaration is a real can of worms. -In HOL it must be ruled out because it requires a type -\isa{t} such that \isa{t} and its power set \isa{t \isasymFun\ bool} have the -same cardinality --- an impossibility. For the same reason it is not possible -to allow recursion involving the type \isa{set}, which is isomorphic to -\isa{t \isasymFun\ bool}. - -Fortunately, a limited form of recursion -involving function spaces is permitted: the recursive type may occur on the -right of a function arrow, but never on the left. Hence the above can of worms -is ruled out but the following example of a potentially infinitely branching tree is -accepted: -\smallskip - -\input{Datatype/document/Fundata.tex} -\bigskip - -If you need nested recursion on the left of a function arrow, there are -alternatives to pure HOL: LCF~\cite{paulson87} is a logic where types like -\begin{isabelle} -\isacommand{datatype} lam = C "lam \isasymrightarrow\ lam" -\end{isabelle} -do indeed make sense. Note the different arrow, -\isa{\isasymrightarrow} instead of \isa{\isasymRightarrow}, -expressing the type of \emph{continuous} functions. -There is even a version of LCF on top of HOL, -called HOLCF~\cite{MuellerNvOS99}. - -\index{*primrec|)} -\index{*datatype|)} - -\subsection{Case Study: Tries} -\label{sec:Trie} - -Tries are a classic search tree data structure~\cite{Knuth3-75} for fast -indexing with strings. Figure~\ref{fig:trie} gives a graphical example of a -trie containing the words ``all'', ``an'', ``ape'', ``can'', ``car'' and -``cat''. When searching a string in a trie, the letters of the string are -examined sequentially. Each letter determines which subtrie to search next. -In this case study we model tries as a datatype, define a lookup and an -update function, and prove that they behave as expected. - -\begin{figure}[htbp] -\begin{center} +\subsection{The Limits of Nested Recursion} How far can we push nested recursion? By the unfolding argument above, we can reduce nested to mutual recursion provided the nested recursion only involves previously defined datatypes. This does not include functions: \begin{isabelle} \isacommand{datatype} t = C "t \isasymRightarrow\ bool" \end{isabelle} This declaration is a real can of worms. In HOL it must be ruled out because it requires a type \isa{t} such that \isa{t} and its power set \isa{t \isasymFun\ bool} have the same cardinality --- an impossibility. For the same reason it is not possible to allow recursion involving the type \isa{set}, which is isomorphic to \isa{t \isasymFun\ bool}. Fortunately, a limited form of recursion involving function spaces is permitted: the recursive type may occur on the right of a function arrow, but never on the left. Hence the above can of worms is ruled out but the following example of a potentially infinitely branching tree is accepted: \smallskip \input{Datatype/document/Fundata.tex} \bigskip If you need nested recursion on the left of a function arrow, there are alternatives to pure HOL\@. In the Logic for Computable Functions (LCF), types like \begin{isabelle} \isacommand{datatype} lam = C "lam \isasymrightarrow\ lam" \end{isabelle} do indeed make sense~\cite{paulson87}. Note the different arrow, \isa{\isasymrightarrow} instead of \isa{\isasymRightarrow}, expressing the type of \emph{continuous} functions. There is even a version of LCF on top of HOL, called HOLCF~\cite{MuellerNvOS99}. \index{*primrec|)} \index{*datatype|)} \subsection{Case Study: Tries} \label{sec:Trie} Tries are a classic search tree data structure~\cite{Knuth3-75} for fast indexing with strings. Figure~\ref{fig:trie} gives a graphical example of a trie containing the words ``all'', ``an'', ``ape'', ``can'', ``car'' and ``cat''. When searching a string in a trie, the letters of the string are examined sequentially. Each letter determines which subtrie to search next. In this case study we model tries as a datatype, define a lookup and an update function, and prove that they behave as expected. \begin{figure}[htbp] \begin{center} \unitlength1mm \begin{picture}(60,30) \put( 5, 0){\makebox(0,0)[b]{l}} @@ -442,58 +341,7 @@ % \put( 5,10){\makebox(0,0)[b]{l}} \put(15,10){\makebox(0,0)[b]{n}} -\put(25,10){\makebox(0,0)[b]{p}} -\put(45,10){\makebox(0,0)[b]{a}} -% -\put(14,19){\line(-3,-2){9}} -\put(15,19){\line(0,-1){5}} -\put(16,19){\line(3,-2){9}} -\put(45,19){\line(0,-1){5}} -% -\put(15,20){\makebox(0,0)[b]{a}} -\put(45,20){\makebox(0,0)[b]{c}} -% -\put(30,30){\line(-3,-2){13}} -\put(30,30){\line(3,-2){13}} -\end{picture} -\end{center} -\caption{A sample trie} -\label{fig:trie} -\end{figure} - -Proper tries associate some value with each string. Since the -information is stored only in the final node associated with the string, many -nodes do not carry any value. This distinction is modeled with the help -of the predefined datatype \isa{option} (see {\S}\ref{sec:option}). -\input{Trie/document/Trie.tex} - -\section{Total Recursive Functions} -\label{sec:recdef} -\index{*recdef|(} - -Although many total functions have a natural primitive recursive definition, -this is not always the case. Arbitrary total recursive functions can be -defined by means of \isacommand{recdef}: you can use full pattern-matching, -recursion need not involve datatypes, and termination is proved by showing -that the arguments of all recursive calls are smaller in a suitable (user -supplied) sense. In this section we restrict ourselves to measure functions; -more advanced termination proofs are discussed in {\S}\ref{sec:beyond-measure}. - -\subsection{Defining Recursive Functions} -\label{sec:recdef-examples} -\input{Recdef/document/examples.tex} - -\subsection{Proving Termination} - -\input{Recdef/document/termination.tex} - -\subsection{Simplification with Recdef} -\label{sec:recdef-simplification} - -\input{Recdef/document/simplification.tex} - -\subsection{Induction} -\index{induction!recursion|(} +\put(25,10){\makebox(0,0)[b]{p}} \put(45,10){\makebox(0,0)[b]{a}} % \put(14,19){\line(-3,-2){9}} \put(15,19){\line(0,-1){5}} \put(16,19){\line(3,-2){9}} \put(45,19){\line(0,-1){5}} % \put(15,20){\makebox(0,0)[b]{a}} \put(45,20){\makebox(0,0)[b]{c}} % \put(30,30){\line(-3,-2){13}} \put(30,30){\line(3,-2){13}} \end{picture} \end{center} \caption{A sample trie} \label{fig:trie} \end{figure} Proper tries associate some value with each string. Since the information is stored only in the final node associated with the string, many nodes do not carry any value. This distinction is modeled with the help of the predefined datatype \isa{option} (see {\S}\ref{sec:option}). \input{Trie/document/Trie.tex} \section{Total Recursive Functions} \label{sec:recdef} \index{*recdef|(} Although many total functions have a natural primitive recursive definition, this is not always the case. Arbitrary total recursive functions can be defined by means of \isacommand{recdef}: you can use full pattern-matching, recursion need not involve datatypes, and termination is proved by showing that the arguments of all recursive calls are smaller in a suitable (user supplied) sense. In this section we restrict ourselves to measure functions; more advanced termination proofs are discussed in {\S}\ref{sec:beyond-measure}. \subsection{Defining Recursive Functions} \label{sec:recdef-examples} \input{Recdef/document/examples.tex} \subsection{Proving Termination} \input{Recdef/document/termination.tex} \subsection{Simplification with Recdef} \label{sec:recdef-simplification} \input{Recdef/document/simplification.tex} \subsection{Induction} \index{induction!recursion|(} \index{recursion induction|(} \input{Recdef/document/Induction.tex}