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;
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@60500
     9
text\<open>Kept separate from theory @{theory Tree} to avoid importing all of
nipkow@59928
    10
theory @{theory Multiset} into @{theory Tree}. Should be merged if
wenzelm@60500
    11
@{theory Multiset} ever becomes part of @{theory Main}.\<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@59928
    17
lemma set_of_mset_tree[simp]: "set_of (mset_tree t) = set_tree t"
nipkow@59928
    18
by(induction t) auto
nipkow@59928
    19
nipkow@59928
    20
lemma size_mset_tree[simp]: "size(mset_tree t) = size t"
nipkow@59928
    21
by(induction t) auto
nipkow@59928
    22
nipkow@59928
    23
lemma mset_map_tree: "mset_tree (map_tree f t) = image_mset f (mset_tree t)"
nipkow@59928
    24
by (induction t) auto
nipkow@59928
    25
nipkow@59928
    26
lemma multiset_of_preorder[simp]: "multiset_of (preorder t) = mset_tree t"
nipkow@59928
    27
by (induction t) (auto simp: ac_simps)
nipkow@59928
    28
nipkow@59928
    29
lemma multiset_of_inorder[simp]: "multiset_of (inorder t) = mset_tree t"
nipkow@59928
    30
by (induction t) (auto simp: ac_simps)
nipkow@59928
    31
nipkow@59928
    32
lemma map_mirror: "mset_tree (mirror t) = mset_tree t"
nipkow@59928
    33
by (induction t) (simp_all add: ac_simps)
nipkow@59928
    34
nipkow@59928
    35
lemma del_rightmost_mset_tree:
nipkow@59928
    36
  "\<lbrakk> del_rightmost t = (t',x);  t \<noteq> \<langle>\<rangle> \<rbrakk> \<Longrightarrow> mset_tree t = {#x#} + mset_tree t'"
nipkow@59928
    37
apply(induction t arbitrary: t' rule: del_rightmost.induct)
nipkow@59928
    38
by (auto split: prod.splits) (auto simp: ac_simps)
nipkow@59928
    39
nipkow@59928
    40
end