--- a/src/HOL/Library/Tree.thy Wed Sep 24 19:11:21 2014 +0200
+++ b/src/HOL/Library/Tree.thy Thu Sep 25 11:38:56 2014 +0200
@@ -14,6 +14,16 @@
| "right Leaf = Leaf"
datatype_compat tree
+text{* Can be seen as counting the number of leaves rather than nodes: *}
+
+definition size1 :: "'a tree \<Rightarrow> nat" where
+"size1 t = size t + 1"
+
+lemma size1_simps[simp]:
+ "size1 \<langle>\<rangle> = 1"
+ "size1 \<langle>l, x, r\<rangle> = size1 l + size1 r"
+by (simp_all add: size1_def)
+
lemma neq_Leaf_iff: "(t \<noteq> \<langle>\<rangle>) = (\<exists>l a r. t = \<langle>l, a, r\<rangle>)"
by (cases t) auto