--- a/src/HOL/Data_Structures/RBT.thy Sat Aug 17 19:04:03 2019 +0200
+++ b/src/HOL/Data_Structures/RBT.thy Mon Aug 19 16:49:24 2019 +0200
@@ -14,13 +14,13 @@
abbreviation B where "B l a r \<equiv> Node l a Black r"
fun baliL :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
-"baliL (R (R t1 a1 t2) a2 t3) a3 t4 = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
-"baliL (R t1 a1 (R t2 a2 t3)) a3 t4 = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
+"baliL (R (R t1 a t2) b t3) c t4 = R (B t1 a t2) b (B t3 c t4)" |
+"baliL (R t1 a (R t2 b t3)) c t4 = R (B t1 a t2) b (B t3 c t4)" |
"baliL t1 a t2 = B t1 a t2"
fun baliR :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
-"baliR t1 a1 (R t2 a2 (R t3 a3 t4)) = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
-"baliR t1 a1 (R (R t2 a2 t3) a3 t4) = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
+"baliR t1 a (R t2 b (R t3 c t4)) = R (B t1 a t2) b (B t3 c t4)" |
+"baliR t1 a (R (R t2 b t3) c t4) = R (B t1 a t2) b (B t3 c t4)" |
"baliR t1 a t2 = B t1 a t2"
fun paint :: "color \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
@@ -28,16 +28,16 @@
"paint c (Node l a _ r) = Node l a c r"
fun baldL :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
-"baldL (R t1 x t2) y t3 = R (B t1 x t2) y t3" |
-"baldL bl x (B t1 y t2) = baliR bl x (R t1 y t2)" |
-"baldL bl x (R (B t1 y t2) z t3) = R (B bl x t1) y (baliR t2 z (paint Red t3))" |
-"baldL t1 x t2 = R t1 x t2"
+"baldL (R t1 a t2) b t3 = R (B t1 a t2) b t3" |
+"baldL bl a (B t1 b t2) = baliR bl a (R t1 b t2)" |
+"baldL bl a (R (B t1 b t2) c t3) = R (B bl a t1) b (baliR t2 c (paint Red t3))" |
+"baldL t1 a t2 = R t1 a t2"
fun baldR :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
-"baldR t1 x (R t2 y t3) = R t1 x (B t2 y t3)" |
-"baldR (B t1 x t2) y t3 = baliL (R t1 x t2) y t3" |
-"baldR (R t1 x (B t2 y t3)) z t4 = R (baliL (paint Red t1) x t2) y (B t3 z t4)" |
-"baldR t1 x t2 = R t1 x t2"
+"baldR t1 a (R t2 b t3) = R t1 a (B t2 b t3)" |
+"baldR (B t1 a t2) b t3 = baliL (R t1 a t2) b t3" |
+"baldR (R t1 a (B t2 b t3)) c t4 = R (baliL (paint Red t1) a t2) b (B t3 c t4)" |
+"baldR t1 a t2 = R t1 a t2"
fun combine :: "'a rbt \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
"combine Leaf t = t" |