# HG changeset patch
# User nipkow
# Date 1484898546 -3600
# Node ID a410e8403957494aec69e089aa90da2c59f6b9d2
# Parent  7c340dcbc323e22b7fe3a33a98829e1e125f7bf7
tuned

diff -r 7c340dcbc323 -r a410e8403957 src/HOL/Library/Tree.thy
--- a/src/HOL/Library/Tree.thy	Thu Jan 19 17:24:05 2017 +0100
+++ b/src/HOL/Library/Tree.thy	Fri Jan 20 08:49:06 2017 +0100
@@ -317,15 +317,15 @@
 assumes "balanced t" "size t \<le> size t'" shows "height t \<le> height t'"
 proof (cases "complete t")
   case True
-  have "(2::nat) ^ height t - 1 \<le> 2 ^ height t' - 1"
+  have "(2::nat) ^ height t \<le> 2 ^ height t'"
   proof -
-    have "2 ^ height t - 1 = size t"
-      using True by (simp add: complete_iff_height size_if_complete)
-    also have "\<dots> \<le> size t'" by(rule assms(2))
-    also have "\<dots> \<le> 2 ^ height t' - 1" by (rule size_height)
+    have "2 ^ height t = size1 t"
+      using True by (simp add: complete_iff_height size1_if_complete)
+    also have "\<dots> \<le> size1 t'" using assms(2) by(simp add: size1_def)
+    also have "\<dots> \<le> 2 ^ height t'" by (rule size1_height)
     finally show ?thesis .
   qed
-  thus ?thesis by (simp add: le_diff_iff)
+  thus ?thesis by (simp)
 next
   case False
   have "(2::nat) ^ min_height t < 2 ^ height t'"
@@ -335,8 +335,7 @@
     also have "\<dots> \<le> size1 t'" using assms(2) by (simp add: size1_def)
     also have "\<dots> \<le> 2 ^ height t'"  by(rule size1_height)
     finally have "(2::nat) ^ min_height t < (2::nat) ^ height t'" .
-    thus ?thesis
-      using power_eq_0_iff[of "2::nat" "height t'"] by linarith
+    thus ?thesis .
   qed
   hence *: "min_height t < height t'" by simp
   have "min_height t + 1 = height t"