merged

--- a/src/HOL/Data_Structures/AVL_Bal_Set.thy	Thu Jul 18 13:52:51 2024 +0200
+++ b/src/HOL/Data_Structures/AVL_Bal_Set.thy	Thu Jul 18 16:00:40 2024 +0200
@@ -67,13 +67,13 @@
    GT \<Rightarrow> let r' = insert x r in if incr r r' then balR l a b r' else Node l (a,b) r')"
 
 fun decr where
-"decr t t' = (t \<noteq> Leaf \<and> (t' = Leaf \<or> \<not> is_bal t \<and> is_bal t'))"
+"decr t t' = (t \<noteq> Leaf \<and> incr t' t)"
 
 fun split_max :: "'a tree_bal \<Rightarrow> 'a tree_bal * 'a" where
 "split_max (Node l (a, ba) r) =
   (if r = Leaf then (l,a)
    else let (r',a') = split_max r;
-            t' = if decr r r' then balL l a ba r' else Node l (a,ba) r'
+            t' = if incr r' r then balL l a ba r' else Node l (a,ba) r'
         in (t', a'))"
 
 fun delete :: "'a::linorder \<Rightarrow> 'a tree_bal \<Rightarrow> 'a tree_bal" where
@@ -82,7 +82,7 @@
   (case cmp x a of
      EQ \<Rightarrow> if l = Leaf then r
            else let (l', a') = split_max l in
-                if decr l l' then balR l' a' ba r else Node l' (a',ba) r |
+                if incr l' l then balR l' a' ba r else Node l' (a',ba) r |
      LT \<Rightarrow> let l' = delete x l in if decr l l' then balR l' a ba r else Node l' (a,ba) r |
      GT \<Rightarrow> let r' = delete x r in if decr r r' then balL l a ba r' else Node l (a,ba) r')"
 
@@ -136,7 +136,7 @@
 
 lemma avl_split_max:
   "\<lbrakk> split_max t = (t',a); avl t; t \<noteq> Leaf \<rbrakk> \<Longrightarrow>
-   avl t' \<and> height t = height t' + (if decr t t' then 1 else 0)"
+   avl t' \<and> height t = height t' + (if incr t' t then 1 else 0)"
 apply(induction t arbitrary: t' a rule: split_max_induct)
  apply(auto simp: max_absorb1 max_absorb2 height_1_iff split!: splits prod.splits)
 done

--- a/src/HOL/Data_Structures/RBT_Set.thy	Thu Jul 18 13:52:51 2024 +0200
+++ b/src/HOL/Data_Structures/RBT_Set.thy	Thu Jul 18 16:00:40 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