src/HOL/Data_Structures/RBT_Set.thy
author nipkow
Thu Jan 26 17:51:13 2017 +0100 (2017-01-26)
changeset 64950 10b8d31634cc
parent 64947 f6ad52152040
child 64951 140addd19343
permissions -rw-r--r--
added concise log height bound lemma
     1 (* Author: Tobias Nipkow, Daniel Stüwe *)
     2 
     3 section \<open>Red-Black Tree Implementation of Sets\<close>
     4 
     5 theory RBT_Set
     6 imports
     7   Complex_Main
     8   RBT
     9   Cmp
    10   Isin2
    11 begin
    12 
    13 fun ins :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
    14 "ins x Leaf = R Leaf x Leaf" |
    15 "ins x (B l a r) =
    16   (case cmp x a of
    17      LT \<Rightarrow> bal (ins x l) a r |
    18      GT \<Rightarrow> bal l a (ins x r) |
    19      EQ \<Rightarrow> B l a r)" |
    20 "ins x (R l a r) =
    21   (case cmp x a of
    22     LT \<Rightarrow> R (ins x l) a r |
    23     GT \<Rightarrow> R l a (ins x r) |
    24     EQ \<Rightarrow> R l a r)"
    25 
    26 definition insert :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
    27 "insert x t = paint Black (ins x t)"
    28 
    29 fun del :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt"
    30 and delL :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt"
    31 and delR :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt"
    32 where
    33 "del x Leaf = Leaf" |
    34 "del x (Node _ l a r) =
    35   (case cmp x a of
    36      LT \<Rightarrow> delL x l a r |
    37      GT \<Rightarrow> delR x l a r |
    38      EQ \<Rightarrow> combine l r)" |
    39 "delL x (B t1 a t2) b t3 = balL (del x (B t1 a t2)) b t3" |
    40 "delL x l a r = R (del x l) a r" |
    41 "delR x t1 a (B t2 b t3) = balR t1 a (del x (B t2 b t3))" | 
    42 "delR x l a r = R l a (del x r)"
    43 
    44 definition delete :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
    45 "delete x t = paint Black (del x t)"
    46 
    47 
    48 subsection "Functional Correctness Proofs"
    49 
    50 lemma inorder_paint: "inorder(paint c t) = inorder t"
    51 by(cases t) (auto)
    52 
    53 lemma inorder_bal:
    54   "inorder(bal l a r) = inorder l @ a # inorder r"
    55 by(cases "(l,a,r)" rule: bal.cases) (auto)
    56 
    57 lemma inorder_ins:
    58   "sorted(inorder t) \<Longrightarrow> inorder(ins x t) = ins_list x (inorder t)"
    59 by(induction x t rule: ins.induct) (auto simp: ins_list_simps inorder_bal)
    60 
    61 lemma inorder_insert:
    62   "sorted(inorder t) \<Longrightarrow> inorder(insert x t) = ins_list x (inorder t)"
    63 by (simp add: insert_def inorder_ins inorder_paint)
    64 
    65 lemma inorder_balL:
    66   "inorder(balL l a r) = inorder l @ a # inorder r"
    67 by(cases "(l,a,r)" rule: balL.cases)(auto simp: inorder_bal inorder_paint)
    68 
    69 lemma inorder_balR:
    70   "inorder(balR l a r) = inorder l @ a # inorder r"
    71 by(cases "(l,a,r)" rule: balR.cases) (auto simp: inorder_bal inorder_paint)
    72 
    73 lemma inorder_combine:
    74   "inorder(combine l r) = inorder l @ inorder r"
    75 by(induction l r rule: combine.induct)
    76   (auto simp: inorder_balL inorder_balR split: tree.split color.split)
    77 
    78 lemma inorder_del:
    79  "sorted(inorder t) \<Longrightarrow>  inorder(del x t) = del_list x (inorder t)"
    80  "sorted(inorder l) \<Longrightarrow>  inorder(delL x l a r) =
    81     del_list x (inorder l) @ a # inorder r"
    82  "sorted(inorder r) \<Longrightarrow>  inorder(delR x l a r) =
    83     inorder l @ a # del_list x (inorder r)"
    84 by(induction x t and x l a r and x l a r rule: del_delL_delR.induct)
    85   (auto simp: del_list_simps inorder_combine inorder_balL inorder_balR)
    86 
    87 lemma inorder_delete:
    88   "sorted(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
    89 by (auto simp: delete_def inorder_del inorder_paint)
    90 
    91 
    92 subsection \<open>Structural invariants\<close>
    93 
    94 text\<open>The proofs are due to Markus Reiter and Alexander Krauss,\<close>
    95 
    96 fun color :: "'a rbt \<Rightarrow> color" where
    97 "color Leaf = Black" |
    98 "color (Node c _ _ _) = c"
    99 
   100 fun bheight :: "'a rbt \<Rightarrow> nat" where
   101 "bheight Leaf = 0" |
   102 "bheight (Node c l x r) = (if c = Black then Suc(bheight l) else bheight l)"
   103 
   104 fun invc :: "'a rbt \<Rightarrow> bool" where
   105 "invc Leaf = True" |
   106 "invc (Node c l a r) =
   107   (invc l \<and> invc r \<and> (c = Red \<longrightarrow> color l = Black \<and> color r = Black))"
   108 
   109 fun invc_sons :: "'a rbt \<Rightarrow> bool" \<comment> \<open>Weaker version\<close> where
   110 "invc_sons Leaf = True" |
   111 "invc_sons (Node c l a r) = (invc l \<and> invc r)"
   112 
   113 fun invh :: "'a rbt \<Rightarrow> bool" where
   114 "invh Leaf = True" |
   115 "invh (Node c l x r) = (invh l \<and> invh r \<and> bheight l = bheight r)"
   116 
   117 lemma invc_sonsI: "invc t \<Longrightarrow> invc_sons t"
   118 by (cases t) simp+
   119 
   120 definition rbt :: "'a rbt \<Rightarrow> bool" where
   121 "rbt t = (invc t \<and> invh t \<and> color t = Black)"
   122 
   123 lemma color_paint_Black: "color (paint Black t) = Black"
   124 by (cases t) auto
   125 
   126 theorem rbt_Leaf: "rbt Leaf"
   127 by (simp add: rbt_def)
   128 
   129 lemma paint_invc_sons: "invc_sons t \<Longrightarrow> invc_sons (paint c t)"
   130 by (cases t) auto
   131 
   132 lemma invc_paint_Black: "invc_sons t \<Longrightarrow> invc (paint Black t)"
   133 by (cases t) auto
   134 
   135 lemma invh_paint: "invh t \<Longrightarrow> invh (paint c t)"
   136 by (cases t) auto
   137 
   138 lemma invc_bal: "\<lbrakk>invc_sons l; invc_sons r\<rbrakk> \<Longrightarrow> invc (bal l a r)" 
   139 by (induct l a r rule: bal.induct) auto
   140 
   141 lemma bheight_bal:
   142   "bheight l = bheight r \<Longrightarrow> bheight (bal l a r) = Suc (bheight l)"
   143 by (induct l a r rule: bal.induct) auto
   144 
   145 lemma invh_bal: 
   146   "\<lbrakk> invh l; invh r; bheight l = bheight r \<rbrakk> \<Longrightarrow> invh (bal l a r)"
   147 by (induct l a r rule: bal.induct) auto
   148 
   149 
   150 subsubsection \<open>Insertion\<close>
   151 
   152 lemma invc_ins: assumes "invc t"
   153   shows "color t = Black \<Longrightarrow> invc (ins x t)" "invc_sons (ins x t)"
   154 using assms
   155 by (induct x t rule: ins.induct) (auto simp: invc_bal invc_sonsI)
   156 
   157 lemma invh_ins: assumes "invh t"
   158   shows "invh (ins x t)" "bheight (ins x t) = bheight t"
   159 using assms
   160 by (induct x t rule: ins.induct) (auto simp: invh_bal bheight_bal)
   161 
   162 theorem rbt_insert: "rbt t \<Longrightarrow> rbt (insert x t)"
   163 by (simp add: invc_ins invh_ins color_paint_Black invc_paint_Black invh_paint
   164   rbt_def insert_def)
   165 
   166 
   167 subsubsection \<open>Deletion\<close>
   168 
   169 lemma bheight_paint_Red:
   170   "color t = Black \<Longrightarrow> bheight (paint Red t) = bheight t - 1"
   171 by (cases t) auto
   172 
   173 lemma balL_invh_with_invc:
   174   assumes "invh lt" "invh rt" "bheight lt + 1 = bheight rt" "invc rt"
   175   shows "bheight (balL lt a rt) = bheight lt + 1"  "invh (balL lt a rt)"
   176 using assms 
   177 by (induct lt a rt rule: balL.induct)
   178    (auto simp: invh_bal invh_paint bheight_bal bheight_paint_Red)
   179 
   180 lemma balL_invh_app: 
   181   assumes "invh lt" "invh rt" "bheight lt + 1 = bheight rt" "color rt = Black"
   182   shows "invh (balL lt a rt)" 
   183         "bheight (balL lt a rt) = bheight rt"
   184 using assms 
   185 by (induct lt a rt rule: balL.induct) (auto simp add: invh_bal bheight_bal) 
   186 
   187 lemma balL_invc: "\<lbrakk>invc_sons l; invc r; color r = Black\<rbrakk> \<Longrightarrow> invc (balL l a r)"
   188 by (induct l a r rule: balL.induct) (simp_all add: invc_bal)
   189 
   190 lemma balL_invc_sons: "\<lbrakk> invc_sons lt; invc rt \<rbrakk> \<Longrightarrow> invc_sons (balL lt a rt)"
   191 by (induct lt a rt rule: balL.induct) (auto simp: invc_bal paint_invc_sons invc_sonsI)
   192 
   193 lemma balR_invh_with_invc:
   194   assumes "invh lt" "invh rt" "bheight lt = bheight rt + 1" "invc lt"
   195   shows "invh (balR lt a rt) \<and> bheight (balR lt a rt) = bheight lt"
   196 using assms
   197 by(induct lt a rt rule: balR.induct)
   198   (auto simp: invh_bal bheight_bal invh_paint bheight_paint_Red)
   199 
   200 lemma invc_balR: "\<lbrakk>invc a; invc_sons b; color a = Black\<rbrakk> \<Longrightarrow> invc (balR a x b)"
   201 by (induct a x b rule: balR.induct) (simp_all add: invc_bal)
   202 
   203 lemma invc_sons_balR: "\<lbrakk> invc lt; invc_sons rt \<rbrakk> \<Longrightarrow>invc_sons (balR lt x rt)"
   204 by (induct lt x rt rule: balR.induct) (auto simp: invc_bal paint_invc_sons invc_sonsI)
   205 
   206 lemma invh_combine:
   207   assumes "invh lt" "invh rt" "bheight lt = bheight rt"
   208   shows "bheight (combine lt rt) = bheight lt" "invh (combine lt rt)"
   209 using assms 
   210 by (induct lt rt rule: combine.induct) 
   211    (auto simp: balL_invh_app split: tree.splits color.splits)
   212 
   213 lemma invc_combine: 
   214   assumes "invc lt" "invc rt"
   215   shows "color lt = Black \<Longrightarrow> color rt = Black \<Longrightarrow> invc (combine lt rt)"
   216          "invc_sons (combine lt rt)"
   217 using assms 
   218 by (induct lt rt rule: combine.induct)
   219    (auto simp: balL_invc invc_sonsI split: tree.splits color.splits)
   220 
   221 
   222 lemma assumes "invh lt" "invc lt"
   223   shows
   224   del_invc_invh: "invh (del x lt) \<and> (color lt = Red \<and> bheight (del x lt) = bheight lt \<and> invc (del x lt) 
   225   \<or> color lt = Black \<and> bheight (del x lt) = bheight lt - 1 \<and> invc_sons (del x lt))"
   226 and  "\<lbrakk>invh rt; bheight lt = bheight rt; invc rt\<rbrakk> \<Longrightarrow>
   227    invh (delL x lt k rt) \<and> 
   228    bheight (delL x lt k rt) = bheight lt \<and> 
   229    (color lt = Black \<and> color rt = Black \<and> invc (delL x lt k rt) \<or> 
   230     (color lt \<noteq> Black \<or> color rt \<noteq> Black) \<and> invc_sons (delL x lt k rt))"
   231   and "\<lbrakk>invh rt; bheight lt = bheight rt; invc rt\<rbrakk> \<Longrightarrow>
   232   invh (delR x lt k rt) \<and> 
   233   bheight (delR x lt k rt) = bheight lt \<and> 
   234   (color lt = Black \<and> color rt = Black \<and> invc (delR x lt k rt) \<or> 
   235    (color lt \<noteq> Black \<or> color rt \<noteq> Black) \<and> invc_sons (delR x lt k rt))"
   236 using assms
   237 proof (induct x lt and x lt k rt and x lt k rt rule: del_delL_delR.induct)
   238 case (2 y c _ y')
   239   have "y = y' \<or> y < y' \<or> y > y'" by auto
   240   thus ?case proof (elim disjE)
   241     assume "y = y'"
   242     with 2 show ?thesis
   243     by (cases c) (simp_all add: invh_combine invc_combine)
   244   next
   245     assume "y < y'"
   246     with 2 show ?thesis by (cases c) (auto simp: invc_sonsI)
   247   next
   248     assume "y' < y"
   249     with 2 show ?thesis by (cases c) (auto simp: invc_sonsI)
   250   qed
   251 next
   252   case (3 y lt z rta y' bb)
   253   thus ?case by (cases "color (Node Black lt z rta) = Black \<and> color bb = Black") (simp add: balL_invh_with_invc balL_invc balL_invc_sons)+
   254 next
   255   case (5 y a y' lt z rta)
   256   thus ?case by (cases "color a = Black \<and> color (Node Black lt z rta) = Black") (simp add: balR_invh_with_invc invc_balR invc_sons_balR)+
   257 next
   258   case ("6_1" y a y') thus ?case by (cases "color a = Black \<and> color Leaf = Black") simp+
   259 qed auto
   260 
   261 theorem rbt_delete: "rbt t \<Longrightarrow> rbt (delete k t)"
   262 by (metis delete_def rbt_def color_paint_Black del_invc_invh invc_paint_Black invc_sonsI invh_paint)
   263 
   264 text \<open>Overall correctness:\<close>
   265 
   266 interpretation Set_by_Ordered
   267 where empty = Leaf and isin = isin and insert = insert and delete = delete
   268 and inorder = inorder and inv = rbt
   269 proof (standard, goal_cases)
   270   case 1 show ?case by simp
   271 next
   272   case 2 thus ?case by(simp add: isin_set)
   273 next
   274   case 3 thus ?case by(simp add: inorder_insert)
   275 next
   276   case 4 thus ?case by(simp add: inorder_delete)
   277 next
   278   case 5 thus ?case by (simp add: rbt_Leaf) 
   279 next
   280   case 6 thus ?case by (simp add: rbt_insert) 
   281 next
   282   case 7 thus ?case by (simp add: rbt_delete) 
   283 qed
   284 
   285 
   286 subsection \<open>Height-Size Relation\<close>
   287 
   288 lemma neq_Black[simp]: "(c \<noteq> Black) = (c = Red)"
   289 by (cases c) auto
   290 
   291 lemma rbt_height_bheight_if_nat: "invc t \<Longrightarrow> invh t \<Longrightarrow>
   292   height t \<le> (if color t = Black then 2 * bheight t else 2 * bheight t + 1)"
   293 by(induction t) (auto split: if_split_asm)
   294 
   295 lemma rbt_height_bheight_if: "invc t \<Longrightarrow> invh t \<Longrightarrow>
   296   (if color t = Black then height t / 2 else (height t - 1) / 2) \<le> bheight t"
   297 by(induction t) (auto split: if_split_asm)
   298 
   299 lemma rbt_height_bheight: "rbt t \<Longrightarrow> height t / 2 \<le> bheight t "
   300 by(auto simp: rbt_def dest: rbt_height_bheight_if)
   301 
   302 lemma bheight_size_bound:  "invc t \<Longrightarrow> invh t \<Longrightarrow> size1 t \<ge>  2 ^ (bheight t)"
   303 by (induction t) auto
   304 
   305 lemma rbt_height_le: assumes "rbt t" shows "height t \<le> 2 * log 2 (size1 t)"
   306 proof -
   307   have "2 powr (height t / 2) \<le> 2 powr bheight t"
   308     using rbt_height_bheight[OF assms] by (simp)
   309   also have "\<dots> \<le> size1 t" using assms
   310     by (simp add: powr_realpow bheight_size_bound rbt_def)
   311   finally have "2 powr (height t / 2) \<le> size1 t" .
   312   hence "height t / 2 \<le> log 2 (size1 t)"
   313     by(simp add: le_log_iff size1_def del: Int.divide_le_eq_numeral1(1))
   314   thus ?thesis by simp
   315 qed
   316 
   317 text \<open>By Daniel St\"uwe\<close>
   318 
   319 lemma color_RedE:"color t = Red \<Longrightarrow> invc t =
   320  (\<exists> l a r . t = R l a r \<and> color l = Black \<and> color r = Black \<and> invc l \<and> invc r)"
   321 by (cases t) auto
   322 
   323 lemma rbt_induct[consumes 1]:
   324   assumes "rbt t"
   325   assumes [simp]: "P Leaf"
   326   assumes "\<And> t l a r. \<lbrakk>t = B l a r; invc t; invh t; Q(l); Q(r)\<rbrakk> \<Longrightarrow> P t"
   327   assumes "\<And> t l a r. \<lbrakk>t = R l a r; invc t; invh t; P(l); P(r)\<rbrakk> \<Longrightarrow> Q t"
   328   assumes "\<And> t . P(t) \<Longrightarrow> Q(t)"
   329   shows "P t"
   330 using assms(1) unfolding rbt_def apply safe
   331 proof (induction t rule: measure_induct[of size])
   332 case (1 t)
   333   note * = 1 assms
   334   show ?case proof (cases t)
   335     case [simp]: (Node c l a r)
   336     show ?thesis proof (cases c)
   337       case Red thus ?thesis using 1 by simp
   338     next
   339       case [simp]: Black
   340       show ?thesis
   341       proof (cases "color l")
   342         case Red
   343         thus ?thesis using * by (cases "color r") (auto simp: color_RedE)
   344       next
   345         case Black
   346         thus ?thesis using * by (cases "color r") (auto simp: color_RedE)
   347       qed
   348     qed
   349   qed simp
   350 qed
   351 
   352 lemma rbt_b_height: "rbt t \<Longrightarrow> bheight t * 2 \<ge> height t"
   353 by (induction t rule: rbt_induct[where Q="\<lambda> t. bheight t * 2 + 1 \<ge> height t"]) auto
   354 
   355 lemma red_b_height: "invc t \<Longrightarrow> invh t \<Longrightarrow> bheight t * 2 + 1 \<ge> height t"
   356 apply (cases t) apply simp
   357   using rbt_b_height unfolding rbt_def
   358   by (cases "color t") fastforce+
   359 
   360 lemma red_b_height2: "invc t \<Longrightarrow> invh t \<Longrightarrow> bheight t \<ge> height t div 2"
   361 using red_b_height by fastforce
   362 
   363 lemma rbt_b_height2: "bheight t \<le> height t"
   364 by (induction t) auto
   365 
   366 lemma "rbt t \<Longrightarrow> size1 t \<le>  4 ^ (bheight t)"
   367 by(induction t rule: rbt_induct[where Q="\<lambda> t. size1 t \<le>  2 * 4 ^ (bheight t)"]) auto
   368 
   369 text \<open>Balanced red-balck tree with all black nodes:\<close>
   370 inductive balB :: "nat \<Rightarrow> unit rbt \<Rightarrow> bool"  where
   371 "balB 0 Leaf" |
   372 "balB h t \<Longrightarrow> balB (Suc h) (B t () t)"
   373 
   374 inductive_cases [elim!]: "balB 0 t"
   375 inductive_cases [elim]: "balB (Suc h) t"
   376 
   377 lemma balB_hs: "balB h t \<Longrightarrow> bheight t = height t"
   378 by (induction h t rule: "balB.induct") auto
   379 
   380 lemma balB_h: "balB h t \<Longrightarrow> h = height t"
   381 by (induction h t rule: "balB.induct") auto
   382 
   383 lemma "rbt t \<Longrightarrow> balB (bheight t) t' \<Longrightarrow> size t' \<le> size t"
   384 by (induction t arbitrary: t' 
   385  rule: rbt_induct[where Q="\<lambda> t . \<forall> h t'. balB (bheight t) t' \<longrightarrow> size t' \<le> size t"])
   386  fastforce+
   387 
   388 lemma balB_bh: "invc t \<Longrightarrow> invh t \<Longrightarrow> balB (bheight t) t' \<Longrightarrow> size t' \<le> size t"
   389 by (induction t arbitrary: t') (fastforce split: if_split_asm)+
   390 
   391 lemma balB_bh3:"\<lbrakk> balB h t; balB (h' + h) t' \<rbrakk> \<Longrightarrow> size t \<le> size t'"
   392 by (induction h t arbitrary: t' h' rule: balB.induct)  fastforce+
   393 
   394 corollary balB_bh3': "\<lbrakk> balB h t; balB h' t'; h \<le> h' \<rbrakk> \<Longrightarrow> size t \<le> size t'"
   395 using balB_bh3 le_Suc_ex by (fastforce simp: algebra_simps)
   396 
   397 lemma exist_pt: "\<exists> t . balB h t"
   398 by (induction h) (auto intro: balB.intros)
   399 
   400 corollary compact_pt:
   401   assumes "invc t" "invh t" "h \<le> bheight t" "balB h t'"
   402   shows   "size t' \<le> size t"
   403 proof -
   404   obtain t'' where "balB (bheight t) t''" using exist_pt by blast
   405   thus ?thesis using assms balB_bh[of t t''] balB_bh3'[of h t' "bheight t" t''] by auto
   406 qed
   407 
   408 lemma balB_bh2: "balB (bheight t) t'\<Longrightarrow> invc t \<Longrightarrow> invh t \<Longrightarrow> height t' \<le> height t"
   409 apply (induction "(bheight t)" t' arbitrary: t rule: balB.induct)
   410 using balB_h rbt_b_height2 by auto
   411 
   412 lemma balB_rbt: "balB h t \<Longrightarrow> rbt t"
   413 unfolding rbt_def
   414 by (induction h t rule: balB.induct) auto
   415 
   416 lemma balB_size[simp]: "balB h t \<Longrightarrow> size1 t = 2^h"
   417 by (induction h t rule: balB.induct) auto
   418 
   419 text \<open>Red-black tree (except that the root may be red) of minimal size
   420 for a given height:\<close>
   421 
   422 inductive RB :: "nat \<Rightarrow> unit rbt \<Rightarrow> bool" where
   423 "RB 0 Leaf" |
   424 "balB (h div 2) t \<Longrightarrow> RB h t' \<Longrightarrow> color t' = Red \<Longrightarrow> RB (Suc h) (B t' () t)" |
   425 "balB (h div 2) t \<Longrightarrow> RB h t' \<Longrightarrow> color t' = Black \<Longrightarrow> RB (Suc h) (R t' () t)" 
   426 
   427 lemmas RB.intros[intro]
   428 
   429 lemma RB_invc: "RB h t \<Longrightarrow> invc t"
   430 apply (induction h t rule: RB.induct)
   431 using balB_rbt unfolding rbt_def by auto
   432 
   433 lemma RB_h: "RB h t \<Longrightarrow> h = height t"
   434 apply (induction h t rule: RB.induct)
   435 using balB_h by auto
   436 
   437 lemma RB_mod: "RB h t \<Longrightarrow> (color t = Black \<longleftrightarrow> h mod 2 = 0)"
   438 apply (induction h t rule: RB.induct)
   439 apply auto
   440 by presburger
   441 
   442 lemma RB_b_height: "RB h t \<Longrightarrow> height t div 2 = bheight t"
   443 proof  (induction h t rule: RB.induct)
   444   case 1 
   445   thus ?case by auto 
   446 next
   447   case (2 h t t')
   448   with RB_mod obtain n where "2*n + 1 = h" 
   449     by (metis color.distinct(1) mult_div_mod_eq parity) 
   450   with 2 balB_h RB_h show ?case by auto
   451 next
   452   case (3 h t t')
   453   with RB_mod[OF 3(2)] parity obtain n where "2*n = h" by blast
   454   with 3 balB_h RB_h show ?case by auto
   455 qed
   456 
   457 lemma weak_RB_induct[consumes 1]: 
   458   "RB h t \<Longrightarrow> P 0 \<langle>\<rangle> \<Longrightarrow> (\<And>h t t' c . balB (h div 2) t \<Longrightarrow> RB h t' \<Longrightarrow>
   459     P h t' \<Longrightarrow> P (Suc h) (Node c t' () t)) \<Longrightarrow> P h t"
   460 using RB.induct by metis
   461 
   462 lemma RB_invh: "RB h t \<Longrightarrow> invh t"
   463 apply (induction h t rule: weak_RB_induct)
   464   using balB_h balB_hs RB_h balB_rbt RB_b_height
   465   unfolding rbt_def
   466 by auto
   467 
   468 lemma RB_bheight_minimal:
   469   "\<lbrakk>RB (height t') t; invc t'; invh t'\<rbrakk> \<Longrightarrow> bheight t \<le> bheight t'"
   470 using RB_b_height RB_h red_b_height2 by fastforce
   471 
   472 lemma RB_minimal: "RB (height t') t \<Longrightarrow> invh t \<Longrightarrow> invc t' \<Longrightarrow> invh t' \<Longrightarrow> size t \<le> size t'"
   473 proof (induction "(height t')" t arbitrary: t' rule: weak_RB_induct)
   474   case 1 thus ?case by auto 
   475 next
   476   case (2 h t t'')
   477   have ***: "size (Node c t'' () t) \<le> size t'"
   478     if assms:
   479       "\<And> (t' :: 'a rbt) . \<lbrakk> h = height t'; invh t''; invc t'; invh t' \<rbrakk>
   480                             \<Longrightarrow> size t'' \<le> size t'"
   481       "Suc h = height t'" "balB (h div 2) t" "RB h t''"
   482       "invc t'" "invh t'" "height l \<ge> height r"
   483       and tt[simp]:"t' = Node c l a r" and last: "invh (Node c t'' () t)"
   484   for t' :: "'a rbt" and c l a r
   485   proof -
   486     from assms have inv: "invc r" "invh r" by auto
   487     from assms have "height l = h" using max_def by auto
   488     with RB_bheight_minimal[of l t''] have
   489       "bheight t \<le> bheight r" using assms last by auto
   490     with compact_pt[OF inv] balB_h balB_hs have 
   491       "size t \<le> size r" using assms(3) by auto moreover
   492     have "size t'' \<le> size l" using assms last by auto ultimately
   493     show ?thesis by simp
   494   qed
   495   
   496   from 2 obtain c l a r where 
   497     t': "t' = Node c l a r" by (cases t') auto
   498   with 2 have inv: "invc l" "invh l" "invc r" "invh r" by auto
   499   show ?case proof (cases "height r \<le> height l")
   500     case True thus ?thesis using ***[OF 2(3,4,1,2,6,7)] t' 2(5) by auto
   501   next
   502     case False 
   503     obtain t''' where t''' : "t''' = Node c r a l" "invc t'''" "invh t'''" using 2 t' by auto
   504     have "size t''' = size t'" and 4 : "Suc h = height t'''" using 2(4) t' t''' by auto
   505     thus ?thesis using ***[OF 2(3) 4 2(1,2) t'''(2,3) _ t'''(1)] 2(5) False by auto
   506   qed
   507 qed
   508 
   509 lemma RB_size: "RB h t \<Longrightarrow> size1 t + 1 = 2^((h+1) div 2) + 2^(h div 2)"
   510 by (induction h t rule: "RB.induct" ) auto
   511 
   512 lemma RB_exist: "\<exists> t . RB h t"
   513 proof (induction h) 
   514   case (Suc n)
   515   obtain r where r: "balB (n div 2) r"  using  exist_pt by blast
   516   obtain l where l: "RB n l"  using  Suc by blast
   517   obtain t where 
   518     "color l = Red   \<Longrightarrow> t = B l () r"
   519     "color l = Black \<Longrightarrow> t = R l () r" by auto
   520   with l and r have "RB (Suc n) t" by (cases "color l") auto
   521   thus ?case by auto
   522 qed auto
   523 
   524 lemma bound:
   525   assumes "invc t"  "invh t" and [simp]:"height t = h"
   526   shows "size t \<ge> 2^((h+1) div 2) + 2^(h div 2) - 2"
   527 proof -
   528   obtain t' where t': "RB h t'" using RB_exist by auto
   529   show ?thesis using RB_size[OF t'] 
   530   RB_minimal[OF _ _ assms(1,2), simplified, OF t' RB_invh[OF t']] assms t' 
   531   unfolding  size1_def by auto
   532 qed
   533 
   534 corollary "rbt t \<Longrightarrow> h = height t \<Longrightarrow> size t \<ge> 2^((h+1) div 2) + 2^(h div 2) - 2"
   535 using bound unfolding rbt_def by blast
   536 
   537 end