doc-src/TutorialI/Recdef/document/Nested2.tex
author wenzelm
Mon Sep 11 18:00:47 2000 +0200 (2000-09-11)
changeset 9924 3370f6aa3200
parent 9834 109b11c4e77e
child 9933 9feb1e0c4cb3
permissions -rw-r--r--
updated;
     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{lemmas}\ {\isacharbrackleft}cong{\isacharbrackright}\ {\isacharequal}\ map{\isacharunderscore}cong\isanewline
    21 \isacommand{lemma}\ {\isachardoublequote}trev{\isacharparenleft}trev\ t{\isacharparenright}\ {\isacharequal}\ t{\isachardoublequote}\isanewline
    22 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ t\ rule{\isacharcolon}trev{\isachardot}induct{\isacharparenright}%
    23 \begin{isamarkuptxt}%
    24 \noindent
    25 This leaves us with a trivial base case \isa{trev\ {\isacharparenleft}trev\ {\isacharparenleft}Var\ x{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ Var\ x} and the step case
    26 \begin{isabelle}%
    27 \ \ \ \ \ {\isasymforall}t{\isachardot}\ t\ {\isasymin}\ set\ ts\ {\isasymlongrightarrow}\ trev\ {\isacharparenleft}trev\ t{\isacharparenright}\ {\isacharequal}\ t\ {\isasymLongrightarrow}\isanewline
    28 \ \ \ \ \ trev\ {\isacharparenleft}trev\ {\isacharparenleft}App\ f\ ts{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ App\ f\ ts%
    29 \end{isabelle}
    30 both of which are solved by simplification:%
    31 \end{isamarkuptxt}%
    32 \isacommand{by}{\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}rev{\isacharunderscore}map\ sym{\isacharbrackleft}OF\ map{\isacharunderscore}compose{\isacharbrackright}{\isacharparenright}%
    33 \begin{isamarkuptext}%
    34 \noindent
    35 If the proof of the induction step mystifies you, we recommend to go through
    36 the chain of simplification steps in detail; you will probably need the help of
    37 \isa{trace{\isacharunderscore}simp}.
    38 %\begin{quote}
    39 %{term[display]"trev(trev(App f ts))"}\\
    40 %{term[display]"App f (rev(map trev (rev(map trev ts))))"}\\
    41 %{term[display]"App f (map trev (rev(rev(map trev ts))))"}\\
    42 %{term[display]"App f (map trev (map trev ts))"}\\
    43 %{term[display]"App f (map (trev o trev) ts)"}\\
    44 %{term[display]"App f (map (%x. x) ts)"}\\
    45 %{term[display]"App f ts"}
    46 %\end{quote}
    47 
    48 The above definition of \isa{trev} is superior to the one in
    49 \S\ref{sec:nested-datatype} because it brings \isa{rev} into play, about
    50 which already know a lot, in particular \isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs}.
    51 Thus this proof is a good example of an important principle:
    52 \begin{quote}
    53 \emph{Chose your definitions carefully\\
    54 because they determine the complexity of your proofs.}
    55 \end{quote}
    56 
    57 Let us now return to the question of how \isacommand{recdef} can come up with
    58 sensible termination conditions in the presence of higher-order functions
    59 like \isa{map}. For a start, if nothing were known about \isa{map},
    60 \isa{map\ trev\ ts} might apply \isa{trev} to arbitrary terms, and thus
    61 \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
    62 \isacommand{recdef} has been supplied with the congruence theorem
    63 \isa{map{\isacharunderscore}cong}:
    64 \begin{isabelle}%
    65 \ \ \ \ \ {\isasymlbrakk}xs\ {\isacharequal}\ ys{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ set\ ys\ {\isasymLongrightarrow}\ f\ x\ {\isacharequal}\ g\ x{\isasymrbrakk}\isanewline
    66 \ \ \ \ \ {\isasymLongrightarrow}\ map\ f\ xs\ {\isacharequal}\ map\ g\ ys%
    67 \end{isabelle}
    68 Its second premise expresses (indirectly) that the second argument of
    69 \isa{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
    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
    73 rules, you can either append the line
    74 \begin{ttbox}
    75 congs <congruence rules>
    76 \end{ttbox}
    77 to the specific occurrence of \isacommand{recdef} or declare them globally:
    78 \begin{ttbox}
    79 lemmas [????????] = <congruence rules>
    80 \end{ttbox}
    81 
    82 Note that \isacommand{recdef} feeds on exactly the same \emph{kind} of
    83 congruence rules as the simplifier (\S\ref{sec:simp-cong}) but that
    84 declaring a congruence rule for the simplifier does not make it
    85 available to \isacommand{recdef}, and vice versa. This is intentional.%
    86 \end{isamarkuptext}%
    87 \end{isabellebody}%
    88 %%% Local Variables:
    89 %%% mode: latex
    90 %%% TeX-master: "root"
    91 %%% End: