# HG changeset patch
# User nipkow
# Date 1721311027 -7200
# Node ID 97dab09aa727ec2cfefc39f8f2a7b5204a8eadb6
# Parent  37482793a949de042b7368355c508deac862cd94
tuned

diff -r 37482793a949 -r 97dab09aa727 src/HOL/Data_Structures/AVL_Bal_Set.thy
--- a/src/HOL/Data_Structures/AVL_Bal_Set.thy	Thu Jul 18 15:17:46 2024 +0200
+++ b/src/HOL/Data_Structures/AVL_Bal_Set.thy	Thu Jul 18 15:57:07 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