|
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} that 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 In the non-recursive case the termination measure degenerates to the empty |
|
87 set \isa{\{\}}. |
|
88 *} |
|
89 |
|
90 (*<*) |
|
91 end |
|
92 (*>*) |