equal
deleted
inserted
replaced
221 lemma n_leaves_append [simp]: |
221 lemma n_leaves_append [simp]: |
222 "n_leaves (append t1 t2) = n_leaves t1 * n_leaves t2" |
222 "n_leaves (append t1 t2) = n_leaves t1 * n_leaves t2" |
223 apply (induct t1) |
223 apply (induct t1) |
224 apply (metis append.simps(1) n_leaves.simps(1) nat_mult_1 plus_nat.simps(1) |
224 apply (metis append.simps(1) n_leaves.simps(1) nat_mult_1 plus_nat.simps(1) |
225 Suc_eq_plus1) |
225 Suc_eq_plus1) |
226 by (simp add: left_distrib) |
226 by (simp add: distrib_right) |
227 |
227 |
228 lemma (*bt_map_append:*) |
228 lemma (*bt_map_append:*) |
229 "bt_map f (append t1 t2) = append (bt_map f t1) (bt_map f t2)" |
229 "bt_map f (append t1 t2) = append (bt_map f t1) (bt_map f t2)" |
230 apply (induct t1) |
230 apply (induct t1) |
231 apply (metis append.simps(1) bt_map.simps(1)) |
231 apply (metis append.simps(1) bt_map.simps(1)) |