src/HOL/Library/Tree_Multiset.thy
 author wenzelm Wed Jun 17 11:03:05 2015 +0200 (2015-06-17) changeset 60500 903bb1495239 parent 59928 b9b7f913a19a child 60502 aa58872267ee permissions -rw-r--r--
isabelle update_cartouches;
```     1 (* Author: Tobias Nipkow *)
```
```     2
```
```     3 section \<open>Multiset of Elements of Binary Tree\<close>
```
```     4
```
```     5 theory Tree_Multiset
```
```     6 imports Multiset Tree
```
```     7 begin
```
```     8
```
```     9 text\<open>Kept separate from theory @{theory Tree} to avoid importing all of
```
```    10 theory @{theory Multiset} into @{theory Tree}. Should be merged if
```
```    11 @{theory Multiset} ever becomes part of @{theory Main}.\<close>
```
```    12
```
```    13 fun mset_tree :: "'a tree \<Rightarrow> 'a multiset" where
```
```    14 "mset_tree Leaf = {#}" |
```
```    15 "mset_tree (Node l a r) = {#a#} + mset_tree l + mset_tree r"
```
```    16
```
```    17 lemma set_of_mset_tree[simp]: "set_of (mset_tree t) = set_tree t"
```
```    18 by(induction t) auto
```
```    19
```
```    20 lemma size_mset_tree[simp]: "size(mset_tree t) = size t"
```
```    21 by(induction t) auto
```
```    22
```
```    23 lemma mset_map_tree: "mset_tree (map_tree f t) = image_mset f (mset_tree t)"
```
```    24 by (induction t) auto
```
```    25
```
```    26 lemma multiset_of_preorder[simp]: "multiset_of (preorder t) = mset_tree t"
```
```    27 by (induction t) (auto simp: ac_simps)
```
```    28
```
```    29 lemma multiset_of_inorder[simp]: "multiset_of (inorder t) = mset_tree t"
```
```    30 by (induction t) (auto simp: ac_simps)
```
```    31
```
```    32 lemma map_mirror: "mset_tree (mirror t) = mset_tree t"
```
```    33 by (induction t) (simp_all add: ac_simps)
```
```    34
```
```    35 lemma del_rightmost_mset_tree:
```
```    36   "\<lbrakk> del_rightmost t = (t',x);  t \<noteq> \<langle>\<rangle> \<rbrakk> \<Longrightarrow> mset_tree t = {#x#} + mset_tree t'"
```
```    37 apply(induction t arbitrary: t' rule: del_rightmost.induct)
```
```    38 by (auto split: prod.splits) (auto simp: ac_simps)
```
```    39
```
```    40 end
```