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 ***
 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 \\ nat";  nipkow@8745  10 recdef fib "measure(\\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@8771  17 \isa{\isasymlambda{}n.$\;$n} which 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 \\ 'a list";  nipkow@8745  30 recdef sep "measure (\\(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 \\ 'a";  nipkow@8745  43 recdef last "measure (\\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 \\ 'a list";  nipkow@8745  53 recdef sep1 "measure (\\(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 \\ 'a \\ 'a list";  nipkow@8745  71 recdef sep2 "measure length"  nipkow@8745  72  "sep2 (x#y#zs) = (\\a. x # a # sep2 zs a)"  nipkow@8745  73  "sep2 xs = (\\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 \\ '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@8745  87 set \isa{\{\}}.  nipkow@8745  88 *}  nipkow@8745  89 nipkow@8745  90 (*<*)  nipkow@8745  91 end  nipkow@8745  92 (*>*)