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 \ nat";  nipkow@9933  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@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 \ 'a list \ 'a list";  nipkow@9933  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@9933  42 consts last :: "'a list \ 'a";  nipkow@9933  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@9933  52 consts sep1 :: "'a \ 'a list \ 'a list";  nipkow@9933  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@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 \ 'a \ 'a list";  nipkow@8745  71 recdef sep2 "measure length"  nipkow@10362  72  "sep2 (x#y#zs) = (\a. x # a # sep2 (y#zs) a)"  nipkow@9933  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@9933  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@9792  87 set @{term"{}"}.  nipkow@8745  88 *}  nipkow@8745  89 nipkow@8745  90 (*<*)  nipkow@8745  91 end  nipkow@8745  92 (*>*)