equal
deleted
inserted
replaced
33 by (induction t) (auto simp: ac_simps) |
33 by (induction t) (auto simp: ac_simps) |
34 |
34 |
35 lemma map_mirror: "mset_tree (mirror t) = mset_tree t" |
35 lemma map_mirror: "mset_tree (mirror t) = mset_tree t" |
36 by (induction t) (simp_all add: ac_simps) |
36 by (induction t) (simp_all add: ac_simps) |
37 |
37 |
38 lemma del_rightmost_mset_tree: |
|
39 "\<lbrakk> del_rightmost t = (t',x); t \<noteq> \<langle>\<rangle> \<rbrakk> \<Longrightarrow> mset_tree t = {#x#} + mset_tree t'" |
|
40 apply(induction t arbitrary: t' rule: del_rightmost.induct) |
|
41 by (auto split: prod.splits) (auto simp: ac_simps) |
|
42 |
|
43 end |
38 end |