59928
|
1 |
(* Author: Tobias Nipkow *)
|
|
2 |
|
60500
|
3 |
section \<open>Multiset of Elements of Binary Tree\<close>
|
59928
|
4 |
|
|
5 |
theory Tree_Multiset
|
|
6 |
imports Multiset Tree
|
|
7 |
begin
|
|
8 |
|
68484
|
9 |
text \<open>
|
69593
|
10 |
Kept separate from theory \<^theory>\<open>HOL-Library.Tree\<close> to avoid importing all of theory \<^theory>\<open>HOL-Library.Multiset\<close> into \<^theory>\<open>HOL-Library.Tree\<close>. Should be merged if \<^theory>\<open>HOL-Library.Multiset\<close> ever becomes part of \<^theory>\<open>Main\<close>.
|
68484
|
11 |
\<close>
|
59928
|
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 |
|
63861
|
17 |
fun subtrees_mset :: "'a tree \<Rightarrow> 'a tree multiset" where
|
|
18 |
"subtrees_mset Leaf = {#Leaf#}" |
|
|
19 |
"subtrees_mset (Node l x r) = add_mset (Node l x r) (subtrees_mset l + subtrees_mset r)"
|
|
20 |
|
|
21 |
|
66556
|
22 |
lemma mset_tree_empty_iff[simp]: "mset_tree t = {#} \<longleftrightarrow> t = Leaf"
|
|
23 |
by (cases t) auto
|
|
24 |
|
60495
|
25 |
lemma set_mset_tree[simp]: "set_mset (mset_tree t) = set_tree t"
|
59928
|
26 |
by(induction t) auto
|
|
27 |
|
|
28 |
lemma size_mset_tree[simp]: "size(mset_tree t) = size t"
|
|
29 |
by(induction t) auto
|
|
30 |
|
|
31 |
lemma mset_map_tree: "mset_tree (map_tree f t) = image_mset f (mset_tree t)"
|
|
32 |
by (induction t) auto
|
|
33 |
|
60505
|
34 |
lemma mset_iff_set_tree: "x \<in># mset_tree t \<longleftrightarrow> x \<in> set_tree t"
|
|
35 |
by(induction t arbitrary: x) auto
|
|
36 |
|
60515
|
37 |
lemma mset_preorder[simp]: "mset (preorder t) = mset_tree t"
|
59928
|
38 |
by (induction t) (auto simp: ac_simps)
|
|
39 |
|
60515
|
40 |
lemma mset_inorder[simp]: "mset (inorder t) = mset_tree t"
|
59928
|
41 |
by (induction t) (auto simp: ac_simps)
|
|
42 |
|
|
43 |
lemma map_mirror: "mset_tree (mirror t) = mset_tree t"
|
|
44 |
by (induction t) (simp_all add: ac_simps)
|
|
45 |
|
63861
|
46 |
lemma in_subtrees_mset_iff[simp]: "s \<in># subtrees_mset t \<longleftrightarrow> s \<in> subtrees t"
|
|
47 |
by(induction t) auto
|
|
48 |
|
59928
|
49 |
end
|