1 (*<*) |
1 (*<*) |
2 theory Nested1 imports Nested0 begin |
2 theory Nested1 imports Nested0 begin |
3 (*>*) |
3 (*>*) |
4 |
4 |
5 text{*\noindent |
5 text\<open>\noindent |
6 Although the definition of @{term trev} below is quite natural, we will have |
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. |
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 |
8 It is precisely this difficulty that is the \textit{raison d'\^etre} of |
9 this subsection. |
9 this subsection. |
10 |
10 |
11 Defining @{term trev} by \isacommand{recdef} rather than \isacommand{primrec} |
11 Defining @{term trev} by \isacommand{recdef} rather than \isacommand{primrec} |
12 simplifies matters because we are now free to use the recursion equation |
12 simplifies matters because we are now free to use the recursion equation |
13 suggested at the end of \S\ref{sec:nested-datatype}: |
13 suggested at the end of \S\ref{sec:nested-datatype}: |
14 *} |
14 \<close> |
15 |
15 |
16 recdef (*<*)(permissive)(*>*)trev "measure size" |
16 recdef (*<*)(permissive)(*>*)trev "measure size" |
17 "trev (Var x) = Var x" |
17 "trev (Var x) = Var x" |
18 "trev (App f ts) = App f (rev(map trev ts))" |
18 "trev (App f ts) = App f (rev(map trev ts))" |
19 |
19 |
20 text{*\noindent |
20 text\<open>\noindent |
21 Remember that function @{term size} is defined for each \isacommand{datatype}. |
21 Remember that function @{term size} is defined for each \isacommand{datatype}. |
22 However, the definition does not succeed. Isabelle complains about an |
22 However, the definition does not succeed. Isabelle complains about an |
23 unproved termination condition |
23 unproved termination condition |
24 @{prop[display]"t : set ts --> size t < Suc (size_term_list ts)"} |
24 @{prop[display]"t : set ts --> size t < Suc (size_term_list ts)"} |
25 where @{term set} returns the set of elements of a list |
25 where @{term set} returns the set of elements of a list |
34 which equals @{term"Suc(size_term_list ts)"}. We will now prove the termination condition and |
34 which equals @{term"Suc(size_term_list ts)"}. We will now prove the termination condition and |
35 continue with our definition. Below we return to the question of how |
35 continue with our definition. Below we return to the question of how |
36 \isacommand{recdef} knows about @{term map}. |
36 \isacommand{recdef} knows about @{term map}. |
37 |
37 |
38 The termination condition is easily proved by induction: |
38 The termination condition is easily proved by induction: |
39 *} |
39 \<close> |
40 |
40 |
41 (*<*) |
41 (*<*) |
42 end |
42 end |
43 (*>*) |
43 (*>*) |