doc-src/TutorialI/Recdef/document/Nested2.tex
author nipkow
Wed Dec 13 09:39:53 2000 +0100 (2000-12-13)
changeset 10654 458068404143
parent 10645 175ccbd5415a
child 10668 3b84288e60b7
permissions -rw-r--r--
*** empty log message ***
     1 %
     2 \begin{isabellebody}%
     3 \def\isabellecontext{Nested{\isadigit{2}}}%
     4 %
     5 \begin{isamarkuptext}%
     6 \noindent
     7 The termintion condition is easily proved by induction:%
     8 \end{isamarkuptext}%
     9 \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}t\ {\isasymin}\ set\ ts\ {\isasymlongrightarrow}\ size\ t\ {\isacharless}\ Suc{\isacharparenleft}term{\isacharunderscore}list{\isacharunderscore}size\ ts{\isacharparenright}{\isachardoublequote}\isanewline
    10 \isacommand{by}{\isacharparenleft}induct{\isacharunderscore}tac\ ts{\isacharcomma}\ auto{\isacharparenright}%
    11 \begin{isamarkuptext}%
    12 \noindent
    13 By making this theorem a simplification rule, \isacommand{recdef}
    14 applies it automatically and the above definition of \isa{trev}
    15 succeeds now. As a reward for our effort, we can now prove the desired
    16 lemma directly. The key is the fact that we no longer need the verbose
    17 induction schema for type \isa{term} but the simpler one arising from
    18 \isa{trev}:%
    19 \end{isamarkuptext}%
    20 \isacommand{lemma}\ {\isachardoublequote}trev{\isacharparenleft}trev\ t{\isacharparenright}\ {\isacharequal}\ t{\isachardoublequote}\isanewline
    21 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ t\ rule{\isacharcolon}trev{\isachardot}induct{\isacharparenright}%
    22 \begin{isamarkuptxt}%
    23 \noindent
    24 This leaves us with a trivial base case \isa{trev\ {\isacharparenleft}trev\ {\isacharparenleft}Var\ x{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ Var\ x} and the step case
    25 \begin{isabelle}%
    26 \ \ \ \ \ {\isasymforall}t{\isachardot}\ t\ {\isasymin}\ set\ ts\ {\isasymlongrightarrow}\ trev\ {\isacharparenleft}trev\ t{\isacharparenright}\ {\isacharequal}\ t\ {\isasymLongrightarrow}\isanewline
    27 \ \ \ \ \ trev\ {\isacharparenleft}trev\ {\isacharparenleft}App\ f\ ts{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ App\ f\ ts%
    28 \end{isabelle}
    29 both of which are solved by simplification:%
    30 \end{isamarkuptxt}%
    31 \isacommand{by}{\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}rev{\isacharunderscore}map\ sym{\isacharbrackleft}OF\ map{\isacharunderscore}compose{\isacharbrackright}\ cong{\isacharcolon}map{\isacharunderscore}cong{\isacharparenright}%
    32 \begin{isamarkuptext}%
    33 \noindent
    34 If the proof of the induction step mystifies you, we recommend to go through
    35 the chain of simplification steps in detail; you will probably need the help of
    36 \isa{trace{\isacharunderscore}simp}. Theorem \isa{map{\isacharunderscore}cong} is discussed below.
    37 %\begin{quote}
    38 %{term[display]"trev(trev(App f ts))"}\\
    39 %{term[display]"App f (rev(map trev (rev(map trev ts))))"}\\
    40 %{term[display]"App f (map trev (rev(rev(map trev ts))))"}\\
    41 %{term[display]"App f (map trev (map trev ts))"}\\
    42 %{term[display]"App f (map (trev o trev) ts)"}\\
    43 %{term[display]"App f (map (%x. x) ts)"}\\
    44 %{term[display]"App f ts"}
    45 %\end{quote}
    46 
    47 The above definition of \isa{trev} is superior to the one in
    48 \S\ref{sec:nested-datatype} because it brings \isa{rev} into play, about
    49 which already know a lot, in particular \isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs}.
    50 Thus this proof is a good example of an important principle:
    51 \begin{quote}
    52 \emph{Chose your definitions carefully\\
    53 because they determine the complexity of your proofs.}
    54 \end{quote}
    55 
    56 Let us now return to the question of how \isacommand{recdef} can come up with
    57 sensible termination conditions in the presence of higher-order functions
    58 like \isa{map}. For a start, if nothing were known about \isa{map},
    59 \isa{map\ trev\ ts} might apply \isa{trev} to arbitrary terms, and thus
    60 \isacommand{recdef} would try to prove the unprovable \isa{size\ t\ {\isacharless}\ Suc\ {\isacharparenleft}term{\isacharunderscore}list{\isacharunderscore}size\ ts{\isacharparenright}}, without any assumption about \isa{t}.  Therefore
    61 \isacommand{recdef} has been supplied with the congruence theorem
    62 \isa{map{\isacharunderscore}cong}:
    63 \begin{isabelle}%
    64 \ \ \ \ \ {\isasymlbrakk}xs\ {\isacharequal}\ ys{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ set\ ys\ {\isasymLongrightarrow}\ f\ x\ {\isacharequal}\ g\ x{\isasymrbrakk}\isanewline
    65 \ \ \ \ \ {\isasymLongrightarrow}\ map\ f\ xs\ {\isacharequal}\ map\ g\ ys%
    66 \end{isabelle}
    67 Its second premise expresses (indirectly) that the second argument of
    68 \isa{map} is only applied to elements of its third argument. Congruence
    69 rules for other higher-order functions on lists look very similar. If you get
    70 into a situation where you need to supply \isacommand{recdef} with new
    71 congruence rules, you can either append a hint locally
    72 to the specific occurrence of \isacommand{recdef}%
    73 \end{isamarkuptext}%
    74 {\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}cong{\isacharcolon}\ map{\isacharunderscore}cong{\isacharparenright}%
    75 \begin{isamarkuptext}%
    76 \noindent
    77 or declare them globally
    78 by giving them the \isaindexbold{recdef_cong} attribute as in%
    79 \end{isamarkuptext}%
    80 \isacommand{declare}\ map{\isacharunderscore}cong{\isacharbrackleft}recdef{\isacharunderscore}cong{\isacharbrackright}%
    81 \begin{isamarkuptext}%
    82 Note that the \isa{cong} and \isa{recdef{\isacharunderscore}cong} attributes are
    83 intentionally kept apart because they control different activities, namely
    84 simplification and making recursive definitions.
    85 % The local \isa{cong} in
    86 % the hints section of \isacommand{recdef} is merely short for \isa{recdef{\isacharunderscore}cong}.
    87 %The simplifier's congruence rules cannot be used by recdef.
    88 %For example the weak congruence rules for if and case would prevent
    89 %recdef from generating sensible termination conditions.%
    90 \end{isamarkuptext}%
    91 \end{isabellebody}%
    92 %%% Local Variables:
    93 %%% mode: latex
    94 %%% TeX-master: "root"
    95 %%% End: