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.
|
9541
|
19 |
A mathematical term like $f(x,g(y))$ becomes @{term"App f [Var x, App g
|
|
20 |
[Var y]]"}, where \isa{f}, \isa{g}, \isa{x}, \isa{y} are
|
8745
|
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"
|
9644
|
49 |
subst_App:
|
8745
|
50 |
"subst s (App f ts) = App f (substs s ts)"
|
|
51 |
|
|
52 |
"substs s [] = []"
|
|
53 |
"substs s (t # ts) = subst s t # substs s ts";
|
|
54 |
|
|
55 |
text{*\noindent
|
9644
|
56 |
You should ignore the label \isa{subst\_App} for the moment.
|
|
57 |
|
8745
|
58 |
Similarly, when proving a statement about terms inductively, we need
|
|
59 |
to prove a related statement about term lists simultaneously. For example,
|
|
60 |
the fact that the identity substitution does not change a term needs to be
|
|
61 |
strengthened and proved as follows:
|
|
62 |
*}
|
|
63 |
|
|
64 |
lemma "subst Var t = (t ::('a,'b)term) \\<and>
|
|
65 |
substs Var ts = (ts::('a,'b)term list)";
|
9458
|
66 |
by(induct_tac t and ts, auto);
|
8745
|
67 |
|
|
68 |
text{*\noindent
|
|
69 |
Note that \isa{Var} is the identity substitution because by definition it
|
9541
|
70 |
leaves variables unchanged: @{term"subst Var (Var x) = Var x"}. Note also
|
8745
|
71 |
that the type annotations are necessary because otherwise there is nothing in
|
|
72 |
the goal to enforce that both halves of the goal talk about the same type
|
|
73 |
parameters \isa{('a,'b)}. As a result, induction would fail
|
|
74 |
because the two halves of the goal would be unrelated.
|
|
75 |
|
|
76 |
\begin{exercise}
|
|
77 |
The fact that substitution distributes over composition can be expressed
|
|
78 |
roughly as follows:
|
|
79 |
\begin{ttbox}
|
|
80 |
subst (f o g) t = subst f (subst g t)
|
|
81 |
\end{ttbox}
|
|
82 |
Correct this statement (you will find that it does not type-check),
|
|
83 |
strengthen it, and prove it. (Note: \ttindexbold{o} is function composition;
|
|
84 |
its definition is found in theorem \isa{o_def}).
|
|
85 |
\end{exercise}
|
9644
|
86 |
\begin{exercise}\label{ex:trev-trev}
|
|
87 |
Define a function \isa{trev} of type @{typ"('a,'b)term => ('a,'b)term"} that
|
|
88 |
recursively reverses the order of arguments of all function symbols in a
|
|
89 |
term. Prove that \isa{trev(trev t) = t}.
|
|
90 |
\end{exercise}
|
|
91 |
|
|
92 |
The experienced functional programmer may feel that our above definition of
|
|
93 |
\isa{subst} is unnecessarily complicated in that \isa{substs} is completely
|
|
94 |
unnecessary. The @{term"App"}-case can be defined directly as
|
|
95 |
\begin{quote}
|
|
96 |
@{term[display]"subst s (App f ts) = App f (map (subst s) ts)"}
|
|
97 |
\end{quote}
|
|
98 |
where @{term"map"} is the standard list function such that
|
|
99 |
\isa{map f [x1,...,xn] = [f x1,...,f xn]}. This is true, but Isabelle insists
|
|
100 |
on the above fixed format. Fortunately, we can easily \emph{prove} that the
|
|
101 |
suggested equation holds:
|
|
102 |
*}
|
|
103 |
|
|
104 |
lemma [simp]: "subst s (App f ts) = App f (map (subst s) ts)"
|
|
105 |
by(induct_tac ts, auto)
|
|
106 |
|
|
107 |
text{*
|
|
108 |
What is more, we can now disable the old defining equation as a
|
|
109 |
simplification rule:
|
|
110 |
*}
|
|
111 |
|
|
112 |
lemmas [simp del] = subst_App
|
|
113 |
|
|
114 |
text{*
|
|
115 |
The advantage is that now we have replaced @{term"substs"} by @{term"map"},
|
|
116 |
we can profit from the large number of pre-proved lemmas about @{term"map"}.
|
|
117 |
We illustrate this with an example, reversing terms:
|
|
118 |
*}
|
|
119 |
|
|
120 |
consts trev :: "('a,'b)term => ('a,'b)term"
|
|
121 |
trevs :: "('a,'b)term list => ('a,'b)term list"
|
|
122 |
primrec "trev (Var x) = Var x"
|
|
123 |
trev_App: "trev (App f ts) = App f (trevs ts)"
|
|
124 |
|
|
125 |
"trevs [] = []"
|
|
126 |
"trevs (t#ts) = trevs ts @ [trev t]"
|
|
127 |
|
|
128 |
text{*\noindent
|
|
129 |
Following the above methodology, we re-express \isa{trev\_App}:
|
|
130 |
*}
|
|
131 |
|
|
132 |
lemma [simp]: "trev (App f ts) = App f (rev(map trev ts))"
|
|
133 |
by(induct_tac ts, auto)
|
|
134 |
lemmas [simp del] = trev_App
|
|
135 |
|
|
136 |
text{*\noindent
|
|
137 |
Now it becomes quite easy to prove @{term"trev(trev t) = t"}, except that we
|
|
138 |
still have to come up with the second half of the conjunction:
|
|
139 |
*}
|
|
140 |
|
|
141 |
lemma "trev(trev t) = (t::('a,'b)term) &
|
|
142 |
map trev (map trev ts) = (ts::('a,'b)term list)";
|
|
143 |
by(induct_tac t and ts, auto simp add:rev_map);
|
|
144 |
|
|
145 |
text{*\noindent
|
|
146 |
Getting rid of this second conjunct requires deriving a new induction schema
|
|
147 |
for \isa{term}, which is beyond what we have learned so far. Please stay
|
|
148 |
tuned, we will solve this final problem in \S\ref{sec:der-ind-schemas}.
|
8745
|
149 |
|
|
150 |
Of course, you may also combine mutual and nested recursion. For example,
|
|
151 |
constructor \isa{Sum} in \S\ref{sec:datatype-mut-rec} could take a list of
|
|
152 |
expressions as its argument: \isa{Sum "'a aexp list"}.
|
|
153 |
*}
|
|
154 |
(*<*)
|
|
155 |
end
|
|
156 |
(*>*)
|