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