8745
|
1 |
(*<*)
|
9792
|
2 |
theory Nested = ABexpr:
|
8745
|
3 |
(*>*)
|
|
4 |
|
|
5 |
text{*
|
|
6 |
So far, all datatypes had the property that on the right-hand side of their
|
|
7 |
definition they occurred only at the top-level, i.e.\ directly below a
|
11256
|
8 |
constructor. Now we consider \emph{nested recursion}, where the recursive
|
11310
|
9 |
datatype occurs nested in some other datatype (but not inside itself!).
|
11256
|
10 |
Consider the following model of terms
|
8745
|
11 |
where function symbols can be applied to a list of arguments:
|
|
12 |
*}
|
9933
|
13 |
(*<*)hide const Var(*>*)
|
10971
|
14 |
datatype ('v,'f)"term" = Var 'v | App 'f "('v,'f)term list";
|
8745
|
15 |
|
|
16 |
text{*\noindent
|
10171
|
17 |
Note that we need to quote @{text term} on the left to avoid confusion with
|
|
18 |
the Isabelle command \isacommand{term}.
|
10971
|
19 |
Parameter @{typ"'v"} is the type of variables and @{typ"'f"} the type of
|
8745
|
20 |
function symbols.
|
9541
|
21 |
A mathematical term like $f(x,g(y))$ becomes @{term"App f [Var x, App g
|
10171
|
22 |
[Var y]]"}, where @{term f}, @{term g}, @{term x}, @{term y} are
|
8745
|
23 |
suitable values, e.g.\ numbers or strings.
|
|
24 |
|
10171
|
25 |
What complicates the definition of @{text term} is the nested occurrence of
|
|
26 |
@{text term} inside @{text list} on the right-hand side. In principle,
|
8745
|
27 |
nested recursion can be eliminated in favour of mutual recursion by unfolding
|
10171
|
28 |
the offending datatypes, here @{text list}. The result for @{text term}
|
8745
|
29 |
would be something like
|
8751
|
30 |
\medskip
|
|
31 |
|
|
32 |
\input{Datatype/document/unfoldnested.tex}
|
|
33 |
\medskip
|
|
34 |
|
|
35 |
\noindent
|
8745
|
36 |
Although we do not recommend this unfolding to the user, it shows how to
|
|
37 |
simulate nested recursion by mutual recursion.
|
10171
|
38 |
Now we return to the initial definition of @{text term} using
|
8745
|
39 |
nested recursion.
|
|
40 |
|
|
41 |
Let us define a substitution function on terms. Because terms involve term
|
|
42 |
lists, we need to define two substitution functions simultaneously:
|
|
43 |
*}
|
|
44 |
|
|
45 |
consts
|
10971
|
46 |
subst :: "('v\<Rightarrow>('v,'f)term) \<Rightarrow> ('v,'f)term \<Rightarrow> ('v,'f)term"
|
|
47 |
substs:: "('v\<Rightarrow>('v,'f)term) \<Rightarrow> ('v,'f)term list \<Rightarrow> ('v,'f)term list";
|
8745
|
48 |
|
|
49 |
primrec
|
|
50 |
"subst s (Var x) = s x"
|
9644
|
51 |
subst_App:
|
8745
|
52 |
"subst s (App f ts) = App f (substs s ts)"
|
|
53 |
|
|
54 |
"substs s [] = []"
|
|
55 |
"substs s (t # ts) = subst s t # substs s ts";
|
|
56 |
|
|
57 |
text{*\noindent
|
10171
|
58 |
Individual equations in a primrec definition may be named as shown for @{thm[source]subst_App}.
|
|
59 |
The significance of this device will become apparent below.
|
9644
|
60 |
|
8745
|
61 |
Similarly, when proving a statement about terms inductively, we need
|
|
62 |
to prove a related statement about term lists simultaneously. For example,
|
|
63 |
the fact that the identity substitution does not change a term needs to be
|
|
64 |
strengthened and proved as follows:
|
|
65 |
*}
|
|
66 |
|
10971
|
67 |
lemma "subst Var t = (t ::('v,'f)term) \<and>
|
|
68 |
substs Var ts = (ts::('v,'f)term list)";
|
10171
|
69 |
apply(induct_tac t and ts, simp_all);
|
|
70 |
done
|
8745
|
71 |
|
|
72 |
text{*\noindent
|
10171
|
73 |
Note that @{term Var} is the identity substitution because by definition it
|
9792
|
74 |
leaves variables unchanged: @{prop"subst Var (Var x) = Var x"}. Note also
|
8745
|
75 |
that the type annotations are necessary because otherwise there is nothing in
|
|
76 |
the goal to enforce that both halves of the goal talk about the same type
|
10971
|
77 |
parameters @{text"('v,'f)"}. As a result, induction would fail
|
8745
|
78 |
because the two halves of the goal would be unrelated.
|
|
79 |
|
|
80 |
\begin{exercise}
|
|
81 |
The fact that substitution distributes over composition can be expressed
|
|
82 |
roughly as follows:
|
10178
|
83 |
@{text[display]"subst (f \<circ> g) t = subst f (subst g t)"}
|
8745
|
84 |
Correct this statement (you will find that it does not type-check),
|
10178
|
85 |
strengthen it, and prove it. (Note: @{text"\<circ>"} is function composition;
|
9792
|
86 |
its definition is found in theorem @{thm[source]o_def}).
|
8745
|
87 |
\end{exercise}
|
9644
|
88 |
\begin{exercise}\label{ex:trev-trev}
|
10971
|
89 |
Define a function @{term trev} of type @{typ"('v,'f)term => ('v,'f)term"}
|
9792
|
90 |
that recursively reverses the order of arguments of all function symbols in a
|
|
91 |
term. Prove that @{prop"trev(trev t) = t"}.
|
9644
|
92 |
\end{exercise}
|
|
93 |
|
10795
|
94 |
The experienced functional programmer may feel that our definition of
|
|
95 |
@{term subst} is too complicated in that @{term substs} is
|
|
96 |
unnecessary. The @{term App}-case can be defined directly as
|
9644
|
97 |
@{term[display]"subst s (App f ts) = App f (map (subst s) ts)"}
|
|
98 |
where @{term"map"} is the standard list function such that
|
9792
|
99 |
@{text"map f [x1,...,xn] = [f x1,...,f xn]"}. This is true, but Isabelle
|
10795
|
100 |
insists on the conjunctive format. Fortunately, we can easily \emph{prove}
|
9792
|
101 |
that the suggested equation holds:
|
9644
|
102 |
*}
|
|
103 |
|
|
104 |
lemma [simp]: "subst s (App f ts) = App f (map (subst s) ts)"
|
10171
|
105 |
apply(induct_tac ts, simp_all)
|
|
106 |
done
|
9644
|
107 |
|
9689
|
108 |
text{*\noindent
|
9644
|
109 |
What is more, we can now disable the old defining equation as a
|
|
110 |
simplification rule:
|
|
111 |
*}
|
|
112 |
|
9933
|
113 |
declare subst_App [simp del]
|
9644
|
114 |
|
|
115 |
text{*\noindent
|
10171
|
116 |
The advantage is that now we have replaced @{term substs} by
|
|
117 |
@{term map}, we can profit from the large number of pre-proved lemmas
|
|
118 |
about @{term map}. Unfortunately inductive proofs about type
|
|
119 |
@{text term} are still awkward because they expect a conjunction. One
|
9689
|
120 |
could derive a new induction principle as well (see
|
10795
|
121 |
\S\ref{sec:derive-ind}), but simpler is to stop using \isacommand{primrec}
|
|
122 |
and to define functions with \isacommand{recdef} instead.
|
11309
|
123 |
Simple uses of \isacommand{recdef} are described in \S\ref{sec:recdef} below,
|
|
124 |
and later (\S\ref{sec:nested-recdef}) we shall see how \isacommand{recdef} can
|
|
125 |
handle nested recursion.
|
8745
|
126 |
|
10971
|
127 |
Of course, you may also combine mutual and nested recursion of datatypes. For example,
|
10171
|
128 |
constructor @{text Sum} in \S\ref{sec:datatype-mut-rec} could take a list of
|
|
129 |
expressions as its argument: @{text Sum}~@{typ[quotes]"'a aexp list"}.
|
8745
|
130 |
*}
|
|
131 |
(*<*)
|
|
132 |
end
|
11256
|
133 |
(*>*)
|