*** empty log message ***
authornipkow
Tue Sep 12 19:03:13 2000 +0200 (2000-09-12)
changeset 9940102f2430cef9
parent 9939 44af7faa677e
child 9941 fe05af7ec816
*** empty log message ***
doc-src/TutorialI/Recdef/Nested2.thy
doc-src/TutorialI/Recdef/document/Nested2.tex
     1.1 --- a/doc-src/TutorialI/Recdef/Nested2.thy	Tue Sep 12 17:39:29 2000 +0200
     1.2 +++ b/doc-src/TutorialI/Recdef/Nested2.thy	Tue Sep 12 19:03:13 2000 +0200
     1.3 @@ -70,19 +70,29 @@
     1.4  rules for other higher-order functions on lists would look very similar but
     1.5  have not been proved yet because they were never needed. If you get into a
     1.6  situation where you need to supply \isacommand{recdef} with new congruence
     1.7 -rules, you can either append the line
     1.8 -\begin{ttbox}
     1.9 -congs <congruence rules>
    1.10 -\end{ttbox}
    1.11 -to the specific occurrence of \isacommand{recdef} or declare them globally:
    1.12 -\begin{ttbox}
    1.13 -lemmas [????????] = <congruence rules>
    1.14 -\end{ttbox}
    1.15 +rules, you can either append a hint locally
    1.16 +to the specific occurrence of \isacommand{recdef}
    1.17 +*}
    1.18 +(*<*)
    1.19 +consts dummy :: "nat => nat"
    1.20 +recdef dummy "{}"
    1.21 +"dummy n = n"
    1.22 +(*>*)
    1.23 +(hints cong: map_cong)
    1.24  
    1.25 -Note that \isacommand{recdef} feeds on exactly the same \emph{kind} of
    1.26 -congruence rules as the simplifier (\S\ref{sec:simp-cong}) but that
    1.27 -declaring a congruence rule for the simplifier does not make it
    1.28 -available to \isacommand{recdef}, and vice versa. This is intentional.
    1.29 +text{*\noindent
    1.30 +or declare them globally
    1.31 +by giving them the @{text recdef_cong} attribute as in
    1.32 +*}
    1.33 +
    1.34 +declare map_cong[recdef_cong];
    1.35 +
    1.36 +text{*
    1.37 +Note that the global @{text cong} and @{text recdef_cong} attributes are
    1.38 +intentionally kept apart because they control different activities, namely
    1.39 +simplification and making recursive definitions. The local @{text cong} in
    1.40 +the hints section of \isacommand{recdef} is merely short for @{text
    1.41 +recdef_cong}.
    1.42  %The simplifier's congruence rules cannot be used by recdef.
    1.43  %For example the weak congruence rules for if and case would prevent
    1.44  %recdef from generating sensible termination conditions.
     2.1 --- a/doc-src/TutorialI/Recdef/document/Nested2.tex	Tue Sep 12 17:39:29 2000 +0200
     2.2 +++ b/doc-src/TutorialI/Recdef/document/Nested2.tex	Tue Sep 12 19:03:13 2000 +0200
     2.3 @@ -69,19 +69,21 @@
     2.4  rules for other higher-order functions on lists would look very similar but
     2.5  have not been proved yet because they were never needed. If you get into a
     2.6  situation where you need to supply \isacommand{recdef} with new congruence
     2.7 -rules, you can either append the line
     2.8 -\begin{ttbox}
     2.9 -congs <congruence rules>
    2.10 -\end{ttbox}
    2.11 -to the specific occurrence of \isacommand{recdef} or declare them globally:
    2.12 -\begin{ttbox}
    2.13 -lemmas [????????] = <congruence rules>
    2.14 -\end{ttbox}
    2.15 -
    2.16 -Note that \isacommand{recdef} feeds on exactly the same \emph{kind} of
    2.17 -congruence rules as the simplifier (\S\ref{sec:simp-cong}) but that
    2.18 -declaring a congruence rule for the simplifier does not make it
    2.19 -available to \isacommand{recdef}, and vice versa. This is intentional.
    2.20 +rules, you can either append a hint locally
    2.21 +to the specific occurrence of \isacommand{recdef}%
    2.22 +\end{isamarkuptext}%
    2.23 +{\isacharparenleft}\isakeyword{hints}\ cong{\isacharcolon}\ map{\isacharunderscore}cong{\isacharparenright}%
    2.24 +\begin{isamarkuptext}%
    2.25 +\noindent
    2.26 +or declare them globally
    2.27 +by giving them the \isa{recdef{\isacharunderscore}cong} attribute as in%
    2.28 +\end{isamarkuptext}%
    2.29 +\isacommand{declare}\ map{\isacharunderscore}cong{\isacharbrackleft}recdef{\isacharunderscore}cong{\isacharbrackright}%
    2.30 +\begin{isamarkuptext}%
    2.31 +Note that the global \isa{cong} and \isa{recdef{\isacharunderscore}cong} attributes are
    2.32 +intentionally kept apart because they control different activities, namely
    2.33 +simplification and making recursive definitions. The local \isa{cong} in
    2.34 +the hints section of \isacommand{recdef} is merely short for \isa{recdef{\isacharunderscore}cong}.
    2.35  %The simplifier's congruence rules cannot be used by recdef.
    2.36  %For example the weak congruence rules for if and case would prevent
    2.37  %recdef from generating sensible termination conditions.%