src/HOL/Data_Structures/RBT_Set.thy
changeset 67963 9541f2c5ce8d
parent 67118 ccab07d1196c
child 67967 5a4280946a25
     1.1 --- a/src/HOL/Data_Structures/RBT_Set.thy	Fri Apr 06 17:34:50 2018 +0200
     1.2 +++ b/src/HOL/Data_Structures/RBT_Set.thy	Sat Apr 07 22:09:57 2018 +0200
     1.3 @@ -281,18 +281,14 @@
     1.4  lemma neq_Black[simp]: "(c \<noteq> Black) = (c = Red)"
     1.5  by (cases c) auto
     1.6  
     1.7 -lemma rbt_height_bheight_if_nat: "invc t \<Longrightarrow> invh t \<Longrightarrow>
     1.8 +lemma rbt_height_bheight_if: "invc t \<Longrightarrow> invh t \<Longrightarrow>
     1.9    height t \<le> (if color t = Black then 2 * bheight t else 2 * bheight t + 1)"
    1.10  by(induction t) (auto split: if_split_asm)
    1.11  
    1.12 -lemma rbt_height_bheight_if: "invc t \<Longrightarrow> invh t \<Longrightarrow>
    1.13 -  (if color t = Black then height t / 2 else (height t - 1) / 2) \<le> bheight t"
    1.14 -by(induction t) (auto split: if_split_asm)
    1.15 -
    1.16  lemma rbt_height_bheight: "rbt t \<Longrightarrow> height t / 2 \<le> bheight t "
    1.17  by(auto simp: rbt_def dest: rbt_height_bheight_if)
    1.18  
    1.19 -lemma bheight_size_bound:  "invc t \<Longrightarrow> invh t \<Longrightarrow> size1 t \<ge>  2 ^ (bheight t)"
    1.20 +lemma bheight_size_bound:  "invc t \<Longrightarrow> invh t \<Longrightarrow> 2 ^ (bheight t) \<le> size1 t"
    1.21  by (induction t) auto
    1.22  
    1.23  lemma rbt_height_le: assumes "rbt t" shows "height t \<le> 2 * log 2 (size1 t)"