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