equal
deleted
inserted
replaced
27 "paint c Leaf = Leaf" | |
27 "paint c Leaf = Leaf" | |
28 "paint c (Node l (a,_) r) = Node l (a,c) r" |
28 "paint c (Node l (a,_) r) = Node l (a,c) r" |
29 |
29 |
30 fun baldL :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where |
30 fun baldL :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where |
31 "baldL (R t1 a t2) b t3 = R (B t1 a t2) b t3" | |
31 "baldL (R t1 a t2) b t3 = R (B t1 a t2) b t3" | |
32 "baldL bl a (B t1 b t2) = baliR bl a (R t1 b t2)" | |
32 "baldL t1 a (B t2 b t3) = baliR t1 a (R t2 b t3)" | |
33 "baldL bl a (R (B t1 b t2) c t3) = R (B bl a t1) b (baliR t2 c (paint Red t3))" | |
33 "baldL t1 a (R (B t2 b t3) c t4) = R (B t1 a t2) b (baliR t3 c (paint Red t4))" | |
34 "baldL t1 a t2 = R t1 a t2" |
34 "baldL t1 a t2 = R t1 a t2" |
35 |
35 |
36 fun baldR :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where |
36 fun baldR :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where |
37 "baldR t1 a (R t2 b t3) = R t1 a (B t2 b t3)" | |
37 "baldR t1 a (R t2 b t3) = R t1 a (B t2 b t3)" | |
38 "baldR (B t1 a t2) b t3 = baliL (R t1 a t2) b t3" | |
38 "baldR (B t1 a t2) b t3 = baliL (R t1 a t2) b t3" | |