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 recursionsee{recursion, wellfounded}}. A relation $<$ is 
26 recursionsee{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 lefthand side of an equation 
29 of all pairs $(r,l)$, where $l$ is the argument on the lefthand 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 righthand side, induces a wellfounded relation. For a systematic 
31 corresponding righthand 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{BaaderNipkow}. 
33 see, for example, \cite{BaaderNipkow}. The HOL library formalizes 

34 some of the theory of wellfounded relations. For example 

35 @{prop"wf r"}\index{*wfbold} 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 lessthan 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(*>*) 