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