author | haftmann |
Mon, 06 Feb 2017 20:56:34 +0100 | |
changeset 64990 | c6a7de505796 |
parent 64960 | 8be78855ee7a |
child 67910 | b42473502373 |
permissions | -rw-r--r-- |
61224 | 1 |
(* Author: Tobias Nipkow *) |
2 |
||
61469
cd82b1023932
added 2-3 trees (simpler and more complete than the version in ex/Tree23)
nipkow
parents:
61231
diff
changeset
|
3 |
section \<open>Red-Black Trees\<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 |
||
64960 | 16 |
fun 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 |
||
21 |
fun baliR :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where |
|
22 |
"baliR t1 a1 (R (R t2 a2 t3) a3 t4) = R (B t1 a1 t2) a2 (B t3 a3 t4)" | |
|
23 |
"baliR t1 a1 (R t2 a2 (R t3 a3 t4)) = R (B t1 a1 t2) a2 (B t3 a3 t4)" | |
|
24 |
"baliR t1 a t2 = B t1 a t2" |
|
61224 | 25 |
|
61749 | 26 |
fun paint :: "color \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where |
27 |
"paint c Leaf = Leaf" | |
|
28 |
"paint c (Node _ l a r) = Node c l a r" |
|
61224 | 29 |
|
64960 | 30 |
fun 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" |
|
61224 | 35 |
|
64960 | 36 |
fun 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" |
|
61224 | 41 |
|
42 |
fun combine :: "'a rbt \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where |
|
43 |
"combine Leaf t = t" | |
|
44 |
"combine t Leaf = t" | |
|
61678 | 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) | |
|
64960 | 52 |
t23 \<Rightarrow> baldL t1 a (B t23 c t4))" | |
61224 | 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 |
||
56 |
end |