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