doc-src/TutorialI/Recdef/document/Nested2.tex
 author nipkow Wed Aug 30 18:09:20 2000 +0200 (2000-08-30) changeset 9754 a123a64cadeb parent 9722 a5f86aed785b child 9792 bbefb6ce5cb2 permissions -rw-r--r--
*** empty log message ***
1 %
2 \begin{isabellebody}%
3 %
4 \begin{isamarkuptext}%
5 \noindent
6 The termintion condition is easily proved by induction:%
7 \end{isamarkuptext}%
8 \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
9 \isacommand{by}{\isacharparenleft}induct{\isacharunderscore}tac\ ts{\isacharcomma}\ auto{\isacharparenright}%
10 \begin{isamarkuptext}%
11 \noindent
12 By making this theorem a simplification rule, \isacommand{recdef}
13 applies it automatically and the above definition of \isa{trev}
14 succeeds now. As a reward for our effort, we can now prove the desired
15 lemma directly. The key is the fact that we no longer need the verbose
16 induction schema for type \isa{term} but the simpler one arising from
17 \isa{trev}:%
18 \end{isamarkuptext}%
19 \isacommand{lemmas}\ {\isacharbrackleft}cong{\isacharbrackright}\ {\isacharequal}\ map{\isacharunderscore}cong\isanewline
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\ \mbox{x}{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ Var\ \mbox{x}} and the step case
25 \begin{quote}
27 \begin{isabelle}%
28 {\isasymforall}\mbox{t}{\isachardot}\ \mbox{t}\ {\isasymin}\ set\ \mbox{ts}\ {\isasymlongrightarrow}\ trev\ {\isacharparenleft}trev\ \mbox{t}{\isacharparenright}\ {\isacharequal}\ \mbox{t}\ {\isasymLongrightarrow}\isanewline
29 trev\ {\isacharparenleft}trev\ {\isacharparenleft}App\ \mbox{f}\ \mbox{ts}{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ App\ \mbox{f}\ \mbox{ts}
30 \end{isabelle}%
32 \end{quote}
33 both of which are solved by simplification:%
34 \end{isamarkuptxt}%
36 \begin{isamarkuptext}%
37 \noindent
38 If the proof of the induction step mystifies you, we recommend to go through
39 the chain of simplification steps in detail; you will probably need the help of
40 \isa{trace{\isacharunderscore}simp}.
41 %\begin{quote}
42 %{term[display]"trev(trev(App f ts))"}\\
43 %{term[display]"App f (rev(map trev (rev(map trev ts))))"}\\
44 %{term[display]"App f (map trev (rev(rev(map trev ts))))"}\\
45 %{term[display]"App f (map trev (map trev ts))"}\\
46 %{term[display]"App f (map (trev o trev) ts)"}\\
47 %{term[display]"App f (map (%x. x) ts)"}\\
48 %{term[display]"App f ts"}
49 %\end{quote}
51 The above definition of \isa{trev} is superior to the one in
52 \S\ref{sec:nested-datatype} because it brings \isa{rev} into play, about
53 which already know a lot, in particular \isa{rev\ {\isacharparenleft}rev\ \mbox{xs}{\isacharparenright}\ {\isacharequal}\ \mbox{xs}}.
54 Thus this proof is a good example of an important principle:
55 \begin{quote}
57 because they determine the complexity of your proofs.}
58 \end{quote}
60 Let us now return to the question of how \isacommand{recdef} can come up with
61 sensible termination conditions in the presence of higher-order functions
62 like \isa{map}. For a start, if nothing were known about \isa{map},
63 \isa{map\ trev\ \mbox{ts}} might apply \isa{trev} to arbitrary terms, and thus
64 \isacommand{recdef} would try to prove the unprovable \isa{size\ \mbox{t}\ {\isacharless}\ Suc\ {\isacharparenleft}term{\isacharunderscore}list{\isacharunderscore}size\ \mbox{ts}{\isacharparenright}}, without any assumption about \isa{\mbox{t}}.  Therefore
65 \isacommand{recdef} has been supplied with the congruence theorem
66 \isa{map{\isacharunderscore}cong}:
67 \begin{quote}
69 \begin{isabelle}%
70 {\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
71 {\isasymLongrightarrow}\ map\ \mbox{f}\ \mbox{xs}\ {\isacharequal}\ map\ \mbox{g}\ \mbox{ys}
72 \end{isabelle}%
74 \end{quote}
75 Its second premise expresses (indirectly) that the second argument of
76 \isa{map} is only applied to elements of its third argument. Congruence
77 rules for other higher-order functions on lists would look very similar but
78 have not been proved yet because they were never needed. If you get into a
79 situation where you need to supply \isacommand{recdef} with new congruence
80 rules, you can either append the line
81 \begin{ttbox}
82 congs <congruence rules>
83 \end{ttbox}
84 to the specific occurrence of \isacommand{recdef} or declare them globally:
85 \begin{ttbox}
86 lemmas [????????] = <congruence rules>
87 \end{ttbox}
89 Note that \isacommand{recdef} feeds on exactly the same \emph{kind} of
90 congruence rules as the simplifier (\S\ref{sec:simp-cong}) but that
91 declaring a congruence rule for the simplifier does not make it
92 available to \isacommand{recdef}, and vice versa. This is intentional.%
93 \end{isamarkuptext}%
94 \end{isabellebody}%
95 %%% Local Variables:
96 %%% mode: latex
97 %%% TeX-master: "root"
98 %%% End: