summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

doc-src/TutorialI/Advanced/WFrec.thy

author | nipkow |

Wed Dec 13 09:39:53 2000 +0100 (2000-12-13) | |

changeset 10654 | 458068404143 |

parent 10545 | 216388848786 |

child 10795 | 9e888d60d3e5 |

permissions | -rw-r--r-- |

*** empty log message ***

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

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 \rmindex{lexicographic product} @{text"<*lex*>"}:

9 *}

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))";

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).

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

24 arbitrary well-founded relations as introduced in \S\ref{sec:Well-founded}.

25 This is called \textbf{well-founded

26 recursion}\indexbold{recursion!well-founded}. Clearly, a function definition

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

28 left-hand side of an equation and $r$ the argument of some recursive call on

29 the corresponding right-hand side, induces a well-founded relation. For a

30 systematic account of termination proofs via well-founded relations see, for

31 example, \cite{Baader-Nipkow}.

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

34 the function) by a well-founded relation on the argument type of the

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

36 constructions of well-founded relations (see \S\ref{sec:Well-founded}). For

37 example, @{term"measure f"} is always well-founded, and the lexicographic

38 product of two well-founded relations is again well-founded, which we relied

39 on when defining Ackermann's function above.

40 Of course the lexicographic product can also be interated:

41 *}

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

44 recdef contrived

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

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

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

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

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

51 text{*

52 Lexicographic products of measure functions already go a long

53 way. Furthermore you may embed some type in an

54 existing well-founded relation via the inverse image construction @{term

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

56 will never have to prove well-foundedness of any relation composed

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

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

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

60 additional lemmas.

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

63 Here is a simplistic example:

64 *}

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

67 recdef f "id(less_than)"

68 "f 0 = 0"

69 "f (Suc n) = f n"

71 text{*\noindent

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

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

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

75 We should first have proved that @{term id} preserves well-foundedness

76 *}

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

79 by simp;

81 text{*\noindent

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

83 \indexbold{*recdef_wf}

84 *}

85 (*<*)

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

87 recdef g "id(less_than)"

88 "g 0 = 0"

89 "g (Suc n) = g n"

90 (*>*)

91 (hints recdef_wf: wf_id)

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