3 \def\isabellecontext{Nested}%
18 \begin{isamarkuptext}%
19 \index{datatypes!and nested recursion}%
20 So far, all datatypes had the property that on the right-hand side of their
21 definition they occurred only at the top-level: directly below a
22 constructor. Now we consider \emph{nested recursion}, where the recursive
23 datatype occurs nested in some other datatype (but not inside itself!).
24 Consider the following model of terms
25 where function symbols can be applied to a list of arguments:%
28 \isacommand{datatype}\isamarkupfalse%
29 \ {\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}{\isachardoublequoteopen}term{\isachardoublequoteclose}\ {\isacharequal}\ Var\ {\isacharprime}v\ {\isacharbar}\ App\ {\isacharprime}f\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term\ list{\isachardoublequoteclose}%
30 \begin{isamarkuptext}%
32 Note that we need to quote \isa{term} on the left to avoid confusion with
33 the Isabelle command \isacommand{term}.
34 Parameter \isa{{\isacharprime}v} is the type of variables and \isa{{\isacharprime}f} the type of
36 A mathematical term like $f(x,g(y))$ becomes \isa{App\ f\ {\isacharbrackleft}Var\ x{\isacharcomma}\ App\ g\ {\isacharbrackleft}Var\ y{\isacharbrackright}{\isacharbrackright}}, where \isa{f}, \isa{g}, \isa{x}, \isa{y} are
37 suitable values, e.g.\ numbers or strings.
39 What complicates the definition of \isa{term} is the nested occurrence of
40 \isa{term} inside \isa{list} on the right-hand side. In principle,
41 nested recursion can be eliminated in favour of mutual recursion by unfolding
42 the offending datatypes, here \isa{list}. The result for \isa{term}
43 would be something like
46 \input{Datatype/document/unfoldnested.tex}
50 Although we do not recommend this unfolding to the user, it shows how to
51 simulate nested recursion by mutual recursion.
52 Now we return to the initial definition of \isa{term} using
55 Let us define a substitution function on terms. Because terms involve term
56 lists, we need to define two substitution functions simultaneously:%
59 \isacommand{primrec}\isamarkupfalse%
61 subst\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}v{\isasymRightarrow}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term\ \ \ \ \ \ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
62 substs{\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}v{\isasymRightarrow}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term\ list{\isachardoublequoteclose}\isanewline
63 \isakeyword{where}\isanewline
64 {\isachardoublequoteopen}subst\ s\ {\isacharparenleft}Var\ x{\isacharparenright}\ {\isacharequal}\ s\ x{\isachardoublequoteclose}\ {\isacharbar}\isanewline
65 \ \ subst{\isacharunderscore}App{\isacharcolon}\isanewline
66 {\isachardoublequoteopen}subst\ s\ {\isacharparenleft}App\ f\ ts{\isacharparenright}\ {\isacharequal}\ App\ f\ {\isacharparenleft}substs\ s\ ts{\isacharparenright}{\isachardoublequoteclose}\ {\isacharbar}\isanewline
68 {\isachardoublequoteopen}substs\ s\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\ {\isacharbar}\isanewline
69 {\isachardoublequoteopen}substs\ s\ {\isacharparenleft}t\ {\isacharhash}\ ts{\isacharparenright}\ {\isacharequal}\ subst\ s\ t\ {\isacharhash}\ substs\ s\ ts{\isachardoublequoteclose}%
70 \begin{isamarkuptext}%
72 Individual equations in a \commdx{primrec} definition may be
73 named as shown for \isa{subst{\isacharunderscore}App}.
74 The significance of this device will become apparent below.
76 Similarly, when proving a statement about terms inductively, we need
77 to prove a related statement about term lists simultaneously. For example,
78 the fact that the identity substitution does not change a term needs to be
79 strengthened and proved as follows:%
82 \isacommand{lemma}\isamarkupfalse%
83 \ subst{\isacharunderscore}id{\isacharcolon}\ {\isachardoublequoteopen}subst\ \ Var\ t\ \ {\isacharequal}\ {\isacharparenleft}t\ {\isacharcolon}{\isacharcolon}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term{\isacharparenright}\ \ {\isasymand}\isanewline
84 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ substs\ Var\ ts\ {\isacharequal}\ {\isacharparenleft}ts{\isacharcolon}{\isacharcolon}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term\ list{\isacharparenright}{\isachardoublequoteclose}\isanewline
91 \isacommand{apply}\isamarkupfalse%
92 {\isacharparenleft}induct{\isacharunderscore}tac\ t\ \isakeyword{and}\ ts{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline
93 \isacommand{done}\isamarkupfalse%
102 \begin{isamarkuptext}%
104 Note that \isa{Var} is the identity substitution because by definition it
105 leaves variables unchanged: \isa{subst\ Var\ {\isacharparenleft}Var\ x{\isacharparenright}\ {\isacharequal}\ Var\ x}. Note also
106 that the type annotations are necessary because otherwise there is nothing in
107 the goal to enforce that both halves of the goal talk about the same type
108 parameters \isa{{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}}. As a result, induction would fail
109 because the two halves of the goal would be unrelated.
112 The fact that substitution distributes over composition can be expressed
115 \ \ \ \ \ subst\ {\isacharparenleft}f\ {\isasymcirc}\ g{\isacharparenright}\ t\ {\isacharequal}\ subst\ f\ {\isacharparenleft}subst\ g\ t{\isacharparenright}%
117 Correct this statement (you will find that it does not type-check),
118 strengthen it, and prove it. (Note: \isa{{\isasymcirc}} is function composition;
119 its definition is found in theorem \isa{o{\isacharunderscore}def}).
121 \begin{exercise}\label{ex:trev-trev}
122 Define a function \isa{trev} of type \isa{{\isacharparenleft}{\isacharprime}v{\isacharcomma}\ {\isacharprime}f{\isacharparenright}\ Nested{\isachardot}term\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}\ {\isacharprime}f{\isacharparenright}\ Nested{\isachardot}term}
123 that recursively reverses the order of arguments of all function symbols in a
124 term. Prove that \isa{trev\ {\isacharparenleft}trev\ t{\isacharparenright}\ {\isacharequal}\ t}.
127 The experienced functional programmer may feel that our definition of
128 \isa{subst} is too complicated in that \isa{substs} is
129 unnecessary. The \isa{App}-case can be defined directly as
131 \ \ \ \ \ subst\ s\ {\isacharparenleft}App\ f\ ts{\isacharparenright}\ {\isacharequal}\ App\ f\ {\isacharparenleft}map\ {\isacharparenleft}subst\ s{\isacharparenright}\ ts{\isacharparenright}%
133 where \isa{map} is the standard list function such that
134 \isa{map\ f\ {\isacharbrackleft}x{\isadigit{1}}{\isacharcomma}{\isachardot}{\isachardot}{\isachardot}{\isacharcomma}xn{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}f\ x{\isadigit{1}}{\isacharcomma}{\isachardot}{\isachardot}{\isachardot}{\isacharcomma}f\ xn{\isacharbrackright}}. This is true, but Isabelle
135 insists on the conjunctive format. Fortunately, we can easily \emph{prove}
136 that the suggested equation holds:%
179 \isacommand{lemma}\isamarkupfalse%
180 \ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}subst\ s\ {\isacharparenleft}App\ f\ ts{\isacharparenright}\ {\isacharequal}\ App\ f\ {\isacharparenleft}map\ {\isacharparenleft}subst\ s{\isacharparenright}\ ts{\isacharparenright}{\isachardoublequoteclose}\isanewline
187 \isacommand{apply}\isamarkupfalse%
188 {\isacharparenleft}induct{\isacharunderscore}tac\ ts{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline
189 \isacommand{done}\isamarkupfalse%
198 \begin{isamarkuptext}%
200 What is more, we can now disable the old defining equation as a
201 simplification rule:%
204 \isacommand{declare}\isamarkupfalse%
205 \ subst{\isacharunderscore}App\ {\isacharbrackleft}simp\ del{\isacharbrackright}%
206 \begin{isamarkuptext}%
207 \noindent The advantage is that now we have replaced \isa{substs} by \isa{map}, we can profit from the large number of
208 pre-proved lemmas about \isa{map}. Unfortunately, inductive proofs
209 about type \isa{term} are still awkward because they expect a
210 conjunction. One could derive a new induction principle as well (see
211 \S\ref{sec:derive-ind}), but simpler is to stop using
212 \isacommand{primrec} and to define functions with \isacommand{fun}
213 instead. Simple uses of \isacommand{fun} are described in
214 \S\ref{sec:fun} below. Advanced applications, including functions
215 over nested datatypes like \isa{term}, are discussed in a
216 separate tutorial~\cite{isabelle-function}.
218 Of course, you may also combine mutual and nested recursion of datatypes. For example,
219 constructor \isa{Sum} in \S\ref{sec:datatype-mut-rec} could take a list of
220 expressions as its argument: \isa{Sum}~\isa{{\isachardoublequote}{\isacharprime}a\ aexp\ list{\isachardoublequote}}.%
239 %%% TeX-master: "root"