merged
authorhaftmann
Wed Mar 03 20:45:48 2010 +0100 (2010-03-03)
changeset 35553a8c8008a2c9d
parent 35549 d3df6465f1a0
parent 35552 364cb98a3e4e
child 35554 1e05ea0a5cd7
merged
src/HOL/Map.thy
     1.1 --- a/src/HOL/Library/RBT.thy	Wed Mar 03 20:21:30 2010 +0100
     1.2 +++ b/src/HOL/Library/RBT.thy	Wed Mar 03 20:45:48 2010 +0100
     1.3 @@ -10,6 +10,8 @@
     1.4  imports Main AssocList
     1.5  begin
     1.6  
     1.7 +subsection {* Datatype of RB trees *}
     1.8 +
     1.9  datatype color = R | B
    1.10  datatype ('a, 'b) rbt = Empty | Branch color "('a, 'b) rbt" 'a 'b "('a, 'b) rbt"
    1.11  
    1.12 @@ -23,39 +25,48 @@
    1.13    case (Branch c) with that show thesis by (cases c) blast+
    1.14  qed
    1.15  
    1.16 -text {* Content of a tree *}
    1.17 +subsection {* Tree properties *}
    1.18  
    1.19 -primrec entries
    1.20 +subsubsection {* Content of a tree *}
    1.21 +
    1.22 +primrec entries :: "('a, 'b) rbt \<Rightarrow> ('a \<times> 'b) list"
    1.23  where 
    1.24    "entries Empty = []"
    1.25  | "entries (Branch _ l k v r) = entries l @ (k,v) # entries r"
    1.26  
    1.27 -text {* Search tree properties *}
    1.28 -
    1.29 -primrec entry_in_tree :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> bool"
    1.30 +abbreviation (input) entry_in_tree :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> bool"
    1.31  where
    1.32 -  "entry_in_tree k v Empty = False"
    1.33 -| "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"
    1.34 +  "entry_in_tree k v t \<equiv> (k, v) \<in> set (entries t)"
    1.35 +
    1.36 +definition keys :: "('a, 'b) rbt \<Rightarrow> 'a list" where
    1.37 +  "keys t = map fst (entries t)"
    1.38  
    1.39 -primrec keys :: "('k, 'v) rbt \<Rightarrow> 'k set"
    1.40 -where
    1.41 -  "keys Empty = {}"
    1.42 -| "keys (Branch _ l k _ r) = { k } \<union> keys l \<union> keys r"
    1.43 +lemma keys_simps [simp, code]:
    1.44 +  "keys Empty = []"
    1.45 +  "keys (Branch c l k v r) = keys l @ k # keys r"
    1.46 +  by (simp_all add: keys_def)
    1.47  
    1.48  lemma entry_in_tree_keys:
    1.49 -  "entry_in_tree k v t \<Longrightarrow> k \<in> keys t"
    1.50 -  by (induct t) auto
    1.51 +  assumes "(k, v) \<in> set (entries t)"
    1.52 +  shows "k \<in> set (keys t)"
    1.53 +proof -
    1.54 +  from assms have "fst (k, v) \<in> fst ` set (entries t)" by (rule imageI)
    1.55 +  then show ?thesis by (simp add: keys_def)
    1.56 +qed
    1.57 +
    1.58 +
    1.59 +subsubsection {* Search tree properties *}
    1.60  
    1.61  definition tree_less :: "'a\<Colon>order \<Rightarrow> ('a, 'b) rbt \<Rightarrow> bool"
    1.62  where
    1.63 -  tree_less_prop: "tree_less k t \<longleftrightarrow> (\<forall>x\<in>keys t. x < k)"
    1.64 +  tree_less_prop: "tree_less k t \<longleftrightarrow> (\<forall>x\<in>set (keys t). x < k)"
    1.65  
    1.66  abbreviation tree_less_symbol (infix "|\<guillemotleft>" 50)
    1.67  where "t |\<guillemotleft> x \<equiv> tree_less x t"
    1.68  
    1.69  definition tree_greater :: "'a\<Colon>order \<Rightarrow> ('a, 'b) rbt \<Rightarrow> bool" (infix "\<guillemotleft>|" 50) 
    1.70  where
    1.71 -  tree_greater_prop: "tree_greater k t = (\<forall>x\<in>keys t. k < x)"
    1.72 +  tree_greater_prop: "tree_greater k t = (\<forall>x\<in>set (keys t). k < x)"
    1.73  
    1.74  lemma tree_less_simps [simp]:
    1.75    "tree_less k Empty = True"
    1.76 @@ -72,55 +83,172 @@
    1.77  lemmas tree_greater_nit = tree_greater_prop entry_in_tree_keys
    1.78  lemmas tree_less_nit = tree_less_prop entry_in_tree_keys
    1.79  
    1.80 -lemma tree_less_trans: "t |\<guillemotleft> x \<Longrightarrow> x < y \<Longrightarrow> t |\<guillemotleft> y"
    1.81 +lemma tree_less_eq_trans: "l |\<guillemotleft> u \<Longrightarrow> u \<le> v \<Longrightarrow> l |\<guillemotleft> v"
    1.82 +  and tree_less_trans: "t |\<guillemotleft> x \<Longrightarrow> x < y \<Longrightarrow> t |\<guillemotleft> y"
    1.83 +  and tree_greater_eq_trans: "u \<le> v \<Longrightarrow> v \<guillemotleft>| r \<Longrightarrow> u \<guillemotleft>| r"
    1.84    and tree_greater_trans: "x < y \<Longrightarrow> y \<guillemotleft>| t \<Longrightarrow> x \<guillemotleft>| t"
    1.85 -by (auto simp: tree_ord_props)
    1.86 +  by (auto simp: tree_ord_props)
    1.87  
    1.88  primrec sorted :: "('a::linorder, 'b) rbt \<Rightarrow> bool"
    1.89  where
    1.90    "sorted Empty = True"
    1.91  | "sorted (Branch c l k v r) = (l |\<guillemotleft> k \<and> k \<guillemotleft>| r \<and> sorted l \<and> sorted r)"
    1.92  
    1.93 +lemma sorted_entries:
    1.94 +  "sorted t \<Longrightarrow> List.sorted (List.map fst (entries t))"
    1.95 +by (induct t) 
    1.96 +  (force simp: sorted_append sorted_Cons tree_ord_props 
    1.97 +      dest!: entry_in_tree_keys)+
    1.98 +
    1.99 +lemma distinct_entries:
   1.100 +  "sorted t \<Longrightarrow> distinct (List.map fst (entries t))"
   1.101 +by (induct t) 
   1.102 +  (force simp: sorted_append sorted_Cons tree_ord_props 
   1.103 +      dest!: entry_in_tree_keys)+
   1.104 +
   1.105 +
   1.106 +subsubsection {* Tree lookup *}
   1.107 +
   1.108  primrec lookup :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b"
   1.109  where
   1.110    "lookup Empty k = None"
   1.111  | "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)"
   1.112  
   1.113 +lemma lookup_keys: "sorted t \<Longrightarrow> dom (lookup t) = set (keys t)"
   1.114 +  by (induct t) (auto simp: dom_def tree_greater_prop tree_less_prop)
   1.115 +
   1.116 +lemma dom_lookup_Branch: 
   1.117 +  "sorted (Branch c t1 k v t2) \<Longrightarrow> 
   1.118 +    dom (lookup (Branch c t1 k v t2)) 
   1.119 +    = Set.insert k (dom (lookup t1) \<union> dom (lookup t2))"
   1.120 +proof -
   1.121 +  assume "sorted (Branch c t1 k v t2)"
   1.122 +  moreover from this have "sorted t1" "sorted t2" by simp_all
   1.123 +  ultimately show ?thesis by (simp add: lookup_keys)
   1.124 +qed
   1.125 +
   1.126 +lemma finite_dom_lookup [simp, intro!]: "finite (dom (lookup t))"
   1.127 +proof (induct t)
   1.128 +  case Empty then show ?case by simp
   1.129 +next
   1.130 +  case (Branch color t1 a b t2)
   1.131 +  let ?A = "Set.insert a (dom (lookup t1) \<union> dom (lookup t2))"
   1.132 +  have "dom (lookup (Branch color t1 a b t2)) \<subseteq> ?A" by (auto split: split_if_asm)
   1.133 +  moreover from Branch have "finite (insert a (dom (lookup t1) \<union> dom (lookup t2)))" by simp
   1.134 +  ultimately show ?case by (rule finite_subset)
   1.135 +qed 
   1.136 +
   1.137  lemma lookup_tree_less[simp]: "t |\<guillemotleft> k \<Longrightarrow> lookup t k = None" 
   1.138  by (induct t) auto
   1.139  
   1.140  lemma lookup_tree_greater[simp]: "k \<guillemotleft>| t \<Longrightarrow> lookup t k = None"
   1.141  by (induct t) auto
   1.142  
   1.143 -lemma lookup_keys: "sorted t \<Longrightarrow> dom (lookup t) = keys t"
   1.144 -by (induct t) (auto simp: dom_def tree_greater_prop tree_less_prop)
   1.145 -
   1.146 -lemma lookup_pit: "sorted t \<Longrightarrow> (lookup t k = Some v) = entry_in_tree k v t"
   1.147 +lemma lookup_in_tree: "sorted t \<Longrightarrow> (lookup t k = Some v) = entry_in_tree k v t"
   1.148  by (induct t) (auto simp: tree_less_prop tree_greater_prop entry_in_tree_keys)
   1.149  
   1.150  lemma lookup_Empty: "lookup Empty = empty"
   1.151  by (rule ext) simp
   1.152  
   1.153 +lemma lookup_map_of_entries:
   1.154 +  "sorted t \<Longrightarrow> lookup t = map_of (entries t)"
   1.155 +proof (induct t)
   1.156 +  case Empty thus ?case by (simp add: lookup_Empty)
   1.157 +next
   1.158 +  case (Branch c t1 k v t2)
   1.159 +  have "lookup (Branch c t1 k v t2) = lookup t2 ++ [k\<mapsto>v] ++ lookup t1"
   1.160 +  proof (rule ext)
   1.161 +    fix x
   1.162 +    from Branch have SORTED: "sorted (Branch c t1 k v t2)" by simp
   1.163 +    let ?thesis = "lookup (Branch c t1 k v t2) x = (lookup t2 ++ [k \<mapsto> v] ++ lookup t1) x"
   1.164 +
   1.165 +    have DOM_T1: "!!k'. k'\<in>dom (lookup t1) \<Longrightarrow> k>k'"
   1.166 +    proof -
   1.167 +      fix k'
   1.168 +      from SORTED have "t1 |\<guillemotleft> k" by simp
   1.169 +      with tree_less_prop have "\<forall>k'\<in>set (keys t1). k>k'" by auto
   1.170 +      moreover assume "k'\<in>dom (lookup t1)"
   1.171 +      ultimately show "k>k'" using lookup_keys SORTED by auto
   1.172 +    qed
   1.173 +    
   1.174 +    have DOM_T2: "!!k'. k'\<in>dom (lookup t2) \<Longrightarrow> k<k'"
   1.175 +    proof -
   1.176 +      fix k'
   1.177 +      from SORTED have "k \<guillemotleft>| t2" by simp
   1.178 +      with tree_greater_prop have "\<forall>k'\<in>set (keys t2). k<k'" by auto
   1.179 +      moreover assume "k'\<in>dom (lookup t2)"
   1.180 +      ultimately show "k<k'" using lookup_keys SORTED by auto
   1.181 +    qed
   1.182 +    
   1.183 +    {
   1.184 +      assume C: "x<k"
   1.185 +      hence "lookup (Branch c t1 k v t2) x = lookup t1 x" by simp
   1.186 +      moreover from C have "x\<notin>dom [k\<mapsto>v]" by simp
   1.187 +      moreover have "x\<notin>dom (lookup t2)" proof
   1.188 +        assume "x\<in>dom (lookup t2)"
   1.189 +        with DOM_T2 have "k<x" by blast
   1.190 +        with C show False by simp
   1.191 +      qed
   1.192 +      ultimately have ?thesis by (simp add: map_add_upd_left map_add_dom_app_simps)
   1.193 +    } moreover {
   1.194 +      assume [simp]: "x=k"
   1.195 +      hence "lookup (Branch c t1 k v t2) x = [k \<mapsto> v] x" by simp
   1.196 +      moreover have "x\<notin>dom (lookup t1)" proof
   1.197 +        assume "x\<in>dom (lookup t1)"
   1.198 +        with DOM_T1 have "k>x" by blast
   1.199 +        thus False by simp
   1.200 +      qed
   1.201 +      ultimately have ?thesis by (simp add: map_add_upd_left map_add_dom_app_simps)
   1.202 +    } moreover {
   1.203 +      assume C: "x>k"
   1.204 +      hence "lookup (Branch c t1 k v t2) x = lookup t2 x" by (simp add: less_not_sym[of k x])
   1.205 +      moreover from C have "x\<notin>dom [k\<mapsto>v]" by simp
   1.206 +      moreover have "x\<notin>dom (lookup t1)" proof
   1.207 +        assume "x\<in>dom (lookup t1)"
   1.208 +        with DOM_T1 have "k>x" by simp
   1.209 +        with C show False by simp
   1.210 +      qed
   1.211 +      ultimately have ?thesis by (simp add: map_add_upd_left map_add_dom_app_simps)
   1.212 +    } ultimately show ?thesis using less_linear by blast
   1.213 +  qed
   1.214 +  also from Branch have "lookup t2 ++ [k \<mapsto> v] ++ lookup t1 = map_of (entries (Branch c t1 k v t2))" by simp
   1.215 +  finally show ?case .
   1.216 +qed
   1.217 +
   1.218 +(*lemma map_of_inject:
   1.219 +  assumes distinct: "distinct (map fst xs)" "distinct (map fst ys)"
   1.220 +  shows "map_of xs = map_of ys \<longleftrightarrow> set xs = set ys"
   1.221 +
   1.222 +lemma entries_eqI:
   1.223 +  assumes sorted: "sorted t1" "sorted t2" 
   1.224 +  assumes lookup: "lookup t1 = lookup t2"
   1.225 +  shows entries: "entries t1 = entries t2"
   1.226 +proof -
   1.227 +  from sorted lookup have "map_of (entries t1) = map_of (entries t2)"
   1.228 +    by (simp_all add: lookup_map_of_entries)
   1.229 +qed*)
   1.230 +
   1.231  (* a kind of extensionality *)
   1.232 -lemma lookup_from_pit: 
   1.233 +lemma lookup_from_in_tree: 
   1.234    assumes sorted: "sorted t1" "sorted t2" 
   1.235    and eq: "\<And>v. entry_in_tree (k\<Colon>'a\<Colon>linorder) v t1 = entry_in_tree k v t2" 
   1.236    shows "lookup t1 k = lookup t2 k"
   1.237  proof (cases "lookup t1 k")
   1.238    case None
   1.239    then have "\<And>v. \<not> entry_in_tree k v t1"
   1.240 -    by (simp add: lookup_pit[symmetric] sorted)
   1.241 +    by (simp add: lookup_in_tree[symmetric] sorted)
   1.242    with None show ?thesis
   1.243 -    by (cases "lookup t2 k") (auto simp: lookup_pit sorted eq)
   1.244 +    by (cases "lookup t2 k") (auto simp: lookup_in_tree sorted eq)
   1.245  next
   1.246    case (Some a)
   1.247    then show ?thesis
   1.248      apply (cases "lookup t2 k")
   1.249 -    apply (auto simp: lookup_pit sorted eq)
   1.250 -    by (auto simp add: lookup_pit[symmetric] sorted Some)
   1.251 +    apply (auto simp: lookup_in_tree sorted eq)
   1.252 +    by (auto simp add: lookup_in_tree[symmetric] sorted Some)
   1.253  qed
   1.254  
   1.255 -subsection {* Red-black properties *}
   1.256 +
   1.257 +subsubsection {* Red-black properties *}
   1.258  
   1.259  primrec color_of :: "('a, 'b) rbt \<Rightarrow> color"
   1.260  where
   1.261 @@ -240,19 +368,23 @@
   1.262    with 1 "5_4" show ?case by simp
   1.263  qed simp+
   1.264  
   1.265 -lemma keys_balance[simp]: 
   1.266 -  "keys (balance l k v r) = { k } \<union> keys l \<union> keys r"
   1.267 -by (induct l k v r rule: balance.induct) auto
   1.268 +lemma entries_balance [simp]:
   1.269 +  "entries (balance l k v r) = entries l @ (k, v) # entries r"
   1.270 +  by (induct l k v r rule: balance.induct) auto
   1.271  
   1.272 -lemma balance_pit:  
   1.273 -  "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)" 
   1.274 -by (induct l v y r rule: balance.induct) auto
   1.275 +lemma keys_balance [simp]: 
   1.276 +  "keys (balance l k v r) = keys l @ k # keys r"
   1.277 +  by (simp add: keys_def)
   1.278 +
   1.279 +lemma balance_in_tree:  
   1.280 +  "entry_in_tree k x (balance l v y r) \<longleftrightarrow> entry_in_tree k x l \<or> k = v \<and> x = y \<or> entry_in_tree k x r"
   1.281 +  by (auto simp add: keys_def)
   1.282  
   1.283  lemma lookup_balance[simp]: 
   1.284  fixes k :: "'a::linorder"
   1.285  assumes "sorted l" "sorted r" "l |\<guillemotleft> k" "k \<guillemotleft>| r"
   1.286  shows "lookup (balance l k v r) x = lookup (Branch B l k v r) x"
   1.287 -by (rule lookup_from_pit) (auto simp:assms balance_pit balance_sorted)
   1.288 +by (rule lookup_from_in_tree) (auto simp:assms balance_in_tree balance_sorted)
   1.289  
   1.290  primrec paint :: "color \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
   1.291  where
   1.292 @@ -264,7 +396,7 @@
   1.293  lemma paint_inv2[simp]: "inv2 t \<Longrightarrow> inv2 (paint c t)" by (cases t) auto
   1.294  lemma paint_color_of[simp]: "color_of (paint B t) = B" by (cases t) auto
   1.295  lemma paint_sorted[simp]: "sorted t \<Longrightarrow> sorted (paint c t)" by (cases t) auto
   1.296 -lemma paint_pit[simp]: "entry_in_tree k x (paint c t) = entry_in_tree k x t" by (cases t) auto
   1.297 +lemma paint_in_tree[simp]: "entry_in_tree k x (paint c t) = entry_in_tree k x t" by (cases t) auto
   1.298  lemma paint_lookup[simp]: "lookup (paint c t) = lookup t" by (rule ext) (cases t, auto)
   1.299  lemma paint_tree_greater[simp]: "(v \<guillemotleft>| paint c t) = (v \<guillemotleft>| t)" by (cases t) auto
   1.300  lemma paint_tree_less[simp]: "(paint c t |\<guillemotleft> v) = (t |\<guillemotleft> v)" by (cases t) auto
   1.301 @@ -294,8 +426,8 @@
   1.302  lemma ins_sorted[simp]: "sorted t \<Longrightarrow> sorted (ins f k x t)"
   1.303    by (induct f k x t rule: ins.induct) (auto simp: balance_sorted)
   1.304  
   1.305 -lemma keys_ins: "keys (ins f k v t) = { k } \<union> keys t"
   1.306 -by (induct f k v t rule: ins.induct) auto
   1.307 +lemma keys_ins: "set (keys (ins f k v t)) = { k } \<union> set (keys t)"
   1.308 +  by (induct f k v t rule: ins.induct) auto
   1.309  
   1.310  lemma lookup_ins: 
   1.311    fixes k :: "'a::linorder"
   1.312 @@ -305,45 +437,45 @@
   1.313  using assms by (induct f k v t rule: ins.induct) auto
   1.314  
   1.315  definition
   1.316 -  insertwithkey :: "('a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
   1.317 +  insert_with_key :: "('a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
   1.318  where
   1.319 -  "insertwithkey f k v t = paint B (ins f k v t)"
   1.320 +  "insert_with_key f k v t = paint B (ins f k v t)"
   1.321  
   1.322 -lemma insertwk_sorted: "sorted t \<Longrightarrow> sorted (insertwithkey f k x t)"
   1.323 -  by (auto simp: insertwithkey_def)
   1.324 +lemma insertwk_sorted: "sorted t \<Longrightarrow> sorted (insert_with_key f k x t)"
   1.325 +  by (auto simp: insert_with_key_def)
   1.326  
   1.327  theorem insertwk_is_rbt: 
   1.328    assumes inv: "is_rbt t" 
   1.329 -  shows "is_rbt (insertwithkey f k x t)"
   1.330 +  shows "is_rbt (insert_with_key f k x t)"
   1.331  using assms
   1.332 -unfolding insertwithkey_def is_rbt_def
   1.333 +unfolding insert_with_key_def is_rbt_def
   1.334  by (auto simp: ins_inv1_inv2)
   1.335  
   1.336  lemma lookup_insertwk: 
   1.337    assumes "sorted t"
   1.338 -  shows "lookup (insertwithkey f k v t) x = ((lookup t)(k |-> case lookup t k of None \<Rightarrow> v 
   1.339 +  shows "lookup (insert_with_key f k v t) x = ((lookup t)(k |-> case lookup t k of None \<Rightarrow> v 
   1.340                                                         | Some w \<Rightarrow> f k w v)) x"
   1.341 -unfolding insertwithkey_def using assms
   1.342 +unfolding insert_with_key_def using assms
   1.343  by (simp add:lookup_ins)
   1.344  
   1.345  definition
   1.346 -  insertw_def: "insertwith f = insertwithkey (\<lambda>_. f)"
   1.347 +  insertw_def: "insert_with f = insert_with_key (\<lambda>_. f)"
   1.348  
   1.349 -lemma insertw_sorted: "sorted t \<Longrightarrow> sorted (insertwith f k v t)" by (simp add: insertwk_sorted insertw_def)
   1.350 -theorem insertw_is_rbt: "is_rbt t \<Longrightarrow> is_rbt (insertwith f k v t)" by (simp add: insertwk_is_rbt insertw_def)
   1.351 +lemma insertw_sorted: "sorted t \<Longrightarrow> sorted (insert_with f k v t)" by (simp add: insertwk_sorted insertw_def)
   1.352 +theorem insertw_is_rbt: "is_rbt t \<Longrightarrow> is_rbt (insert_with f k v t)" by (simp add: insertwk_is_rbt insertw_def)
   1.353  
   1.354  lemma lookup_insertw:
   1.355    assumes "is_rbt t"
   1.356 -  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))"
   1.357 +  shows "lookup (insert_with f k v t) = (lookup t)(k \<mapsto> (if k:dom (lookup t) then f (the (lookup t k)) v else v))"
   1.358  using assms
   1.359  unfolding insertw_def
   1.360  by (rule_tac ext) (cases "lookup t k", auto simp:lookup_insertwk dom_def)
   1.361  
   1.362  definition insert :: "'a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" where
   1.363 -  "insert k v t = insertwithkey (\<lambda>_ _ nv. nv) k v t"
   1.364 +  "insert = insert_with_key (\<lambda>_ _ nv. nv)"
   1.365  
   1.366  lemma insert_sorted: "sorted t \<Longrightarrow> sorted (insert k v t)" by (simp add: insertwk_sorted insert_def)
   1.367 -theorem insert_is_rbt: "is_rbt t \<Longrightarrow> is_rbt (insert k v t)" by (simp add: insertwk_is_rbt insert_def)
   1.368 +theorem insert_is_rbt [simp]: "is_rbt t \<Longrightarrow> is_rbt (insert k v t)" by (simp add: insertwk_is_rbt insert_def)
   1.369  
   1.370  lemma lookup_insert: 
   1.371    assumes "is_rbt t"
   1.372 @@ -359,178 +491,174 @@
   1.373  by (cases t rule: rbt_cases) auto
   1.374  
   1.375  fun
   1.376 -  balleft :: "('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
   1.377 +  balance_left :: "('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
   1.378  where
   1.379 -  "balleft (Branch R a k x b) s y c = Branch R (Branch B a k x b) s y c" |
   1.380 -  "balleft bl k x (Branch B a s y b) = balance bl k x (Branch R a s y b)" |
   1.381 -  "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))" |
   1.382 -  "balleft t k x s = Empty"
   1.383 +  "balance_left (Branch R a k x b) s y c = Branch R (Branch B a k x b) s y c" |
   1.384 +  "balance_left bl k x (Branch B a s y b) = balance bl k x (Branch R a s y b)" |
   1.385 +  "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))" |
   1.386 +  "balance_left t k x s = Empty"
   1.387  
   1.388 -lemma balleft_inv2_with_inv1:
   1.389 +lemma balance_left_inv2_with_inv1:
   1.390    assumes "inv2 lt" "inv2 rt" "bheight lt + 1 = bheight rt" "inv1 rt"
   1.391 -  shows "bheight (balleft lt k v rt) = bheight lt + 1"
   1.392 -  and   "inv2 (balleft lt k v rt)"
   1.393 +  shows "bheight (balance_left lt k v rt) = bheight lt + 1"
   1.394 +  and   "inv2 (balance_left lt k v rt)"
   1.395  using assms 
   1.396 -by (induct lt k v rt rule: balleft.induct) (auto simp: balance_inv2 balance_bheight)
   1.397 +by (induct lt k v rt rule: balance_left.induct) (auto simp: balance_inv2 balance_bheight)
   1.398  
   1.399 -lemma balleft_inv2_app: 
   1.400 +lemma balance_left_inv2_app: 
   1.401    assumes "inv2 lt" "inv2 rt" "bheight lt + 1 = bheight rt" "color_of rt = B"
   1.402 -  shows "inv2 (balleft lt k v rt)" 
   1.403 -        "bheight (balleft lt k v rt) = bheight rt"
   1.404 +  shows "inv2 (balance_left lt k v rt)" 
   1.405 +        "bheight (balance_left lt k v rt) = bheight rt"
   1.406  using assms 
   1.407 -by (induct lt k v rt rule: balleft.induct) (auto simp add: balance_inv2 balance_bheight)+ 
   1.408 +by (induct lt k v rt rule: balance_left.induct) (auto simp add: balance_inv2 balance_bheight)+ 
   1.409  
   1.410 -lemma balleft_inv1: "\<lbrakk>inv1l a; inv1 b; color_of b = B\<rbrakk> \<Longrightarrow> inv1 (balleft a k x b)"
   1.411 -  by (induct a k x b rule: balleft.induct) (simp add: balance_inv1)+
   1.412 +lemma balance_left_inv1: "\<lbrakk>inv1l a; inv1 b; color_of b = B\<rbrakk> \<Longrightarrow> inv1 (balance_left a k x b)"
   1.413 +  by (induct a k x b rule: balance_left.induct) (simp add: balance_inv1)+
   1.414  
   1.415 -lemma balleft_inv1l: "\<lbrakk> inv1l lt; inv1 rt \<rbrakk> \<Longrightarrow> inv1l (balleft lt k x rt)"
   1.416 -by (induct lt k x rt rule: balleft.induct) (auto simp: balance_inv1)
   1.417 +lemma balance_left_inv1l: "\<lbrakk> inv1l lt; inv1 rt \<rbrakk> \<Longrightarrow> inv1l (balance_left lt k x rt)"
   1.418 +by (induct lt k x rt rule: balance_left.induct) (auto simp: balance_inv1)
   1.419  
   1.420 -lemma balleft_sorted: "\<lbrakk> sorted l; sorted r; tree_less k l; tree_greater k r \<rbrakk> \<Longrightarrow> sorted (balleft l k v r)"
   1.421 -apply (induct l k v r rule: balleft.induct)
   1.422 +lemma balance_left_sorted: "\<lbrakk> sorted l; sorted r; tree_less k l; tree_greater k r \<rbrakk> \<Longrightarrow> sorted (balance_left l k v r)"
   1.423 +apply (induct l k v r rule: balance_left.induct)
   1.424  apply (auto simp: balance_sorted)
   1.425  apply (unfold tree_greater_prop tree_less_prop)
   1.426  by force+
   1.427  
   1.428 -lemma balleft_tree_greater: 
   1.429 +lemma balance_left_tree_greater: 
   1.430    fixes k :: "'a::order"
   1.431    assumes "k \<guillemotleft>| a" "k \<guillemotleft>| b" "k < x" 
   1.432 -  shows "k \<guillemotleft>| balleft a x t b"
   1.433 +  shows "k \<guillemotleft>| balance_left a x t b"
   1.434  using assms 
   1.435 -by (induct a x t b rule: balleft.induct) auto
   1.436 +by (induct a x t b rule: balance_left.induct) auto
   1.437  
   1.438 -lemma balleft_tree_less: 
   1.439 +lemma balance_left_tree_less: 
   1.440    fixes k :: "'a::order"
   1.441    assumes "a |\<guillemotleft> k" "b |\<guillemotleft> k" "x < k" 
   1.442 -  shows "balleft a x t b |\<guillemotleft> k"
   1.443 +  shows "balance_left a x t b |\<guillemotleft> k"
   1.444  using assms
   1.445 -by (induct a x t b rule: balleft.induct) auto
   1.446 +by (induct a x t b rule: balance_left.induct) auto
   1.447  
   1.448 -lemma balleft_pit: 
   1.449 +lemma balance_left_in_tree: 
   1.450    assumes "inv1l l" "inv1 r" "bheight l + 1 = bheight r"
   1.451 -  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)"
   1.452 +  shows "entry_in_tree k v (balance_left l a b r) = (entry_in_tree k v l \<or> k = a \<and> v = b \<or> entry_in_tree k v r)"
   1.453  using assms 
   1.454 -by (induct l k v r rule: balleft.induct) (auto simp: balance_pit)
   1.455 +by (induct l k v r rule: balance_left.induct) (auto simp: balance_in_tree)
   1.456  
   1.457  fun
   1.458 -  balright :: "('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
   1.459 +  balance_right :: "('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
   1.460  where
   1.461 -  "balright a k x (Branch R b s y c) = Branch R a k x (Branch B b s y c)" |
   1.462 -  "balright (Branch B a k x b) s y bl = balance (Branch R a k x b) s y bl" |
   1.463 -  "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)" |
   1.464 -  "balright t k x s = Empty"
   1.465 +  "balance_right a k x (Branch R b s y c) = Branch R a k x (Branch B b s y c)" |
   1.466 +  "balance_right (Branch B a k x b) s y bl = balance (Branch R a k x b) s y bl" |
   1.467 +  "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)" |
   1.468 +  "balance_right t k x s = Empty"
   1.469  
   1.470 -lemma balright_inv2_with_inv1:
   1.471 +lemma balance_right_inv2_with_inv1:
   1.472    assumes "inv2 lt" "inv2 rt" "bheight lt = bheight rt + 1" "inv1 lt"
   1.473 -  shows "inv2 (balright lt k v rt) \<and> bheight (balright lt k v rt) = bheight lt"
   1.474 +  shows "inv2 (balance_right lt k v rt) \<and> bheight (balance_right lt k v rt) = bheight lt"
   1.475  using assms
   1.476 -by (induct lt k v rt rule: balright.induct) (auto simp: balance_inv2 balance_bheight)
   1.477 +by (induct lt k v rt rule: balance_right.induct) (auto simp: balance_inv2 balance_bheight)
   1.478  
   1.479 -lemma balright_inv1: "\<lbrakk>inv1 a; inv1l b; color_of a = B\<rbrakk> \<Longrightarrow> inv1 (balright a k x b)"
   1.480 -by (induct a k x b rule: balright.induct) (simp add: balance_inv1)+
   1.481 +lemma balance_right_inv1: "\<lbrakk>inv1 a; inv1l b; color_of a = B\<rbrakk> \<Longrightarrow> inv1 (balance_right a k x b)"
   1.482 +by (induct a k x b rule: balance_right.induct) (simp add: balance_inv1)+
   1.483  
   1.484 -lemma balright_inv1l: "\<lbrakk> inv1 lt; inv1l rt \<rbrakk> \<Longrightarrow>inv1l (balright lt k x rt)"
   1.485 -by (induct lt k x rt rule: balright.induct) (auto simp: balance_inv1)
   1.486 +lemma balance_right_inv1l: "\<lbrakk> inv1 lt; inv1l rt \<rbrakk> \<Longrightarrow>inv1l (balance_right lt k x rt)"
   1.487 +by (induct lt k x rt rule: balance_right.induct) (auto simp: balance_inv1)
   1.488  
   1.489 -lemma balright_sorted: "\<lbrakk> sorted l; sorted r; tree_less k l; tree_greater k r \<rbrakk> \<Longrightarrow> sorted (balright l k v r)"
   1.490 -apply (induct l k v r rule: balright.induct)
   1.491 +lemma balance_right_sorted: "\<lbrakk> sorted l; sorted r; tree_less k l; tree_greater k r \<rbrakk> \<Longrightarrow> sorted (balance_right l k v r)"
   1.492 +apply (induct l k v r rule: balance_right.induct)
   1.493  apply (auto simp:balance_sorted)
   1.494  apply (unfold tree_less_prop tree_greater_prop)
   1.495  by force+
   1.496  
   1.497 -lemma balright_tree_greater: 
   1.498 +lemma balance_right_tree_greater: 
   1.499    fixes k :: "'a::order"
   1.500    assumes "k \<guillemotleft>| a" "k \<guillemotleft>| b" "k < x" 
   1.501 -  shows "k \<guillemotleft>| balright a x t b"
   1.502 -using assms by (induct a x t b rule: balright.induct) auto
   1.503 +  shows "k \<guillemotleft>| balance_right a x t b"
   1.504 +using assms by (induct a x t b rule: balance_right.induct) auto
   1.505  
   1.506 -lemma balright_tree_less: 
   1.507 +lemma balance_right_tree_less: 
   1.508    fixes k :: "'a::order"
   1.509    assumes "a |\<guillemotleft> k" "b |\<guillemotleft> k" "x < k" 
   1.510 -  shows "balright a x t b |\<guillemotleft> k"
   1.511 -using assms by (induct a x t b rule: balright.induct) auto
   1.512 +  shows "balance_right a x t b |\<guillemotleft> k"
   1.513 +using assms by (induct a x t b rule: balance_right.induct) auto
   1.514  
   1.515 -lemma balright_pit:
   1.516 +lemma balance_right_in_tree:
   1.517    assumes "inv1 l" "inv1l r" "bheight l = bheight r + 1" "inv2 l" "inv2 r"
   1.518 -  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)"
   1.519 -using assms by (induct l k v r rule: balright.induct) (auto simp: balance_pit)
   1.520 -
   1.521 -
   1.522 -text {* app *}
   1.523 +  shows "entry_in_tree x y (balance_right l k v r) = (entry_in_tree x y l \<or> x = k \<and> y = v \<or> entry_in_tree x y r)"
   1.524 +using assms by (induct l k v r rule: balance_right.induct) (auto simp: balance_in_tree)
   1.525  
   1.526  fun
   1.527 -  app :: "('a,'b) rbt \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
   1.528 +  combine :: "('a,'b) rbt \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
   1.529  where
   1.530 -  "app Empty x = x" 
   1.531 -| "app x Empty = x" 
   1.532 -| "app (Branch R a k x b) (Branch R c s y d) = (case (app b c) of
   1.533 +  "combine Empty x = x" 
   1.534 +| "combine x Empty = x" 
   1.535 +| "combine (Branch R a k x b) (Branch R c s y d) = (case (combine b c) of
   1.536                                        Branch R b2 t z c2 \<Rightarrow> (Branch R (Branch R a k x b2) t z (Branch R c2 s y d)) |
   1.537                                        bc \<Rightarrow> Branch R a k x (Branch R bc s y d))" 
   1.538 -| "app (Branch B a k x b) (Branch B c s y d) = (case (app b c) of
   1.539 +| "combine (Branch B a k x b) (Branch B c s y d) = (case (combine b c) of
   1.540                                        Branch R b2 t z c2 \<Rightarrow> Branch R (Branch B a k x b2) t z (Branch B c2 s y d) |
   1.541 -                                      bc \<Rightarrow> balleft a k x (Branch B bc s y d))" 
   1.542 -| "app a (Branch R b k x c) = Branch R (app a b) k x c" 
   1.543 -| "app (Branch R a k x b) c = Branch R a k x (app b c)" 
   1.544 +                                      bc \<Rightarrow> balance_left a k x (Branch B bc s y d))" 
   1.545 +| "combine a (Branch R b k x c) = Branch R (combine a b) k x c" 
   1.546 +| "combine (Branch R a k x b) c = Branch R a k x (combine b c)" 
   1.547  
   1.548 -lemma app_inv2:
   1.549 +lemma combine_inv2:
   1.550    assumes "inv2 lt" "inv2 rt" "bheight lt = bheight rt"
   1.551 -  shows "bheight (app lt rt) = bheight lt" "inv2 (app lt rt)"
   1.552 +  shows "bheight (combine lt rt) = bheight lt" "inv2 (combine lt rt)"
   1.553  using assms 
   1.554 -by (induct lt rt rule: app.induct) 
   1.555 -   (auto simp: balleft_inv2_app split: rbt.splits color.splits)
   1.556 +by (induct lt rt rule: combine.induct) 
   1.557 +   (auto simp: balance_left_inv2_app split: rbt.splits color.splits)
   1.558  
   1.559 -lemma app_inv1: 
   1.560 +lemma combine_inv1: 
   1.561    assumes "inv1 lt" "inv1 rt"
   1.562 -  shows "color_of lt = B \<Longrightarrow> color_of rt = B \<Longrightarrow> inv1 (app lt rt)"
   1.563 -         "inv1l (app lt rt)"
   1.564 +  shows "color_of lt = B \<Longrightarrow> color_of rt = B \<Longrightarrow> inv1 (combine lt rt)"
   1.565 +         "inv1l (combine lt rt)"
   1.566  using assms 
   1.567 -by (induct lt rt rule: app.induct)
   1.568 -   (auto simp: balleft_inv1 split: rbt.splits color.splits)
   1.569 +by (induct lt rt rule: combine.induct)
   1.570 +   (auto simp: balance_left_inv1 split: rbt.splits color.splits)
   1.571  
   1.572 -lemma app_tree_greater[simp]: 
   1.573 +lemma combine_tree_greater[simp]: 
   1.574    fixes k :: "'a::linorder"
   1.575    assumes "k \<guillemotleft>| l" "k \<guillemotleft>| r" 
   1.576 -  shows "k \<guillemotleft>| app l r"
   1.577 +  shows "k \<guillemotleft>| combine l r"
   1.578  using assms 
   1.579 -by (induct l r rule: app.induct)
   1.580 -   (auto simp: balleft_tree_greater split:rbt.splits color.splits)
   1.581 +by (induct l r rule: combine.induct)
   1.582 +   (auto simp: balance_left_tree_greater split:rbt.splits color.splits)
   1.583  
   1.584 -lemma app_tree_less[simp]: 
   1.585 +lemma combine_tree_less[simp]: 
   1.586    fixes k :: "'a::linorder"
   1.587    assumes "l |\<guillemotleft> k" "r |\<guillemotleft> k" 
   1.588 -  shows "app l r |\<guillemotleft> k"
   1.589 +  shows "combine l r |\<guillemotleft> k"
   1.590  using assms 
   1.591 -by (induct l r rule: app.induct)
   1.592 -   (auto simp: balleft_tree_less split:rbt.splits color.splits)
   1.593 +by (induct l r rule: combine.induct)
   1.594 +   (auto simp: balance_left_tree_less split:rbt.splits color.splits)
   1.595  
   1.596 -lemma app_sorted: 
   1.597 +lemma combine_sorted: 
   1.598    fixes k :: "'a::linorder"
   1.599    assumes "sorted l" "sorted r" "l |\<guillemotleft> k" "k \<guillemotleft>| r"
   1.600 -  shows "sorted (app l r)"
   1.601 -using assms proof (induct l r rule: app.induct)
   1.602 +  shows "sorted (combine l r)"
   1.603 +using assms proof (induct l r rule: combine.induct)
   1.604    case (3 a x v b c y w d)
   1.605    hence ineqs: "a |\<guillemotleft> x" "x \<guillemotleft>| b" "b |\<guillemotleft> k" "k \<guillemotleft>| c" "c |\<guillemotleft> y" "y \<guillemotleft>| d"
   1.606      by auto
   1.607    with 3
   1.608    show ?case
   1.609 -    apply (cases "app b c" rule: rbt_cases)
   1.610 -    apply auto
   1.611 -    by (metis app_tree_greater app_tree_less ineqs ineqs tree_less_simps(2) tree_greater_simps(2) tree_greater_trans tree_less_trans)+
   1.612 +    by (cases "combine b c" rule: rbt_cases)
   1.613 +      (auto, (metis combine_tree_greater combine_tree_less ineqs ineqs tree_less_simps(2) tree_greater_simps(2) tree_greater_trans tree_less_trans)+)
   1.614  next
   1.615    case (4 a x v b c y w d)
   1.616    hence "x < k \<and> tree_greater k c" by simp
   1.617    hence "tree_greater x c" by (blast dest: tree_greater_trans)
   1.618 -  with 4 have 2: "tree_greater x (app b c)" by (simp add: app_tree_greater)
   1.619 +  with 4 have 2: "tree_greater x (combine b c)" by (simp add: combine_tree_greater)
   1.620    from 4 have "k < y \<and> tree_less k b" by simp
   1.621    hence "tree_less y b" by (blast dest: tree_less_trans)
   1.622 -  with 4 have 3: "tree_less y (app b c)" by (simp add: app_tree_less)
   1.623 +  with 4 have 3: "tree_less y (combine b c)" by (simp add: combine_tree_less)
   1.624    show ?case
   1.625 -  proof (cases "app b c" rule: rbt_cases)
   1.626 +  proof (cases "combine b c" rule: rbt_cases)
   1.627      case Empty
   1.628      from 4 have "x < y \<and> tree_greater y d" by auto
   1.629      hence "tree_greater x d" by (blast dest: tree_greater_trans)
   1.630      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
   1.631 -    with Empty show ?thesis by (simp add: balleft_sorted)
   1.632 +    with Empty show ?thesis by (simp add: balance_left_sorted)
   1.633    next
   1.634      case (Red lta va ka rta)
   1.635      with 2 4 have "x < va \<and> tree_less x a" by simp
   1.636 @@ -542,71 +670,71 @@
   1.637      case (Black lta va ka rta)
   1.638      from 4 have "x < y \<and> tree_greater y d" by auto
   1.639      hence "tree_greater x d" by (blast dest: tree_greater_trans)
   1.640 -    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
   1.641 -    with Black show ?thesis by (simp add: balleft_sorted)
   1.642 +    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
   1.643 +    with Black show ?thesis by (simp add: balance_left_sorted)
   1.644    qed
   1.645  next
   1.646    case (5 va vb vd vc b x w c)
   1.647    hence "k < x \<and> tree_less k (Branch B va vb vd vc)" by simp
   1.648    hence "tree_less x (Branch B va vb vd vc)" by (blast dest: tree_less_trans)
   1.649 -  with 5 show ?case by (simp add: app_tree_less)
   1.650 +  with 5 show ?case by (simp add: combine_tree_less)
   1.651  next
   1.652    case (6 a x v b va vb vd vc)
   1.653    hence "x < k \<and> tree_greater k (Branch B va vb vd vc)" by simp
   1.654    hence "tree_greater x (Branch B va vb vd vc)" by (blast dest: tree_greater_trans)
   1.655 -  with 6 show ?case by (simp add: app_tree_greater)
   1.656 +  with 6 show ?case by (simp add: combine_tree_greater)
   1.657  qed simp+
   1.658  
   1.659 -lemma app_pit: 
   1.660 +lemma combine_in_tree: 
   1.661    assumes "inv2 l" "inv2 r" "bheight l = bheight r" "inv1 l" "inv1 r"
   1.662 -  shows "entry_in_tree k v (app l r) = (entry_in_tree k v l \<or> entry_in_tree k v r)"
   1.663 +  shows "entry_in_tree k v (combine l r) = (entry_in_tree k v l \<or> entry_in_tree k v r)"
   1.664  using assms 
   1.665 -proof (induct l r rule: app.induct)
   1.666 +proof (induct l r rule: combine.induct)
   1.667    case (4 _ _ _ b c)
   1.668 -  hence a: "bheight (app b c) = bheight b" by (simp add: app_inv2)
   1.669 -  from 4 have b: "inv1l (app b c)" by (simp add: app_inv1)
   1.670 +  hence a: "bheight (combine b c) = bheight b" by (simp add: combine_inv2)
   1.671 +  from 4 have b: "inv1l (combine b c)" by (simp add: combine_inv1)
   1.672  
   1.673    show ?case
   1.674 -  proof (cases "app b c" rule: rbt_cases)
   1.675 +  proof (cases "combine b c" rule: rbt_cases)
   1.676      case Empty
   1.677 -    with 4 a show ?thesis by (auto simp: balleft_pit)
   1.678 +    with 4 a show ?thesis by (auto simp: balance_left_in_tree)
   1.679    next
   1.680      case (Red lta ka va rta)
   1.681      with 4 show ?thesis by auto
   1.682    next
   1.683      case (Black lta ka va rta)
   1.684 -    with a b 4  show ?thesis by (auto simp: balleft_pit)
   1.685 +    with a b 4  show ?thesis by (auto simp: balance_left_in_tree)
   1.686    qed 
   1.687  qed (auto split: rbt.splits color.splits)
   1.688  
   1.689  fun
   1.690 -  delformLeft :: "('a\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" and
   1.691 -  delformRight :: "('a\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" and
   1.692 +  del_from_left :: "('a\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" and
   1.693 +  del_from_right :: "('a\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" and
   1.694    del :: "('a\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
   1.695  where
   1.696    "del x Empty = Empty" |
   1.697 -  "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))" |
   1.698 -  "delformLeft x (Branch B lt z v rt) y s b = balleft (del x (Branch B lt z v rt)) y s b" |
   1.699 -  "delformLeft x a y s b = Branch R (del x a) y s b" |
   1.700 -  "delformRight x a y s (Branch B lt z v rt) = balright a y s (del x (Branch B lt z v rt))" | 
   1.701 -  "delformRight x a y s b = Branch R a y s (del x b)"
   1.702 +  "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))" |
   1.703 +  "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" |
   1.704 +  "del_from_left x a y s b = Branch R (del x a) y s b" |
   1.705 +  "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))" | 
   1.706 +  "del_from_right x a y s b = Branch R a y s (del x b)"
   1.707  
   1.708  lemma 
   1.709    assumes "inv2 lt" "inv1 lt"
   1.710    shows
   1.711    "\<lbrakk>inv2 rt; bheight lt = bheight rt; inv1 rt\<rbrakk> \<Longrightarrow>
   1.712 -  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))"
   1.713 +  inv2 (del_from_left x lt k v rt) \<and> bheight (del_from_left x lt k v rt) = bheight lt \<and> (color_of lt = B \<and> color_of rt = B \<and> inv1 (del_from_left x lt k v rt) \<or> (color_of lt \<noteq> B \<or> color_of rt \<noteq> B) \<and> inv1l (del_from_left x lt k v rt))"
   1.714    and "\<lbrakk>inv2 rt; bheight lt = bheight rt; inv1 rt\<rbrakk> \<Longrightarrow>
   1.715 -  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))"
   1.716 +  inv2 (del_from_right x lt k v rt) \<and> bheight (del_from_right x lt k v rt) = bheight lt \<and> (color_of lt = B \<and> color_of rt = B \<and> inv1 (del_from_right x lt k v rt) \<or> (color_of lt \<noteq> B \<or> color_of rt \<noteq> B) \<and> inv1l (del_from_right x lt k v rt))"
   1.717    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) 
   1.718    \<or> color_of lt = B \<and> bheight (del x lt) = bheight lt - 1 \<and> inv1l (del x lt))"
   1.719  using assms
   1.720 -proof (induct x lt k v rt and x lt k v rt and x lt rule: delformLeft_delformRight_del.induct)
   1.721 +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)
   1.722  case (2 y c _ y')
   1.723    have "y = y' \<or> y < y' \<or> y > y'" by auto
   1.724    thus ?case proof (elim disjE)
   1.725      assume "y = y'"
   1.726 -    with 2 show ?thesis by (cases c) (simp add: app_inv2 app_inv1)+
   1.727 +    with 2 show ?thesis by (cases c) (simp add: combine_inv2 combine_inv1)+
   1.728    next
   1.729      assume "y < y'"
   1.730      with 2 show ?thesis by (cases c) auto
   1.731 @@ -616,35 +744,35 @@
   1.732    qed
   1.733  next
   1.734    case (3 y lt z v rta y' ss bb) 
   1.735 -  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)+
   1.736 +  thus ?case by (cases "color_of (Branch B lt z v rta) = B \<and> color_of bb = B") (simp add: balance_left_inv2_with_inv1 balance_left_inv1 balance_left_inv1l)+
   1.737  next
   1.738    case (5 y a y' ss lt z v rta)
   1.739 -  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)+
   1.740 +  thus ?case by (cases "color_of a = B \<and> color_of (Branch B lt z v rta) = B") (simp add: balance_right_inv2_with_inv1 balance_right_inv1 balance_right_inv1l)+
   1.741  next
   1.742    case ("6_1" y a y' ss) thus ?case by (cases "color_of a = B \<and> color_of Empty = B") simp+
   1.743  qed auto
   1.744  
   1.745  lemma 
   1.746 -  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)"
   1.747 -  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)"
   1.748 +  del_from_left_tree_less: "\<lbrakk>tree_less v lt; tree_less v rt; k < v\<rbrakk> \<Longrightarrow> tree_less v (del_from_left x lt k y rt)"
   1.749 +  and del_from_right_tree_less: "\<lbrakk>tree_less v lt; tree_less v rt; k < v\<rbrakk> \<Longrightarrow> tree_less v (del_from_right x lt k y rt)"
   1.750    and del_tree_less: "tree_less v lt \<Longrightarrow> tree_less v (del x lt)"
   1.751 -by (induct x lt k y rt and x lt k y rt and x lt rule: delformLeft_delformRight_del.induct) 
   1.752 -   (auto simp: balleft_tree_less balright_tree_less)
   1.753 +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) 
   1.754 +   (auto simp: balance_left_tree_less balance_right_tree_less)
   1.755  
   1.756 -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)"
   1.757 -  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)"
   1.758 +lemma del_from_left_tree_greater: "\<lbrakk>tree_greater v lt; tree_greater v rt; k > v\<rbrakk> \<Longrightarrow> tree_greater v (del_from_left x lt k y rt)"
   1.759 +  and del_from_right_tree_greater: "\<lbrakk>tree_greater v lt; tree_greater v rt; k > v\<rbrakk> \<Longrightarrow> tree_greater v (del_from_right x lt k y rt)"
   1.760    and del_tree_greater: "tree_greater v lt \<Longrightarrow> tree_greater v (del x lt)"
   1.761 -by (induct x lt k y rt and x lt k y rt and x lt rule: delformLeft_delformRight_del.induct)
   1.762 -   (auto simp: balleft_tree_greater balright_tree_greater)
   1.763 +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)
   1.764 +   (auto simp: balance_left_tree_greater balance_right_tree_greater)
   1.765  
   1.766 -lemma "\<lbrakk>sorted lt; sorted rt; tree_less k lt; tree_greater k rt\<rbrakk> \<Longrightarrow> sorted (delformLeft x lt k y rt)"
   1.767 -  and "\<lbrakk>sorted lt; sorted rt; tree_less k lt; tree_greater k rt\<rbrakk> \<Longrightarrow> sorted (delformRight x lt k y rt)"
   1.768 +lemma "\<lbrakk>sorted lt; sorted rt; tree_less k lt; tree_greater k rt\<rbrakk> \<Longrightarrow> sorted (del_from_left x lt k y rt)"
   1.769 +  and "\<lbrakk>sorted lt; sorted rt; tree_less k lt; tree_greater k rt\<rbrakk> \<Longrightarrow> sorted (del_from_right x lt k y rt)"
   1.770    and del_sorted: "sorted lt \<Longrightarrow> sorted (del x lt)"
   1.771 -proof (induct x lt k y rt and x lt k y rt and x lt rule: delformLeft_delformRight_del.induct)
   1.772 +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)
   1.773    case (3 x lta zz v rta yy ss bb)
   1.774    from 3 have "tree_less yy (Branch B lta zz v rta)" by simp
   1.775    hence "tree_less yy (del x (Branch B lta zz v rta))" by (rule del_tree_less)
   1.776 -  with 3 show ?case by (simp add: balleft_sorted)
   1.777 +  with 3 show ?case by (simp add: balance_left_sorted)
   1.778  next
   1.779    case ("4_2" x vaa vbb vdd vc yy ss bb)
   1.780    hence "tree_less yy (Branch R vaa vbb vdd vc)" by simp
   1.781 @@ -654,18 +782,18 @@
   1.782    case (5 x aa yy ss lta zz v rta) 
   1.783    hence "tree_greater yy (Branch B lta zz v rta)" by simp
   1.784    hence "tree_greater yy (del x (Branch B lta zz v rta))" by (rule del_tree_greater)
   1.785 -  with 5 show ?case by (simp add: balright_sorted)
   1.786 +  with 5 show ?case by (simp add: balance_right_sorted)
   1.787  next
   1.788    case ("6_2" x aa yy ss vaa vbb vdd vc)
   1.789    hence "tree_greater yy (Branch R vaa vbb vdd vc)" by simp
   1.790    hence "tree_greater yy (del x (Branch R vaa vbb vdd vc))" by (rule del_tree_greater)
   1.791    with "6_2" show ?case by simp
   1.792 -qed (auto simp: app_sorted)
   1.793 +qed (auto simp: combine_sorted)
   1.794  
   1.795 -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)))"
   1.796 -  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)))"
   1.797 -  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))"
   1.798 -proof (induct x lt kt y rt and x lt kt y rt and x t rule: delformLeft_delformRight_del.induct)
   1.799 +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 (del_from_left x lt kt y rt) = (False \<or> (x \<noteq> k \<and> entry_in_tree k v (Branch c lt kt y rt)))"
   1.800 +  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 (del_from_right x lt kt y rt) = (False \<or> (x \<noteq> k \<and> entry_in_tree k v (Branch c lt kt y rt)))"
   1.801 +  and del_in_tree: "\<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))"
   1.802 +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)
   1.803    case (2 xx c aa yy ss bb)
   1.804    have "xx = yy \<or> xx < yy \<or> xx > yy" by auto
   1.805    from this 2 show ?case proof (elim disjE)
   1.806 @@ -674,15 +802,15 @@
   1.807        case True
   1.808        from 2 `xx = yy` `xx = k` have "sorted (Branch c aa yy ss bb) \<and> k = yy" by simp
   1.809        hence "\<not> entry_in_tree k v aa" "\<not> entry_in_tree k v bb" by (auto simp: tree_less_nit tree_greater_prop)
   1.810 -      with `xx = yy` 2 `xx = k` show ?thesis by (simp add: app_pit)
   1.811 -    qed (simp add: app_pit)
   1.812 +      with `xx = yy` 2 `xx = k` show ?thesis by (simp add: combine_in_tree)
   1.813 +    qed (simp add: combine_in_tree)
   1.814    qed simp+
   1.815  next    
   1.816    case (3 xx lta zz vv rta yy ss bb)
   1.817    def mt[simp]: mt == "Branch B lta zz vv rta"
   1.818    from 3 have "inv2 mt \<and> inv1 mt" by simp
   1.819    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)
   1.820 -  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)
   1.821 +  with 3 have 4: "entry_in_tree k v (del_from_left 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: balance_left_in_tree)
   1.822    thus ?case proof (cases "xx = k")
   1.823      case True
   1.824      from 3 True have "tree_greater yy bb \<and> yy > k" by simp
   1.825 @@ -706,13 +834,13 @@
   1.826      with "4_2" have "k < yy \<and> tree_greater yy bb" by simp
   1.827      hence "tree_greater k bb" by (blast dest: tree_greater_trans)
   1.828      with True "4_2" show ?thesis by (auto simp: tree_greater_nit)
   1.829 -  qed simp
   1.830 +  qed auto
   1.831  next
   1.832    case (5 xx aa yy ss lta zz vv rta)
   1.833    def mt[simp]: mt == "Branch B lta zz vv rta"
   1.834    from 5 have "inv2 mt \<and> inv1 mt" by simp
   1.835    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)
   1.836 -  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)
   1.837 +  with 5 have 3: "entry_in_tree k v (del_from_right 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: balance_right_in_tree)
   1.838    thus ?case proof (cases "xx = k")
   1.839      case True
   1.840      from 5 True have "tree_less yy aa \<and> yy < k" by simp
   1.841 @@ -734,14 +862,14 @@
   1.842      with "6_2" have "k > yy \<and> tree_less yy aa" by simp
   1.843      hence "tree_less k aa" by (blast dest: tree_less_trans)
   1.844      with True "6_2" show ?thesis by (auto simp: tree_less_nit)
   1.845 -  qed simp
   1.846 +  qed auto
   1.847  qed simp
   1.848  
   1.849  
   1.850  definition delete where
   1.851    delete_def: "delete k t = paint B (del k t)"
   1.852  
   1.853 -theorem delete_is_rbt[simp]: assumes "is_rbt t" shows "is_rbt (delete k t)"
   1.854 +theorem delete_is_rbt [simp]: assumes "is_rbt t" shows "is_rbt (delete k t)"
   1.855  proof -
   1.856    from assms have "inv2 t" and "inv1 t" unfolding is_rbt_def by auto 
   1.857    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)
   1.858 @@ -751,11 +879,11 @@
   1.859      by (auto intro: paint_sorted del_sorted)
   1.860  qed
   1.861  
   1.862 -lemma delete_pit: 
   1.863 +lemma delete_in_tree: 
   1.864    assumes "is_rbt t" 
   1.865    shows "entry_in_tree k v (delete x t) = (x \<noteq> k \<and> entry_in_tree k v t)"
   1.866    using assms unfolding is_rbt_def delete_def
   1.867 -  by (auto simp: del_pit)
   1.868 +  by (auto simp: del_in_tree)
   1.869  
   1.870  lemma lookup_delete:
   1.871    assumes is_rbt: "is_rbt t"
   1.872 @@ -766,35 +894,36 @@
   1.873    proof (cases "x = k")
   1.874      assume "x = k" 
   1.875      with is_rbt show ?thesis
   1.876 -      by (cases "lookup (delete k t) k") (auto simp: lookup_pit delete_pit)
   1.877 +      by (cases "lookup (delete k t) k") (auto simp: lookup_in_tree delete_in_tree)
   1.878    next
   1.879      assume "x \<noteq> k"
   1.880      thus ?thesis
   1.881 -      by auto (metis is_rbt delete_is_rbt delete_pit is_rbt_sorted lookup_from_pit)
   1.882 +      by auto (metis is_rbt delete_is_rbt delete_in_tree is_rbt_sorted lookup_from_in_tree)
   1.883    qed
   1.884  qed
   1.885  
   1.886 +
   1.887  subsection {* Union *}
   1.888  
   1.889  primrec
   1.890 -  unionwithkey :: "('a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
   1.891 +  union_with_key :: "('a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
   1.892  where
   1.893 -  "unionwithkey f t Empty = t"
   1.894 -| "unionwithkey f t (Branch c lt k v rt) = unionwithkey f (unionwithkey f (insertwithkey f k v t) lt) rt"
   1.895 +  "union_with_key f t Empty = t"
   1.896 +| "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"
   1.897  
   1.898 -lemma unionwk_sorted: "sorted lt \<Longrightarrow> sorted (unionwithkey f lt rt)" 
   1.899 +lemma unionwk_sorted: "sorted lt \<Longrightarrow> sorted (union_with_key f lt rt)" 
   1.900    by (induct rt arbitrary: lt) (auto simp: insertwk_sorted)
   1.901 -theorem unionwk_is_rbt[simp]: "is_rbt lt \<Longrightarrow> is_rbt (unionwithkey f lt rt)" 
   1.902 +theorem unionwk_is_rbt[simp]: "is_rbt lt \<Longrightarrow> is_rbt (union_with_key f lt rt)" 
   1.903    by (induct rt arbitrary: lt) (simp add: insertwk_is_rbt)+
   1.904  
   1.905  definition
   1.906 -  unionwith where
   1.907 -  "unionwith f = unionwithkey (\<lambda>_. f)"
   1.908 +  union_with where
   1.909 +  "union_with f = union_with_key (\<lambda>_. f)"
   1.910  
   1.911 -theorem unionw_is_rbt: "is_rbt lt \<Longrightarrow> is_rbt (unionwith f lt rt)" unfolding unionwith_def by simp
   1.912 +theorem unionw_is_rbt: "is_rbt lt \<Longrightarrow> is_rbt (union_with f lt rt)" unfolding union_with_def by simp
   1.913  
   1.914  definition union where
   1.915 -  "union = unionwithkey (%_ _ rv. rv)"
   1.916 +  "union = union_with_key (%_ _ rv. rv)"
   1.917  
   1.918  theorem union_is_rbt: "is_rbt lt \<Longrightarrow> is_rbt (union lt rt)" unfolding union_def by simp
   1.919  
   1.920 @@ -811,7 +940,7 @@
   1.921    case Empty thus ?case by (auto simp: union_def)
   1.922  next
   1.923    case (Branch c l k v r s)
   1.924 -  hence sortedrl: "sorted r" "sorted l" "l |\<guillemotleft> k" "k \<guillemotleft>| r" by auto
   1.925 +  then have "sorted r" "sorted l" "l |\<guillemotleft> k" "k \<guillemotleft>| r" by auto
   1.926  
   1.927    have meq: "lookup s(k \<mapsto> v) ++ lookup l ++ lookup r =
   1.928      lookup s ++
   1.929 @@ -839,178 +968,79 @@
   1.930      qed
   1.931    qed
   1.932  
   1.933 -  from Branch
   1.934 -  have IHs:
   1.935 +  from Branch have is_rbt: "is_rbt (RBT.union (RBT.insert k v s) l)"
   1.936 +    by (auto intro: union_is_rbt insert_is_rbt)
   1.937 +  with Branch have IHs:
   1.938      "lookup (union (union (insert k v s) l) r) = lookup (union (insert k v s) l) ++ lookup r"
   1.939      "lookup (union (insert k v s) l) = lookup (insert k v s) ++ lookup l"
   1.940 -    by (auto intro: union_is_rbt insert_is_rbt)
   1.941 +    by auto
   1.942    
   1.943    with meq show ?case
   1.944      by (auto simp: lookup_insert[OF Branch(3)])
   1.945 +
   1.946  qed
   1.947  
   1.948 -subsection {* Adjust *}
   1.949 +
   1.950 +subsection {* Modifying existing entries *}
   1.951  
   1.952  primrec
   1.953 -  adjustwithkey :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
   1.954 +  map_entry :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
   1.955  where
   1.956 -  "adjustwithkey f k Empty = Empty"
   1.957 -| "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))"
   1.958 +  "map_entry f k Empty = Empty"
   1.959 +| "map_entry f k (Branch c lt x v rt) = (if k < x then (Branch c (map_entry f k lt) x v rt) else if k > x then (Branch c lt x v (map_entry f k rt)) else (Branch c lt x (f x v) rt))"
   1.960  
   1.961 -lemma adjustwk_color_of: "color_of (adjustwithkey f k t) = color_of t" by (induct t) simp+
   1.962 -lemma adjustwk_inv1: "inv1 (adjustwithkey f k t) = inv1 t" by (induct t) (simp add: adjustwk_color_of)+
   1.963 -lemma adjustwk_inv2: "inv2 (adjustwithkey f k t) = inv2 t" "bheight (adjustwithkey f k t) = bheight t" by (induct t) simp+
   1.964 -lemma adjustwk_tree_greater: "tree_greater k (adjustwithkey f kk t) = tree_greater k t" by (induct t) simp+
   1.965 -lemma adjustwk_tree_less: "tree_less k (adjustwithkey f kk t) = tree_less k t" by (induct t) simp+
   1.966 -lemma adjustwk_sorted: "sorted (adjustwithkey f k t) = sorted t" by (induct t) (simp add: adjustwk_tree_less adjustwk_tree_greater)+
   1.967 +lemma map_entrywk_color_of: "color_of (map_entry f k t) = color_of t" by (induct t) simp+
   1.968 +lemma map_entrywk_inv1: "inv1 (map_entry f k t) = inv1 t" by (induct t) (simp add: map_entrywk_color_of)+
   1.969 +lemma map_entrywk_inv2: "inv2 (map_entry f k t) = inv2 t" "bheight (map_entry f k t) = bheight t" by (induct t) simp+
   1.970 +lemma map_entrywk_tree_greater: "tree_greater k (map_entry f kk t) = tree_greater k t" by (induct t) simp+
   1.971 +lemma map_entrywk_tree_less: "tree_less k (map_entry f kk t) = tree_less k t" by (induct t) simp+
   1.972 +lemma map_entrywk_sorted: "sorted (map_entry f k t) = sorted t" by (induct t) (simp add: map_entrywk_tree_less map_entrywk_tree_greater)+
   1.973  
   1.974 -theorem adjustwk_is_rbt[simp]: "is_rbt (adjustwithkey f k t) = is_rbt t" 
   1.975 -unfolding is_rbt_def by (simp add: adjustwk_inv2 adjustwk_color_of adjustwk_sorted adjustwk_inv1 )
   1.976 +theorem map_entrywk_is_rbt [simp]: "is_rbt (map_entry f k t) = is_rbt t" 
   1.977 +unfolding is_rbt_def by (simp add: map_entrywk_inv2 map_entrywk_color_of map_entrywk_sorted map_entrywk_inv1 )
   1.978  
   1.979 -theorem adjustwithkey_map[simp]:
   1.980 -  "lookup (adjustwithkey f k t) x = 
   1.981 +theorem map_entry_map [simp]:
   1.982 +  "lookup (map_entry f k t) x = 
   1.983    (if x = k then case lookup t x of None \<Rightarrow> None | Some y \<Rightarrow> Some (f k y)
   1.984              else lookup t x)"
   1.985  by (induct t arbitrary: x) (auto split:option.splits)
   1.986  
   1.987 -definition adjust where
   1.988 -  "adjust f = adjustwithkey (\<lambda>_. f)"
   1.989  
   1.990 -theorem adjust_is_rbt[simp]: "is_rbt (adjust f k t) = is_rbt t" unfolding adjust_def by simp
   1.991 -
   1.992 -theorem adjust_map[simp]:
   1.993 -  "lookup (adjust f k t) x = 
   1.994 -  (if x = k then case lookup t x of None \<Rightarrow> None | Some y \<Rightarrow> Some (f y)
   1.995 -            else lookup t x)"
   1.996 -unfolding adjust_def by simp
   1.997 -
   1.998 -subsection {* Map *}
   1.999 -
  1.1000 -primrec
  1.1001 -  mapwithkey :: "('a::linorder \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'c) rbt"
  1.1002 -where
  1.1003 -  "mapwithkey f Empty = Empty"
  1.1004 -| "mapwithkey f (Branch c lt k v rt) = Branch c (mapwithkey f lt) k (f k v) (mapwithkey f rt)"
  1.1005 -
  1.1006 -theorem mapwk_keys[simp]: "keys (mapwithkey f t) = keys t" by (induct t) auto
  1.1007 -lemma mapwk_tree_greater: "tree_greater k (mapwithkey f t) = tree_greater k t" by (induct t) simp+
  1.1008 -lemma mapwk_tree_less: "tree_less k (mapwithkey f t) = tree_less k t" by (induct t) simp+
  1.1009 -lemma mapwk_sorted: "sorted (mapwithkey f t) = sorted t"  by (induct t) (simp add: mapwk_tree_less mapwk_tree_greater)+
  1.1010 -lemma mapwk_color_of: "color_of (mapwithkey f t) = color_of t" by (induct t) simp+
  1.1011 -lemma mapwk_inv1: "inv1 (mapwithkey f t) = inv1 t" by (induct t) (simp add: mapwk_color_of)+
  1.1012 -lemma mapwk_inv2: "inv2 (mapwithkey f t) = inv2 t" "bheight (mapwithkey f t) = bheight t" by (induct t) simp+
  1.1013 -theorem mapwk_is_rbt[simp]: "is_rbt (mapwithkey f t) = is_rbt t" 
  1.1014 -unfolding is_rbt_def by (simp add: mapwk_inv1 mapwk_inv2 mapwk_sorted mapwk_color_of)
  1.1015 -
  1.1016 -theorem lookup_mapwk[simp]: "lookup (mapwithkey f t) x = Option.map (f x) (lookup t x)"
  1.1017 -by (induct t) auto
  1.1018 -
  1.1019 -definition map
  1.1020 -where map_def: "map f == mapwithkey (\<lambda>_. f)"
  1.1021 -
  1.1022 -theorem map_keys[simp]: "keys (map f t) = keys t" unfolding map_def by simp
  1.1023 -theorem map_is_rbt[simp]: "is_rbt (map f t) = is_rbt t" unfolding map_def by simp
  1.1024 -theorem lookup_map[simp]: "lookup (map f t) = Option.map f o lookup t"
  1.1025 -  by (rule ext) (simp add:map_def)
  1.1026 -
  1.1027 -subsection {* Fold *}
  1.1028 -
  1.1029 -text {* The following is still incomplete... *}
  1.1030 +subsection {* Mapping all entries *}
  1.1031  
  1.1032  primrec
  1.1033 -  foldwithkey :: "('a::linorder \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a,'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c"
  1.1034 +  map :: "('a::linorder \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'c) rbt"
  1.1035  where
  1.1036 -  "foldwithkey f Empty v = v"
  1.1037 -| "foldwithkey f (Branch c lt k x rt) v = foldwithkey f rt (f k x (foldwithkey f lt v))"
  1.1038 -
  1.1039 -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"
  1.1040 -proof (rule ext)
  1.1041 -  fix x
  1.1042 -  assume SORTED: "sorted (Branch c t1 k v t2)"
  1.1043 -  let ?thesis = "RBT.lookup (Branch c t1 k v t2) x = (RBT.lookup t2 ++ [k \<mapsto> v] ++ RBT.lookup t1) x"
  1.1044 -
  1.1045 -  have DOM_T1: "!!k'. k'\<in>dom (RBT.lookup t1) \<Longrightarrow> k>k'"
  1.1046 -  proof -
  1.1047 -    fix k'
  1.1048 -    from SORTED have "t1 |\<guillemotleft> k" by simp
  1.1049 -    with tree_less_prop have "\<forall>k'\<in>keys t1. k>k'" by auto
  1.1050 -    moreover assume "k'\<in>dom (RBT.lookup t1)"
  1.1051 -    ultimately show "k>k'" using RBT.lookup_keys SORTED by auto
  1.1052 -  qed
  1.1053 -
  1.1054 -  have DOM_T2: "!!k'. k'\<in>dom (RBT.lookup t2) \<Longrightarrow> k<k'"
  1.1055 -  proof -
  1.1056 -    fix k'
  1.1057 -    from SORTED have "k \<guillemotleft>| t2" by simp
  1.1058 -    with tree_greater_prop have "\<forall>k'\<in>keys t2. k<k'" by auto
  1.1059 -    moreover assume "k'\<in>dom (RBT.lookup t2)"
  1.1060 -    ultimately show "k<k'" using RBT.lookup_keys SORTED by auto
  1.1061 -  qed
  1.1062 +  "map f Empty = Empty"
  1.1063 +| "map f (Branch c lt k v rt) = Branch c (map f lt) k (f k v) (map f rt)"
  1.1064  
  1.1065 -  {
  1.1066 -    assume C: "x<k"
  1.1067 -    hence "RBT.lookup (Branch c t1 k v t2) x = RBT.lookup t1 x" by simp
  1.1068 -    moreover from C have "x\<notin>dom [k\<mapsto>v]" by simp
  1.1069 -    moreover have "x\<notin>dom (RBT.lookup t2)" proof
  1.1070 -      assume "x\<in>dom (RBT.lookup t2)"
  1.1071 -      with DOM_T2 have "k<x" by blast
  1.1072 -      with C show False by simp
  1.1073 -    qed
  1.1074 -    ultimately have ?thesis by (simp add: map_add_upd_left map_add_dom_app_simps)
  1.1075 -  } moreover {
  1.1076 -    assume [simp]: "x=k"
  1.1077 -    hence "RBT.lookup (Branch c t1 k v t2) x = [k \<mapsto> v] x" by simp
  1.1078 -    moreover have "x\<notin>dom (RBT.lookup t1)" proof
  1.1079 -      assume "x\<in>dom (RBT.lookup t1)"
  1.1080 -      with DOM_T1 have "k>x" by blast
  1.1081 -      thus False by simp
  1.1082 -    qed
  1.1083 -    ultimately have ?thesis by (simp add: map_add_upd_left map_add_dom_app_simps)
  1.1084 -  } moreover {
  1.1085 -    assume C: "x>k"
  1.1086 -    hence "RBT.lookup (Branch c t1 k v t2) x = RBT.lookup t2 x" by (simp add: less_not_sym[of k x])
  1.1087 -    moreover from C have "x\<notin>dom [k\<mapsto>v]" by simp
  1.1088 -    moreover have "x\<notin>dom (RBT.lookup t1)" proof
  1.1089 -      assume "x\<in>dom (RBT.lookup t1)"
  1.1090 -      with DOM_T1 have "k>x" by simp
  1.1091 -      with C show False by simp
  1.1092 -    qed
  1.1093 -    ultimately have ?thesis by (simp add: map_add_upd_left map_add_dom_app_simps)
  1.1094 -  } ultimately show ?thesis using less_linear by blast
  1.1095 -qed
  1.1096 +lemma map_entries [simp]: "entries (map f t) = List.map (\<lambda>(k, v). (k, f k v)) (entries t)"
  1.1097 +  by (induct t) auto
  1.1098 +lemma map_keys [simp]: "keys (map f t) = keys t" by (simp add: keys_def split_def)
  1.1099 +lemma map_tree_greater: "tree_greater k (map f t) = tree_greater k t" by (induct t) simp+
  1.1100 +lemma map_tree_less: "tree_less k (map f t) = tree_less k t" by (induct t) simp+
  1.1101 +lemma map_sorted: "sorted (map f t) = sorted t"  by (induct t) (simp add: map_tree_less map_tree_greater)+
  1.1102 +lemma map_color_of: "color_of (map f t) = color_of t" by (induct t) simp+
  1.1103 +lemma map_inv1: "inv1 (map f t) = inv1 t" by (induct t) (simp add: map_color_of)+
  1.1104 +lemma map_inv2: "inv2 (map f t) = inv2 t" "bheight (map f t) = bheight t" by (induct t) simp+
  1.1105 +theorem map_is_rbt [simp]: "is_rbt (map f t) = is_rbt t" 
  1.1106 +unfolding is_rbt_def by (simp add: map_inv1 map_inv2 map_sorted map_color_of)
  1.1107  
  1.1108 -lemma map_of_entries:
  1.1109 -  shows "sorted t \<Longrightarrow> map_of (entries t) = lookup t"
  1.1110 -proof (induct t)
  1.1111 -  case Empty thus ?case by (simp add: RBT.lookup_Empty)
  1.1112 -next
  1.1113 -  case (Branch c t1 k v t2)
  1.1114 -  hence "map_of (entries (Branch c t1 k v t2)) = RBT.lookup t2 ++ [k \<mapsto> v] ++ RBT.lookup t1" by simp
  1.1115 -  also note lookup_entries_aux [OF Branch.prems,symmetric]
  1.1116 -  finally show ?case .
  1.1117 -qed
  1.1118 -
  1.1119 -lemma fold_entries_fold:
  1.1120 -  "foldwithkey f t x = foldl (\<lambda>x (k,v). f k v x) x (entries t)"
  1.1121 -by (induct t arbitrary: x) auto
  1.1122 -
  1.1123 -lemma entries_pit[simp]: "(k, v) \<in> set (entries t) = entry_in_tree k v t"
  1.1124 +theorem lookup_map [simp]: "lookup (map f t) x = Option.map (f x) (lookup t x)"
  1.1125  by (induct t) auto
  1.1126  
  1.1127 -lemma sorted_entries:
  1.1128 -  "sorted t \<Longrightarrow> List.sorted (List.map fst (entries t))"
  1.1129 -by (induct t) 
  1.1130 -  (force simp: sorted_append sorted_Cons tree_ord_props 
  1.1131 -      dest!: entry_in_tree_keys)+
  1.1132 +
  1.1133 +subsection {* Folding over entries *}
  1.1134 +
  1.1135 +definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c" where
  1.1136 +  "fold f t s = foldl (\<lambda>s (k, v). f k v s) s (entries t)"
  1.1137  
  1.1138 -lemma distinct_entries:
  1.1139 -  "sorted t \<Longrightarrow> distinct (List.map fst (entries t))"
  1.1140 -by (induct t) 
  1.1141 -  (force simp: sorted_append sorted_Cons tree_ord_props 
  1.1142 -      dest!: entry_in_tree_keys)+
  1.1143 +lemma fold_simps [simp, code]:
  1.1144 +  "fold f Empty = id"
  1.1145 +  "fold f (Branch c lt k v rt) = fold f rt \<circ> f k v \<circ> fold f lt"
  1.1146 +  by (simp_all add: fold_def expand_fun_eq)
  1.1147  
  1.1148 -hide (open) const Empty insert delete entries lookup map fold union adjust sorted
  1.1149 -
  1.1150 +hide (open) const Empty insert delete entries lookup map_entry map fold union sorted
  1.1151  (*>*)
  1.1152  
  1.1153  text {* 
  1.1154 @@ -1018,6 +1048,7 @@
  1.1155    used as an efficient representation of finite maps.
  1.1156  *}
  1.1157  
  1.1158 +
  1.1159  subsection {* Data type and invariant *}
  1.1160  
  1.1161  text {*
  1.1162 @@ -1040,6 +1071,7 @@
  1.1163    $O(\log n)$.  
  1.1164  *}
  1.1165  
  1.1166 +
  1.1167  subsection {* Operations *}
  1.1168  
  1.1169  text {*
  1.1170 @@ -1081,6 +1113,7 @@
  1.1171    @{thm map_is_rbt}\hfill(@{text "map_is_rbt"})
  1.1172  *}
  1.1173  
  1.1174 +
  1.1175  subsection {* Map Semantics *}
  1.1176  
  1.1177  text {*
     2.1 --- a/src/HOL/Map.thy	Wed Mar 03 20:21:30 2010 +0100
     2.2 +++ b/src/HOL/Map.thy	Wed Mar 03 20:45:48 2010 +0100
     2.3 @@ -332,12 +332,12 @@
     2.4  by (fastsimp simp: map_add_def dom_def inj_on_def split: option.splits)
     2.5  
     2.6  lemma map_upds_fold_map_upd:
     2.7 -  "f(ks[\<mapsto>]vs) = foldl (\<lambda>f (k, v). f(k\<mapsto>v)) f (zip ks vs)"
     2.8 +  "m(ks[\<mapsto>]vs) = foldl (\<lambda>m (k, v). m(k \<mapsto> v)) m (zip ks vs)"
     2.9  unfolding map_upds_def proof (rule sym, rule zip_obtain_same_length)
    2.10    fix ks :: "'a list" and vs :: "'b list"
    2.11    assume "length ks = length vs"
    2.12 -  then show "foldl (\<lambda>f (k, v). f(k\<mapsto>v)) f (zip ks vs) = f ++ map_of (rev (zip ks vs))"
    2.13 -    by (induct arbitrary: f rule: list_induct2) simp_all
    2.14 +  then show "foldl (\<lambda>m (k, v). m(k\<mapsto>v)) m (zip ks vs) = m ++ map_of (rev (zip ks vs))"
    2.15 +    by(induct arbitrary: m rule: list_induct2) simp_all
    2.16  qed
    2.17  
    2.18  lemma map_add_map_of_foldr:
     3.1 --- a/src/HOL/Nat_Transfer.thy	Wed Mar 03 20:21:30 2010 +0100
     3.2 +++ b/src/HOL/Nat_Transfer.thy	Wed Mar 03 20:45:48 2010 +0100
     3.3 @@ -25,7 +25,7 @@
     3.4  lemma TransferMorphism_nat_int: "TransferMorphism nat (op <= (0::int))"
     3.5    by (simp add: TransferMorphism_def)
     3.6  
     3.7 -declare TransferMorphism_nat_int[transfer
     3.8 +declare TransferMorphism_nat_int [transfer
     3.9    add mode: manual
    3.10    return: nat_0_le
    3.11    labels: natint
    3.12 @@ -80,7 +80,7 @@
    3.13        (nat (x::int) dvd nat y) = (x dvd y)"
    3.14    by (auto simp add: zdvd_int)
    3.15  
    3.16 -declare TransferMorphism_nat_int[transfer add return:
    3.17 +declare TransferMorphism_nat_int [transfer add return:
    3.18    transfer_nat_int_numerals
    3.19    transfer_nat_int_functions
    3.20    transfer_nat_int_function_closures
    3.21 @@ -118,7 +118,7 @@
    3.22      (EX x. Q x \<and> P x) = (EX x. Q x \<and> P' x)"
    3.23    by auto
    3.24  
    3.25 -declare TransferMorphism_nat_int[transfer add
    3.26 +declare TransferMorphism_nat_int [transfer add
    3.27    return: transfer_nat_int_quantifiers
    3.28    cong: all_cong ex_cong]
    3.29  
    3.30 @@ -190,7 +190,7 @@
    3.31      {(x::int). x >= 0 & P x} = {x. x >= 0 & P' x}"
    3.32    by auto
    3.33  
    3.34 -declare TransferMorphism_nat_int[transfer add
    3.35 +declare TransferMorphism_nat_int [transfer add
    3.36    return: transfer_nat_int_set_functions
    3.37      transfer_nat_int_set_function_closures
    3.38      transfer_nat_int_set_relations
    3.39 @@ -262,7 +262,7 @@
    3.40    apply (subst setprod_cong, assumption, auto)
    3.41  done
    3.42  
    3.43 -declare TransferMorphism_nat_int[transfer add
    3.44 +declare TransferMorphism_nat_int [transfer add
    3.45    return: transfer_nat_int_sum_prod transfer_nat_int_sum_prod2
    3.46      transfer_nat_int_sum_prod_closure
    3.47    cong: transfer_nat_int_sum_prod_cong]
    3.48 @@ -275,7 +275,7 @@
    3.49  lemma TransferMorphism_int_nat: "TransferMorphism int (UNIV :: nat set)"
    3.50    by (simp add: TransferMorphism_def)
    3.51  
    3.52 -declare TransferMorphism_int_nat[transfer add
    3.53 +declare TransferMorphism_int_nat [transfer add
    3.54    mode: manual
    3.55  (*  labels: int-nat *)
    3.56    return: nat_int
    3.57 @@ -326,7 +326,7 @@
    3.58      "(int x dvd int y) = (x dvd y)"
    3.59    by (auto simp add: zdvd_int)
    3.60  
    3.61 -declare TransferMorphism_int_nat[transfer add return:
    3.62 +declare TransferMorphism_int_nat [transfer add return:
    3.63    transfer_int_nat_numerals
    3.64    transfer_int_nat_functions
    3.65    transfer_int_nat_function_closures
    3.66 @@ -346,7 +346,7 @@
    3.67    apply auto
    3.68  done
    3.69  
    3.70 -declare TransferMorphism_int_nat[transfer add
    3.71 +declare TransferMorphism_int_nat [transfer add
    3.72    return: transfer_int_nat_quantifiers]
    3.73  
    3.74  
    3.75 @@ -401,7 +401,7 @@
    3.76      {(x::nat). P x} = {x. P' x}"
    3.77    by auto
    3.78  
    3.79 -declare TransferMorphism_int_nat[transfer add
    3.80 +declare TransferMorphism_int_nat [transfer add
    3.81    return: transfer_int_nat_set_functions
    3.82      transfer_int_nat_set_function_closures
    3.83      transfer_int_nat_set_relations
    3.84 @@ -433,7 +433,7 @@
    3.85    apply (subst int_setprod, auto simp add: cong: setprod_cong)
    3.86  done
    3.87  
    3.88 -declare TransferMorphism_int_nat[transfer add
    3.89 +declare TransferMorphism_int_nat [transfer add
    3.90    return: transfer_int_nat_sum_prod transfer_int_nat_sum_prod2
    3.91    cong: setsum_cong setprod_cong]
    3.92