2 theory termination = Main:;
6 When a function is defined via \isacommand{recdef}, Isabelle tries to prove
7 its termination with the help of the user-supplied measure. All of the above
8 examples are simple enough that Isabelle can prove automatically that the
9 measure of the argument goes down in each recursive call. In that case
10 $f$.\isa{simps} contains the defining equations (or variants derived from
11 them) as theorems. For example, look (via \isacommand{thm}) at
12 \isa{sep.simps} and \isa{sep1.simps} to see that they define the same
13 function. What is more, those equations are automatically declared as
16 In general, Isabelle may not be able to prove all termination condition
17 (there is one for each recursive call) automatically. For example,
18 termination of the following artificial function
21 consts f :: "nat*nat \\<Rightarrow> nat";
22 recdef f "measure(\\<lambda>(x,y). x-y)"
23 "f(x,y) = (if x \\<le> y then x else f(x,y+1))";
26 is not proved automatically (although maybe it should be). Isabelle prints a
27 kind of error message showing you what it was unable to prove. You will then
28 have to prove it as a separate lemma before you attempt the definition
29 of your function once more. In our case the required lemma is the obvious one:
32 lemma termi_lem[simp]: "\\<not> x \\<le> y \\<Longrightarrow> x - Suc y < x - y";
35 It was not proved automatically because of the special nature of \isa{-}
36 on \isa{nat}. This requires more arithmetic than is tried by default:
42 Because \isacommand{recdef}'s the termination prover involves simplification,
43 we have declared our lemma a simplification rule. Therefore our second
44 attempt to define our function will automatically take it into account:
47 consts g :: "nat*nat \\<Rightarrow> nat";
48 recdef g "measure(\\<lambda>(x,y). x-y)"
49 "g(x,y) = (if x \\<le> y then x else g(x,y+1))";
52 This time everything works fine. Now \isa{g.simps} contains precisely the
53 stated recursion equation for \isa{g} and they are simplification
54 rules. Thus we can automatically prove
57 theorem wow: "g(1,0) = g(1,1)";
61 More exciting theorems require induction, which is discussed below.
63 Because lemma \isa{termi_lem} above was only turned into a
64 simplification rule for the sake of the termination proof, we may want to
68 lemmas [simp del] = termi_lem;
71 The attentive reader may wonder why we chose to call our function \isa{g}
72 rather than \isa{f} the second time around. The reason is that, despite
73 the failed termination proof, the definition of \isa{f} did not
74 fail (and thus we could not define it a second time). However, all theorems
75 about \isa{f}, for example \isa{f.simps}, carry as a precondition the
76 unproved termination condition. Moreover, the theorems \isa{f.simps} are
77 not simplification rules. However, this mechanism allows a delayed proof of
78 termination: instead of proving \isa{termi_lem} up front, we could prove
79 it later on and then use it to remove the preconditions from the theorems
80 about \isa{f}. In most cases this is more cumbersome than proving things
82 %FIXME, with one exception: nested recursion.
84 Although all the above examples employ measure functions, \isacommand{recdef}
85 allows arbitrary wellfounded relations. For example, termination of
86 Ackermann's function requires the lexicographic product \isa{<*lex*>}:
89 consts ack :: "nat*nat \\<Rightarrow> nat";
90 recdef ack "measure(%m. m) <*lex*> measure(%n. n)"
92 "ack(Suc m,0) = ack(m, 1)"
93 "ack(Suc m,Suc n) = ack(m,ack(Suc m,n))";
96 For details see the manual~\cite{isabelle-HOL} and the examples in the