# HG changeset patch
# User nipkow
# Date 1453199769 -3600
# Node ID 6acae6430fccfdf092e6a4a3411a5941f085719b
# Parent  eca7b38c8ee5cd5e6dccb1486835be2444fb20f7# Parent  e5bc7cbb0bcca8fa49d35deb989e73035cd24fb4
merged

diff -r eca7b38c8ee5 -r 6acae6430fcc src/HOL/Library/Tree.thy
--- a/src/HOL/Library/Tree.thy	Tue Jan 19 11:19:25 2016 +0100
+++ b/src/HOL/Library/Tree.thy	Tue Jan 19 11:36:09 2016 +0100
@@ -58,6 +58,27 @@
 lemma height_map_tree[simp]: "height (map_tree f t) = height t"
 by (induction t) auto
 
+lemma size1_height: "size t + 1 \<le> 2 ^ height (t::'a tree)"
+proof(induction t)
+  case (Node l a r)
+  show ?case
+  proof (cases "height l \<le> height r")
+    case True
+    have "size(Node l a r) + 1 = (size l + 1) + (size r + 1)" by simp
+    also have "size l + 1 \<le> 2 ^ height l" by(rule Node.IH(1))
+    also have "size r + 1 \<le> 2 ^ height r" by(rule Node.IH(2))
+    also have "(2::nat) ^ height l \<le> 2 ^ height r" using True by simp
+    finally show ?thesis using True by (auto simp: max_def mult_2)
+  next
+    case False
+    have "size(Node l a r) + 1 = (size l + 1) + (size r + 1)" by simp
+    also have "size l + 1 \<le> 2 ^ height l" by(rule Node.IH(1))
+    also have "size r + 1 \<le> 2 ^ height r" by(rule Node.IH(2))
+    also have "(2::nat) ^ height r \<le> 2 ^ height l" using False by simp
+    finally show ?thesis using False by (auto simp: max_def mult_2)
+  qed
+qed simp
+
 
 subsection "The set of subtrees"