equal
deleted
inserted
replaced
262 |
262 |
263 lemma n_leaves_append [simp]: |
263 lemma n_leaves_append [simp]: |
264 "n_leaves (append t1 t2) = n_leaves t1 * n_leaves t2" |
264 "n_leaves (append t1 t2) = n_leaves t1 * n_leaves t2" |
265 apply (induct t1) |
265 apply (induct t1) |
266 apply (metis append.simps(1) n_leaves.simps(1) nat_mult_1 plus_nat.simps(1) |
266 apply (metis append.simps(1) n_leaves.simps(1) nat_mult_1 plus_nat.simps(1) |
267 semiring_norm(111)) |
267 Suc_eq_plus1) |
268 by (simp add: left_distrib) |
268 by (simp add: left_distrib) |
269 |
269 |
270 declare [[ sledgehammer_problem_prefix = "BT__bt_map_append" ]] |
270 declare [[ sledgehammer_problem_prefix = "BT__bt_map_append" ]] |
271 |
271 |
272 lemma (*bt_map_append:*) |
272 lemma (*bt_map_append:*) |