32 @{term[display,margin=60]"ALL t. t : set ts --> trev (trev t) = t ==> trev (trev (App f ts)) = App f ts"} |
32 @{term[display,margin=60]"ALL t. t : set ts --> trev (trev t) = t ==> trev (trev (App f ts)) = App f ts"} |
33 \end{quote} |
33 \end{quote} |
34 both of which are solved by simplification: |
34 both of which are solved by simplification: |
35 *}; |
35 *}; |
36 |
36 |
37 by(simp_all del:map_compose add:sym[OF map_compose] rev_map); |
37 by(simp_all add:rev_map sym[OF map_compose]); |
38 |
38 |
39 text{*\noindent |
39 text{*\noindent |
40 If this surprises you, see Datatype/Nested2...... |
40 If the proof of the induction step mystifies you, we recommend to go through |
|
41 the chain of simplification steps in detail, probably with the help of |
|
42 \isa{trace\_simp}. |
|
43 %\begin{quote} |
|
44 %{term[display]"trev(trev(App f ts))"}\\ |
|
45 %{term[display]"App f (rev(map trev (rev(map trev ts))))"}\\ |
|
46 %{term[display]"App f (map trev (rev(rev(map trev ts))))"}\\ |
|
47 %{term[display]"App f (map trev (map trev ts))"}\\ |
|
48 %{term[display]"App f (map (trev o trev) ts)"}\\ |
|
49 %{term[display]"App f (map (%x. x) ts)"}\\ |
|
50 %{term[display]"App f ts"} |
|
51 %\end{quote} |
41 |
52 |
42 The above definition of @{term"trev"} is superior to the one in \S\ref{sec:nested-datatype} |
53 The above definition of @{term"trev"} is superior to the one in \S\ref{sec:nested-datatype} |
43 because it brings @{term"rev"} into play, about which already know a lot, in particular |
54 because it brings @{term"rev"} into play, about which already know a lot, in particular |
44 @{prop"rev(rev xs) = xs"}. |
55 @{prop"rev(rev xs) = xs"}. |
45 Thus this proof is a good example of an important principle: |
56 Thus this proof is a good example of an important principle: |
46 \begin{quote} |
57 \begin{quote} |
47 \emph{Chose your definitions carefully\\ |
58 \emph{Chose your definitions carefully\\ |
48 because they determine the complexity of your proofs.} |
59 because they determine the complexity of your proofs.} |
49 \end{quote} |
60 \end{quote} |
50 |
61 |
51 Let us now return to the question of how \isacommand{recdef} can come up with sensible termination |
62 Let us now return to the question of how \isacommand{recdef} can come up with |
52 conditions in the presence of higher-order functions like @{term"map"}. For a start, if nothing |
63 sensible termination conditions in the presence of higher-order functions |
53 were known about @{term"map"}, @{term"map trev ts"} might apply @{term"trev"} to arbitrary terms, |
64 like @{term"map"}. For a start, if nothing were known about @{term"map"}, |
54 and thus \isacommand{recdef} would try to prove the unprovable |
65 @{term"map trev ts"} might apply @{term"trev"} to arbitrary terms, and thus |
55 @{term"size t < Suc (term_size ts)"}, without any assumption about \isa{t}. |
66 \isacommand{recdef} would try to prove the unprovable @{term"size t < Suc |
56 Therefore \isacommand{recdef} has been supplied with the congruence theorem \isa{map\_cong}: |
67 (term_size ts)"}, without any assumption about \isa{t}. Therefore |
|
68 \isacommand{recdef} has been supplied with the congruence theorem |
|
69 \isa{map\_cong}: |
57 \begin{quote} |
70 \begin{quote} |
58 @{thm[display,margin=50]"map_cong"[no_vars]} |
71 @{thm[display,margin=50]"map_cong"[no_vars]} |
59 \end{quote} |
72 \end{quote} |
60 Its second premise expresses (indirectly) that the second argument of @{term"map"} is only applied |
73 Its second premise expresses (indirectly) that the second argument of |
61 to elements of its third argument. Congruence rules for other higher-order functions on lists would |
74 @{term"map"} is only applied to elements of its third argument. Congruence |
62 look very similar but have not been proved yet because they were never needed. |
75 rules for other higher-order functions on lists would look very similar but |
63 If you get into a situation where you need to supply \isacommand{recdef} with new congruence |
76 have not been proved yet because they were never needed. If you get into a |
|
77 situation where you need to supply \isacommand{recdef} with new congruence |
64 rules, you can either append the line |
78 rules, you can either append the line |
65 \begin{ttbox} |
79 \begin{ttbox} |
66 congs <congruence rules> |
80 congs <congruence rules> |
67 \end{ttbox} |
81 \end{ttbox} |
68 to the specific occurrence of \isacommand{recdef} or declare them globally: |
82 to the specific occurrence of \isacommand{recdef} or declare them globally: |