correct definition for skip_black
authorAndreas Lochbihler
Wed Oct 10 15:05:07 2012 +0200 (2012-10-10)
changeset 498079a0843995fd3
parent 49771 b1493798d253
child 49808 418991ce7567
correct definition for skip_black
src/HOL/Library/RBT_Impl.thy
     1.1 --- a/src/HOL/Library/RBT_Impl.thy	Wed Oct 10 13:04:15 2012 +0200
     1.2 +++ b/src/HOL/Library/RBT_Impl.thy	Wed Oct 10 15:05:07 2012 +0200
     1.3 @@ -1725,10 +1725,9 @@
     1.4    "skip_red (Branch color.R l k v r) = l"
     1.5  | "skip_red t = t"
     1.6  
     1.7 -fun skip_black :: "('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
     1.8 +definition skip_black :: "('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
     1.9  where
    1.10 -  "skip_black (Branch color.B l k v r) = l"
    1.11 -| "skip_black t = t"
    1.12 +  "skip_black t = (let t' = skip_red t in case t' of Branch color.B l k v r \<Rightarrow> l | _ \<Rightarrow> t')"
    1.13  
    1.14  datatype compare = LT | GT | EQ
    1.15  
    1.16 @@ -1761,9 +1760,9 @@
    1.17    compare.eq.refl compare.eq.simps
    1.18    compare.EQ_def compare.GT_def compare.LT_def
    1.19    equal_compare_def
    1.20 -  skip_red_def skip_red.simps skip_red.induct 
    1.21 -  skip_black_def skip_black.simps skip_black.induct
    1.22 -  compare_height.simps
    1.23 +  skip_red_def skip_red.simps skip_red.cases skip_red.induct 
    1.24 +  skip_black_def
    1.25 +  compare_height_def compare_height.simps
    1.26  
    1.27  subsection {* union and intersection of sorted associative lists *}
    1.28