doc-src/TutorialI/Recdef/document/Nested2.tex
 author nipkow Tue Sep 12 19:03:13 2000 +0200 (2000-09-12) changeset 9940 102f2430cef9 parent 9933 9feb1e0c4cb3 child 10171 59d6633835fa permissions -rw-r--r--
*** empty log message ***
     1 %

     2 \begin{isabellebody}%

     3 \def\isabellecontext{Nested2}%

     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 would look very similar but

    70 have not been proved yet because they were never needed. If you get into a

    71 situation where you need to supply \isacommand{recdef} with new congruence

    72 rules, you can either append a hint locally

    73 to the specific occurrence of \isacommand{recdef}%

    74 \end{isamarkuptext}%

    75 {\isacharparenleft}\isakeyword{hints}\ cong{\isacharcolon}\ map{\isacharunderscore}cong{\isacharparenright}%

    76 \begin{isamarkuptext}%

    77 \noindent

    78 or declare them globally

    79 by giving them the \isa{recdef{\isacharunderscore}cong} attribute as in%

    80 \end{isamarkuptext}%

    81 \isacommand{declare}\ map{\isacharunderscore}cong{\isacharbrackleft}recdef{\isacharunderscore}cong{\isacharbrackright}%

    82 \begin{isamarkuptext}%

    83 Note that the global \isa{cong} and \isa{recdef{\isacharunderscore}cong} attributes are

    84 intentionally kept apart because they control different activities, namely

    85 simplification and making recursive definitions. 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: