src/HOL/Library/Tree_Multiset.thy
author haftmann
Fri Mar 22 19:18:08 2019 +0000 (4 months ago)
changeset 69946 494934c30f38
parent 69593 3dda49e08b9d
permissions -rw-r--r--
improved code equations taken over from AFP
nipkow@59928
     1
(* Author: Tobias Nipkow *)
nipkow@59928
     2
wenzelm@60500
     3
section \<open>Multiset of Elements of Binary Tree\<close>
nipkow@59928
     4
nipkow@59928
     5
theory Tree_Multiset
nipkow@59928
     6
imports Multiset Tree
nipkow@59928
     7
begin
nipkow@59928
     8
wenzelm@68484
     9
text \<open>
wenzelm@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>.
wenzelm@68484
    11
\<close>
nipkow@59928
    12
nipkow@59928
    13
fun mset_tree :: "'a tree \<Rightarrow> 'a multiset" where
nipkow@59928
    14
"mset_tree Leaf = {#}" |
nipkow@59928
    15
"mset_tree (Node l a r) = {#a#} + mset_tree l + mset_tree r"
nipkow@59928
    16
nipkow@63861
    17
fun subtrees_mset :: "'a tree \<Rightarrow> 'a tree multiset" where
nipkow@63861
    18
"subtrees_mset Leaf = {#Leaf#}" |
nipkow@63861
    19
"subtrees_mset (Node l x r) = add_mset (Node l x r) (subtrees_mset l + subtrees_mset r)"
nipkow@63861
    20
nipkow@63861
    21
nipkow@66556
    22
lemma mset_tree_empty_iff[simp]: "mset_tree t = {#} \<longleftrightarrow> t = Leaf"
nipkow@66556
    23
by (cases t) auto
nipkow@66556
    24
nipkow@60495
    25
lemma set_mset_tree[simp]: "set_mset (mset_tree t) = set_tree t"
nipkow@59928
    26
by(induction t) auto
nipkow@59928
    27
nipkow@59928
    28
lemma size_mset_tree[simp]: "size(mset_tree t) = size t"
nipkow@59928
    29
by(induction t) auto
nipkow@59928
    30
nipkow@59928
    31
lemma mset_map_tree: "mset_tree (map_tree f t) = image_mset f (mset_tree t)"
nipkow@59928
    32
by (induction t) auto
nipkow@59928
    33
nipkow@60505
    34
lemma mset_iff_set_tree: "x \<in># mset_tree t \<longleftrightarrow> x \<in> set_tree t"
nipkow@60505
    35
by(induction t arbitrary: x) auto
nipkow@60505
    36
nipkow@60515
    37
lemma mset_preorder[simp]: "mset (preorder t) = mset_tree t"
nipkow@59928
    38
by (induction t) (auto simp: ac_simps)
nipkow@59928
    39
nipkow@60515
    40
lemma mset_inorder[simp]: "mset (inorder t) = mset_tree t"
nipkow@59928
    41
by (induction t) (auto simp: ac_simps)
nipkow@59928
    42
nipkow@59928
    43
lemma map_mirror: "mset_tree (mirror t) = mset_tree t"
nipkow@59928
    44
by (induction t) (simp_all add: ac_simps)
nipkow@59928
    45
nipkow@63861
    46
lemma in_subtrees_mset_iff[simp]: "s \<in># subtrees_mset t \<longleftrightarrow> s \<in> subtrees t"
nipkow@63861
    47
by(induction t) auto
nipkow@63861
    48
nipkow@59928
    49
end