--- 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
--- 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)