18 preorder :: 'a bt => 'a list |
18 preorder :: 'a bt => 'a list |
19 inorder :: 'a bt => 'a list |
19 inorder :: 'a bt => 'a list |
20 postorder :: 'a bt => 'a list |
20 postorder :: 'a bt => 'a list |
21 |
21 |
22 primrec n_nodes bt |
22 primrec n_nodes bt |
23 n_nodes_Lf "n_nodes (Lf) = 0" |
23 "n_nodes (Lf) = 0" |
24 n_nodes_Br "n_nodes (Br a t1 t2) = Suc(n_nodes t1 + n_nodes t2)" |
24 "n_nodes (Br a t1 t2) = Suc(n_nodes t1 + n_nodes t2)" |
25 |
25 |
26 primrec n_leaves bt |
26 primrec n_leaves bt |
27 n_leaves_Lf "n_leaves (Lf) = Suc 0" |
27 "n_leaves (Lf) = Suc 0" |
28 n_leaves_Br "n_leaves (Br a t1 t2) = n_leaves t1 + n_leaves t2" |
28 "n_leaves (Br a t1 t2) = n_leaves t1 + n_leaves t2" |
29 |
29 |
30 primrec reflect bt |
30 primrec reflect bt |
31 reflect_Lf "reflect (Lf) = Lf" |
31 "reflect (Lf) = Lf" |
32 reflect_Br "reflect (Br a t1 t2) = Br a (reflect t2) (reflect t1)" |
32 "reflect (Br a t1 t2) = Br a (reflect t2) (reflect t1)" |
33 |
33 |
34 primrec bt_map bt |
34 primrec bt_map bt |
35 bt_map_Lf "bt_map f Lf = Lf" |
35 "bt_map f Lf = Lf" |
36 bt_map_Br "bt_map f (Br a t1 t2) = Br (f a) (bt_map f t1) (bt_map f t2)" |
36 "bt_map f (Br a t1 t2) = Br (f a) (bt_map f t1) (bt_map f t2)" |
37 |
37 |
38 primrec preorder bt |
38 primrec preorder bt |
39 preorder_Lf "preorder (Lf) = []" |
39 "preorder (Lf) = []" |
40 preorder_Br "preorder (Br a t1 t2) = [a] @ (preorder t1) @ (preorder t2)" |
40 "preorder (Br a t1 t2) = [a] @ (preorder t1) @ (preorder t2)" |
41 |
41 |
42 primrec inorder bt |
42 primrec inorder bt |
43 inorder_Lf "inorder (Lf) = []" |
43 "inorder (Lf) = []" |
44 inorder_Br "inorder (Br a t1 t2) = (inorder t1) @ [a] @ (inorder t2)" |
44 "inorder (Br a t1 t2) = (inorder t1) @ [a] @ (inorder t2)" |
45 |
45 |
46 primrec postorder bt |
46 primrec postorder bt |
47 postorder_Lf "postorder (Lf) = []" |
47 "postorder (Lf) = []" |
48 postorder_Br "postorder (Br a t1 t2) = (postorder t1) @ (postorder t2) @ [a]" |
48 "postorder (Br a t1 t2) = (postorder t1) @ (postorder t2) @ [a]" |
49 |
49 |
50 end |
50 end |
|
51 |