1 (*<*) |
|
2 theory Nested1 imports Nested0 begin |
|
3 (*>*) |
|
4 |
|
5 text{*\noindent |
|
6 Although the definition of @{term trev} below is quite natural, we will have |
|
7 to overcome a minor difficulty in convincing Isabelle of its termination. |
|
8 It is precisely this difficulty that is the \textit{raison d'\^etre} of |
|
9 this subsection. |
|
10 |
|
11 Defining @{term trev} by \isacommand{recdef} rather than \isacommand{primrec} |
|
12 simplifies matters because we are now free to use the recursion equation |
|
13 suggested at the end of \S\ref{sec:nested-datatype}: |
|
14 *} |
|
15 |
|
16 recdef (*<*)(permissive)(*>*)trev "measure size" |
|
17 "trev (Var x) = Var x" |
|
18 "trev (App f ts) = App f (rev(map trev ts))" |
|
19 |
|
20 text{*\noindent |
|
21 Remember that function @{term size} is defined for each \isacommand{datatype}. |
|
22 However, the definition does not succeed. Isabelle complains about an |
|
23 unproved termination condition |
|
24 @{prop[display]"t : set ts --> size t < Suc (term_list_size ts)"} |
|
25 where @{term set} returns the set of elements of a list |
|
26 and @{text"term_list_size :: term list \<Rightarrow> nat"} is an auxiliary |
|
27 function automatically defined by Isabelle |
|
28 (while processing the declaration of @{text term}). Why does the |
|
29 recursive call of @{const trev} lead to this |
|
30 condition? Because \isacommand{recdef} knows that @{term map} |
|
31 will apply @{const trev} only to elements of @{term ts}. Thus the |
|
32 condition expresses that the size of the argument @{prop"t : set ts"} of any |
|
33 recursive call of @{const trev} is strictly less than @{term"size(App f ts)"}, |
|
34 which equals @{term"Suc(term_list_size ts)"}. We will now prove the termination condition and |
|
35 continue with our definition. Below we return to the question of how |
|
36 \isacommand{recdef} knows about @{term map}. |
|
37 |
|
38 The termination condition is easily proved by induction: |
|
39 *} |
|
40 |
|
41 (*<*) |
|
42 end |
|
43 (*>*) |
|