author | wenzelm |
Sat, 26 Jun 2021 20:55:43 +0200 | |
changeset 73884 | 0a12ca4f3e8d |
parent 71830 | 7a997ead54b0 |
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 |
||
70755
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70571
diff
changeset
|
11 |
type_synonym 'a rbt = "('a*color)tree" |
61224 | 12 |
|
70755
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70571
diff
changeset
|
13 |
abbreviation R where "R l a r \<equiv> Node l (a, Red) r" |
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70571
diff
changeset
|
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" | |
|
70755
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70571
diff
changeset
|
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" | |
71349 | 32 |
"baldL t1 a (B t2 b t3) = baliR t1 a (R t2 b t3)" | |
33 |
"baldL t1 a (R (B t2 b t3) c t4) = R (B t1 a t2) b (baliR t3 c (paint Red t4))" | |
|
70571 | 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 |
|
71830 | 42 |
fun join :: "'a rbt \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where |
43 |
"join Leaf t = t" | |
|
44 |
"join t Leaf = t" | |
|
45 |
"join (R t1 a t2) (R t3 c t4) = |
|
46 |
(case join t2 t3 of |
|
61678 | 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))" | |
|
71830 | 49 |
"join (B t1 a t2) (B t3 c t4) = |
50 |
(case join t2 t3 of |
|
71348 | 51 |
R u2 b u3 \<Rightarrow> R (B t1 a u2) b (B u3 c t4) | |
64960 | 52 |
t23 \<Rightarrow> baldL t1 a (B t23 c t4))" | |
71830 | 53 |
"join t1 (R t2 a t3) = R (join t1 t2) a t3" | |
54 |
"join (R t1 a t2) t3 = R t1 a (join t2 t3)" |
|
61224 | 55 |
|
56 |
end |