24 arbitrary \emph{wellfounded relations}, i.e.\ \emph{wellfounded |
24 arbitrary \emph{wellfounded relations}, i.e.\ \emph{wellfounded |
25 recursion}\indexbold{recursion!wellfounded}\index{wellfounded |
25 recursion}\indexbold{recursion!wellfounded}\index{wellfounded |
26 recursion|see{recursion, wellfounded}}. A relation $<$ is |
26 recursion|see{recursion, wellfounded}}. A relation $<$ is |
27 \bfindex{wellfounded} if it has no infinite descending chain $\cdots < |
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 |
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 |
29 of all pairs $(r,l)$, where $l$ is the argument on the left-hand side |
30 and $r$ the argument of some recursive call on the corresponding |
30 of an equation and $r$ the argument of some recursive call on the |
31 right-hand side, induces a wellfounded relation. For a systematic |
31 corresponding right-hand side, induces a wellfounded relation. For a |
32 account of termination proofs via wellfounded relations see, for |
32 systematic account of termination proofs via wellfounded relations |
33 example, \cite{Baader-Nipkow}. |
33 see, for example, \cite{Baader-Nipkow}. The HOL library formalizes |
|
34 some of the theory of wellfounded relations. For example |
|
35 @{prop"wf r"}\index{*wf|bold} means that relation @{term[show_types]"r::('a*'a)set"} is |
|
36 wellfounded. |
34 |
37 |
35 Each \isacommand{recdef} definition should be accompanied (after the |
38 Each \isacommand{recdef} definition should be accompanied (after the |
36 name of the function) by a wellfounded relation on the argument type |
39 name of the function) by a wellfounded relation on the argument type |
37 of the function. For example, @{term measure} is defined by |
40 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}"} |
41 @{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. |
42 and it has been proved that @{term"measure f"} is always wellfounded. |
40 |
43 |
41 In addition to @{term measure}, the library provides |
44 In addition to @{term measure}, the library provides |
42 a number of further constructions for obtaining wellfounded relations. |
45 a number of further constructions for obtaining wellfounded relations. |
|
46 Above we have already met @{text"<*lex*>"} of type |
|
47 @{typ[display,source]"('a \<times> 'a)set \<Rightarrow> ('b \<times> 'b)set \<Rightarrow> (('a \<times> 'b) \<times> ('a \<times> 'b))set"} |
|
48 Of course the lexicographic product can also be interated, as in the following |
|
49 function definition: |
|
50 *} |
43 |
51 |
44 wf proof auto if stndard constructions. |
52 consts contrived :: "nat \<times> nat \<times> nat \<Rightarrow> nat" |
|
53 recdef contrived |
|
54 "measure(\<lambda>i. i) <*lex*> measure(\<lambda>j. j) <*lex*> measure(\<lambda>k. k)" |
|
55 "contrived(i,j,Suc k) = contrived(i,j,k)" |
|
56 "contrived(i,Suc j,0) = contrived(i,j,j)" |
|
57 "contrived(Suc i,0,0) = contrived(i,i,i)" |
|
58 "contrived(0,0,0) = 0" |
|
59 |
|
60 text{* |
|
61 Lexicographic products of measure functions already go a long way. A |
|
62 further useful construction is the embedding of some type in an |
|
63 existing wellfounded relation via the inverse image of a function: |
|
64 @{thm[display,show_types]inv_image_def[no_vars]} |
|
65 \begin{sloppypar} |
|
66 \noindent |
|
67 For example, @{term measure} is actually defined as @{term"inv_mage less_than"}, where |
|
68 @{term less_than} of type @{typ"(nat \<times> nat)set"} is the less-than relation on type @{typ nat} |
|
69 (as opposed to @{term"op <"}, which is of type @{typ"nat \<Rightarrow> nat \<Rightarrow> bool"}). |
|
70 \end{sloppypar} |
|
71 |
|
72 %Finally there is also {finite_psubset} the proper subset relation on finite sets |
|
73 |
|
74 All the above constructions are known to \isacommand{recdef}. Thus you |
|
75 will never have to prove wellfoundedness of any relation composed |
|
76 solely of these building blocks. But of course the proof of |
|
77 termination of your function definition, i.e.\ that the arguments |
|
78 decrease with every recursive call, may still require you to provide |
|
79 additional lemmas. |
|
80 |
|
81 It is also possible to use your own wellfounded relations with \isacommand{recdef}. |
|
82 Here is a simplistic example: |
45 *} |
83 *} |
|
84 |
|
85 consts f :: "nat \<Rightarrow> nat" |
|
86 recdef f "id(less_than)" |
|
87 "f 0 = 0" |
|
88 "f (Suc n) = f n" |
|
89 |
|
90 text{* |
|
91 Since \isacommand{recdef} is not prepared for @{term id}, the identity |
|
92 function, this leads to the complaint that it could not prove |
|
93 @{prop"wf (id less_than)"}, the wellfoundedness of @{term"id |
|
94 less_than"}. We should first have proved that @{term id} preserves wellfoundedness |
|
95 *} |
|
96 |
|
97 lemma wf_id: "wf r \<Longrightarrow> wf(id r)" |
|
98 by simp; |
|
99 |
|
100 text{*\noindent |
|
101 and should have added the following hint to our above definition: |
|
102 *} |
|
103 (*<*) |
|
104 consts g :: "nat \<Rightarrow> nat" |
|
105 recdef g "id(less_than)" |
|
106 "g 0 = 0" |
|
107 "g (Suc n) = g n" |
|
108 (*>*) |
|
109 (hints recdef_wf add: wf_id) |
46 (*<*)end(*>*) |
110 (*<*)end(*>*) |