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

*** empty log message ***

\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} which 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
For non-recursive functions the termination measure degenerates to the empty
set \isa{\{\}}.%
\end{isamarkuptext}%
\end{isabelle}%