doc-src/TutorialI/Recdef/examples.thy
author nipkow
Tue Oct 31 08:53:12 2000 +0100 (2000-10-31)
changeset 10362 c6b197ccf1f1
parent 9933 9feb1e0c4cb3
child 10654 458068404143
permissions -rw-r--r--
*** empty log message ***
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@9933
     9
consts fib :: "nat \<Rightarrow> nat";
nipkow@9933
    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@9792
    16
The definition of @{term"fib"} is accompanied by a \bfindex{measure function}
nipkow@9792
    17
@{term"%n. n"} which maps the argument of @{term"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@9792
    20
argument of each recursive call. In the case of @{term"fib"} this is
nipkow@8745
    21
obviously true because the measure function is the identity and
nipkow@9792
    22
@{term"Suc(Suc x)"} is strictly greater than both @{term"x"} and
nipkow@9541
    23
@{term"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@9933
    29
consts sep :: "'a \<times> 'a list \<Rightarrow> 'a list";
nipkow@9933
    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@9933
    42
consts last :: "'a list \<Rightarrow> 'a";
nipkow@9933
    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@9933
    52
consts sep1 :: "'a \<times> 'a list \<Rightarrow> 'a list";
nipkow@9933
    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@9792
    58
This defines exactly the same function as @{term"sep"} above, i.e.\
nipkow@9792
    59
@{prop"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@9933
    70
consts sep2 :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list";
nipkow@8745
    71
recdef sep2 "measure length"
nipkow@10362
    72
  "sep2 (x#y#zs) = (\<lambda>a. x # a # sep2 (y#zs) a)"
nipkow@9933
    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@9933
    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@8771
    86
For non-recursive functions the termination measure degenerates to the empty
nipkow@9792
    87
set @{term"{}"}.
nipkow@8745
    88
*}
nipkow@8745
    89
nipkow@8745
    90
(*<*)
nipkow@8745
    91
end
nipkow@8745
    92
(*>*)