src/HOL/Data_Structures/RBT_Set.thy
changeset 71555 7a0a6c56015e
parent 70944 3fb16bed5d6c
child 71557 857453c0db3d
equal deleted inserted replaced
71554:a956b769903e 71555:7a0a6c56015e
   289 
   289 
   290 lemma neq_Black[simp]: "(c \<noteq> Black) = (c = Red)"
   290 lemma neq_Black[simp]: "(c \<noteq> Black) = (c = Red)"
   291 by (cases c) auto
   291 by (cases c) auto
   292 
   292 
   293 lemma rbt_height_bheight_if: "invc t \<Longrightarrow> invh t \<Longrightarrow>
   293 lemma rbt_height_bheight_if: "invc t \<Longrightarrow> invh t \<Longrightarrow>
   294   height t \<le> (if color t = Black then 2 * bheight t else 2 * bheight t + 1)"
   294   height t \<le> 2 * bheight t + (if color t = Black then 0 else 1)"
   295 by(induction t) (auto split: if_split_asm)
   295 by(induction t) (auto split: if_split_asm)
   296 
   296 
   297 lemma rbt_height_bheight: "rbt t \<Longrightarrow> height t / 2 \<le> bheight t "
   297 lemma rbt_height_bheight: "rbt t \<Longrightarrow> height t / 2 \<le> bheight t "
   298 by(auto simp: rbt_def dest: rbt_height_bheight_if)
   298 by(auto simp: rbt_def dest: rbt_height_bheight_if)
   299 
   299