# HG changeset patch # User nipkow # Date 1577488543 -3600 # Node ID 857453c0db3d7d4924c08ce328530dc986e45e4b # Parent 3c4c171344f483f5a08b6f7c7244825a5bf02574 tuned diff -r 3c4c171344f4 -r 857453c0db3d src/HOL/Data_Structures/RBT.thy --- a/src/HOL/Data_Structures/RBT.thy Fri Dec 27 16:02:23 2019 +0100 +++ b/src/HOL/Data_Structures/RBT.thy Sat Dec 28 00:15:43 2019 +0100 @@ -48,7 +48,7 @@ t23 \ R t1 a (R t23 c t4))" | "combine (B t1 a t2) (B t3 c t4) = (case combine t2 t3 of - R t2' b t3' \ R (B t1 a t2') b (B t3' c t4) | + R u2 b u3 \ R (B t1 a u2) b (B u3 c t4) | t23 \ baldL t1 a (B t23 c t4))" | "combine t1 (R t2 a t3) = R (combine t1 t2) a t3" | "combine (R t1 a t2) t3 = R t1 a (combine t2 t3)" diff -r 3c4c171344f4 -r 857453c0db3d src/HOL/Data_Structures/RBT_Set.thy --- a/src/HOL/Data_Structures/RBT_Set.thy Fri Dec 27 16:02:23 2019 +0100 +++ b/src/HOL/Data_Structures/RBT_Set.thy Sat Dec 28 00:15:43 2019 +0100 @@ -195,7 +195,7 @@ lemma invh_baldL_invc: "\ invh l; invh r; bheight l + 1 = bheight r; invc r \ - \ invh (baldL l a r) \ bheight (baldL l a r) = bheight l + 1" + \ invh (baldL l a r) \ bheight (baldL l a r) = bheight r" by (induct l a r rule: baldL.induct) (auto simp: invh_baliR invh_paint bheight_baliR bheight_paint_Red)