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