src/HOL/Data_Structures/RBT.thy
author nipkow
Mon Jun 11 16:29:27 2018 +0200 (14 months ago)
changeset 68413 b56ed5010e69
parent 67910 b42473502373
child 70571 e72daea2aab6
permissions -rw-r--r--
tuned order of arguments
nipkow@61224
     1
(* Author: Tobias Nipkow *)
nipkow@61224
     2
nipkow@61469
     3
section \<open>Red-Black Trees\<close>
nipkow@61224
     4
nipkow@61224
     5
theory RBT
nipkow@61224
     6
imports Tree2
nipkow@61224
     7
begin
nipkow@61224
     8
nipkow@61224
     9
datatype color = Red | Black
nipkow@61224
    10
nipkow@61224
    11
type_synonym 'a rbt = "('a,color)tree"
nipkow@61224
    12
nipkow@68413
    13
abbreviation R where "R l a r \<equiv> Node l a Red r"
nipkow@68413
    14
abbreviation B where "B l a r \<equiv> Node l a Black r"
nipkow@61224
    15
nipkow@64960
    16
fun baliL :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
nipkow@64960
    17
"baliL (R (R t1 a1 t2) a2 t3) a3 t4 = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
nipkow@64960
    18
"baliL (R t1 a1 (R t2 a2 t3)) a3 t4 = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
nipkow@64960
    19
"baliL t1 a t2 = B t1 a t2"
nipkow@64960
    20
nipkow@64960
    21
fun baliR :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
nipkow@67910
    22
"baliR t1 a1 (R t2 a2 (R t3 a3 t4)) = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
nipkow@64960
    23
"baliR t1 a1 (R (R t2 a2 t3) a3 t4) = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
nipkow@64960
    24
"baliR t1 a t2 = B t1 a t2"
nipkow@61224
    25
nipkow@61749
    26
fun paint :: "color \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
nipkow@61749
    27
"paint c Leaf = Leaf" |
nipkow@68413
    28
"paint c (Node l a _ r) = Node l a c r"
nipkow@61224
    29
nipkow@64960
    30
fun baldL :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
nipkow@64960
    31
"baldL (R t1 x t2) y t3 = R (B t1 x t2) y t3" |
nipkow@64960
    32
"baldL bl x (B t1 y t2) = baliR bl x (R t1 y t2)" |
nipkow@64960
    33
"baldL bl x (R (B t1 y t2) z t3) = R (B bl x t1) y (baliR t2 z (paint Red t3))" |
nipkow@64960
    34
"baldL t1 x t2 = R t1 x t2"
nipkow@61224
    35
nipkow@64960
    36
fun baldR :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
nipkow@64960
    37
"baldR t1 x (R t2 y t3) = R t1 x (B t2 y t3)" |
nipkow@64960
    38
"baldR (B t1 x t2) y t3 = baliL (R t1 x t2) y t3" |
nipkow@64960
    39
"baldR (R t1 x (B t2 y t3)) z t4 = R (baliL (paint Red t1) x t2) y (B t3 z t4)" |
nipkow@64960
    40
"baldR t1 x t2 = R t1 x t2"
nipkow@61224
    41
nipkow@61224
    42
fun combine :: "'a rbt \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
nipkow@61224
    43
"combine Leaf t = t" |
nipkow@61224
    44
"combine t Leaf = t" |
nipkow@61678
    45
"combine (R t1 a t2) (R t3 c t4) =
nipkow@61678
    46
  (case combine t2 t3 of
nipkow@61678
    47
     R u2 b u3 \<Rightarrow> (R (R t1 a u2) b (R u3 c t4)) |
nipkow@61678
    48
     t23 \<Rightarrow> R t1 a (R t23 c t4))" |
nipkow@61678
    49
"combine (B t1 a t2) (B t3 c t4) =
nipkow@61678
    50
  (case combine t2 t3 of
nipkow@61678
    51
     R t2' b t3' \<Rightarrow> R (B t1 a t2') b (B t3' c t4) |
nipkow@64960
    52
     t23 \<Rightarrow> baldL t1 a (B t23 c t4))" |
nipkow@61224
    53
"combine t1 (R t2 a t3) = R (combine t1 t2) a t3" |
nipkow@61224
    54
"combine (R t1 a t2) t3 = R t1 a (combine t2 t3)" 
nipkow@61224
    55
nipkow@61224
    56
end