diff -r f86bcf439837 -r 37482793a949 src/HOL/Data_Structures/RBT_Set.thy
--- a/src/HOL/Data_Structures/RBT_Set.thy	Wed Jul 10 08:37:54 2024 +0200
+++ b/src/HOL/Data_Structures/RBT_Set.thy	Thu Jul 18 15:17:46 2024 +0200
@@ -307,10 +307,13 @@
 lemma bheight_size_bound:  "invc t \<Longrightarrow> invh t \<Longrightarrow> 2 ^ (bheight t) \<le> size1 t"
 by (induction t) auto
 
+lemma bheight_le_min_height:  "invh t \<Longrightarrow> bheight t \<le> min_height t"
+by (induction t) auto
+
 lemma rbt_height_le: assumes "rbt t" shows "height t \<le> 2 * log 2 (size1 t)"
 proof -
   have "2 powr (height t / 2) \<le> 2 powr bheight t"
-    using rbt_height_bheight[OF assms] by (simp)
+    using rbt_height_bheight[OF assms] by simp
   also have "\<dots> \<le> size1 t" using assms
     by (simp add: powr_realpow bheight_size_bound rbt_def)
   finally have "2 powr (height t / 2) \<le> size1 t" .
@@ -319,4 +322,15 @@
   thus ?thesis by simp
 qed
 
+lemma rbt_height_le2: assumes "rbt t" shows "height t \<le> 2 * log 2 (size1 t)"
+proof -
+  have "height t \<le> 2 * bheight t"
+    using rbt_height_bheight_if assms[simplified rbt_def] by fastforce
+  also have "\<dots> \<le> 2 * min_height t"
+    using bheight_le_min_height assms[simplified rbt_def] by auto
+  also have "\<dots> \<le> 2 * log 2 (size1 t)"
+    using le_log2_of_power min_height_size1 by auto
+  finally show ?thesis by simp
+qed
+
 end