--- a/src/HOL/Library/Tree.thy Wed Apr 20 16:50:20 2016 +0200
+++ b/src/HOL/Library/Tree.thy Fri Apr 22 15:34:37 2016 +0200
@@ -83,6 +83,19 @@
qed simp
+subsection "Balanced"
+
+fun balanced :: "'a tree \<Rightarrow> bool" where
+"balanced Leaf = True" |
+"balanced (Node l x r) = (balanced l \<and> balanced r \<and> height l = height r)"
+
+lemma balanced_size1: "balanced t \<Longrightarrow> size1 t = 2 ^ height t"
+by (induction t) auto
+
+lemma balanced_size: "balanced t \<Longrightarrow> size t = 2 ^ height t - 1"
+using balanced_size1[simplified size1_def] by fastforce
+
+
subsection "The set of subtrees"
fun subtrees :: "'a tree \<Rightarrow> 'a tree set" where