nipkow@9722: % nipkow@9722: \begin{isabellebody}% wenzelm@9924: \def\isabellecontext{Nested2}% nipkow@9690: % nipkow@9690: \begin{isamarkuptext}% nipkow@9690: \noindent nipkow@9690: The termintion condition is easily proved by induction:% nipkow@9690: \end{isamarkuptext}% nipkow@9754: \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 wenzelm@9698: \isacommand{by}{\isacharparenleft}induct{\isacharunderscore}tac\ ts{\isacharcomma}\ auto{\isacharparenright}% nipkow@9690: \begin{isamarkuptext}% nipkow@9690: \noindent nipkow@9690: By making this theorem a simplification rule, \isacommand{recdef} nipkow@9690: applies it automatically and the above definition of \isa{trev} nipkow@9690: succeeds now. As a reward for our effort, we can now prove the desired nipkow@9690: lemma directly. The key is the fact that we no longer need the verbose nipkow@9690: induction schema for type \isa{term} but the simpler one arising from nipkow@9690: \isa{trev}:% nipkow@9690: \end{isamarkuptext}% wenzelm@9698: \isacommand{lemma}\ {\isachardoublequote}trev{\isacharparenleft}trev\ t{\isacharparenright}\ {\isacharequal}\ t{\isachardoublequote}\isanewline wenzelm@9698: \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ t\ rule{\isacharcolon}trev{\isachardot}induct{\isacharparenright}% nipkow@9690: \begin{isamarkuptxt}% nipkow@9690: \noindent nipkow@9792: This leaves us with a trivial base case \isa{trev\ {\isacharparenleft}trev\ {\isacharparenleft}Var\ x{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ Var\ x} and the step case nipkow@9690: \begin{isabelle}% nipkow@9834: \ \ \ \ \ {\isasymforall}t{\isachardot}\ t\ {\isasymin}\ set\ ts\ {\isasymlongrightarrow}\ trev\ {\isacharparenleft}trev\ t{\isacharparenright}\ {\isacharequal}\ t\ {\isasymLongrightarrow}\isanewline nipkow@9834: \ \ \ \ \ trev\ {\isacharparenleft}trev\ {\isacharparenleft}App\ f\ ts{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ App\ f\ ts% wenzelm@9924: \end{isabelle} nipkow@9690: both of which are solved by simplification:% nipkow@9690: \end{isamarkuptxt}% nipkow@9933: \isacommand{by}{\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}rev{\isacharunderscore}map\ sym{\isacharbrackleft}OF\ map{\isacharunderscore}compose{\isacharbrackright}\ cong{\isacharcolon}map{\isacharunderscore}cong{\isacharparenright}% nipkow@9690: \begin{isamarkuptext}% nipkow@9690: \noindent nipkow@9721: If the proof of the induction step mystifies you, we recommend to go through nipkow@9754: the chain of simplification steps in detail; you will probably need the help of nipkow@9933: \isa{trace{\isacharunderscore}simp}. Theorem \isa{map{\isacharunderscore}cong} is discussed below. nipkow@9721: %\begin{quote} nipkow@9721: %{term[display]"trev(trev(App f ts))"}\\ nipkow@9721: %{term[display]"App f (rev(map trev (rev(map trev ts))))"}\\ nipkow@9721: %{term[display]"App f (map trev (rev(rev(map trev ts))))"}\\ nipkow@9721: %{term[display]"App f (map trev (map trev ts))"}\\ nipkow@9721: %{term[display]"App f (map (trev o trev) ts)"}\\ nipkow@9721: %{term[display]"App f (map (%x. x) ts)"}\\ nipkow@9721: %{term[display]"App f ts"} nipkow@9721: %\end{quote} nipkow@9690: nipkow@9754: The above definition of \isa{trev} is superior to the one in nipkow@9754: \S\ref{sec:nested-datatype} because it brings \isa{rev} into play, about nipkow@9792: which already know a lot, in particular \isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs}. nipkow@9690: Thus this proof is a good example of an important principle: nipkow@9690: \begin{quote} nipkow@9690: \emph{Chose your definitions carefully\\ nipkow@9690: because they determine the complexity of your proofs.} nipkow@9690: \end{quote} nipkow@9690: nipkow@9721: Let us now return to the question of how \isacommand{recdef} can come up with nipkow@9721: sensible termination conditions in the presence of higher-order functions nipkow@9721: like \isa{map}. For a start, if nothing were known about \isa{map}, nipkow@9792: \isa{map\ trev\ ts} might apply \isa{trev} to arbitrary terms, and thus nipkow@9792: \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 nipkow@9721: \isacommand{recdef} has been supplied with the congruence theorem nipkow@9754: \isa{map{\isacharunderscore}cong}: nipkow@9690: \begin{isabelle}% nipkow@9834: \ \ \ \ \ {\isasymlbrakk}xs\ {\isacharequal}\ ys{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ set\ ys\ {\isasymLongrightarrow}\ f\ x\ {\isacharequal}\ g\ x{\isasymrbrakk}\isanewline nipkow@9834: \ \ \ \ \ {\isasymLongrightarrow}\ map\ f\ xs\ {\isacharequal}\ map\ g\ ys% wenzelm@9924: \end{isabelle} nipkow@9721: Its second premise expresses (indirectly) that the second argument of nipkow@9721: \isa{map} is only applied to elements of its third argument. Congruence nipkow@9721: rules for other higher-order functions on lists would look very similar but nipkow@9721: have not been proved yet because they were never needed. If you get into a nipkow@9721: situation where you need to supply \isacommand{recdef} with new congruence nipkow@9940: rules, you can either append a hint locally nipkow@9940: to the specific occurrence of \isacommand{recdef}% nipkow@9940: \end{isamarkuptext}% nipkow@10171: {\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}cong{\isacharcolon}\ map{\isacharunderscore}cong{\isacharparenright}% nipkow@9940: \begin{isamarkuptext}% nipkow@9940: \noindent nipkow@9940: or declare them globally nipkow@9940: by giving them the \isa{recdef{\isacharunderscore}cong} attribute as in% nipkow@9940: \end{isamarkuptext}% nipkow@9940: \isacommand{declare}\ map{\isacharunderscore}cong{\isacharbrackleft}recdef{\isacharunderscore}cong{\isacharbrackright}% nipkow@9940: \begin{isamarkuptext}% nipkow@10171: Note that the \isa{cong} and \isa{recdef{\isacharunderscore}cong} attributes are nipkow@9940: intentionally kept apart because they control different activities, namely nipkow@10171: simplification and making recursive definitions. nipkow@10171: % The local \isa{cong} in nipkow@10171: % the hints section of \isacommand{recdef} is merely short for \isa{recdef{\isacharunderscore}cong}. nipkow@9933: %The simplifier's congruence rules cannot be used by recdef. nipkow@9933: %For example the weak congruence rules for if and case would prevent nipkow@9933: %recdef from generating sensible termination conditions.% nipkow@9690: \end{isamarkuptext}% nipkow@9722: \end{isabellebody}% nipkow@9690: %%% Local Variables: nipkow@9690: %%% mode: latex nipkow@9690: %%% TeX-master: "root" nipkow@9690: %%% End: