--- 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
*}
--- 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)
--- 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
--- 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}%
--- 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
--- 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
--- 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}%
--- 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 [] \<Rightarrow> zs | y#ys \<Rightarrow> 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:
*}
--- 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
--- 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
--- 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 \<Rightarrow> 'key \<Rightarrow> 'val option";
--- 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
--- 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}