--- a/doc-src/TutorialI/document/Nested.tex Tue Aug 28 13:15:15 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,240 +0,0 @@
-%
-\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: