doc-src/TutorialI/Recdef/examples.thy
author nipkow
Wed Apr 19 11:56:31 2000 +0200 (2000-04-19)
changeset 8745 13b32661dde4
child 8771 026f37a86ea7
permissions -rw-r--r--
I wonder which files i forgot.
nipkow@8745
     1
(*<*)
nipkow@8745
     2
theory examples = Main:;
nipkow@8745
     3
(*>*)
nipkow@8745
     4
nipkow@8745
     5
text{*
nipkow@8745
     6
Here is a simple example, the Fibonacci function:
nipkow@8745
     7
*}
nipkow@8745
     8
nipkow@8745
     9
consts fib :: "nat \\<Rightarrow> nat";
nipkow@8745
    10
recdef fib "measure(\\<lambda>n. n)"
nipkow@8745
    11
  "fib 0 = 0"
nipkow@8745
    12
  "fib 1 = 1"
nipkow@8745
    13
  "fib (Suc(Suc x)) = fib x + fib (Suc x)";
nipkow@8745
    14
nipkow@8745
    15
text{*\noindent
nipkow@8745
    16
The definition of \isa{fib} is accompanied by a \bfindex{measure function}
nipkow@8745
    17
\isa{\isasymlambda{}n.$\;$n} that maps the argument of \isa{fib} to a
nipkow@8745
    18
natural number. The requirement is that in each equation the measure of the
nipkow@8745
    19
argument on the left-hand side is strictly greater than the measure of the
nipkow@8745
    20
argument of each recursive call. In the case of \isa{fib} this is
nipkow@8745
    21
obviously true because the measure function is the identity and
nipkow@8745
    22
\isa{Suc(Suc~x)} is strictly greater than both \isa{x} and
nipkow@8745
    23
\isa{Suc~x}.
nipkow@8745
    24
nipkow@8745
    25
Slightly more interesting is the insertion of a fixed element
nipkow@8745
    26
between any two elements of a list:
nipkow@8745
    27
*}
nipkow@8745
    28
nipkow@8745
    29
consts sep :: "'a * 'a list \\<Rightarrow> 'a list";
nipkow@8745
    30
recdef sep "measure (\\<lambda>(a,xs). length xs)"
nipkow@8745
    31
  "sep(a, [])     = []"
nipkow@8745
    32
  "sep(a, [x])    = [x]"
nipkow@8745
    33
  "sep(a, x#y#zs) = x # a # sep(a,y#zs)";
nipkow@8745
    34
nipkow@8745
    35
text{*\noindent
nipkow@8745
    36
This time the measure is the length of the list, which decreases with the
nipkow@8745
    37
recursive call; the first component of the argument tuple is irrelevant.
nipkow@8745
    38
nipkow@8745
    39
Pattern matching need not be exhaustive:
nipkow@8745
    40
*}
nipkow@8745
    41
nipkow@8745
    42
consts last :: "'a list \\<Rightarrow> 'a";
nipkow@8745
    43
recdef last "measure (\\<lambda>xs. length xs)"
nipkow@8745
    44
  "last [x]      = x"
nipkow@8745
    45
  "last (x#y#zs) = last (y#zs)";
nipkow@8745
    46
nipkow@8745
    47
text{*
nipkow@8745
    48
Overlapping patterns are disambiguated by taking the order of equations into
nipkow@8745
    49
account, just as in functional programming:
nipkow@8745
    50
*}
nipkow@8745
    51
nipkow@8745
    52
consts sep1 :: "'a * 'a list \\<Rightarrow> 'a list";
nipkow@8745
    53
recdef sep1 "measure (\\<lambda>(a,xs). length xs)"
nipkow@8745
    54
  "sep1(a, x#y#zs) = x # a # sep1(a,y#zs)"
nipkow@8745
    55
  "sep1(a, xs)     = xs";
nipkow@8745
    56
nipkow@8745
    57
text{*\noindent
nipkow@8745
    58
This defines exactly the same function as \isa{sep} above, i.e.\
nipkow@8745
    59
\isa{sep1 = sep}.
nipkow@8745
    60
nipkow@8745
    61
\begin{warn}
nipkow@8745
    62
  \isacommand{recdef} only takes the first argument of a (curried)
nipkow@8745
    63
  recursive function into account. This means both the termination measure
nipkow@8745
    64
  and pattern matching can only use that first argument. In general, you will
nipkow@8745
    65
  therefore have to combine several arguments into a tuple. In case only one
nipkow@8745
    66
  argument is relevant for termination, you can also rearrange the order of
nipkow@8745
    67
  arguments as in the following definition:
nipkow@8745
    68
\end{warn}
nipkow@8745
    69
*}
nipkow@8745
    70
consts sep2 :: "'a list \\<Rightarrow> 'a \\<Rightarrow> 'a list";
nipkow@8745
    71
recdef sep2 "measure length"
nipkow@8745
    72
  "sep2 (x#y#zs) = (\\<lambda>a. x # a # sep2 zs a)"
nipkow@8745
    73
  "sep2 xs       = (\\<lambda>a. xs)";
nipkow@8745
    74
nipkow@8745
    75
text{*
nipkow@8745
    76
Because of its pattern-matching syntax, \isacommand{recdef} is also useful
nipkow@8745
    77
for the definition of non-recursive functions:
nipkow@8745
    78
*}
nipkow@8745
    79
nipkow@8745
    80
consts swap12 :: "'a list \\<Rightarrow> 'a list";
nipkow@8745
    81
recdef swap12 "{}"
nipkow@8745
    82
  "swap12 (x#y#zs) = y#x#zs"
nipkow@8745
    83
  "swap12 zs       = zs";
nipkow@8745
    84
nipkow@8745
    85
text{*\noindent
nipkow@8745
    86
In the non-recursive case the termination measure degenerates to the empty
nipkow@8745
    87
set \isa{\{\}}.
nipkow@8745
    88
*}
nipkow@8745
    89
nipkow@8745
    90
(*<*)
nipkow@8745
    91
end
nipkow@8745
    92
(*>*)