doc-src/TutorialI/Recdef/examples.thy
 changeset 8745 13b32661dde4 child 8771 026f37a86ea7
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-src/TutorialI/Recdef/examples.thy	Wed Apr 19 11:56:31 2000 +0200
1.3 @@ -0,0 +1,92 @@
1.4 +(*<*)
1.5 +theory examples = Main:;
1.6 +(*>*)
1.7 +
1.8 +text{*
1.9 +Here is a simple example, the Fibonacci function:
1.10 +*}
1.11 +
1.12 +consts fib :: "nat \\<Rightarrow> nat";
1.13 +recdef fib "measure(\\<lambda>n. n)"
1.14 +  "fib 0 = 0"
1.15 +  "fib 1 = 1"
1.16 +  "fib (Suc(Suc x)) = fib x + fib (Suc x)";
1.17 +
1.18 +text{*\noindent
1.19 +The definition of \isa{fib} is accompanied by a \bfindex{measure function}
1.20 +\isa{\isasymlambda{}n.$\;$n} that maps the argument of \isa{fib} to a
1.21 +natural number. The requirement is that in each equation the measure of the
1.22 +argument on the left-hand side is strictly greater than the measure of the
1.23 +argument of each recursive call. In the case of \isa{fib} this is
1.24 +obviously true because the measure function is the identity and
1.25 +\isa{Suc(Suc~x)} is strictly greater than both \isa{x} and
1.26 +\isa{Suc~x}.
1.27 +
1.28 +Slightly more interesting is the insertion of a fixed element
1.29 +between any two elements of a list:
1.30 +*}
1.31 +
1.32 +consts sep :: "'a * 'a list \\<Rightarrow> 'a list";
1.33 +recdef sep "measure (\\<lambda>(a,xs). length xs)"
1.34 +  "sep(a, [])     = []"
1.35 +  "sep(a, [x])    = [x]"
1.36 +  "sep(a, x#y#zs) = x # a # sep(a,y#zs)";
1.37 +
1.38 +text{*\noindent
1.39 +This time the measure is the length of the list, which decreases with the
1.40 +recursive call; the first component of the argument tuple is irrelevant.
1.41 +
1.42 +Pattern matching need not be exhaustive:
1.43 +*}
1.44 +
1.45 +consts last :: "'a list \\<Rightarrow> 'a";
1.46 +recdef last "measure (\\<lambda>xs. length xs)"
1.47 +  "last [x]      = x"
1.48 +  "last (x#y#zs) = last (y#zs)";
1.49 +
1.50 +text{*
1.51 +Overlapping patterns are disambiguated by taking the order of equations into
1.52 +account, just as in functional programming:
1.53 +*}
1.54 +
1.55 +consts sep1 :: "'a * 'a list \\<Rightarrow> 'a list";
1.56 +recdef sep1 "measure (\\<lambda>(a,xs). length xs)"
1.57 +  "sep1(a, x#y#zs) = x # a # sep1(a,y#zs)"
1.58 +  "sep1(a, xs)     = xs";
1.59 +
1.60 +text{*\noindent
1.61 +This defines exactly the same function as \isa{sep} above, i.e.\
1.62 +\isa{sep1 = sep}.
1.63 +
1.64 +\begin{warn}
1.65 +  \isacommand{recdef} only takes the first argument of a (curried)
1.66 +  recursive function into account. This means both the termination measure
1.67 +  and pattern matching can only use that first argument. In general, you will
1.68 +  therefore have to combine several arguments into a tuple. In case only one
1.69 +  argument is relevant for termination, you can also rearrange the order of
1.70 +  arguments as in the following definition:
1.71 +\end{warn}
1.72 +*}
1.73 +consts sep2 :: "'a list \\<Rightarrow> 'a \\<Rightarrow> 'a list";
1.74 +recdef sep2 "measure length"
1.75 +  "sep2 (x#y#zs) = (\\<lambda>a. x # a # sep2 zs a)"
1.76 +  "sep2 xs       = (\\<lambda>a. xs)";
1.77 +
1.78 +text{*
1.79 +Because of its pattern-matching syntax, \isacommand{recdef} is also useful
1.80 +for the definition of non-recursive functions:
1.81 +*}
1.82 +
1.83 +consts swap12 :: "'a list \\<Rightarrow> 'a list";
1.84 +recdef swap12 "{}"
1.85 +  "swap12 (x#y#zs) = y#x#zs"
1.86 +  "swap12 zs       = zs";
1.87 +
1.88 +text{*\noindent
1.89 +In the non-recursive case the termination measure degenerates to the empty
1.90 +set \isa{\{\}}.
1.91 +*}
1.92 +
1.93 +(*<*)
1.94 +end
1.95 +(*>*)