1(* Author: Tobias Nipkow *) 2 3section \<open>Red-Black Trees\<close> 4 5theory RBT 6imports Tree2 7begin 8 9datatype color = Red | Black 10 11type_synonym 'a rbt = "('a,color)tree" 12 13abbreviation R where "R l a r \<equiv> Node l a Red r" 14abbreviation B where "B l a r \<equiv> Node l a Black r" 15 16fun baliL :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where 17"baliL (R (R t1 a1 t2) a2 t3) a3 t4 = R (B t1 a1 t2) a2 (B t3 a3 t4)" | 18"baliL (R t1 a1 (R t2 a2 t3)) a3 t4 = R (B t1 a1 t2) a2 (B t3 a3 t4)" | 19"baliL t1 a t2 = B t1 a t2" 20 21fun baliR :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where 22"baliR t1 a1 (R t2 a2 (R t3 a3 t4)) = R (B t1 a1 t2) a2 (B t3 a3 t4)" | 23"baliR t1 a1 (R (R t2 a2 t3) a3 t4) = R (B t1 a1 t2) a2 (B t3 a3 t4)" | 24"baliR t1 a t2 = B t1 a t2" 25 26fun paint :: "color \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where 27"paint c Leaf = Leaf" | 28"paint c (Node l a _ r) = Node l a c r" 29 30fun baldL :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where 31"baldL (R t1 x t2) y t3 = R (B t1 x t2) y t3" | 32"baldL bl x (B t1 y t2) = baliR bl x (R t1 y t2)" | 33"baldL bl x (R (B t1 y t2) z t3) = R (B bl x t1) y (baliR t2 z (paint Red t3))" | 34"baldL t1 x t2 = R t1 x t2" 35 36fun baldR :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where 37"baldR t1 x (R t2 y t3) = R t1 x (B t2 y t3)" | 38"baldR (B t1 x t2) y t3 = baliL (R t1 x t2) y t3" | 39"baldR (R t1 x (B t2 y t3)) z t4 = R (baliL (paint Red t1) x t2) y (B t3 z t4)" | 40"baldR t1 x t2 = R t1 x t2" 41 42fun combine :: "'a rbt \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where 43"combine Leaf t = t" | 44"combine t Leaf = t" | 45"combine (R t1 a t2) (R t3 c t4) = 46 (case combine t2 t3 of 47 R u2 b u3 \<Rightarrow> (R (R t1 a u2) b (R u3 c t4)) | 48 t23 \<Rightarrow> R t1 a (R t23 c t4))" | 49"combine (B t1 a t2) (B t3 c t4) = 50 (case combine t2 t3 of 51 R t2' b t3' \<Rightarrow> R (B t1 a t2') b (B t3' c t4) | 52 t23 \<Rightarrow> baldL t1 a (B t23 c t4))" | 53"combine t1 (R t2 a t3) = R (combine t1 t2) a t3" | 54"combine (R t1 a t2) t3 = R t1 a (combine t2 t3)" 55 56end 57