8745
|
1 |
(*<*)
|
16417
|
2 |
theory Tree imports Main begin
|
8745
|
3 |
(*>*)
|
|
4 |
|
|
5 |
text{*\noindent
|
11456
|
6 |
Define the datatype of \rmindex{binary trees}:
|
8745
|
7 |
*}
|
|
8 |
|
|
9 |
datatype 'a tree = Tip | Node "'a tree" 'a "'a tree";(*<*)
|
|
10 |
|
27015
|
11 |
primrec mirror :: "'a tree \<Rightarrow> 'a tree" where
|
|
12 |
"mirror Tip = Tip" |
|
9493
|
13 |
"mirror (Node l x r) = Node (mirror r) x (mirror l)";(*>*)
|
8745
|
14 |
|
|
15 |
text{*\noindent
|
11456
|
16 |
Define a function @{term"mirror"} that mirrors a binary tree
|
10795
|
17 |
by swapping subtrees recursively. Prove
|
8745
|
18 |
*}
|
|
19 |
|
|
20 |
lemma mirror_mirror: "mirror(mirror t) = t";
|
|
21 |
(*<*)
|
|
22 |
apply(induct_tac t);
|
9458
|
23 |
by(auto);
|
8745
|
24 |
|
27015
|
25 |
primrec flatten :: "'a tree => 'a list" where
|
|
26 |
"flatten Tip = []" |
|
9493
|
27 |
"flatten (Node l x r) = flatten l @ [x] @ flatten r";
|
|
28 |
(*>*)
|
|
29 |
|
|
30 |
text{*\noindent
|
9792
|
31 |
Define a function @{term"flatten"} that flattens a tree into a list
|
9493
|
32 |
by traversing it in infix order. Prove
|
|
33 |
*}
|
|
34 |
|
|
35 |
lemma "flatten(mirror t) = rev(flatten t)";
|
|
36 |
(*<*)
|
|
37 |
apply(induct_tac t);
|
|
38 |
by(auto);
|
|
39 |
|
8745
|
40 |
end
|
|
41 |
(*>*)
|