doc-src/TutorialI/Recdef/Nested2.thy
changeset 9940 102f2430cef9
parent 9933 9feb1e0c4cb3
child 10171 59d6633835fa
equal deleted inserted replaced
9939:44af7faa677e 9940:102f2430cef9
    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;(*>*)