52 because they determine the complexity of your proofs.} |
52 because they determine the complexity of your proofs.} |
53 \end{quote} |
53 \end{quote} |
54 |
54 |
55 Let us now return to the question of how \isacommand{recdef} can come up with |
55 Let us now return to the question of how \isacommand{recdef} can come up with |
56 sensible termination conditions in the presence of higher-order functions |
56 sensible termination conditions in the presence of higher-order functions |
57 like @{term"map"}. For a start, if nothing were known about @{term"map"}, |
57 like @{term"map"}. For a start, if nothing were known about @{term"map"}, then |
58 @{term"map trev ts"} might apply @{term"trev"} to arbitrary terms, and thus |
58 @{term"map trev ts"} might apply @{term"trev"} to arbitrary terms, and thus |
59 \isacommand{recdef} would try to prove the unprovable @{term"size t < Suc |
59 \isacommand{recdef} would try to prove the unprovable @{term"size t < Suc |
60 (term_list_size ts)"}, without any assumption about @{term"t"}. Therefore |
60 (term_list_size ts)"}, without any assumption about @{term"t"}. Therefore |
61 \isacommand{recdef} has been supplied with the congruence theorem |
61 \isacommand{recdef} has been supplied with the congruence theorem |
62 @{thm[source]map_cong}: |
62 @{thm[source]map_cong}: |
63 @{thm[display,margin=50]"map_cong"[no_vars]} |
63 @{thm[display,margin=50]"map_cong"[no_vars]} |
64 Its second premise expresses (indirectly) that the first argument of |
64 Its second premise expresses that in @{term"map f xs"}, |
65 @{term"map"} is only applied to elements of its second argument. Congruence |
65 function @{term"f"} is only applied to elements of list @{term"xs"}. Congruence |
66 rules for other higher-order functions on lists look very similar. If you get |
66 rules for other higher-order functions on lists are similar. If you get |
67 into a situation where you need to supply \isacommand{recdef} with new |
67 into a situation where you need to supply \isacommand{recdef} with new |
68 congruence rules, you can either append a hint after the end of |
68 congruence rules, you can append a hint after the end of |
69 the recursion equations |
69 the recursion equations: |
70 *} |
70 *} |
71 (*<*) |
71 (*<*) |
72 consts dummy :: "nat => nat" |
72 consts dummy :: "nat => nat" |
73 recdef dummy "{}" |
73 recdef dummy "{}" |
74 "dummy n = n" |
74 "dummy n = n" |
75 (*>*) |
75 (*>*) |
76 (hints recdef_cong: map_cong) |
76 (hints recdef_cong: map_cong) |
77 |
77 |
78 text{*\noindent |
78 text{*\noindent |
79 or declare them globally |
79 Or you can declare them globally |
80 by giving them the \attrdx{recdef_cong} attribute as in |
80 by giving them the \attrdx{recdef_cong} attribute: |
81 *} |
81 *} |
82 |
82 |
83 declare map_cong[recdef_cong] |
83 declare map_cong[recdef_cong] |
84 |
84 |
85 text{* |
85 text{* |
86 Note that the @{text cong} and @{text recdef_cong} attributes are |
86 The @{text cong} and @{text recdef_cong} attributes are |
87 intentionally kept apart because they control different activities, namely |
87 intentionally kept apart because they control different activities, namely |
88 simplification and making recursive definitions. |
88 simplification and making recursive definitions. |
89 % The local @{text cong} in |
89 % The local @{text cong} in |
90 % the hints section of \isacommand{recdef} is merely short for @{text recdef_cong}. |
90 % the hints section of \isacommand{recdef} is merely short for @{text recdef_cong}. |
91 %The simplifier's congruence rules cannot be used by recdef. |
91 %The simplifier's congruence rules cannot be used by recdef. |