9493
|
1 |
(*<*)
|
16417
|
2 |
theory Tree2 imports Tree begin
|
9493
|
3 |
(*>*)
|
|
4 |
|
|
5 |
text{*\noindent In Exercise~\ref{ex:Tree} we defined a function
|
9792
|
6 |
@{term"flatten"} from trees to lists. The straightforward version of
|
|
7 |
@{term"flatten"} is based on @{text"@"} and is thus, like @{term"rev"},
|
|
8 |
quadratic. A linear time version of @{term"flatten"} again reqires an extra
|
9493
|
9 |
argument, the accumulator: *}
|
|
10 |
|
13305
|
11 |
consts flatten2 :: "'a tree \<Rightarrow> 'a list \<Rightarrow> 'a list"
|
9493
|
12 |
(*<*)
|
|
13 |
primrec
|
|
14 |
"flatten2 Tip xs = xs"
|
|
15 |
"flatten2 (Node l x r) xs = flatten2 l (x#(flatten2 r xs))"
|
|
16 |
(*>*)
|
|
17 |
|
9792
|
18 |
text{*\noindent Define @{term"flatten2"} and prove
|
9493
|
19 |
*}
|
|
20 |
(*<*)
|
|
21 |
lemma [simp]: "!xs. flatten2 t xs = flatten t @ xs";
|
|
22 |
apply(induct_tac t);
|
|
23 |
by(auto);
|
|
24 |
(*>*)
|
|
25 |
lemma "flatten2 t [] = flatten t";
|
|
26 |
(*<*)
|
|
27 |
by(simp);
|
|
28 |
|
|
29 |
end
|
|
30 |
(*>*)
|