# HG changeset patch
# User wenzelm
# Date 1434573022 -7200
# Node ID 5e67a223a141e68b6522a354485b34d5fc23bfd6
# Parent  16993a3f4967e35914855d7f51df0e2e1a5fb0db# Parent  64d27b9f00a0ce73475542de32c6fc535f774d03
merged

diff -r 64d27b9f00a0 -r 5e67a223a141 src/HOL/Library/Tree.thy
--- a/src/HOL/Library/Tree.thy	Wed Jun 17 22:29:12 2015 +0200
+++ b/src/HOL/Library/Tree.thy	Wed Jun 17 22:30:22 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: "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 64d27b9f00a0 -r 5e67a223a141 src/HOL/Library/Tree_Multiset.thy
--- a/src/HOL/Library/Tree_Multiset.thy	Wed Jun 17 22:29:12 2015 +0200
+++ b/src/HOL/Library/Tree_Multiset.thy	Wed Jun 17 22:30:22 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)