2 theory termination = examples:
6 When a function~$f$ is defined via \isacommand{recdef}, Isabelle tries to prove
7 its termination with the help of the user-supplied measure. Each of the examples
8 above is simple enough that Isabelle can automatically prove that the
9 argument's measure decreases in each recursive call. As a result,
10 $f$@{text".simps"} will contain the defining equations (or variants derived
11 from them) as theorems. For example, look (via \isacommand{thm}) at
12 @{thm[source]sep.simps} and @{thm[source]sep1.simps} to see that they define
13 the same function. What is more, those equations are automatically declared as
16 Isabelle may fail to prove some termination conditions
17 (there is one for each recursive call). For example,
18 termination of the following artificial function
21 consts f :: "nat\<times>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. Isabelle prints a
27 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: "\<not> x \<le> y \<Longrightarrow> x - Suc y < x - y";
35 It was not proved automatically because of the special nature of subtraction
36 on @{typ"nat"}. This requires more arithmetic than is tried by default:
43 Because \isacommand{recdef}'s termination prover involves simplification,
44 we include in our second attempt a hint: the \attrdx{recdef_simp} attribute
45 says to use @{thm[source]termi_lem} as
46 a simplification rule.
49 consts g :: "nat\<times>nat \<Rightarrow> nat";
50 recdef g "measure(\<lambda>(x,y). x-y)"
51 "g(x,y) = (if x \<le> y then x else g(x,y+1))"
52 (hints recdef_simp: termi_lem)
55 This time everything works fine. Now @{thm[source]g.simps} contains precisely
56 the stated recursion equation for @{term g} and they are simplification
57 rules. Thus we can automatically prove
60 theorem "g(1,0) = g(1,1)";
65 More exciting theorems require induction, which is discussed below.
67 If the termination proof requires a new lemma that is of general use, you can
68 turn it permanently into a simplification rule, in which case the above
69 \isacommand{hint} is not necessary. But our @{thm[source]termi_lem} is not
70 sufficiently general to warrant this distinction.
72 The attentive reader may wonder why we chose to call our function @{term g}
73 rather than @{term f} the second time around. The reason is that, despite
74 the failed termination proof, the definition of @{term f} did not
75 fail, and thus we could not define it a second time. However, all theorems
76 about @{term f}, for example @{thm[source]f.simps}, carry as a precondition
77 the unproved termination condition. Moreover, the theorems
78 @{thm[source]f.simps} are not simplification rules. However, this mechanism
79 allows a delayed proof of termination: instead of proving
80 @{thm[source]termi_lem} up front, we could prove
81 it later on and then use it to remove the preconditions from the theorems
82 about @{term f}. In most cases this is more cumbersome than proving things
84 %FIXME, with one exception: nested recursion.