move RBT implementation into type class contexts
authorAndreas Lochbihler
Fri Apr 13 11:45:30 2012 +0200 (2012-04-13)
changeset 474502ada2be850cb
parent 47438 11a0aa6cc677
child 47451 ab606e685d52
move RBT implementation into type class contexts
src/HOL/Library/RBT.thy
src/HOL/Library/RBT_Impl.thy
src/HOL/Library/RBT_Mapping.thy
     1.1 --- a/src/HOL/Library/RBT.thy	Thu Apr 12 13:47:21 2012 +0200
     1.2 +++ b/src/HOL/Library/RBT.thy	Fri Apr 13 11:45:30 2012 +0200
     1.3 @@ -35,7 +35,7 @@
     1.4  subsection {* Primitive operations *}
     1.5  
     1.6  definition lookup :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b" where
     1.7 -  [code]: "lookup t = RBT_Impl.lookup (impl_of t)"
     1.8 +  [code]: "lookup t = rbt_lookup (impl_of t)"
     1.9  
    1.10  definition empty :: "('a\<Colon>linorder, 'b) rbt" where
    1.11    "empty = RBT RBT_Impl.Empty"
    1.12 @@ -45,17 +45,17 @@
    1.13    by (simp add: empty_def RBT_inverse)
    1.14  
    1.15  definition insert :: "'a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" where
    1.16 -  "insert k v t = RBT (RBT_Impl.insert k v (impl_of t))"
    1.17 +  "insert k v t = RBT (rbt_insert k v (impl_of t))"
    1.18  
    1.19  lemma impl_of_insert [code abstract]:
    1.20 -  "impl_of (insert k v t) = RBT_Impl.insert k v (impl_of t)"
    1.21 +  "impl_of (insert k v t) = rbt_insert k v (impl_of t)"
    1.22    by (simp add: insert_def RBT_inverse)
    1.23  
    1.24  definition delete :: "'a\<Colon>linorder \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" where
    1.25 -  "delete k t = RBT (RBT_Impl.delete k (impl_of t))"
    1.26 +  "delete k t = RBT (rbt_delete k (impl_of t))"
    1.27  
    1.28  lemma impl_of_delete [code abstract]:
    1.29 -  "impl_of (delete k t) = RBT_Impl.delete k (impl_of t)"
    1.30 +  "impl_of (delete k t) = rbt_delete k (impl_of t)"
    1.31    by (simp add: delete_def RBT_inverse)
    1.32  
    1.33  definition entries :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a \<times> 'b) list" where
    1.34 @@ -65,17 +65,17 @@
    1.35    [code]: "keys t = RBT_Impl.keys (impl_of t)"
    1.36  
    1.37  definition bulkload :: "('a\<Colon>linorder \<times> 'b) list \<Rightarrow> ('a, 'b) rbt" where
    1.38 -  "bulkload xs = RBT (RBT_Impl.bulkload xs)"
    1.39 +  "bulkload xs = RBT (rbt_bulkload xs)"
    1.40  
    1.41  lemma impl_of_bulkload [code abstract]:
    1.42 -  "impl_of (bulkload xs) = RBT_Impl.bulkload xs"
    1.43 +  "impl_of (bulkload xs) = rbt_bulkload xs"
    1.44    by (simp add: bulkload_def RBT_inverse)
    1.45  
    1.46  definition map_entry :: "'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt" where
    1.47 -  "map_entry k f t = RBT (RBT_Impl.map_entry k f (impl_of t))"
    1.48 +  "map_entry k f t = RBT (rbt_map_entry k f (impl_of t))"
    1.49  
    1.50  lemma impl_of_map_entry [code abstract]:
    1.51 -  "impl_of (map_entry k f t) = RBT_Impl.map_entry k f (impl_of t)"
    1.52 +  "impl_of (map_entry k f t) = rbt_map_entry k f (impl_of t)"
    1.53    by (simp add: map_entry_def RBT_inverse)
    1.54  
    1.55  definition map :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt" where
    1.56 @@ -98,11 +98,11 @@
    1.57  subsection {* Abstract lookup properties *}
    1.58  
    1.59  lemma lookup_RBT:
    1.60 -  "is_rbt t \<Longrightarrow> lookup (RBT t) = RBT_Impl.lookup t"
    1.61 +  "is_rbt t \<Longrightarrow> lookup (RBT t) = rbt_lookup t"
    1.62    by (simp add: lookup_def RBT_inverse)
    1.63  
    1.64  lemma lookup_impl_of:
    1.65 -  "RBT_Impl.lookup (impl_of t) = lookup t"
    1.66 +  "rbt_lookup (impl_of t) = lookup t"
    1.67    by (simp add: lookup_def)
    1.68  
    1.69  lemma entries_impl_of:
    1.70 @@ -119,11 +119,11 @@
    1.71  
    1.72  lemma lookup_insert [simp]:
    1.73    "lookup (insert k v t) = (lookup t)(k \<mapsto> v)"
    1.74 -  by (simp add: insert_def lookup_RBT lookup_insert lookup_impl_of)
    1.75 +  by (simp add: insert_def lookup_RBT rbt_lookup_rbt_insert lookup_impl_of)
    1.76  
    1.77  lemma lookup_delete [simp]:
    1.78    "lookup (delete k t) = (lookup t)(k := None)"
    1.79 -  by (simp add: delete_def lookup_RBT RBT_Impl.lookup_delete lookup_impl_of restrict_complement_singleton_eq)
    1.80 +  by (simp add: delete_def lookup_RBT rbt_lookup_rbt_delete lookup_impl_of restrict_complement_singleton_eq)
    1.81  
    1.82  lemma map_of_entries [simp]:
    1.83    "map_of (entries t) = lookup t"
    1.84 @@ -131,19 +131,19 @@
    1.85  
    1.86  lemma entries_lookup:
    1.87    "entries t1 = entries t2 \<longleftrightarrow> lookup t1 = lookup t2"
    1.88 -  by (simp add: entries_def lookup_def entries_lookup)
    1.89 +  by (simp add: entries_def lookup_def entries_rbt_lookup)
    1.90  
    1.91  lemma lookup_bulkload [simp]:
    1.92    "lookup (bulkload xs) = map_of xs"
    1.93 -  by (simp add: bulkload_def lookup_RBT RBT_Impl.lookup_bulkload)
    1.94 +  by (simp add: bulkload_def lookup_RBT rbt_lookup_rbt_bulkload)
    1.95  
    1.96  lemma lookup_map_entry [simp]:
    1.97    "lookup (map_entry k f t) = (lookup t)(k := Option.map f (lookup t k))"
    1.98 -  by (simp add: map_entry_def lookup_RBT RBT_Impl.lookup_map_entry lookup_impl_of)
    1.99 +  by (simp add: map_entry_def lookup_RBT rbt_lookup_rbt_map_entry lookup_impl_of)
   1.100  
   1.101  lemma lookup_map [simp]:
   1.102    "lookup (map f t) k = Option.map (f k) (lookup t k)"
   1.103 -  by (simp add: map_def lookup_RBT RBT_Impl.lookup_map lookup_impl_of)
   1.104 +  by (simp add: map_def lookup_RBT rbt_lookup_map lookup_impl_of)
   1.105  
   1.106  lemma fold_fold:
   1.107    "fold f t = List.fold (prod_case f) (entries t)"
   1.108 @@ -154,7 +154,7 @@
   1.109    by (simp add: rbt_eq_iff is_empty_def impl_of_empty split: rbt.split)
   1.110  
   1.111  lemma RBT_lookup_empty [simp]: (*FIXME*)
   1.112 -  "RBT_Impl.lookup t = Map.empty \<longleftrightarrow> t = RBT_Impl.Empty"
   1.113 +  "rbt_lookup t = Map.empty \<longleftrightarrow> t = RBT_Impl.Empty"
   1.114    by (cases t) (auto simp add: fun_eq_iff)
   1.115  
   1.116  lemma lookup_empty_empty [simp]:
   1.117 @@ -163,7 +163,7 @@
   1.118  
   1.119  lemma sorted_keys [iff]:
   1.120    "sorted (keys t)"
   1.121 -  by (simp add: keys_def RBT_Impl.keys_def sorted_entries)
   1.122 +  by (simp add: keys_def RBT_Impl.keys_def rbt_sorted_entries)
   1.123  
   1.124  lemma distinct_keys [iff]:
   1.125    "distinct (keys t)"
     2.1 --- a/src/HOL/Library/RBT_Impl.thy	Thu Apr 12 13:47:21 2012 +0200
     2.2 +++ b/src/HOL/Library/RBT_Impl.thy	Fri Apr 13 11:45:30 2012 +0200
     2.3 @@ -1,4 +1,4 @@
     2.4 -(*  Title:      HOL/Library/RBT_Impl.thy
     2.5 +(*  Title:      RBT_Impl.thy
     2.6      Author:     Markus Reiter, TU Muenchen
     2.7      Author:     Alexander Krauss, TU Muenchen
     2.8  *)
     2.9 @@ -65,202 +65,221 @@
    2.10  
    2.11  subsubsection {* Search tree properties *}
    2.12  
    2.13 -definition tree_less :: "'a\<Colon>order \<Rightarrow> ('a, 'b) rbt \<Rightarrow> bool"
    2.14 -where
    2.15 -  tree_less_prop: "tree_less k t \<longleftrightarrow> (\<forall>x\<in>set (keys t). x < k)"
    2.16 +context ord begin
    2.17  
    2.18 -abbreviation tree_less_symbol (infix "|\<guillemotleft>" 50)
    2.19 -where "t |\<guillemotleft> x \<equiv> tree_less x t"
    2.20 +definition rbt_less :: "'a \<Rightarrow> ('a, 'b) rbt \<Rightarrow> bool"
    2.21 +where
    2.22 +  rbt_less_prop: "rbt_less k t \<longleftrightarrow> (\<forall>x\<in>set (keys t). x < k)"
    2.23  
    2.24 -definition tree_greater :: "'a\<Colon>order \<Rightarrow> ('a, 'b) rbt \<Rightarrow> bool" (infix "\<guillemotleft>|" 50) 
    2.25 +abbreviation rbt_less_symbol (infix "|\<guillemotleft>" 50)
    2.26 +where "t |\<guillemotleft> x \<equiv> rbt_less x t"
    2.27 +
    2.28 +definition rbt_greater :: "'a \<Rightarrow> ('a, 'b) rbt \<Rightarrow> bool" (infix "\<guillemotleft>|" 50) 
    2.29  where
    2.30 -  tree_greater_prop: "tree_greater k t = (\<forall>x\<in>set (keys t). k < x)"
    2.31 +  rbt_greater_prop: "rbt_greater k t = (\<forall>x\<in>set (keys t). k < x)"
    2.32  
    2.33 -lemma tree_less_simps [simp]:
    2.34 -  "tree_less k Empty = True"
    2.35 -  "tree_less k (Branch c lt kt v rt) \<longleftrightarrow> kt < k \<and> tree_less k lt \<and> tree_less k rt"
    2.36 -  by (auto simp add: tree_less_prop)
    2.37 +lemma rbt_less_simps [simp]:
    2.38 +  "Empty |\<guillemotleft> k = True"
    2.39 +  "Branch c lt kt v rt |\<guillemotleft> k \<longleftrightarrow> kt < k \<and> lt |\<guillemotleft> k \<and> rt |\<guillemotleft> k"
    2.40 +  by (auto simp add: rbt_less_prop)
    2.41  
    2.42 -lemma tree_greater_simps [simp]:
    2.43 -  "tree_greater k Empty = True"
    2.44 -  "tree_greater k (Branch c lt kt v rt) \<longleftrightarrow> k < kt \<and> tree_greater k lt \<and> tree_greater k rt"
    2.45 -  by (auto simp add: tree_greater_prop)
    2.46 +lemma rbt_greater_simps [simp]:
    2.47 +  "k \<guillemotleft>| Empty = True"
    2.48 +  "k \<guillemotleft>| (Branch c lt kt v rt) \<longleftrightarrow> k < kt \<and> k \<guillemotleft>| lt \<and> k \<guillemotleft>| rt"
    2.49 +  by (auto simp add: rbt_greater_prop)
    2.50  
    2.51 -lemmas tree_ord_props = tree_less_prop tree_greater_prop
    2.52 +lemmas rbt_ord_props = rbt_less_prop rbt_greater_prop
    2.53 +
    2.54 +lemmas rbt_greater_nit = rbt_greater_prop entry_in_tree_keys
    2.55 +lemmas rbt_less_nit = rbt_less_prop entry_in_tree_keys
    2.56  
    2.57 -lemmas tree_greater_nit = tree_greater_prop entry_in_tree_keys
    2.58 -lemmas tree_less_nit = tree_less_prop entry_in_tree_keys
    2.59 +lemma (in order)
    2.60 +  shows rbt_less_eq_trans: "l |\<guillemotleft> u \<Longrightarrow> u \<le> v \<Longrightarrow> l |\<guillemotleft> v"
    2.61 +  and rbt_less_trans: "t |\<guillemotleft> x \<Longrightarrow> x < y \<Longrightarrow> t |\<guillemotleft> y"
    2.62 +  and rbt_greater_eq_trans: "u \<le> v \<Longrightarrow> v \<guillemotleft>| r \<Longrightarrow> u \<guillemotleft>| r"
    2.63 +  and rbt_greater_trans: "x < y \<Longrightarrow> y \<guillemotleft>| t \<Longrightarrow> x \<guillemotleft>| t"
    2.64 +  by (auto simp: rbt_ord_props)
    2.65  
    2.66 -lemma tree_less_eq_trans: "l |\<guillemotleft> u \<Longrightarrow> u \<le> v \<Longrightarrow> l |\<guillemotleft> v"
    2.67 -  and tree_less_trans: "t |\<guillemotleft> x \<Longrightarrow> x < y \<Longrightarrow> t |\<guillemotleft> y"
    2.68 -  and tree_greater_eq_trans: "u \<le> v \<Longrightarrow> v \<guillemotleft>| r \<Longrightarrow> u \<guillemotleft>| r"
    2.69 -  and tree_greater_trans: "x < y \<Longrightarrow> y \<guillemotleft>| t \<Longrightarrow> x \<guillemotleft>| t"
    2.70 -  by (auto simp: tree_ord_props)
    2.71 -
    2.72 -primrec sorted :: "('a::linorder, 'b) rbt \<Rightarrow> bool"
    2.73 +primrec rbt_sorted :: "('a, 'b) rbt \<Rightarrow> bool"
    2.74  where
    2.75 -  "sorted Empty = True"
    2.76 -| "sorted (Branch c l k v r) = (l |\<guillemotleft> k \<and> k \<guillemotleft>| r \<and> sorted l \<and> sorted r)"
    2.77 +  "rbt_sorted Empty = True"
    2.78 +| "rbt_sorted (Branch c l k v r) = (l |\<guillemotleft> k \<and> k \<guillemotleft>| r \<and> rbt_sorted l \<and> rbt_sorted r)"
    2.79 +
    2.80 +end
    2.81  
    2.82 -lemma sorted_entries:
    2.83 -  "sorted t \<Longrightarrow> List.sorted (List.map fst (entries t))"
    2.84 +context linorder begin
    2.85 +
    2.86 +lemma rbt_sorted_entries:
    2.87 +  "rbt_sorted t \<Longrightarrow> List.sorted (List.map fst (entries t))"
    2.88  by (induct t) 
    2.89 -  (force simp: sorted_append sorted_Cons tree_ord_props 
    2.90 +  (force simp: sorted_append sorted_Cons rbt_ord_props 
    2.91        dest!: entry_in_tree_keys)+
    2.92  
    2.93  lemma distinct_entries:
    2.94 -  "sorted t \<Longrightarrow> distinct (List.map fst (entries t))"
    2.95 +  "rbt_sorted t \<Longrightarrow> distinct (List.map fst (entries t))"
    2.96  by (induct t) 
    2.97 -  (force simp: sorted_append sorted_Cons tree_ord_props 
    2.98 +  (force simp: sorted_append sorted_Cons rbt_ord_props 
    2.99        dest!: entry_in_tree_keys)+
   2.100  
   2.101 -
   2.102  subsubsection {* Tree lookup *}
   2.103  
   2.104 -primrec lookup :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b"
   2.105 +primrec (in ord) rbt_lookup :: "('a, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b"
   2.106  where
   2.107 -  "lookup Empty k = None"
   2.108 -| "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)"
   2.109 +  "rbt_lookup Empty k = None"
   2.110 +| "rbt_lookup (Branch _ l x y r) k = 
   2.111 +   (if k < x then rbt_lookup l k else if x < k then rbt_lookup r k else Some y)"
   2.112  
   2.113 -lemma lookup_keys: "sorted t \<Longrightarrow> dom (lookup t) = set (keys t)"
   2.114 -  by (induct t) (auto simp: dom_def tree_greater_prop tree_less_prop)
   2.115 +lemma rbt_lookup_keys: "rbt_sorted t \<Longrightarrow> dom (rbt_lookup t) = set (keys t)"
   2.116 +  by (induct t) (auto simp: dom_def rbt_greater_prop rbt_less_prop)
   2.117  
   2.118 -lemma dom_lookup_Branch: 
   2.119 -  "sorted (Branch c t1 k v t2) \<Longrightarrow> 
   2.120 -    dom (lookup (Branch c t1 k v t2)) 
   2.121 -    = Set.insert k (dom (lookup t1) \<union> dom (lookup t2))"
   2.122 +lemma dom_rbt_lookup_Branch: 
   2.123 +  "rbt_sorted (Branch c t1 k v t2) \<Longrightarrow> 
   2.124 +    dom (rbt_lookup (Branch c t1 k v t2)) 
   2.125 +    = Set.insert k (dom (rbt_lookup t1) \<union> dom (rbt_lookup t2))"
   2.126  proof -
   2.127 -  assume "sorted (Branch c t1 k v t2)"
   2.128 -  moreover from this have "sorted t1" "sorted t2" by simp_all
   2.129 -  ultimately show ?thesis by (simp add: lookup_keys)
   2.130 +  assume "rbt_sorted (Branch c t1 k v t2)"
   2.131 +  moreover from this have "rbt_sorted t1" "rbt_sorted t2" by simp_all
   2.132 +  ultimately show ?thesis by (simp add: rbt_lookup_keys)
   2.133  qed
   2.134  
   2.135 -lemma finite_dom_lookup [simp, intro!]: "finite (dom (lookup t))"
   2.136 +lemma finite_dom_rbt_lookup [simp, intro!]: "finite (dom (rbt_lookup t))"
   2.137  proof (induct t)
   2.138    case Empty then show ?case by simp
   2.139  next
   2.140    case (Branch color t1 a b t2)
   2.141 -  let ?A = "Set.insert a (dom (lookup t1) \<union> dom (lookup t2))"
   2.142 -  have "dom (lookup (Branch color t1 a b t2)) \<subseteq> ?A" by (auto split: split_if_asm)
   2.143 -  moreover from Branch have "finite (insert a (dom (lookup t1) \<union> dom (lookup t2)))" by simp
   2.144 +  let ?A = "Set.insert a (dom (rbt_lookup t1) \<union> dom (rbt_lookup t2))"
   2.145 +  have "dom (rbt_lookup (Branch color t1 a b t2)) \<subseteq> ?A" by (auto split: split_if_asm)
   2.146 +  moreover from Branch have "finite (insert a (dom (rbt_lookup t1) \<union> dom (rbt_lookup t2)))" by simp
   2.147    ultimately show ?case by (rule finite_subset)
   2.148  qed 
   2.149  
   2.150 -lemma lookup_tree_less[simp]: "t |\<guillemotleft> k \<Longrightarrow> lookup t k = None" 
   2.151 +end
   2.152 +
   2.153 +context ord begin
   2.154 +
   2.155 +lemma rbt_lookup_rbt_less[simp]: "t |\<guillemotleft> k \<Longrightarrow> rbt_lookup t k = None" 
   2.156  by (induct t) auto
   2.157  
   2.158 -lemma lookup_tree_greater[simp]: "k \<guillemotleft>| t \<Longrightarrow> lookup t k = None"
   2.159 +lemma rbt_lookup_rbt_greater[simp]: "k \<guillemotleft>| t \<Longrightarrow> rbt_lookup t k = None"
   2.160  by (induct t) auto
   2.161  
   2.162 -lemma lookup_Empty: "lookup Empty = empty"
   2.163 +lemma rbt_lookup_Empty: "rbt_lookup Empty = empty"
   2.164  by (rule ext) simp
   2.165  
   2.166 +end
   2.167 +
   2.168 +context linorder begin
   2.169 +
   2.170  lemma map_of_entries:
   2.171 -  "sorted t \<Longrightarrow> map_of (entries t) = lookup t"
   2.172 +  "rbt_sorted t \<Longrightarrow> map_of (entries t) = rbt_lookup t"
   2.173  proof (induct t)
   2.174 -  case Empty thus ?case by (simp add: lookup_Empty)
   2.175 +  case Empty thus ?case by (simp add: rbt_lookup_Empty)
   2.176  next
   2.177    case (Branch c t1 k v t2)
   2.178 -  have "lookup (Branch c t1 k v t2) = lookup t2 ++ [k\<mapsto>v] ++ lookup t1"
   2.179 +  have "rbt_lookup (Branch c t1 k v t2) = rbt_lookup t2 ++ [k\<mapsto>v] ++ rbt_lookup t1"
   2.180    proof (rule ext)
   2.181      fix x
   2.182 -    from Branch have SORTED: "sorted (Branch c t1 k v t2)" by simp
   2.183 -    let ?thesis = "lookup (Branch c t1 k v t2) x = (lookup t2 ++ [k \<mapsto> v] ++ lookup t1) x"
   2.184 +    from Branch have RBT_SORTED: "rbt_sorted (Branch c t1 k v t2)" by simp
   2.185 +    let ?thesis = "rbt_lookup (Branch c t1 k v t2) x = (rbt_lookup t2 ++ [k \<mapsto> v] ++ rbt_lookup t1) x"
   2.186  
   2.187 -    have DOM_T1: "!!k'. k'\<in>dom (lookup t1) \<Longrightarrow> k>k'"
   2.188 +    have DOM_T1: "!!k'. k'\<in>dom (rbt_lookup t1) \<Longrightarrow> k>k'"
   2.189      proof -
   2.190        fix k'
   2.191 -      from SORTED have "t1 |\<guillemotleft> k" by simp
   2.192 -      with tree_less_prop have "\<forall>k'\<in>set (keys t1). k>k'" by auto
   2.193 -      moreover assume "k'\<in>dom (lookup t1)"
   2.194 -      ultimately show "k>k'" using lookup_keys SORTED by auto
   2.195 +      from RBT_SORTED have "t1 |\<guillemotleft> k" by simp
   2.196 +      with rbt_less_prop have "\<forall>k'\<in>set (keys t1). k>k'" by auto
   2.197 +      moreover assume "k'\<in>dom (rbt_lookup t1)"
   2.198 +      ultimately show "k>k'" using rbt_lookup_keys RBT_SORTED by auto
   2.199      qed
   2.200      
   2.201 -    have DOM_T2: "!!k'. k'\<in>dom (lookup t2) \<Longrightarrow> k<k'"
   2.202 +    have DOM_T2: "!!k'. k'\<in>dom (rbt_lookup t2) \<Longrightarrow> k<k'"
   2.203      proof -
   2.204        fix k'
   2.205 -      from SORTED have "k \<guillemotleft>| t2" by simp
   2.206 -      with tree_greater_prop have "\<forall>k'\<in>set (keys t2). k<k'" by auto
   2.207 -      moreover assume "k'\<in>dom (lookup t2)"
   2.208 -      ultimately show "k<k'" using lookup_keys SORTED by auto
   2.209 +      from RBT_SORTED have "k \<guillemotleft>| t2" by simp
   2.210 +      with rbt_greater_prop have "\<forall>k'\<in>set (keys t2). k<k'" by auto
   2.211 +      moreover assume "k'\<in>dom (rbt_lookup t2)"
   2.212 +      ultimately show "k<k'" using rbt_lookup_keys RBT_SORTED by auto
   2.213      qed
   2.214      
   2.215      {
   2.216        assume C: "x<k"
   2.217 -      hence "lookup (Branch c t1 k v t2) x = lookup t1 x" by simp
   2.218 +      hence "rbt_lookup (Branch c t1 k v t2) x = rbt_lookup t1 x" by simp
   2.219        moreover from C have "x\<notin>dom [k\<mapsto>v]" by simp
   2.220 -      moreover have "x\<notin>dom (lookup t2)" proof
   2.221 -        assume "x\<in>dom (lookup t2)"
   2.222 +      moreover have "x \<notin> dom (rbt_lookup t2)"
   2.223 +      proof
   2.224 +        assume "x \<in> dom (rbt_lookup t2)"
   2.225          with DOM_T2 have "k<x" by blast
   2.226          with C show False by simp
   2.227        qed
   2.228        ultimately have ?thesis by (simp add: map_add_upd_left map_add_dom_app_simps)
   2.229      } moreover {
   2.230        assume [simp]: "x=k"
   2.231 -      hence "lookup (Branch c t1 k v t2) x = [k \<mapsto> v] x" by simp
   2.232 -      moreover have "x\<notin>dom (lookup t1)" proof
   2.233 -        assume "x\<in>dom (lookup t1)"
   2.234 +      hence "rbt_lookup (Branch c t1 k v t2) x = [k \<mapsto> v] x" by simp
   2.235 +      moreover have "x \<notin> dom (rbt_lookup t1)" 
   2.236 +      proof
   2.237 +        assume "x \<in> dom (rbt_lookup t1)"
   2.238          with DOM_T1 have "k>x" by blast
   2.239          thus False by simp
   2.240        qed
   2.241        ultimately have ?thesis by (simp add: map_add_upd_left map_add_dom_app_simps)
   2.242      } moreover {
   2.243        assume C: "x>k"
   2.244 -      hence "lookup (Branch c t1 k v t2) x = lookup t2 x" by (simp add: less_not_sym[of k x])
   2.245 +      hence "rbt_lookup (Branch c t1 k v t2) x = rbt_lookup t2 x" by (simp add: less_not_sym[of k x])
   2.246        moreover from C have "x\<notin>dom [k\<mapsto>v]" by simp
   2.247 -      moreover have "x\<notin>dom (lookup t1)" proof
   2.248 -        assume "x\<in>dom (lookup t1)"
   2.249 +      moreover have "x\<notin>dom (rbt_lookup t1)" proof
   2.250 +        assume "x\<in>dom (rbt_lookup t1)"
   2.251          with DOM_T1 have "k>x" by simp
   2.252          with C show False by simp
   2.253        qed
   2.254        ultimately have ?thesis by (simp add: map_add_upd_left map_add_dom_app_simps)
   2.255      } ultimately show ?thesis using less_linear by blast
   2.256    qed
   2.257 -  also from Branch have "lookup t2 ++ [k \<mapsto> v] ++ lookup t1 = map_of (entries (Branch c t1 k v t2))" by simp
   2.258 +  also from Branch 
   2.259 +  have "rbt_lookup t2 ++ [k \<mapsto> v] ++ rbt_lookup t1 = map_of (entries (Branch c t1 k v t2))" by simp
   2.260    finally show ?case by simp
   2.261  qed
   2.262  
   2.263 -lemma lookup_in_tree: "sorted t \<Longrightarrow> lookup t k = Some v \<longleftrightarrow> (k, v) \<in> set (entries t)"
   2.264 +lemma rbt_lookup_in_tree: "rbt_sorted t \<Longrightarrow> rbt_lookup t k = Some v \<longleftrightarrow> (k, v) \<in> set (entries t)"
   2.265    by (simp add: map_of_entries [symmetric] distinct_entries)
   2.266  
   2.267  lemma set_entries_inject:
   2.268 -  assumes sorted: "sorted t1" "sorted t2" 
   2.269 +  assumes rbt_sorted: "rbt_sorted t1" "rbt_sorted t2" 
   2.270    shows "set (entries t1) = set (entries t2) \<longleftrightarrow> entries t1 = entries t2"
   2.271  proof -
   2.272 -  from sorted have "distinct (map fst (entries t1))"
   2.273 +  from rbt_sorted have "distinct (map fst (entries t1))"
   2.274      "distinct (map fst (entries t2))"
   2.275      by (auto intro: distinct_entries)
   2.276 -  with sorted show ?thesis
   2.277 -    by (auto intro: map_sorted_distinct_set_unique sorted_entries simp add: distinct_map)
   2.278 +  with rbt_sorted show ?thesis
   2.279 +    by (auto intro: map_sorted_distinct_set_unique rbt_sorted_entries simp add: distinct_map)
   2.280  qed
   2.281  
   2.282  lemma entries_eqI:
   2.283 -  assumes sorted: "sorted t1" "sorted t2" 
   2.284 -  assumes lookup: "lookup t1 = lookup t2"
   2.285 +  assumes rbt_sorted: "rbt_sorted t1" "rbt_sorted t2" 
   2.286 +  assumes rbt_lookup: "rbt_lookup t1 = rbt_lookup t2"
   2.287    shows "entries t1 = entries t2"
   2.288  proof -
   2.289 -  from sorted lookup have "map_of (entries t1) = map_of (entries t2)"
   2.290 +  from rbt_sorted rbt_lookup have "map_of (entries t1) = map_of (entries t2)"
   2.291      by (simp add: map_of_entries)
   2.292 -  with sorted have "set (entries t1) = set (entries t2)"
   2.293 +  with rbt_sorted have "set (entries t1) = set (entries t2)"
   2.294      by (simp add: map_of_inject_set distinct_entries)
   2.295 -  with sorted show ?thesis by (simp add: set_entries_inject)
   2.296 +  with rbt_sorted show ?thesis by (simp add: set_entries_inject)
   2.297  qed
   2.298  
   2.299 -lemma entries_lookup:
   2.300 -  assumes "sorted t1" "sorted t2" 
   2.301 -  shows "entries t1 = entries t2 \<longleftrightarrow> lookup t1 = lookup t2"
   2.302 +lemma entries_rbt_lookup:
   2.303 +  assumes "rbt_sorted t1" "rbt_sorted t2" 
   2.304 +  shows "entries t1 = entries t2 \<longleftrightarrow> rbt_lookup t1 = rbt_lookup t2"
   2.305    using assms by (auto intro: entries_eqI simp add: map_of_entries [symmetric])
   2.306  
   2.307 -lemma lookup_from_in_tree: 
   2.308 -  assumes "sorted t1" "sorted t2" 
   2.309 -  and "\<And>v. (k\<Colon>'a\<Colon>linorder, v) \<in> set (entries t1) \<longleftrightarrow> (k, v) \<in> set (entries t2)" 
   2.310 -  shows "lookup t1 k = lookup t2 k"
   2.311 +lemma rbt_lookup_from_in_tree: 
   2.312 +  assumes "rbt_sorted t1" "rbt_sorted t2" 
   2.313 +  and "\<And>v. (k, v) \<in> set (entries t1) \<longleftrightarrow> (k, v) \<in> set (entries t2)" 
   2.314 +  shows "rbt_lookup t1 k = rbt_lookup t2 k"
   2.315  proof -
   2.316 -  from assms have "k \<in> dom (lookup t1) \<longleftrightarrow> k \<in> dom (lookup t2)"
   2.317 -    by (simp add: keys_entries lookup_keys)
   2.318 -  with assms show ?thesis by (auto simp add: lookup_in_tree [symmetric])
   2.319 +  from assms have "k \<in> dom (rbt_lookup t1) \<longleftrightarrow> k \<in> dom (rbt_lookup t2)"
   2.320 +    by (simp add: keys_entries rbt_lookup_keys)
   2.321 +  with assms show ?thesis by (auto simp add: rbt_lookup_in_tree [symmetric])
   2.322  qed
   2.323  
   2.324 +end
   2.325  
   2.326  subsubsection {* Red-black properties *}
   2.327  
   2.328 @@ -290,15 +309,18 @@
   2.329    "inv2 Empty = True"
   2.330  | "inv2 (Branch c lt k v rt) = (inv2 lt \<and> inv2 rt \<and> bheight lt = bheight rt)"
   2.331  
   2.332 -definition is_rbt :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> bool" where
   2.333 -  "is_rbt t \<longleftrightarrow> inv1 t \<and> inv2 t \<and> color_of t = B \<and> sorted t"
   2.334 +context ord begin
   2.335  
   2.336 -lemma is_rbt_sorted [simp]:
   2.337 -  "is_rbt t \<Longrightarrow> sorted t" by (simp add: is_rbt_def)
   2.338 +definition is_rbt :: "('a, 'b) rbt \<Rightarrow> bool" where
   2.339 +  "is_rbt t \<longleftrightarrow> inv1 t \<and> inv2 t \<and> color_of t = B \<and> rbt_sorted t"
   2.340 +
   2.341 +lemma is_rbt_rbt_sorted [simp]:
   2.342 +  "is_rbt t \<Longrightarrow> rbt_sorted t" by (simp add: is_rbt_def)
   2.343  
   2.344  theorem Empty_is_rbt [simp]:
   2.345    "is_rbt Empty" by (simp add: is_rbt_def)
   2.346  
   2.347 +end
   2.348  
   2.349  subsection {* Insertion *}
   2.350  
   2.351 @@ -324,61 +346,65 @@
   2.352    using assms
   2.353    by (induct l k v r rule: balance.induct) auto
   2.354  
   2.355 -lemma balance_tree_greater[simp]: "(v \<guillemotleft>| balance a k x b) = (v \<guillemotleft>| a \<and> v \<guillemotleft>| b \<and> v < k)" 
   2.356 +context ord begin
   2.357 +
   2.358 +lemma balance_rbt_greater[simp]: "(v \<guillemotleft>| balance a k x b) = (v \<guillemotleft>| a \<and> v \<guillemotleft>| b \<and> v < k)" 
   2.359    by (induct a k x b rule: balance.induct) auto
   2.360  
   2.361 -lemma balance_tree_less[simp]: "(balance a k x b |\<guillemotleft> v) = (a |\<guillemotleft> v \<and> b |\<guillemotleft> v \<and> k < v)"
   2.362 +lemma balance_rbt_less[simp]: "(balance a k x b |\<guillemotleft> v) = (a |\<guillemotleft> v \<and> b |\<guillemotleft> v \<and> k < v)"
   2.363    by (induct a k x b rule: balance.induct) auto
   2.364  
   2.365 -lemma balance_sorted: 
   2.366 -  fixes k :: "'a::linorder"
   2.367 -  assumes "sorted l" "sorted r" "l |\<guillemotleft> k" "k \<guillemotleft>| r"
   2.368 -  shows "sorted (balance l k v r)"
   2.369 +end
   2.370 +
   2.371 +lemma (in linorder) balance_rbt_sorted: 
   2.372 +  fixes k :: "'a"
   2.373 +  assumes "rbt_sorted l" "rbt_sorted r" "l |\<guillemotleft> k" "k \<guillemotleft>| r"
   2.374 +  shows "rbt_sorted (balance l k v r)"
   2.375  using assms proof (induct l k v r rule: balance.induct)
   2.376    case ("2_2" a x w b y t c z s va vb vd vc)
   2.377    hence "y < z \<and> z \<guillemotleft>| Branch B va vb vd vc" 
   2.378 -    by (auto simp add: tree_ord_props)
   2.379 -  hence "tree_greater y (Branch B va vb vd vc)" by (blast dest: tree_greater_trans)
   2.380 +    by (auto simp add: rbt_ord_props)
   2.381 +  hence "y \<guillemotleft>| (Branch B va vb vd vc)" by (blast dest: rbt_greater_trans)
   2.382    with "2_2" show ?case by simp
   2.383  next
   2.384    case ("3_2" va vb vd vc x w b y s c z)
   2.385 -  from "3_2" have "x < y \<and> tree_less x (Branch B va vb vd vc)" 
   2.386 +  from "3_2" have "x < y \<and> Branch B va vb vd vc |\<guillemotleft> x" 
   2.387      by simp
   2.388 -  hence "tree_less y (Branch B va vb vd vc)" by (blast dest: tree_less_trans)
   2.389 +  hence "Branch B va vb vd vc |\<guillemotleft> y" by (blast dest: rbt_less_trans)
   2.390    with "3_2" show ?case by simp
   2.391  next
   2.392    case ("3_3" x w b y s c z t va vb vd vc)
   2.393 -  from "3_3" have "y < z \<and> tree_greater z (Branch B va vb vd vc)" by simp
   2.394 -  hence "tree_greater y (Branch B va vb vd vc)" by (blast dest: tree_greater_trans)
   2.395 +  from "3_3" have "y < z \<and> z \<guillemotleft>| Branch B va vb vd vc" by simp
   2.396 +  hence "y \<guillemotleft>| Branch B va vb vd vc" by (blast dest: rbt_greater_trans)
   2.397    with "3_3" show ?case by simp
   2.398  next
   2.399    case ("3_4" vd ve vg vf x w b y s c z t va vb vii vc)
   2.400 -  hence "x < y \<and> tree_less x (Branch B vd ve vg vf)" by simp
   2.401 -  hence 1: "tree_less y (Branch B vd ve vg vf)" by (blast dest: tree_less_trans)
   2.402 -  from "3_4" have "y < z \<and> tree_greater z (Branch B va vb vii vc)" by simp
   2.403 -  hence "tree_greater y (Branch B va vb vii vc)" by (blast dest: tree_greater_trans)
   2.404 +  hence "x < y \<and> Branch B vd ve vg vf |\<guillemotleft> x" by simp
   2.405 +  hence 1: "Branch B vd ve vg vf |\<guillemotleft> y" by (blast dest: rbt_less_trans)
   2.406 +  from "3_4" have "y < z \<and> z \<guillemotleft>| Branch B va vb vii vc" by simp
   2.407 +  hence "y \<guillemotleft>| Branch B va vb vii vc" by (blast dest: rbt_greater_trans)
   2.408    with 1 "3_4" show ?case by simp
   2.409  next
   2.410    case ("4_2" va vb vd vc x w b y s c z t dd)
   2.411 -  hence "x < y \<and> tree_less x (Branch B va vb vd vc)" by simp
   2.412 -  hence "tree_less y (Branch B va vb vd vc)" by (blast dest: tree_less_trans)
   2.413 +  hence "x < y \<and> Branch B va vb vd vc |\<guillemotleft> x" by simp
   2.414 +  hence "Branch B va vb vd vc |\<guillemotleft> y" by (blast dest: rbt_less_trans)
   2.415    with "4_2" show ?case by simp
   2.416  next
   2.417    case ("5_2" x w b y s c z t va vb vd vc)
   2.418 -  hence "y < z \<and> tree_greater z (Branch B va vb vd vc)" by simp
   2.419 -  hence "tree_greater y (Branch B va vb vd vc)" by (blast dest: tree_greater_trans)
   2.420 +  hence "y < z \<and> z \<guillemotleft>| Branch B va vb vd vc" by simp
   2.421 +  hence "y \<guillemotleft>| Branch B va vb vd vc" by (blast dest: rbt_greater_trans)
   2.422    with "5_2" show ?case by simp
   2.423  next
   2.424    case ("5_3" va vb vd vc x w b y s c z t)
   2.425 -  hence "x < y \<and> tree_less x (Branch B va vb vd vc)" by simp
   2.426 -  hence "tree_less y (Branch B va vb vd vc)" by (blast dest: tree_less_trans)
   2.427 +  hence "x < y \<and> Branch B va vb vd vc |\<guillemotleft> x" by simp
   2.428 +  hence "Branch B va vb vd vc |\<guillemotleft> y" by (blast dest: rbt_less_trans)
   2.429    with "5_3" show ?case by simp
   2.430  next
   2.431    case ("5_4" va vb vg vc x w b y s c z t vd ve vii vf)
   2.432 -  hence "x < y \<and> tree_less x (Branch B va vb vg vc)" by simp
   2.433 -  hence 1: "tree_less y (Branch B va vb vg vc)" by (blast dest: tree_less_trans)
   2.434 -  from "5_4" have "y < z \<and> tree_greater z (Branch B vd ve vii vf)" by simp
   2.435 -  hence "tree_greater y (Branch B vd ve vii vf)" by (blast dest: tree_greater_trans)
   2.436 +  hence "x < y \<and> Branch B va vb vg vc |\<guillemotleft> x" by simp
   2.437 +  hence 1: "Branch B va vb vg vc |\<guillemotleft> y" by (blast dest: rbt_less_trans)
   2.438 +  from "5_4" have "y < z \<and> z \<guillemotleft>| Branch B vd ve vii vf" by simp
   2.439 +  hence "y \<guillemotleft>| Branch B vd ve vii vf" by (blast dest: rbt_greater_trans)
   2.440    with 1 "5_4" show ?case by simp
   2.441  qed simp+
   2.442  
   2.443 @@ -394,11 +420,11 @@
   2.444    "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"
   2.445    by (auto simp add: keys_def)
   2.446  
   2.447 -lemma lookup_balance[simp]: 
   2.448 -fixes k :: "'a::linorder"
   2.449 -assumes "sorted l" "sorted r" "l |\<guillemotleft> k" "k \<guillemotleft>| r"
   2.450 -shows "lookup (balance l k v r) x = lookup (Branch B l k v r) x"
   2.451 -by (rule lookup_from_in_tree) (auto simp:assms balance_in_tree balance_sorted)
   2.452 +lemma (in linorder) rbt_lookup_balance[simp]: 
   2.453 +fixes k :: "'a"
   2.454 +assumes "rbt_sorted l" "rbt_sorted r" "l |\<guillemotleft> k" "k \<guillemotleft>| r"
   2.455 +shows "rbt_lookup (balance l k v r) x = rbt_lookup (Branch B l k v r) x"
   2.456 +by (rule rbt_lookup_from_in_tree) (auto simp:assms balance_in_tree balance_rbt_sorted)
   2.457  
   2.458  primrec paint :: "color \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
   2.459  where
   2.460 @@ -409,95 +435,112 @@
   2.461  lemma paint_inv1[simp]: "inv1l t \<Longrightarrow> inv1 (paint B t)" by (cases t) auto
   2.462  lemma paint_inv2[simp]: "inv2 t \<Longrightarrow> inv2 (paint c t)" by (cases t) auto
   2.463  lemma paint_color_of[simp]: "color_of (paint B t) = B" by (cases t) auto
   2.464 -lemma paint_sorted[simp]: "sorted t \<Longrightarrow> sorted (paint c t)" by (cases t) auto
   2.465  lemma paint_in_tree[simp]: "entry_in_tree k x (paint c t) = entry_in_tree k x t" by (cases t) auto
   2.466 -lemma paint_lookup[simp]: "lookup (paint c t) = lookup t" by (rule ext) (cases t, auto)
   2.467 -lemma paint_tree_greater[simp]: "(v \<guillemotleft>| paint c t) = (v \<guillemotleft>| t)" by (cases t) auto
   2.468 -lemma paint_tree_less[simp]: "(paint c t |\<guillemotleft> v) = (t |\<guillemotleft> v)" by (cases t) auto
   2.469 +
   2.470 +context ord begin
   2.471 +
   2.472 +lemma paint_rbt_sorted[simp]: "rbt_sorted t \<Longrightarrow> rbt_sorted (paint c t)" by (cases t) auto
   2.473 +lemma paint_rbt_lookup[simp]: "rbt_lookup (paint c t) = rbt_lookup t" by (rule ext) (cases t, auto)
   2.474 +lemma paint_rbt_greater[simp]: "(v \<guillemotleft>| paint c t) = (v \<guillemotleft>| t)" by (cases t) auto
   2.475 +lemma paint_rbt_less[simp]: "(paint c t |\<guillemotleft> v) = (t |\<guillemotleft> v)" by (cases t) auto
   2.476  
   2.477  fun
   2.478 -  ins :: "('a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
   2.479 +  rbt_ins :: "('a \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
   2.480  where
   2.481 -  "ins f k v Empty = Branch R Empty k v Empty" |
   2.482 -  "ins f k v (Branch B l x y r) = (if k < x then balance (ins f k v l) x y r
   2.483 -                               else if k > x then balance l x y (ins f k v r)
   2.484 -                               else Branch B l x (f k y v) r)" |
   2.485 -  "ins f k v (Branch R l x y r) = (if k < x then Branch R (ins f k v l) x y r
   2.486 -                               else if k > x then Branch R l x y (ins f k v r)
   2.487 -                               else Branch R l x (f k y v) r)"
   2.488 +  "rbt_ins f k v Empty = Branch R Empty k v Empty" |
   2.489 +  "rbt_ins f k v (Branch B l x y r) = (if k < x then balance (rbt_ins f k v l) x y r
   2.490 +                                       else if k > x then balance l x y (rbt_ins f k v r)
   2.491 +                                       else Branch B l x (f k y v) r)" |
   2.492 +  "rbt_ins f k v (Branch R l x y r) = (if k < x then Branch R (rbt_ins f k v l) x y r
   2.493 +                                       else if k > x then Branch R l x y (rbt_ins f k v r)
   2.494 +                                       else Branch R l x (f k y v) r)"
   2.495  
   2.496  lemma ins_inv1_inv2: 
   2.497    assumes "inv1 t" "inv2 t"
   2.498 -  shows "inv2 (ins f k x t)" "bheight (ins f k x t) = bheight t" 
   2.499 -  "color_of t = B \<Longrightarrow> inv1 (ins f k x t)" "inv1l (ins f k x t)"
   2.500 +  shows "inv2 (rbt_ins f k x t)" "bheight (rbt_ins f k x t) = bheight t" 
   2.501 +  "color_of t = B \<Longrightarrow> inv1 (rbt_ins f k x t)" "inv1l (rbt_ins f k x t)"
   2.502    using assms
   2.503 -  by (induct f k x t rule: ins.induct) (auto simp: balance_inv1 balance_inv2 balance_bheight)
   2.504 +  by (induct f k x t rule: rbt_ins.induct) (auto simp: balance_inv1 balance_inv2 balance_bheight)
   2.505 +
   2.506 +end
   2.507 +
   2.508 +context linorder begin
   2.509  
   2.510 -lemma ins_tree_greater[simp]: "(v \<guillemotleft>| ins f k x t) = (v \<guillemotleft>| t \<and> k > v)"
   2.511 -  by (induct f k x t rule: ins.induct) auto
   2.512 -lemma ins_tree_less[simp]: "(ins f k x t |\<guillemotleft> v) = (t |\<guillemotleft> v \<and> k < v)"
   2.513 -  by (induct f k x t rule: ins.induct) auto
   2.514 -lemma ins_sorted[simp]: "sorted t \<Longrightarrow> sorted (ins f k x t)"
   2.515 -  by (induct f k x t rule: ins.induct) (auto simp: balance_sorted)
   2.516 +lemma ins_rbt_greater[simp]: "(v \<guillemotleft>| rbt_ins f (k :: 'a) x t) = (v \<guillemotleft>| t \<and> k > v)"
   2.517 +  by (induct f k x t rule: rbt_ins.induct) auto
   2.518 +lemma ins_rbt_less[simp]: "(rbt_ins f k x t |\<guillemotleft> v) = (t |\<guillemotleft> v \<and> k < v)"
   2.519 +  by (induct f k x t rule: rbt_ins.induct) auto
   2.520 +lemma ins_rbt_sorted[simp]: "rbt_sorted t \<Longrightarrow> rbt_sorted (rbt_ins f k x t)"
   2.521 +  by (induct f k x t rule: rbt_ins.induct) (auto simp: balance_rbt_sorted)
   2.522  
   2.523 -lemma keys_ins: "set (keys (ins f k v t)) = { k } \<union> set (keys t)"
   2.524 -  by (induct f k v t rule: ins.induct) auto
   2.525 +lemma keys_ins: "set (keys (rbt_ins f k v t)) = { k } \<union> set (keys t)"
   2.526 +  by (induct f k v t rule: rbt_ins.induct) auto
   2.527  
   2.528 -lemma lookup_ins: 
   2.529 -  fixes k :: "'a::linorder"
   2.530 -  assumes "sorted t"
   2.531 -  shows "lookup (ins f k v t) x = ((lookup t)(k |-> case lookup t k of None \<Rightarrow> v 
   2.532 -                                                       | Some w \<Rightarrow> f k w v)) x"
   2.533 -using assms by (induct f k v t rule: ins.induct) auto
   2.534 +lemma rbt_lookup_ins: 
   2.535 +  fixes k :: "'a"
   2.536 +  assumes "rbt_sorted t"
   2.537 +  shows "rbt_lookup (rbt_ins f k v t) x = ((rbt_lookup t)(k |-> case rbt_lookup t k of None \<Rightarrow> v 
   2.538 +                                                                | Some w \<Rightarrow> f k w v)) x"
   2.539 +using assms by (induct f k v t rule: rbt_ins.induct) auto
   2.540 +
   2.541 +end
   2.542 +
   2.543 +context ord begin
   2.544 +
   2.545 +definition rbt_insert_with_key :: "('a \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
   2.546 +where "rbt_insert_with_key f k v t = paint B (rbt_ins f k v t)"
   2.547 +
   2.548 +definition rbt_insertw_def: "rbt_insert_with f = rbt_insert_with_key (\<lambda>_. f)"
   2.549  
   2.550 -definition
   2.551 -  insert_with_key :: "('a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
   2.552 -where
   2.553 -  "insert_with_key f k v t = paint B (ins f k v t)"
   2.554 +definition rbt_insert :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" where
   2.555 +  "rbt_insert = rbt_insert_with_key (\<lambda>_ _ nv. nv)"
   2.556 +
   2.557 +end
   2.558 +
   2.559 +context linorder begin
   2.560  
   2.561 -lemma insertwk_sorted: "sorted t \<Longrightarrow> sorted (insert_with_key f k x t)"
   2.562 -  by (auto simp: insert_with_key_def)
   2.563 +lemma rbt_insertwk_rbt_sorted: "rbt_sorted t \<Longrightarrow> rbt_sorted (rbt_insert_with_key f (k :: 'a) x t)"
   2.564 +  by (auto simp: rbt_insert_with_key_def)
   2.565  
   2.566 -theorem insertwk_is_rbt: 
   2.567 +theorem rbt_insertwk_is_rbt: 
   2.568    assumes inv: "is_rbt t" 
   2.569 -  shows "is_rbt (insert_with_key f k x t)"
   2.570 +  shows "is_rbt (rbt_insert_with_key f k x t)"
   2.571  using assms
   2.572 -unfolding insert_with_key_def is_rbt_def
   2.573 +unfolding rbt_insert_with_key_def is_rbt_def
   2.574  by (auto simp: ins_inv1_inv2)
   2.575  
   2.576 -lemma lookup_insertwk: 
   2.577 -  assumes "sorted t"
   2.578 -  shows "lookup (insert_with_key f k v t) x = ((lookup t)(k |-> case lookup t k of None \<Rightarrow> v 
   2.579 +lemma rbt_lookup_rbt_insertwk: 
   2.580 +  assumes "rbt_sorted t"
   2.581 +  shows "rbt_lookup (rbt_insert_with_key f k v t) x = ((rbt_lookup t)(k |-> case rbt_lookup t k of None \<Rightarrow> v 
   2.582                                                         | Some w \<Rightarrow> f k w v)) x"
   2.583 -unfolding insert_with_key_def using assms
   2.584 -by (simp add:lookup_ins)
   2.585 +unfolding rbt_insert_with_key_def using assms
   2.586 +by (simp add:rbt_lookup_ins)
   2.587  
   2.588 -definition
   2.589 -  insertw_def: "insert_with f = insert_with_key (\<lambda>_. f)"
   2.590 +lemma rbt_insertw_rbt_sorted: "rbt_sorted t \<Longrightarrow> rbt_sorted (rbt_insert_with f k v t)" 
   2.591 +  by (simp add: rbt_insertwk_rbt_sorted rbt_insertw_def)
   2.592 +theorem rbt_insertw_is_rbt: "is_rbt t \<Longrightarrow> is_rbt (rbt_insert_with f k v t)"
   2.593 +  by (simp add: rbt_insertwk_is_rbt rbt_insertw_def)
   2.594  
   2.595 -lemma insertw_sorted: "sorted t \<Longrightarrow> sorted (insert_with f k v t)" by (simp add: insertwk_sorted insertw_def)
   2.596 -theorem insertw_is_rbt: "is_rbt t \<Longrightarrow> is_rbt (insert_with f k v t)" by (simp add: insertwk_is_rbt insertw_def)
   2.597 -
   2.598 -lemma lookup_insertw:
   2.599 +lemma rbt_lookup_rbt_insertw:
   2.600    assumes "is_rbt t"
   2.601 -  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))"
   2.602 +  shows "rbt_lookup (rbt_insert_with f k v t) = (rbt_lookup t)(k \<mapsto> (if k:dom (rbt_lookup t) then f (the (rbt_lookup t k)) v else v))"
   2.603  using assms
   2.604 -unfolding insertw_def
   2.605 -by (rule_tac ext) (cases "lookup t k", auto simp:lookup_insertwk dom_def)
   2.606 +unfolding rbt_insertw_def
   2.607 +by (rule_tac ext) (cases "rbt_lookup t k", auto simp:rbt_lookup_rbt_insertwk dom_def)
   2.608  
   2.609 -definition insert :: "'a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" where
   2.610 -  "insert = insert_with_key (\<lambda>_ _ nv. nv)"
   2.611 +lemma rbt_insert_rbt_sorted: "rbt_sorted t \<Longrightarrow> rbt_sorted (rbt_insert k v t)"
   2.612 +  by (simp add: rbt_insertwk_rbt_sorted rbt_insert_def)
   2.613 +theorem rbt_insert_is_rbt [simp]: "is_rbt t \<Longrightarrow> is_rbt (rbt_insert k v t)"
   2.614 +  by (simp add: rbt_insertwk_is_rbt rbt_insert_def)
   2.615  
   2.616 -lemma insert_sorted: "sorted t \<Longrightarrow> sorted (insert k v t)" by (simp add: insertwk_sorted insert_def)
   2.617 -theorem insert_is_rbt [simp]: "is_rbt t \<Longrightarrow> is_rbt (insert k v t)" by (simp add: insertwk_is_rbt insert_def)
   2.618 -
   2.619 -lemma lookup_insert: 
   2.620 +lemma rbt_lookup_rbt_insert: 
   2.621    assumes "is_rbt t"
   2.622 -  shows "lookup (insert k v t) = (lookup t)(k\<mapsto>v)"
   2.623 -unfolding insert_def
   2.624 +  shows "rbt_lookup (rbt_insert k v t) = (rbt_lookup t)(k\<mapsto>v)"
   2.625 +unfolding rbt_insert_def
   2.626  using assms
   2.627 -by (rule_tac ext) (simp add: lookup_insertwk split:option.split)
   2.628 +by (rule_tac ext) (simp add: rbt_lookup_rbt_insertwk split:option.split)
   2.629  
   2.630 +end
   2.631  
   2.632  subsection {* Deletion *}
   2.633  
   2.634 @@ -532,26 +575,31 @@
   2.635  lemma balance_left_inv1l: "\<lbrakk> inv1l lt; inv1 rt \<rbrakk> \<Longrightarrow> inv1l (balance_left lt k x rt)"
   2.636  by (induct lt k x rt rule: balance_left.induct) (auto simp: balance_inv1)
   2.637  
   2.638 -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)"
   2.639 +lemma (in linorder) balance_left_rbt_sorted: 
   2.640 +  "\<lbrakk> rbt_sorted l; rbt_sorted r; rbt_less k l; k \<guillemotleft>| r \<rbrakk> \<Longrightarrow> rbt_sorted (balance_left l k v r)"
   2.641  apply (induct l k v r rule: balance_left.induct)
   2.642 -apply (auto simp: balance_sorted)
   2.643 -apply (unfold tree_greater_prop tree_less_prop)
   2.644 +apply (auto simp: balance_rbt_sorted)
   2.645 +apply (unfold rbt_greater_prop rbt_less_prop)
   2.646  by force+
   2.647  
   2.648 -lemma balance_left_tree_greater: 
   2.649 -  fixes k :: "'a::order"
   2.650 +context order begin
   2.651 +
   2.652 +lemma balance_left_rbt_greater: 
   2.653 +  fixes k :: "'a"
   2.654    assumes "k \<guillemotleft>| a" "k \<guillemotleft>| b" "k < x" 
   2.655    shows "k \<guillemotleft>| balance_left a x t b"
   2.656  using assms 
   2.657  by (induct a x t b rule: balance_left.induct) auto
   2.658  
   2.659 -lemma balance_left_tree_less: 
   2.660 -  fixes k :: "'a::order"
   2.661 +lemma balance_left_rbt_less: 
   2.662 +  fixes k :: "'a"
   2.663    assumes "a |\<guillemotleft> k" "b |\<guillemotleft> k" "x < k" 
   2.664    shows "balance_left a x t b |\<guillemotleft> k"
   2.665  using assms
   2.666  by (induct a x t b rule: balance_left.induct) auto
   2.667  
   2.668 +end
   2.669 +
   2.670  lemma balance_left_in_tree: 
   2.671    assumes "inv1l l" "inv1 r" "bheight l + 1 = bheight r"
   2.672    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)"
   2.673 @@ -578,24 +626,29 @@
   2.674  lemma balance_right_inv1l: "\<lbrakk> inv1 lt; inv1l rt \<rbrakk> \<Longrightarrow>inv1l (balance_right lt k x rt)"
   2.675  by (induct lt k x rt rule: balance_right.induct) (auto simp: balance_inv1)
   2.676  
   2.677 -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)"
   2.678 +lemma (in linorder) balance_right_rbt_sorted:
   2.679 +  "\<lbrakk> rbt_sorted l; rbt_sorted r; rbt_less k l; k \<guillemotleft>| r \<rbrakk> \<Longrightarrow> rbt_sorted (balance_right l k v r)"
   2.680  apply (induct l k v r rule: balance_right.induct)
   2.681 -apply (auto simp:balance_sorted)
   2.682 -apply (unfold tree_less_prop tree_greater_prop)
   2.683 +apply (auto simp:balance_rbt_sorted)
   2.684 +apply (unfold rbt_less_prop rbt_greater_prop)
   2.685  by force+
   2.686  
   2.687 -lemma balance_right_tree_greater: 
   2.688 -  fixes k :: "'a::order"
   2.689 +context order begin
   2.690 +
   2.691 +lemma balance_right_rbt_greater: 
   2.692 +  fixes k :: "'a"
   2.693    assumes "k \<guillemotleft>| a" "k \<guillemotleft>| b" "k < x" 
   2.694    shows "k \<guillemotleft>| balance_right a x t b"
   2.695  using assms by (induct a x t b rule: balance_right.induct) auto
   2.696  
   2.697 -lemma balance_right_tree_less: 
   2.698 -  fixes k :: "'a::order"
   2.699 +lemma balance_right_rbt_less: 
   2.700 +  fixes k :: "'a"
   2.701    assumes "a |\<guillemotleft> k" "b |\<guillemotleft> k" "x < k" 
   2.702    shows "balance_right a x t b |\<guillemotleft> k"
   2.703  using assms by (induct a x t b rule: balance_right.induct) auto
   2.704  
   2.705 +end
   2.706 +
   2.707  lemma balance_right_in_tree:
   2.708    assumes "inv1 l" "inv1l r" "bheight l = bheight r + 1" "inv2 l" "inv2 r"
   2.709    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)"
   2.710 @@ -607,11 +660,11 @@
   2.711    "combine Empty x = x" 
   2.712  | "combine x Empty = x" 
   2.713  | "combine (Branch R a k x b) (Branch R c s y d) = (case (combine b c) of
   2.714 -                                      Branch R b2 t z c2 \<Rightarrow> (Branch R (Branch R a k x b2) t z (Branch R c2 s y d)) |
   2.715 -                                      bc \<Rightarrow> Branch R a k x (Branch R bc s y d))" 
   2.716 +                                    Branch R b2 t z c2 \<Rightarrow> (Branch R (Branch R a k x b2) t z (Branch R c2 s y d)) |
   2.717 +                                    bc \<Rightarrow> Branch R a k x (Branch R bc s y d))" 
   2.718  | "combine (Branch B a k x b) (Branch B c s y d) = (case (combine b c) of
   2.719 -                                      Branch R b2 t z c2 \<Rightarrow> Branch R (Branch B a k x b2) t z (Branch B c2 s y d) |
   2.720 -                                      bc \<Rightarrow> balance_left a k x (Branch B bc s y d))" 
   2.721 +                                    Branch R b2 t z c2 \<Rightarrow> Branch R (Branch B a k x b2) t z (Branch B c2 s y d) |
   2.722 +                                    bc \<Rightarrow> balance_left a k x (Branch B bc s y d))" 
   2.723  | "combine a (Branch R b k x c) = Branch R (combine a b) k x c" 
   2.724  | "combine (Branch R a k x b) c = Branch R a k x (combine b c)" 
   2.725  
   2.726 @@ -630,26 +683,28 @@
   2.727  by (induct lt rt rule: combine.induct)
   2.728     (auto simp: balance_left_inv1 split: rbt.splits color.splits)
   2.729  
   2.730 -lemma combine_tree_greater[simp]: 
   2.731 -  fixes k :: "'a::linorder"
   2.732 +context linorder begin
   2.733 +
   2.734 +lemma combine_rbt_greater[simp]: 
   2.735 +  fixes k :: "'a"
   2.736    assumes "k \<guillemotleft>| l" "k \<guillemotleft>| r" 
   2.737    shows "k \<guillemotleft>| combine l r"
   2.738  using assms 
   2.739  by (induct l r rule: combine.induct)
   2.740 -   (auto simp: balance_left_tree_greater split:rbt.splits color.splits)
   2.741 +   (auto simp: balance_left_rbt_greater split:rbt.splits color.splits)
   2.742  
   2.743 -lemma combine_tree_less[simp]: 
   2.744 -  fixes k :: "'a::linorder"
   2.745 +lemma combine_rbt_less[simp]: 
   2.746 +  fixes k :: "'a"
   2.747    assumes "l |\<guillemotleft> k" "r |\<guillemotleft> k" 
   2.748    shows "combine l r |\<guillemotleft> k"
   2.749  using assms 
   2.750  by (induct l r rule: combine.induct)
   2.751 -   (auto simp: balance_left_tree_less split:rbt.splits color.splits)
   2.752 +   (auto simp: balance_left_rbt_less split:rbt.splits color.splits)
   2.753  
   2.754 -lemma combine_sorted: 
   2.755 -  fixes k :: "'a::linorder"
   2.756 -  assumes "sorted l" "sorted r" "l |\<guillemotleft> k" "k \<guillemotleft>| r"
   2.757 -  shows "sorted (combine l r)"
   2.758 +lemma combine_rbt_sorted: 
   2.759 +  fixes k :: "'a"
   2.760 +  assumes "rbt_sorted l" "rbt_sorted r" "l |\<guillemotleft> k" "k \<guillemotleft>| r"
   2.761 +  shows "rbt_sorted (combine l r)"
   2.762  using assms proof (induct l r rule: combine.induct)
   2.763    case (3 a x v b c y w d)
   2.764    hence ineqs: "a |\<guillemotleft> x" "x \<guillemotleft>| b" "b |\<guillemotleft> k" "k \<guillemotleft>| c" "c |\<guillemotleft> y" "y \<guillemotleft>| d"
   2.765 @@ -657,48 +712,52 @@
   2.766    with 3
   2.767    show ?case
   2.768      by (cases "combine b c" rule: rbt_cases)
   2.769 -      (auto, (metis combine_tree_greater combine_tree_less ineqs ineqs tree_less_simps(2) tree_greater_simps(2) tree_greater_trans tree_less_trans)+)
   2.770 +      (auto, (metis combine_rbt_greater combine_rbt_less ineqs ineqs rbt_less_simps(2) rbt_greater_simps(2) rbt_greater_trans rbt_less_trans)+)
   2.771  next
   2.772    case (4 a x v b c y w d)
   2.773 -  hence "x < k \<and> tree_greater k c" by simp
   2.774 -  hence "tree_greater x c" by (blast dest: tree_greater_trans)
   2.775 -  with 4 have 2: "tree_greater x (combine b c)" by (simp add: combine_tree_greater)
   2.776 -  from 4 have "k < y \<and> tree_less k b" by simp
   2.777 -  hence "tree_less y b" by (blast dest: tree_less_trans)
   2.778 -  with 4 have 3: "tree_less y (combine b c)" by (simp add: combine_tree_less)
   2.779 +  hence "x < k \<and> rbt_greater k c" by simp
   2.780 +  hence "rbt_greater x c" by (blast dest: rbt_greater_trans)
   2.781 +  with 4 have 2: "rbt_greater x (combine b c)" by (simp add: combine_rbt_greater)
   2.782 +  from 4 have "k < y \<and> rbt_less k b" by simp
   2.783 +  hence "rbt_less y b" by (blast dest: rbt_less_trans)
   2.784 +  with 4 have 3: "rbt_less y (combine b c)" by (simp add: combine_rbt_less)
   2.785    show ?case
   2.786    proof (cases "combine b c" rule: rbt_cases)
   2.787      case Empty
   2.788 -    from 4 have "x < y \<and> tree_greater y d" by auto
   2.789 -    hence "tree_greater x d" by (blast dest: tree_greater_trans)
   2.790 -    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
   2.791 -    with Empty show ?thesis by (simp add: balance_left_sorted)
   2.792 +    from 4 have "x < y \<and> rbt_greater y d" by auto
   2.793 +    hence "rbt_greater x d" by (blast dest: rbt_greater_trans)
   2.794 +    with 4 Empty have "rbt_sorted a" and "rbt_sorted (Branch B Empty y w d)"
   2.795 +      and "rbt_less x a" and "rbt_greater x (Branch B Empty y w d)" by auto
   2.796 +    with Empty show ?thesis by (simp add: balance_left_rbt_sorted)
   2.797    next
   2.798      case (Red lta va ka rta)
   2.799 -    with 2 4 have "x < va \<and> tree_less x a" by simp
   2.800 -    hence 5: "tree_less va a" by (blast dest: tree_less_trans)
   2.801 -    from Red 3 4 have "va < y \<and> tree_greater y d" by simp
   2.802 -    hence "tree_greater va d" by (blast dest: tree_greater_trans)
   2.803 +    with 2 4 have "x < va \<and> rbt_less x a" by simp
   2.804 +    hence 5: "rbt_less va a" by (blast dest: rbt_less_trans)
   2.805 +    from Red 3 4 have "va < y \<and> rbt_greater y d" by simp
   2.806 +    hence "rbt_greater va d" by (blast dest: rbt_greater_trans)
   2.807      with Red 2 3 4 5 show ?thesis by simp
   2.808    next
   2.809      case (Black lta va ka rta)
   2.810 -    from 4 have "x < y \<and> tree_greater y d" by auto
   2.811 -    hence "tree_greater x d" by (blast dest: tree_greater_trans)
   2.812 -    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
   2.813 -    with Black show ?thesis by (simp add: balance_left_sorted)
   2.814 +    from 4 have "x < y \<and> rbt_greater y d" by auto
   2.815 +    hence "rbt_greater x d" by (blast dest: rbt_greater_trans)
   2.816 +    with Black 2 3 4 have "rbt_sorted a" and "rbt_sorted (Branch B (combine b c) y w d)" 
   2.817 +      and "rbt_less x a" and "rbt_greater x (Branch B (combine b c) y w d)" by auto
   2.818 +    with Black show ?thesis by (simp add: balance_left_rbt_sorted)
   2.819    qed
   2.820  next
   2.821    case (5 va vb vd vc b x w c)
   2.822 -  hence "k < x \<and> tree_less k (Branch B va vb vd vc)" by simp
   2.823 -  hence "tree_less x (Branch B va vb vd vc)" by (blast dest: tree_less_trans)
   2.824 -  with 5 show ?case by (simp add: combine_tree_less)
   2.825 +  hence "k < x \<and> rbt_less k (Branch B va vb vd vc)" by simp
   2.826 +  hence "rbt_less x (Branch B va vb vd vc)" by (blast dest: rbt_less_trans)
   2.827 +  with 5 show ?case by (simp add: combine_rbt_less)
   2.828  next
   2.829    case (6 a x v b va vb vd vc)
   2.830 -  hence "x < k \<and> tree_greater k (Branch B va vb vd vc)" by simp
   2.831 -  hence "tree_greater x (Branch B va vb vd vc)" by (blast dest: tree_greater_trans)
   2.832 -  with 6 show ?case by (simp add: combine_tree_greater)
   2.833 +  hence "x < k \<and> rbt_greater k (Branch B va vb vd vc)" by simp
   2.834 +  hence "rbt_greater x (Branch B va vb vd vc)" by (blast dest: rbt_greater_trans)
   2.835 +  with 6 show ?case by (simp add: combine_rbt_greater)
   2.836  qed simp+
   2.837  
   2.838 +end
   2.839 +
   2.840  lemma combine_in_tree: 
   2.841    assumes "inv2 l" "inv2 r" "bheight l = bheight r" "inv1 l" "inv1 r"
   2.842    shows "entry_in_tree k v (combine l r) = (entry_in_tree k v l \<or> entry_in_tree k v r)"
   2.843 @@ -721,29 +780,43 @@
   2.844    qed 
   2.845  qed (auto split: rbt.splits color.splits)
   2.846  
   2.847 +context ord begin
   2.848 +
   2.849  fun
   2.850 -  del_from_left :: "('a\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" and
   2.851 -  del_from_right :: "('a\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" and
   2.852 -  del :: "('a\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
   2.853 +  rbt_del_from_left :: "'a \<Rightarrow> ('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" and
   2.854 +  rbt_del_from_right :: "'a \<Rightarrow> ('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" and
   2.855 +  rbt_del :: "'a\<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
   2.856  where
   2.857 -  "del x Empty = Empty" |
   2.858 -  "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))" |
   2.859 -  "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" |
   2.860 -  "del_from_left x a y s b = Branch R (del x a) y s b" |
   2.861 -  "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))" | 
   2.862 -  "del_from_right x a y s b = Branch R a y s (del x b)"
   2.863 +  "rbt_del x Empty = Empty" |
   2.864 +  "rbt_del x (Branch c a y s b) = 
   2.865 +   (if x < y then rbt_del_from_left x a y s b 
   2.866 +    else (if x > y then rbt_del_from_right x a y s b else combine a b))" |
   2.867 +  "rbt_del_from_left x (Branch B lt z v rt) y s b = balance_left (rbt_del x (Branch B lt z v rt)) y s b" |
   2.868 +  "rbt_del_from_left x a y s b = Branch R (rbt_del x a) y s b" |
   2.869 +  "rbt_del_from_right x a y s (Branch B lt z v rt) = balance_right a y s (rbt_del x (Branch B lt z v rt))" | 
   2.870 +  "rbt_del_from_right x a y s b = Branch R a y s (rbt_del x b)"
   2.871 +
   2.872 +end
   2.873 +
   2.874 +context linorder begin
   2.875  
   2.876  lemma 
   2.877    assumes "inv2 lt" "inv1 lt"
   2.878    shows
   2.879    "\<lbrakk>inv2 rt; bheight lt = bheight rt; inv1 rt\<rbrakk> \<Longrightarrow>
   2.880 -  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))"
   2.881 +   inv2 (rbt_del_from_left x lt k v rt) \<and> 
   2.882 +   bheight (rbt_del_from_left x lt k v rt) = bheight lt \<and> 
   2.883 +   (color_of lt = B \<and> color_of rt = B \<and> inv1 (rbt_del_from_left x lt k v rt) \<or> 
   2.884 +    (color_of lt \<noteq> B \<or> color_of rt \<noteq> B) \<and> inv1l (rbt_del_from_left x lt k v rt))"
   2.885    and "\<lbrakk>inv2 rt; bheight lt = bheight rt; inv1 rt\<rbrakk> \<Longrightarrow>
   2.886 -  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))"
   2.887 -  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) 
   2.888 -  \<or> color_of lt = B \<and> bheight (del x lt) = bheight lt - 1 \<and> inv1l (del x lt))"
   2.889 +  inv2 (rbt_del_from_right x lt k v rt) \<and> 
   2.890 +  bheight (rbt_del_from_right x lt k v rt) = bheight lt \<and> 
   2.891 +  (color_of lt = B \<and> color_of rt = B \<and> inv1 (rbt_del_from_right x lt k v rt) \<or> 
   2.892 +   (color_of lt \<noteq> B \<or> color_of rt \<noteq> B) \<and> inv1l (rbt_del_from_right x lt k v rt))"
   2.893 +  and rbt_del_inv1_inv2: "inv2 (rbt_del x lt) \<and> (color_of lt = R \<and> bheight (rbt_del x lt) = bheight lt \<and> inv1 (rbt_del x lt) 
   2.894 +  \<or> color_of lt = B \<and> bheight (rbt_del x lt) = bheight lt - 1 \<and> inv1l (rbt_del x lt))"
   2.895  using assms
   2.896 -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)
   2.897 +proof (induct x lt k v rt and x lt k v rt and x lt rule: rbt_del_from_left_rbt_del_from_right_rbt_del.induct)
   2.898  case (2 y c _ y')
   2.899    have "y = y' \<or> y < y' \<or> y > y'" by auto
   2.900    thus ?case proof (elim disjE)
   2.901 @@ -767,55 +840,55 @@
   2.902  qed auto
   2.903  
   2.904  lemma 
   2.905 -  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)"
   2.906 -  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)"
   2.907 -  and del_tree_less: "tree_less v lt \<Longrightarrow> tree_less v (del x lt)"
   2.908 -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) 
   2.909 -   (auto simp: balance_left_tree_less balance_right_tree_less)
   2.910 +  rbt_del_from_left_rbt_less: "\<lbrakk> lt |\<guillemotleft> v; rt |\<guillemotleft> v; k < v\<rbrakk> \<Longrightarrow> rbt_del_from_left x lt k y rt |\<guillemotleft> v"
   2.911 +  and rbt_del_from_right_rbt_less: "\<lbrakk>lt |\<guillemotleft> v; rt |\<guillemotleft> v; k < v\<rbrakk> \<Longrightarrow> rbt_del_from_right x lt k y rt |\<guillemotleft> v"
   2.912 +  and rbt_del_rbt_less: "lt |\<guillemotleft> v \<Longrightarrow> rbt_del x lt |\<guillemotleft> v"
   2.913 +by (induct x lt k y rt and x lt k y rt and x lt rule: rbt_del_from_left_rbt_del_from_right_rbt_del.induct) 
   2.914 +   (auto simp: balance_left_rbt_less balance_right_rbt_less)
   2.915  
   2.916 -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)"
   2.917 -  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)"
   2.918 -  and del_tree_greater: "tree_greater v lt \<Longrightarrow> tree_greater v (del x lt)"
   2.919 -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)
   2.920 -   (auto simp: balance_left_tree_greater balance_right_tree_greater)
   2.921 +lemma rbt_del_from_left_rbt_greater: "\<lbrakk>v \<guillemotleft>| lt; v \<guillemotleft>| rt; k > v\<rbrakk> \<Longrightarrow> v \<guillemotleft>| rbt_del_from_left x lt k y rt"
   2.922 +  and rbt_del_from_right_rbt_greater: "\<lbrakk>v \<guillemotleft>| lt; v \<guillemotleft>| rt; k > v\<rbrakk> \<Longrightarrow> v \<guillemotleft>| rbt_del_from_right x lt k y rt"
   2.923 +  and rbt_del_rbt_greater: "v \<guillemotleft>| lt \<Longrightarrow> v \<guillemotleft>| rbt_del x lt"
   2.924 +by (induct x lt k y rt and x lt k y rt and x lt rule: rbt_del_from_left_rbt_del_from_right_rbt_del.induct)
   2.925 +   (auto simp: balance_left_rbt_greater balance_right_rbt_greater)
   2.926  
   2.927 -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)"
   2.928 -  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)"
   2.929 -  and del_sorted: "sorted lt \<Longrightarrow> sorted (del x lt)"
   2.930 -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)
   2.931 +lemma "\<lbrakk>rbt_sorted lt; rbt_sorted rt; lt |\<guillemotleft> k; k \<guillemotleft>| rt\<rbrakk> \<Longrightarrow> rbt_sorted (rbt_del_from_left x lt k y rt)"
   2.932 +  and "\<lbrakk>rbt_sorted lt; rbt_sorted rt; lt |\<guillemotleft> k; k \<guillemotleft>| rt\<rbrakk> \<Longrightarrow> rbt_sorted (rbt_del_from_right x lt k y rt)"
   2.933 +  and rbt_del_rbt_sorted: "rbt_sorted lt \<Longrightarrow> rbt_sorted (rbt_del x lt)"
   2.934 +proof (induct x lt k y rt and x lt k y rt and x lt rule: rbt_del_from_left_rbt_del_from_right_rbt_del.induct)
   2.935    case (3 x lta zz v rta yy ss bb)
   2.936 -  from 3 have "tree_less yy (Branch B lta zz v rta)" by simp
   2.937 -  hence "tree_less yy (del x (Branch B lta zz v rta))" by (rule del_tree_less)
   2.938 -  with 3 show ?case by (simp add: balance_left_sorted)
   2.939 +  from 3 have "Branch B lta zz v rta |\<guillemotleft> yy" by simp
   2.940 +  hence "rbt_del x (Branch B lta zz v rta) |\<guillemotleft> yy" by (rule rbt_del_rbt_less)
   2.941 +  with 3 show ?case by (simp add: balance_left_rbt_sorted)
   2.942  next
   2.943    case ("4_2" x vaa vbb vdd vc yy ss bb)
   2.944 -  hence "tree_less yy (Branch R vaa vbb vdd vc)" by simp
   2.945 -  hence "tree_less yy (del x (Branch R vaa vbb vdd vc))" by (rule del_tree_less)
   2.946 +  hence "Branch R vaa vbb vdd vc |\<guillemotleft> yy" by simp
   2.947 +  hence "rbt_del x (Branch R vaa vbb vdd vc) |\<guillemotleft> yy" by (rule rbt_del_rbt_less)
   2.948    with "4_2" show ?case by simp
   2.949  next
   2.950    case (5 x aa yy ss lta zz v rta) 
   2.951 -  hence "tree_greater yy (Branch B lta zz v rta)" by simp
   2.952 -  hence "tree_greater yy (del x (Branch B lta zz v rta))" by (rule del_tree_greater)
   2.953 -  with 5 show ?case by (simp add: balance_right_sorted)
   2.954 +  hence "yy \<guillemotleft>| Branch B lta zz v rta" by simp
   2.955 +  hence "yy \<guillemotleft>| rbt_del x (Branch B lta zz v rta)" by (rule rbt_del_rbt_greater)
   2.956 +  with 5 show ?case by (simp add: balance_right_rbt_sorted)
   2.957  next
   2.958    case ("6_2" x aa yy ss vaa vbb vdd vc)
   2.959 -  hence "tree_greater yy (Branch R vaa vbb vdd vc)" by simp
   2.960 -  hence "tree_greater yy (del x (Branch R vaa vbb vdd vc))" by (rule del_tree_greater)
   2.961 +  hence "yy \<guillemotleft>| Branch R vaa vbb vdd vc" by simp
   2.962 +  hence "yy \<guillemotleft>| rbt_del x (Branch R vaa vbb vdd vc)" by (rule rbt_del_rbt_greater)
   2.963    with "6_2" show ?case by simp
   2.964 -qed (auto simp: combine_sorted)
   2.965 +qed (auto simp: combine_rbt_sorted)
   2.966  
   2.967 -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)))"
   2.968 -  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)))"
   2.969 -  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))"
   2.970 -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)
   2.971 +lemma "\<lbrakk>rbt_sorted lt; rbt_sorted rt; lt |\<guillemotleft> kt; kt \<guillemotleft>| rt; inv1 lt; inv1 rt; inv2 lt; inv2 rt; bheight lt = bheight rt; x < kt\<rbrakk> \<Longrightarrow> entry_in_tree k v (rbt_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)))"
   2.972 +  and "\<lbrakk>rbt_sorted lt; rbt_sorted rt; lt |\<guillemotleft> kt; kt \<guillemotleft>| rt; inv1 lt; inv1 rt; inv2 lt; inv2 rt; bheight lt = bheight rt; x > kt\<rbrakk> \<Longrightarrow> entry_in_tree k v (rbt_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)))"
   2.973 +  and rbt_del_in_tree: "\<lbrakk>rbt_sorted t; inv1 t; inv2 t\<rbrakk> \<Longrightarrow> entry_in_tree k v (rbt_del x t) = (False \<or> (x \<noteq> k \<and> entry_in_tree k v t))"
   2.974 +proof (induct x lt kt y rt and x lt kt y rt and x t rule: rbt_del_from_left_rbt_del_from_right_rbt_del.induct)
   2.975    case (2 xx c aa yy ss bb)
   2.976    have "xx = yy \<or> xx < yy \<or> xx > yy" by auto
   2.977    from this 2 show ?case proof (elim disjE)
   2.978      assume "xx = yy"
   2.979      with 2 show ?thesis proof (cases "xx = k")
   2.980        case True
   2.981 -      from 2 `xx = yy` `xx = k` have "sorted (Branch c aa yy ss bb) \<and> k = yy" by simp
   2.982 -      hence "\<not> entry_in_tree k v aa" "\<not> entry_in_tree k v bb" by (auto simp: tree_less_nit tree_greater_prop)
   2.983 +      from 2 `xx = yy` `xx = k` have "rbt_sorted (Branch c aa yy ss bb) \<and> k = yy" by simp
   2.984 +      hence "\<not> entry_in_tree k v aa" "\<not> entry_in_tree k v bb" by (auto simp: rbt_less_nit rbt_greater_prop)
   2.985        with `xx = yy` 2 `xx = k` show ?thesis by (simp add: combine_in_tree)
   2.986      qed (simp add: combine_in_tree)
   2.987    qed simp+
   2.988 @@ -823,143 +896,147 @@
   2.989    case (3 xx lta zz vv rta yy ss bb)
   2.990    def mt[simp]: mt == "Branch B lta zz vv rta"
   2.991    from 3 have "inv2 mt \<and> inv1 mt" by simp
   2.992 -  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)
   2.993 -  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)
   2.994 +  hence "inv2 (rbt_del xx mt) \<and> (color_of mt = R \<and> bheight (rbt_del xx mt) = bheight mt \<and> inv1 (rbt_del xx mt) \<or> color_of mt = B \<and> bheight (rbt_del xx mt) = bheight mt - 1 \<and> inv1l (rbt_del xx mt))" by (blast dest: rbt_del_inv1_inv2)
   2.995 +  with 3 have 4: "entry_in_tree k v (rbt_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)
   2.996    thus ?case proof (cases "xx = k")
   2.997      case True
   2.998 -    from 3 True have "tree_greater yy bb \<and> yy > k" by simp
   2.999 -    hence "tree_greater k bb" by (blast dest: tree_greater_trans)
  2.1000 -    with 3 4 True show ?thesis by (auto simp: tree_greater_nit)
  2.1001 +    from 3 True have "yy \<guillemotleft>| bb \<and> yy > k" by simp
  2.1002 +    hence "k \<guillemotleft>| bb" by (blast dest: rbt_greater_trans)
  2.1003 +    with 3 4 True show ?thesis by (auto simp: rbt_greater_nit)
  2.1004    qed auto
  2.1005  next
  2.1006    case ("4_1" xx yy ss bb)
  2.1007    show ?case proof (cases "xx = k")
  2.1008      case True
  2.1009 -    with "4_1" have "tree_greater yy bb \<and> k < yy" by simp
  2.1010 -    hence "tree_greater k bb" by (blast dest: tree_greater_trans)
  2.1011 +    with "4_1" have "yy \<guillemotleft>| bb \<and> k < yy" by simp
  2.1012 +    hence "k \<guillemotleft>| bb" by (blast dest: rbt_greater_trans)
  2.1013      with "4_1" `xx = k` 
  2.1014 -   have "entry_in_tree k v (Branch R Empty yy ss bb) = entry_in_tree k v Empty" by (auto simp: tree_greater_nit)
  2.1015 +   have "entry_in_tree k v (Branch R Empty yy ss bb) = entry_in_tree k v Empty" by (auto simp: rbt_greater_nit)
  2.1016      thus ?thesis by auto
  2.1017    qed simp+
  2.1018  next
  2.1019    case ("4_2" xx vaa vbb vdd vc yy ss bb)
  2.1020    thus ?case proof (cases "xx = k")
  2.1021      case True
  2.1022 -    with "4_2" have "k < yy \<and> tree_greater yy bb" by simp
  2.1023 -    hence "tree_greater k bb" by (blast dest: tree_greater_trans)
  2.1024 -    with True "4_2" show ?thesis by (auto simp: tree_greater_nit)
  2.1025 +    with "4_2" have "k < yy \<and> yy \<guillemotleft>| bb" by simp
  2.1026 +    hence "k \<guillemotleft>| bb" by (blast dest: rbt_greater_trans)
  2.1027 +    with True "4_2" show ?thesis by (auto simp: rbt_greater_nit)
  2.1028    qed auto
  2.1029  next
  2.1030    case (5 xx aa yy ss lta zz vv rta)
  2.1031    def mt[simp]: mt == "Branch B lta zz vv rta"
  2.1032    from 5 have "inv2 mt \<and> inv1 mt" by simp
  2.1033 -  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)
  2.1034 -  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)
  2.1035 +  hence "inv2 (rbt_del xx mt) \<and> (color_of mt = R \<and> bheight (rbt_del xx mt) = bheight mt \<and> inv1 (rbt_del xx mt) \<or> color_of mt = B \<and> bheight (rbt_del xx mt) = bheight mt - 1 \<and> inv1l (rbt_del xx mt))" by (blast dest: rbt_del_inv1_inv2)
  2.1036 +  with 5 have 3: "entry_in_tree k v (rbt_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)
  2.1037    thus ?case proof (cases "xx = k")
  2.1038      case True
  2.1039 -    from 5 True have "tree_less yy aa \<and> yy < k" by simp
  2.1040 -    hence "tree_less k aa" by (blast dest: tree_less_trans)
  2.1041 -    with 3 5 True show ?thesis by (auto simp: tree_less_nit)
  2.1042 +    from 5 True have "aa |\<guillemotleft> yy \<and> yy < k" by simp
  2.1043 +    hence "aa |\<guillemotleft> k" by (blast dest: rbt_less_trans)
  2.1044 +    with 3 5 True show ?thesis by (auto simp: rbt_less_nit)
  2.1045    qed auto
  2.1046  next
  2.1047    case ("6_1" xx aa yy ss)
  2.1048    show ?case proof (cases "xx = k")
  2.1049      case True
  2.1050 -    with "6_1" have "tree_less yy aa \<and> k > yy" by simp
  2.1051 -    hence "tree_less k aa" by (blast dest: tree_less_trans)
  2.1052 -    with "6_1" `xx = k` show ?thesis by (auto simp: tree_less_nit)
  2.1053 +    with "6_1" have "aa |\<guillemotleft> yy \<and> k > yy" by simp
  2.1054 +    hence "aa |\<guillemotleft> k" by (blast dest: rbt_less_trans)
  2.1055 +    with "6_1" `xx = k` show ?thesis by (auto simp: rbt_less_nit)
  2.1056    qed simp
  2.1057  next
  2.1058    case ("6_2" xx aa yy ss vaa vbb vdd vc)
  2.1059    thus ?case proof (cases "xx = k")
  2.1060      case True
  2.1061 -    with "6_2" have "k > yy \<and> tree_less yy aa" by simp
  2.1062 -    hence "tree_less k aa" by (blast dest: tree_less_trans)
  2.1063 -    with True "6_2" show ?thesis by (auto simp: tree_less_nit)
  2.1064 +    with "6_2" have "k > yy \<and> aa |\<guillemotleft> yy" by simp
  2.1065 +    hence "aa |\<guillemotleft> k" by (blast dest: rbt_less_trans)
  2.1066 +    with True "6_2" show ?thesis by (auto simp: rbt_less_nit)
  2.1067    qed auto
  2.1068  qed simp
  2.1069  
  2.1070 +definition (in ord) rbt_delete where
  2.1071 +  "rbt_delete k t = paint B (rbt_del k t)"
  2.1072  
  2.1073 -definition delete where
  2.1074 -  delete_def: "delete k t = paint B (del k t)"
  2.1075 -
  2.1076 -theorem delete_is_rbt [simp]: assumes "is_rbt t" shows "is_rbt (delete k t)"
  2.1077 +theorem rbt_delete_is_rbt [simp]: assumes "is_rbt t" shows "is_rbt (rbt_delete k t)"
  2.1078  proof -
  2.1079    from assms have "inv2 t" and "inv1 t" unfolding is_rbt_def by auto 
  2.1080 -  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)
  2.1081 -  hence "inv2 (del k t) \<and> inv1l (del k t)" by (cases "color_of t") auto
  2.1082 +  hence "inv2 (rbt_del k t) \<and> (color_of t = R \<and> bheight (rbt_del k t) = bheight t \<and> inv1 (rbt_del k t) \<or> color_of t = B \<and> bheight (rbt_del k t) = bheight t - 1 \<and> inv1l (rbt_del k t))" by (rule rbt_del_inv1_inv2)
  2.1083 +  hence "inv2 (rbt_del k t) \<and> inv1l (rbt_del k t)" by (cases "color_of t") auto
  2.1084    with assms show ?thesis
  2.1085 -    unfolding is_rbt_def delete_def
  2.1086 -    by (auto intro: paint_sorted del_sorted)
  2.1087 +    unfolding is_rbt_def rbt_delete_def
  2.1088 +    by (auto intro: paint_rbt_sorted rbt_del_rbt_sorted)
  2.1089  qed
  2.1090  
  2.1091 -lemma delete_in_tree: 
  2.1092 +lemma rbt_delete_in_tree: 
  2.1093    assumes "is_rbt t" 
  2.1094 -  shows "entry_in_tree k v (delete x t) = (x \<noteq> k \<and> entry_in_tree k v t)"
  2.1095 -  using assms unfolding is_rbt_def delete_def
  2.1096 -  by (auto simp: del_in_tree)
  2.1097 +  shows "entry_in_tree k v (rbt_delete x t) = (x \<noteq> k \<and> entry_in_tree k v t)"
  2.1098 +  using assms unfolding is_rbt_def rbt_delete_def
  2.1099 +  by (auto simp: rbt_del_in_tree)
  2.1100  
  2.1101 -lemma lookup_delete:
  2.1102 +lemma rbt_lookup_rbt_delete:
  2.1103    assumes is_rbt: "is_rbt t"
  2.1104 -  shows "lookup (delete k t) = (lookup t)|`(-{k})"
  2.1105 +  shows "rbt_lookup (rbt_delete k t) = (rbt_lookup t)|`(-{k})"
  2.1106  proof
  2.1107    fix x
  2.1108 -  show "lookup (delete k t) x = (lookup t |` (-{k})) x" 
  2.1109 +  show "rbt_lookup (rbt_delete k t) x = (rbt_lookup t |` (-{k})) x" 
  2.1110    proof (cases "x = k")
  2.1111      assume "x = k" 
  2.1112      with is_rbt show ?thesis
  2.1113 -      by (cases "lookup (delete k t) k") (auto simp: lookup_in_tree delete_in_tree)
  2.1114 +      by (cases "rbt_lookup (rbt_delete k t) k") (auto simp: rbt_lookup_in_tree rbt_delete_in_tree)
  2.1115    next
  2.1116      assume "x \<noteq> k"
  2.1117      thus ?thesis
  2.1118 -      by auto (metis is_rbt delete_is_rbt delete_in_tree is_rbt_sorted lookup_from_in_tree)
  2.1119 +      by auto (metis is_rbt rbt_delete_is_rbt rbt_delete_in_tree is_rbt_rbt_sorted rbt_lookup_from_in_tree)
  2.1120    qed
  2.1121  qed
  2.1122  
  2.1123 +end
  2.1124  
  2.1125  subsection {* Union *}
  2.1126  
  2.1127 -primrec
  2.1128 -  union_with_key :: "('a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
  2.1129 +context ord begin
  2.1130 +
  2.1131 +primrec rbt_union_with_key :: "('a \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
  2.1132  where
  2.1133 -  "union_with_key f t Empty = t"
  2.1134 -| "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"
  2.1135 +  "rbt_union_with_key f t Empty = t"
  2.1136 +| "rbt_union_with_key f t (Branch c lt k v rt) = rbt_union_with_key f (rbt_union_with_key f (rbt_insert_with_key f k v t) lt) rt"
  2.1137  
  2.1138 -lemma unionwk_sorted: "sorted lt \<Longrightarrow> sorted (union_with_key f lt rt)" 
  2.1139 -  by (induct rt arbitrary: lt) (auto simp: insertwk_sorted)
  2.1140 -theorem unionwk_is_rbt[simp]: "is_rbt lt \<Longrightarrow> is_rbt (union_with_key f lt rt)" 
  2.1141 -  by (induct rt arbitrary: lt) (simp add: insertwk_is_rbt)+
  2.1142 +definition rbt_union_with where
  2.1143 +  "rbt_union_with f = rbt_union_with_key (\<lambda>_. f)"
  2.1144 +
  2.1145 +definition rbt_union where
  2.1146 +  "rbt_union = rbt_union_with_key (%_ _ rv. rv)"
  2.1147 +
  2.1148 +end
  2.1149  
  2.1150 -definition
  2.1151 -  union_with where
  2.1152 -  "union_with f = union_with_key (\<lambda>_. f)"
  2.1153 +context linorder begin
  2.1154  
  2.1155 -theorem unionw_is_rbt: "is_rbt lt \<Longrightarrow> is_rbt (union_with f lt rt)" unfolding union_with_def by simp
  2.1156 +lemma rbt_unionwk_rbt_sorted: "rbt_sorted lt \<Longrightarrow> rbt_sorted (rbt_union_with_key f lt rt)" 
  2.1157 +  by (induct rt arbitrary: lt) (auto simp: rbt_insertwk_rbt_sorted)
  2.1158 +theorem rbt_unionwk_is_rbt[simp]: "is_rbt lt \<Longrightarrow> is_rbt (rbt_union_with_key f lt rt)" 
  2.1159 +  by (induct rt arbitrary: lt) (simp add: rbt_insertwk_is_rbt)+
  2.1160  
  2.1161 -definition union where
  2.1162 -  "union = union_with_key (%_ _ rv. rv)"
  2.1163 +theorem rbt_unionw_is_rbt: "is_rbt lt \<Longrightarrow> is_rbt (rbt_union_with f lt rt)" unfolding rbt_union_with_def by simp
  2.1164 +
  2.1165 +theorem rbt_union_is_rbt: "is_rbt lt \<Longrightarrow> is_rbt (rbt_union lt rt)" unfolding rbt_union_def by simp
  2.1166  
  2.1167 -theorem union_is_rbt: "is_rbt lt \<Longrightarrow> is_rbt (union lt rt)" unfolding union_def by simp
  2.1168 -
  2.1169 -lemma union_Branch[simp]:
  2.1170 -  "union t (Branch c lt k v rt) = union (union (insert k v t) lt) rt"
  2.1171 -  unfolding union_def insert_def
  2.1172 +lemma (in ord) rbt_union_Branch[simp]:
  2.1173 +  "rbt_union t (Branch c lt k v rt) = rbt_union (rbt_union (rbt_insert k v t) lt) rt"
  2.1174 +  unfolding rbt_union_def rbt_insert_def
  2.1175    by simp
  2.1176  
  2.1177 -lemma lookup_union:
  2.1178 -  assumes "is_rbt s" "sorted t"
  2.1179 -  shows "lookup (union s t) = lookup s ++ lookup t"
  2.1180 +lemma rbt_lookup_rbt_union:
  2.1181 +  assumes "is_rbt s" "rbt_sorted t"
  2.1182 +  shows "rbt_lookup (rbt_union s t) = rbt_lookup s ++ rbt_lookup t"
  2.1183  using assms
  2.1184  proof (induct t arbitrary: s)
  2.1185 -  case Empty thus ?case by (auto simp: union_def)
  2.1186 +  case Empty thus ?case by (auto simp: rbt_union_def)
  2.1187  next
  2.1188    case (Branch c l k v r s)
  2.1189 -  then have "sorted r" "sorted l" "l |\<guillemotleft> k" "k \<guillemotleft>| r" by auto
  2.1190 +  then have "rbt_sorted r" "rbt_sorted l" "l |\<guillemotleft> k" "k \<guillemotleft>| r" by auto
  2.1191  
  2.1192 -  have meq: "lookup s(k \<mapsto> v) ++ lookup l ++ lookup r =
  2.1193 -    lookup s ++
  2.1194 -    (\<lambda>a. if a < k then lookup l a
  2.1195 -    else if k < a then lookup r a else Some v)" (is "?m1 = ?m2")
  2.1196 +  have meq: "rbt_lookup s(k \<mapsto> v) ++ rbt_lookup l ++ rbt_lookup r =
  2.1197 +    rbt_lookup s ++
  2.1198 +    (\<lambda>a. if a < k then rbt_lookup l a
  2.1199 +    else if k < a then rbt_lookup r a else Some v)" (is "?m1 = ?m2")
  2.1200    proof (rule ext)
  2.1201      fix a
  2.1202  
  2.1203 @@ -967,7 +1044,7 @@
  2.1204      thus "?m1 a = ?m2 a"
  2.1205      proof (elim disjE)
  2.1206        assume "k < a"
  2.1207 -      with `l |\<guillemotleft> k` have "l |\<guillemotleft> a" by (rule tree_less_trans)
  2.1208 +      with `l |\<guillemotleft> k` have "l |\<guillemotleft> a" by (rule rbt_less_trans)
  2.1209        with `k < a` show ?thesis
  2.1210          by (auto simp: map_add_def split: option.splits)
  2.1211      next
  2.1212 @@ -976,52 +1053,57 @@
  2.1213        show ?thesis by (auto simp: map_add_def)
  2.1214      next
  2.1215        assume "a < k"
  2.1216 -      from this `k \<guillemotleft>| r` have "a \<guillemotleft>| r" by (rule tree_greater_trans)
  2.1217 +      from this `k \<guillemotleft>| r` have "a \<guillemotleft>| r" by (rule rbt_greater_trans)
  2.1218        with `a < k` show ?thesis
  2.1219          by (auto simp: map_add_def split: option.splits)
  2.1220      qed
  2.1221    qed
  2.1222  
  2.1223 -  from Branch have is_rbt: "is_rbt (RBT_Impl.union (RBT_Impl.insert k v s) l)"
  2.1224 -    by (auto intro: union_is_rbt insert_is_rbt)
  2.1225 +  from Branch have is_rbt: "is_rbt (RBT_Impl.rbt_union (RBT_Impl.rbt_insert k v s) l)"
  2.1226 +    by (auto intro: rbt_union_is_rbt rbt_insert_is_rbt)
  2.1227    with Branch have IHs:
  2.1228 -    "lookup (union (union (insert k v s) l) r) = lookup (union (insert k v s) l) ++ lookup r"
  2.1229 -    "lookup (union (insert k v s) l) = lookup (insert k v s) ++ lookup l"
  2.1230 +    "rbt_lookup (rbt_union (rbt_union (rbt_insert k v s) l) r) = rbt_lookup (rbt_union (rbt_insert k v s) l) ++ rbt_lookup r"
  2.1231 +    "rbt_lookup (rbt_union (rbt_insert k v s) l) = rbt_lookup (rbt_insert k v s) ++ rbt_lookup l"
  2.1232      by auto
  2.1233    
  2.1234    with meq show ?case
  2.1235 -    by (auto simp: lookup_insert[OF Branch(3)])
  2.1236 +    by (auto simp: rbt_lookup_rbt_insert[OF Branch(3)])
  2.1237  
  2.1238  qed
  2.1239  
  2.1240 +end
  2.1241  
  2.1242  subsection {* Modifying existing entries *}
  2.1243  
  2.1244 +context ord begin
  2.1245 +
  2.1246  primrec
  2.1247 -  map_entry :: "'a\<Colon>linorder \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
  2.1248 +  rbt_map_entry :: "'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
  2.1249  where
  2.1250 -  "map_entry k f Empty = Empty"
  2.1251 -| "map_entry k f (Branch c lt x v rt) =
  2.1252 -    (if k < x then Branch c (map_entry k f lt) x v rt
  2.1253 -    else if k > x then (Branch c lt x v (map_entry k f rt))
  2.1254 +  "rbt_map_entry k f Empty = Empty"
  2.1255 +| "rbt_map_entry k f (Branch c lt x v rt) =
  2.1256 +    (if k < x then Branch c (rbt_map_entry k f lt) x v rt
  2.1257 +    else if k > x then (Branch c lt x v (rbt_map_entry k f rt))
  2.1258      else Branch c lt x (f v) rt)"
  2.1259  
  2.1260 -lemma map_entry_color_of: "color_of (map_entry k f t) = color_of t" by (induct t) simp+
  2.1261 -lemma map_entry_inv1: "inv1 (map_entry k f t) = inv1 t" by (induct t) (simp add: map_entry_color_of)+
  2.1262 -lemma map_entry_inv2: "inv2 (map_entry k f t) = inv2 t" "bheight (map_entry k f t) = bheight t" by (induct t) simp+
  2.1263 -lemma map_entry_tree_greater: "tree_greater a (map_entry k f t) = tree_greater a t" by (induct t) simp+
  2.1264 -lemma map_entry_tree_less: "tree_less a (map_entry k f t) = tree_less a t" by (induct t) simp+
  2.1265 -lemma map_entry_sorted: "sorted (map_entry k f t) = sorted t"
  2.1266 -  by (induct t) (simp_all add: map_entry_tree_less map_entry_tree_greater)
  2.1267 +
  2.1268 +lemma rbt_map_entry_color_of: "color_of (rbt_map_entry k f t) = color_of t" by (induct t) simp+
  2.1269 +lemma rbt_map_entry_inv1: "inv1 (rbt_map_entry k f t) = inv1 t" by (induct t) (simp add: rbt_map_entry_color_of)+
  2.1270 +lemma rbt_map_entry_inv2: "inv2 (rbt_map_entry k f t) = inv2 t" "bheight (rbt_map_entry k f t) = bheight t" by (induct t) simp+
  2.1271 +lemma rbt_map_entry_rbt_greater: "rbt_greater a (rbt_map_entry k f t) = rbt_greater a t" by (induct t) simp+
  2.1272 +lemma rbt_map_entry_rbt_less: "rbt_less a (rbt_map_entry k f t) = rbt_less a t" by (induct t) simp+
  2.1273 +lemma rbt_map_entry_rbt_sorted: "rbt_sorted (rbt_map_entry k f t) = rbt_sorted t"
  2.1274 +  by (induct t) (simp_all add: rbt_map_entry_rbt_less rbt_map_entry_rbt_greater)
  2.1275  
  2.1276 -theorem map_entry_is_rbt [simp]: "is_rbt (map_entry k f t) = is_rbt t" 
  2.1277 -unfolding is_rbt_def by (simp add: map_entry_inv2 map_entry_color_of map_entry_sorted map_entry_inv1 )
  2.1278 +theorem rbt_map_entry_is_rbt [simp]: "is_rbt (rbt_map_entry k f t) = is_rbt t" 
  2.1279 +unfolding is_rbt_def by (simp add: rbt_map_entry_inv2 rbt_map_entry_color_of rbt_map_entry_rbt_sorted rbt_map_entry_inv1 )
  2.1280  
  2.1281 -theorem lookup_map_entry:
  2.1282 -  "lookup (map_entry k f t) = (lookup t)(k := Option.map f (lookup t k))"
  2.1283 +end
  2.1284 +
  2.1285 +theorem (in linorder) rbt_lookup_rbt_map_entry:
  2.1286 +  "rbt_lookup (rbt_map_entry k f t) = (rbt_lookup t)(k := Option.map f (rbt_lookup t k))"
  2.1287    by (induct t) (auto split: option.splits simp add: fun_eq_iff)
  2.1288  
  2.1289 -
  2.1290  subsection {* Mapping all entries *}
  2.1291  
  2.1292  primrec
  2.1293 @@ -1033,18 +1115,28 @@
  2.1294  lemma map_entries [simp]: "entries (map f t) = List.map (\<lambda>(k, v). (k, f k v)) (entries t)"
  2.1295    by (induct t) auto
  2.1296  lemma map_keys [simp]: "keys (map f t) = keys t" by (simp add: keys_def split_def)
  2.1297 -lemma map_tree_greater: "tree_greater k (map f t) = tree_greater k t" by (induct t) simp+
  2.1298 -lemma map_tree_less: "tree_less k (map f t) = tree_less k t" by (induct t) simp+
  2.1299 -lemma map_sorted: "sorted (map f t) = sorted t"  by (induct t) (simp add: map_tree_less map_tree_greater)+
  2.1300  lemma map_color_of: "color_of (map f t) = color_of t" by (induct t) simp+
  2.1301  lemma map_inv1: "inv1 (map f t) = inv1 t" by (induct t) (simp add: map_color_of)+
  2.1302  lemma map_inv2: "inv2 (map f t) = inv2 t" "bheight (map f t) = bheight t" by (induct t) simp+
  2.1303 +
  2.1304 +context ord begin
  2.1305 +
  2.1306 +lemma map_rbt_greater: "rbt_greater k (map f t) = rbt_greater k t" by (induct t) simp+
  2.1307 +lemma map_rbt_less: "rbt_less k (map f t) = rbt_less k t" by (induct t) simp+
  2.1308 +lemma map_rbt_sorted: "rbt_sorted (map f t) = rbt_sorted t"  by (induct t) (simp add: map_rbt_less map_rbt_greater)+
  2.1309  theorem map_is_rbt [simp]: "is_rbt (map f t) = is_rbt t" 
  2.1310 -unfolding is_rbt_def by (simp add: map_inv1 map_inv2 map_sorted map_color_of)
  2.1311 +unfolding is_rbt_def by (simp add: map_inv1 map_inv2 map_rbt_sorted map_color_of)
  2.1312  
  2.1313 -theorem lookup_map: "lookup (map f t) x = Option.map (f x) (lookup t x)"
  2.1314 -  by (induct t) auto
  2.1315 +end
  2.1316  
  2.1317 +theorem (in linorder) rbt_lookup_map: "rbt_lookup (map f t) x = Option.map (f x) (rbt_lookup t x)"
  2.1318 +  apply(induct t)
  2.1319 +  apply auto
  2.1320 +  apply(subgoal_tac "x = a")
  2.1321 +  apply auto
  2.1322 +  done
  2.1323 + (* FIXME: simproc "antisym less" does not work for linorder context, only for linorder type class
  2.1324 +    by (induct t) auto *)
  2.1325  
  2.1326  subsection {* Folding over entries *}
  2.1327  
  2.1328 @@ -1059,26 +1151,73 @@
  2.1329  
  2.1330  subsection {* Bulkloading a tree *}
  2.1331  
  2.1332 -definition bulkload :: "('a \<times> 'b) list \<Rightarrow> ('a\<Colon>linorder, 'b) rbt" where
  2.1333 -  "bulkload xs = foldr (\<lambda>(k, v). insert k v) xs Empty"
  2.1334 +definition (in ord) rbt_bulkload :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) rbt" where
  2.1335 +  "rbt_bulkload xs = foldr (\<lambda>(k, v). rbt_insert k v) xs Empty"
  2.1336 +
  2.1337 +context linorder begin
  2.1338  
  2.1339 -lemma bulkload_is_rbt [simp, intro]:
  2.1340 -  "is_rbt (bulkload xs)"
  2.1341 -  unfolding bulkload_def by (induct xs) auto
  2.1342 +lemma rbt_bulkload_is_rbt [simp, intro]:
  2.1343 +  "is_rbt (rbt_bulkload xs)"
  2.1344 +  unfolding rbt_bulkload_def by (induct xs) auto
  2.1345  
  2.1346 -lemma lookup_bulkload:
  2.1347 -  "lookup (bulkload xs) = map_of xs"
  2.1348 +lemma rbt_lookup_rbt_bulkload:
  2.1349 +  "rbt_lookup (rbt_bulkload xs) = map_of xs"
  2.1350  proof -
  2.1351    obtain ys where "ys = rev xs" by simp
  2.1352    have "\<And>t. is_rbt t \<Longrightarrow>
  2.1353 -    lookup (List.fold (prod_case insert) ys t) = lookup t ++ map_of (rev ys)"
  2.1354 -      by (induct ys) (simp_all add: bulkload_def lookup_insert prod_case_beta)
  2.1355 +    rbt_lookup (List.fold (prod_case rbt_insert) ys t) = rbt_lookup t ++ map_of (rev ys)"
  2.1356 +      by (induct ys) (simp_all add: rbt_bulkload_def rbt_lookup_rbt_insert prod_case_beta)
  2.1357    from this Empty_is_rbt have
  2.1358 -    "lookup (List.fold (prod_case insert) (rev xs) Empty) = lookup Empty ++ map_of xs"
  2.1359 +    "rbt_lookup (List.fold (prod_case rbt_insert) (rev xs) Empty) = rbt_lookup Empty ++ map_of xs"
  2.1360       by (simp add: `ys = rev xs`)
  2.1361 -  then show ?thesis by (simp add: bulkload_def lookup_Empty foldr_conv_fold)
  2.1362 +  then show ?thesis by (simp add: rbt_bulkload_def rbt_lookup_Empty foldr_conv_fold)
  2.1363  qed
  2.1364  
  2.1365 -hide_const (open) R B Empty insert delete entries keys bulkload lookup map_entry map fold union sorted
  2.1366 +end
  2.1367 +
  2.1368 +lemmas [code] =
  2.1369 +  ord.rbt_less_prop
  2.1370 +  ord.rbt_greater_prop
  2.1371 +  ord.rbt_sorted.simps
  2.1372 +  ord.rbt_lookup.simps
  2.1373 +  ord.is_rbt_def
  2.1374 +  ord.rbt_ins.simps
  2.1375 +  ord.rbt_insert_with_key_def
  2.1376 +  ord.rbt_insertw_def
  2.1377 +  ord.rbt_insert_def
  2.1378 +  ord.rbt_del_from_left.simps
  2.1379 +  ord.rbt_del_from_right.simps
  2.1380 +  ord.rbt_del.simps
  2.1381 +  ord.rbt_delete_def
  2.1382 +  ord.rbt_union_with_key.simps
  2.1383 +  ord.rbt_union_with_def
  2.1384 +  ord.rbt_union_def
  2.1385 +  ord.rbt_map_entry.simps
  2.1386 +  ord.rbt_bulkload_def
  2.1387 +
  2.1388 +text {* Restore original type constraints for constants *}
  2.1389 +setup {*
  2.1390 +  fold Sign.add_const_constraint
  2.1391 +    [(@{const_name rbt_less}, SOME @{typ "('a :: order) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> bool"}),
  2.1392 +     (@{const_name rbt_greater}, SOME @{typ "('a :: order) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> bool"}),
  2.1393 +     (@{const_name rbt_sorted}, SOME @{typ "('a :: linorder, 'b) rbt \<Rightarrow> bool"}),
  2.1394 +     (@{const_name rbt_lookup}, SOME @{typ "('a :: linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b"}),
  2.1395 +     (@{const_name is_rbt}, SOME @{typ "('a :: linorder, 'b) rbt \<Rightarrow> bool"}),
  2.1396 +     (@{const_name rbt_ins}, SOME @{typ "('a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"}),
  2.1397 +     (@{const_name rbt_insert_with_key}, SOME @{typ "('a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"}),
  2.1398 +     (@{const_name rbt_insert_with}, SOME @{typ "('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a :: linorder) \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"}),
  2.1399 +     (@{const_name rbt_insert}, SOME @{typ "('a :: linorder) \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"}),
  2.1400 +     (@{const_name rbt_del_from_left}, SOME @{typ "('a\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"}),
  2.1401 +     (@{const_name rbt_del_from_right}, SOME @{typ "('a\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"}),
  2.1402 +     (@{const_name rbt_del}, SOME @{typ "('a\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"}),
  2.1403 +     (@{const_name rbt_delete}, SOME @{typ "('a\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"}),
  2.1404 +     (@{const_name rbt_union_with_key}, SOME @{typ "('a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"}),
  2.1405 +     (@{const_name rbt_union_with}, SOME @{typ "('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder,'b) rbt \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"}),
  2.1406 +     (@{const_name rbt_union}, SOME @{typ "('a\<Colon>linorder,'b) rbt \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"}),
  2.1407 +     (@{const_name rbt_map_entry}, SOME @{typ "'a\<Colon>linorder \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"}),
  2.1408 +     (@{const_name rbt_bulkload}, SOME @{typ "('a \<times> 'b) list \<Rightarrow> ('a\<Colon>linorder,'b) rbt"})]
  2.1409 +*}
  2.1410 +
  2.1411 +hide_const (open) R B Empty entries keys map fold
  2.1412  
  2.1413  end
     3.1 --- a/src/HOL/Library/RBT_Mapping.thy	Thu Apr 12 13:47:21 2012 +0200
     3.2 +++ b/src/HOL/Library/RBT_Mapping.thy	Fri Apr 13 11:45:30 2012 +0200
     3.3 @@ -40,7 +40,7 @@
     3.4  
     3.5  lemma keys_Mapping [code]:
     3.6    "Mapping.keys (Mapping t) = set (keys t)"
     3.7 -  by (simp add: RBT.keys_def Mapping_def Mapping.keys_def lookup_def lookup_keys)
     3.8 +  by (simp add: RBT.keys_def Mapping_def Mapping.keys_def lookup_def rbt_lookup_keys)
     3.9  
    3.10  lemma ordered_keys_Mapping [code]:
    3.11    "Mapping.ordered_keys (Mapping t) = keys t"
    3.12 @@ -144,22 +144,22 @@
    3.13    @{thm Empty_is_rbt}\hfill(@{text "Empty_is_rbt"})
    3.14  
    3.15    \noindent
    3.16 -  @{thm insert_is_rbt}\hfill(@{text "insert_is_rbt"})
    3.17 +  @{thm rbt_insert_is_rbt}\hfill(@{text "rbt_insert_is_rbt"})
    3.18  
    3.19    \noindent
    3.20 -  @{thm delete_is_rbt}\hfill(@{text "delete_is_rbt"})
    3.21 +  @{thm rbt_delete_is_rbt}\hfill(@{text "delete_is_rbt"})
    3.22  
    3.23    \noindent
    3.24 -  @{thm bulkload_is_rbt}\hfill(@{text "bulkload_is_rbt"})
    3.25 +  @{thm rbt_bulkload_is_rbt}\hfill(@{text "bulkload_is_rbt"})
    3.26  
    3.27    \noindent
    3.28 -  @{thm map_entry_is_rbt}\hfill(@{text "map_entry_is_rbt"})
    3.29 +  @{thm rbt_map_entry_is_rbt}\hfill(@{text "map_entry_is_rbt"})
    3.30  
    3.31    \noindent
    3.32    @{thm map_is_rbt}\hfill(@{text "map_is_rbt"})
    3.33  
    3.34    \noindent
    3.35 -  @{thm union_is_rbt}\hfill(@{text "union_is_rbt"})
    3.36 +  @{thm rbt_union_is_rbt}\hfill(@{text "union_is_rbt"})
    3.37  *}
    3.38  
    3.39