make baliL and baliR symmetric
authornipkow
Thu Mar 22 13:53:15 2018 +0100 (14 months ago)
changeset 67910b42473502373
parent 67909 f55b07f4d1ee
child 67926 e6b9703b9656
make baliL and baliR symmetric
src/HOL/Data_Structures/RBT.thy
     1.1 --- a/src/HOL/Data_Structures/RBT.thy	Wed Mar 21 20:17:25 2018 +0100
     1.2 +++ b/src/HOL/Data_Structures/RBT.thy	Thu Mar 22 13:53:15 2018 +0100
     1.3 @@ -19,8 +19,8 @@
     1.4  "baliL t1 a t2 = B t1 a t2"
     1.5  
     1.6  fun baliR :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
     1.7 +"baliR t1 a1 (R t2 a2 (R t3 a3 t4)) = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
     1.8  "baliR t1 a1 (R (R t2 a2 t3) a3 t4) = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
     1.9 -"baliR t1 a1 (R t2 a2 (R t3 a3 t4)) = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
    1.10  "baliR t1 a t2 = B t1 a t2"
    1.11  
    1.12  fun paint :: "color \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where