1.1 --- a/doc-src/TutorialI/Datatype/document/Nested.tex	Wed Jan 24 11:59:15 2001 +0100
     1.2 +++ b/doc-src/TutorialI/Datatype/document/Nested.tex	Wed Jan 24 12:29:10 2001 +0100
     1.3 @@ -8,12 +8,12 @@
     1.4  constructor. This is not the case any longer for the following model of terms
     1.5  where function symbols can be applied to a list of arguments:%
     1.6  \end{isamarkuptext}%
     1.7 -\isacommand{datatype}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}{\isachardoublequote}term{\isachardoublequote}\ {\isacharequal}\ Var\ {\isacharprime}a\ {\isacharbar}\ App\ {\isacharprime}b\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term\ list{\isachardoublequote}%
     1.8 +\isacommand{datatype}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}{\isachardoublequote}term{\isachardoublequote}\ {\isacharequal}\ Var\ {\isacharprime}v\ {\isacharbar}\ App\ {\isacharprime}f\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term\ list{\isachardoublequote}%
     1.9  \begin{isamarkuptext}%
    1.10  \noindent
    1.11  Note that we need to quote \isa{term} on the left to avoid confusion with
    1.12  the Isabelle command \isacommand{term}.
    1.13 -Parameter \isa{{\isacharprime}a} is the type of variables and \isa{{\isacharprime}b} the type of
    1.14 +Parameter \isa{{\isacharprime}v} is the type of variables and \isa{{\isacharprime}f} the type of
    1.15  function symbols.
    1.16  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
    1.17  suitable values, e.g.\ numbers or strings.
    1.18 @@ -38,8 +38,8 @@
    1.19  lists, we need to define two substitution functions simultaneously:%
    1.20  \end{isamarkuptext}%
    1.21  \isacommand{consts}\isanewline
    1.22 -subst\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isasymRightarrow}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term\ \ \ \ \ \ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isachardoublequote}\isanewline
    1.23 -substs{\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isasymRightarrow}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term\ list{\isachardoublequote}\isanewline
    1.24 +subst\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\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{\isachardoublequote}\isanewline
    1.25 +substs{\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\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{\isachardoublequote}\isanewline
    1.26  \isanewline
    1.27  \isacommand{primrec}\isanewline
    1.28  \ \ {\isachardoublequote}subst\ s\ {\isacharparenleft}Var\ x{\isacharparenright}\ {\isacharequal}\ s\ x{\isachardoublequote}\isanewline
    1.29 @@ -58,8 +58,8 @@
    1.30  the fact that the identity substitution does not change a term needs to be
    1.31  strengthened and proved as follows:%
    1.32  \end{isamarkuptext}%
    1.33 -\isacommand{lemma}\ {\isachardoublequote}subst\ \ Var\ t\ \ {\isacharequal}\ {\isacharparenleft}t\ {\isacharcolon}{\isacharcolon}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isacharparenright}\ \ {\isasymand}\isanewline
    1.34 -\ \ \ \ \ \ \ \ substs\ Var\ ts\ {\isacharequal}\ {\isacharparenleft}ts{\isacharcolon}{\isacharcolon}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term\ list{\isacharparenright}{\isachardoublequote}\isanewline
    1.35 +\isacommand{lemma}\ {\isachardoublequote}subst\ \ Var\ t\ \ {\isacharequal}\ {\isacharparenleft}t\ {\isacharcolon}{\isacharcolon}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term{\isacharparenright}\ \ {\isasymand}\isanewline
    1.36 +\ \ \ \ \ \ \ \ substs\ Var\ ts\ {\isacharequal}\ {\isacharparenleft}ts{\isacharcolon}{\isacharcolon}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term\ list{\isacharparenright}{\isachardoublequote}\isanewline
    1.37  \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ t\ \isakeyword{and}\ ts{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline
    1.38  \isacommand{done}%
    1.39  \begin{isamarkuptext}%
    1.40 @@ -68,7 +68,7 @@
    1.41  leaves variables unchanged: \isa{subst\ Var\ {\isacharparenleft}Var\ x{\isacharparenright}\ {\isacharequal}\ Var\ x}. Note also
    1.42  that the type annotations are necessary because otherwise there is nothing in
    1.43  the goal to enforce that both halves of the goal talk about the same type
    1.44 -parameters \isa{{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}}. As a result, induction would fail
    1.45 +parameters \isa{{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}}. As a result, induction would fail
    1.46  because the two halves of the goal would be unrelated.
    1.47  
    1.48  \begin{exercise}
    1.49 @@ -82,7 +82,7 @@
    1.50  its definition is found in theorem \isa{o{\isacharunderscore}def}).
    1.51  \end{exercise}
    1.52  \begin{exercise}\label{ex:trev-trev}
    1.53 -  Define a function \isa{trev} of type \isa{{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}b{\isacharparenright}\ term\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}b{\isacharparenright}\ term}
    1.54 +  Define a function \isa{trev} of type \isa{{\isacharparenleft}{\isacharprime}v{\isacharcomma}\ {\isacharprime}f{\isacharparenright}\ term\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}\ {\isacharprime}f{\isacharparenright}\ term}
    1.55  that recursively reverses the order of arguments of all function symbols in a
    1.56    term. Prove that \isa{trev\ {\isacharparenleft}trev\ t{\isacharparenright}\ {\isacharequal}\ t}.
    1.57  \end{exercise}
    1.58 @@ -118,7 +118,7 @@
    1.59  and to define functions with \isacommand{recdef} instead.
    1.60  The details are explained in \S\ref{sec:nested-recdef} below.
    1.61  
    1.62 -Of course, you may also combine mutual and nested recursion. For example,
    1.63 +Of course, you may also combine mutual and nested recursion of datatypes. For example,
    1.64  constructor \isa{Sum} in \S\ref{sec:datatype-mut-rec} could take a list of
    1.65  expressions as its argument: \isa{Sum}~\isa{{\isachardoublequote}{\isacharprime}a\ aexp\ list{\isachardoublequote}}.%
    1.66  \end{isamarkuptext}%