--- a/src/HOL/Library/Tree_Real.thy Wed Oct 03 20:55:59 2018 +0200
+++ b/src/HOL/Library/Tree_Real.thy Thu Oct 04 10:35:29 2018 +0200
@@ -37,29 +37,24 @@
assume *: "\<not> complete t"
hence "height t = min_height t + 1"
using assms min_height_le_height[of t]
- by(auto simp add: balanced_def complete_iff_height)
- hence "size1 t < 2 ^ (min_height t + 1)"
- by (metis * size1_height_if_incomplete)
- hence "log 2 (size1 t) < min_height t + 1"
- using log2_of_power_less size1_ge0 by blast
- thus ?thesis using min_height_size1_log[of t] by linarith
+ by(auto simp: balanced_def complete_iff_height)
+ hence "size1 t < 2 ^ (min_height t + 1)" by (metis * size1_height_if_incomplete)
+ from floor_log_nat_eq_if[OF min_height_size1 this] show ?thesis by simp
qed
lemma height_balanced: assumes "balanced t"
shows "height t = nat(ceiling(log 2 (size1 t)))"
proof cases
assume *: "complete t"
- hence "size1 t = 2 ^ height t"
- by (simp add: size1_if_complete)
- from log2_of_power_eq[OF this] show ?thesis
- by linarith
+ hence "size1 t = 2 ^ height t" by (simp add: size1_if_complete)
+ from log2_of_power_eq[OF this] show ?thesis by linarith
next
assume *: "\<not> complete t"
hence **: "height t = min_height t + 1"
using assms min_height_le_height[of t]
by(auto simp add: balanced_def complete_iff_height)
hence "size1 t \<le> 2 ^ (min_height t + 1)" by (metis size1_height)
- from log2_of_power_le[OF this size1_ge0] min_height_size1_log_if_incomplete[OF *] **
+ from log2_of_power_le[OF this size1_ge0] min_height_size1_log_if_incomplete[OF *] **
show ?thesis by linarith
qed