doc-src/TutorialI/Recdef/document/Nested2.tex
 author nipkow Tue Aug 29 15:13:10 2000 +0200 (2000-08-29) changeset 9721 7e51c9f3d5a0 parent 9719 c753196599f9 child 9722 a5f86aed785b permissions -rw-r--r--
*** empty log message ***
     1 \begin{isabelle}%

     2 %

     3 \begin{isamarkuptext}%

     4 \noindent

     5 The termintion condition is easily proved by induction:%

     6 \end{isamarkuptext}%

     7 \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}t\ {\isasymin}\ set\ ts\ {\isasymlongrightarrow}\ size\ t\ {\isacharless}\ Suc{\isacharparenleft}term{\isacharunderscore}size\ ts{\isacharparenright}{\isachardoublequote}\isanewline

     8 \isacommand{by}{\isacharparenleft}induct{\isacharunderscore}tac\ ts{\isacharcomma}\ auto{\isacharparenright}%

     9 \begin{isamarkuptext}%

    10 \noindent

    11 By making this theorem a simplification rule, \isacommand{recdef}

    12 applies it automatically and the above definition of \isa{trev}

    13 succeeds now. As a reward for our effort, we can now prove the desired

    14 lemma directly. The key is the fact that we no longer need the verbose

    15 induction schema for type \isa{term} but the simpler one arising from

    16 \isa{trev}:%

    17 \end{isamarkuptext}%

    18 \isacommand{lemmas}\ {\isacharbrackleft}cong{\isacharbrackright}\ {\isacharequal}\ map{\isacharunderscore}cong\isanewline

    19 \isacommand{lemma}\ {\isachardoublequote}trev{\isacharparenleft}trev\ t{\isacharparenright}\ {\isacharequal}\ t{\isachardoublequote}\isanewline

    20 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ t\ rule{\isacharcolon}trev{\isachardot}induct{\isacharparenright}%

    21 \begin{isamarkuptxt}%

    22 \noindent

    23 This leaves us with a trivial base case \isa{trev\ {\isacharparenleft}trev\ {\isacharparenleft}Var\ \mbox{x}{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ Var\ \mbox{x}} and the step case

    24 \begin{quote}

    25

    26 \begin{isabelle}%

    27 {\isasymforall}\mbox{t}{\isachardot}\ \mbox{t}\ {\isasymin}\ set\ \mbox{ts}\ {\isasymlongrightarrow}\ trev\ {\isacharparenleft}trev\ \mbox{t}{\isacharparenright}\ {\isacharequal}\ \mbox{t}\ {\isasymLongrightarrow}\isanewline

    28 trev\ {\isacharparenleft}trev\ {\isacharparenleft}App\ \mbox{f}\ \mbox{ts}{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ App\ \mbox{f}\ \mbox{ts}

    29 \end{isabelle}%

    30

    31 \end{quote}

    32 both of which are solved by simplification:%

    33 \end{isamarkuptxt}%

    34 \isacommand{by}{\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}rev{\isacharunderscore}map\ sym{\isacharbrackleft}OF\ map{\isacharunderscore}compose{\isacharbrackright}{\isacharparenright}%

    35 \begin{isamarkuptext}%

    36 \noindent

    37 If the proof of the induction step mystifies you, we recommend to go through

    38 the chain of simplification steps in detail, probably with the help of

    39 \isa{trace\_simp}.

    40 %\begin{quote}

    41 %{term[display]"trev(trev(App f ts))"}\\

    42 %{term[display]"App f (rev(map trev (rev(map trev ts))))"}\\

    43 %{term[display]"App f (map trev (rev(rev(map trev ts))))"}\\

    44 %{term[display]"App f (map trev (map trev ts))"}\\

    45 %{term[display]"App f (map (trev o trev) ts)"}\\

    46 %{term[display]"App f (map (%x. x) ts)"}\\

    47 %{term[display]"App f ts"}

    48 %\end{quote}

    49

    50 The above definition of \isa{trev} is superior to the one in \S\ref{sec:nested-datatype}

    51 because it brings \isa{rev} into play, about which already know a lot, in particular

    52 \isa{rev\ {\isacharparenleft}rev\ \mbox{xs}{\isacharparenright}\ {\isacharequal}\ \mbox{xs}}.

    53 Thus this proof is a good example of an important principle:

    54 \begin{quote}

    55 \emph{Chose your definitions carefully\\

    56 because they determine the complexity of your proofs.}

    57 \end{quote}

    58

    59 Let us now return to the question of how \isacommand{recdef} can come up with

    60 sensible termination conditions in the presence of higher-order functions

    61 like \isa{map}. For a start, if nothing were known about \isa{map},

    62 \isa{map\ trev\ \mbox{ts}} might apply \isa{trev} to arbitrary terms, and thus

    63 \isacommand{recdef} would try to prove the unprovable \isa{size\ \mbox{t}\ {\isacharless}\ Suc\ {\isacharparenleft}term{\isacharunderscore}size\ \mbox{ts}{\isacharparenright}}, without any assumption about \isa{t}.  Therefore

    64 \isacommand{recdef} has been supplied with the congruence theorem

    65 \isa{map\_cong}:

    66 \begin{quote}

    67

    68 \begin{isabelle}%

    69 {\isasymlbrakk}\mbox{xs}\ {\isacharequal}\ \mbox{ys}{\isacharsemicolon}\ {\isasymAnd}\mbox{x}{\isachardot}\ \mbox{x}\ {\isasymin}\ set\ \mbox{ys}\ {\isasymLongrightarrow}\ \mbox{f}\ \mbox{x}\ {\isacharequal}\ \mbox{g}\ \mbox{x}{\isasymrbrakk}\isanewline

    70 {\isasymLongrightarrow}\ map\ \mbox{f}\ \mbox{xs}\ {\isacharequal}\ map\ \mbox{g}\ \mbox{ys}

    71 \end{isabelle}%

    72

    73 \end{quote}

    74 Its second premise expresses (indirectly) that the second argument of

    75 \isa{map} is only applied to elements of its third argument. Congruence

    76 rules for other higher-order functions on lists would look very similar but

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

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

    79 rules, you can either append the line

    80 \begin{ttbox}

    81 congs <congruence rules>

    82 \end{ttbox}

    83 to the specific occurrence of \isacommand{recdef} or declare them globally:

    84 \begin{ttbox}

    85 lemmas [????????] = <congruence rules>

    86 \end{ttbox}

    87

    88 Note that \isacommand{recdef} feeds on exactly the same \emph{kind} of

    89 congruence rules as the simplifier (\S\ref{sec:simp-cong}) but that

    90 declaring a congruence rule for the simplifier does not make it

    91 available to \isacommand{recdef}, and vice versa. This is intentional.%

    92 \end{isamarkuptext}%

    93 \end{isabelle}%

    94 %%% Local Variables:

    95 %%% mode: latex

    96 %%% TeX-master: "root"

    97 %%% End: