doc-src/TutorialI/Recdef/document/Nested2.tex
 author nipkow Mon Aug 28 10:16:58 2000 +0200 (2000-08-28) changeset 9690 50f22b1b136a child 9698 f0740137a65d permissions -rw-r--r--
*** empty log message ***
 nipkow@9690 1 \begin{isabelle}% nipkow@9690 2 % nipkow@9690 3 \begin{isamarkuptext}% nipkow@9690 4 \noindent nipkow@9690 5 The termintion condition is easily proved by induction:% nipkow@9690 6 \end{isamarkuptext}% nipkow@9690 7 \isacommand{lemma}\ [simp]:\ {"}t\ {\isasymin}\ set\ ts\ {\isasymlongrightarrow}\ size\ t\ <\ Suc(term\_size\ ts){"}\isanewline nipkow@9690 8 \isacommand{by}(induct\_tac\ ts,\ auto)% nipkow@9690 9 \begin{isamarkuptext}% nipkow@9690 10 \noindent nipkow@9690 11 By making this theorem a simplification rule, \isacommand{recdef} nipkow@9690 12 applies it automatically and the above definition of \isa{trev} nipkow@9690 13 succeeds now. As a reward for our effort, we can now prove the desired nipkow@9690 14 lemma directly. The key is the fact that we no longer need the verbose nipkow@9690 15 induction schema for type \isa{term} but the simpler one arising from nipkow@9690 16 \isa{trev}:% nipkow@9690 17 \end{isamarkuptext}% nipkow@9690 18 \isacommand{lemmas}\ [cong]\ =\ map\_cong\isanewline nipkow@9690 19 \isacommand{lemma}\ {"}trev(trev\ t)\ =\ t{"}\isanewline nipkow@9690 20 \isacommand{apply}(induct\_tac\ t\ rule:trev.induct)% nipkow@9690 21 \begin{isamarkuptxt}% nipkow@9690 22 \noindent nipkow@9690 23 This leaves us with a trivial base case \isa{trev\ (trev\ (Var\ \mbox{x}))\ =\ Var\ \mbox{x}} and the step case nipkow@9690 24 \begin{quote} nipkow@9690 25 nipkow@9690 26 \begin{isabelle}% nipkow@9690 27 {\isasymforall}\mbox{t}.\ \mbox{t}\ {\isasymin}\ set\ \mbox{ts}\ {\isasymlongrightarrow}\ trev\ (trev\ \mbox{t})\ =\ \mbox{t}\ {\isasymLongrightarrow}\isanewline nipkow@9690 28 trev\ (trev\ (App\ \mbox{f}\ \mbox{ts}))\ =\ App\ \mbox{f}\ \mbox{ts} nipkow@9690 29 \end{isabelle}% nipkow@9690 30 nipkow@9690 31 \end{quote} nipkow@9690 32 both of which are solved by simplification:% nipkow@9690 33 \end{isamarkuptxt}% nipkow@9690 34 \isacommand{by}(simp\_all\ del:map\_compose\ add:sym[OF\ map\_compose]\ rev\_map)% nipkow@9690 35 \begin{isamarkuptext}% nipkow@9690 36 \noindent nipkow@9690 37 If this surprises you, see Datatype/Nested2...... nipkow@9690 38 nipkow@9690 39 The above definition of \isa{trev} is superior to the one in \S\ref{sec:nested-datatype} nipkow@9690 40 because it brings \isa{rev} into play, about which already know a lot, in particular nipkow@9690 41 \isa{rev\ (rev\ \mbox{xs})\ =\ \mbox{xs}}. nipkow@9690 42 Thus this proof is a good example of an important principle: nipkow@9690 43 \begin{quote} nipkow@9690 44 \emph{Chose your definitions carefully\\ nipkow@9690 45 because they determine the complexity of your proofs.} nipkow@9690 46 \end{quote} nipkow@9690 47 nipkow@9690 48 Let us now return to the question of how \isacommand{recdef} can come up with sensible termination nipkow@9690 49 conditions in the presence of higher-order functions like \isa{map}. For a start, if nothing nipkow@9690 50 were known about \isa{map}, \isa{map\ trev\ \mbox{ts}} might apply \isa{trev} to arbitrary terms, nipkow@9690 51 and thus \isacommand{recdef} would try to prove the unprovable nipkow@9690 52 \isa{size\ \mbox{t}\ <\ Suc\ (term\_size\ \mbox{ts})}, without any assumption about \isa{t}. nipkow@9690 53 Therefore \isacommand{recdef} has been supplied with the congruence theorem \isa{map\_cong}: nipkow@9690 54 \begin{quote} nipkow@9690 55 nipkow@9690 56 \begin{isabelle}% nipkow@9690 57 {\isasymlbrakk}\mbox{xs}\ =\ \mbox{ys};\ {\isasymAnd}\mbox{x}.\ \mbox{x}\ {\isasymin}\ set\ \mbox{ys}\ {\isasymLongrightarrow}\ \mbox{f}\ \mbox{x}\ =\ \mbox{g}\ \mbox{x}{\isasymrbrakk}\isanewline nipkow@9690 58 {\isasymLongrightarrow}\ map\ \mbox{f}\ \mbox{xs}\ =\ map\ \mbox{g}\ \mbox{ys} nipkow@9690 59 \end{isabelle}% nipkow@9690 60 nipkow@9690 61 \end{quote} nipkow@9690 62 Its second premise expresses (indirectly) that the second argument of \isa{map} is only applied nipkow@9690 63 to elements of its third argument. Congruence rules for other higher-order functions on lists would nipkow@9690 64 look very similar but have not been proved yet because they were never needed. nipkow@9690 65 If you get into a situation where you need to supply \isacommand{recdef} with new congruence nipkow@9690 66 rules, you can either append the line nipkow@9690 67 \begin{ttbox} nipkow@9690 68 congs nipkow@9690 69 \end{ttbox} nipkow@9690 70 to the specific occurrence of \isacommand{recdef} or declare them globally: nipkow@9690 71 \begin{ttbox} nipkow@9690 72 lemmas [????????] = nipkow@9690 73 \end{ttbox} nipkow@9690 74 nipkow@9690 75 Note that \isacommand{recdef} feeds on exactly the same \emph{kind} of nipkow@9690 76 congruence rules as the simplifier (\S\ref{sec:simp-cong}) but that nipkow@9690 77 declaring a congruence rule for the simplifier does not make it nipkow@9690 78 available to \isacommand{recdef}, and vice versa. This is intentional.% nipkow@9690 79 \end{isamarkuptext}% nipkow@9690 80 \end{isabelle}% nipkow@9690 81 %%% Local Variables: nipkow@9690 82 %%% mode: latex nipkow@9690 83 %%% TeX-master: "root" nipkow@9690 84 %%% End: