equal
deleted
inserted
replaced
12 "fib 1 = 1" |
12 "fib 1 = 1" |
13 "fib (Suc(Suc x)) = fib x + fib (Suc x)"; |
13 "fib (Suc(Suc x)) = fib x + fib (Suc x)"; |
14 |
14 |
15 text{*\noindent |
15 text{*\noindent |
16 The definition of \isa{fib} is accompanied by a \bfindex{measure function} |
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 |
17 \isa{\isasymlambda{}n.$\;$n} which maps the argument of \isa{fib} to a |
18 natural number. The requirement is that in each equation the measure of the |
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 |
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 |
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 |
21 obviously true because the measure function is the identity and |
22 \isa{Suc(Suc~x)} is strictly greater than both \isa{x} and |
22 \isa{Suc(Suc~x)} is strictly greater than both \isa{x} and |
81 recdef swap12 "{}" |
81 recdef swap12 "{}" |
82 "swap12 (x#y#zs) = y#x#zs" |
82 "swap12 (x#y#zs) = y#x#zs" |
83 "swap12 zs = zs"; |
83 "swap12 zs = zs"; |
84 |
84 |
85 text{*\noindent |
85 text{*\noindent |
86 In the non-recursive case the termination measure degenerates to the empty |
86 For non-recursive functions the termination measure degenerates to the empty |
87 set \isa{\{\}}. |
87 set \isa{\{\}}. |
88 *} |
88 *} |
89 |
89 |
90 (*<*) |
90 (*<*) |
91 end |
91 end |