# HG changeset patch
# User nipkow
# Date 1434565321 -7200
# Node ID 83231b558ce429c283bffb72aa39c2c1d5ca28e2
# Parent  17741c71a731accaca8d1c44c3953a437af3e3b9# Parent  9e6584184315b098442ee51ef835cb5542c67336
merged

diff -r 17741c71a731 -r 83231b558ce4 src/HOL/Library/Tree.thy
--- a/src/HOL/Library/Tree.thy	Wed Jun 17 18:58:46 2015 +0200
+++ b/src/HOL/Library/Tree.thy	Wed Jun 17 20:22:01 2015 +0200
@@ -24,6 +24,9 @@
   "size1 \<langle>l, x, r\<rangle> = size1 l + size1 r"
 by (simp_all add: size1_def)
 
+lemma size_0_iff_Leaf[simp]: "size t = 0 \<longleftrightarrow> t = Leaf"
+by(cases t) auto
+
 lemma neq_Leaf_iff: "(t \<noteq> \<langle>\<rangle>) = (\<exists>l a r. t = \<langle>l, a, r\<rangle>)"
 by (cases t) auto
 
@@ -126,6 +129,14 @@
 done
 
 
+subsection "The heap predicate"
+
+fun heap :: "'a::linorder tree \<Rightarrow> bool" where
+"heap Leaf = True" |
+"heap (Node l m r) =
+  (heap l \<and> heap r \<and> (\<forall>x \<in> set_tree l \<union> set_tree r. m \<le> x))"
+
+
 subsection "Function @{text mirror}"
 
 fun mirror :: "'a tree \<Rightarrow> 'a tree" where
diff -r 17741c71a731 -r 83231b558ce4 src/HOL/Library/Tree_Multiset.thy
--- a/src/HOL/Library/Tree_Multiset.thy	Wed Jun 17 18:58:46 2015 +0200
+++ b/src/HOL/Library/Tree_Multiset.thy	Wed Jun 17 20:22:01 2015 +0200
@@ -23,6 +23,9 @@
 lemma mset_map_tree: "mset_tree (map_tree f t) = image_mset f (mset_tree t)"
 by (induction t) auto
 
+lemma mset_iff_set_tree: "x \<in># mset_tree t \<longleftrightarrow> x \<in> set_tree t"
+by(induction t arbitrary: x) auto
+
 lemma multiset_of_preorder[simp]: "multiset_of (preorder t) = mset_tree t"
 by (induction t) (auto simp: ac_simps)