# HG changeset patch
# User nipkow
# Date 1411637936 -7200
# Node ID 566117a31cc02398329dae4cdce14525e47229ed
# Parent  8d124c73c37adf0a1e42dbeecfbd08a1459a76c8
added function size1

diff -r 8d124c73c37a -r 566117a31cc0 src/HOL/Library/Tree.thy
--- 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