8745
|
1 |
(*<*)
|
|
2 |
theory Nested = Main:;
|
|
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
|
|
8 |
constructor. This is not the case any longer for the following model of terms
|
|
9 |
where function symbols can be applied to a list of arguments:
|
|
10 |
*}
|
|
11 |
|
|
12 |
datatype ('a,'b)"term" = Var 'a | App 'b "('a,'b)term list";
|
|
13 |
|
|
14 |
text{*\noindent
|
|
15 |
Note that we need to quote \isa{term} on the left to avoid confusion with
|
|
16 |
the command \isacommand{term}.
|
|
17 |
Parameter \isa{'a} is the type of variables and \isa{'b} the type of
|
|
18 |
function symbols.
|
|
19 |
A mathematical term like $f(x,g(y))$ becomes \isa{App f [Var x, App g
|
|
20 |
[Var y]]}, where \isa{f}, \isa{g}, \isa{x}, \isa{y} are
|
|
21 |
suitable values, e.g.\ numbers or strings.
|
|
22 |
|
|
23 |
What complicates the definition of \isa{term} is the nested occurrence of
|
|
24 |
\isa{term} inside \isa{list} on the right-hand side. In principle,
|
|
25 |
nested recursion can be eliminated in favour of mutual recursion by unfolding
|
|
26 |
the offending datatypes, here \isa{list}. The result for \isa{term}
|
|
27 |
would be something like
|
8751
|
28 |
\medskip
|
|
29 |
|
|
30 |
\input{Datatype/document/unfoldnested.tex}
|
|
31 |
\medskip
|
|
32 |
|
|
33 |
\noindent
|
8745
|
34 |
Although we do not recommend this unfolding to the user, it shows how to
|
|
35 |
simulate nested recursion by mutual recursion.
|
|
36 |
Now we return to the initial definition of \isa{term} using
|
|
37 |
nested recursion.
|
|
38 |
|
|
39 |
Let us define a substitution function on terms. Because terms involve term
|
|
40 |
lists, we need to define two substitution functions simultaneously:
|
|
41 |
*}
|
|
42 |
|
|
43 |
consts
|
|
44 |
subst :: "('a\\<Rightarrow>('a,'b)term) \\<Rightarrow> ('a,'b)term \\<Rightarrow> ('a,'b)term"
|
|
45 |
substs:: "('a\\<Rightarrow>('a,'b)term) \\<Rightarrow> ('a,'b)term list \\<Rightarrow> ('a,'b)term list";
|
|
46 |
|
|
47 |
primrec
|
|
48 |
"subst s (Var x) = s x"
|
|
49 |
"subst s (App f ts) = App f (substs s ts)"
|
|
50 |
|
|
51 |
"substs s [] = []"
|
|
52 |
"substs s (t # ts) = subst s t # substs s ts";
|
|
53 |
|
|
54 |
text{*\noindent
|
|
55 |
Similarly, when proving a statement about terms inductively, we need
|
|
56 |
to prove a related statement about term lists simultaneously. For example,
|
|
57 |
the fact that the identity substitution does not change a term needs to be
|
|
58 |
strengthened and proved as follows:
|
|
59 |
*}
|
|
60 |
|
|
61 |
lemma "subst Var t = (t ::('a,'b)term) \\<and>
|
|
62 |
substs Var ts = (ts::('a,'b)term list)";
|
|
63 |
apply(induct_tac t and ts, auto).;
|
|
64 |
|
|
65 |
text{*\noindent
|
|
66 |
Note that \isa{Var} is the identity substitution because by definition it
|
|
67 |
leaves variables unchanged: \isa{subst Var (Var $x$) = Var $x$}. Note also
|
|
68 |
that the type annotations are necessary because otherwise there is nothing in
|
|
69 |
the goal to enforce that both halves of the goal talk about the same type
|
|
70 |
parameters \isa{('a,'b)}. As a result, induction would fail
|
|
71 |
because the two halves of the goal would be unrelated.
|
|
72 |
|
|
73 |
\begin{exercise}
|
|
74 |
The fact that substitution distributes over composition can be expressed
|
|
75 |
roughly as follows:
|
|
76 |
\begin{ttbox}
|
|
77 |
subst (f o g) t = subst f (subst g t)
|
|
78 |
\end{ttbox}
|
|
79 |
Correct this statement (you will find that it does not type-check),
|
|
80 |
strengthen it, and prove it. (Note: \ttindexbold{o} is function composition;
|
|
81 |
its definition is found in theorem \isa{o_def}).
|
|
82 |
\end{exercise}
|
|
83 |
|
|
84 |
Of course, you may also combine mutual and nested recursion. For example,
|
|
85 |
constructor \isa{Sum} in \S\ref{sec:datatype-mut-rec} could take a list of
|
|
86 |
expressions as its argument: \isa{Sum "'a aexp list"}.
|
|
87 |
*}
|
|
88 |
(*<*)
|
|
89 |
|
|
90 |
lemma "subst s (App f ts) = App f (map (subst s) ts)";
|
|
91 |
apply(induct_tac ts, auto).;
|
|
92 |
|
|
93 |
end
|
|
94 |
(*>*)
|