|
61224
|
1 |
(* Author: Tobias Nipkow *)
|
|
|
2 |
|
|
61231
|
3 |
section \<open>Red-Black Tree\<close>
|
|
61224
|
4 |
|
|
|
5 |
theory RBT
|
|
|
6 |
imports Tree2
|
|
|
7 |
begin
|
|
|
8 |
|
|
|
9 |
datatype color = Red | Black
|
|
|
10 |
|
|
|
11 |
type_synonym 'a rbt = "('a,color)tree"
|
|
|
12 |
|
|
|
13 |
abbreviation R where "R l a r \<equiv> Node Red l a r"
|
|
|
14 |
abbreviation B where "B l a r \<equiv> Node Black l a r"
|
|
|
15 |
|
|
|
16 |
fun bal :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
|
|
|
17 |
(* The first line is superfluous; it merely speeds up pattern compilation *)
|
|
|
18 |
"bal (R t1 a1 t2) a2 (R t3 a3 t4) = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
|
|
|
19 |
"bal (R (R t1 a1 t2) a2 t3) a3 t4 = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
|
|
|
20 |
"bal (R t1 a1 (R t2 a2 t3)) a3 t4 = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
|
|
|
21 |
"bal t1 a1 (R t2 a2 (R t3 a3 t4)) = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
|
|
|
22 |
"bal t1 a1 (R (R t2 a2 t3) a3 t4) = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
|
|
|
23 |
"bal t1 a t2 = B t1 a t2"
|
|
|
24 |
|
|
|
25 |
fun red :: "'a rbt \<Rightarrow> 'a rbt" where
|
|
|
26 |
"red Leaf = Leaf" |
|
|
|
27 |
"red (Node _ l a r) = R l a r"
|
|
|
28 |
|
|
|
29 |
fun balL :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
|
|
|
30 |
"balL (R t1 x t2) s t3 = R (B t1 x t2) s t3" |
|
|
|
31 |
"balL bl x (B t1 y t2) = bal bl x (R t1 y t2)" |
|
|
|
32 |
"balL bl x (R (B t1 y t2) z t3) = R (B bl x t1) y (bal t2 z (red t3))" |
|
|
|
33 |
"balL t1 x t2 = R t1 x t2"
|
|
|
34 |
|
|
|
35 |
fun balR :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
|
|
|
36 |
"balR t1 x (R t2 y t3) = R t1 x (B t2 y t3)" |
|
|
|
37 |
"balR (B t1 x t2) y bl = bal (R t1 x t2) y bl" |
|
|
|
38 |
"balR (R t1 x (B t2 y t3)) z bl = R (bal (red t1) x t2) y (B t3 z bl)" |
|
|
|
39 |
"balR t1 x t2 = R t1 x t2"
|
|
|
40 |
|
|
|
41 |
fun combine :: "'a rbt \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
|
|
|
42 |
"combine Leaf t = t" |
|
|
|
43 |
"combine t Leaf = t" |
|
|
|
44 |
"combine (R a x b) (R c y d) = (case combine b c of
|
|
|
45 |
R b2 z c2 \<Rightarrow> (R (R a x b2) z (R c2 y d)) |
|
|
|
46 |
bc \<Rightarrow> R a x (R bc y d))" |
|
|
|
47 |
"combine (B t1 a t2) (B t3 c t4) = (case combine t2 t3 of
|
|
|
48 |
R t2' b t3' \<Rightarrow> R (B t1 a t2') b (B t3' c t4) |
|
|
|
49 |
t23 \<Rightarrow> balL t1 a (B t23 c t4))" |
|
|
|
50 |
"combine t1 (R t2 a t3) = R (combine t1 t2) a t3" |
|
|
|
51 |
"combine (R t1 a t2) t3 = R t1 a (combine t2 t3)"
|
|
|
52 |
|
|
|
53 |
end
|