# HG changeset patch
# User nipkow
# Date 1458292496 -3600
# Node ID 7e6bb43e72178175e4dba1a742c7ee9b216490d5
# Parent  d23be25c08358098ef10f9d6db61e45294ffbbfd
added tree lemmas

diff -r d23be25c0835 -r 7e6bb43e7217 src/HOL/Data_Structures/Tree2.thy
--- a/src/HOL/Data_Structures/Tree2.thy	Fri Mar 18 08:32:37 2016 +0100
+++ b/src/HOL/Data_Structures/Tree2.thy	Fri Mar 18 10:14:56 2016 +0100
@@ -14,4 +14,15 @@
 "height Leaf = 0" |
 "height (Node _ l a r) = max (height l) (height r) + 1"
 
+definition size1 :: "('a,'b) tree \<Rightarrow> nat" where
+"size1 t = size t + 1"
+
+lemma size1_simps[simp]:
+  "size1 \<langle>\<rangle> = 1"
+  "size1 \<langle>u, l, x, r\<rangle> = size1 l + size1 r"
+by (simp_all add: size1_def)
+
+lemma size1_ge0[simp]: "0 < size1 t"
+by (simp add: size1_def)
+
 end
diff -r d23be25c0835 -r 7e6bb43e7217 src/HOL/Library/Tree.thy
--- a/src/HOL/Library/Tree.thy	Fri Mar 18 08:32:37 2016 +0100
+++ b/src/HOL/Library/Tree.thy	Fri Mar 18 10:14:56 2016 +0100
@@ -24,6 +24,9 @@
   "size1 \<langle>l, x, r\<rangle> = size1 l + size1 r"
 by (simp_all add: size1_def)
 
+lemma size1_ge0[simp]: "0 < size1 t"
+by (simp add: size1_def)
+
 lemma size_0_iff_Leaf: "size t = 0 \<longleftrightarrow> t = Leaf"
 by(cases t) auto