src/HOL/Library/Tree_Multiset.thy
author wenzelm
Tue May 15 13:57:39 2018 +0200 (16 months ago)
changeset 68189 6163c90694ef
parent 66556 2d24e2c02130
child 68484 59793df7f853
permissions -rw-r--r--
tuned headers;
     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 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 
    22 lemma mset_tree_empty_iff[simp]: "mset_tree t = {#} \<longleftrightarrow> t = Leaf"
    23 by (cases t) auto
    24 
    25 lemma set_mset_tree[simp]: "set_mset (mset_tree t) = set_tree t"
    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 
    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 
    37 lemma mset_preorder[simp]: "mset (preorder t) = mset_tree t"
    38 by (induction t) (auto simp: ac_simps)
    39 
    40 lemma mset_inorder[simp]: "mset (inorder t) = mset_tree t"
    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 
    46 lemma in_subtrees_mset_iff[simp]: "s \<in># subtrees_mset t \<longleftrightarrow> s \<in> subtrees t"
    47 by(induction t) auto
    48 
    49 end