new theory Library/Tree_Multiset.thy

--- a/src/HOL/Library/Library.thy	Sat Apr 04 22:22:38 2015 +0200
+++ b/src/HOL/Library/Library.thy	Mon Apr 06 15:23:50 2015 +0200
@@ -71,7 +71,7 @@
   Sublist
   Sum_of_Squares
   Transitive_Closure_Table
-  Tree
+  Tree_Multiset
   While_Combinator
 begin
 end

--- a/src/HOL/Library/Tree.thy	Sat Apr 04 22:22:38 2015 +0200
+++ b/src/HOL/Library/Tree.thy	Mon Apr 06 15:23:50 2015 +0200
@@ -98,9 +98,6 @@
 "bst \<langle>\<rangle> \<longleftrightarrow> True" |
 "bst \<langle>l, a, r\<rangle> \<longleftrightarrow> bst l \<and> bst r \<and> (\<forall>x\<in>set_tree l. x < a) \<and> (\<forall>x\<in>set_tree r. a < x)"
 
-lemma (in linorder) bst_imp_sorted: "bst t \<Longrightarrow> sorted (inorder t)"
-by (induction t) (auto simp: sorted_append sorted_Cons intro: less_imp_le less_trans)
-
 text{* In case there are duplicates: *}
 
 fun (in linorder) bst_eq :: "'a tree \<Rightarrow> bool" where
@@ -108,11 +105,26 @@
 "bst_eq \<langle>l,a,r\<rangle> \<longleftrightarrow>
  bst_eq l \<and> bst_eq r \<and> (\<forall>x\<in>set_tree l. x \<le> a) \<and> (\<forall>x\<in>set_tree r. a \<le> x)"
 
+lemma (in linorder) bst_eq_if_bst: "bst t \<Longrightarrow> bst_eq t"
+by (induction t) (auto)
+
 lemma (in linorder) bst_eq_imp_sorted: "bst_eq t \<Longrightarrow> sorted (inorder t)"
 apply (induction t)
  apply(simp)
 by (fastforce simp: sorted_append sorted_Cons intro: less_imp_le less_trans)
 
+lemma (in linorder) distinct_preorder_if_bst: "bst t \<Longrightarrow> distinct (preorder t)"
+apply (induction t)
+ apply simp
+apply(fastforce elim: order.asym)
+done
+
+lemma (in linorder) distinct_inorder_if_bst: "bst t \<Longrightarrow> distinct (inorder t)"
+apply (induction t)
+ apply simp
+apply(fastforce elim: order.asym)
+done
+
 
 subsection "Function @{text mirror}"
 

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Tree_Multiset.thy	Mon Apr 06 15:23:50 2015 +0200
@@ -0,0 +1,40 @@
+(* Author: Tobias Nipkow *)
+
+section {* Multiset of Elements of Binary Tree *}
+
+theory Tree_Multiset
+imports Multiset Tree
+begin
+
+text{* Kept separate from theory @{theory Tree} to avoid importing all of
+theory @{theory Multiset} into @{theory Tree}. Should be merged if
+@{theory Multiset} ever becomes part of @{theory Main}. *}
+
+fun mset_tree :: "'a tree \<Rightarrow> 'a multiset" where
+"mset_tree Leaf = {#}" |
+"mset_tree (Node l a r) = {#a#} + mset_tree l + mset_tree r"
+
+lemma set_of_mset_tree[simp]: "set_of (mset_tree t) = set_tree t"
+by(induction t) auto
+
+lemma size_mset_tree[simp]: "size(mset_tree t) = size t"
+by(induction t) auto
+
+lemma mset_map_tree: "mset_tree (map_tree f t) = image_mset f (mset_tree t)"
+by (induction t) auto
+
+lemma multiset_of_preorder[simp]: "multiset_of (preorder t) = mset_tree t"
+by (induction t) (auto simp: ac_simps)
+
+lemma multiset_of_inorder[simp]: "multiset_of (inorder t) = mset_tree t"
+by (induction t) (auto simp: ac_simps)
+
+lemma map_mirror: "mset_tree (mirror t) = mset_tree t"
+by (induction t) (simp_all add: ac_simps)
+
+lemma del_rightmost_mset_tree:
+  "\<lbrakk> del_rightmost t = (t',x);  t \<noteq> \<langle>\<rangle> \<rbrakk> \<Longrightarrow> mset_tree t = {#x#} + mset_tree t'"
+apply(induction t arbitrary: t' rule: del_rightmost.induct)
+by (auto split: prod.splits) (auto simp: ac_simps)
+
+end