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