68 Its second premise expresses (indirectly) that the second argument of |
68 Its second premise expresses (indirectly) that the second argument of |
69 @{term"map"} is only applied to elements of its third argument. Congruence |
69 @{term"map"} is only applied to elements of its third argument. Congruence |
70 rules for other higher-order functions on lists would look very similar but |
70 rules for other higher-order functions on lists would look very similar but |
71 have not been proved yet because they were never needed. If you get into a |
71 have not been proved yet because they were never needed. If you get into a |
72 situation where you need to supply \isacommand{recdef} with new congruence |
72 situation where you need to supply \isacommand{recdef} with new congruence |
73 rules, you can either append the line |
73 rules, you can either append a hint locally |
74 \begin{ttbox} |
74 to the specific occurrence of \isacommand{recdef} |
75 congs <congruence rules> |
75 *} |
76 \end{ttbox} |
76 (*<*) |
77 to the specific occurrence of \isacommand{recdef} or declare them globally: |
77 consts dummy :: "nat => nat" |
78 \begin{ttbox} |
78 recdef dummy "{}" |
79 lemmas [????????] = <congruence rules> |
79 "dummy n = n" |
80 \end{ttbox} |
80 (*>*) |
|
81 (hints cong: map_cong) |
81 |
82 |
82 Note that \isacommand{recdef} feeds on exactly the same \emph{kind} of |
83 text{*\noindent |
83 congruence rules as the simplifier (\S\ref{sec:simp-cong}) but that |
84 or declare them globally |
84 declaring a congruence rule for the simplifier does not make it |
85 by giving them the @{text recdef_cong} attribute as in |
85 available to \isacommand{recdef}, and vice versa. This is intentional. |
86 *} |
|
87 |
|
88 declare map_cong[recdef_cong]; |
|
89 |
|
90 text{* |
|
91 Note that the global @{text cong} and @{text recdef_cong} attributes are |
|
92 intentionally kept apart because they control different activities, namely |
|
93 simplification and making recursive definitions. The local @{text cong} in |
|
94 the hints section of \isacommand{recdef} is merely short for @{text |
|
95 recdef_cong}. |
86 %The simplifier's congruence rules cannot be used by recdef. |
96 %The simplifier's congruence rules cannot be used by recdef. |
87 %For example the weak congruence rules for if and case would prevent |
97 %For example the weak congruence rules for if and case would prevent |
88 %recdef from generating sensible termination conditions. |
98 %recdef from generating sensible termination conditions. |
89 *}; |
99 *}; |
90 (*<*)end;(*>*) |
100 (*<*)end;(*>*) |