2 theory Nested imports ABexpr begin
6 \index{datatypes!and nested recursion}%
7 So far, all datatypes had the property that on the right-hand side of their
8 definition they occurred only at the top-level: directly below a
9 constructor. Now we consider \emph{nested recursion}, where the recursive
10 datatype occurs nested in some other datatype (but not inside itself!).
11 Consider the following model of terms
12 where function symbols can be applied to a list of arguments:
14 (*<*)hide_const Var(*>*)
15 datatype ('v,'f)"term" = Var 'v | App 'f "('v,'f)term list";
18 Note that we need to quote @{text term} on the left to avoid confusion with
19 the Isabelle command \isacommand{term}.
20 Parameter @{typ"'v"} is the type of variables and @{typ"'f"} the type of
22 A mathematical term like $f(x,g(y))$ becomes @{term"App f [Var x, App g
23 [Var y]]"}, where @{term f}, @{term g}, @{term x}, @{term y} are
24 suitable values, e.g.\ numbers or strings.
26 What complicates the definition of @{text term} is the nested occurrence of
27 @{text term} inside @{text list} on the right-hand side. In principle,
28 nested recursion can be eliminated in favour of mutual recursion by unfolding
29 the offending datatypes, here @{text list}. The result for @{text term}
30 would be something like
33 \input{Datatype/document/unfoldnested.tex}
37 Although we do not recommend this unfolding to the user, it shows how to
38 simulate nested recursion by mutual recursion.
39 Now we return to the initial definition of @{text term} using
42 Let us define a substitution function on terms. Because terms involve term
43 lists, we need to define two substitution functions simultaneously:
47 subst :: "('v\<Rightarrow>('v,'f)term) \<Rightarrow> ('v,'f)term \<Rightarrow> ('v,'f)term" and
48 substs:: "('v\<Rightarrow>('v,'f)term) \<Rightarrow> ('v,'f)term list \<Rightarrow> ('v,'f)term list"
50 "subst s (Var x) = s x" |
52 "subst s (App f ts) = App f (substs s ts)" |
55 "substs s (t # ts) = subst s t # substs s ts"
58 Individual equations in a \commdx{primrec} definition may be
59 named as shown for @{thm[source]subst_App}.
60 The significance of this device will become apparent below.
62 Similarly, when proving a statement about terms inductively, we need
63 to prove a related statement about term lists simultaneously. For example,
64 the fact that the identity substitution does not change a term needs to be
65 strengthened and proved as follows:
68 lemma subst_id(*<*)(*referred to from ABexpr*)(*>*): "subst Var t = (t ::('v,'f)term) \<and>
69 substs Var ts = (ts::('v,'f)term list)";
70 apply(induct_tac t and ts, simp_all);
74 Note that @{term Var} is the identity substitution because by definition it
75 leaves variables unchanged: @{prop"subst Var (Var x) = Var x"}. Note also
76 that the type annotations are necessary because otherwise there is nothing in
77 the goal to enforce that both halves of the goal talk about the same type
78 parameters @{text"('v,'f)"}. As a result, induction would fail
79 because the two halves of the goal would be unrelated.
82 The fact that substitution distributes over composition can be expressed
84 @{text[display]"subst (f \<circ> g) t = subst f (subst g t)"}
85 Correct this statement (you will find that it does not type-check),
86 strengthen it, and prove it. (Note: @{text"\<circ>"} is function composition;
87 its definition is found in theorem @{thm[source]o_def}).
89 \begin{exercise}\label{ex:trev-trev}
90 Define a function @{term trev} of type @{typ"('v,'f)term => ('v,'f)term"}
91 that recursively reverses the order of arguments of all function symbols in a
92 term. Prove that @{prop"trev(trev t) = t"}.
95 The experienced functional programmer may feel that our definition of
96 @{term subst} is too complicated in that @{const substs} is
97 unnecessary. The @{term App}-case can be defined directly as
98 @{term[display]"subst s (App f ts) = App f (map (subst s) ts)"}
99 where @{term"map"} is the standard list function such that
100 @{text"map f [x1,...,xn] = [f x1,...,f xn]"}. This is true, but Isabelle
101 insists on the conjunctive format. Fortunately, we can easily \emph{prove}
102 that the suggested equation holds:
106 lemma "subst ((subst f) \<circ> g) t = subst f (subst g t) \<and>
107 substs ((subst f) \<circ> g) ts = substs f (substs g ts)"
108 apply (induct_tac t and ts)
114 consts trev :: "('v,'f) term \<Rightarrow> ('v,'f) term"
115 trevs:: "('v,'f) term list \<Rightarrow> ('v,'f) term list"
117 "trev (Var v) = Var v"
118 "trev (App f ts) = App f (trevs ts)"
121 "trevs (t#ts) = (trevs ts) @ [(trev t)]"
123 lemma [simp]: "\<forall> ys. trevs (xs @ ys) = (trevs ys) @ (trevs xs)"
124 apply (induct_tac xs, auto)
127 lemma "trev (trev t) = (t::('v,'f)term) \<and>
128 trevs (trevs ts) = (ts::('v,'f)term list)"
129 apply (induct_tac t and ts, simp_all)
133 lemma [simp]: "subst s (App f ts) = App f (map (subst s) ts)"
134 apply(induct_tac ts, simp_all)
138 What is more, we can now disable the old defining equation as a
142 declare subst_App [simp del]
144 text{*\noindent The advantage is that now we have replaced @{const
145 substs} by @{const map}, we can profit from the large number of
146 pre-proved lemmas about @{const map}. Unfortunately, inductive proofs
147 about type @{text term} are still awkward because they expect a
148 conjunction. One could derive a new induction principle as well (see
149 \S\ref{sec:derive-ind}), but simpler is to stop using
150 \isacommand{primrec} and to define functions with \isacommand{fun}
151 instead. Simple uses of \isacommand{fun} are described in
152 \S\ref{sec:fun} below. Advanced applications, including functions
153 over nested datatypes like @{text term}, are discussed in a
154 separate tutorial~\cite{isabelle-function}.
156 Of course, you may also combine mutual and nested recursion of datatypes. For example,
157 constructor @{text Sum} in \S\ref{sec:datatype-mut-rec} could take a list of
158 expressions as its argument: @{text Sum}~@{typ[quotes]"'a aexp list"}.