|
1 (*<*)theory WFrec = Main:(*>*) |
|
2 |
|
3 text{*\noindent |
|
4 So far, all recursive definitions where shown to terminate via measure |
|
5 functions. Sometimes this can be quite inconvenient or even |
|
6 impossible. Fortunately, \isacommand{recdef} supports much more |
|
7 general definitions. For example, termination of Ackermann's function |
|
8 can be shown by means of the lexicographic product @{text"<*lex*>"}: |
|
9 *} |
|
10 |
|
11 consts ack :: "nat\<times>nat \<Rightarrow> nat"; |
|
12 recdef ack "measure(\<lambda>m. m) <*lex*> measure(\<lambda>n. n)" |
|
13 "ack(0,n) = Suc n" |
|
14 "ack(Suc m,0) = ack(m, 1)" |
|
15 "ack(Suc m,Suc n) = ack(m,ack(Suc m,n))"; |
|
16 |
|
17 text{*\noindent |
|
18 The lexicographic product decreases if either its first component |
|
19 decreases (as in the second equation and in the outer call in the |
|
20 third equation) or its first component stays the same and the second |
|
21 component decreases (as in the inner call in the third equation). |
|
22 |
|
23 In general, \isacommand{recdef} supports termination proofs based on |
|
24 arbitrary \emph{wellfounded relations}, i.e.\ \emph{wellfounded |
|
25 recursion}\indexbold{recursion!wellfounded}\index{wellfounded |
|
26 recursion|see{recursion, wellfounded}}. A relation $<$ is |
|
27 \bfindex{wellfounded} if it has no infinite descending chain $\cdots < |
|
28 a@2 < a@1 < a@0$. Clearly, a function definition is total iff the set |
|
29 of all pairs $(r,l)$, where $l$ is the argument on the left-hand side of an equation |
|
30 and $r$ the argument of some recursive call on the corresponding |
|
31 right-hand side, induces a wellfounded relation. For a systematic |
|
32 account of termination proofs via wellfounded relations see, for |
|
33 example, \cite{Baader-Nipkow}. |
|
34 |
|
35 Each \isacommand{recdef} definition should be accompanied (after the |
|
36 name of the function) by a wellfounded relation on the argument type |
|
37 of the function. For example, @{term measure} is defined by |
|
38 @{prop[display]"measure(f::'a \<Rightarrow> nat) \<equiv> {(y,x). f y < f x}"} |
|
39 and it has been proved that @{term"measure f"} is always wellfounded. |
|
40 |
|
41 In addition to @{term measure}, the library provides |
|
42 a number of further constructions for obtaining wellfounded relations. |
|
43 |
|
44 wf proof auto if stndard constructions. |
|
45 *} |
|
46 (*<*)end(*>*) |