--- a/src/HOL/Library/Tree.thy Wed Jun 17 18:13:44 2015 +0200
+++ b/src/HOL/Library/Tree.thy Wed Jun 17 20:21:40 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