diff -r 6c018eb1e177 -r 1ba3aacfa4d3 src/HOL/Library/Tree.thy
--- 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