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 +(*>*)