equal
deleted
inserted
replaced
6 Define the datatype of \rmindex{binary trees}: |
6 Define the datatype of \rmindex{binary trees}: |
7 *} |
7 *} |
8 |
8 |
9 datatype 'a tree = Tip | Node "'a tree" 'a "'a tree";(*<*) |
9 datatype 'a tree = Tip | Node "'a tree" 'a "'a tree";(*<*) |
10 |
10 |
11 consts mirror :: "'a tree \<Rightarrow> 'a tree"; |
11 primrec mirror :: "'a tree \<Rightarrow> 'a tree" where |
12 primrec |
12 "mirror Tip = Tip" | |
13 "mirror Tip = Tip" |
|
14 "mirror (Node l x r) = Node (mirror r) x (mirror l)";(*>*) |
13 "mirror (Node l x r) = Node (mirror r) x (mirror l)";(*>*) |
15 |
14 |
16 text{*\noindent |
15 text{*\noindent |
17 Define a function @{term"mirror"} that mirrors a binary tree |
16 Define a function @{term"mirror"} that mirrors a binary tree |
18 by swapping subtrees recursively. Prove |
17 by swapping subtrees recursively. Prove |
21 lemma mirror_mirror: "mirror(mirror t) = t"; |
20 lemma mirror_mirror: "mirror(mirror t) = t"; |
22 (*<*) |
21 (*<*) |
23 apply(induct_tac t); |
22 apply(induct_tac t); |
24 by(auto); |
23 by(auto); |
25 |
24 |
26 consts flatten :: "'a tree => 'a list" |
25 primrec flatten :: "'a tree => 'a list" where |
27 primrec |
26 "flatten Tip = []" | |
28 "flatten Tip = []" |
|
29 "flatten (Node l x r) = flatten l @ [x] @ flatten r"; |
27 "flatten (Node l x r) = flatten l @ [x] @ flatten r"; |
30 (*>*) |
28 (*>*) |
31 |
29 |
32 text{*\noindent |
30 text{*\noindent |
33 Define a function @{term"flatten"} that flattens a tree into a list |
31 Define a function @{term"flatten"} that flattens a tree into a list |