doc-src/TutorialI/Recdef/document/examples.tex

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Recdef/document/examples.tex	Wed Apr 19 12:59:38 2000 +0200
@@ -0,0 +1,80 @@
+\begin{isabelle}%
+%
+\begin{isamarkuptext}%
+Here is a simple example, the Fibonacci function:%
+\end{isamarkuptext}%
+\isacommand{consts}~fib~::~{"}nat~{\isasymRightarrow}~nat{"}\isanewline
+\isacommand{recdef}~fib~{"}measure({\isasymlambda}n.~n){"}\isanewline
+~~{"}fib~0~=~0{"}\isanewline
+~~{"}fib~1~=~1{"}\isanewline
+~~{"}fib~(Suc(Suc~x))~=~fib~x~+~fib~(Suc~x){"}%
+\begin{isamarkuptext}%
+\noindent
+The definition of \isa{fib} is accompanied by a \bfindex{measure function}
+\isa{\isasymlambda{}n.$\;$n} that maps the argument of \isa{fib} to a
+natural number. The requirement is that in each equation the measure of the
+argument on the left-hand side is strictly greater than the measure of the
+argument of each recursive call. In the case of \isa{fib} this is
+obviously true because the measure function is the identity and
+\isa{Suc(Suc~x)} is strictly greater than both \isa{x} and
+\isa{Suc~x}.
+
+Slightly more interesting is the insertion of a fixed element
+between any two elements of a list:%
+\end{isamarkuptext}%
+\isacommand{consts}~sep~::~{"}'a~*~'a~list~{\isasymRightarrow}~'a~list{"}\isanewline
+\isacommand{recdef}~sep~{"}measure~({\isasymlambda}(a,xs).~length~xs){"}\isanewline
+~~{"}sep(a,~[])~~~~~=~[]{"}\isanewline
+~~{"}sep(a,~[x])~~~~=~[x]{"}\isanewline
+~~{"}sep(a,~x\#y\#zs)~=~x~\#~a~\#~sep(a,y\#zs){"}%
+\begin{isamarkuptext}%
+\noindent
+This time the measure is the length of the list, which decreases with the
+recursive call; the first component of the argument tuple is irrelevant.
+
+Pattern matching need not be exhaustive:%
+\end{isamarkuptext}%
+\isacommand{consts}~last~::~{"}'a~list~{\isasymRightarrow}~'a{"}\isanewline
+\isacommand{recdef}~last~{"}measure~({\isasymlambda}xs.~length~xs){"}\isanewline
+~~{"}last~[x]~~~~~~=~x{"}\isanewline
+~~{"}last~(x\#y\#zs)~=~last~(y\#zs){"}%
+\begin{isamarkuptext}%
+Overlapping patterns are disambiguated by taking the order of equations into
+account, just as in functional programming:%
+\end{isamarkuptext}%
+\isacommand{consts}~sep1~::~{"}'a~*~'a~list~{\isasymRightarrow}~'a~list{"}\isanewline
+\isacommand{recdef}~sep1~{"}measure~({\isasymlambda}(a,xs).~length~xs){"}\isanewline
+~~{"}sep1(a,~x\#y\#zs)~=~x~\#~a~\#~sep1(a,y\#zs){"}\isanewline
+~~{"}sep1(a,~xs)~~~~~=~xs{"}%
+\begin{isamarkuptext}%
+\noindent
+This defines exactly the same function as \isa{sep} above, i.e.\
+\isa{sep1 = sep}.
+
+\begin{warn}
+  \isacommand{recdef} only takes the first argument of a (curried)
+  recursive function into account. This means both the termination measure
+  and pattern matching can only use that first argument. In general, you will
+  therefore have to combine several arguments into a tuple. In case only one
+  argument is relevant for termination, you can also rearrange the order of
+  arguments as in the following definition:
+\end{warn}%
+\end{isamarkuptext}%
+\isacommand{consts}~sep2~::~{"}'a~list~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a~list{"}\isanewline
+\isacommand{recdef}~sep2~{"}measure~length{"}\isanewline
+~~{"}sep2~(x\#y\#zs)~=~({\isasymlambda}a.~x~\#~a~\#~sep2~zs~a){"}\isanewline
+~~{"}sep2~xs~~~~~~~=~({\isasymlambda}a.~xs){"}%
+\begin{isamarkuptext}%
+Because of its pattern-matching syntax, \isacommand{recdef} is also useful
+for the definition of non-recursive functions:%
+\end{isamarkuptext}%
+\isacommand{consts}~swap12~::~{"}'a~list~{\isasymRightarrow}~'a~list{"}\isanewline
+\isacommand{recdef}~swap12~{"}{\isabraceleft}{\isabraceright}{"}\isanewline
+~~{"}swap12~(x\#y\#zs)~=~y\#x\#zs{"}\isanewline
+~~{"}swap12~zs~~~~~~~=~zs{"}%
+\begin{isamarkuptext}%
+\noindent
+In the non-recursive case the termination measure degenerates to the empty
+set \isa{\{\}}.%
+\end{isamarkuptext}%
+\end{isabelle}%