3 \def\isabellecontext{WFrec}%
8 So far, all recursive definitions were shown to terminate via measure
9 functions. Sometimes this can be inconvenient or
10 impossible. Fortunately, \isacommand{recdef} supports much more
11 general definitions. For example, termination of Ackermann's function
12 can be shown by means of the \rmindex{lexicographic product} \isa{{\isacharless}{\isacharasterisk}lex{\isacharasterisk}{\isachargreater}}:%
15 \isacommand{consts}\ ack\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
17 \isacommand{recdef}\ ack\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}m{\isachardot}\ m{\isacharparenright}\ {\isacharless}{\isacharasterisk}lex{\isacharasterisk}{\isachargreater}\ measure{\isacharparenleft}{\isasymlambda}n{\isachardot}\ n{\isacharparenright}{\isachardoublequote}\isanewline
18 \ \ {\isachardoublequote}ack{\isacharparenleft}{\isadigit{0}}{\isacharcomma}n{\isacharparenright}\ \ \ \ \ \ \ \ \ {\isacharequal}\ Suc\ n{\isachardoublequote}\isanewline
19 \ \ {\isachardoublequote}ack{\isacharparenleft}Suc\ m{\isacharcomma}{\isadigit{0}}{\isacharparenright}\ \ \ \ \ {\isacharequal}\ ack{\isacharparenleft}m{\isacharcomma}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline
20 \ \ {\isachardoublequote}ack{\isacharparenleft}Suc\ m{\isacharcomma}Suc\ n{\isacharparenright}\ {\isacharequal}\ ack{\isacharparenleft}m{\isacharcomma}ack{\isacharparenleft}Suc\ m{\isacharcomma}n{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
22 \begin{isamarkuptext}%
24 The lexicographic product decreases if either its first component
25 decreases (as in the second equation and in the outer call in the
26 third equation) or its first component stays the same and the second
27 component decreases (as in the inner call in the third equation).
29 In general, \isacommand{recdef} supports termination proofs based on
30 arbitrary well-founded relations as introduced in \S\ref{sec:Well-founded}.
31 This is called \textbf{well-founded
32 recursion}\indexbold{recursion!well-founded}. A function definition
33 is total if and only if the set of
34 all pairs $(r,l)$, where $l$ is the argument on the
35 left-hand side of an equation and $r$ the argument of some recursive call on
36 the corresponding right-hand side, induces a well-founded relation. For a
37 systematic account of termination proofs via well-founded relations see, for
38 example, Baader and Nipkow~\cite{Baader-Nipkow}.
40 Each \isacommand{recdef} definition should be accompanied (after the function's
41 name) by a well-founded relation on the function's argument type.
42 Isabelle/HOL formalizes some of the most important
43 constructions of well-founded relations (see \S\ref{sec:Well-founded}). For
44 example, \isa{measure\ f} is always well-founded. The lexicographic
45 product of two well-founded relations is again well-founded, which we relied
46 on when defining Ackermann's function above.
47 Of course the lexicographic product can also be iterated:%
50 \isacommand{consts}\ contrived\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymtimes}\ nat\ {\isasymtimes}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
52 \isacommand{recdef}\ contrived\isanewline
53 \ \ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}i{\isachardot}\ i{\isacharparenright}\ {\isacharless}{\isacharasterisk}lex{\isacharasterisk}{\isachargreater}\ measure{\isacharparenleft}{\isasymlambda}j{\isachardot}\ j{\isacharparenright}\ {\isacharless}{\isacharasterisk}lex{\isacharasterisk}{\isachargreater}\ measure{\isacharparenleft}{\isasymlambda}k{\isachardot}\ k{\isacharparenright}{\isachardoublequote}\isanewline
54 {\isachardoublequote}contrived{\isacharparenleft}i{\isacharcomma}j{\isacharcomma}Suc\ k{\isacharparenright}\ {\isacharequal}\ contrived{\isacharparenleft}i{\isacharcomma}j{\isacharcomma}k{\isacharparenright}{\isachardoublequote}\isanewline
55 {\isachardoublequote}contrived{\isacharparenleft}i{\isacharcomma}Suc\ j{\isacharcomma}{\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ contrived{\isacharparenleft}i{\isacharcomma}j{\isacharcomma}j{\isacharparenright}{\isachardoublequote}\isanewline
56 {\isachardoublequote}contrived{\isacharparenleft}Suc\ i{\isacharcomma}{\isadigit{0}}{\isacharcomma}{\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ contrived{\isacharparenleft}i{\isacharcomma}i{\isacharcomma}i{\isacharparenright}{\isachardoublequote}\isanewline
57 {\isachardoublequote}contrived{\isacharparenleft}{\isadigit{0}}{\isacharcomma}{\isadigit{0}}{\isacharcomma}{\isadigit{0}}{\isacharparenright}\ \ \ \ \ {\isacharequal}\ {\isadigit{0}}{\isachardoublequote}\isamarkupfalse%
59 \begin{isamarkuptext}%
60 Lexicographic products of measure functions already go a long
61 way. Furthermore, you may embed a type in an
62 existing well-founded relation via the inverse image construction \isa{inv{\isacharunderscore}image}. All these constructions are known to \isacommand{recdef}. Thus you
63 will never have to prove well-foundedness of any relation composed
64 solely of these building blocks. But of course the proof of
65 termination of your function definition --- that the arguments
66 decrease with every recursive call --- may still require you to provide
69 It is also possible to use your own well-founded relations with
70 \isacommand{recdef}. For example, the greater-than relation can be made
71 well-founded by cutting it off at a certain point. Here is an example
72 of a recursive function that calls itself with increasing values up to ten:%
75 \isacommand{consts}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
77 \isacommand{recdef}\ f\ {\isachardoublequote}{\isacharbraceleft}{\isacharparenleft}i{\isacharcomma}j{\isacharparenright}{\isachardot}\ j{\isacharless}i\ {\isasymand}\ i\ {\isasymle}\ {\isacharparenleft}{\isadigit{1}}{\isadigit{0}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharbraceright}{\isachardoublequote}\isanewline
78 {\isachardoublequote}f\ i\ {\isacharequal}\ {\isacharparenleft}if\ {\isadigit{1}}{\isadigit{0}}\ {\isasymle}\ i\ then\ {\isadigit{0}}\ else\ i\ {\isacharasterisk}\ f{\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
80 \begin{isamarkuptext}%
82 Since \isacommand{recdef} is not prepared for the relation supplied above,
83 Isabelle rejects the definition. We should first have proved that
84 our relation was well-founded:%
87 \isacommand{lemma}\ wf{\isacharunderscore}greater{\isacharcolon}\ {\isachardoublequote}wf\ {\isacharbraceleft}{\isacharparenleft}i{\isacharcomma}j{\isacharparenright}{\isachardot}\ j{\isacharless}i\ {\isasymand}\ i\ {\isasymle}\ {\isacharparenleft}N{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharbraceright}{\isachardoublequote}\isamarkupfalse%
91 The proof is by showing that our relation is a subset of another well-founded
92 relation: one given by a measure function.\index{*wf_subset (theorem)}%
95 \isacommand{apply}\ {\isacharparenleft}rule\ wf{\isacharunderscore}subset\ {\isacharbrackleft}of\ {\isachardoublequote}measure\ {\isacharparenleft}{\isasymlambda}k{\isacharcolon}{\isacharcolon}nat{\isachardot}\ N{\isacharminus}k{\isacharparenright}{\isachardoublequote}{\isacharbrackright}{\isacharcomma}\ blast{\isacharparenright}\isamarkupfalse%
99 \ {\isadigit{1}}{\isachardot}\ {\isacharbraceleft}{\isacharparenleft}i{\isacharcomma}\ j{\isacharparenright}{\isachardot}\ j\ {\isacharless}\ i\ {\isasymand}\ i\ {\isasymle}\ N{\isacharbraceright}\ {\isasymsubseteq}\ measure\ {\isacharparenleft}op\ {\isacharminus}\ N{\isacharparenright}%
103 The inclusion remains to be proved. After unfolding some definitions,
104 we are left with simple arithmetic:%
107 \isacommand{apply}\ {\isacharparenleft}clarify{\isacharcomma}\ simp\ add{\isacharcolon}\ measure{\isacharunderscore}def\ inv{\isacharunderscore}image{\isacharunderscore}def{\isacharparenright}\isamarkupfalse%
109 \begin{isamarkuptxt}%
111 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ b{\isachardot}\ {\isasymlbrakk}b\ {\isacharless}\ a{\isacharsemicolon}\ a\ {\isasymle}\ N{\isasymrbrakk}\ {\isasymLongrightarrow}\ N\ {\isacharminus}\ a\ {\isacharless}\ N\ {\isacharminus}\ b%
115 And that is dispatched automatically:%
118 \isacommand{by}\ arith\isamarkupfalse%
120 \begin{isamarkuptext}%
123 Armed with this lemma, we use the \attrdx{recdef_wf} attribute to attach a
124 crucial hint\cmmdx{hints} to our definition:%
128 {\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}wf{\isacharcolon}\ wf{\isacharunderscore}greater{\isacharparenright}\isamarkupfalse%
130 \begin{isamarkuptext}%
132 Alternatively, we could have given \isa{measure\ {\isacharparenleft}{\isasymlambda}k{\isacharcolon}{\isacharcolon}nat{\isachardot}\ {\isadigit{1}}{\isadigit{0}}{\isacharminus}k{\isacharparenright}} for the
133 well-founded relation in our \isacommand{recdef}. However, the arithmetic
134 goal in the lemma above would have arisen instead in the \isacommand{recdef}
135 termination proof, where we have less control. A tailor-made termination
136 relation makes even more sense when it can be used in several function
144 %%% TeX-master: "root"