src/HOL/Library/Tree_Multiset.thy
 author haftmann Wed Jul 18 20:51:21 2018 +0200 (11 months ago) changeset 68658 16cc1161ad7f parent 68484 59793df7f853 child 69593 3dda49e08b9d permissions -rw-r--r--
tuned equation
```     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>
```
```    10   Kept separate from theory @{theory "HOL-Library.Tree"} to avoid importing all of theory @{theory
```
```    11   "HOL-Library.Multiset"} into @{theory "HOL-Library.Tree"}. Should be merged if @{theory
```
```    12   "HOL-Library.Multiset"} ever becomes part of @{theory Main}.
```
```    13 \<close>
```
```    14
```
```    15 fun mset_tree :: "'a tree \<Rightarrow> 'a multiset" where
```
```    16 "mset_tree Leaf = {#}" |
```
```    17 "mset_tree (Node l a r) = {#a#} + mset_tree l + mset_tree r"
```
```    18
```
```    19 fun subtrees_mset :: "'a tree \<Rightarrow> 'a tree multiset" where
```
```    20 "subtrees_mset Leaf = {#Leaf#}" |
```
```    21 "subtrees_mset (Node l x r) = add_mset (Node l x r) (subtrees_mset l + subtrees_mset r)"
```
```    22
```
```    23
```
```    24 lemma mset_tree_empty_iff[simp]: "mset_tree t = {#} \<longleftrightarrow> t = Leaf"
```
```    25 by (cases t) auto
```
```    26
```
```    27 lemma set_mset_tree[simp]: "set_mset (mset_tree t) = set_tree t"
```
```    28 by(induction t) auto
```
```    29
```
```    30 lemma size_mset_tree[simp]: "size(mset_tree t) = size t"
```
```    31 by(induction t) auto
```
```    32
```
```    33 lemma mset_map_tree: "mset_tree (map_tree f t) = image_mset f (mset_tree t)"
```
```    34 by (induction t) auto
```
```    35
```
```    36 lemma mset_iff_set_tree: "x \<in># mset_tree t \<longleftrightarrow> x \<in> set_tree t"
```
```    37 by(induction t arbitrary: x) auto
```
```    38
```
```    39 lemma mset_preorder[simp]: "mset (preorder t) = mset_tree t"
```
```    40 by (induction t) (auto simp: ac_simps)
```
```    41
```
```    42 lemma mset_inorder[simp]: "mset (inorder t) = mset_tree t"
```
```    43 by (induction t) (auto simp: ac_simps)
```
```    44
```
```    45 lemma map_mirror: "mset_tree (mirror t) = mset_tree t"
```
```    46 by (induction t) (simp_all add: ac_simps)
```
```    47
```
```    48 lemma in_subtrees_mset_iff[simp]: "s \<in># subtrees_mset t \<longleftrightarrow> s \<in> subtrees t"
```
```    49 by(induction t) auto
```
```    50
```
```    51 end
```