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