src/HOL/Data_Structures/RBT_Set.thy
changeset 64950 10b8d31634cc
parent 64947 f6ad52152040
child 64951 140addd19343
     1.1 --- a/src/HOL/Data_Structures/RBT_Set.thy	Wed Jan 25 23:09:06 2017 +0100
     1.2 +++ b/src/HOL/Data_Structures/RBT_Set.thy	Thu Jan 26 17:51:13 2017 +0100
     1.3 @@ -4,6 +4,7 @@
     1.4  
     1.5  theory RBT_Set
     1.6  imports
     1.7 +  Complex_Main
     1.8    RBT
     1.9    Cmp
    1.10    Isin2
    1.11 @@ -284,6 +285,35 @@
    1.12  
    1.13  subsection \<open>Height-Size Relation\<close>
    1.14  
    1.15 +lemma neq_Black[simp]: "(c \<noteq> Black) = (c = Red)"
    1.16 +by (cases c) auto
    1.17 +
    1.18 +lemma rbt_height_bheight_if_nat: "invc t \<Longrightarrow> invh t \<Longrightarrow>
    1.19 +  height t \<le> (if color t = Black then 2 * bheight t else 2 * bheight t + 1)"
    1.20 +by(induction t) (auto split: if_split_asm)
    1.21 +
    1.22 +lemma rbt_height_bheight_if: "invc t \<Longrightarrow> invh t \<Longrightarrow>
    1.23 +  (if color t = Black then height t / 2 else (height t - 1) / 2) \<le> bheight t"
    1.24 +by(induction t) (auto split: if_split_asm)
    1.25 +
    1.26 +lemma rbt_height_bheight: "rbt t \<Longrightarrow> height t / 2 \<le> bheight t "
    1.27 +by(auto simp: rbt_def dest: rbt_height_bheight_if)
    1.28 +
    1.29 +lemma bheight_size_bound:  "invc t \<Longrightarrow> invh t \<Longrightarrow> size1 t \<ge>  2 ^ (bheight t)"
    1.30 +by (induction t) auto
    1.31 +
    1.32 +lemma rbt_height_le: assumes "rbt t" shows "height t \<le> 2 * log 2 (size1 t)"
    1.33 +proof -
    1.34 +  have "2 powr (height t / 2) \<le> 2 powr bheight t"
    1.35 +    using rbt_height_bheight[OF assms] by (simp)
    1.36 +  also have "\<dots> \<le> size1 t" using assms
    1.37 +    by (simp add: powr_realpow bheight_size_bound rbt_def)
    1.38 +  finally have "2 powr (height t / 2) \<le> size1 t" .
    1.39 +  hence "height t / 2 \<le> log 2 (size1 t)"
    1.40 +    by(simp add: le_log_iff size1_def del: Int.divide_le_eq_numeral1(1))
    1.41 +  thus ?thesis by simp
    1.42 +qed
    1.43 +
    1.44  text \<open>By Daniel St\"uwe\<close>
    1.45  
    1.46  lemma color_RedE:"color t = Red \<Longrightarrow> invc t =
    1.47 @@ -336,9 +366,6 @@
    1.48  lemma "rbt t \<Longrightarrow> size1 t \<le>  4 ^ (bheight t)"
    1.49  by(induction t rule: rbt_induct[where Q="\<lambda> t. size1 t \<le>  2 * 4 ^ (bheight t)"]) auto
    1.50  
    1.51 -lemma bheight_size_bound:  "rbt t \<Longrightarrow> size1 t \<ge>  2 ^ (bheight t)"
    1.52 -by (induction t rule: rbt_induct[where Q="\<lambda> t. size1 t \<ge>  2 ^ (bheight t)"]) auto
    1.53 -
    1.54  text \<open>Balanced red-balck tree with all black nodes:\<close>
    1.55  inductive balB :: "nat \<Rightarrow> unit rbt \<Rightarrow> bool"  where
    1.56  "balB 0 Leaf" |