1 (*<*) |
|
2 theory "termination" imports examples begin |
|
3 (*>*) |
|
4 |
|
5 text{* |
|
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 |
|
14 simplification rules. |
|
15 |
|
16 Isabelle may fail to prove the termination condition for some |
|
17 recursive call. Let us try to define Quicksort:*} |
|
18 |
|
19 consts qs :: "nat list \<Rightarrow> nat list" |
|
20 recdef(*<*)(permissive)(*>*) qs "measure length" |
|
21 "qs [] = []" |
|
22 "qs(x#xs) = qs(filter (\<lambda>y. y\<le>x) xs) @ [x] @ qs(filter (\<lambda>y. x<y) xs)" |
|
23 |
|
24 text{*\noindent where @{term filter} is predefined and @{term"filter P xs"} |
|
25 is the list of elements of @{term xs} satisfying @{term P}. |
|
26 This definition of @{term qs} fails, and Isabelle prints an error message |
|
27 showing you what it was unable to prove: |
|
28 @{text[display]"length (filter ... xs) < Suc (length xs)"} |
|
29 We can either prove this as a separate lemma, or try to figure out which |
|
30 existing lemmas may help. We opt for the second alternative. The theory of |
|
31 lists contains the simplification rule @{thm length_filter_le[no_vars]}, |
|
32 which is what we need, provided we turn \mbox{@{text"< Suc"}} |
|
33 into |
|
34 @{text"\<le>"} so that the rule applies. Lemma |
|
35 @{thm[source]less_Suc_eq_le} does just that: @{thm less_Suc_eq_le[no_vars]}. |
|
36 |
|
37 Now we retry the above definition but supply the lemma(s) just found (or |
|
38 proved). Because \isacommand{recdef}'s termination prover involves |
|
39 simplification, we include in our second attempt a hint: the |
|
40 \attrdx{recdef_simp} attribute says to use @{thm[source]less_Suc_eq_le} as a |
|
41 simplification rule.\cmmdx{hints} *} |
|
42 |
|
43 (*<*)global consts qs :: "nat list \<Rightarrow> nat list" (*>*) |
|
44 recdef qs "measure length" |
|
45 "qs [] = []" |
|
46 "qs(x#xs) = qs(filter (\<lambda>y. y\<le>x) xs) @ [x] @ qs(filter (\<lambda>y. x<y) xs)" |
|
47 (hints recdef_simp: less_Suc_eq_le) |
|
48 (*<*)local(*>*) |
|
49 text{*\noindent |
|
50 This time everything works fine. Now @{thm[source]qs.simps} contains precisely |
|
51 the stated recursion equations for @{text qs} and they have become |
|
52 simplification rules. |
|
53 Thus we can automatically prove results such as this one: |
|
54 *} |
|
55 |
|
56 theorem "qs[2,3,0] = qs[3,0,2]" |
|
57 apply(simp) |
|
58 done |
|
59 |
|
60 text{*\noindent |
|
61 More exciting theorems require induction, which is discussed below. |
|
62 |
|
63 If the termination proof requires a lemma that is of general use, you can |
|
64 turn it permanently into a simplification rule, in which case the above |
|
65 \isacommand{hint} is not necessary. But in the case of |
|
66 @{thm[source]less_Suc_eq_le} this would be of dubious value. |
|
67 *} |
|
68 (*<*) |
|
69 end |
|
70 (*>*) |
|