8745
|
1 |
(*<*)
|
9792
|
2 |
theory termination = examples:
|
8745
|
3 |
(*>*)
|
|
4 |
|
|
5 |
text{*
|
11309
|
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,
|
9792
|
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
|
8745
|
14 |
simplification rules.
|
|
15 |
|
11458
|
16 |
Isabelle may fail to prove the termination condition for some
|
12489
|
17 |
recursive call. Let us try to define Quicksort:*}
|
8745
|
18 |
|
12489
|
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)"
|
8745
|
23 |
|
12489
|
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[no_vars]},
|
|
32 |
which is already
|
|
33 |
close to what we need, except that we still need to turn \mbox{@{text"< Suc"}}
|
|
34 |
into
|
|
35 |
@{text"\<le>"} for the simplification rule to apply. Lemma
|
|
36 |
@{thm[source]less_Suc_eq_le} does just that: @{thm less_Suc_eq_le[no_vars]}.
|
8745
|
37 |
|
12489
|
38 |
Now we retry the above definition but supply the lemma(s) just found (or
|
|
39 |
proved). Because \isacommand{recdef}'s termination prover involves
|
|
40 |
simplification, we include in our second attempt a hint: the
|
|
41 |
\attrdx{recdef_simp} attribute says to use @{thm[source]less_Suc_eq_le} as a
|
13111
|
42 |
simplification rule.\cmmdx{hints} *}
|
8745
|
43 |
|
12489
|
44 |
(*<*)global consts qs :: "nat list \<Rightarrow> nat list" (*>*)
|
|
45 |
recdef qs "measure length"
|
|
46 |
"qs [] = []"
|
|
47 |
"qs(x#xs) = qs(filter (\<lambda>y. y\<le>x) xs) @ [x] @ qs(filter (\<lambda>y. x<y) xs)"
|
|
48 |
(hints recdef_simp: less_Suc_eq_le)
|
|
49 |
(*<*)local(*>*)
|
|
50 |
text{*\noindent
|
|
51 |
This time everything works fine. Now @{thm[source]qs.simps} contains precisely
|
|
52 |
the stated recursion equations for @{text qs} and they have become
|
|
53 |
simplification rules.
|
|
54 |
Thus we can automatically prove results such as this one:
|
8745
|
55 |
*}
|
|
56 |
|
12489
|
57 |
theorem "qs[2,3,0] = qs[3,0,2]"
|
11626
|
58 |
apply(simp)
|
10171
|
59 |
done
|
8745
|
60 |
|
|
61 |
text{*\noindent
|
|
62 |
More exciting theorems require induction, which is discussed below.
|
|
63 |
|
12489
|
64 |
If the termination proof requires a lemma that is of general use, you can
|
9933
|
65 |
turn it permanently into a simplification rule, in which case the above
|
12489
|
66 |
\isacommand{hint} is not necessary. But in the case of
|
|
67 |
@{thm[source]less_Suc_eq_le} this would be of dubious value.
|
8745
|
68 |
*}
|
|
69 |
(*<*)
|
|
70 |
end
|
|
71 |
(*>*)
|