12 |
11 |
13 datatype 'a bt = |
12 datatype 'a bt = |
14 Lf |
13 Lf |
15 | Br 'a "'a bt" "'a bt" |
14 | Br 'a "'a bt" "'a bt" |
16 |
15 |
17 consts |
16 primrec n_nodes :: "'a bt => nat" where |
18 n_nodes :: "'a bt => nat" |
17 "n_nodes Lf = 0" |
19 n_leaves :: "'a bt => nat" |
18 | "n_nodes (Br a t1 t2) = Suc (n_nodes t1 + n_nodes t2)" |
20 depth :: "'a bt => nat" |
|
21 reflect :: "'a bt => 'a bt" |
|
22 bt_map :: "('a => 'b) => ('a bt => 'b bt)" |
|
23 preorder :: "'a bt => 'a list" |
|
24 inorder :: "'a bt => 'a list" |
|
25 postorder :: "'a bt => 'a list" |
|
26 append :: "'a bt => 'a bt => 'a bt" |
|
27 |
19 |
28 primrec |
20 primrec n_leaves :: "'a bt => nat" where |
29 "n_nodes Lf = 0" |
21 "n_leaves Lf = Suc 0" |
30 "n_nodes (Br a t1 t2) = Suc (n_nodes t1 + n_nodes t2)" |
22 | "n_leaves (Br a t1 t2) = n_leaves t1 + n_leaves t2" |
31 |
23 |
32 primrec |
24 primrec depth :: "'a bt => nat" where |
33 "n_leaves Lf = Suc 0" |
25 "depth Lf = 0" |
34 "n_leaves (Br a t1 t2) = n_leaves t1 + n_leaves t2" |
26 | "depth (Br a t1 t2) = Suc (max (depth t1) (depth t2))" |
35 |
27 |
36 primrec |
28 primrec reflect :: "'a bt => 'a bt" where |
37 "depth Lf = 0" |
29 "reflect Lf = Lf" |
38 "depth (Br a t1 t2) = Suc (max (depth t1) (depth t2))" |
30 | "reflect (Br a t1 t2) = Br a (reflect t2) (reflect t1)" |
39 |
31 |
40 primrec |
32 primrec bt_map :: "('a => 'b) => ('a bt => 'b bt)" where |
41 "reflect Lf = Lf" |
33 "bt_map f Lf = Lf" |
42 "reflect (Br a t1 t2) = Br a (reflect t2) (reflect t1)" |
34 | "bt_map f (Br a t1 t2) = Br (f a) (bt_map f t1) (bt_map f t2)" |
43 |
35 |
44 primrec |
36 primrec preorder :: "'a bt => 'a list" where |
45 "bt_map f Lf = Lf" |
37 "preorder Lf = []" |
46 "bt_map f (Br a t1 t2) = Br (f a) (bt_map f t1) (bt_map f t2)" |
38 | "preorder (Br a t1 t2) = [a] @ (preorder t1) @ (preorder t2)" |
47 |
39 |
48 primrec |
40 primrec inorder :: "'a bt => 'a list" where |
49 "preorder Lf = []" |
41 "inorder Lf = []" |
50 "preorder (Br a t1 t2) = [a] @ (preorder t1) @ (preorder t2)" |
42 | "inorder (Br a t1 t2) = (inorder t1) @ [a] @ (inorder t2)" |
51 |
43 |
52 primrec |
44 primrec postorder :: "'a bt => 'a list" where |
53 "inorder Lf = []" |
45 "postorder Lf = []" |
54 "inorder (Br a t1 t2) = (inorder t1) @ [a] @ (inorder t2)" |
46 | "postorder (Br a t1 t2) = (postorder t1) @ (postorder t2) @ [a]" |
55 |
47 |
56 primrec |
48 primrec append :: "'a bt => 'a bt => 'a bt" where |
57 "postorder Lf = []" |
|
58 "postorder (Br a t1 t2) = (postorder t1) @ (postorder t2) @ [a]" |
|
59 |
|
60 primrec |
|
61 "append Lf t = t" |
49 "append Lf t = t" |
62 "append (Br a t1 t2) t = Br a (append t1 t) (append t2 t)" |
50 | "append (Br a t1 t2) t = Br a (append t1 t) (append t2 t)" |
63 |
|
64 |
51 |
65 text {* \medskip BT simplification *} |
52 text {* \medskip BT simplification *} |
66 |
53 |
67 lemma n_leaves_reflect: "n_leaves (reflect t) = n_leaves t" |
54 lemma n_leaves_reflect: "n_leaves (reflect t) = n_leaves t" |
68 apply (induct t) |
55 apply (induct t) |