src/HOL/Data_Structures/RBT_Set.thy
changeset 68413 b56ed5010e69
parent 67967 5a4280946a25
child 68431 b294e095f64c
     1.1 --- a/src/HOL/Data_Structures/RBT_Set.thy	Mon Jun 11 08:15:43 2018 +0200
     1.2 +++ b/src/HOL/Data_Structures/RBT_Set.thy	Mon Jun 11 16:29:27 2018 +0200
     1.3 @@ -28,11 +28,11 @@
     1.4  
     1.5  fun color :: "'a rbt \<Rightarrow> color" where
     1.6  "color Leaf = Black" |
     1.7 -"color (Node c _ _ _) = c"
     1.8 +"color (Node _ _ c _) = c"
     1.9  
    1.10  fun del :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
    1.11  "del x Leaf = Leaf" |
    1.12 -"del x (Node _ l a r) =
    1.13 +"del x (Node l a _ r) =
    1.14    (case cmp x a of
    1.15       LT \<Rightarrow> if l \<noteq> Leaf \<and> color l = Black
    1.16             then baldL (del x l) a r else R (del x l) a r |
    1.17 @@ -97,20 +97,20 @@
    1.18  
    1.19  fun bheight :: "'a rbt \<Rightarrow> nat" where
    1.20  "bheight Leaf = 0" |
    1.21 -"bheight (Node c l x r) = (if c = Black then bheight l + 1 else bheight l)"
    1.22 +"bheight (Node l x c r) = (if c = Black then bheight l + 1 else bheight l)"
    1.23  
    1.24  fun invc :: "'a rbt \<Rightarrow> bool" where
    1.25  "invc Leaf = True" |
    1.26 -"invc (Node c l a r) =
    1.27 +"invc (Node l a c r) =
    1.28    (invc l \<and> invc r \<and> (c = Red \<longrightarrow> color l = Black \<and> color r = Black))"
    1.29  
    1.30  fun invc2 :: "'a rbt \<Rightarrow> bool" \<comment> \<open>Weaker version\<close> where
    1.31  "invc2 Leaf = True" |
    1.32 -"invc2 (Node c l a r) = (invc l \<and> invc r)"
    1.33 +"invc2 (Node l a c r) = (invc l \<and> invc r)"
    1.34  
    1.35  fun invh :: "'a rbt \<Rightarrow> bool" where
    1.36  "invh Leaf = True" |
    1.37 -"invh (Node c l x r) = (invh l \<and> invh r \<and> bheight l = bheight r)"
    1.38 +"invh (Node l x c r) = (invh l \<and> invh r \<and> bheight l = bheight r)"
    1.39  
    1.40  lemma invc2I: "invc t \<Longrightarrow> invc2 t"
    1.41  by (cases t) simp+
    1.42 @@ -232,7 +232,7 @@
    1.43     (color t = Red \<and> bheight (del x t) = bheight t \<and> invc (del x t) \<or>
    1.44      color t = Black \<and> bheight (del x t) = bheight t - 1 \<and> invc2 (del x t))"
    1.45  proof (induct x t rule: del.induct)
    1.46 -case (2 x c _ y)
    1.47 +case (2 x _ y c)
    1.48    have "x = y \<or> x < y \<or> x > y" by auto
    1.49    thus ?case proof (elim disjE)
    1.50      assume "x = y"