doc-src/TutorialI/Datatype/Nested.thy

XSYMBOL_INSTALLFONTS is back;

(*<*)
theory Nested = ABexpr:
(*>*)

text{*
So far, all datatypes had the property that on the right-hand side of their
definition they occurred only at the top-level, i.e.\ directly below a
constructor. This is not the case any longer for the following model of terms
where function symbols can be applied to a list of arguments:
*}
(*<*)hide const Var(*>*)
datatype ('a,'b)"term" = Var 'a | App 'b "('a,'b)term list";

text{*\noindent
Note that we need to quote @{text"term"} on the left to avoid confusion with
the command \isacommand{term}.
Parameter @{typ"'a"} is the type of variables and @{typ"'b"} the type of
function symbols.
A mathematical term like $f(x,g(y))$ becomes @{term"App f [Var x, App g
  [Var y]]"}, where @{term"f"}, @{term"g"}, @{term"x"}, @{term"y"} are
suitable values, e.g.\ numbers or strings.

What complicates the definition of @{text"term"} is the nested occurrence of
@{text"term"} inside @{text"list"} on the right-hand side. In principle,
nested recursion can be eliminated in favour of mutual recursion by unfolding
the offending datatypes, here @{text"list"}. The result for @{text"term"}
would be something like
\medskip

\input{Datatype/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 @{text"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:
*}

consts
subst :: "('a\\<Rightarrow>('a,'b)term) \\<Rightarrow> ('a,'b)term      \\<Rightarrow> ('a,'b)term"
substs:: "('a\\<Rightarrow>('a,'b)term) \\<Rightarrow> ('a,'b)term list \\<Rightarrow> ('a,'b)term list";

primrec
  "subst s (Var x) = s x"
  subst_App:
  "subst s (App f ts) = App f (substs s ts)"

  "substs s [] = []"
  "substs s (t # ts) = subst s t # substs s ts";

text{*\noindent
(Please ignore the label @{thm[source]subst_App} for the moment.)

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:
*}

lemma "subst  Var t  = (t ::('a,'b)term)  \\<and>
        substs Var ts = (ts::('a,'b)term list)";
by(induct_tac t and ts, simp_all);

text{*\noindent
Note that @{term"Var"} is the identity substitution because by definition it
leaves variables unchanged: @{prop"subst Var (Var x) = 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 @{text"('a,'b)"}. 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:
@{text[display]"subst (f o g) t = subst f (subst g t)"}
Correct this statement (you will find that it does not type-check),
strengthen it, and prove it. (Note: \isaindexbold{o} is function composition;
its definition is found in theorem @{thm[source]o_def}).
\end{exercise}
\begin{exercise}\label{ex:trev-trev}
  Define a function @{text"trev"} of type @{typ"('a,'b)term => ('a,'b)term"}
that recursively reverses the order of arguments of all function symbols in a
  term. Prove that @{prop"trev(trev t) = t"}.
\end{exercise}

The experienced functional programmer may feel that our above definition of
@{term"subst"} is unnecessarily complicated in that @{term"substs"} is
completely unnecessary. The @{term"App"}-case can be defined directly as
@{term[display]"subst s (App f ts) = App f (map (subst s) ts)"}
where @{term"map"} is the standard list function such that
@{text"map f [x1,...,xn] = [f x1,...,f xn]"}. This is true, but Isabelle
insists on the above fixed format. Fortunately, we can easily \emph{prove}
that the suggested equation holds:
*}

lemma [simp]: "subst s (App f ts) = App f (map (subst s) ts)"
by(induct_tac ts, simp_all)

text{*\noindent
What is more, we can now disable the old defining equation as a
simplification rule:
*}

declare subst_App [simp del]

text{*\noindent
The advantage is that now we have replaced @{term"substs"} by
@{term"map"}, we can profit from the large number of pre-proved lemmas
about @{term"map"}.  Unfortunately inductive proofs about type
@{text"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 turns out to be simpler to define
functions by \isacommand{recdef} instead of \isacommand{primrec}.
The details are explained in \S\ref{sec:advanced-recdef} below.

Of course, you may also combine mutual and nested recursion. For example,
constructor @{text"Sum"} in \S\ref{sec:datatype-mut-rec} could take a list of
expressions as its argument: @{text"Sum"}~@{typ[quotes]"'a aexp list"}.
*}
(*<*)
end
(*>*)