equal
deleted
inserted
replaced
21 reflect :: "'a bt => 'a bt" |
21 reflect :: "'a bt => 'a bt" |
22 bt_map :: "('a => 'b) => ('a bt => 'b bt)" |
22 bt_map :: "('a => 'b) => ('a bt => 'b bt)" |
23 preorder :: "'a bt => 'a list" |
23 preorder :: "'a bt => 'a list" |
24 inorder :: "'a bt => 'a list" |
24 inorder :: "'a bt => 'a list" |
25 postorder :: "'a bt => 'a list" |
25 postorder :: "'a bt => 'a list" |
26 append :: "'a bt => 'a bt => 'a bt" |
26 appnd :: "'a bt => 'a bt => 'a bt" |
27 |
27 |
28 primrec |
28 primrec |
29 "n_nodes Lf = 0" |
29 "n_nodes Lf = 0" |
30 "n_nodes (Br a t1 t2) = Suc (n_nodes t1 + n_nodes t2)" |
30 "n_nodes (Br a t1 t2) = Suc (n_nodes t1 + n_nodes t2)" |
31 |
31 |
56 primrec |
56 primrec |
57 "postorder Lf = []" |
57 "postorder Lf = []" |
58 "postorder (Br a t1 t2) = (postorder t1) @ (postorder t2) @ [a]" |
58 "postorder (Br a t1 t2) = (postorder t1) @ (postorder t2) @ [a]" |
59 |
59 |
60 primrec |
60 primrec |
61 "append Lf t = t" |
61 "appnd Lf t = t" |
62 "append (Br a t1 t2) t = Br a (append t1 t) (append t2 t)" |
62 "appnd (Br a t1 t2) t = Br a (appnd t1 t) (appnd t2 t)" |
63 |
63 |
64 |
64 |
65 text {* \medskip BT simplification *} |
65 text {* \medskip BT simplification *} |
66 |
66 |
67 lemma n_leaves_reflect: "n_leaves (reflect t) = n_leaves t" |
67 lemma n_leaves_reflect: "n_leaves (reflect t) = n_leaves t" |
141 text {* |
141 text {* |
142 Analogues of the standard properties of the append function for lists. |
142 Analogues of the standard properties of the append function for lists. |
143 *} |
143 *} |
144 |
144 |
145 lemma append_assoc [simp]: |
145 lemma append_assoc [simp]: |
146 "append (append t1 t2) t3 = append t1 (append t2 t3)" |
146 "appnd (appnd t1 t2) t3 = appnd t1 (appnd t2 t3)" |
147 apply (induct t1) |
147 apply (induct t1) |
148 apply simp_all |
148 apply simp_all |
149 done |
149 done |
150 |
150 |
151 lemma append_Lf2 [simp]: "append t Lf = t" |
151 lemma append_Lf2 [simp]: "appnd t Lf = t" |
152 apply (induct t) |
152 apply (induct t) |
153 apply simp_all |
153 apply simp_all |
154 done |
154 done |
155 |
155 |
156 lemma depth_append [simp]: "depth (append t1 t2) = depth t1 + depth t2" |
156 lemma depth_append [simp]: "depth (appnd t1 t2) = depth t1 + depth t2" |
157 apply (induct t1) |
157 apply (induct t1) |
158 apply (simp_all add: max_add_distrib_left) |
158 apply (simp_all add: max_add_distrib_left) |
159 done |
159 done |
160 |
160 |
161 lemma n_leaves_append [simp]: |
161 lemma n_leaves_append [simp]: |
162 "n_leaves (append t1 t2) = n_leaves t1 * n_leaves t2" |
162 "n_leaves (appnd t1 t2) = n_leaves t1 * n_leaves t2" |
163 apply (induct t1) |
163 apply (induct t1) |
164 apply (simp_all add: left_distrib) |
164 apply (simp_all add: left_distrib) |
165 done |
165 done |
166 |
166 |
167 lemma bt_map_append: |
167 lemma bt_map_append: |
168 "bt_map f (append t1 t2) = append (bt_map f t1) (bt_map f t2)" |
168 "bt_map f (appnd t1 t2) = appnd (bt_map f t1) (bt_map f t2)" |
169 apply (induct t1) |
169 apply (induct t1) |
170 apply simp_all |
170 apply simp_all |
171 done |
171 done |
172 |
172 |
173 end |
173 end |