doc-src/TutorialI/Recdef/examples.thy
 author nipkow Tue Sep 12 15:43:15 2000 +0200 (2000-09-12) changeset 9933 9feb1e0c4cb3 parent 9792 bbefb6ce5cb2 child 10362 c6b197ccf1f1 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 @{term"fib"} is accompanied by a \bfindex{measure function}

    17 @{term"%n. n"} which maps the argument of @{term"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 @{term"fib"} this is

    21 obviously true because the measure function is the identity and

    22 @{term"Suc(Suc x)"} is strictly greater than both @{term"x"} and

    23 @{term"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 \<times> '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 \<times> '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 @{term"sep"} above, i.e.\

    59 @{prop"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 @{term"{}"}.

    88 *}

    89

    90 (*<*)

    91 end

    92 (*>*)