src/HOL/Library/RBT.thy
author haftmann
Wed Mar 03 08:28:33 2010 +0100 (2010-03-03)
changeset 35534 14d8d72f8b1f
parent 32245 0c1cb95a434d
child 35550 e2bc7f8d8d51
permissions -rw-r--r--
more explicit naming scheme
krauss@26192
     1
(*  Title:      RBT.thy
krauss@26192
     2
    Author:     Markus Reiter, TU Muenchen
krauss@26192
     3
    Author:     Alexander Krauss, TU Muenchen
krauss@26192
     4
*)
krauss@26192
     5
krauss@26192
     6
header {* Red-Black Trees *}
krauss@26192
     7
krauss@26192
     8
(*<*)
krauss@26192
     9
theory RBT
haftmann@30738
    10
imports Main AssocList
krauss@26192
    11
begin
krauss@26192
    12
krauss@26192
    13
datatype color = R | B
haftmann@35534
    14
datatype ('a, 'b) rbt = Empty | Branch color "('a, 'b) rbt" 'a 'b "('a, 'b) rbt"
haftmann@35534
    15
haftmann@35534
    16
lemma rbt_cases:
haftmann@35534
    17
  obtains (Empty) "t = Empty" 
haftmann@35534
    18
  | (Red) l k v r where "t = Branch R l k v r" 
haftmann@35534
    19
  | (Black) l k v r where "t = Branch B l k v r"
haftmann@35534
    20
proof (cases t)
haftmann@35534
    21
  case Empty with that show thesis by blast
haftmann@35534
    22
next
haftmann@35534
    23
  case (Branch c) with that show thesis by (cases c) blast+
haftmann@35534
    24
qed
haftmann@35534
    25
haftmann@35534
    26
text {* Content of a tree *}
haftmann@35534
    27
haftmann@35534
    28
primrec entries
haftmann@35534
    29
where 
haftmann@35534
    30
  "entries Empty = []"
haftmann@35534
    31
| "entries (Branch _ l k v r) = entries l @ (k,v) # entries r"
krauss@26192
    32
krauss@32245
    33
text {* Search tree properties *}
krauss@26192
    34
haftmann@35534
    35
primrec entry_in_tree :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> bool"
krauss@26192
    36
where
haftmann@35534
    37
  "entry_in_tree k v Empty = False"
haftmann@35534
    38
| "entry_in_tree k v (Branch c l x y r) \<longleftrightarrow> k = x \<and> v = y \<or> entry_in_tree k v l \<or> entry_in_tree k v r"
krauss@26192
    39
haftmann@35534
    40
primrec keys :: "('k, 'v) rbt \<Rightarrow> 'k set"
krauss@26192
    41
where
krauss@26192
    42
  "keys Empty = {}"
haftmann@35534
    43
| "keys (Branch _ l k _ r) = { k } \<union> keys l \<union> keys r"
krauss@26192
    44
haftmann@35534
    45
lemma entry_in_tree_keys:
haftmann@35534
    46
  "entry_in_tree k v t \<Longrightarrow> k \<in> keys t"
haftmann@35534
    47
  by (induct t) auto
krauss@26192
    48
haftmann@35534
    49
definition tree_less :: "'a\<Colon>order \<Rightarrow> ('a, 'b) rbt \<Rightarrow> bool"
krauss@26192
    50
where
haftmann@35534
    51
  tree_less_prop: "tree_less k t \<longleftrightarrow> (\<forall>x\<in>keys t. x < k)"
haftmann@35534
    52
haftmann@35534
    53
abbreviation tree_less_symbol (infix "|\<guillemotleft>" 50)
haftmann@35534
    54
where "t |\<guillemotleft> x \<equiv> tree_less x t"
krauss@26192
    55
haftmann@35534
    56
definition tree_greater :: "'a\<Colon>order \<Rightarrow> ('a, 'b) rbt \<Rightarrow> bool" (infix "\<guillemotleft>|" 50) 
haftmann@35534
    57
where
haftmann@35534
    58
  tree_greater_prop: "tree_greater k t = (\<forall>x\<in>keys t. k < x)"
krauss@26192
    59
haftmann@35534
    60
lemma tree_less_simps [simp]:
haftmann@35534
    61
  "tree_less k Empty = True"
haftmann@35534
    62
  "tree_less k (Branch c lt kt v rt) \<longleftrightarrow> kt < k \<and> tree_less k lt \<and> tree_less k rt"
haftmann@35534
    63
  by (auto simp add: tree_less_prop)
krauss@26192
    64
haftmann@35534
    65
lemma tree_greater_simps [simp]:
haftmann@35534
    66
  "tree_greater k Empty = True"
haftmann@35534
    67
  "tree_greater k (Branch c lt kt v rt) \<longleftrightarrow> k < kt \<and> tree_greater k lt \<and> tree_greater k rt"
haftmann@35534
    68
  by (auto simp add: tree_greater_prop)
krauss@26192
    69
haftmann@35534
    70
lemmas tree_ord_props = tree_less_prop tree_greater_prop
krauss@26192
    71
haftmann@35534
    72
lemmas tree_greater_nit = tree_greater_prop entry_in_tree_keys
haftmann@35534
    73
lemmas tree_less_nit = tree_less_prop entry_in_tree_keys
krauss@26192
    74
haftmann@35534
    75
lemma tree_less_trans: "t |\<guillemotleft> x \<Longrightarrow> x < y \<Longrightarrow> t |\<guillemotleft> y"
haftmann@35534
    76
  and tree_greater_trans: "x < y \<Longrightarrow> y \<guillemotleft>| t \<Longrightarrow> x \<guillemotleft>| t"
haftmann@35534
    77
by (auto simp: tree_ord_props)
krauss@26192
    78
haftmann@35534
    79
primrec sorted :: "('a::linorder, 'b) rbt \<Rightarrow> bool"
krauss@26192
    80
where
haftmann@35534
    81
  "sorted Empty = True"
haftmann@35534
    82
| "sorted (Branch c l k v r) = (l |\<guillemotleft> k \<and> k \<guillemotleft>| r \<and> sorted l \<and> sorted r)"
krauss@26192
    83
haftmann@35534
    84
primrec lookup :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b"
haftmann@35534
    85
where
haftmann@35534
    86
  "lookup Empty k = None"
haftmann@35534
    87
| "lookup (Branch _ l x y r) k = (if k < x then lookup l k else if x < k then lookup r k else Some y)"
haftmann@35534
    88
haftmann@35534
    89
lemma lookup_tree_less[simp]: "t |\<guillemotleft> k \<Longrightarrow> lookup t k = None" 
krauss@26192
    90
by (induct t) auto
krauss@26192
    91
haftmann@35534
    92
lemma lookup_tree_greater[simp]: "k \<guillemotleft>| t \<Longrightarrow> lookup t k = None"
krauss@26192
    93
by (induct t) auto
krauss@26192
    94
haftmann@35534
    95
lemma lookup_keys: "sorted t \<Longrightarrow> dom (lookup t) = keys t"
haftmann@35534
    96
by (induct t) (auto simp: dom_def tree_greater_prop tree_less_prop)
krauss@26192
    97
haftmann@35534
    98
lemma lookup_pit: "sorted t \<Longrightarrow> (lookup t k = Some v) = entry_in_tree k v t"
haftmann@35534
    99
by (induct t) (auto simp: tree_less_prop tree_greater_prop entry_in_tree_keys)
krauss@26192
   100
haftmann@35534
   101
lemma lookup_Empty: "lookup Empty = empty"
krauss@26192
   102
by (rule ext) simp
krauss@26192
   103
krauss@26192
   104
(* a kind of extensionality *)
haftmann@35534
   105
lemma lookup_from_pit: 
haftmann@35534
   106
  assumes sorted: "sorted t1" "sorted t2" 
haftmann@35534
   107
  and eq: "\<And>v. entry_in_tree (k\<Colon>'a\<Colon>linorder) v t1 = entry_in_tree k v t2" 
haftmann@35534
   108
  shows "lookup t1 k = lookup t2 k"
haftmann@35534
   109
proof (cases "lookup t1 k")
krauss@26192
   110
  case None
haftmann@35534
   111
  then have "\<And>v. \<not> entry_in_tree k v t1"
haftmann@35534
   112
    by (simp add: lookup_pit[symmetric] sorted)
krauss@26192
   113
  with None show ?thesis
haftmann@35534
   114
    by (cases "lookup t2 k") (auto simp: lookup_pit sorted eq)
krauss@26192
   115
next
krauss@26192
   116
  case (Some a)
krauss@26192
   117
  then show ?thesis
haftmann@35534
   118
    apply (cases "lookup t2 k")
haftmann@35534
   119
    apply (auto simp: lookup_pit sorted eq)
haftmann@35534
   120
    by (auto simp add: lookup_pit[symmetric] sorted Some)
krauss@26192
   121
qed
krauss@26192
   122
krauss@26192
   123
subsection {* Red-black properties *}
krauss@26192
   124
haftmann@35534
   125
primrec color_of :: "('a, 'b) rbt \<Rightarrow> color"
krauss@26192
   126
where
haftmann@35534
   127
  "color_of Empty = B"
haftmann@35534
   128
| "color_of (Branch c _ _ _ _) = c"
krauss@26192
   129
haftmann@35534
   130
primrec bheight :: "('a,'b) rbt \<Rightarrow> nat"
haftmann@35534
   131
where
haftmann@35534
   132
  "bheight Empty = 0"
haftmann@35534
   133
| "bheight (Branch c lt k v rt) = (if c = B then Suc (bheight lt) else bheight lt)"
haftmann@35534
   134
haftmann@35534
   135
primrec inv1 :: "('a, 'b) rbt \<Rightarrow> bool"
krauss@26192
   136
where
krauss@26192
   137
  "inv1 Empty = True"
haftmann@35534
   138
| "inv1 (Branch c lt k v rt) \<longleftrightarrow> inv1 lt \<and> inv1 rt \<and> (c = B \<or> color_of lt = B \<and> color_of rt = B)"
krauss@26192
   139
haftmann@35534
   140
primrec inv1l :: "('a, 'b) rbt \<Rightarrow> bool" -- {* Weaker version *}
krauss@26192
   141
where
krauss@26192
   142
  "inv1l Empty = True"
haftmann@35534
   143
| "inv1l (Branch c l k v r) = (inv1 l \<and> inv1 r)"
krauss@26192
   144
lemma [simp]: "inv1 t \<Longrightarrow> inv1l t" by (cases t) simp+
krauss@26192
   145
haftmann@35534
   146
primrec inv2 :: "('a, 'b) rbt \<Rightarrow> bool"
krauss@26192
   147
where
krauss@26192
   148
  "inv2 Empty = True"
haftmann@35534
   149
| "inv2 (Branch c lt k v rt) = (inv2 lt \<and> inv2 rt \<and> bheight lt = bheight rt)"
krauss@26192
   150
haftmann@35534
   151
definition is_rbt :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> bool" where
haftmann@35534
   152
  "is_rbt t \<longleftrightarrow> inv1 t \<and> inv2 t \<and> color_of t = B \<and> sorted t"
krauss@26192
   153
haftmann@35534
   154
lemma is_rbt_sorted [simp]:
haftmann@35534
   155
  "is_rbt t \<Longrightarrow> sorted t" by (simp add: is_rbt_def)
krauss@26192
   156
haftmann@35534
   157
theorem Empty_is_rbt [simp]:
haftmann@35534
   158
  "is_rbt Empty" by (simp add: is_rbt_def)
krauss@26192
   159
krauss@26192
   160
krauss@26192
   161
subsection {* Insertion *}
krauss@26192
   162
krauss@26192
   163
fun (* slow, due to massive case splitting *)
krauss@26192
   164
  balance :: "('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
krauss@26192
   165
where
haftmann@35534
   166
  "balance (Branch R a w x b) s t (Branch R c y z d) = Branch R (Branch B a w x b) s t (Branch B c y z d)" |
haftmann@35534
   167
  "balance (Branch R (Branch R a w x b) s t c) y z d = Branch R (Branch B a w x b) s t (Branch B c y z d)" |
haftmann@35534
   168
  "balance (Branch R a w x (Branch R b s t c)) y z d = Branch R (Branch B a w x b) s t (Branch B c y z d)" |
haftmann@35534
   169
  "balance a w x (Branch R b s t (Branch R c y z d)) = Branch R (Branch B a w x b) s t (Branch B c y z d)" |
haftmann@35534
   170
  "balance a w x (Branch R (Branch R b s t c) y z d) = Branch R (Branch B a w x b) s t (Branch B c y z d)" |
haftmann@35534
   171
  "balance a s t b = Branch B a s t b"
krauss@26192
   172
krauss@26192
   173
lemma balance_inv1: "\<lbrakk>inv1l l; inv1l r\<rbrakk> \<Longrightarrow> inv1 (balance l k v r)" 
krauss@26192
   174
  by (induct l k v r rule: balance.induct) auto
krauss@26192
   175
haftmann@35534
   176
lemma balance_bheight: "bheight l = bheight r \<Longrightarrow> bheight (balance l k v r) = Suc (bheight l)"
krauss@26192
   177
  by (induct l k v r rule: balance.induct) auto
krauss@26192
   178
krauss@26192
   179
lemma balance_inv2: 
haftmann@35534
   180
  assumes "inv2 l" "inv2 r" "bheight l = bheight r"
krauss@26192
   181
  shows "inv2 (balance l k v r)"
krauss@26192
   182
  using assms
krauss@26192
   183
  by (induct l k v r rule: balance.induct) auto
krauss@26192
   184
haftmann@35534
   185
lemma balance_tree_greater[simp]: "(v \<guillemotleft>| balance a k x b) = (v \<guillemotleft>| a \<and> v \<guillemotleft>| b \<and> v < k)" 
krauss@26192
   186
  by (induct a k x b rule: balance.induct) auto
krauss@26192
   187
haftmann@35534
   188
lemma balance_tree_less[simp]: "(balance a k x b |\<guillemotleft> v) = (a |\<guillemotleft> v \<and> b |\<guillemotleft> v \<and> k < v)"
krauss@26192
   189
  by (induct a k x b rule: balance.induct) auto
krauss@26192
   190
haftmann@35534
   191
lemma balance_sorted: 
krauss@26192
   192
  fixes k :: "'a::linorder"
haftmann@35534
   193
  assumes "sorted l" "sorted r" "l |\<guillemotleft> k" "k \<guillemotleft>| r"
haftmann@35534
   194
  shows "sorted (balance l k v r)"
krauss@26192
   195
using assms proof (induct l k v r rule: balance.induct)
krauss@26192
   196
  case ("2_2" a x w b y t c z s va vb vd vc)
haftmann@35534
   197
  hence "y < z \<and> z \<guillemotleft>| Branch B va vb vd vc" 
haftmann@35534
   198
    by (auto simp add: tree_ord_props)
haftmann@35534
   199
  hence "tree_greater y (Branch B va vb vd vc)" by (blast dest: tree_greater_trans)
krauss@26192
   200
  with "2_2" show ?case by simp
krauss@26192
   201
next
krauss@26192
   202
  case ("3_2" va vb vd vc x w b y s c z)
haftmann@35534
   203
  from "3_2" have "x < y \<and> tree_less x (Branch B va vb vd vc)" 
haftmann@35534
   204
    by simp
haftmann@35534
   205
  hence "tree_less y (Branch B va vb vd vc)" by (blast dest: tree_less_trans)
krauss@26192
   206
  with "3_2" show ?case by simp
krauss@26192
   207
next
krauss@26192
   208
  case ("3_3" x w b y s c z t va vb vd vc)
haftmann@35534
   209
  from "3_3" have "y < z \<and> tree_greater z (Branch B va vb vd vc)" by simp
haftmann@35534
   210
  hence "tree_greater y (Branch B va vb vd vc)" by (blast dest: tree_greater_trans)
krauss@26192
   211
  with "3_3" show ?case by simp
krauss@26192
   212
next
krauss@26192
   213
  case ("3_4" vd ve vg vf x w b y s c z t va vb vii vc)
haftmann@35534
   214
  hence "x < y \<and> tree_less x (Branch B vd ve vg vf)" by simp
haftmann@35534
   215
  hence 1: "tree_less y (Branch B vd ve vg vf)" by (blast dest: tree_less_trans)
haftmann@35534
   216
  from "3_4" have "y < z \<and> tree_greater z (Branch B va vb vii vc)" by simp
haftmann@35534
   217
  hence "tree_greater y (Branch B va vb vii vc)" by (blast dest: tree_greater_trans)
krauss@26192
   218
  with 1 "3_4" show ?case by simp
krauss@26192
   219
next
krauss@26192
   220
  case ("4_2" va vb vd vc x w b y s c z t dd)
haftmann@35534
   221
  hence "x < y \<and> tree_less x (Branch B va vb vd vc)" by simp
haftmann@35534
   222
  hence "tree_less y (Branch B va vb vd vc)" by (blast dest: tree_less_trans)
krauss@26192
   223
  with "4_2" show ?case by simp
krauss@26192
   224
next
krauss@26192
   225
  case ("5_2" x w b y s c z t va vb vd vc)
haftmann@35534
   226
  hence "y < z \<and> tree_greater z (Branch B va vb vd vc)" by simp
haftmann@35534
   227
  hence "tree_greater y (Branch B va vb vd vc)" by (blast dest: tree_greater_trans)
krauss@26192
   228
  with "5_2" show ?case by simp
krauss@26192
   229
next
krauss@26192
   230
  case ("5_3" va vb vd vc x w b y s c z t)
haftmann@35534
   231
  hence "x < y \<and> tree_less x (Branch B va vb vd vc)" by simp
haftmann@35534
   232
  hence "tree_less y (Branch B va vb vd vc)" by (blast dest: tree_less_trans)
krauss@26192
   233
  with "5_3" show ?case by simp
krauss@26192
   234
next
krauss@26192
   235
  case ("5_4" va vb vg vc x w b y s c z t vd ve vii vf)
haftmann@35534
   236
  hence "x < y \<and> tree_less x (Branch B va vb vg vc)" by simp
haftmann@35534
   237
  hence 1: "tree_less y (Branch B va vb vg vc)" by (blast dest: tree_less_trans)
haftmann@35534
   238
  from "5_4" have "y < z \<and> tree_greater z (Branch B vd ve vii vf)" by simp
haftmann@35534
   239
  hence "tree_greater y (Branch B vd ve vii vf)" by (blast dest: tree_greater_trans)
krauss@26192
   240
  with 1 "5_4" show ?case by simp
krauss@26192
   241
qed simp+
krauss@26192
   242
krauss@26192
   243
lemma keys_balance[simp]: 
krauss@26192
   244
  "keys (balance l k v r) = { k } \<union> keys l \<union> keys r"
krauss@26192
   245
by (induct l k v r rule: balance.induct) auto
krauss@26192
   246
krauss@26192
   247
lemma balance_pit:  
haftmann@35534
   248
  "entry_in_tree k x (balance l v y r) = (entry_in_tree k x l \<or> k = v \<and> x = y \<or> entry_in_tree k x r)" 
krauss@26192
   249
by (induct l v y r rule: balance.induct) auto
krauss@26192
   250
haftmann@35534
   251
lemma lookup_balance[simp]: 
krauss@26192
   252
fixes k :: "'a::linorder"
haftmann@35534
   253
assumes "sorted l" "sorted r" "l |\<guillemotleft> k" "k \<guillemotleft>| r"
haftmann@35534
   254
shows "lookup (balance l k v r) x = lookup (Branch B l k v r) x"
haftmann@35534
   255
by (rule lookup_from_pit) (auto simp:assms balance_pit balance_sorted)
krauss@26192
   256
krauss@26192
   257
primrec paint :: "color \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
krauss@26192
   258
where
krauss@26192
   259
  "paint c Empty = Empty"
haftmann@35534
   260
| "paint c (Branch _ l k v r) = Branch c l k v r"
krauss@26192
   261
krauss@26192
   262
lemma paint_inv1l[simp]: "inv1l t \<Longrightarrow> inv1l (paint c t)" by (cases t) auto
krauss@26192
   263
lemma paint_inv1[simp]: "inv1l t \<Longrightarrow> inv1 (paint B t)" by (cases t) auto
krauss@26192
   264
lemma paint_inv2[simp]: "inv2 t \<Longrightarrow> inv2 (paint c t)" by (cases t) auto
haftmann@35534
   265
lemma paint_color_of[simp]: "color_of (paint B t) = B" by (cases t) auto
haftmann@35534
   266
lemma paint_sorted[simp]: "sorted t \<Longrightarrow> sorted (paint c t)" by (cases t) auto
haftmann@35534
   267
lemma paint_pit[simp]: "entry_in_tree k x (paint c t) = entry_in_tree k x t" by (cases t) auto
haftmann@35534
   268
lemma paint_lookup[simp]: "lookup (paint c t) = lookup t" by (rule ext) (cases t, auto)
haftmann@35534
   269
lemma paint_tree_greater[simp]: "(v \<guillemotleft>| paint c t) = (v \<guillemotleft>| t)" by (cases t) auto
haftmann@35534
   270
lemma paint_tree_less[simp]: "(paint c t |\<guillemotleft> v) = (t |\<guillemotleft> v)" by (cases t) auto
krauss@26192
   271
krauss@26192
   272
fun
krauss@26192
   273
  ins :: "('a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
krauss@26192
   274
where
haftmann@35534
   275
  "ins f k v Empty = Branch R Empty k v Empty" |
haftmann@35534
   276
  "ins f k v (Branch B l x y r) = (if k < x then balance (ins f k v l) x y r
krauss@26192
   277
                               else if k > x then balance l x y (ins f k v r)
haftmann@35534
   278
                               else Branch B l x (f k y v) r)" |
haftmann@35534
   279
  "ins f k v (Branch R l x y r) = (if k < x then Branch R (ins f k v l) x y r
haftmann@35534
   280
                               else if k > x then Branch R l x y (ins f k v r)
haftmann@35534
   281
                               else Branch R l x (f k y v) r)"
krauss@26192
   282
krauss@26192
   283
lemma ins_inv1_inv2: 
krauss@26192
   284
  assumes "inv1 t" "inv2 t"
haftmann@35534
   285
  shows "inv2 (ins f k x t)" "bheight (ins f k x t) = bheight t" 
haftmann@35534
   286
  "color_of t = B \<Longrightarrow> inv1 (ins f k x t)" "inv1l (ins f k x t)"
krauss@26192
   287
  using assms
haftmann@35534
   288
  by (induct f k x t rule: ins.induct) (auto simp: balance_inv1 balance_inv2 balance_bheight)
krauss@26192
   289
haftmann@35534
   290
lemma ins_tree_greater[simp]: "(v \<guillemotleft>| ins f k x t) = (v \<guillemotleft>| t \<and> k > v)"
krauss@26192
   291
  by (induct f k x t rule: ins.induct) auto
haftmann@35534
   292
lemma ins_tree_less[simp]: "(ins f k x t |\<guillemotleft> v) = (t |\<guillemotleft> v \<and> k < v)"
krauss@26192
   293
  by (induct f k x t rule: ins.induct) auto
haftmann@35534
   294
lemma ins_sorted[simp]: "sorted t \<Longrightarrow> sorted (ins f k x t)"
haftmann@35534
   295
  by (induct f k x t rule: ins.induct) (auto simp: balance_sorted)
krauss@26192
   296
krauss@26192
   297
lemma keys_ins: "keys (ins f k v t) = { k } \<union> keys t"
krauss@26192
   298
by (induct f k v t rule: ins.induct) auto
krauss@26192
   299
haftmann@35534
   300
lemma lookup_ins: 
krauss@26192
   301
  fixes k :: "'a::linorder"
haftmann@35534
   302
  assumes "sorted t"
haftmann@35534
   303
  shows "lookup (ins f k v t) x = ((lookup t)(k |-> case lookup t k of None \<Rightarrow> v 
krauss@26192
   304
                                                       | Some w \<Rightarrow> f k w v)) x"
krauss@26192
   305
using assms by (induct f k v t rule: ins.induct) auto
krauss@26192
   306
krauss@26192
   307
definition
krauss@26192
   308
  insertwithkey :: "('a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
krauss@26192
   309
where
krauss@26192
   310
  "insertwithkey f k v t = paint B (ins f k v t)"
krauss@26192
   311
haftmann@35534
   312
lemma insertwk_sorted: "sorted t \<Longrightarrow> sorted (insertwithkey f k x t)"
krauss@26192
   313
  by (auto simp: insertwithkey_def)
krauss@26192
   314
haftmann@35534
   315
theorem insertwk_is_rbt: 
haftmann@35534
   316
  assumes inv: "is_rbt t" 
haftmann@35534
   317
  shows "is_rbt (insertwithkey f k x t)"
krauss@26192
   318
using assms
haftmann@35534
   319
unfolding insertwithkey_def is_rbt_def
krauss@26192
   320
by (auto simp: ins_inv1_inv2)
krauss@26192
   321
haftmann@35534
   322
lemma lookup_insertwk: 
haftmann@35534
   323
  assumes "sorted t"
haftmann@35534
   324
  shows "lookup (insertwithkey f k v t) x = ((lookup t)(k |-> case lookup t k of None \<Rightarrow> v 
krauss@26192
   325
                                                       | Some w \<Rightarrow> f k w v)) x"
krauss@26192
   326
unfolding insertwithkey_def using assms
haftmann@35534
   327
by (simp add:lookup_ins)
krauss@26192
   328
krauss@26192
   329
definition
krauss@26192
   330
  insertw_def: "insertwith f = insertwithkey (\<lambda>_. f)"
krauss@26192
   331
haftmann@35534
   332
lemma insertw_sorted: "sorted t \<Longrightarrow> sorted (insertwith f k v t)" by (simp add: insertwk_sorted insertw_def)
haftmann@35534
   333
theorem insertw_is_rbt: "is_rbt t \<Longrightarrow> is_rbt (insertwith f k v t)" by (simp add: insertwk_is_rbt insertw_def)
krauss@26192
   334
haftmann@35534
   335
lemma lookup_insertw:
haftmann@35534
   336
  assumes "is_rbt t"
haftmann@35534
   337
  shows "lookup (insertwith f k v t) = (lookup t)(k \<mapsto> (if k:dom (lookup t) then f (the (lookup t k)) v else v))"
krauss@26192
   338
using assms
krauss@26192
   339
unfolding insertw_def
haftmann@35534
   340
by (rule_tac ext) (cases "lookup t k", auto simp:lookup_insertwk dom_def)
krauss@26192
   341
haftmann@35534
   342
definition insert :: "'a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" where
haftmann@35534
   343
  "insert k v t = insertwithkey (\<lambda>_ _ nv. nv) k v t"
krauss@26192
   344
haftmann@35534
   345
lemma insert_sorted: "sorted t \<Longrightarrow> sorted (insert k v t)" by (simp add: insertwk_sorted insert_def)
haftmann@35534
   346
theorem insert_is_rbt: "is_rbt t \<Longrightarrow> is_rbt (insert k v t)" by (simp add: insertwk_is_rbt insert_def)
krauss@26192
   347
haftmann@35534
   348
lemma lookup_insert: 
haftmann@35534
   349
  assumes "is_rbt t"
haftmann@35534
   350
  shows "lookup (insert k v t) = (lookup t)(k\<mapsto>v)"
haftmann@35534
   351
unfolding insert_def
krauss@26192
   352
using assms
haftmann@35534
   353
by (rule_tac ext) (simp add: lookup_insertwk split:option.split)
krauss@26192
   354
krauss@26192
   355
krauss@26192
   356
subsection {* Deletion *}
krauss@26192
   357
haftmann@35534
   358
lemma bheight_paintR'[simp]: "color_of t = B \<Longrightarrow> bheight (paint R t) = bheight t - 1"
krauss@26192
   359
by (cases t rule: rbt_cases) auto
krauss@26192
   360
krauss@26192
   361
fun
krauss@26192
   362
  balleft :: "('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
krauss@26192
   363
where
haftmann@35534
   364
  "balleft (Branch R a k x b) s y c = Branch R (Branch B a k x b) s y c" |
haftmann@35534
   365
  "balleft bl k x (Branch B a s y b) = balance bl k x (Branch R a s y b)" |
haftmann@35534
   366
  "balleft bl k x (Branch R (Branch B a s y b) t z c) = Branch R (Branch B bl k x a) s y (balance b t z (paint R c))" |
krauss@26192
   367
  "balleft t k x s = Empty"
krauss@26192
   368
krauss@26192
   369
lemma balleft_inv2_with_inv1:
haftmann@35534
   370
  assumes "inv2 lt" "inv2 rt" "bheight lt + 1 = bheight rt" "inv1 rt"
haftmann@35534
   371
  shows "bheight (balleft lt k v rt) = bheight lt + 1"
krauss@26192
   372
  and   "inv2 (balleft lt k v rt)"
krauss@26192
   373
using assms 
haftmann@35534
   374
by (induct lt k v rt rule: balleft.induct) (auto simp: balance_inv2 balance_bheight)
krauss@26192
   375
krauss@26192
   376
lemma balleft_inv2_app: 
haftmann@35534
   377
  assumes "inv2 lt" "inv2 rt" "bheight lt + 1 = bheight rt" "color_of rt = B"
krauss@26192
   378
  shows "inv2 (balleft lt k v rt)" 
haftmann@35534
   379
        "bheight (balleft lt k v rt) = bheight rt"
krauss@26192
   380
using assms 
haftmann@35534
   381
by (induct lt k v rt rule: balleft.induct) (auto simp add: balance_inv2 balance_bheight)+ 
krauss@26192
   382
haftmann@35534
   383
lemma balleft_inv1: "\<lbrakk>inv1l a; inv1 b; color_of b = B\<rbrakk> \<Longrightarrow> inv1 (balleft a k x b)"
krauss@26192
   384
  by (induct a k x b rule: balleft.induct) (simp add: balance_inv1)+
krauss@26192
   385
krauss@26192
   386
lemma balleft_inv1l: "\<lbrakk> inv1l lt; inv1 rt \<rbrakk> \<Longrightarrow> inv1l (balleft lt k x rt)"
krauss@26192
   387
by (induct lt k x rt rule: balleft.induct) (auto simp: balance_inv1)
krauss@26192
   388
haftmann@35534
   389
lemma balleft_sorted: "\<lbrakk> sorted l; sorted r; tree_less k l; tree_greater k r \<rbrakk> \<Longrightarrow> sorted (balleft l k v r)"
krauss@26192
   390
apply (induct l k v r rule: balleft.induct)
haftmann@35534
   391
apply (auto simp: balance_sorted)
haftmann@35534
   392
apply (unfold tree_greater_prop tree_less_prop)
krauss@26192
   393
by force+
krauss@26192
   394
haftmann@35534
   395
lemma balleft_tree_greater: 
krauss@26192
   396
  fixes k :: "'a::order"
krauss@26192
   397
  assumes "k \<guillemotleft>| a" "k \<guillemotleft>| b" "k < x" 
krauss@26192
   398
  shows "k \<guillemotleft>| balleft a x t b"
krauss@26192
   399
using assms 
krauss@26192
   400
by (induct a x t b rule: balleft.induct) auto
krauss@26192
   401
haftmann@35534
   402
lemma balleft_tree_less: 
krauss@26192
   403
  fixes k :: "'a::order"
krauss@26192
   404
  assumes "a |\<guillemotleft> k" "b |\<guillemotleft> k" "x < k" 
krauss@26192
   405
  shows "balleft a x t b |\<guillemotleft> k"
krauss@26192
   406
using assms
krauss@26192
   407
by (induct a x t b rule: balleft.induct) auto
krauss@26192
   408
krauss@26192
   409
lemma balleft_pit: 
haftmann@35534
   410
  assumes "inv1l l" "inv1 r" "bheight l + 1 = bheight r"
haftmann@35534
   411
  shows "entry_in_tree k v (balleft l a b r) = (entry_in_tree k v l \<or> k = a \<and> v = b \<or> entry_in_tree k v r)"
krauss@26192
   412
using assms 
krauss@26192
   413
by (induct l k v r rule: balleft.induct) (auto simp: balance_pit)
krauss@26192
   414
krauss@26192
   415
fun
krauss@26192
   416
  balright :: "('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
krauss@26192
   417
where
haftmann@35534
   418
  "balright a k x (Branch R b s y c) = Branch R a k x (Branch B b s y c)" |
haftmann@35534
   419
  "balright (Branch B a k x b) s y bl = balance (Branch R a k x b) s y bl" |
haftmann@35534
   420
  "balright (Branch R a k x (Branch B b s y c)) t z bl = Branch R (balance (paint R a) k x b) s y (Branch B c t z bl)" |
krauss@26192
   421
  "balright t k x s = Empty"
krauss@26192
   422
krauss@26192
   423
lemma balright_inv2_with_inv1:
haftmann@35534
   424
  assumes "inv2 lt" "inv2 rt" "bheight lt = bheight rt + 1" "inv1 lt"
haftmann@35534
   425
  shows "inv2 (balright lt k v rt) \<and> bheight (balright lt k v rt) = bheight lt"
krauss@26192
   426
using assms
haftmann@35534
   427
by (induct lt k v rt rule: balright.induct) (auto simp: balance_inv2 balance_bheight)
krauss@26192
   428
haftmann@35534
   429
lemma balright_inv1: "\<lbrakk>inv1 a; inv1l b; color_of a = B\<rbrakk> \<Longrightarrow> inv1 (balright a k x b)"
krauss@26192
   430
by (induct a k x b rule: balright.induct) (simp add: balance_inv1)+
krauss@26192
   431
krauss@26192
   432
lemma balright_inv1l: "\<lbrakk> inv1 lt; inv1l rt \<rbrakk> \<Longrightarrow>inv1l (balright lt k x rt)"
krauss@26192
   433
by (induct lt k x rt rule: balright.induct) (auto simp: balance_inv1)
krauss@26192
   434
haftmann@35534
   435
lemma balright_sorted: "\<lbrakk> sorted l; sorted r; tree_less k l; tree_greater k r \<rbrakk> \<Longrightarrow> sorted (balright l k v r)"
krauss@26192
   436
apply (induct l k v r rule: balright.induct)
haftmann@35534
   437
apply (auto simp:balance_sorted)
haftmann@35534
   438
apply (unfold tree_less_prop tree_greater_prop)
krauss@26192
   439
by force+
krauss@26192
   440
haftmann@35534
   441
lemma balright_tree_greater: 
krauss@26192
   442
  fixes k :: "'a::order"
krauss@26192
   443
  assumes "k \<guillemotleft>| a" "k \<guillemotleft>| b" "k < x" 
krauss@26192
   444
  shows "k \<guillemotleft>| balright a x t b"
krauss@26192
   445
using assms by (induct a x t b rule: balright.induct) auto
krauss@26192
   446
haftmann@35534
   447
lemma balright_tree_less: 
krauss@26192
   448
  fixes k :: "'a::order"
krauss@26192
   449
  assumes "a |\<guillemotleft> k" "b |\<guillemotleft> k" "x < k" 
krauss@26192
   450
  shows "balright a x t b |\<guillemotleft> k"
krauss@26192
   451
using assms by (induct a x t b rule: balright.induct) auto
krauss@26192
   452
krauss@26192
   453
lemma balright_pit:
haftmann@35534
   454
  assumes "inv1 l" "inv1l r" "bheight l = bheight r + 1" "inv2 l" "inv2 r"
haftmann@35534
   455
  shows "entry_in_tree x y (balright l k v r) = (entry_in_tree x y l \<or> x = k \<and> y = v \<or> entry_in_tree x y r)"
krauss@26192
   456
using assms by (induct l k v r rule: balright.induct) (auto simp: balance_pit)
krauss@26192
   457
krauss@26192
   458
krauss@26192
   459
text {* app *}
krauss@26192
   460
krauss@26192
   461
fun
krauss@26192
   462
  app :: "('a,'b) rbt \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
krauss@26192
   463
where
krauss@26192
   464
  "app Empty x = x" 
krauss@26192
   465
| "app x Empty = x" 
haftmann@35534
   466
| "app (Branch R a k x b) (Branch R c s y d) = (case (app b c) of
haftmann@35534
   467
                                      Branch R b2 t z c2 \<Rightarrow> (Branch R (Branch R a k x b2) t z (Branch R c2 s y d)) |
haftmann@35534
   468
                                      bc \<Rightarrow> Branch R a k x (Branch R bc s y d))" 
haftmann@35534
   469
| "app (Branch B a k x b) (Branch B c s y d) = (case (app b c) of
haftmann@35534
   470
                                      Branch R b2 t z c2 \<Rightarrow> Branch R (Branch B a k x b2) t z (Branch B c2 s y d) |
haftmann@35534
   471
                                      bc \<Rightarrow> balleft a k x (Branch B bc s y d))" 
haftmann@35534
   472
| "app a (Branch R b k x c) = Branch R (app a b) k x c" 
haftmann@35534
   473
| "app (Branch R a k x b) c = Branch R a k x (app b c)" 
krauss@26192
   474
krauss@26192
   475
lemma app_inv2:
haftmann@35534
   476
  assumes "inv2 lt" "inv2 rt" "bheight lt = bheight rt"
haftmann@35534
   477
  shows "bheight (app lt rt) = bheight lt" "inv2 (app lt rt)"
krauss@26192
   478
using assms 
krauss@26192
   479
by (induct lt rt rule: app.induct) 
krauss@26192
   480
   (auto simp: balleft_inv2_app split: rbt.splits color.splits)
krauss@26192
   481
krauss@26192
   482
lemma app_inv1: 
krauss@26192
   483
  assumes "inv1 lt" "inv1 rt"
haftmann@35534
   484
  shows "color_of lt = B \<Longrightarrow> color_of rt = B \<Longrightarrow> inv1 (app lt rt)"
krauss@26192
   485
         "inv1l (app lt rt)"
krauss@26192
   486
using assms 
krauss@26192
   487
by (induct lt rt rule: app.induct)
krauss@26192
   488
   (auto simp: balleft_inv1 split: rbt.splits color.splits)
krauss@26192
   489
haftmann@35534
   490
lemma app_tree_greater[simp]: 
krauss@26192
   491
  fixes k :: "'a::linorder"
krauss@26192
   492
  assumes "k \<guillemotleft>| l" "k \<guillemotleft>| r" 
krauss@26192
   493
  shows "k \<guillemotleft>| app l r"
krauss@26192
   494
using assms 
krauss@26192
   495
by (induct l r rule: app.induct)
haftmann@35534
   496
   (auto simp: balleft_tree_greater split:rbt.splits color.splits)
krauss@26192
   497
haftmann@35534
   498
lemma app_tree_less[simp]: 
krauss@26192
   499
  fixes k :: "'a::linorder"
krauss@26192
   500
  assumes "l |\<guillemotleft> k" "r |\<guillemotleft> k" 
krauss@26192
   501
  shows "app l r |\<guillemotleft> k"
krauss@26192
   502
using assms 
krauss@26192
   503
by (induct l r rule: app.induct)
haftmann@35534
   504
   (auto simp: balleft_tree_less split:rbt.splits color.splits)
krauss@26192
   505
haftmann@35534
   506
lemma app_sorted: 
krauss@26192
   507
  fixes k :: "'a::linorder"
haftmann@35534
   508
  assumes "sorted l" "sorted r" "l |\<guillemotleft> k" "k \<guillemotleft>| r"
haftmann@35534
   509
  shows "sorted (app l r)"
krauss@26192
   510
using assms proof (induct l r rule: app.induct)
krauss@26192
   511
  case (3 a x v b c y w d)
krauss@26192
   512
  hence ineqs: "a |\<guillemotleft> x" "x \<guillemotleft>| b" "b |\<guillemotleft> k" "k \<guillemotleft>| c" "c |\<guillemotleft> y" "y \<guillemotleft>| d"
krauss@26192
   513
    by auto
krauss@26192
   514
  with 3
krauss@26192
   515
  show ?case
krauss@26192
   516
    apply (cases "app b c" rule: rbt_cases)
krauss@26192
   517
    apply auto
haftmann@35534
   518
    by (metis app_tree_greater app_tree_less ineqs ineqs tree_less_simps(2) tree_greater_simps(2) tree_greater_trans tree_less_trans)+
krauss@26192
   519
next
krauss@26192
   520
  case (4 a x v b c y w d)
haftmann@35534
   521
  hence "x < k \<and> tree_greater k c" by simp
haftmann@35534
   522
  hence "tree_greater x c" by (blast dest: tree_greater_trans)
haftmann@35534
   523
  with 4 have 2: "tree_greater x (app b c)" by (simp add: app_tree_greater)
haftmann@35534
   524
  from 4 have "k < y \<and> tree_less k b" by simp
haftmann@35534
   525
  hence "tree_less y b" by (blast dest: tree_less_trans)
haftmann@35534
   526
  with 4 have 3: "tree_less y (app b c)" by (simp add: app_tree_less)
krauss@26192
   527
  show ?case
krauss@26192
   528
  proof (cases "app b c" rule: rbt_cases)
krauss@26192
   529
    case Empty
haftmann@35534
   530
    from 4 have "x < y \<and> tree_greater y d" by auto
haftmann@35534
   531
    hence "tree_greater x d" by (blast dest: tree_greater_trans)
haftmann@35534
   532
    with 4 Empty have "sorted a" and "sorted (Branch B Empty y w d)" and "tree_less x a" and "tree_greater x (Branch B Empty y w d)" by auto
haftmann@35534
   533
    with Empty show ?thesis by (simp add: balleft_sorted)
krauss@26192
   534
  next
krauss@26192
   535
    case (Red lta va ka rta)
haftmann@35534
   536
    with 2 4 have "x < va \<and> tree_less x a" by simp
haftmann@35534
   537
    hence 5: "tree_less va a" by (blast dest: tree_less_trans)
haftmann@35534
   538
    from Red 3 4 have "va < y \<and> tree_greater y d" by simp
haftmann@35534
   539
    hence "tree_greater va d" by (blast dest: tree_greater_trans)
krauss@26192
   540
    with Red 2 3 4 5 show ?thesis by simp
krauss@26192
   541
  next
krauss@26192
   542
    case (Black lta va ka rta)
haftmann@35534
   543
    from 4 have "x < y \<and> tree_greater y d" by auto
haftmann@35534
   544
    hence "tree_greater x d" by (blast dest: tree_greater_trans)
haftmann@35534
   545
    with Black 2 3 4 have "sorted a" and "sorted (Branch B (app b c) y w d)" and "tree_less x a" and "tree_greater x (Branch B (app b c) y w d)" by auto
haftmann@35534
   546
    with Black show ?thesis by (simp add: balleft_sorted)
krauss@26192
   547
  qed
krauss@26192
   548
next
krauss@26192
   549
  case (5 va vb vd vc b x w c)
haftmann@35534
   550
  hence "k < x \<and> tree_less k (Branch B va vb vd vc)" by simp
haftmann@35534
   551
  hence "tree_less x (Branch B va vb vd vc)" by (blast dest: tree_less_trans)
haftmann@35534
   552
  with 5 show ?case by (simp add: app_tree_less)
krauss@26192
   553
next
krauss@26192
   554
  case (6 a x v b va vb vd vc)
haftmann@35534
   555
  hence "x < k \<and> tree_greater k (Branch B va vb vd vc)" by simp
haftmann@35534
   556
  hence "tree_greater x (Branch B va vb vd vc)" by (blast dest: tree_greater_trans)
haftmann@35534
   557
  with 6 show ?case by (simp add: app_tree_greater)
krauss@26192
   558
qed simp+
krauss@26192
   559
krauss@26192
   560
lemma app_pit: 
haftmann@35534
   561
  assumes "inv2 l" "inv2 r" "bheight l = bheight r" "inv1 l" "inv1 r"
haftmann@35534
   562
  shows "entry_in_tree k v (app l r) = (entry_in_tree k v l \<or> entry_in_tree k v r)"
krauss@26192
   563
using assms 
krauss@26192
   564
proof (induct l r rule: app.induct)
krauss@26192
   565
  case (4 _ _ _ b c)
haftmann@35534
   566
  hence a: "bheight (app b c) = bheight b" by (simp add: app_inv2)
krauss@26192
   567
  from 4 have b: "inv1l (app b c)" by (simp add: app_inv1)
krauss@26192
   568
krauss@26192
   569
  show ?case
krauss@26192
   570
  proof (cases "app b c" rule: rbt_cases)
krauss@26192
   571
    case Empty
krauss@26192
   572
    with 4 a show ?thesis by (auto simp: balleft_pit)
krauss@26192
   573
  next
krauss@26192
   574
    case (Red lta ka va rta)
krauss@26192
   575
    with 4 show ?thesis by auto
krauss@26192
   576
  next
krauss@26192
   577
    case (Black lta ka va rta)
krauss@26192
   578
    with a b 4  show ?thesis by (auto simp: balleft_pit)
krauss@26192
   579
  qed 
krauss@26192
   580
qed (auto split: rbt.splits color.splits)
krauss@26192
   581
krauss@26192
   582
fun
krauss@26192
   583
  delformLeft :: "('a\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" and
krauss@26192
   584
  delformRight :: "('a\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" and
krauss@26192
   585
  del :: "('a\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
krauss@26192
   586
where
krauss@26192
   587
  "del x Empty = Empty" |
haftmann@35534
   588
  "del x (Branch c a y s b) = (if x < y then delformLeft x a y s b else (if x > y then delformRight x a y s b else app a b))" |
haftmann@35534
   589
  "delformLeft x (Branch B lt z v rt) y s b = balleft (del x (Branch B lt z v rt)) y s b" |
haftmann@35534
   590
  "delformLeft x a y s b = Branch R (del x a) y s b" |
haftmann@35534
   591
  "delformRight x a y s (Branch B lt z v rt) = balright a y s (del x (Branch B lt z v rt))" | 
haftmann@35534
   592
  "delformRight x a y s b = Branch R a y s (del x b)"
krauss@26192
   593
krauss@26192
   594
lemma 
krauss@26192
   595
  assumes "inv2 lt" "inv1 lt"
krauss@26192
   596
  shows
haftmann@35534
   597
  "\<lbrakk>inv2 rt; bheight lt = bheight rt; inv1 rt\<rbrakk> \<Longrightarrow>
haftmann@35534
   598
  inv2 (delformLeft x lt k v rt) \<and> bheight (delformLeft x lt k v rt) = bheight lt \<and> (color_of lt = B \<and> color_of rt = B \<and> inv1 (delformLeft x lt k v rt) \<or> (color_of lt \<noteq> B \<or> color_of rt \<noteq> B) \<and> inv1l (delformLeft x lt k v rt))"
haftmann@35534
   599
  and "\<lbrakk>inv2 rt; bheight lt = bheight rt; inv1 rt\<rbrakk> \<Longrightarrow>
haftmann@35534
   600
  inv2 (delformRight x lt k v rt) \<and> bheight (delformRight x lt k v rt) = bheight lt \<and> (color_of lt = B \<and> color_of rt = B \<and> inv1 (delformRight x lt k v rt) \<or> (color_of lt \<noteq> B \<or> color_of rt \<noteq> B) \<and> inv1l (delformRight x lt k v rt))"
haftmann@35534
   601
  and del_inv1_inv2: "inv2 (del x lt) \<and> (color_of lt = R \<and> bheight (del x lt) = bheight lt \<and> inv1 (del x lt) 
haftmann@35534
   602
  \<or> color_of lt = B \<and> bheight (del x lt) = bheight lt - 1 \<and> inv1l (del x lt))"
krauss@26192
   603
using assms
krauss@26192
   604
proof (induct x lt k v rt and x lt k v rt and x lt rule: delformLeft_delformRight_del.induct)
krauss@26192
   605
case (2 y c _ y')
krauss@26192
   606
  have "y = y' \<or> y < y' \<or> y > y'" by auto
krauss@26192
   607
  thus ?case proof (elim disjE)
krauss@26192
   608
    assume "y = y'"
krauss@26192
   609
    with 2 show ?thesis by (cases c) (simp add: app_inv2 app_inv1)+
krauss@26192
   610
  next
krauss@26192
   611
    assume "y < y'"
krauss@26192
   612
    with 2 show ?thesis by (cases c) auto
krauss@26192
   613
  next
krauss@26192
   614
    assume "y' < y"
krauss@26192
   615
    with 2 show ?thesis by (cases c) auto
krauss@26192
   616
  qed
krauss@26192
   617
next
krauss@26192
   618
  case (3 y lt z v rta y' ss bb) 
haftmann@35534
   619
  thus ?case by (cases "color_of (Branch B lt z v rta) = B \<and> color_of bb = B") (simp add: balleft_inv2_with_inv1 balleft_inv1 balleft_inv1l)+
krauss@26192
   620
next
krauss@26192
   621
  case (5 y a y' ss lt z v rta)
haftmann@35534
   622
  thus ?case by (cases "color_of a = B \<and> color_of (Branch B lt z v rta) = B") (simp add: balright_inv2_with_inv1 balright_inv1 balright_inv1l)+
krauss@26192
   623
next
haftmann@35534
   624
  case ("6_1" y a y' ss) thus ?case by (cases "color_of a = B \<and> color_of Empty = B") simp+
krauss@26192
   625
qed auto
krauss@26192
   626
krauss@26192
   627
lemma 
haftmann@35534
   628
  delformLeft_tree_less: "\<lbrakk>tree_less v lt; tree_less v rt; k < v\<rbrakk> \<Longrightarrow> tree_less v (delformLeft x lt k y rt)"
haftmann@35534
   629
  and delformRight_tree_less: "\<lbrakk>tree_less v lt; tree_less v rt; k < v\<rbrakk> \<Longrightarrow> tree_less v (delformRight x lt k y rt)"
haftmann@35534
   630
  and del_tree_less: "tree_less v lt \<Longrightarrow> tree_less v (del x lt)"
krauss@26192
   631
by (induct x lt k y rt and x lt k y rt and x lt rule: delformLeft_delformRight_del.induct) 
haftmann@35534
   632
   (auto simp: balleft_tree_less balright_tree_less)
krauss@26192
   633
haftmann@35534
   634
lemma delformLeft_tree_greater: "\<lbrakk>tree_greater v lt; tree_greater v rt; k > v\<rbrakk> \<Longrightarrow> tree_greater v (delformLeft x lt k y rt)"
haftmann@35534
   635
  and delformRight_tree_greater: "\<lbrakk>tree_greater v lt; tree_greater v rt; k > v\<rbrakk> \<Longrightarrow> tree_greater v (delformRight x lt k y rt)"
haftmann@35534
   636
  and del_tree_greater: "tree_greater v lt \<Longrightarrow> tree_greater v (del x lt)"
krauss@26192
   637
by (induct x lt k y rt and x lt k y rt and x lt rule: delformLeft_delformRight_del.induct)
haftmann@35534
   638
   (auto simp: balleft_tree_greater balright_tree_greater)
krauss@26192
   639
haftmann@35534
   640
lemma "\<lbrakk>sorted lt; sorted rt; tree_less k lt; tree_greater k rt\<rbrakk> \<Longrightarrow> sorted (delformLeft x lt k y rt)"
haftmann@35534
   641
  and "\<lbrakk>sorted lt; sorted rt; tree_less k lt; tree_greater k rt\<rbrakk> \<Longrightarrow> sorted (delformRight x lt k y rt)"
haftmann@35534
   642
  and del_sorted: "sorted lt \<Longrightarrow> sorted (del x lt)"
krauss@26192
   643
proof (induct x lt k y rt and x lt k y rt and x lt rule: delformLeft_delformRight_del.induct)
krauss@26192
   644
  case (3 x lta zz v rta yy ss bb)
haftmann@35534
   645
  from 3 have "tree_less yy (Branch B lta zz v rta)" by simp
haftmann@35534
   646
  hence "tree_less yy (del x (Branch B lta zz v rta))" by (rule del_tree_less)
haftmann@35534
   647
  with 3 show ?case by (simp add: balleft_sorted)
krauss@26192
   648
next
krauss@26192
   649
  case ("4_2" x vaa vbb vdd vc yy ss bb)
haftmann@35534
   650
  hence "tree_less yy (Branch R vaa vbb vdd vc)" by simp
haftmann@35534
   651
  hence "tree_less yy (del x (Branch R vaa vbb vdd vc))" by (rule del_tree_less)
krauss@26192
   652
  with "4_2" show ?case by simp
krauss@26192
   653
next
krauss@26192
   654
  case (5 x aa yy ss lta zz v rta) 
haftmann@35534
   655
  hence "tree_greater yy (Branch B lta zz v rta)" by simp
haftmann@35534
   656
  hence "tree_greater yy (del x (Branch B lta zz v rta))" by (rule del_tree_greater)
haftmann@35534
   657
  with 5 show ?case by (simp add: balright_sorted)
krauss@26192
   658
next
krauss@26192
   659
  case ("6_2" x aa yy ss vaa vbb vdd vc)
haftmann@35534
   660
  hence "tree_greater yy (Branch R vaa vbb vdd vc)" by simp
haftmann@35534
   661
  hence "tree_greater yy (del x (Branch R vaa vbb vdd vc))" by (rule del_tree_greater)
krauss@26192
   662
  with "6_2" show ?case by simp
haftmann@35534
   663
qed (auto simp: app_sorted)
krauss@26192
   664
haftmann@35534
   665
lemma "\<lbrakk>sorted lt; sorted rt; tree_less kt lt; tree_greater kt rt; inv1 lt; inv1 rt; inv2 lt; inv2 rt; bheight lt = bheight rt; x < kt\<rbrakk> \<Longrightarrow> entry_in_tree k v (delformLeft x lt kt y rt) = (False \<or> (x \<noteq> k \<and> entry_in_tree k v (Branch c lt kt y rt)))"
haftmann@35534
   666
  and "\<lbrakk>sorted lt; sorted rt; tree_less kt lt; tree_greater kt rt; inv1 lt; inv1 rt; inv2 lt; inv2 rt; bheight lt = bheight rt; x > kt\<rbrakk> \<Longrightarrow> entry_in_tree k v (delformRight x lt kt y rt) = (False \<or> (x \<noteq> k \<and> entry_in_tree k v (Branch c lt kt y rt)))"
haftmann@35534
   667
  and del_pit: "\<lbrakk>sorted t; inv1 t; inv2 t\<rbrakk> \<Longrightarrow> entry_in_tree k v (del x t) = (False \<or> (x \<noteq> k \<and> entry_in_tree k v t))"
krauss@26192
   668
proof (induct x lt kt y rt and x lt kt y rt and x t rule: delformLeft_delformRight_del.induct)
krauss@26192
   669
  case (2 xx c aa yy ss bb)
krauss@26192
   670
  have "xx = yy \<or> xx < yy \<or> xx > yy" by auto
krauss@26192
   671
  from this 2 show ?case proof (elim disjE)
krauss@26192
   672
    assume "xx = yy"
krauss@26192
   673
    with 2 show ?thesis proof (cases "xx = k")
krauss@26192
   674
      case True
haftmann@35534
   675
      from 2 `xx = yy` `xx = k` have "sorted (Branch c aa yy ss bb) \<and> k = yy" by simp
haftmann@35534
   676
      hence "\<not> entry_in_tree k v aa" "\<not> entry_in_tree k v bb" by (auto simp: tree_less_nit tree_greater_prop)
krauss@26192
   677
      with `xx = yy` 2 `xx = k` show ?thesis by (simp add: app_pit)
krauss@26192
   678
    qed (simp add: app_pit)
krauss@26192
   679
  qed simp+
krauss@26192
   680
next    
krauss@26192
   681
  case (3 xx lta zz vv rta yy ss bb)
haftmann@35534
   682
  def mt[simp]: mt == "Branch B lta zz vv rta"
krauss@26192
   683
  from 3 have "inv2 mt \<and> inv1 mt" by simp
haftmann@35534
   684
  hence "inv2 (del xx mt) \<and> (color_of mt = R \<and> bheight (del xx mt) = bheight mt \<and> inv1 (del xx mt) \<or> color_of mt = B \<and> bheight (del xx mt) = bheight mt - 1 \<and> inv1l (del xx mt))" by (blast dest: del_inv1_inv2)
haftmann@35534
   685
  with 3 have 4: "entry_in_tree k v (delformLeft xx mt yy ss bb) = (False \<or> xx \<noteq> k \<and> entry_in_tree k v mt \<or> (k = yy \<and> v = ss) \<or> entry_in_tree k v bb)" by (simp add: balleft_pit)
krauss@26192
   686
  thus ?case proof (cases "xx = k")
krauss@26192
   687
    case True
haftmann@35534
   688
    from 3 True have "tree_greater yy bb \<and> yy > k" by simp
haftmann@35534
   689
    hence "tree_greater k bb" by (blast dest: tree_greater_trans)
haftmann@35534
   690
    with 3 4 True show ?thesis by (auto simp: tree_greater_nit)
krauss@26192
   691
  qed auto
krauss@26192
   692
next
krauss@26192
   693
  case ("4_1" xx yy ss bb)
krauss@26192
   694
  show ?case proof (cases "xx = k")
krauss@26192
   695
    case True
haftmann@35534
   696
    with "4_1" have "tree_greater yy bb \<and> k < yy" by simp
haftmann@35534
   697
    hence "tree_greater k bb" by (blast dest: tree_greater_trans)
krauss@26192
   698
    with "4_1" `xx = k` 
haftmann@35534
   699
   have "entry_in_tree k v (Branch R Empty yy ss bb) = entry_in_tree k v Empty" by (auto simp: tree_greater_nit)
krauss@26192
   700
    thus ?thesis by auto
krauss@26192
   701
  qed simp+
krauss@26192
   702
next
krauss@26192
   703
  case ("4_2" xx vaa vbb vdd vc yy ss bb)
krauss@26192
   704
  thus ?case proof (cases "xx = k")
krauss@26192
   705
    case True
haftmann@35534
   706
    with "4_2" have "k < yy \<and> tree_greater yy bb" by simp
haftmann@35534
   707
    hence "tree_greater k bb" by (blast dest: tree_greater_trans)
haftmann@35534
   708
    with True "4_2" show ?thesis by (auto simp: tree_greater_nit)
krauss@26192
   709
  qed simp
krauss@26192
   710
next
krauss@26192
   711
  case (5 xx aa yy ss lta zz vv rta)
haftmann@35534
   712
  def mt[simp]: mt == "Branch B lta zz vv rta"
krauss@26192
   713
  from 5 have "inv2 mt \<and> inv1 mt" by simp
haftmann@35534
   714
  hence "inv2 (del xx mt) \<and> (color_of mt = R \<and> bheight (del xx mt) = bheight mt \<and> inv1 (del xx mt) \<or> color_of mt = B \<and> bheight (del xx mt) = bheight mt - 1 \<and> inv1l (del xx mt))" by (blast dest: del_inv1_inv2)
haftmann@35534
   715
  with 5 have 3: "entry_in_tree k v (delformRight xx aa yy ss mt) = (entry_in_tree k v aa \<or> (k = yy \<and> v = ss) \<or> False \<or> xx \<noteq> k \<and> entry_in_tree k v mt)" by (simp add: balright_pit)
krauss@26192
   716
  thus ?case proof (cases "xx = k")
krauss@26192
   717
    case True
haftmann@35534
   718
    from 5 True have "tree_less yy aa \<and> yy < k" by simp
haftmann@35534
   719
    hence "tree_less k aa" by (blast dest: tree_less_trans)
haftmann@35534
   720
    with 3 5 True show ?thesis by (auto simp: tree_less_nit)
krauss@26192
   721
  qed auto
krauss@26192
   722
next
krauss@26192
   723
  case ("6_1" xx aa yy ss)
krauss@26192
   724
  show ?case proof (cases "xx = k")
krauss@26192
   725
    case True
haftmann@35534
   726
    with "6_1" have "tree_less yy aa \<and> k > yy" by simp
haftmann@35534
   727
    hence "tree_less k aa" by (blast dest: tree_less_trans)
haftmann@35534
   728
    with "6_1" `xx = k` show ?thesis by (auto simp: tree_less_nit)
krauss@26192
   729
  qed simp
krauss@26192
   730
next
krauss@26192
   731
  case ("6_2" xx aa yy ss vaa vbb vdd vc)
krauss@26192
   732
  thus ?case proof (cases "xx = k")
krauss@26192
   733
    case True
haftmann@35534
   734
    with "6_2" have "k > yy \<and> tree_less yy aa" by simp
haftmann@35534
   735
    hence "tree_less k aa" by (blast dest: tree_less_trans)
haftmann@35534
   736
    with True "6_2" show ?thesis by (auto simp: tree_less_nit)
krauss@26192
   737
  qed simp
krauss@26192
   738
qed simp
krauss@26192
   739
krauss@26192
   740
krauss@26192
   741
definition delete where
krauss@26192
   742
  delete_def: "delete k t = paint B (del k t)"
krauss@26192
   743
haftmann@35534
   744
theorem delete_is_rbt[simp]: assumes "is_rbt t" shows "is_rbt (delete k t)"
krauss@26192
   745
proof -
haftmann@35534
   746
  from assms have "inv2 t" and "inv1 t" unfolding is_rbt_def by auto 
haftmann@35534
   747
  hence "inv2 (del k t) \<and> (color_of t = R \<and> bheight (del k t) = bheight t \<and> inv1 (del k t) \<or> color_of t = B \<and> bheight (del k t) = bheight t - 1 \<and> inv1l (del k t))" by (rule del_inv1_inv2)
haftmann@35534
   748
  hence "inv2 (del k t) \<and> inv1l (del k t)" by (cases "color_of t") auto
krauss@26192
   749
  with assms show ?thesis
haftmann@35534
   750
    unfolding is_rbt_def delete_def
haftmann@35534
   751
    by (auto intro: paint_sorted del_sorted)
krauss@26192
   752
qed
krauss@26192
   753
krauss@26192
   754
lemma delete_pit: 
haftmann@35534
   755
  assumes "is_rbt t" 
haftmann@35534
   756
  shows "entry_in_tree k v (delete x t) = (x \<noteq> k \<and> entry_in_tree k v t)"
haftmann@35534
   757
  using assms unfolding is_rbt_def delete_def
krauss@26192
   758
  by (auto simp: del_pit)
krauss@26192
   759
haftmann@35534
   760
lemma lookup_delete:
haftmann@35534
   761
  assumes is_rbt: "is_rbt t"
haftmann@35534
   762
  shows "lookup (delete k t) = (lookup t)|`(-{k})"
krauss@26192
   763
proof
krauss@26192
   764
  fix x
haftmann@35534
   765
  show "lookup (delete k t) x = (lookup t |` (-{k})) x" 
krauss@26192
   766
  proof (cases "x = k")
krauss@26192
   767
    assume "x = k" 
haftmann@35534
   768
    with is_rbt show ?thesis
haftmann@35534
   769
      by (cases "lookup (delete k t) k") (auto simp: lookup_pit delete_pit)
krauss@26192
   770
  next
krauss@26192
   771
    assume "x \<noteq> k"
krauss@26192
   772
    thus ?thesis
haftmann@35534
   773
      by auto (metis is_rbt delete_is_rbt delete_pit is_rbt_sorted lookup_from_pit)
krauss@26192
   774
  qed
krauss@26192
   775
qed
krauss@26192
   776
krauss@26192
   777
subsection {* Union *}
krauss@26192
   778
krauss@26192
   779
primrec
krauss@26192
   780
  unionwithkey :: "('a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
krauss@26192
   781
where
krauss@26192
   782
  "unionwithkey f t Empty = t"
haftmann@35534
   783
| "unionwithkey f t (Branch c lt k v rt) = unionwithkey f (unionwithkey f (insertwithkey f k v t) lt) rt"
krauss@26192
   784
haftmann@35534
   785
lemma unionwk_sorted: "sorted lt \<Longrightarrow> sorted (unionwithkey f lt rt)" 
haftmann@35534
   786
  by (induct rt arbitrary: lt) (auto simp: insertwk_sorted)
haftmann@35534
   787
theorem unionwk_is_rbt[simp]: "is_rbt lt \<Longrightarrow> is_rbt (unionwithkey f lt rt)" 
haftmann@35534
   788
  by (induct rt arbitrary: lt) (simp add: insertwk_is_rbt)+
krauss@26192
   789
krauss@26192
   790
definition
krauss@26192
   791
  unionwith where
krauss@26192
   792
  "unionwith f = unionwithkey (\<lambda>_. f)"
krauss@26192
   793
haftmann@35534
   794
theorem unionw_is_rbt: "is_rbt lt \<Longrightarrow> is_rbt (unionwith f lt rt)" unfolding unionwith_def by simp
krauss@26192
   795
krauss@26192
   796
definition union where
krauss@26192
   797
  "union = unionwithkey (%_ _ rv. rv)"
krauss@26192
   798
haftmann@35534
   799
theorem union_is_rbt: "is_rbt lt \<Longrightarrow> is_rbt (union lt rt)" unfolding union_def by simp
krauss@26192
   800
haftmann@35534
   801
lemma union_Branch[simp]:
haftmann@35534
   802
  "union t (Branch c lt k v rt) = union (union (insert k v t) lt) rt"
haftmann@35534
   803
  unfolding union_def insert_def
krauss@26192
   804
  by simp
krauss@26192
   805
haftmann@35534
   806
lemma lookup_union:
haftmann@35534
   807
  assumes "is_rbt s" "sorted t"
haftmann@35534
   808
  shows "lookup (union s t) = lookup s ++ lookup t"
krauss@26192
   809
using assms
krauss@26192
   810
proof (induct t arbitrary: s)
krauss@26192
   811
  case Empty thus ?case by (auto simp: union_def)
krauss@26192
   812
next
haftmann@35534
   813
  case (Branch c l k v r s)
haftmann@35534
   814
  hence sortedrl: "sorted r" "sorted l" "l |\<guillemotleft> k" "k \<guillemotleft>| r" by auto
krauss@26192
   815
haftmann@35534
   816
  have meq: "lookup s(k \<mapsto> v) ++ lookup l ++ lookup r =
haftmann@35534
   817
    lookup s ++
haftmann@35534
   818
    (\<lambda>a. if a < k then lookup l a
haftmann@35534
   819
    else if k < a then lookup r a else Some v)" (is "?m1 = ?m2")
krauss@26192
   820
  proof (rule ext)
krauss@26192
   821
    fix a
krauss@26192
   822
krauss@26192
   823
   have "k < a \<or> k = a \<or> k > a" by auto
krauss@26192
   824
    thus "?m1 a = ?m2 a"
krauss@26192
   825
    proof (elim disjE)
krauss@26192
   826
      assume "k < a"
haftmann@35534
   827
      with `l |\<guillemotleft> k` have "l |\<guillemotleft> a" by (rule tree_less_trans)
krauss@26192
   828
      with `k < a` show ?thesis
krauss@26192
   829
        by (auto simp: map_add_def split: option.splits)
krauss@26192
   830
    next
krauss@26192
   831
      assume "k = a"
krauss@26192
   832
      with `l |\<guillemotleft> k` `k \<guillemotleft>| r` 
krauss@26192
   833
      show ?thesis by (auto simp: map_add_def)
krauss@26192
   834
    next
krauss@26192
   835
      assume "a < k"
haftmann@35534
   836
      from this `k \<guillemotleft>| r` have "a \<guillemotleft>| r" by (rule tree_greater_trans)
krauss@26192
   837
      with `a < k` show ?thesis
krauss@26192
   838
        by (auto simp: map_add_def split: option.splits)
krauss@26192
   839
    qed
krauss@26192
   840
  qed
krauss@26192
   841
haftmann@35534
   842
  from Branch
krauss@26192
   843
  have IHs:
haftmann@35534
   844
    "lookup (union (union (insert k v s) l) r) = lookup (union (insert k v s) l) ++ lookup r"
haftmann@35534
   845
    "lookup (union (insert k v s) l) = lookup (insert k v s) ++ lookup l"
haftmann@35534
   846
    by (auto intro: union_is_rbt insert_is_rbt)
krauss@26192
   847
  
krauss@26192
   848
  with meq show ?case
haftmann@35534
   849
    by (auto simp: lookup_insert[OF Branch(3)])
krauss@26192
   850
qed
krauss@26192
   851
krauss@26192
   852
subsection {* Adjust *}
krauss@26192
   853
krauss@26192
   854
primrec
krauss@26192
   855
  adjustwithkey :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
krauss@26192
   856
where
krauss@26192
   857
  "adjustwithkey f k Empty = Empty"
haftmann@35534
   858
| "adjustwithkey f k (Branch c lt x v rt) = (if k < x then (Branch c (adjustwithkey f k lt) x v rt) else if k > x then (Branch c lt x v (adjustwithkey f k rt)) else (Branch c lt x (f x v) rt))"
krauss@26192
   859
haftmann@35534
   860
lemma adjustwk_color_of: "color_of (adjustwithkey f k t) = color_of t" by (induct t) simp+
haftmann@35534
   861
lemma adjustwk_inv1: "inv1 (adjustwithkey f k t) = inv1 t" by (induct t) (simp add: adjustwk_color_of)+
haftmann@35534
   862
lemma adjustwk_inv2: "inv2 (adjustwithkey f k t) = inv2 t" "bheight (adjustwithkey f k t) = bheight t" by (induct t) simp+
haftmann@35534
   863
lemma adjustwk_tree_greater: "tree_greater k (adjustwithkey f kk t) = tree_greater k t" by (induct t) simp+
haftmann@35534
   864
lemma adjustwk_tree_less: "tree_less k (adjustwithkey f kk t) = tree_less k t" by (induct t) simp+
haftmann@35534
   865
lemma adjustwk_sorted: "sorted (adjustwithkey f k t) = sorted t" by (induct t) (simp add: adjustwk_tree_less adjustwk_tree_greater)+
krauss@26192
   866
haftmann@35534
   867
theorem adjustwk_is_rbt[simp]: "is_rbt (adjustwithkey f k t) = is_rbt t" 
haftmann@35534
   868
unfolding is_rbt_def by (simp add: adjustwk_inv2 adjustwk_color_of adjustwk_sorted adjustwk_inv1 )
krauss@26192
   869
krauss@26192
   870
theorem adjustwithkey_map[simp]:
haftmann@35534
   871
  "lookup (adjustwithkey f k t) x = 
haftmann@35534
   872
  (if x = k then case lookup t x of None \<Rightarrow> None | Some y \<Rightarrow> Some (f k y)
haftmann@35534
   873
            else lookup t x)"
krauss@26192
   874
by (induct t arbitrary: x) (auto split:option.splits)
krauss@26192
   875
krauss@26192
   876
definition adjust where
krauss@26192
   877
  "adjust f = adjustwithkey (\<lambda>_. f)"
krauss@26192
   878
haftmann@35534
   879
theorem adjust_is_rbt[simp]: "is_rbt (adjust f k t) = is_rbt t" unfolding adjust_def by simp
krauss@26192
   880
krauss@26192
   881
theorem adjust_map[simp]:
haftmann@35534
   882
  "lookup (adjust f k t) x = 
haftmann@35534
   883
  (if x = k then case lookup t x of None \<Rightarrow> None | Some y \<Rightarrow> Some (f y)
haftmann@35534
   884
            else lookup t x)"
krauss@26192
   885
unfolding adjust_def by simp
krauss@26192
   886
krauss@26192
   887
subsection {* Map *}
krauss@26192
   888
krauss@26192
   889
primrec
krauss@26192
   890
  mapwithkey :: "('a::linorder \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'c) rbt"
krauss@26192
   891
where
krauss@26192
   892
  "mapwithkey f Empty = Empty"
haftmann@35534
   893
| "mapwithkey f (Branch c lt k v rt) = Branch c (mapwithkey f lt) k (f k v) (mapwithkey f rt)"
krauss@26192
   894
krauss@26192
   895
theorem mapwk_keys[simp]: "keys (mapwithkey f t) = keys t" by (induct t) auto
haftmann@35534
   896
lemma mapwk_tree_greater: "tree_greater k (mapwithkey f t) = tree_greater k t" by (induct t) simp+
haftmann@35534
   897
lemma mapwk_tree_less: "tree_less k (mapwithkey f t) = tree_less k t" by (induct t) simp+
haftmann@35534
   898
lemma mapwk_sorted: "sorted (mapwithkey f t) = sorted t"  by (induct t) (simp add: mapwk_tree_less mapwk_tree_greater)+
haftmann@35534
   899
lemma mapwk_color_of: "color_of (mapwithkey f t) = color_of t" by (induct t) simp+
haftmann@35534
   900
lemma mapwk_inv1: "inv1 (mapwithkey f t) = inv1 t" by (induct t) (simp add: mapwk_color_of)+
haftmann@35534
   901
lemma mapwk_inv2: "inv2 (mapwithkey f t) = inv2 t" "bheight (mapwithkey f t) = bheight t" by (induct t) simp+
haftmann@35534
   902
theorem mapwk_is_rbt[simp]: "is_rbt (mapwithkey f t) = is_rbt t" 
haftmann@35534
   903
unfolding is_rbt_def by (simp add: mapwk_inv1 mapwk_inv2 mapwk_sorted mapwk_color_of)
krauss@26192
   904
haftmann@35534
   905
theorem lookup_mapwk[simp]: "lookup (mapwithkey f t) x = Option.map (f x) (lookup t x)"
krauss@26192
   906
by (induct t) auto
krauss@26192
   907
krauss@26192
   908
definition map
krauss@26192
   909
where map_def: "map f == mapwithkey (\<lambda>_. f)"
krauss@26192
   910
krauss@26192
   911
theorem map_keys[simp]: "keys (map f t) = keys t" unfolding map_def by simp
haftmann@35534
   912
theorem map_is_rbt[simp]: "is_rbt (map f t) = is_rbt t" unfolding map_def by simp
haftmann@35534
   913
theorem lookup_map[simp]: "lookup (map f t) = Option.map f o lookup t"
krauss@26192
   914
  by (rule ext) (simp add:map_def)
krauss@26192
   915
krauss@26192
   916
subsection {* Fold *}
krauss@26192
   917
krauss@26192
   918
text {* The following is still incomplete... *}
krauss@26192
   919
krauss@26192
   920
primrec
krauss@26192
   921
  foldwithkey :: "('a::linorder \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a,'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c"
krauss@26192
   922
where
krauss@26192
   923
  "foldwithkey f Empty v = v"
haftmann@35534
   924
| "foldwithkey f (Branch c lt k x rt) v = foldwithkey f rt (f k x (foldwithkey f lt v))"
krauss@26192
   925
haftmann@35534
   926
lemma lookup_entries_aux: "sorted (Branch c t1 k v t2) \<Longrightarrow> RBT.lookup (Branch c t1 k v t2) = RBT.lookup t2 ++ [k\<mapsto>v] ++ RBT.lookup t1"
krauss@32237
   927
proof (rule ext)
krauss@32237
   928
  fix x
haftmann@35534
   929
  assume SORTED: "sorted (Branch c t1 k v t2)"
haftmann@35534
   930
  let ?thesis = "RBT.lookup (Branch c t1 k v t2) x = (RBT.lookup t2 ++ [k \<mapsto> v] ++ RBT.lookup t1) x"
krauss@32237
   931
haftmann@35534
   932
  have DOM_T1: "!!k'. k'\<in>dom (RBT.lookup t1) \<Longrightarrow> k>k'"
krauss@32237
   933
  proof -
krauss@32237
   934
    fix k'
haftmann@35534
   935
    from SORTED have "t1 |\<guillemotleft> k" by simp
haftmann@35534
   936
    with tree_less_prop have "\<forall>k'\<in>keys t1. k>k'" by auto
haftmann@35534
   937
    moreover assume "k'\<in>dom (RBT.lookup t1)"
haftmann@35534
   938
    ultimately show "k>k'" using RBT.lookup_keys SORTED by auto
krauss@32237
   939
  qed
krauss@32237
   940
haftmann@35534
   941
  have DOM_T2: "!!k'. k'\<in>dom (RBT.lookup t2) \<Longrightarrow> k<k'"
krauss@32237
   942
  proof -
krauss@32237
   943
    fix k'
haftmann@35534
   944
    from SORTED have "k \<guillemotleft>| t2" by simp
haftmann@35534
   945
    with tree_greater_prop have "\<forall>k'\<in>keys t2. k<k'" by auto
haftmann@35534
   946
    moreover assume "k'\<in>dom (RBT.lookup t2)"
haftmann@35534
   947
    ultimately show "k<k'" using RBT.lookup_keys SORTED by auto
krauss@32237
   948
  qed
krauss@32237
   949
krauss@32237
   950
  {
krauss@32237
   951
    assume C: "x<k"
haftmann@35534
   952
    hence "RBT.lookup (Branch c t1 k v t2) x = RBT.lookup t1 x" by simp
krauss@32237
   953
    moreover from C have "x\<notin>dom [k\<mapsto>v]" by simp
haftmann@35534
   954
    moreover have "x\<notin>dom (RBT.lookup t2)" proof
haftmann@35534
   955
      assume "x\<in>dom (RBT.lookup t2)"
krauss@32237
   956
      with DOM_T2 have "k<x" by blast
krauss@32237
   957
      with C show False by simp
krauss@32237
   958
    qed
krauss@32237
   959
    ultimately have ?thesis by (simp add: map_add_upd_left map_add_dom_app_simps)
krauss@32237
   960
  } moreover {
krauss@32237
   961
    assume [simp]: "x=k"
haftmann@35534
   962
    hence "RBT.lookup (Branch c t1 k v t2) x = [k \<mapsto> v] x" by simp
haftmann@35534
   963
    moreover have "x\<notin>dom (RBT.lookup t1)" proof
haftmann@35534
   964
      assume "x\<in>dom (RBT.lookup t1)"
krauss@32237
   965
      with DOM_T1 have "k>x" by blast
krauss@32237
   966
      thus False by simp
krauss@32237
   967
    qed
krauss@32237
   968
    ultimately have ?thesis by (simp add: map_add_upd_left map_add_dom_app_simps)
krauss@32237
   969
  } moreover {
krauss@32237
   970
    assume C: "x>k"
haftmann@35534
   971
    hence "RBT.lookup (Branch c t1 k v t2) x = RBT.lookup t2 x" by (simp add: less_not_sym[of k x])
krauss@32237
   972
    moreover from C have "x\<notin>dom [k\<mapsto>v]" by simp
haftmann@35534
   973
    moreover have "x\<notin>dom (RBT.lookup t1)" proof
haftmann@35534
   974
      assume "x\<in>dom (RBT.lookup t1)"
krauss@32237
   975
      with DOM_T1 have "k>x" by simp
krauss@32237
   976
      with C show False by simp
krauss@32237
   977
    qed
krauss@32237
   978
    ultimately have ?thesis by (simp add: map_add_upd_left map_add_dom_app_simps)
krauss@32237
   979
  } ultimately show ?thesis using less_linear by blast
krauss@32237
   980
qed
krauss@32237
   981
haftmann@35534
   982
lemma map_of_entries:
haftmann@35534
   983
  shows "sorted t \<Longrightarrow> map_of (entries t) = lookup t"
krauss@32237
   984
proof (induct t)
haftmann@35534
   985
  case Empty thus ?case by (simp add: RBT.lookup_Empty)
krauss@32237
   986
next
haftmann@35534
   987
  case (Branch c t1 k v t2)
haftmann@35534
   988
  hence "map_of (entries (Branch c t1 k v t2)) = RBT.lookup t2 ++ [k \<mapsto> v] ++ RBT.lookup t1" by simp
haftmann@35534
   989
  also note lookup_entries_aux [OF Branch.prems,symmetric]
krauss@32237
   990
  finally show ?case .
krauss@32237
   991
qed
krauss@26192
   992
haftmann@35534
   993
lemma fold_entries_fold:
haftmann@35534
   994
  "foldwithkey f t x = foldl (\<lambda>x (k,v). f k v x) x (entries t)"
krauss@26192
   995
by (induct t arbitrary: x) auto
krauss@26192
   996
haftmann@35534
   997
lemma entries_pit[simp]: "(k, v) \<in> set (entries t) = entry_in_tree k v t"
krauss@26192
   998
by (induct t) auto
krauss@26192
   999
haftmann@35534
  1000
lemma sorted_entries:
haftmann@35534
  1001
  "sorted t \<Longrightarrow> List.sorted (List.map fst (entries t))"
krauss@26192
  1002
by (induct t) 
haftmann@35534
  1003
  (force simp: sorted_append sorted_Cons tree_ord_props 
haftmann@35534
  1004
      dest!: entry_in_tree_keys)+
krauss@26192
  1005
haftmann@35534
  1006
lemma distinct_entries:
haftmann@35534
  1007
  "sorted t \<Longrightarrow> distinct (List.map fst (entries t))"
krauss@26192
  1008
by (induct t) 
haftmann@35534
  1009
  (force simp: sorted_append sorted_Cons tree_ord_props 
haftmann@35534
  1010
      dest!: entry_in_tree_keys)+
haftmann@35534
  1011
haftmann@35534
  1012
hide (open) const Empty insert delete entries lookup map fold union adjust sorted
haftmann@35534
  1013
krauss@26192
  1014
(*>*)
krauss@26192
  1015
krauss@26192
  1016
text {* 
krauss@26192
  1017
  This theory defines purely functional red-black trees which can be
krauss@26192
  1018
  used as an efficient representation of finite maps.
krauss@26192
  1019
*}
krauss@26192
  1020
krauss@26192
  1021
subsection {* Data type and invariant *}
krauss@26192
  1022
krauss@26192
  1023
text {*
krauss@26192
  1024
  The type @{typ "('k, 'v) rbt"} denotes red-black trees with keys of
krauss@26192
  1025
  type @{typ "'k"} and values of type @{typ "'v"}. To function
haftmann@35534
  1026
  properly, the key type musorted belong to the @{text "linorder"} class.
krauss@26192
  1027
krauss@26192
  1028
  A value @{term t} of this type is a valid red-black tree if it
haftmann@35534
  1029
  satisfies the invariant @{text "is_rbt t"}.
krauss@26192
  1030
  This theory provides lemmas to prove that the invariant is
krauss@26192
  1031
  satisfied throughout the computation.
krauss@26192
  1032
haftmann@35534
  1033
  The interpretation function @{const "RBT.lookup"} returns the partial
krauss@26192
  1034
  map represented by a red-black tree:
haftmann@35534
  1035
  @{term_type[display] "RBT.lookup"}
krauss@26192
  1036
krauss@26192
  1037
  This function should be used for reasoning about the semantics of the RBT
krauss@26192
  1038
  operations. Furthermore, it implements the lookup functionality for
haftmann@35534
  1039
  the data sortedructure: It is executable and the lookup is performed in
krauss@26192
  1040
  $O(\log n)$.  
krauss@26192
  1041
*}
krauss@26192
  1042
krauss@26192
  1043
subsection {* Operations *}
krauss@26192
  1044
krauss@26192
  1045
text {*
krauss@26192
  1046
  Currently, the following operations are supported:
krauss@26192
  1047
haftmann@35534
  1048
  @{term_type[display] "RBT.Empty"}
krauss@26192
  1049
  Returns the empty tree. $O(1)$
krauss@26192
  1050
haftmann@35534
  1051
  @{term_type[display] "RBT.insert"}
krauss@26192
  1052
  Updates the map at a given position. $O(\log n)$
krauss@26192
  1053
haftmann@35534
  1054
  @{term_type[display] "RBT.delete"}
krauss@26192
  1055
  Deletes a map entry at a given position. $O(\log n)$
krauss@26192
  1056
haftmann@35534
  1057
  @{term_type[display] "RBT.union"}
krauss@26192
  1058
  Forms the union of two trees, preferring entries from the first one.
krauss@26192
  1059
haftmann@35534
  1060
  @{term_type[display] "RBT.map"}
krauss@26192
  1061
  Maps a function over the values of a map. $O(n)$
krauss@26192
  1062
*}
krauss@26192
  1063
krauss@26192
  1064
krauss@26192
  1065
subsection {* Invariant preservation *}
krauss@26192
  1066
krauss@26192
  1067
text {*
krauss@26192
  1068
  \noindent
haftmann@35534
  1069
  @{thm Empty_is_rbt}\hfill(@{text "Empty_is_rbt"})
krauss@26192
  1070
krauss@26192
  1071
  \noindent
haftmann@35534
  1072
  @{thm insert_is_rbt}\hfill(@{text "insert_is_rbt"})
krauss@26192
  1073
krauss@26192
  1074
  \noindent
haftmann@35534
  1075
  @{thm delete_is_rbt}\hfill(@{text "delete_is_rbt"})
krauss@26192
  1076
krauss@26192
  1077
  \noindent
haftmann@35534
  1078
  @{thm union_is_rbt}\hfill(@{text "union_is_rbt"})
krauss@26192
  1079
krauss@26192
  1080
  \noindent
haftmann@35534
  1081
  @{thm map_is_rbt}\hfill(@{text "map_is_rbt"})
krauss@26192
  1082
*}
krauss@26192
  1083
krauss@26192
  1084
subsection {* Map Semantics *}
krauss@26192
  1085
krauss@26192
  1086
text {*
krauss@26192
  1087
  \noindent
haftmann@35534
  1088
  \underline{@{text "lookup_Empty"}}
haftmann@35534
  1089
  @{thm[display] lookup_Empty}
krauss@26192
  1090
  \vspace{1ex}
krauss@26192
  1091
krauss@26192
  1092
  \noindent
haftmann@35534
  1093
  \underline{@{text "lookup_insert"}}
haftmann@35534
  1094
  @{thm[display] lookup_insert}
krauss@26192
  1095
  \vspace{1ex}
krauss@26192
  1096
krauss@26192
  1097
  \noindent
haftmann@35534
  1098
  \underline{@{text "lookup_delete"}}
haftmann@35534
  1099
  @{thm[display] lookup_delete}
krauss@26192
  1100
  \vspace{1ex}
krauss@26192
  1101
krauss@26192
  1102
  \noindent
haftmann@35534
  1103
  \underline{@{text "lookup_union"}}
haftmann@35534
  1104
  @{thm[display] lookup_union}
krauss@26192
  1105
  \vspace{1ex}
krauss@26192
  1106
krauss@26192
  1107
  \noindent
haftmann@35534
  1108
  \underline{@{text "lookup_map"}}
haftmann@35534
  1109
  @{thm[display] lookup_map}
krauss@26192
  1110
  \vspace{1ex}
krauss@26192
  1111
*}
krauss@26192
  1112
krauss@26192
  1113
end