src/HOL/Data_Structures/RBT_Set.thy
author nipkow
Wed Jun 13 15:24:20 2018 +0200 (10 months ago)
changeset 68440 6826718f732d
parent 68431 b294e095f64c
child 68998 818898556504
permissions -rw-r--r--
qualify interpretations to avoid clashes
nipkow@64951
     1
(* Author: Tobias Nipkow *)
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@68431
    13
definition empty :: "'a rbt" where
nipkow@68431
    14
"empty = Leaf"
nipkow@68431
    15
nipkow@63411
    16
fun ins :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
nipkow@61749
    17
"ins x Leaf = R Leaf x Leaf" |
nipkow@61749
    18
"ins x (B l a r) =
nipkow@61678
    19
  (case cmp x a of
nipkow@64960
    20
     LT \<Rightarrow> baliL (ins x l) a r |
nipkow@64960
    21
     GT \<Rightarrow> baliR l a (ins x r) |
nipkow@61678
    22
     EQ \<Rightarrow> B l a r)" |
nipkow@61749
    23
"ins x (R l a r) =
nipkow@61678
    24
  (case cmp x a of
nipkow@61749
    25
    LT \<Rightarrow> R (ins x l) a r |
nipkow@61749
    26
    GT \<Rightarrow> R l a (ins x r) |
nipkow@61678
    27
    EQ \<Rightarrow> R l a r)"
nipkow@61224
    28
nipkow@63411
    29
definition insert :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
nipkow@61749
    30
"insert x t = paint Black (ins x t)"
nipkow@61749
    31
nipkow@66087
    32
fun color :: "'a rbt \<Rightarrow> color" where
nipkow@66087
    33
"color Leaf = Black" |
nipkow@68413
    34
"color (Node _ _ c _) = c"
nipkow@66087
    35
nipkow@66087
    36
fun del :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
nipkow@61749
    37
"del x Leaf = Leaf" |
nipkow@68413
    38
"del x (Node l a _ r) =
nipkow@61678
    39
  (case cmp x a of
nipkow@66087
    40
     LT \<Rightarrow> if l \<noteq> Leaf \<and> color l = Black
nipkow@66087
    41
           then baldL (del x l) a r else R (del x l) a r |
nipkow@66087
    42
     GT \<Rightarrow> if r \<noteq> Leaf\<and> color r = Black
nipkow@66087
    43
           then baldR l a (del x r) else R l a (del x r) |
nipkow@66087
    44
     EQ \<Rightarrow> combine l r)"
nipkow@61749
    45
nipkow@63411
    46
definition delete :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
nipkow@61749
    47
"delete x t = paint Black (del x t)"
nipkow@61224
    48
nipkow@61224
    49
nipkow@61224
    50
subsection "Functional Correctness Proofs"
nipkow@61224
    51
nipkow@61749
    52
lemma inorder_paint: "inorder(paint c t) = inorder t"
nipkow@62526
    53
by(cases t) (auto)
nipkow@61749
    54
nipkow@64960
    55
lemma inorder_baliL:
nipkow@64960
    56
  "inorder(baliL l a r) = inorder l @ a # inorder r"
nipkow@64960
    57
by(cases "(l,a,r)" rule: baliL.cases) (auto)
nipkow@64960
    58
nipkow@64960
    59
lemma inorder_baliR:
nipkow@64960
    60
  "inorder(baliR l a r) = inorder l @ a # inorder r"
nipkow@64960
    61
by(cases "(l,a,r)" rule: baliR.cases) (auto)
nipkow@61224
    62
nipkow@61749
    63
lemma inorder_ins:
nipkow@61749
    64
  "sorted(inorder t) \<Longrightarrow> inorder(ins x t) = ins_list x (inorder t)"
nipkow@64960
    65
by(induction x t rule: ins.induct)
nipkow@64960
    66
  (auto simp: ins_list_simps inorder_baliL inorder_baliR)
nipkow@61749
    67
nipkow@61224
    68
lemma inorder_insert:
nipkow@61749
    69
  "sorted(inorder t) \<Longrightarrow> inorder(insert x t) = ins_list x (inorder t)"
nipkow@61749
    70
by (simp add: insert_def inorder_ins inorder_paint)
nipkow@61224
    71
nipkow@64960
    72
lemma inorder_baldL:
nipkow@64960
    73
  "inorder(baldL l a r) = inorder l @ a # inorder r"
nipkow@64960
    74
by(cases "(l,a,r)" rule: baldL.cases)
nipkow@64960
    75
  (auto simp:  inorder_baliL inorder_baliR inorder_paint)
nipkow@61224
    76
nipkow@64960
    77
lemma inorder_baldR:
nipkow@64960
    78
  "inorder(baldR l a r) = inorder l @ a # inorder r"
nipkow@64960
    79
by(cases "(l,a,r)" rule: baldR.cases)
nipkow@64960
    80
  (auto simp:  inorder_baliL inorder_baliR inorder_paint)
nipkow@61224
    81
nipkow@61224
    82
lemma inorder_combine:
nipkow@61224
    83
  "inorder(combine l r) = inorder l @ inorder r"
nipkow@61224
    84
by(induction l r rule: combine.induct)
nipkow@64960
    85
  (auto simp: inorder_baldL inorder_baldR split: tree.split color.split)
nipkow@61224
    86
nipkow@61749
    87
lemma inorder_del:
nipkow@61749
    88
 "sorted(inorder t) \<Longrightarrow>  inorder(del x t) = del_list x (inorder t)"
nipkow@66087
    89
by(induction x t rule: del.induct)
nipkow@64960
    90
  (auto simp: del_list_simps inorder_combine inorder_baldL inorder_baldR)
nipkow@61224
    91
nipkow@61749
    92
lemma inorder_delete:
nipkow@61749
    93
  "sorted(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
nipkow@61749
    94
by (auto simp: delete_def inorder_del inorder_paint)
nipkow@61749
    95
nipkow@61581
    96
nipkow@63411
    97
subsection \<open>Structural invariants\<close>
nipkow@61224
    98
nipkow@64952
    99
text\<open>The proofs are due to Markus Reiter and Alexander Krauss.\<close>
nipkow@61754
   100
nipkow@61754
   101
fun bheight :: "'a rbt \<Rightarrow> nat" where
nipkow@61754
   102
"bheight Leaf = 0" |
nipkow@68413
   103
"bheight (Node l x c r) = (if c = Black then bheight l + 1 else bheight l)"
nipkow@61754
   104
nipkow@63411
   105
fun invc :: "'a rbt \<Rightarrow> bool" where
nipkow@63411
   106
"invc Leaf = True" |
nipkow@68413
   107
"invc (Node l a c r) =
nipkow@64947
   108
  (invc l \<and> invc r \<and> (c = Red \<longrightarrow> color l = Black \<and> color r = Black))"
nipkow@61754
   109
nipkow@64953
   110
fun invc2 :: "'a rbt \<Rightarrow> bool" \<comment> \<open>Weaker version\<close> where
nipkow@64953
   111
"invc2 Leaf = True" |
nipkow@68413
   112
"invc2 (Node l a c r) = (invc l \<and> invc r)"
nipkow@61754
   113
nipkow@63411
   114
fun invh :: "'a rbt \<Rightarrow> bool" where
nipkow@63411
   115
"invh Leaf = True" |
nipkow@68413
   116
"invh (Node l x c r) = (invh l \<and> invh r \<and> bheight l = bheight r)"
nipkow@61754
   117
nipkow@64953
   118
lemma invc2I: "invc t \<Longrightarrow> invc2 t"
nipkow@61754
   119
by (cases t) simp+
nipkow@61754
   120
nipkow@61754
   121
definition rbt :: "'a rbt \<Rightarrow> bool" where
nipkow@63411
   122
"rbt t = (invc t \<and> invh t \<and> color t = Black)"
nipkow@61754
   123
nipkow@61754
   124
lemma color_paint_Black: "color (paint Black t) = Black"
nipkow@61754
   125
by (cases t) auto
nipkow@61754
   126
nipkow@64953
   127
lemma paint_invc2: "invc2 t \<Longrightarrow> invc2 (paint c t)"
nipkow@61754
   128
by (cases t) auto
nipkow@61754
   129
nipkow@64953
   130
lemma invc_paint_Black: "invc2 t \<Longrightarrow> invc (paint Black t)"
nipkow@61754
   131
by (cases t) auto
nipkow@61754
   132
nipkow@63411
   133
lemma invh_paint: "invh t \<Longrightarrow> invh (paint c t)"
nipkow@61754
   134
by (cases t) auto
nipkow@61754
   135
nipkow@64960
   136
lemma invc_baliL:
nipkow@64960
   137
  "\<lbrakk>invc2 l; invc r\<rbrakk> \<Longrightarrow> invc (baliL l a r)" 
nipkow@64960
   138
by (induct l a r rule: baliL.induct) auto
nipkow@64960
   139
nipkow@64960
   140
lemma invc_baliR:
nipkow@64960
   141
  "\<lbrakk>invc l; invc2 r\<rbrakk> \<Longrightarrow> invc (baliR l a r)" 
nipkow@64960
   142
by (induct l a r rule: baliR.induct) auto
nipkow@64960
   143
nipkow@64960
   144
lemma bheight_baliL:
nipkow@64960
   145
  "bheight l = bheight r \<Longrightarrow> bheight (baliL l a r) = Suc (bheight l)"
nipkow@64960
   146
by (induct l a r rule: baliL.induct) auto
nipkow@61754
   147
nipkow@64960
   148
lemma bheight_baliR:
nipkow@64960
   149
  "bheight l = bheight r \<Longrightarrow> bheight (baliR l a r) = Suc (bheight l)"
nipkow@64960
   150
by (induct l a r rule: baliR.induct) auto
nipkow@61754
   151
nipkow@64960
   152
lemma invh_baliL: 
nipkow@64960
   153
  "\<lbrakk> invh l; invh r; bheight l = bheight r \<rbrakk> \<Longrightarrow> invh (baliL l a r)"
nipkow@64960
   154
by (induct l a r rule: baliL.induct) auto
nipkow@64960
   155
nipkow@64960
   156
lemma invh_baliR: 
nipkow@64960
   157
  "\<lbrakk> invh l; invh r; bheight l = bheight r \<rbrakk> \<Longrightarrow> invh (baliR l a r)"
nipkow@64960
   158
by (induct l a r rule: baliR.induct) auto
nipkow@61754
   159
nipkow@61754
   160
nipkow@61754
   161
subsubsection \<open>Insertion\<close>
nipkow@61754
   162
nipkow@63411
   163
lemma invc_ins: assumes "invc t"
nipkow@64953
   164
  shows "color t = Black \<Longrightarrow> invc (ins x t)" "invc2 (ins x t)"
nipkow@61754
   165
using assms
nipkow@64960
   166
by (induct x t rule: ins.induct) (auto simp: invc_baliL invc_baliR invc2I)
nipkow@61754
   167
nipkow@63411
   168
lemma invh_ins: assumes "invh t"
nipkow@63411
   169
  shows "invh (ins x t)" "bheight (ins x t) = bheight t"
nipkow@61754
   170
using assms
nipkow@64960
   171
by(induct x t rule: ins.induct)
nipkow@64960
   172
  (auto simp: invh_baliL invh_baliR bheight_baliL bheight_baliR)
nipkow@61754
   173
nipkow@63411
   174
theorem rbt_insert: "rbt t \<Longrightarrow> rbt (insert x t)"
nipkow@66087
   175
by (simp add: invc_ins(2) invh_ins(1) color_paint_Black invc_paint_Black invh_paint
nipkow@61754
   176
  rbt_def insert_def)
nipkow@61754
   177
nipkow@63411
   178
nipkow@63411
   179
subsubsection \<open>Deletion\<close>
nipkow@63411
   180
nipkow@63411
   181
lemma bheight_paint_Red:
nipkow@63411
   182
  "color t = Black \<Longrightarrow> bheight (paint Red t) = bheight t - 1"
nipkow@61754
   183
by (cases t) auto
nipkow@61754
   184
nipkow@66087
   185
lemma invh_baldL_invc:
nipkow@66087
   186
  "\<lbrakk> invh l;  invh r;  bheight l + 1 = bheight r;  invc r \<rbrakk>
nipkow@66087
   187
   \<Longrightarrow> invh (baldL l a r) \<and> bheight (baldL l a r) = bheight l + 1"
nipkow@64960
   188
by (induct l a r rule: baldL.induct)
nipkow@64960
   189
   (auto simp: invh_baliR invh_paint bheight_baliR bheight_paint_Red)
nipkow@61754
   190
nipkow@66087
   191
lemma invh_baldL_Black: 
nipkow@66087
   192
  "\<lbrakk> invh l;  invh r;  bheight l + 1 = bheight r;  color r = Black \<rbrakk>
nipkow@66087
   193
   \<Longrightarrow> invh (baldL l a r) \<and> bheight (baldL l a r) = bheight r"
nipkow@64960
   194
by (induct l a r rule: baldL.induct) (auto simp add: invh_baliR bheight_baliR) 
nipkow@61754
   195
nipkow@66087
   196
lemma invc_baldL: "\<lbrakk>invc2 l; invc r; color r = Black\<rbrakk> \<Longrightarrow> invc (baldL l a r)"
nipkow@64960
   197
by (induct l a r rule: baldL.induct) (simp_all add: invc_baliR)
nipkow@61754
   198
nipkow@66087
   199
lemma invc2_baldL: "\<lbrakk> invc2 l; invc r \<rbrakk> \<Longrightarrow> invc2 (baldL l a r)"
nipkow@64960
   200
by (induct l a r rule: baldL.induct) (auto simp: invc_baliR paint_invc2 invc2I)
nipkow@61754
   201
nipkow@66087
   202
lemma invh_baldR_invc:
nipkow@66087
   203
  "\<lbrakk> invh l;  invh r;  bheight l = bheight r + 1;  invc l \<rbrakk>
nipkow@66087
   204
  \<Longrightarrow> invh (baldR l a r) \<and> bheight (baldR l a r) = bheight l"
nipkow@64960
   205
by(induct l a r rule: baldR.induct)
nipkow@64960
   206
  (auto simp: invh_baliL bheight_baliL invh_paint bheight_paint_Red)
nipkow@61754
   207
nipkow@64960
   208
lemma invc_baldR: "\<lbrakk>invc a; invc2 b; color a = Black\<rbrakk> \<Longrightarrow> invc (baldR a x b)"
nipkow@64960
   209
by (induct a x b rule: baldR.induct) (simp_all add: invc_baliL)
nipkow@61754
   210
nipkow@64960
   211
lemma invc2_baldR: "\<lbrakk> invc l; invc2 r \<rbrakk> \<Longrightarrow>invc2 (baldR l x r)"
nipkow@64960
   212
by (induct l x r rule: baldR.induct) (auto simp: invc_baliL paint_invc2 invc2I)
nipkow@61754
   213
nipkow@63411
   214
lemma invh_combine:
nipkow@66087
   215
  "\<lbrakk> invh l; invh r; bheight l = bheight r \<rbrakk>
nipkow@66087
   216
  \<Longrightarrow> invh (combine l r) \<and> bheight (combine l r) = bheight l"
nipkow@64960
   217
by (induct l r rule: combine.induct) 
nipkow@66087
   218
   (auto simp: invh_baldL_Black split: tree.splits color.splits)
nipkow@61754
   219
nipkow@63411
   220
lemma invc_combine: 
nipkow@64960
   221
  assumes "invc l" "invc r"
nipkow@64960
   222
  shows "color l = Black \<Longrightarrow> color r = Black \<Longrightarrow> invc (combine l r)"
nipkow@64960
   223
         "invc2 (combine l r)"
nipkow@61754
   224
using assms 
nipkow@64960
   225
by (induct l r rule: combine.induct)
nipkow@66087
   226
   (auto simp: invc_baldL invc2I split: tree.splits color.splits)
nipkow@61754
   227
nipkow@66087
   228
lemma neq_LeafD: "t \<noteq> Leaf \<Longrightarrow> \<exists>c l x r. t = Node c l x r"
nipkow@66087
   229
by(cases t) auto
nipkow@66087
   230
nipkow@66088
   231
lemma del_invc_invh: "invh t \<Longrightarrow> invc t \<Longrightarrow> invh (del x t) \<and>
nipkow@66088
   232
   (color t = Red \<and> bheight (del x t) = bheight t \<and> invc (del x t) \<or>
nipkow@66088
   233
    color t = Black \<and> bheight (del x t) = bheight t - 1 \<and> invc2 (del x t))"
nipkow@66088
   234
proof (induct x t rule: del.induct)
nipkow@68413
   235
case (2 x _ y c)
nipkow@66088
   236
  have "x = y \<or> x < y \<or> x > y" by auto
nipkow@61754
   237
  thus ?case proof (elim disjE)
nipkow@66088
   238
    assume "x = y"
nipkow@63411
   239
    with 2 show ?thesis
nipkow@63411
   240
    by (cases c) (simp_all add: invh_combine invc_combine)
nipkow@61754
   241
  next
nipkow@66088
   242
    assume "x < y"
nipkow@66087
   243
    with 2 show ?thesis
nipkow@66087
   244
      by(cases c)
nipkow@66087
   245
        (auto simp: invh_baldL_invc invc_baldL invc2_baldL dest: neq_LeafD)
nipkow@61754
   246
  next
nipkow@66088
   247
    assume "y < x"
nipkow@66087
   248
    with 2 show ?thesis
nipkow@66087
   249
      by(cases c)
nipkow@66087
   250
        (auto simp: invh_baldR_invc invc_baldR invc2_baldR dest: neq_LeafD)
nipkow@61754
   251
  qed
nipkow@61754
   252
qed auto
nipkow@61754
   253
nipkow@63411
   254
theorem rbt_delete: "rbt t \<Longrightarrow> rbt (delete k t)"
nipkow@64953
   255
by (metis delete_def rbt_def color_paint_Black del_invc_invh invc_paint_Black invc2I invh_paint)
nipkow@63411
   256
nipkow@63411
   257
text \<open>Overall correctness:\<close>
nipkow@63411
   258
nipkow@68440
   259
interpretation S: Set_by_Ordered
nipkow@68431
   260
where empty = empty and isin = isin and insert = insert and delete = delete
nipkow@63411
   261
and inorder = inorder and inv = rbt
nipkow@63411
   262
proof (standard, goal_cases)
nipkow@68431
   263
  case 1 show ?case by (simp add: empty_def)
nipkow@63411
   264
next
nipkow@67967
   265
  case 2 thus ?case by(simp add: isin_set_inorder)
nipkow@63411
   266
next
nipkow@63411
   267
  case 3 thus ?case by(simp add: inorder_insert)
nipkow@63411
   268
next
nipkow@63411
   269
  case 4 thus ?case by(simp add: inorder_delete)
nipkow@63411
   270
next
nipkow@68431
   271
  case 5 thus ?case by (simp add: rbt_def empty_def) 
nipkow@63411
   272
next
nipkow@63411
   273
  case 6 thus ?case by (simp add: rbt_insert) 
nipkow@63411
   274
next
nipkow@63411
   275
  case 7 thus ?case by (simp add: rbt_delete) 
nipkow@63411
   276
qed
nipkow@63411
   277
nipkow@63411
   278
nipkow@63411
   279
subsection \<open>Height-Size Relation\<close>
nipkow@63411
   280
nipkow@64950
   281
lemma neq_Black[simp]: "(c \<noteq> Black) = (c = Red)"
nipkow@64950
   282
by (cases c) auto
nipkow@64950
   283
nipkow@67963
   284
lemma rbt_height_bheight_if: "invc t \<Longrightarrow> invh t \<Longrightarrow>
nipkow@64950
   285
  height t \<le> (if color t = Black then 2 * bheight t else 2 * bheight t + 1)"
nipkow@64950
   286
by(induction t) (auto split: if_split_asm)
nipkow@64950
   287
nipkow@64950
   288
lemma rbt_height_bheight: "rbt t \<Longrightarrow> height t / 2 \<le> bheight t "
nipkow@64950
   289
by(auto simp: rbt_def dest: rbt_height_bheight_if)
nipkow@64950
   290
nipkow@67963
   291
lemma bheight_size_bound:  "invc t \<Longrightarrow> invh t \<Longrightarrow> 2 ^ (bheight t) \<le> size1 t"
nipkow@64950
   292
by (induction t) auto
nipkow@64950
   293
nipkow@64950
   294
lemma rbt_height_le: assumes "rbt t" shows "height t \<le> 2 * log 2 (size1 t)"
nipkow@64950
   295
proof -
nipkow@64950
   296
  have "2 powr (height t / 2) \<le> 2 powr bheight t"
nipkow@64950
   297
    using rbt_height_bheight[OF assms] by (simp)
nipkow@64950
   298
  also have "\<dots> \<le> size1 t" using assms
nipkow@64950
   299
    by (simp add: powr_realpow bheight_size_bound rbt_def)
nipkow@64950
   300
  finally have "2 powr (height t / 2) \<le> size1 t" .
nipkow@64950
   301
  hence "height t / 2 \<le> log 2 (size1 t)"
haftmann@67118
   302
    by (simp add: le_log_iff size1_def del: divide_le_eq_numeral1(1))
nipkow@64950
   303
  thus ?thesis by simp
nipkow@64950
   304
qed
nipkow@64950
   305
nipkow@61224
   306
end