nipkow@10187

1 
(*<*)theory WFrec = Main:(*>*)

nipkow@10187

2 

nipkow@10187

3 
text{*\noindent

nipkow@10187

4 
So far, all recursive definitions where shown to terminate via measure

nipkow@10187

5 
functions. Sometimes this can be quite inconvenient or even

nipkow@10187

6 
impossible. Fortunately, \isacommand{recdef} supports much more

nipkow@10187

7 
general definitions. For example, termination of Ackermann's function

nipkow@10654

8 
can be shown by means of the \rmindex{lexicographic product} @{text"<*lex*>"}:

nipkow@10187

9 
*}

nipkow@10187

10 

nipkow@10187

11 
consts ack :: "nat\<times>nat \<Rightarrow> nat";

nipkow@10187

12 
recdef ack "measure(\<lambda>m. m) <*lex*> measure(\<lambda>n. n)"

nipkow@10187

13 
"ack(0,n) = Suc n"

nipkow@10187

14 
"ack(Suc m,0) = ack(m, 1)"

nipkow@10187

15 
"ack(Suc m,Suc n) = ack(m,ack(Suc m,n))";

nipkow@10187

16 

nipkow@10187

17 
text{*\noindent

nipkow@10187

18 
The lexicographic product decreases if either its first component

nipkow@10187

19 
decreases (as in the second equation and in the outer call in the

nipkow@10187

20 
third equation) or its first component stays the same and the second

nipkow@10187

21 
component decreases (as in the inner call in the third equation).

nipkow@10187

22 

nipkow@10187

23 
In general, \isacommand{recdef} supports termination proofs based on

nipkow@10396

24 
arbitrary wellfounded relations as introduced in \S\ref{sec:Wellfounded}.

nipkow@10396

25 
This is called \textbf{wellfounded

nipkow@10545

26 
recursion}\indexbold{recursion!wellfounded}. Clearly, a function definition

nipkow@10545

27 
is total iff the set of all pairs $(r,l)$, where $l$ is the argument on the

nipkow@10396

28 
lefthand side of an equation and $r$ the argument of some recursive call on

nipkow@10396

29 
the corresponding righthand side, induces a wellfounded relation. For a

nipkow@10396

30 
systematic account of termination proofs via wellfounded relations see, for

nipkow@10396

31 
example, \cite{BaaderNipkow}.

nipkow@10187

32 

nipkow@10396

33 
Each \isacommand{recdef} definition should be accompanied (after the name of

nipkow@10396

34 
the function) by a wellfounded relation on the argument type of the

nipkow@10396

35 
function. The HOL library formalizes some of the most important

nipkow@10396

36 
constructions of wellfounded relations (see \S\ref{sec:Wellfounded}). For

nipkow@10396

37 
example, @{term"measure f"} is always wellfounded, and the lexicographic

nipkow@10396

38 
product of two wellfounded relations is again wellfounded, which we relied

nipkow@10396

39 
on when defining Ackermann's function above.

nipkow@10396

40 
Of course the lexicographic product can also be interated:

nipkow@10189

41 
*}

nipkow@10187

42 

nipkow@10189

43 
consts contrived :: "nat \<times> nat \<times> nat \<Rightarrow> nat"

nipkow@10189

44 
recdef contrived

nipkow@10189

45 
"measure(\<lambda>i. i) <*lex*> measure(\<lambda>j. j) <*lex*> measure(\<lambda>k. k)"

nipkow@10189

46 
"contrived(i,j,Suc k) = contrived(i,j,k)"

nipkow@10189

47 
"contrived(i,Suc j,0) = contrived(i,j,j)"

nipkow@10189

48 
"contrived(Suc i,0,0) = contrived(i,i,i)"

nipkow@10189

49 
"contrived(0,0,0) = 0"

nipkow@10189

50 

nipkow@10189

51 
text{*

nipkow@10396

52 
Lexicographic products of measure functions already go a long

nipkow@10522

53 
way. Furthermore you may embed some type in an

nipkow@10396

54 
existing wellfounded relation via the inverse image construction @{term

nipkow@10396

55 
inv_image}. All these constructions are known to \isacommand{recdef}. Thus you

paulson@10241

56 
will never have to prove wellfoundedness of any relation composed

nipkow@10189

57 
solely of these building blocks. But of course the proof of

nipkow@10189

58 
termination of your function definition, i.e.\ that the arguments

nipkow@10189

59 
decrease with every recursive call, may still require you to provide

nipkow@10189

60 
additional lemmas.

nipkow@10189

61 

paulson@10241

62 
It is also possible to use your own wellfounded relations with \isacommand{recdef}.

nipkow@10189

63 
Here is a simplistic example:

nipkow@10187

64 
*}

nipkow@10189

65 

nipkow@10189

66 
consts f :: "nat \<Rightarrow> nat"

nipkow@10189

67 
recdef f "id(less_than)"

nipkow@10189

68 
"f 0 = 0"

nipkow@10189

69 
"f (Suc n) = f n"

nipkow@10189

70 

nipkow@10396

71 
text{*\noindent

nipkow@10189

72 
Since \isacommand{recdef} is not prepared for @{term id}, the identity

nipkow@10189

73 
function, this leads to the complaint that it could not prove

nipkow@10396

74 
@{prop"wf (id less_than)"}.

nipkow@10396

75 
We should first have proved that @{term id} preserves wellfoundedness

nipkow@10189

76 
*}

nipkow@10189

77 

nipkow@10189

78 
lemma wf_id: "wf r \<Longrightarrow> wf(id r)"

nipkow@10189

79 
by simp;

nipkow@10189

80 

nipkow@10189

81 
text{*\noindent

nipkow@10396

82 
and should have appended the following hint to our above definition:

nipkow@10654

83 
\indexbold{*recdef_wf}

nipkow@10189

84 
*}

nipkow@10189

85 
(*<*)

nipkow@10189

86 
consts g :: "nat \<Rightarrow> nat"

nipkow@10189

87 
recdef g "id(less_than)"

nipkow@10189

88 
"g 0 = 0"

nipkow@10189

89 
"g (Suc n) = g n"

nipkow@10189

90 
(*>*)

nipkow@10654

91 
(hints recdef_wf: wf_id)

nipkow@10396

92 
(*<*)end(*>*)
