author | wenzelm |
Sat, 22 Oct 2016 21:10:02 +0200 | |
changeset 64350 | 3af8566788e7 |
parent 61749 | 7f530d7e552d |
child 64952 | f11e974b47e0 |
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 |
||
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 |
||
61749 | 25 |
fun paint :: "color \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where |
26 |
"paint c Leaf = Leaf" | |
|
27 |
"paint c (Node _ l a r) = Node c l a r" |
|
61224 | 28 |
|
29 |
fun balL :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where |
|
61534 | 30 |
"balL (R t1 x t2) y t3 = R (B t1 x t2) y t3" | |
61224 | 31 |
"balL bl x (B t1 y t2) = bal bl x (R t1 y t2)" | |
61749 | 32 |
"balL bl x (R (B t1 y t2) z t3) = R (B bl x t1) y (bal t2 z (paint Red t3))" | |
61224 | 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)" | |
|
61534 | 37 |
"balR (B t1 x t2) y t3 = bal (R t1 x t2) y t3" | |
61749 | 38 |
"balR (R t1 x (B t2 y t3)) z t4 = R (bal (paint Red t1) x t2) y (B t3 z t4)" | |
61224 | 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" | |
|
61678 | 44 |
"combine (R t1 a t2) (R t3 c t4) = |
45 |
(case combine t2 t3 of |
|
46 |
R u2 b u3 \<Rightarrow> (R (R t1 a u2) b (R u3 c t4)) | |
|
47 |
t23 \<Rightarrow> R t1 a (R t23 c t4))" | |
|
48 |
"combine (B t1 a t2) (B t3 c t4) = |
|
49 |
(case combine t2 t3 of |
|
50 |
R t2' b t3' \<Rightarrow> R (B t1 a t2') b (B t3' c t4) | |
|
51 |
t23 \<Rightarrow> balL t1 a (B t23 c t4))" | |
|
61224 | 52 |
"combine t1 (R t2 a t3) = R (combine t1 t2) a t3" | |
53 |
"combine (R t1 a t2) t3 = R t1 a (combine t2 t3)" |
|
54 |
||
55 |
end |