merged
authorhuffman
Wed Mar 03 20:20:41 2010 -0800 (2010-03-03)
changeset 3556420995afa8fa1
parent 35563 f5ec817df77f
parent 35554 1e05ea0a5cd7
child 35565 56b070cd7ab3
child 35572 44eeda8cb708
merged
     1.1 --- a/Admin/isatest/isatest-stats	Wed Mar 03 10:40:40 2010 -0800
     1.2 +++ b/Admin/isatest/isatest-stats	Wed Mar 03 20:20:41 2010 -0800
     1.3 @@ -6,7 +6,7 @@
     1.4  
     1.5  THIS=$(cd "$(dirname "$0")"; pwd -P)
     1.6  
     1.7 -PLATFORMS="at-poly at64-poly mac-poly-M4 mac-poly64-M4 mac-poly-M8 mac-poly64-M8 at-poly-5.1-para-e at64-poly-5.1-para at-mac-poly-5.1-para afp at-sml-dev sun-poly"
     1.8 +PLATFORMS="at-poly at-poly-test at64-poly mac-poly-M4 mac-poly64-M4 mac-poly-M8 mac-poly64-M8 at-poly-5.1-para-e at64-poly-5.1-para at-mac-poly-5.1-para afp at-sml-dev sun-poly"
     1.9  
    1.10  ISABELLE_SESSIONS="\
    1.11    HOL-Plain \
     2.1 --- a/src/HOL/Library/RBT.thy	Wed Mar 03 10:40:40 2010 -0800
     2.2 +++ b/src/HOL/Library/RBT.thy	Wed Mar 03 20:20:41 2010 -0800
     2.3 @@ -10,6 +10,8 @@
     2.4  imports Main AssocList
     2.5  begin
     2.6  
     2.7 +subsection {* Datatype of RB trees *}
     2.8 +
     2.9  datatype color = R | B
    2.10  datatype ('a, 'b) rbt = Empty | Branch color "('a, 'b) rbt" 'a 'b "('a, 'b) rbt"
    2.11  
    2.12 @@ -23,39 +25,48 @@
    2.13    case (Branch c) with that show thesis by (cases c) blast+
    2.14  qed
    2.15  
    2.16 -text {* Content of a tree *}
    2.17 +subsection {* Tree properties *}
    2.18  
    2.19 -primrec entries
    2.20 +subsubsection {* Content of a tree *}
    2.21 +
    2.22 +primrec entries :: "('a, 'b) rbt \<Rightarrow> ('a \<times> 'b) list"
    2.23  where 
    2.24    "entries Empty = []"
    2.25  | "entries (Branch _ l k v r) = entries l @ (k,v) # entries r"
    2.26  
    2.27 -text {* Search tree properties *}
    2.28 -
    2.29 -primrec entry_in_tree :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> bool"
    2.30 +abbreviation (input) entry_in_tree :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> bool"
    2.31  where
    2.32 -  "entry_in_tree k v Empty = False"
    2.33 -| "entry_in_tree k v (Branch c l x y r) \<longleftrightarrow> k = x \<and> v = y \<or> entry_in_tree k v l \<or> entry_in_tree k v r"
    2.34 +  "entry_in_tree k v t \<equiv> (k, v) \<in> set (entries t)"
    2.35 +
    2.36 +definition keys :: "('a, 'b) rbt \<Rightarrow> 'a list" where
    2.37 +  "keys t = map fst (entries t)"
    2.38  
    2.39 -primrec keys :: "('k, 'v) rbt \<Rightarrow> 'k set"
    2.40 -where
    2.41 -  "keys Empty = {}"
    2.42 -| "keys (Branch _ l k _ r) = { k } \<union> keys l \<union> keys r"
    2.43 +lemma keys_simps [simp, code]:
    2.44 +  "keys Empty = []"
    2.45 +  "keys (Branch c l k v r) = keys l @ k # keys r"
    2.46 +  by (simp_all add: keys_def)
    2.47  
    2.48  lemma entry_in_tree_keys:
    2.49 -  "entry_in_tree k v t \<Longrightarrow> k \<in> keys t"
    2.50 -  by (induct t) auto
    2.51 +  assumes "(k, v) \<in> set (entries t)"
    2.52 +  shows "k \<in> set (keys t)"
    2.53 +proof -
    2.54 +  from assms have "fst (k, v) \<in> fst ` set (entries t)" by (rule imageI)
    2.55 +  then show ?thesis by (simp add: keys_def)
    2.56 +qed
    2.57 +
    2.58 +
    2.59 +subsubsection {* Search tree properties *}
    2.60  
    2.61  definition tree_less :: "'a\<Colon>order \<Rightarrow> ('a, 'b) rbt \<Rightarrow> bool"
    2.62  where
    2.63 -  tree_less_prop: "tree_less k t \<longleftrightarrow> (\<forall>x\<in>keys t. x < k)"
    2.64 +  tree_less_prop: "tree_less k t \<longleftrightarrow> (\<forall>x\<in>set (keys t). x < k)"
    2.65  
    2.66  abbreviation tree_less_symbol (infix "|\<guillemotleft>" 50)
    2.67  where "t |\<guillemotleft> x \<equiv> tree_less x t"
    2.68  
    2.69  definition tree_greater :: "'a\<Colon>order \<Rightarrow> ('a, 'b) rbt \<Rightarrow> bool" (infix "\<guillemotleft>|" 50) 
    2.70  where
    2.71 -  tree_greater_prop: "tree_greater k t = (\<forall>x\<in>keys t. k < x)"
    2.72 +  tree_greater_prop: "tree_greater k t = (\<forall>x\<in>set (keys t). k < x)"
    2.73  
    2.74  lemma tree_less_simps [simp]:
    2.75    "tree_less k Empty = True"
    2.76 @@ -72,55 +83,172 @@
    2.77  lemmas tree_greater_nit = tree_greater_prop entry_in_tree_keys
    2.78  lemmas tree_less_nit = tree_less_prop entry_in_tree_keys
    2.79  
    2.80 -lemma tree_less_trans: "t |\<guillemotleft> x \<Longrightarrow> x < y \<Longrightarrow> t |\<guillemotleft> y"
    2.81 +lemma tree_less_eq_trans: "l |\<guillemotleft> u \<Longrightarrow> u \<le> v \<Longrightarrow> l |\<guillemotleft> v"
    2.82 +  and tree_less_trans: "t |\<guillemotleft> x \<Longrightarrow> x < y \<Longrightarrow> t |\<guillemotleft> y"
    2.83 +  and tree_greater_eq_trans: "u \<le> v \<Longrightarrow> v \<guillemotleft>| r \<Longrightarrow> u \<guillemotleft>| r"
    2.84    and tree_greater_trans: "x < y \<Longrightarrow> y \<guillemotleft>| t \<Longrightarrow> x \<guillemotleft>| t"
    2.85 -by (auto simp: tree_ord_props)
    2.86 +  by (auto simp: tree_ord_props)
    2.87  
    2.88  primrec sorted :: "('a::linorder, 'b) rbt \<Rightarrow> bool"
    2.89  where
    2.90    "sorted Empty = True"
    2.91  | "sorted (Branch c l k v r) = (l |\<guillemotleft> k \<and> k \<guillemotleft>| r \<and> sorted l \<and> sorted r)"
    2.92  
    2.93 +lemma sorted_entries:
    2.94 +  "sorted t \<Longrightarrow> List.sorted (List.map fst (entries t))"
    2.95 +by (induct t) 
    2.96 +  (force simp: sorted_append sorted_Cons tree_ord_props 
    2.97 +      dest!: entry_in_tree_keys)+
    2.98 +
    2.99 +lemma distinct_entries:
   2.100 +  "sorted t \<Longrightarrow> distinct (List.map fst (entries t))"
   2.101 +by (induct t) 
   2.102 +  (force simp: sorted_append sorted_Cons tree_ord_props 
   2.103 +      dest!: entry_in_tree_keys)+
   2.104 +
   2.105 +
   2.106 +subsubsection {* Tree lookup *}
   2.107 +
   2.108  primrec lookup :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b"
   2.109  where
   2.110    "lookup Empty k = None"
   2.111  | "lookup (Branch _ l x y r) k = (if k < x then lookup l k else if x < k then lookup r k else Some y)"
   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 +
   2.116 +lemma dom_lookup_Branch: 
   2.117 +  "sorted (Branch c t1 k v t2) \<Longrightarrow> 
   2.118 +    dom (lookup (Branch c t1 k v t2)) 
   2.119 +    = Set.insert k (dom (lookup t1) \<union> dom (lookup t2))"
   2.120 +proof -
   2.121 +  assume "sorted (Branch c t1 k v t2)"
   2.122 +  moreover from this have "sorted t1" "sorted t2" by simp_all
   2.123 +  ultimately show ?thesis by (simp add: lookup_keys)
   2.124 +qed
   2.125 +
   2.126 +lemma finite_dom_lookup [simp, intro!]: "finite (dom (lookup t))"
   2.127 +proof (induct t)
   2.128 +  case Empty then show ?case by simp
   2.129 +next
   2.130 +  case (Branch color t1 a b t2)
   2.131 +  let ?A = "Set.insert a (dom (lookup t1) \<union> dom (lookup t2))"
   2.132 +  have "dom (lookup (Branch color t1 a b t2)) \<subseteq> ?A" by (auto split: split_if_asm)
   2.133 +  moreover from Branch have "finite (insert a (dom (lookup t1) \<union> dom (lookup t2)))" by simp
   2.134 +  ultimately show ?case by (rule finite_subset)
   2.135 +qed 
   2.136 +
   2.137  lemma lookup_tree_less[simp]: "t |\<guillemotleft> k \<Longrightarrow> lookup t k = None" 
   2.138  by (induct t) auto
   2.139  
   2.140  lemma lookup_tree_greater[simp]: "k \<guillemotleft>| t \<Longrightarrow> lookup t k = None"
   2.141  by (induct t) auto
   2.142  
   2.143 -lemma lookup_keys: "sorted t \<Longrightarrow> dom (lookup t) = keys t"
   2.144 -by (induct t) (auto simp: dom_def tree_greater_prop tree_less_prop)
   2.145 -
   2.146 -lemma lookup_pit: "sorted t \<Longrightarrow> (lookup t k = Some v) = entry_in_tree k v t"
   2.147 +lemma lookup_in_tree: "sorted t \<Longrightarrow> (lookup t k = Some v) = entry_in_tree k v t"
   2.148  by (induct t) (auto simp: tree_less_prop tree_greater_prop entry_in_tree_keys)
   2.149  
   2.150  lemma lookup_Empty: "lookup Empty = empty"
   2.151  by (rule ext) simp
   2.152  
   2.153 +lemma lookup_map_of_entries:
   2.154 +  "sorted t \<Longrightarrow> lookup t = map_of (entries t)"
   2.155 +proof (induct t)
   2.156 +  case Empty thus ?case by (simp add: lookup_Empty)
   2.157 +next
   2.158 +  case (Branch c t1 k v t2)
   2.159 +  have "lookup (Branch c t1 k v t2) = lookup t2 ++ [k\<mapsto>v] ++ lookup t1"
   2.160 +  proof (rule ext)
   2.161 +    fix x
   2.162 +    from Branch have SORTED: "sorted (Branch c t1 k v t2)" by simp
   2.163 +    let ?thesis = "lookup (Branch c t1 k v t2) x = (lookup t2 ++ [k \<mapsto> v] ++ lookup t1) x"
   2.164 +
   2.165 +    have DOM_T1: "!!k'. k'\<in>dom (lookup t1) \<Longrightarrow> k>k'"
   2.166 +    proof -
   2.167 +      fix k'
   2.168 +      from SORTED have "t1 |\<guillemotleft> k" by simp
   2.169 +      with tree_less_prop have "\<forall>k'\<in>set (keys t1). k>k'" by auto
   2.170 +      moreover assume "k'\<in>dom (lookup t1)"
   2.171 +      ultimately show "k>k'" using lookup_keys SORTED by auto
   2.172 +    qed
   2.173 +    
   2.174 +    have DOM_T2: "!!k'. k'\<in>dom (lookup t2) \<Longrightarrow> k<k'"
   2.175 +    proof -
   2.176 +      fix k'
   2.177 +      from SORTED have "k \<guillemotleft>| t2" by simp
   2.178 +      with tree_greater_prop have "\<forall>k'\<in>set (keys t2). k<k'" by auto
   2.179 +      moreover assume "k'\<in>dom (lookup t2)"
   2.180 +      ultimately show "k<k'" using lookup_keys SORTED by auto
   2.181 +    qed
   2.182 +    
   2.183 +    {
   2.184 +      assume C: "x<k"
   2.185 +      hence "lookup (Branch c t1 k v t2) x = lookup t1 x" by simp
   2.186 +      moreover from C have "x\<notin>dom [k\<mapsto>v]" by simp
   2.187 +      moreover have "x\<notin>dom (lookup t2)" proof
   2.188 +        assume "x\<in>dom (lookup t2)"
   2.189 +        with DOM_T2 have "k<x" by blast
   2.190 +        with C show False by simp
   2.191 +      qed
   2.192 +      ultimately have ?thesis by (simp add: map_add_upd_left map_add_dom_app_simps)
   2.193 +    } moreover {
   2.194 +      assume [simp]: "x=k"
   2.195 +      hence "lookup (Branch c t1 k v t2) x = [k \<mapsto> v] x" by simp
   2.196 +      moreover have "x\<notin>dom (lookup t1)" proof
   2.197 +        assume "x\<in>dom (lookup t1)"
   2.198 +        with DOM_T1 have "k>x" by blast
   2.199 +        thus False by simp
   2.200 +      qed
   2.201 +      ultimately have ?thesis by (simp add: map_add_upd_left map_add_dom_app_simps)
   2.202 +    } moreover {
   2.203 +      assume C: "x>k"
   2.204 +      hence "lookup (Branch c t1 k v t2) x = lookup t2 x" by (simp add: less_not_sym[of k x])
   2.205 +      moreover from C have "x\<notin>dom [k\<mapsto>v]" by simp
   2.206 +      moreover have "x\<notin>dom (lookup t1)" proof
   2.207 +        assume "x\<in>dom (lookup t1)"
   2.208 +        with DOM_T1 have "k>x" by simp
   2.209 +        with C show False by simp
   2.210 +      qed
   2.211 +      ultimately have ?thesis by (simp add: map_add_upd_left map_add_dom_app_simps)
   2.212 +    } ultimately show ?thesis using less_linear by blast
   2.213 +  qed
   2.214 +  also from Branch have "lookup t2 ++ [k \<mapsto> v] ++ lookup t1 = map_of (entries (Branch c t1 k v t2))" by simp
   2.215 +  finally show ?case .
   2.216 +qed
   2.217 +
   2.218 +(*lemma map_of_inject:
   2.219 +  assumes distinct: "distinct (map fst xs)" "distinct (map fst ys)"
   2.220 +  shows "map_of xs = map_of ys \<longleftrightarrow> set xs = set ys"
   2.221 +
   2.222 +lemma entries_eqI:
   2.223 +  assumes sorted: "sorted t1" "sorted t2" 
   2.224 +  assumes lookup: "lookup t1 = lookup t2"
   2.225 +  shows entries: "entries t1 = entries t2"
   2.226 +proof -
   2.227 +  from sorted lookup have "map_of (entries t1) = map_of (entries t2)"
   2.228 +    by (simp_all add: lookup_map_of_entries)
   2.229 +qed*)
   2.230 +
   2.231  (* a kind of extensionality *)
   2.232 -lemma lookup_from_pit: 
   2.233 +lemma lookup_from_in_tree: 
   2.234    assumes sorted: "sorted t1" "sorted t2" 
   2.235    and eq: "\<And>v. entry_in_tree (k\<Colon>'a\<Colon>linorder) v t1 = entry_in_tree k v t2" 
   2.236    shows "lookup t1 k = lookup t2 k"
   2.237  proof (cases "lookup t1 k")
   2.238    case None
   2.239    then have "\<And>v. \<not> entry_in_tree k v t1"
   2.240 -    by (simp add: lookup_pit[symmetric] sorted)
   2.241 +    by (simp add: lookup_in_tree[symmetric] sorted)
   2.242    with None show ?thesis
   2.243 -    by (cases "lookup t2 k") (auto simp: lookup_pit sorted eq)
   2.244 +    by (cases "lookup t2 k") (auto simp: lookup_in_tree sorted eq)
   2.245  next
   2.246    case (Some a)
   2.247    then show ?thesis
   2.248      apply (cases "lookup t2 k")
   2.249 -    apply (auto simp: lookup_pit sorted eq)
   2.250 -    by (auto simp add: lookup_pit[symmetric] sorted Some)
   2.251 +    apply (auto simp: lookup_in_tree sorted eq)
   2.252 +    by (auto simp add: lookup_in_tree[symmetric] sorted Some)
   2.253  qed
   2.254  
   2.255 -subsection {* Red-black properties *}
   2.256 +
   2.257 +subsubsection {* Red-black properties *}
   2.258  
   2.259  primrec color_of :: "('a, 'b) rbt \<Rightarrow> color"
   2.260  where
   2.261 @@ -240,19 +368,23 @@
   2.262    with 1 "5_4" show ?case by simp
   2.263  qed simp+
   2.264  
   2.265 -lemma keys_balance[simp]: 
   2.266 -  "keys (balance l k v r) = { k } \<union> keys l \<union> keys r"
   2.267 -by (induct l k v r rule: balance.induct) auto
   2.268 +lemma entries_balance [simp]:
   2.269 +  "entries (balance l k v r) = entries l @ (k, v) # entries r"
   2.270 +  by (induct l k v r rule: balance.induct) auto
   2.271  
   2.272 -lemma balance_pit:  
   2.273 -  "entry_in_tree k x (balance l v y r) = (entry_in_tree k x l \<or> k = v \<and> x = y \<or> entry_in_tree k x r)" 
   2.274 -by (induct l v y r rule: balance.induct) auto
   2.275 +lemma keys_balance [simp]: 
   2.276 +  "keys (balance l k v r) = keys l @ k # keys r"
   2.277 +  by (simp add: keys_def)
   2.278 +
   2.279 +lemma balance_in_tree:  
   2.280 +  "entry_in_tree k x (balance l v y r) \<longleftrightarrow> entry_in_tree k x l \<or> k = v \<and> x = y \<or> entry_in_tree k x r"
   2.281 +  by (auto simp add: keys_def)
   2.282  
   2.283  lemma lookup_balance[simp]: 
   2.284  fixes k :: "'a::linorder"
   2.285  assumes "sorted l" "sorted r" "l |\<guillemotleft> k" "k \<guillemotleft>| r"
   2.286  shows "lookup (balance l k v r) x = lookup (Branch B l k v r) x"
   2.287 -by (rule lookup_from_pit) (auto simp:assms balance_pit balance_sorted)
   2.288 +by (rule lookup_from_in_tree) (auto simp:assms balance_in_tree balance_sorted)
   2.289  
   2.290  primrec paint :: "color \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
   2.291  where
   2.292 @@ -264,7 +396,7 @@
   2.293  lemma paint_inv2[simp]: "inv2 t \<Longrightarrow> inv2 (paint c t)" by (cases t) auto
   2.294  lemma paint_color_of[simp]: "color_of (paint B t) = B" by (cases t) auto
   2.295  lemma paint_sorted[simp]: "sorted t \<Longrightarrow> sorted (paint c t)" by (cases t) auto
   2.296 -lemma paint_pit[simp]: "entry_in_tree k x (paint c t) = entry_in_tree k x t" by (cases t) auto
   2.297 +lemma paint_in_tree[simp]: "entry_in_tree k x (paint c t) = entry_in_tree k x t" by (cases t) auto
   2.298  lemma paint_lookup[simp]: "lookup (paint c t) = lookup t" by (rule ext) (cases t, auto)
   2.299  lemma paint_tree_greater[simp]: "(v \<guillemotleft>| paint c t) = (v \<guillemotleft>| t)" by (cases t) auto
   2.300  lemma paint_tree_less[simp]: "(paint c t |\<guillemotleft> v) = (t |\<guillemotleft> v)" by (cases t) auto
   2.301 @@ -294,8 +426,8 @@
   2.302  lemma ins_sorted[simp]: "sorted t \<Longrightarrow> sorted (ins f k x t)"
   2.303    by (induct f k x t rule: ins.induct) (auto simp: balance_sorted)
   2.304  
   2.305 -lemma keys_ins: "keys (ins f k v t) = { k } \<union> keys t"
   2.306 -by (induct f k v t rule: ins.induct) auto
   2.307 +lemma keys_ins: "set (keys (ins f k v t)) = { k } \<union> set (keys t)"
   2.308 +  by (induct f k v t rule: ins.induct) auto
   2.309  
   2.310  lemma lookup_ins: 
   2.311    fixes k :: "'a::linorder"
   2.312 @@ -305,45 +437,45 @@
   2.313  using assms by (induct f k v t rule: ins.induct) auto
   2.314  
   2.315  definition
   2.316 -  insertwithkey :: "('a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
   2.317 +  insert_with_key :: "('a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
   2.318  where
   2.319 -  "insertwithkey f k v t = paint B (ins f k v t)"
   2.320 +  "insert_with_key f k v t = paint B (ins f k v t)"
   2.321  
   2.322 -lemma insertwk_sorted: "sorted t \<Longrightarrow> sorted (insertwithkey f k x t)"
   2.323 -  by (auto simp: insertwithkey_def)
   2.324 +lemma insertwk_sorted: "sorted t \<Longrightarrow> sorted (insert_with_key f k x t)"
   2.325 +  by (auto simp: insert_with_key_def)
   2.326  
   2.327  theorem insertwk_is_rbt: 
   2.328    assumes inv: "is_rbt t" 
   2.329 -  shows "is_rbt (insertwithkey f k x t)"
   2.330 +  shows "is_rbt (insert_with_key f k x t)"
   2.331  using assms
   2.332 -unfolding insertwithkey_def is_rbt_def
   2.333 +unfolding insert_with_key_def is_rbt_def
   2.334  by (auto simp: ins_inv1_inv2)
   2.335  
   2.336  lemma lookup_insertwk: 
   2.337    assumes "sorted t"
   2.338 -  shows "lookup (insertwithkey f k v t) x = ((lookup t)(k |-> case lookup t k of None \<Rightarrow> v 
   2.339 +  shows "lookup (insert_with_key f k v t) x = ((lookup t)(k |-> case lookup t k of None \<Rightarrow> v 
   2.340                                                         | Some w \<Rightarrow> f k w v)) x"
   2.341 -unfolding insertwithkey_def using assms
   2.342 +unfolding insert_with_key_def using assms
   2.343  by (simp add:lookup_ins)
   2.344  
   2.345  definition
   2.346 -  insertw_def: "insertwith f = insertwithkey (\<lambda>_. f)"
   2.347 +  insertw_def: "insert_with f = insert_with_key (\<lambda>_. f)"
   2.348  
   2.349 -lemma insertw_sorted: "sorted t \<Longrightarrow> sorted (insertwith f k v t)" by (simp add: insertwk_sorted insertw_def)
   2.350 -theorem insertw_is_rbt: "is_rbt t \<Longrightarrow> is_rbt (insertwith f k v t)" by (simp add: insertwk_is_rbt insertw_def)
   2.351 +lemma insertw_sorted: "sorted t \<Longrightarrow> sorted (insert_with f k v t)" by (simp add: insertwk_sorted insertw_def)
   2.352 +theorem insertw_is_rbt: "is_rbt t \<Longrightarrow> is_rbt (insert_with f k v t)" by (simp add: insertwk_is_rbt insertw_def)
   2.353  
   2.354  lemma lookup_insertw:
   2.355    assumes "is_rbt t"
   2.356 -  shows "lookup (insertwith f k v t) = (lookup t)(k \<mapsto> (if k:dom (lookup t) then f (the (lookup t k)) v else v))"
   2.357 +  shows "lookup (insert_with f k v t) = (lookup t)(k \<mapsto> (if k:dom (lookup t) then f (the (lookup t k)) v else v))"
   2.358  using assms
   2.359  unfolding insertw_def
   2.360  by (rule_tac ext) (cases "lookup t k", auto simp:lookup_insertwk dom_def)
   2.361  
   2.362  definition insert :: "'a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" where
   2.363 -  "insert k v t = insertwithkey (\<lambda>_ _ nv. nv) k v t"
   2.364 +  "insert = insert_with_key (\<lambda>_ _ nv. nv)"
   2.365  
   2.366  lemma insert_sorted: "sorted t \<Longrightarrow> sorted (insert k v t)" by (simp add: insertwk_sorted insert_def)
   2.367 -theorem insert_is_rbt: "is_rbt t \<Longrightarrow> is_rbt (insert k v t)" by (simp add: insertwk_is_rbt insert_def)
   2.368 +theorem insert_is_rbt [simp]: "is_rbt t \<Longrightarrow> is_rbt (insert k v t)" by (simp add: insertwk_is_rbt insert_def)
   2.369  
   2.370  lemma lookup_insert: 
   2.371    assumes "is_rbt t"
   2.372 @@ -359,178 +491,174 @@
   2.373  by (cases t rule: rbt_cases) auto
   2.374  
   2.375  fun
   2.376 -  balleft :: "('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
   2.377 +  balance_left :: "('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
   2.378  where
   2.379 -  "balleft (Branch R a k x b) s y c = Branch R (Branch B a k x b) s y c" |
   2.380 -  "balleft bl k x (Branch B a s y b) = balance bl k x (Branch R a s y b)" |
   2.381 -  "balleft bl k x (Branch R (Branch B a s y b) t z c) = Branch R (Branch B bl k x a) s y (balance b t z (paint R c))" |
   2.382 -  "balleft t k x s = Empty"
   2.383 +  "balance_left (Branch R a k x b) s y c = Branch R (Branch B a k x b) s y c" |
   2.384 +  "balance_left bl k x (Branch B a s y b) = balance bl k x (Branch R a s y b)" |
   2.385 +  "balance_left bl k x (Branch R (Branch B a s y b) t z c) = Branch R (Branch B bl k x a) s y (balance b t z (paint R c))" |
   2.386 +  "balance_left t k x s = Empty"
   2.387  
   2.388 -lemma balleft_inv2_with_inv1:
   2.389 +lemma balance_left_inv2_with_inv1:
   2.390    assumes "inv2 lt" "inv2 rt" "bheight lt + 1 = bheight rt" "inv1 rt"
   2.391 -  shows "bheight (balleft lt k v rt) = bheight lt + 1"
   2.392 -  and   "inv2 (balleft lt k v rt)"
   2.393 +  shows "bheight (balance_left lt k v rt) = bheight lt + 1"
   2.394 +  and   "inv2 (balance_left lt k v rt)"
   2.395  using assms 
   2.396 -by (induct lt k v rt rule: balleft.induct) (auto simp: balance_inv2 balance_bheight)
   2.397 +by (induct lt k v rt rule: balance_left.induct) (auto simp: balance_inv2 balance_bheight)
   2.398  
   2.399 -lemma balleft_inv2_app: 
   2.400 +lemma balance_left_inv2_app: 
   2.401    assumes "inv2 lt" "inv2 rt" "bheight lt + 1 = bheight rt" "color_of rt = B"
   2.402 -  shows "inv2 (balleft lt k v rt)" 
   2.403 -        "bheight (balleft lt k v rt) = bheight rt"
   2.404 +  shows "inv2 (balance_left lt k v rt)" 
   2.405 +        "bheight (balance_left lt k v rt) = bheight rt"
   2.406  using assms 
   2.407 -by (induct lt k v rt rule: balleft.induct) (auto simp add: balance_inv2 balance_bheight)+ 
   2.408 +by (induct lt k v rt rule: balance_left.induct) (auto simp add: balance_inv2 balance_bheight)+ 
   2.409  
   2.410 -lemma balleft_inv1: "\<lbrakk>inv1l a; inv1 b; color_of b = B\<rbrakk> \<Longrightarrow> inv1 (balleft a k x b)"
   2.411 -  by (induct a k x b rule: balleft.induct) (simp add: balance_inv1)+
   2.412 +lemma balance_left_inv1: "\<lbrakk>inv1l a; inv1 b; color_of b = B\<rbrakk> \<Longrightarrow> inv1 (balance_left a k x b)"
   2.413 +  by (induct a k x b rule: balance_left.induct) (simp add: balance_inv1)+
   2.414  
   2.415 -lemma balleft_inv1l: "\<lbrakk> inv1l lt; inv1 rt \<rbrakk> \<Longrightarrow> inv1l (balleft lt k x rt)"
   2.416 -by (induct lt k x rt rule: balleft.induct) (auto simp: balance_inv1)
   2.417 +lemma balance_left_inv1l: "\<lbrakk> inv1l lt; inv1 rt \<rbrakk> \<Longrightarrow> inv1l (balance_left lt k x rt)"
   2.418 +by (induct lt k x rt rule: balance_left.induct) (auto simp: balance_inv1)
   2.419  
   2.420 -lemma balleft_sorted: "\<lbrakk> sorted l; sorted r; tree_less k l; tree_greater k r \<rbrakk> \<Longrightarrow> sorted (balleft l k v r)"
   2.421 -apply (induct l k v r rule: balleft.induct)
   2.422 +lemma balance_left_sorted: "\<lbrakk> sorted l; sorted r; tree_less k l; tree_greater k r \<rbrakk> \<Longrightarrow> sorted (balance_left l k v r)"
   2.423 +apply (induct l k v r rule: balance_left.induct)
   2.424  apply (auto simp: balance_sorted)
   2.425  apply (unfold tree_greater_prop tree_less_prop)
   2.426  by force+
   2.427  
   2.428 -lemma balleft_tree_greater: 
   2.429 +lemma balance_left_tree_greater: 
   2.430    fixes k :: "'a::order"
   2.431    assumes "k \<guillemotleft>| a" "k \<guillemotleft>| b" "k < x" 
   2.432 -  shows "k \<guillemotleft>| balleft a x t b"
   2.433 +  shows "k \<guillemotleft>| balance_left a x t b"
   2.434  using assms 
   2.435 -by (induct a x t b rule: balleft.induct) auto
   2.436 +by (induct a x t b rule: balance_left.induct) auto
   2.437  
   2.438 -lemma balleft_tree_less: 
   2.439 +lemma balance_left_tree_less: 
   2.440    fixes k :: "'a::order"
   2.441    assumes "a |\<guillemotleft> k" "b |\<guillemotleft> k" "x < k" 
   2.442 -  shows "balleft a x t b |\<guillemotleft> k"
   2.443 +  shows "balance_left a x t b |\<guillemotleft> k"
   2.444  using assms
   2.445 -by (induct a x t b rule: balleft.induct) auto
   2.446 +by (induct a x t b rule: balance_left.induct) auto
   2.447  
   2.448 -lemma balleft_pit: 
   2.449 +lemma balance_left_in_tree: 
   2.450    assumes "inv1l l" "inv1 r" "bheight l + 1 = bheight r"
   2.451 -  shows "entry_in_tree k v (balleft l a b r) = (entry_in_tree k v l \<or> k = a \<and> v = b \<or> entry_in_tree k v r)"
   2.452 +  shows "entry_in_tree k v (balance_left l a b r) = (entry_in_tree k v l \<or> k = a \<and> v = b \<or> entry_in_tree k v r)"
   2.453  using assms 
   2.454 -by (induct l k v r rule: balleft.induct) (auto simp: balance_pit)
   2.455 +by (induct l k v r rule: balance_left.induct) (auto simp: balance_in_tree)
   2.456  
   2.457  fun
   2.458 -  balright :: "('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
   2.459 +  balance_right :: "('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
   2.460  where
   2.461 -  "balright a k x (Branch R b s y c) = Branch R a k x (Branch B b s y c)" |
   2.462 -  "balright (Branch B a k x b) s y bl = balance (Branch R a k x b) s y bl" |
   2.463 -  "balright (Branch R a k x (Branch B b s y c)) t z bl = Branch R (balance (paint R a) k x b) s y (Branch B c t z bl)" |
   2.464 -  "balright t k x s = Empty"
   2.465 +  "balance_right a k x (Branch R b s y c) = Branch R a k x (Branch B b s y c)" |
   2.466 +  "balance_right (Branch B a k x b) s y bl = balance (Branch R a k x b) s y bl" |
   2.467 +  "balance_right (Branch R a k x (Branch B b s y c)) t z bl = Branch R (balance (paint R a) k x b) s y (Branch B c t z bl)" |
   2.468 +  "balance_right t k x s = Empty"
   2.469  
   2.470 -lemma balright_inv2_with_inv1:
   2.471 +lemma balance_right_inv2_with_inv1:
   2.472    assumes "inv2 lt" "inv2 rt" "bheight lt = bheight rt + 1" "inv1 lt"
   2.473 -  shows "inv2 (balright lt k v rt) \<and> bheight (balright lt k v rt) = bheight lt"
   2.474 +  shows "inv2 (balance_right lt k v rt) \<and> bheight (balance_right lt k v rt) = bheight lt"
   2.475  using assms
   2.476 -by (induct lt k v rt rule: balright.induct) (auto simp: balance_inv2 balance_bheight)
   2.477 +by (induct lt k v rt rule: balance_right.induct) (auto simp: balance_inv2 balance_bheight)
   2.478  
   2.479 -lemma balright_inv1: "\<lbrakk>inv1 a; inv1l b; color_of a = B\<rbrakk> \<Longrightarrow> inv1 (balright a k x b)"
   2.480 -by (induct a k x b rule: balright.induct) (simp add: balance_inv1)+
   2.481 +lemma balance_right_inv1: "\<lbrakk>inv1 a; inv1l b; color_of a = B\<rbrakk> \<Longrightarrow> inv1 (balance_right a k x b)"
   2.482 +by (induct a k x b rule: balance_right.induct) (simp add: balance_inv1)+
   2.483  
   2.484 -lemma balright_inv1l: "\<lbrakk> inv1 lt; inv1l rt \<rbrakk> \<Longrightarrow>inv1l (balright lt k x rt)"
   2.485 -by (induct lt k x rt rule: balright.induct) (auto simp: balance_inv1)
   2.486 +lemma balance_right_inv1l: "\<lbrakk> inv1 lt; inv1l rt \<rbrakk> \<Longrightarrow>inv1l (balance_right lt k x rt)"
   2.487 +by (induct lt k x rt rule: balance_right.induct) (auto simp: balance_inv1)
   2.488  
   2.489 -lemma balright_sorted: "\<lbrakk> sorted l; sorted r; tree_less k l; tree_greater k r \<rbrakk> \<Longrightarrow> sorted (balright l k v r)"
   2.490 -apply (induct l k v r rule: balright.induct)
   2.491 +lemma balance_right_sorted: "\<lbrakk> sorted l; sorted r; tree_less k l; tree_greater k r \<rbrakk> \<Longrightarrow> sorted (balance_right l k v r)"
   2.492 +apply (induct l k v r rule: balance_right.induct)
   2.493  apply (auto simp:balance_sorted)
   2.494  apply (unfold tree_less_prop tree_greater_prop)
   2.495  by force+
   2.496  
   2.497 -lemma balright_tree_greater: 
   2.498 +lemma balance_right_tree_greater: 
   2.499    fixes k :: "'a::order"
   2.500    assumes "k \<guillemotleft>| a" "k \<guillemotleft>| b" "k < x" 
   2.501 -  shows "k \<guillemotleft>| balright a x t b"
   2.502 -using assms by (induct a x t b rule: balright.induct) auto
   2.503 +  shows "k \<guillemotleft>| balance_right a x t b"
   2.504 +using assms by (induct a x t b rule: balance_right.induct) auto
   2.505  
   2.506 -lemma balright_tree_less: 
   2.507 +lemma balance_right_tree_less: 
   2.508    fixes k :: "'a::order"
   2.509    assumes "a |\<guillemotleft> k" "b |\<guillemotleft> k" "x < k" 
   2.510 -  shows "balright a x t b |\<guillemotleft> k"
   2.511 -using assms by (induct a x t b rule: balright.induct) auto
   2.512 +  shows "balance_right a x t b |\<guillemotleft> k"
   2.513 +using assms by (induct a x t b rule: balance_right.induct) auto
   2.514  
   2.515 -lemma balright_pit:
   2.516 +lemma balance_right_in_tree:
   2.517    assumes "inv1 l" "inv1l r" "bheight l = bheight r + 1" "inv2 l" "inv2 r"
   2.518 -  shows "entry_in_tree x y (balright l k v r) = (entry_in_tree x y l \<or> x = k \<and> y = v \<or> entry_in_tree x y r)"
   2.519 -using assms by (induct l k v r rule: balright.induct) (auto simp: balance_pit)
   2.520 -
   2.521 -
   2.522 -text {* app *}
   2.523 +  shows "entry_in_tree x y (balance_right l k v r) = (entry_in_tree x y l \<or> x = k \<and> y = v \<or> entry_in_tree x y r)"
   2.524 +using assms by (induct l k v r rule: balance_right.induct) (auto simp: balance_in_tree)
   2.525  
   2.526  fun
   2.527 -  app :: "('a,'b) rbt \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
   2.528 +  combine :: "('a,'b) rbt \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
   2.529  where
   2.530 -  "app Empty x = x" 
   2.531 -| "app x Empty = x" 
   2.532 -| "app (Branch R a k x b) (Branch R c s y d) = (case (app b c) of
   2.533 +  "combine Empty x = x" 
   2.534 +| "combine x Empty = x" 
   2.535 +| "combine (Branch R a k x b) (Branch R c s y d) = (case (combine b c) of
   2.536                                        Branch R b2 t z c2 \<Rightarrow> (Branch R (Branch R a k x b2) t z (Branch R c2 s y d)) |
   2.537                                        bc \<Rightarrow> Branch R a k x (Branch R bc s y d))" 
   2.538 -| "app (Branch B a k x b) (Branch B c s y d) = (case (app b c) of
   2.539 +| "combine (Branch B a k x b) (Branch B c s y d) = (case (combine b c) of
   2.540                                        Branch R b2 t z c2 \<Rightarrow> Branch R (Branch B a k x b2) t z (Branch B c2 s y d) |
   2.541 -                                      bc \<Rightarrow> balleft a k x (Branch B bc s y d))" 
   2.542 -| "app a (Branch R b k x c) = Branch R (app a b) k x c" 
   2.543 -| "app (Branch R a k x b) c = Branch R a k x (app b c)" 
   2.544 +                                      bc \<Rightarrow> balance_left a k x (Branch B bc s y d))" 
   2.545 +| "combine a (Branch R b k x c) = Branch R (combine a b) k x c" 
   2.546 +| "combine (Branch R a k x b) c = Branch R a k x (combine b c)" 
   2.547  
   2.548 -lemma app_inv2:
   2.549 +lemma combine_inv2:
   2.550    assumes "inv2 lt" "inv2 rt" "bheight lt = bheight rt"
   2.551 -  shows "bheight (app lt rt) = bheight lt" "inv2 (app lt rt)"
   2.552 +  shows "bheight (combine lt rt) = bheight lt" "inv2 (combine lt rt)"
   2.553  using assms 
   2.554 -by (induct lt rt rule: app.induct) 
   2.555 -   (auto simp: balleft_inv2_app split: rbt.splits color.splits)
   2.556 +by (induct lt rt rule: combine.induct) 
   2.557 +   (auto simp: balance_left_inv2_app split: rbt.splits color.splits)
   2.558  
   2.559 -lemma app_inv1: 
   2.560 +lemma combine_inv1: 
   2.561    assumes "inv1 lt" "inv1 rt"
   2.562 -  shows "color_of lt = B \<Longrightarrow> color_of rt = B \<Longrightarrow> inv1 (app lt rt)"
   2.563 -         "inv1l (app lt rt)"
   2.564 +  shows "color_of lt = B \<Longrightarrow> color_of rt = B \<Longrightarrow> inv1 (combine lt rt)"
   2.565 +         "inv1l (combine lt rt)"
   2.566  using assms 
   2.567 -by (induct lt rt rule: app.induct)
   2.568 -   (auto simp: balleft_inv1 split: rbt.splits color.splits)
   2.569 +by (induct lt rt rule: combine.induct)
   2.570 +   (auto simp: balance_left_inv1 split: rbt.splits color.splits)
   2.571  
   2.572 -lemma app_tree_greater[simp]: 
   2.573 +lemma combine_tree_greater[simp]: 
   2.574    fixes k :: "'a::linorder"
   2.575    assumes "k \<guillemotleft>| l" "k \<guillemotleft>| r" 
   2.576 -  shows "k \<guillemotleft>| app l r"
   2.577 +  shows "k \<guillemotleft>| combine l r"
   2.578  using assms 
   2.579 -by (induct l r rule: app.induct)
   2.580 -   (auto simp: balleft_tree_greater split:rbt.splits color.splits)
   2.581 +by (induct l r rule: combine.induct)
   2.582 +   (auto simp: balance_left_tree_greater split:rbt.splits color.splits)
   2.583  
   2.584 -lemma app_tree_less[simp]: 
   2.585 +lemma combine_tree_less[simp]: 
   2.586    fixes k :: "'a::linorder"
   2.587    assumes "l |\<guillemotleft> k" "r |\<guillemotleft> k" 
   2.588 -  shows "app l r |\<guillemotleft> k"
   2.589 +  shows "combine l r |\<guillemotleft> k"
   2.590  using assms 
   2.591 -by (induct l r rule: app.induct)
   2.592 -   (auto simp: balleft_tree_less split:rbt.splits color.splits)
   2.593 +by (induct l r rule: combine.induct)
   2.594 +   (auto simp: balance_left_tree_less split:rbt.splits color.splits)
   2.595  
   2.596 -lemma app_sorted: 
   2.597 +lemma combine_sorted: 
   2.598    fixes k :: "'a::linorder"
   2.599    assumes "sorted l" "sorted r" "l |\<guillemotleft> k" "k \<guillemotleft>| r"
   2.600 -  shows "sorted (app l r)"
   2.601 -using assms proof (induct l r rule: app.induct)
   2.602 +  shows "sorted (combine l r)"
   2.603 +using assms proof (induct l r rule: combine.induct)
   2.604    case (3 a x v b c y w d)
   2.605    hence ineqs: "a |\<guillemotleft> x" "x \<guillemotleft>| b" "b |\<guillemotleft> k" "k \<guillemotleft>| c" "c |\<guillemotleft> y" "y \<guillemotleft>| d"
   2.606      by auto
   2.607    with 3
   2.608    show ?case
   2.609 -    apply (cases "app b c" rule: rbt_cases)
   2.610 -    apply auto
   2.611 -    by (metis app_tree_greater app_tree_less ineqs ineqs tree_less_simps(2) tree_greater_simps(2) tree_greater_trans tree_less_trans)+
   2.612 +    by (cases "combine b c" rule: rbt_cases)
   2.613 +      (auto, (metis combine_tree_greater combine_tree_less ineqs ineqs tree_less_simps(2) tree_greater_simps(2) tree_greater_trans tree_less_trans)+)
   2.614  next
   2.615    case (4 a x v b c y w d)
   2.616    hence "x < k \<and> tree_greater k c" by simp
   2.617    hence "tree_greater x c" by (blast dest: tree_greater_trans)
   2.618 -  with 4 have 2: "tree_greater x (app b c)" by (simp add: app_tree_greater)
   2.619 +  with 4 have 2: "tree_greater x (combine b c)" by (simp add: combine_tree_greater)
   2.620    from 4 have "k < y \<and> tree_less k b" by simp
   2.621    hence "tree_less y b" by (blast dest: tree_less_trans)
   2.622 -  with 4 have 3: "tree_less y (app b c)" by (simp add: app_tree_less)
   2.623 +  with 4 have 3: "tree_less y (combine b c)" by (simp add: combine_tree_less)
   2.624    show ?case
   2.625 -  proof (cases "app b c" rule: rbt_cases)
   2.626 +  proof (cases "combine b c" rule: rbt_cases)
   2.627      case Empty
   2.628      from 4 have "x < y \<and> tree_greater y d" by auto
   2.629      hence "tree_greater x d" by (blast dest: tree_greater_trans)
   2.630      with 4 Empty have "sorted a" and "sorted (Branch B Empty y w d)" and "tree_less x a" and "tree_greater x (Branch B Empty y w d)" by auto
   2.631 -    with Empty show ?thesis by (simp add: balleft_sorted)
   2.632 +    with Empty show ?thesis by (simp add: balance_left_sorted)
   2.633    next
   2.634      case (Red lta va ka rta)
   2.635      with 2 4 have "x < va \<and> tree_less x a" by simp
   2.636 @@ -542,71 +670,71 @@
   2.637      case (Black lta va ka rta)
   2.638      from 4 have "x < y \<and> tree_greater y d" by auto
   2.639      hence "tree_greater x d" by (blast dest: tree_greater_trans)
   2.640 -    with Black 2 3 4 have "sorted a" and "sorted (Branch B (app b c) y w d)" and "tree_less x a" and "tree_greater x (Branch B (app b c) y w d)" by auto
   2.641 -    with Black show ?thesis by (simp add: balleft_sorted)
   2.642 +    with Black 2 3 4 have "sorted a" and "sorted (Branch B (combine b c) y w d)" and "tree_less x a" and "tree_greater x (Branch B (combine b c) y w d)" by auto
   2.643 +    with Black show ?thesis by (simp add: balance_left_sorted)
   2.644    qed
   2.645  next
   2.646    case (5 va vb vd vc b x w c)
   2.647    hence "k < x \<and> tree_less k (Branch B va vb vd vc)" by simp
   2.648    hence "tree_less x (Branch B va vb vd vc)" by (blast dest: tree_less_trans)
   2.649 -  with 5 show ?case by (simp add: app_tree_less)
   2.650 +  with 5 show ?case by (simp add: combine_tree_less)
   2.651  next
   2.652    case (6 a x v b va vb vd vc)
   2.653    hence "x < k \<and> tree_greater k (Branch B va vb vd vc)" by simp
   2.654    hence "tree_greater x (Branch B va vb vd vc)" by (blast dest: tree_greater_trans)
   2.655 -  with 6 show ?case by (simp add: app_tree_greater)
   2.656 +  with 6 show ?case by (simp add: combine_tree_greater)
   2.657  qed simp+
   2.658  
   2.659 -lemma app_pit: 
   2.660 +lemma combine_in_tree: 
   2.661    assumes "inv2 l" "inv2 r" "bheight l = bheight r" "inv1 l" "inv1 r"
   2.662 -  shows "entry_in_tree k v (app l r) = (entry_in_tree k v l \<or> entry_in_tree k v r)"
   2.663 +  shows "entry_in_tree k v (combine l r) = (entry_in_tree k v l \<or> entry_in_tree k v r)"
   2.664  using assms 
   2.665 -proof (induct l r rule: app.induct)
   2.666 +proof (induct l r rule: combine.induct)
   2.667    case (4 _ _ _ b c)
   2.668 -  hence a: "bheight (app b c) = bheight b" by (simp add: app_inv2)
   2.669 -  from 4 have b: "inv1l (app b c)" by (simp add: app_inv1)
   2.670 +  hence a: "bheight (combine b c) = bheight b" by (simp add: combine_inv2)
   2.671 +  from 4 have b: "inv1l (combine b c)" by (simp add: combine_inv1)
   2.672  
   2.673    show ?case
   2.674 -  proof (cases "app b c" rule: rbt_cases)
   2.675 +  proof (cases "combine b c" rule: rbt_cases)
   2.676      case Empty
   2.677 -    with 4 a show ?thesis by (auto simp: balleft_pit)
   2.678 +    with 4 a show ?thesis by (auto simp: balance_left_in_tree)
   2.679    next
   2.680      case (Red lta ka va rta)
   2.681      with 4 show ?thesis by auto
   2.682    next
   2.683      case (Black lta ka va rta)
   2.684 -    with a b 4  show ?thesis by (auto simp: balleft_pit)
   2.685 +    with a b 4  show ?thesis by (auto simp: balance_left_in_tree)
   2.686    qed 
   2.687  qed (auto split: rbt.splits color.splits)
   2.688  
   2.689  fun
   2.690 -  delformLeft :: "('a\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" and
   2.691 -  delformRight :: "('a\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" and
   2.692 +  del_from_left :: "('a\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" and
   2.693 +  del_from_right :: "('a\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt" and
   2.694    del :: "('a\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
   2.695  where
   2.696    "del x Empty = Empty" |
   2.697 -  "del x (Branch c a y s b) = (if x < y then delformLeft x a y s b else (if x > y then delformRight x a y s b else app a b))" |
   2.698 -  "delformLeft x (Branch B lt z v rt) y s b = balleft (del x (Branch B lt z v rt)) y s b" |
   2.699 -  "delformLeft x a y s b = Branch R (del x a) y s b" |
   2.700 -  "delformRight x a y s (Branch B lt z v rt) = balright a y s (del x (Branch B lt z v rt))" | 
   2.701 -  "delformRight x a y s b = Branch R a y s (del x b)"
   2.702 +  "del x (Branch c a y s b) = (if x < y then del_from_left x a y s b else (if x > y then del_from_right x a y s b else combine a b))" |
   2.703 +  "del_from_left x (Branch B lt z v rt) y s b = balance_left (del x (Branch B lt z v rt)) y s b" |
   2.704 +  "del_from_left x a y s b = Branch R (del x a) y s b" |
   2.705 +  "del_from_right x a y s (Branch B lt z v rt) = balance_right a y s (del x (Branch B lt z v rt))" | 
   2.706 +  "del_from_right x a y s b = Branch R a y s (del x b)"
   2.707  
   2.708  lemma 
   2.709    assumes "inv2 lt" "inv1 lt"
   2.710    shows
   2.711    "\<lbrakk>inv2 rt; bheight lt = bheight rt; inv1 rt\<rbrakk> \<Longrightarrow>
   2.712 -  inv2 (delformLeft x lt k v rt) \<and> bheight (delformLeft x lt k v rt) = bheight lt \<and> (color_of lt = B \<and> color_of rt = B \<and> inv1 (delformLeft x lt k v rt) \<or> (color_of lt \<noteq> B \<or> color_of rt \<noteq> B) \<and> inv1l (delformLeft x lt k v rt))"
   2.713 +  inv2 (del_from_left x lt k v rt) \<and> bheight (del_from_left x lt k v rt) = bheight lt \<and> (color_of lt = B \<and> color_of rt = B \<and> inv1 (del_from_left x lt k v rt) \<or> (color_of lt \<noteq> B \<or> color_of rt \<noteq> B) \<and> inv1l (del_from_left x lt k v rt))"
   2.714    and "\<lbrakk>inv2 rt; bheight lt = bheight rt; inv1 rt\<rbrakk> \<Longrightarrow>
   2.715 -  inv2 (delformRight x lt k v rt) \<and> bheight (delformRight x lt k v rt) = bheight lt \<and> (color_of lt = B \<and> color_of rt = B \<and> inv1 (delformRight x lt k v rt) \<or> (color_of lt \<noteq> B \<or> color_of rt \<noteq> B) \<and> inv1l (delformRight x lt k v rt))"
   2.716 +  inv2 (del_from_right x lt k v rt) \<and> bheight (del_from_right x lt k v rt) = bheight lt \<and> (color_of lt = B \<and> color_of rt = B \<and> inv1 (del_from_right x lt k v rt) \<or> (color_of lt \<noteq> B \<or> color_of rt \<noteq> B) \<and> inv1l (del_from_right x lt k v rt))"
   2.717    and del_inv1_inv2: "inv2 (del x lt) \<and> (color_of lt = R \<and> bheight (del x lt) = bheight lt \<and> inv1 (del x lt) 
   2.718    \<or> color_of lt = B \<and> bheight (del x lt) = bheight lt - 1 \<and> inv1l (del x lt))"
   2.719  using assms
   2.720 -proof (induct x lt k v rt and x lt k v rt and x lt rule: delformLeft_delformRight_del.induct)
   2.721 +proof (induct x lt k v rt and x lt k v rt and x lt rule: del_from_left_del_from_right_del.induct)
   2.722  case (2 y c _ y')
   2.723    have "y = y' \<or> y < y' \<or> y > y'" by auto
   2.724    thus ?case proof (elim disjE)
   2.725      assume "y = y'"
   2.726 -    with 2 show ?thesis by (cases c) (simp add: app_inv2 app_inv1)+
   2.727 +    with 2 show ?thesis by (cases c) (simp add: combine_inv2 combine_inv1)+
   2.728    next
   2.729      assume "y < y'"
   2.730      with 2 show ?thesis by (cases c) auto
   2.731 @@ -616,35 +744,35 @@
   2.732    qed
   2.733  next
   2.734    case (3 y lt z v rta y' ss bb) 
   2.735 -  thus ?case by (cases "color_of (Branch B lt z v rta) = B \<and> color_of bb = B") (simp add: balleft_inv2_with_inv1 balleft_inv1 balleft_inv1l)+
   2.736 +  thus ?case by (cases "color_of (Branch B lt z v rta) = B \<and> color_of bb = B") (simp add: balance_left_inv2_with_inv1 balance_left_inv1 balance_left_inv1l)+
   2.737  next
   2.738    case (5 y a y' ss lt z v rta)
   2.739 -  thus ?case by (cases "color_of a = B \<and> color_of (Branch B lt z v rta) = B") (simp add: balright_inv2_with_inv1 balright_inv1 balright_inv1l)+
   2.740 +  thus ?case by (cases "color_of a = B \<and> color_of (Branch B lt z v rta) = B") (simp add: balance_right_inv2_with_inv1 balance_right_inv1 balance_right_inv1l)+
   2.741  next
   2.742    case ("6_1" y a y' ss) thus ?case by (cases "color_of a = B \<and> color_of Empty = B") simp+
   2.743  qed auto
   2.744  
   2.745  lemma 
   2.746 -  delformLeft_tree_less: "\<lbrakk>tree_less v lt; tree_less v rt; k < v\<rbrakk> \<Longrightarrow> tree_less v (delformLeft x lt k y rt)"
   2.747 -  and delformRight_tree_less: "\<lbrakk>tree_less v lt; tree_less v rt; k < v\<rbrakk> \<Longrightarrow> tree_less v (delformRight x lt k y rt)"
   2.748 +  del_from_left_tree_less: "\<lbrakk>tree_less v lt; tree_less v rt; k < v\<rbrakk> \<Longrightarrow> tree_less v (del_from_left x lt k y rt)"
   2.749 +  and del_from_right_tree_less: "\<lbrakk>tree_less v lt; tree_less v rt; k < v\<rbrakk> \<Longrightarrow> tree_less v (del_from_right x lt k y rt)"
   2.750    and del_tree_less: "tree_less v lt \<Longrightarrow> tree_less v (del x lt)"
   2.751 -by (induct x lt k y rt and x lt k y rt and x lt rule: delformLeft_delformRight_del.induct) 
   2.752 -   (auto simp: balleft_tree_less balright_tree_less)
   2.753 +by (induct x lt k y rt and x lt k y rt and x lt rule: del_from_left_del_from_right_del.induct) 
   2.754 +   (auto simp: balance_left_tree_less balance_right_tree_less)
   2.755  
   2.756 -lemma delformLeft_tree_greater: "\<lbrakk>tree_greater v lt; tree_greater v rt; k > v\<rbrakk> \<Longrightarrow> tree_greater v (delformLeft x lt k y rt)"
   2.757 -  and delformRight_tree_greater: "\<lbrakk>tree_greater v lt; tree_greater v rt; k > v\<rbrakk> \<Longrightarrow> tree_greater v (delformRight x lt k y rt)"
   2.758 +lemma del_from_left_tree_greater: "\<lbrakk>tree_greater v lt; tree_greater v rt; k > v\<rbrakk> \<Longrightarrow> tree_greater v (del_from_left x lt k y rt)"
   2.759 +  and del_from_right_tree_greater: "\<lbrakk>tree_greater v lt; tree_greater v rt; k > v\<rbrakk> \<Longrightarrow> tree_greater v (del_from_right x lt k y rt)"
   2.760    and del_tree_greater: "tree_greater v lt \<Longrightarrow> tree_greater v (del x lt)"
   2.761 -by (induct x lt k y rt and x lt k y rt and x lt rule: delformLeft_delformRight_del.induct)
   2.762 -   (auto simp: balleft_tree_greater balright_tree_greater)
   2.763 +by (induct x lt k y rt and x lt k y rt and x lt rule: del_from_left_del_from_right_del.induct)
   2.764 +   (auto simp: balance_left_tree_greater balance_right_tree_greater)
   2.765  
   2.766 -lemma "\<lbrakk>sorted lt; sorted rt; tree_less k lt; tree_greater k rt\<rbrakk> \<Longrightarrow> sorted (delformLeft x lt k y rt)"
   2.767 -  and "\<lbrakk>sorted lt; sorted rt; tree_less k lt; tree_greater k rt\<rbrakk> \<Longrightarrow> sorted (delformRight x lt k y rt)"
   2.768 +lemma "\<lbrakk>sorted lt; sorted rt; tree_less k lt; tree_greater k rt\<rbrakk> \<Longrightarrow> sorted (del_from_left x lt k y rt)"
   2.769 +  and "\<lbrakk>sorted lt; sorted rt; tree_less k lt; tree_greater k rt\<rbrakk> \<Longrightarrow> sorted (del_from_right x lt k y rt)"
   2.770    and del_sorted: "sorted lt \<Longrightarrow> sorted (del x lt)"
   2.771 -proof (induct x lt k y rt and x lt k y rt and x lt rule: delformLeft_delformRight_del.induct)
   2.772 +proof (induct x lt k y rt and x lt k y rt and x lt rule: del_from_left_del_from_right_del.induct)
   2.773    case (3 x lta zz v rta yy ss bb)
   2.774    from 3 have "tree_less yy (Branch B lta zz v rta)" by simp
   2.775    hence "tree_less yy (del x (Branch B lta zz v rta))" by (rule del_tree_less)
   2.776 -  with 3 show ?case by (simp add: balleft_sorted)
   2.777 +  with 3 show ?case by (simp add: balance_left_sorted)
   2.778  next
   2.779    case ("4_2" x vaa vbb vdd vc yy ss bb)
   2.780    hence "tree_less yy (Branch R vaa vbb vdd vc)" by simp
   2.781 @@ -654,18 +782,18 @@
   2.782    case (5 x aa yy ss lta zz v rta) 
   2.783    hence "tree_greater yy (Branch B lta zz v rta)" by simp
   2.784    hence "tree_greater yy (del x (Branch B lta zz v rta))" by (rule del_tree_greater)
   2.785 -  with 5 show ?case by (simp add: balright_sorted)
   2.786 +  with 5 show ?case by (simp add: balance_right_sorted)
   2.787  next
   2.788    case ("6_2" x aa yy ss vaa vbb vdd vc)
   2.789    hence "tree_greater yy (Branch R vaa vbb vdd vc)" by simp
   2.790    hence "tree_greater yy (del x (Branch R vaa vbb vdd vc))" by (rule del_tree_greater)
   2.791    with "6_2" show ?case by simp
   2.792 -qed (auto simp: app_sorted)
   2.793 +qed (auto simp: combine_sorted)
   2.794  
   2.795 -lemma "\<lbrakk>sorted lt; sorted rt; tree_less kt lt; tree_greater kt rt; inv1 lt; inv1 rt; inv2 lt; inv2 rt; bheight lt = bheight rt; x < kt\<rbrakk> \<Longrightarrow> entry_in_tree k v (delformLeft x lt kt y rt) = (False \<or> (x \<noteq> k \<and> entry_in_tree k v (Branch c lt kt y rt)))"
   2.796 -  and "\<lbrakk>sorted lt; sorted rt; tree_less kt lt; tree_greater kt rt; inv1 lt; inv1 rt; inv2 lt; inv2 rt; bheight lt = bheight rt; x > kt\<rbrakk> \<Longrightarrow> entry_in_tree k v (delformRight x lt kt y rt) = (False \<or> (x \<noteq> k \<and> entry_in_tree k v (Branch c lt kt y rt)))"
   2.797 -  and del_pit: "\<lbrakk>sorted t; inv1 t; inv2 t\<rbrakk> \<Longrightarrow> entry_in_tree k v (del x t) = (False \<or> (x \<noteq> k \<and> entry_in_tree k v t))"
   2.798 -proof (induct x lt kt y rt and x lt kt y rt and x t rule: delformLeft_delformRight_del.induct)
   2.799 +lemma "\<lbrakk>sorted lt; sorted rt; tree_less kt lt; tree_greater kt rt; inv1 lt; inv1 rt; inv2 lt; inv2 rt; bheight lt = bheight rt; x < kt\<rbrakk> \<Longrightarrow> entry_in_tree k v (del_from_left x lt kt y rt) = (False \<or> (x \<noteq> k \<and> entry_in_tree k v (Branch c lt kt y rt)))"
   2.800 +  and "\<lbrakk>sorted lt; sorted rt; tree_less kt lt; tree_greater kt rt; inv1 lt; inv1 rt; inv2 lt; inv2 rt; bheight lt = bheight rt; x > kt\<rbrakk> \<Longrightarrow> entry_in_tree k v (del_from_right x lt kt y rt) = (False \<or> (x \<noteq> k \<and> entry_in_tree k v (Branch c lt kt y rt)))"
   2.801 +  and del_in_tree: "\<lbrakk>sorted t; inv1 t; inv2 t\<rbrakk> \<Longrightarrow> entry_in_tree k v (del x t) = (False \<or> (x \<noteq> k \<and> entry_in_tree k v t))"
   2.802 +proof (induct x lt kt y rt and x lt kt y rt and x t rule: del_from_left_del_from_right_del.induct)
   2.803    case (2 xx c aa yy ss bb)
   2.804    have "xx = yy \<or> xx < yy \<or> xx > yy" by auto
   2.805    from this 2 show ?case proof (elim disjE)
   2.806 @@ -674,15 +802,15 @@
   2.807        case True
   2.808        from 2 `xx = yy` `xx = k` have "sorted (Branch c aa yy ss bb) \<and> k = yy" by simp
   2.809        hence "\<not> entry_in_tree k v aa" "\<not> entry_in_tree k v bb" by (auto simp: tree_less_nit tree_greater_prop)
   2.810 -      with `xx = yy` 2 `xx = k` show ?thesis by (simp add: app_pit)
   2.811 -    qed (simp add: app_pit)
   2.812 +      with `xx = yy` 2 `xx = k` show ?thesis by (simp add: combine_in_tree)
   2.813 +    qed (simp add: combine_in_tree)
   2.814    qed simp+
   2.815  next    
   2.816    case (3 xx lta zz vv rta yy ss bb)
   2.817    def mt[simp]: mt == "Branch B lta zz vv rta"
   2.818    from 3 have "inv2 mt \<and> inv1 mt" by simp
   2.819    hence "inv2 (del xx mt) \<and> (color_of mt = R \<and> bheight (del xx mt) = bheight mt \<and> inv1 (del xx mt) \<or> color_of mt = B \<and> bheight (del xx mt) = bheight mt - 1 \<and> inv1l (del xx mt))" by (blast dest: del_inv1_inv2)
   2.820 -  with 3 have 4: "entry_in_tree k v (delformLeft xx mt yy ss bb) = (False \<or> xx \<noteq> k \<and> entry_in_tree k v mt \<or> (k = yy \<and> v = ss) \<or> entry_in_tree k v bb)" by (simp add: balleft_pit)
   2.821 +  with 3 have 4: "entry_in_tree k v (del_from_left xx mt yy ss bb) = (False \<or> xx \<noteq> k \<and> entry_in_tree k v mt \<or> (k = yy \<and> v = ss) \<or> entry_in_tree k v bb)" by (simp add: balance_left_in_tree)
   2.822    thus ?case proof (cases "xx = k")
   2.823      case True
   2.824      from 3 True have "tree_greater yy bb \<and> yy > k" by simp
   2.825 @@ -706,13 +834,13 @@
   2.826      with "4_2" have "k < yy \<and> tree_greater yy bb" by simp
   2.827      hence "tree_greater k bb" by (blast dest: tree_greater_trans)
   2.828      with True "4_2" show ?thesis by (auto simp: tree_greater_nit)
   2.829 -  qed simp
   2.830 +  qed auto
   2.831  next
   2.832    case (5 xx aa yy ss lta zz vv rta)
   2.833    def mt[simp]: mt == "Branch B lta zz vv rta"
   2.834    from 5 have "inv2 mt \<and> inv1 mt" by simp
   2.835    hence "inv2 (del xx mt) \<and> (color_of mt = R \<and> bheight (del xx mt) = bheight mt \<and> inv1 (del xx mt) \<or> color_of mt = B \<and> bheight (del xx mt) = bheight mt - 1 \<and> inv1l (del xx mt))" by (blast dest: del_inv1_inv2)
   2.836 -  with 5 have 3: "entry_in_tree k v (delformRight xx aa yy ss mt) = (entry_in_tree k v aa \<or> (k = yy \<and> v = ss) \<or> False \<or> xx \<noteq> k \<and> entry_in_tree k v mt)" by (simp add: balright_pit)
   2.837 +  with 5 have 3: "entry_in_tree k v (del_from_right xx aa yy ss mt) = (entry_in_tree k v aa \<or> (k = yy \<and> v = ss) \<or> False \<or> xx \<noteq> k \<and> entry_in_tree k v mt)" by (simp add: balance_right_in_tree)
   2.838    thus ?case proof (cases "xx = k")
   2.839      case True
   2.840      from 5 True have "tree_less yy aa \<and> yy < k" by simp
   2.841 @@ -734,14 +862,14 @@
   2.842      with "6_2" have "k > yy \<and> tree_less yy aa" by simp
   2.843      hence "tree_less k aa" by (blast dest: tree_less_trans)
   2.844      with True "6_2" show ?thesis by (auto simp: tree_less_nit)
   2.845 -  qed simp
   2.846 +  qed auto
   2.847  qed simp
   2.848  
   2.849  
   2.850  definition delete where
   2.851    delete_def: "delete k t = paint B (del k t)"
   2.852  
   2.853 -theorem delete_is_rbt[simp]: assumes "is_rbt t" shows "is_rbt (delete k t)"
   2.854 +theorem delete_is_rbt [simp]: assumes "is_rbt t" shows "is_rbt (delete k t)"
   2.855  proof -
   2.856    from assms have "inv2 t" and "inv1 t" unfolding is_rbt_def by auto 
   2.857    hence "inv2 (del k t) \<and> (color_of t = R \<and> bheight (del k t) = bheight t \<and> inv1 (del k t) \<or> color_of t = B \<and> bheight (del k t) = bheight t - 1 \<and> inv1l (del k t))" by (rule del_inv1_inv2)
   2.858 @@ -751,11 +879,11 @@
   2.859      by (auto intro: paint_sorted del_sorted)
   2.860  qed
   2.861  
   2.862 -lemma delete_pit: 
   2.863 +lemma delete_in_tree: 
   2.864    assumes "is_rbt t" 
   2.865    shows "entry_in_tree k v (delete x t) = (x \<noteq> k \<and> entry_in_tree k v t)"
   2.866    using assms unfolding is_rbt_def delete_def
   2.867 -  by (auto simp: del_pit)
   2.868 +  by (auto simp: del_in_tree)
   2.869  
   2.870  lemma lookup_delete:
   2.871    assumes is_rbt: "is_rbt t"
   2.872 @@ -766,35 +894,36 @@
   2.873    proof (cases "x = k")
   2.874      assume "x = k" 
   2.875      with is_rbt show ?thesis
   2.876 -      by (cases "lookup (delete k t) k") (auto simp: lookup_pit delete_pit)
   2.877 +      by (cases "lookup (delete k t) k") (auto simp: lookup_in_tree delete_in_tree)
   2.878    next
   2.879      assume "x \<noteq> k"
   2.880      thus ?thesis
   2.881 -      by auto (metis is_rbt delete_is_rbt delete_pit is_rbt_sorted lookup_from_pit)
   2.882 +      by auto (metis is_rbt delete_is_rbt delete_in_tree is_rbt_sorted lookup_from_in_tree)
   2.883    qed
   2.884  qed
   2.885  
   2.886 +
   2.887  subsection {* Union *}
   2.888  
   2.889  primrec
   2.890 -  unionwithkey :: "('a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
   2.891 +  union_with_key :: "('a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
   2.892  where
   2.893 -  "unionwithkey f t Empty = t"
   2.894 -| "unionwithkey f t (Branch c lt k v rt) = unionwithkey f (unionwithkey f (insertwithkey f k v t) lt) rt"
   2.895 +  "union_with_key f t Empty = t"
   2.896 +| "union_with_key f t (Branch c lt k v rt) = union_with_key f (union_with_key f (insert_with_key f k v t) lt) rt"
   2.897  
   2.898 -lemma unionwk_sorted: "sorted lt \<Longrightarrow> sorted (unionwithkey f lt rt)" 
   2.899 +lemma unionwk_sorted: "sorted lt \<Longrightarrow> sorted (union_with_key f lt rt)" 
   2.900    by (induct rt arbitrary: lt) (auto simp: insertwk_sorted)
   2.901 -theorem unionwk_is_rbt[simp]: "is_rbt lt \<Longrightarrow> is_rbt (unionwithkey f lt rt)" 
   2.902 +theorem unionwk_is_rbt[simp]: "is_rbt lt \<Longrightarrow> is_rbt (union_with_key f lt rt)" 
   2.903    by (induct rt arbitrary: lt) (simp add: insertwk_is_rbt)+
   2.904  
   2.905  definition
   2.906 -  unionwith where
   2.907 -  "unionwith f = unionwithkey (\<lambda>_. f)"
   2.908 +  union_with where
   2.909 +  "union_with f = union_with_key (\<lambda>_. f)"
   2.910  
   2.911 -theorem unionw_is_rbt: "is_rbt lt \<Longrightarrow> is_rbt (unionwith f lt rt)" unfolding unionwith_def by simp
   2.912 +theorem unionw_is_rbt: "is_rbt lt \<Longrightarrow> is_rbt (union_with f lt rt)" unfolding union_with_def by simp
   2.913  
   2.914  definition union where
   2.915 -  "union = unionwithkey (%_ _ rv. rv)"
   2.916 +  "union = union_with_key (%_ _ rv. rv)"
   2.917  
   2.918  theorem union_is_rbt: "is_rbt lt \<Longrightarrow> is_rbt (union lt rt)" unfolding union_def by simp
   2.919  
   2.920 @@ -811,7 +940,7 @@
   2.921    case Empty thus ?case by (auto simp: union_def)
   2.922  next
   2.923    case (Branch c l k v r s)
   2.924 -  hence sortedrl: "sorted r" "sorted l" "l |\<guillemotleft> k" "k \<guillemotleft>| r" by auto
   2.925 +  then have "sorted r" "sorted l" "l |\<guillemotleft> k" "k \<guillemotleft>| r" by auto
   2.926  
   2.927    have meq: "lookup s(k \<mapsto> v) ++ lookup l ++ lookup r =
   2.928      lookup s ++
   2.929 @@ -839,178 +968,79 @@
   2.930      qed
   2.931    qed
   2.932  
   2.933 -  from Branch
   2.934 -  have IHs:
   2.935 +  from Branch have is_rbt: "is_rbt (RBT.union (RBT.insert k v s) l)"
   2.936 +    by (auto intro: union_is_rbt insert_is_rbt)
   2.937 +  with Branch have IHs:
   2.938      "lookup (union (union (insert k v s) l) r) = lookup (union (insert k v s) l) ++ lookup r"
   2.939      "lookup (union (insert k v s) l) = lookup (insert k v s) ++ lookup l"
   2.940 -    by (auto intro: union_is_rbt insert_is_rbt)
   2.941 +    by auto
   2.942    
   2.943    with meq show ?case
   2.944      by (auto simp: lookup_insert[OF Branch(3)])
   2.945 +
   2.946  qed
   2.947  
   2.948 -subsection {* Adjust *}
   2.949 +
   2.950 +subsection {* Modifying existing entries *}
   2.951  
   2.952  primrec
   2.953 -  adjustwithkey :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
   2.954 +  map_entry :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
   2.955  where
   2.956 -  "adjustwithkey f k Empty = Empty"
   2.957 -| "adjustwithkey f k (Branch c lt x v rt) = (if k < x then (Branch c (adjustwithkey f k lt) x v rt) else if k > x then (Branch c lt x v (adjustwithkey f k rt)) else (Branch c lt x (f x v) rt))"
   2.958 +  "map_entry f k Empty = Empty"
   2.959 +| "map_entry f k (Branch c lt x v rt) = (if k < x then (Branch c (map_entry f k lt) x v rt) else if k > x then (Branch c lt x v (map_entry f k rt)) else (Branch c lt x (f x v) rt))"
   2.960  
   2.961 -lemma adjustwk_color_of: "color_of (adjustwithkey f k t) = color_of t" by (induct t) simp+
   2.962 -lemma adjustwk_inv1: "inv1 (adjustwithkey f k t) = inv1 t" by (induct t) (simp add: adjustwk_color_of)+
   2.963 -lemma adjustwk_inv2: "inv2 (adjustwithkey f k t) = inv2 t" "bheight (adjustwithkey f k t) = bheight t" by (induct t) simp+
   2.964 -lemma adjustwk_tree_greater: "tree_greater k (adjustwithkey f kk t) = tree_greater k t" by (induct t) simp+
   2.965 -lemma adjustwk_tree_less: "tree_less k (adjustwithkey f kk t) = tree_less k t" by (induct t) simp+
   2.966 -lemma adjustwk_sorted: "sorted (adjustwithkey f k t) = sorted t" by (induct t) (simp add: adjustwk_tree_less adjustwk_tree_greater)+
   2.967 +lemma map_entrywk_color_of: "color_of (map_entry f k t) = color_of t" by (induct t) simp+
   2.968 +lemma map_entrywk_inv1: "inv1 (map_entry f k t) = inv1 t" by (induct t) (simp add: map_entrywk_color_of)+
   2.969 +lemma map_entrywk_inv2: "inv2 (map_entry f k t) = inv2 t" "bheight (map_entry f k t) = bheight t" by (induct t) simp+
   2.970 +lemma map_entrywk_tree_greater: "tree_greater k (map_entry f kk t) = tree_greater k t" by (induct t) simp+
   2.971 +lemma map_entrywk_tree_less: "tree_less k (map_entry f kk t) = tree_less k t" by (induct t) simp+
   2.972 +lemma map_entrywk_sorted: "sorted (map_entry f k t) = sorted t" by (induct t) (simp add: map_entrywk_tree_less map_entrywk_tree_greater)+
   2.973  
   2.974 -theorem adjustwk_is_rbt[simp]: "is_rbt (adjustwithkey f k t) = is_rbt t" 
   2.975 -unfolding is_rbt_def by (simp add: adjustwk_inv2 adjustwk_color_of adjustwk_sorted adjustwk_inv1 )
   2.976 +theorem map_entrywk_is_rbt [simp]: "is_rbt (map_entry f k t) = is_rbt t" 
   2.977 +unfolding is_rbt_def by (simp add: map_entrywk_inv2 map_entrywk_color_of map_entrywk_sorted map_entrywk_inv1 )
   2.978  
   2.979 -theorem adjustwithkey_map[simp]:
   2.980 -  "lookup (adjustwithkey f k t) x = 
   2.981 +theorem map_entry_map [simp]:
   2.982 +  "lookup (map_entry f k t) x = 
   2.983    (if x = k then case lookup t x of None \<Rightarrow> None | Some y \<Rightarrow> Some (f k y)
   2.984              else lookup t x)"
   2.985  by (induct t arbitrary: x) (auto split:option.splits)
   2.986  
   2.987 -definition adjust where
   2.988 -  "adjust f = adjustwithkey (\<lambda>_. f)"
   2.989  
   2.990 -theorem adjust_is_rbt[simp]: "is_rbt (adjust f k t) = is_rbt t" unfolding adjust_def by simp
   2.991 -
   2.992 -theorem adjust_map[simp]:
   2.993 -  "lookup (adjust f k t) x = 
   2.994 -  (if x = k then case lookup t x of None \<Rightarrow> None | Some y \<Rightarrow> Some (f y)
   2.995 -            else lookup t x)"
   2.996 -unfolding adjust_def by simp
   2.997 -
   2.998 -subsection {* Map *}
   2.999 -
  2.1000 -primrec
  2.1001 -  mapwithkey :: "('a::linorder \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'c) rbt"
  2.1002 -where
  2.1003 -  "mapwithkey f Empty = Empty"
  2.1004 -| "mapwithkey f (Branch c lt k v rt) = Branch c (mapwithkey f lt) k (f k v) (mapwithkey f rt)"
  2.1005 -
  2.1006 -theorem mapwk_keys[simp]: "keys (mapwithkey f t) = keys t" by (induct t) auto
  2.1007 -lemma mapwk_tree_greater: "tree_greater k (mapwithkey f t) = tree_greater k t" by (induct t) simp+
  2.1008 -lemma mapwk_tree_less: "tree_less k (mapwithkey f t) = tree_less k t" by (induct t) simp+
  2.1009 -lemma mapwk_sorted: "sorted (mapwithkey f t) = sorted t"  by (induct t) (simp add: mapwk_tree_less mapwk_tree_greater)+
  2.1010 -lemma mapwk_color_of: "color_of (mapwithkey f t) = color_of t" by (induct t) simp+
  2.1011 -lemma mapwk_inv1: "inv1 (mapwithkey f t) = inv1 t" by (induct t) (simp add: mapwk_color_of)+
  2.1012 -lemma mapwk_inv2: "inv2 (mapwithkey f t) = inv2 t" "bheight (mapwithkey f t) = bheight t" by (induct t) simp+
  2.1013 -theorem mapwk_is_rbt[simp]: "is_rbt (mapwithkey f t) = is_rbt t" 
  2.1014 -unfolding is_rbt_def by (simp add: mapwk_inv1 mapwk_inv2 mapwk_sorted mapwk_color_of)
  2.1015 -
  2.1016 -theorem lookup_mapwk[simp]: "lookup (mapwithkey f t) x = Option.map (f x) (lookup t x)"
  2.1017 -by (induct t) auto
  2.1018 -
  2.1019 -definition map
  2.1020 -where map_def: "map f == mapwithkey (\<lambda>_. f)"
  2.1021 -
  2.1022 -theorem map_keys[simp]: "keys (map f t) = keys t" unfolding map_def by simp
  2.1023 -theorem map_is_rbt[simp]: "is_rbt (map f t) = is_rbt t" unfolding map_def by simp
  2.1024 -theorem lookup_map[simp]: "lookup (map f t) = Option.map f o lookup t"
  2.1025 -  by (rule ext) (simp add:map_def)
  2.1026 -
  2.1027 -subsection {* Fold *}
  2.1028 -
  2.1029 -text {* The following is still incomplete... *}
  2.1030 +subsection {* Mapping all entries *}
  2.1031  
  2.1032  primrec
  2.1033 -  foldwithkey :: "('a::linorder \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a,'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c"
  2.1034 +  map :: "('a::linorder \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'c) rbt"
  2.1035  where
  2.1036 -  "foldwithkey f Empty v = v"
  2.1037 -| "foldwithkey f (Branch c lt k x rt) v = foldwithkey f rt (f k x (foldwithkey f lt v))"
  2.1038 -
  2.1039 -lemma lookup_entries_aux: "sorted (Branch c t1 k v t2) \<Longrightarrow> RBT.lookup (Branch c t1 k v t2) = RBT.lookup t2 ++ [k\<mapsto>v] ++ RBT.lookup t1"
  2.1040 -proof (rule ext)
  2.1041 -  fix x
  2.1042 -  assume SORTED: "sorted (Branch c t1 k v t2)"
  2.1043 -  let ?thesis = "RBT.lookup (Branch c t1 k v t2) x = (RBT.lookup t2 ++ [k \<mapsto> v] ++ RBT.lookup t1) x"
  2.1044 -
  2.1045 -  have DOM_T1: "!!k'. k'\<in>dom (RBT.lookup t1) \<Longrightarrow> k>k'"
  2.1046 -  proof -
  2.1047 -    fix k'
  2.1048 -    from SORTED have "t1 |\<guillemotleft> k" by simp
  2.1049 -    with tree_less_prop have "\<forall>k'\<in>keys t1. k>k'" by auto
  2.1050 -    moreover assume "k'\<in>dom (RBT.lookup t1)"
  2.1051 -    ultimately show "k>k'" using RBT.lookup_keys SORTED by auto
  2.1052 -  qed
  2.1053 -
  2.1054 -  have DOM_T2: "!!k'. k'\<in>dom (RBT.lookup t2) \<Longrightarrow> k<k'"
  2.1055 -  proof -
  2.1056 -    fix k'
  2.1057 -    from SORTED have "k \<guillemotleft>| t2" by simp
  2.1058 -    with tree_greater_prop have "\<forall>k'\<in>keys t2. k<k'" by auto
  2.1059 -    moreover assume "k'\<in>dom (RBT.lookup t2)"
  2.1060 -    ultimately show "k<k'" using RBT.lookup_keys SORTED by auto
  2.1061 -  qed
  2.1062 +  "map f Empty = Empty"
  2.1063 +| "map f (Branch c lt k v rt) = Branch c (map f lt) k (f k v) (map f rt)"
  2.1064  
  2.1065 -  {
  2.1066 -    assume C: "x<k"
  2.1067 -    hence "RBT.lookup (Branch c t1 k v t2) x = RBT.lookup t1 x" by simp
  2.1068 -    moreover from C have "x\<notin>dom [k\<mapsto>v]" by simp
  2.1069 -    moreover have "x\<notin>dom (RBT.lookup t2)" proof
  2.1070 -      assume "x\<in>dom (RBT.lookup t2)"
  2.1071 -      with DOM_T2 have "k<x" by blast
  2.1072 -      with C show False by simp
  2.1073 -    qed
  2.1074 -    ultimately have ?thesis by (simp add: map_add_upd_left map_add_dom_app_simps)
  2.1075 -  } moreover {
  2.1076 -    assume [simp]: "x=k"
  2.1077 -    hence "RBT.lookup (Branch c t1 k v t2) x = [k \<mapsto> v] x" by simp
  2.1078 -    moreover have "x\<notin>dom (RBT.lookup t1)" proof
  2.1079 -      assume "x\<in>dom (RBT.lookup t1)"
  2.1080 -      with DOM_T1 have "k>x" by blast
  2.1081 -      thus False by simp
  2.1082 -    qed
  2.1083 -    ultimately have ?thesis by (simp add: map_add_upd_left map_add_dom_app_simps)
  2.1084 -  } moreover {
  2.1085 -    assume C: "x>k"
  2.1086 -    hence "RBT.lookup (Branch c t1 k v t2) x = RBT.lookup t2 x" by (simp add: less_not_sym[of k x])
  2.1087 -    moreover from C have "x\<notin>dom [k\<mapsto>v]" by simp
  2.1088 -    moreover have "x\<notin>dom (RBT.lookup t1)" proof
  2.1089 -      assume "x\<in>dom (RBT.lookup t1)"
  2.1090 -      with DOM_T1 have "k>x" by simp
  2.1091 -      with C show False by simp
  2.1092 -    qed
  2.1093 -    ultimately have ?thesis by (simp add: map_add_upd_left map_add_dom_app_simps)
  2.1094 -  } ultimately show ?thesis using less_linear by blast
  2.1095 -qed
  2.1096 +lemma map_entries [simp]: "entries (map f t) = List.map (\<lambda>(k, v). (k, f k v)) (entries t)"
  2.1097 +  by (induct t) auto
  2.1098 +lemma map_keys [simp]: "keys (map f t) = keys t" by (simp add: keys_def split_def)
  2.1099 +lemma map_tree_greater: "tree_greater k (map f t) = tree_greater k t" by (induct t) simp+
  2.1100 +lemma map_tree_less: "tree_less k (map f t) = tree_less k t" by (induct t) simp+
  2.1101 +lemma map_sorted: "sorted (map f t) = sorted t"  by (induct t) (simp add: map_tree_less map_tree_greater)+
  2.1102 +lemma map_color_of: "color_of (map f t) = color_of t" by (induct t) simp+
  2.1103 +lemma map_inv1: "inv1 (map f t) = inv1 t" by (induct t) (simp add: map_color_of)+
  2.1104 +lemma map_inv2: "inv2 (map f t) = inv2 t" "bheight (map f t) = bheight t" by (induct t) simp+
  2.1105 +theorem map_is_rbt [simp]: "is_rbt (map f t) = is_rbt t" 
  2.1106 +unfolding is_rbt_def by (simp add: map_inv1 map_inv2 map_sorted map_color_of)
  2.1107  
  2.1108 -lemma map_of_entries:
  2.1109 -  shows "sorted t \<Longrightarrow> map_of (entries t) = lookup t"
  2.1110 -proof (induct t)
  2.1111 -  case Empty thus ?case by (simp add: RBT.lookup_Empty)
  2.1112 -next
  2.1113 -  case (Branch c t1 k v t2)
  2.1114 -  hence "map_of (entries (Branch c t1 k v t2)) = RBT.lookup t2 ++ [k \<mapsto> v] ++ RBT.lookup t1" by simp
  2.1115 -  also note lookup_entries_aux [OF Branch.prems,symmetric]
  2.1116 -  finally show ?case .
  2.1117 -qed
  2.1118 -
  2.1119 -lemma fold_entries_fold:
  2.1120 -  "foldwithkey f t x = foldl (\<lambda>x (k,v). f k v x) x (entries t)"
  2.1121 -by (induct t arbitrary: x) auto
  2.1122 -
  2.1123 -lemma entries_pit[simp]: "(k, v) \<in> set (entries t) = entry_in_tree k v t"
  2.1124 +theorem lookup_map [simp]: "lookup (map f t) x = Option.map (f x) (lookup t x)"
  2.1125  by (induct t) auto
  2.1126  
  2.1127 -lemma sorted_entries:
  2.1128 -  "sorted t \<Longrightarrow> List.sorted (List.map fst (entries t))"
  2.1129 -by (induct t) 
  2.1130 -  (force simp: sorted_append sorted_Cons tree_ord_props 
  2.1131 -      dest!: entry_in_tree_keys)+
  2.1132 +
  2.1133 +subsection {* Folding over entries *}
  2.1134 +
  2.1135 +definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c" where
  2.1136 +  "fold f t s = foldl (\<lambda>s (k, v). f k v s) s (entries t)"
  2.1137  
  2.1138 -lemma distinct_entries:
  2.1139 -  "sorted t \<Longrightarrow> distinct (List.map fst (entries t))"
  2.1140 -by (induct t) 
  2.1141 -  (force simp: sorted_append sorted_Cons tree_ord_props 
  2.1142 -      dest!: entry_in_tree_keys)+
  2.1143 +lemma fold_simps [simp, code]:
  2.1144 +  "fold f Empty = id"
  2.1145 +  "fold f (Branch c lt k v rt) = fold f rt \<circ> f k v \<circ> fold f lt"
  2.1146 +  by (simp_all add: fold_def expand_fun_eq)
  2.1147  
  2.1148 -hide (open) const Empty insert delete entries lookup map fold union adjust sorted
  2.1149 -
  2.1150 +hide (open) const Empty insert delete entries lookup map_entry map fold union sorted
  2.1151  (*>*)
  2.1152  
  2.1153  text {* 
  2.1154 @@ -1018,6 +1048,7 @@
  2.1155    used as an efficient representation of finite maps.
  2.1156  *}
  2.1157  
  2.1158 +
  2.1159  subsection {* Data type and invariant *}
  2.1160  
  2.1161  text {*
  2.1162 @@ -1040,6 +1071,7 @@
  2.1163    $O(\log n)$.  
  2.1164  *}
  2.1165  
  2.1166 +
  2.1167  subsection {* Operations *}
  2.1168  
  2.1169  text {*
  2.1170 @@ -1081,6 +1113,7 @@
  2.1171    @{thm map_is_rbt}\hfill(@{text "map_is_rbt"})
  2.1172  *}
  2.1173  
  2.1174 +
  2.1175  subsection {* Map Semantics *}
  2.1176  
  2.1177  text {*
     3.1 --- a/src/HOL/Map.thy	Wed Mar 03 10:40:40 2010 -0800
     3.2 +++ b/src/HOL/Map.thy	Wed Mar 03 20:20:41 2010 -0800
     3.3 @@ -332,12 +332,12 @@
     3.4  by (fastsimp simp: map_add_def dom_def inj_on_def split: option.splits)
     3.5  
     3.6  lemma map_upds_fold_map_upd:
     3.7 -  "f(ks[\<mapsto>]vs) = foldl (\<lambda>f (k, v). f(k\<mapsto>v)) f (zip ks vs)"
     3.8 +  "m(ks[\<mapsto>]vs) = foldl (\<lambda>m (k, v). m(k \<mapsto> v)) m (zip ks vs)"
     3.9  unfolding map_upds_def proof (rule sym, rule zip_obtain_same_length)
    3.10    fix ks :: "'a list" and vs :: "'b list"
    3.11    assume "length ks = length vs"
    3.12 -  then show "foldl (\<lambda>f (k, v). f(k\<mapsto>v)) f (zip ks vs) = f ++ map_of (rev (zip ks vs))"
    3.13 -    by (induct arbitrary: f rule: list_induct2) simp_all
    3.14 +  then show "foldl (\<lambda>m (k, v). m(k\<mapsto>v)) m (zip ks vs) = m ++ map_of (rev (zip ks vs))"
    3.15 +    by(induct arbitrary: m rule: list_induct2) simp_all
    3.16  qed
    3.17  
    3.18  lemma map_add_map_of_foldr:
     4.1 --- a/src/HOL/Nat_Transfer.thy	Wed Mar 03 10:40:40 2010 -0800
     4.2 +++ b/src/HOL/Nat_Transfer.thy	Wed Mar 03 20:20:41 2010 -0800
     4.3 @@ -25,7 +25,7 @@
     4.4  lemma TransferMorphism_nat_int: "TransferMorphism nat (op <= (0::int))"
     4.5    by (simp add: TransferMorphism_def)
     4.6  
     4.7 -declare TransferMorphism_nat_int[transfer
     4.8 +declare TransferMorphism_nat_int [transfer
     4.9    add mode: manual
    4.10    return: nat_0_le
    4.11    labels: natint
    4.12 @@ -80,7 +80,7 @@
    4.13        (nat (x::int) dvd nat y) = (x dvd y)"
    4.14    by (auto simp add: zdvd_int)
    4.15  
    4.16 -declare TransferMorphism_nat_int[transfer add return:
    4.17 +declare TransferMorphism_nat_int [transfer add return:
    4.18    transfer_nat_int_numerals
    4.19    transfer_nat_int_functions
    4.20    transfer_nat_int_function_closures
    4.21 @@ -118,7 +118,7 @@
    4.22      (EX x. Q x \<and> P x) = (EX x. Q x \<and> P' x)"
    4.23    by auto
    4.24  
    4.25 -declare TransferMorphism_nat_int[transfer add
    4.26 +declare TransferMorphism_nat_int [transfer add
    4.27    return: transfer_nat_int_quantifiers
    4.28    cong: all_cong ex_cong]
    4.29  
    4.30 @@ -190,7 +190,7 @@
    4.31      {(x::int). x >= 0 & P x} = {x. x >= 0 & P' x}"
    4.32    by auto
    4.33  
    4.34 -declare TransferMorphism_nat_int[transfer add
    4.35 +declare TransferMorphism_nat_int [transfer add
    4.36    return: transfer_nat_int_set_functions
    4.37      transfer_nat_int_set_function_closures
    4.38      transfer_nat_int_set_relations
    4.39 @@ -262,7 +262,7 @@
    4.40    apply (subst setprod_cong, assumption, auto)
    4.41  done
    4.42  
    4.43 -declare TransferMorphism_nat_int[transfer add
    4.44 +declare TransferMorphism_nat_int [transfer add
    4.45    return: transfer_nat_int_sum_prod transfer_nat_int_sum_prod2
    4.46      transfer_nat_int_sum_prod_closure
    4.47    cong: transfer_nat_int_sum_prod_cong]
    4.48 @@ -275,7 +275,7 @@
    4.49  lemma TransferMorphism_int_nat: "TransferMorphism int (UNIV :: nat set)"
    4.50    by (simp add: TransferMorphism_def)
    4.51  
    4.52 -declare TransferMorphism_int_nat[transfer add
    4.53 +declare TransferMorphism_int_nat [transfer add
    4.54    mode: manual
    4.55  (*  labels: int-nat *)
    4.56    return: nat_int
    4.57 @@ -326,7 +326,7 @@
    4.58      "(int x dvd int y) = (x dvd y)"
    4.59    by (auto simp add: zdvd_int)
    4.60  
    4.61 -declare TransferMorphism_int_nat[transfer add return:
    4.62 +declare TransferMorphism_int_nat [transfer add return:
    4.63    transfer_int_nat_numerals
    4.64    transfer_int_nat_functions
    4.65    transfer_int_nat_function_closures
    4.66 @@ -346,7 +346,7 @@
    4.67    apply auto
    4.68  done
    4.69  
    4.70 -declare TransferMorphism_int_nat[transfer add
    4.71 +declare TransferMorphism_int_nat [transfer add
    4.72    return: transfer_int_nat_quantifiers]
    4.73  
    4.74  
    4.75 @@ -401,7 +401,7 @@
    4.76      {(x::nat). P x} = {x. P' x}"
    4.77    by auto
    4.78  
    4.79 -declare TransferMorphism_int_nat[transfer add
    4.80 +declare TransferMorphism_int_nat [transfer add
    4.81    return: transfer_int_nat_set_functions
    4.82      transfer_int_nat_set_function_closures
    4.83      transfer_int_nat_set_relations
    4.84 @@ -433,7 +433,7 @@
    4.85    apply (subst int_setprod, auto simp add: cong: setprod_cong)
    4.86  done
    4.87  
    4.88 -declare TransferMorphism_int_nat[transfer add
    4.89 +declare TransferMorphism_int_nat [transfer add
    4.90    return: transfer_int_nat_sum_prod transfer_int_nat_sum_prod2
    4.91    cong: setsum_cong setprod_cong]
    4.92  
     5.1 --- a/src/Pure/consts.ML	Wed Mar 03 10:40:40 2010 -0800
     5.2 +++ b/src/Pure/consts.ML	Wed Mar 03 20:20:41 2010 -0800
     5.3 @@ -21,8 +21,9 @@
     5.4    val space_of: T -> Name_Space.T
     5.5    val is_concealed: T -> string -> bool
     5.6    val intern: T -> xstring -> string
     5.7 +  val extern: T -> string -> xstring
     5.8    val intern_syntax: T -> xstring -> string
     5.9 -  val extern: T -> string -> xstring
    5.10 +  val extern_syntax: T -> string -> xstring
    5.11    val read_const: T -> string -> term
    5.12    val certify: Pretty.pp -> Type.tsig -> bool -> T -> term -> term  (*exception TYPE*)
    5.13    val typargs: T -> string * typ -> typ list
    5.14 @@ -126,10 +127,15 @@
    5.15  val intern = Name_Space.intern o space_of;
    5.16  val extern = Name_Space.extern o space_of;
    5.17  
    5.18 -fun intern_syntax consts name =
    5.19 -  (case try Syntax.unmark_const name of
    5.20 +fun intern_syntax consts s =
    5.21 +  (case try Syntax.unmark_const s of
    5.22      SOME c => c
    5.23 -  | NONE => intern consts name);
    5.24 +  | NONE => intern consts s);
    5.25 +
    5.26 +fun extern_syntax consts s =
    5.27 +  (case try Syntax.unmark_const s of
    5.28 +    SOME c => extern consts c
    5.29 +  | NONE => s);
    5.30  
    5.31  
    5.32  (* read_const *)