diff -r 619531d87ce4 -r 4e2ee88276d2 doc-src/TutorialI/document/Nested.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/document/Nested.tex	Thu Jul 26 19:59:06 2012 +0200
@@ -0,0 +1,240 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{Nested}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\begin{isamarkuptext}%
+\index{datatypes!and nested recursion}%
+So far, all datatypes had the property that on the right-hand side of their
+definition they occurred only at the top-level: directly below a
+constructor. Now we consider \emph{nested recursion}, where the recursive
+datatype occurs nested in some other datatype (but not inside itself!).
+Consider the following model of terms
+where function symbols can be applied to a list of arguments:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{datatype}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}f{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteopen}}term{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{3D}{\isacharequal}}\ Var\ {\isaliteral{27}{\isacharprime}}v\ {\isaliteral{7C}{\isacharbar}}\ App\ {\isaliteral{27}{\isacharprime}}f\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}f{\isaliteral{29}{\isacharparenright}}term\ list{\isaliteral{22}{\isachardoublequoteclose}}%
+\begin{isamarkuptext}%
+\noindent
+Note that we need to quote \isa{term} on the left to avoid confusion with
+the Isabelle command \isacommand{term}.
+Parameter \isa{{\isaliteral{27}{\isacharprime}}v} is the type of variables and \isa{{\isaliteral{27}{\isacharprime}}f} the type of
+function symbols.
+A mathematical term like $f(x,g(y))$ becomes \isa{App\ f\ {\isaliteral{5B}{\isacharbrackleft}}Var\ x{\isaliteral{2C}{\isacharcomma}}\ App\ g\ {\isaliteral{5B}{\isacharbrackleft}}Var\ y{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{5D}{\isacharbrackright}}}, where \isa{f}, \isa{g}, \isa{x}, \isa{y} are
+suitable values, e.g.\ numbers or strings.
+
+What complicates the definition of \isa{term} is the nested occurrence of
+\isa{term} inside \isa{list} on the right-hand side. In principle,
+nested recursion can be eliminated in favour of mutual recursion by unfolding
+the offending datatypes, here \isa{list}. The result for \isa{term}
+would be something like
+\medskip
+
+\input{document/unfoldnested.tex}
+\medskip
+
+\noindent
+Although we do not recommend this unfolding to the user, it shows how to
+simulate nested recursion by mutual recursion.
+Now we return to the initial definition of \isa{term} using
+nested recursion.
+
+Let us define a substitution function on terms. Because terms involve term
+lists, we need to define two substitution functions simultaneously:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{primrec}\isamarkupfalse%
+\isanewline
+subst\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}f{\isaliteral{29}{\isacharparenright}}term{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}f{\isaliteral{29}{\isacharparenright}}term\ \ \ \ \ \ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}f{\isaliteral{29}{\isacharparenright}}term{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\isanewline
+substs{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}f{\isaliteral{29}{\isacharparenright}}term{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}f{\isaliteral{29}{\isacharparenright}}term\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}f{\isaliteral{29}{\isacharparenright}}term\ list{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\isakeyword{where}\isanewline
+{\isaliteral{22}{\isachardoublequoteopen}}subst\ s\ {\isaliteral{28}{\isacharparenleft}}Var\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ s\ x{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
+\ \ subst{\isaliteral{5F}{\isacharunderscore}}App{\isaliteral{3A}{\isacharcolon}}\isanewline
+{\isaliteral{22}{\isachardoublequoteopen}}subst\ s\ {\isaliteral{28}{\isacharparenleft}}App\ f\ ts{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ App\ f\ {\isaliteral{28}{\isacharparenleft}}substs\ s\ ts{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
+\isanewline
+{\isaliteral{22}{\isachardoublequoteopen}}substs\ s\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
+{\isaliteral{22}{\isachardoublequoteopen}}substs\ s\ {\isaliteral{28}{\isacharparenleft}}t\ {\isaliteral{23}{\isacharhash}}\ ts{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ subst\ s\ t\ {\isaliteral{23}{\isacharhash}}\ substs\ s\ ts{\isaliteral{22}{\isachardoublequoteclose}}%
+\begin{isamarkuptext}%
+\noindent
+Individual equations in a \commdx{primrec} definition may be
+named as shown for \isa{subst{\isaliteral{5F}{\isacharunderscore}}App}.
+The significance of this device will become apparent below.
+
+Similarly, when proving a statement about terms inductively, we need
+to prove a related statement about term lists simultaneously. For example,
+the fact that the identity substitution does not change a term needs to be
+strengthened and proved as follows:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ subst{\isaliteral{5F}{\isacharunderscore}}id{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}subst\ \ Var\ t\ \ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}t\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}f{\isaliteral{29}{\isacharparenright}}term{\isaliteral{29}{\isacharparenright}}\ \ {\isaliteral{5C3C616E643E}{\isasymand}}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ substs\ Var\ ts\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}ts{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}f{\isaliteral{29}{\isacharparenright}}term\ list{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{apply}\isamarkupfalse%
+{\isaliteral{28}{\isacharparenleft}}induct{\isaliteral{5F}{\isacharunderscore}}tac\ t\ \isakeyword{and}\ ts{\isaliteral{2C}{\isacharcomma}}\ simp{\isaliteral{5F}{\isacharunderscore}}all{\isaliteral{29}{\isacharparenright}}\isanewline
+\isacommand{done}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+\noindent
+Note that \isa{Var} is the identity substitution because by definition it
+leaves variables unchanged: \isa{subst\ Var\ {\isaliteral{28}{\isacharparenleft}}Var\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ Var\ x}. Note also
+that the type annotations are necessary because otherwise there is nothing in
+the goal to enforce that both halves of the goal talk about the same type
+parameters \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}f{\isaliteral{29}{\isacharparenright}}}. As a result, induction would fail
+because the two halves of the goal would be unrelated.
+
+\begin{exercise}
+The fact that substitution distributes over composition can be expressed
+roughly as follows:
+\begin{isabelle}%
+\ \ \ \ \ subst\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ g{\isaliteral{29}{\isacharparenright}}\ t\ {\isaliteral{3D}{\isacharequal}}\ subst\ f\ {\isaliteral{28}{\isacharparenleft}}subst\ g\ t{\isaliteral{29}{\isacharparenright}}%
+\end{isabelle}
+Correct this statement (you will find that it does not type-check),
+strengthen it, and prove it. (Note: \isa{{\isaliteral{5C3C636972633E}{\isasymcirc}}} is function composition;
+its definition is found in theorem \isa{o{\isaliteral{5F}{\isacharunderscore}}def}).
+\end{exercise}
+\begin{exercise}\label{ex:trev-trev}
+  Define a function \isa{trev} of type \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}f{\isaliteral{29}{\isacharparenright}}\ Nested{\isaliteral{2E}{\isachardot}}term\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}f{\isaliteral{29}{\isacharparenright}}\ Nested{\isaliteral{2E}{\isachardot}}term}
+that recursively reverses the order of arguments of all function symbols in a
+  term. Prove that \isa{trev\ {\isaliteral{28}{\isacharparenleft}}trev\ t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ t}.
+\end{exercise}
+
+The experienced functional programmer may feel that our definition of
+\isa{subst} is too complicated in that \isa{substs} is
+unnecessary. The \isa{App}-case can be defined directly as
+\begin{isabelle}%
+\ \ \ \ \ subst\ s\ {\isaliteral{28}{\isacharparenleft}}App\ f\ ts{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ App\ f\ {\isaliteral{28}{\isacharparenleft}}map\ {\isaliteral{28}{\isacharparenleft}}subst\ s{\isaliteral{29}{\isacharparenright}}\ ts{\isaliteral{29}{\isacharparenright}}%
+\end{isabelle}
+where \isa{map} is the standard list function such that
+\isa{map\ f\ {\isaliteral{5B}{\isacharbrackleft}}x{\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2C}{\isacharcomma}}xn{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}f\ x{\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2C}{\isacharcomma}}f\ xn{\isaliteral{5D}{\isacharbrackright}}}. This is true, but Isabelle
+insists on the conjunctive format. Fortunately, we can easily \emph{prove}
+that the suggested equation holds:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isacommand{lemma}\isamarkupfalse%
+\ {\isaliteral{5B}{\isacharbrackleft}}simp{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}subst\ s\ {\isaliteral{28}{\isacharparenleft}}App\ f\ ts{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ App\ f\ {\isaliteral{28}{\isacharparenleft}}map\ {\isaliteral{28}{\isacharparenleft}}subst\ s{\isaliteral{29}{\isacharparenright}}\ ts{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{apply}\isamarkupfalse%
+{\isaliteral{28}{\isacharparenleft}}induct{\isaliteral{5F}{\isacharunderscore}}tac\ ts{\isaliteral{2C}{\isacharcomma}}\ simp{\isaliteral{5F}{\isacharunderscore}}all{\isaliteral{29}{\isacharparenright}}\isanewline
+\isacommand{done}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+\noindent
+What is more, we can now disable the old defining equation as a
+simplification rule:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{declare}\isamarkupfalse%
+\ subst{\isaliteral{5F}{\isacharunderscore}}App\ {\isaliteral{5B}{\isacharbrackleft}}simp\ del{\isaliteral{5D}{\isacharbrackright}}%
+\begin{isamarkuptext}%
+\noindent The advantage is that now we have replaced \isa{substs} by \isa{map}, we can profit from the large number of
+pre-proved lemmas about \isa{map}.  Unfortunately, inductive proofs
+about type \isa{term} are still awkward because they expect a
+conjunction. One could derive a new induction principle as well (see
+\S\ref{sec:derive-ind}), but simpler is to stop using
+\isacommand{primrec} and to define functions with \isacommand{fun}
+instead.  Simple uses of \isacommand{fun} are described in
+\S\ref{sec:fun} below.  Advanced applications, including functions
+over nested datatypes like \isa{term}, are discussed in a
+separate tutorial~\cite{isabelle-function}.
+
+Of course, you may also combine mutual and nested recursion of datatypes. For example,
+constructor \isa{Sum} in \S\ref{sec:datatype-mut-rec} could take a list of
+expressions as its argument: \isa{Sum}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a\ aexp\ list{\isaliteral{22}{\isachardoublequote}}}.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End: