# HG changeset patch
# User nipkow
# Date 1485449473 -3600
# Node ID 10b8d31634cc0f5f5d1442d46d01ca201d95d13d
# Parent  09b872c58c32c1a7ea067f6504e3507c3d9dfc3b
added concise log height bound lemma

diff -r 09b872c58c32 -r 10b8d31634cc src/HOL/Data_Structures/RBT_Set.thy
--- a/src/HOL/Data_Structures/RBT_Set.thy	Wed Jan 25 23:09:06 2017 +0100
+++ b/src/HOL/Data_Structures/RBT_Set.thy	Thu Jan 26 17:51:13 2017 +0100
@@ -4,6 +4,7 @@
 
 theory RBT_Set
 imports
+  Complex_Main
   RBT
   Cmp
   Isin2
@@ -284,6 +285,35 @@
 
 subsection \<open>Height-Size Relation\<close>
 
+lemma neq_Black[simp]: "(c \<noteq> Black) = (c = Red)"
+by (cases c) auto
+
+lemma rbt_height_bheight_if_nat: "invc t \<Longrightarrow> invh t \<Longrightarrow>
+  height t \<le> (if color t = Black then 2 * bheight t else 2 * bheight t + 1)"
+by(induction t) (auto split: if_split_asm)
+
+lemma rbt_height_bheight_if: "invc t \<Longrightarrow> invh t \<Longrightarrow>
+  (if color t = Black then height t / 2 else (height t - 1) / 2) \<le> bheight t"
+by(induction t) (auto split: if_split_asm)
+
+lemma rbt_height_bheight: "rbt t \<Longrightarrow> height t / 2 \<le> bheight t "
+by(auto simp: rbt_def dest: rbt_height_bheight_if)
+
+lemma bheight_size_bound:  "invc t \<Longrightarrow> invh t \<Longrightarrow> size1 t \<ge>  2 ^ (bheight t)"
+by (induction t) auto
+
+lemma rbt_height_le: assumes "rbt t" shows "height t \<le> 2 * log 2 (size1 t)"
+proof -
+  have "2 powr (height t / 2) \<le> 2 powr bheight t"
+    using rbt_height_bheight[OF assms] by (simp)
+  also have "\<dots> \<le> size1 t" using assms
+    by (simp add: powr_realpow bheight_size_bound rbt_def)
+  finally have "2 powr (height t / 2) \<le> size1 t" .
+  hence "height t / 2 \<le> log 2 (size1 t)"
+    by(simp add: le_log_iff size1_def del: Int.divide_le_eq_numeral1(1))
+  thus ?thesis by simp
+qed
+
 text \<open>By Daniel St\"uwe\<close>
 
 lemma color_RedE:"color t = Red \<Longrightarrow> invc t =
@@ -336,9 +366,6 @@
 lemma "rbt t \<Longrightarrow> size1 t \<le>  4 ^ (bheight t)"
 by(induction t rule: rbt_induct[where Q="\<lambda> t. size1 t \<le>  2 * 4 ^ (bheight t)"]) auto
 
-lemma bheight_size_bound:  "rbt t \<Longrightarrow> size1 t \<ge>  2 ^ (bheight t)"
-by (induction t rule: rbt_induct[where Q="\<lambda> t. size1 t \<ge>  2 ^ (bheight t)"]) auto
-
 text \<open>Balanced red-balck tree with all black nodes:\<close>
 inductive balB :: "nat \<Rightarrow> unit rbt \<Rightarrow> bool"  where
 "balB 0 Leaf" |