(*<*)

theory examples = Main:;

(*>*)

text{*

Here is a simple example, the Fibonacci function:

*}

consts fib :: "nat \\<Rightarrow> nat";

recdef fib "measure(\\<lambda>n. n)"

  "fib 0 = 0"

  "fib 1 = 1"

  "fib (Suc(Suc x)) = fib x + fib (Suc x)";

text{*\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:

*}

consts sep :: "'a * 'a list \\<Rightarrow> 'a list";

recdef sep "measure (\\<lambda>(a,xs). length xs)"

  "sep(a, [])     = []"

  "sep(a, [x])    = [x]"

  "sep(a, x#y#zs) = x # a # sep(a,y#zs)";

text{*\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:

*}

consts last :: "'a list \\<Rightarrow> 'a";

recdef last "measure (\\<lambda>xs. length xs)"

  "last [x]      = x"

  "last (x#y#zs) = last (y#zs)";

text{*

Overlapping patterns are disambiguated by taking the order of equations into

account, just as in functional programming:

*}

consts sep1 :: "'a * 'a list \\<Rightarrow> 'a list";

recdef sep1 "measure (\\<lambda>(a,xs). length xs)"

  "sep1(a, x#y#zs) = x # a # sep1(a,y#zs)"

  "sep1(a, xs)     = xs";

text{*\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}

*}

consts sep2 :: "'a list \\<Rightarrow> 'a \\<Rightarrow> 'a list";

recdef sep2 "measure length"

  "sep2 (x#y#zs) = (\\<lambda>a. x # a # sep2 zs a)"

  "sep2 xs       = (\\<lambda>a. xs)";

text{*

Because of its pattern-matching syntax, \isacommand{recdef} is also useful

for the definition of non-recursive functions:

*}

consts swap12 :: "'a list \\<Rightarrow> 'a list";

recdef swap12 "{}"

  "swap12 (x#y#zs) = y#x#zs"

  "swap12 zs       = zs";

text{*\noindent

For non-recursive functions the termination measure degenerates to the empty

set \isa{\{\}}.

*}

(*<*)

end

(*>*)