author | nipkow |
Mon, 19 Aug 2019 16:49:24 +0200 | |
changeset 70571 | e72daea2aab6 |
parent 68413 | b56ed5010e69 |
child 70755 | 3fb16bed5d6c |
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 |
||
68413 | 13 |
abbreviation R where "R l a r \<equiv> Node l a Red r" |
14 |
abbreviation B where "B l a r \<equiv> Node l a Black r" |
|
61224 | 15 |
|
64960 | 16 |
fun baliL :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where |
70571 | 17 |
"baliL (R (R t1 a t2) b t3) c t4 = R (B t1 a t2) b (B t3 c t4)" | |
18 |
"baliL (R t1 a (R t2 b t3)) c t4 = R (B t1 a t2) b (B t3 c t4)" | |
|
64960 | 19 |
"baliL t1 a t2 = B t1 a t2" |
20 |
||
21 |
fun baliR :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where |
|
70571 | 22 |
"baliR t1 a (R t2 b (R t3 c t4)) = R (B t1 a t2) b (B t3 c t4)" | |
23 |
"baliR t1 a (R (R t2 b t3) c t4) = R (B t1 a t2) b (B t3 c t4)" | |
|
64960 | 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" | |
|
68413 | 28 |
"paint c (Node l a _ r) = Node l a c r" |
61224 | 29 |
|
64960 | 30 |
fun baldL :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where |
70571 | 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)" | |
|
33 |
"baldL bl a (R (B t1 b t2) c t3) = R (B bl a t1) b (baliR t2 c (paint Red t3))" | |
|
34 |
"baldL t1 a t2 = R t1 a t2" |
|
61224 | 35 |
|
64960 | 36 |
fun baldR :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where |
70571 | 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" | |
|
39 |
"baldR (R t1 a (B t2 b t3)) c t4 = R (baliL (paint Red t1) a t2) b (B t3 c t4)" | |
|
40 |
"baldR t1 a t2 = R t1 a 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 |