efficient construction of red black trees from sorted associative lists
authorAndreas Lochbihler
Wed Oct 10 13:03:50 2012 +0200 (2012-10-10)
changeset 49770cf6a78acf445
parent 49759 ecf1d5d87e5e
child 49771 b1493798d253
efficient construction of red black trees from sorted associative lists
CONTRIBUTORS
NEWS
src/HOL/Library/RBT_Impl.thy
     1.1 --- a/CONTRIBUTORS	Tue Oct 09 17:33:46 2012 +0200
     1.2 +++ b/CONTRIBUTORS	Wed Oct 10 13:03:50 2012 +0200
     1.3 @@ -9,6 +9,9 @@
     1.4  * 2012: Makarius Wenzel, Université Paris-Sud / LRI
     1.5    Improvements of Isabelle/Scala and Isabelle/jEdit Prover IDE.
     1.6  
     1.7 +* October 2012: Andreas Lochbihler, KIT
     1.8 +  Efficient construction of red black trees from sorted associative lists.
     1.9 +
    1.10  * September 2012: Florian Haftmann, TUM
    1.11    Lattice instances for type option.
    1.12  
     2.1 --- a/NEWS	Tue Oct 09 17:33:46 2012 +0200
     2.2 +++ b/NEWS	Wed Oct 10 13:03:50 2012 +0200
     2.3 @@ -134,6 +134,10 @@
     2.4  appear in a constant's type. This alternative to adding TYPE('a) as
     2.5  another parameter avoids unnecessary closures in generated code.
     2.6  
     2.7 +* Library/RBT_Impl.thy: efficient construction of red-black trees 
     2.8 +from sorted associative lists. Merging two trees with rbt_union may
     2.9 +return a structurally different tree than before. MINOR INCOMPATIBILITY.
    2.10 +
    2.11  * Simproc "finite_Collect" rewrites set comprehensions into pointfree
    2.12  expressions.
    2.13  
     3.1 --- a/src/HOL/Library/RBT_Impl.thy	Tue Oct 09 17:33:46 2012 +0200
     3.2 +++ b/src/HOL/Library/RBT_Impl.thy	Wed Oct 10 13:03:50 2012 +0200
     3.3 @@ -113,13 +113,13 @@
     3.4  context linorder begin
     3.5  
     3.6  lemma rbt_sorted_entries:
     3.7 -  "rbt_sorted t \<Longrightarrow> List.sorted (List.map fst (entries t))"
     3.8 +  "rbt_sorted t \<Longrightarrow> List.sorted (map fst (entries t))"
     3.9  by (induct t) 
    3.10    (force simp: sorted_append sorted_Cons rbt_ord_props 
    3.11        dest!: entry_in_tree_keys)+
    3.12  
    3.13  lemma distinct_entries:
    3.14 -  "rbt_sorted t \<Longrightarrow> distinct (List.map fst (entries t))"
    3.15 +  "rbt_sorted t \<Longrightarrow> distinct (map fst (entries t))"
    3.16  by (induct t) 
    3.17    (force simp: sorted_append sorted_Cons rbt_ord_props 
    3.18        dest!: entry_in_tree_keys)+
    3.19 @@ -998,89 +998,6 @@
    3.20  
    3.21  end
    3.22  
    3.23 -subsection {* Union *}
    3.24 -
    3.25 -context ord begin
    3.26 -
    3.27 -primrec rbt_union_with_key :: "('a \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
    3.28 -where
    3.29 -  "rbt_union_with_key f t Empty = t"
    3.30 -| "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"
    3.31 -
    3.32 -definition rbt_union_with where
    3.33 -  "rbt_union_with f = rbt_union_with_key (\<lambda>_. f)"
    3.34 -
    3.35 -definition rbt_union where
    3.36 -  "rbt_union = rbt_union_with_key (%_ _ rv. rv)"
    3.37 -
    3.38 -end
    3.39 -
    3.40 -context linorder begin
    3.41 -
    3.42 -lemma rbt_unionwk_rbt_sorted: "rbt_sorted lt \<Longrightarrow> rbt_sorted (rbt_union_with_key f lt rt)" 
    3.43 -  by (induct rt arbitrary: lt) (auto simp: rbt_insertwk_rbt_sorted)
    3.44 -theorem rbt_unionwk_is_rbt[simp]: "is_rbt lt \<Longrightarrow> is_rbt (rbt_union_with_key f lt rt)" 
    3.45 -  by (induct rt arbitrary: lt) (simp add: rbt_insertwk_is_rbt)+
    3.46 -
    3.47 -theorem rbt_unionw_is_rbt: "is_rbt lt \<Longrightarrow> is_rbt (rbt_union_with f lt rt)" unfolding rbt_union_with_def by simp
    3.48 -
    3.49 -theorem rbt_union_is_rbt: "is_rbt lt \<Longrightarrow> is_rbt (rbt_union lt rt)" unfolding rbt_union_def by simp
    3.50 -
    3.51 -lemma (in ord) rbt_union_Branch[simp]:
    3.52 -  "rbt_union t (Branch c lt k v rt) = rbt_union (rbt_union (rbt_insert k v t) lt) rt"
    3.53 -  unfolding rbt_union_def rbt_insert_def
    3.54 -  by simp
    3.55 -
    3.56 -lemma rbt_lookup_rbt_union:
    3.57 -  assumes "is_rbt s" "rbt_sorted t"
    3.58 -  shows "rbt_lookup (rbt_union s t) = rbt_lookup s ++ rbt_lookup t"
    3.59 -using assms
    3.60 -proof (induct t arbitrary: s)
    3.61 -  case Empty thus ?case by (auto simp: rbt_union_def)
    3.62 -next
    3.63 -  case (Branch c l k v r s)
    3.64 -  then have "rbt_sorted r" "rbt_sorted l" "l |\<guillemotleft> k" "k \<guillemotleft>| r" by auto
    3.65 -
    3.66 -  have meq: "rbt_lookup s(k \<mapsto> v) ++ rbt_lookup l ++ rbt_lookup r =
    3.67 -    rbt_lookup s ++
    3.68 -    (\<lambda>a. if a < k then rbt_lookup l a
    3.69 -    else if k < a then rbt_lookup r a else Some v)" (is "?m1 = ?m2")
    3.70 -  proof (rule ext)
    3.71 -    fix a
    3.72 -
    3.73 -   have "k < a \<or> k = a \<or> k > a" by auto
    3.74 -    thus "?m1 a = ?m2 a"
    3.75 -    proof (elim disjE)
    3.76 -      assume "k < a"
    3.77 -      with `l |\<guillemotleft> k` have "l |\<guillemotleft> a" by (rule rbt_less_trans)
    3.78 -      with `k < a` show ?thesis
    3.79 -        by (auto simp: map_add_def split: option.splits)
    3.80 -    next
    3.81 -      assume "k = a"
    3.82 -      with `l |\<guillemotleft> k` `k \<guillemotleft>| r` 
    3.83 -      show ?thesis by (auto simp: map_add_def)
    3.84 -    next
    3.85 -      assume "a < k"
    3.86 -      from this `k \<guillemotleft>| r` have "a \<guillemotleft>| r" by (rule rbt_greater_trans)
    3.87 -      with `a < k` show ?thesis
    3.88 -        by (auto simp: map_add_def split: option.splits)
    3.89 -    qed
    3.90 -  qed
    3.91 -
    3.92 -  from Branch have is_rbt: "is_rbt (rbt_union (rbt_insert k v s) l)"
    3.93 -    by (auto intro: rbt_union_is_rbt rbt_insert_is_rbt)
    3.94 -  with Branch have IHs:
    3.95 -    "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"
    3.96 -    "rbt_lookup (rbt_union (rbt_insert k v s) l) = rbt_lookup (rbt_insert k v s) ++ rbt_lookup l"
    3.97 -    by auto
    3.98 -  
    3.99 -  with meq show ?case
   3.100 -    by (auto simp: rbt_lookup_rbt_insert[OF Branch(3)])
   3.101 -
   3.102 -qed
   3.103 -
   3.104 -end
   3.105 -
   3.106  subsection {* Modifying existing entries *}
   3.107  
   3.108  context ord begin
   3.109 @@ -1146,16 +1063,23 @@
   3.110   (* FIXME: simproc "antisym less" does not work for linorder context, only for linorder type class
   3.111      by (induct t) auto *)
   3.112  
   3.113 +hide_const (open) map
   3.114 +
   3.115  subsection {* Folding over entries *}
   3.116  
   3.117  definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c" where
   3.118    "fold f t = List.fold (prod_case f) (entries t)"
   3.119  
   3.120 -lemma fold_simps [simp, code]:
   3.121 +lemma fold_simps [simp]:
   3.122    "fold f Empty = id"
   3.123    "fold f (Branch c lt k v rt) = fold f rt \<circ> f k v \<circ> fold f lt"
   3.124    by (simp_all add: fold_def fun_eq_iff)
   3.125  
   3.126 +lemma fold_code [code]:
   3.127 +  "fold f Empty c = c"
   3.128 +  "fold f (Branch c lt k v rt) c = fold f rt (f k v (fold f lt c))"
   3.129 +by(simp_all)
   3.130 +
   3.131  (* fold with continuation predicate *)
   3.132  
   3.133  fun foldi :: "('c \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a :: linorder, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c" 
   3.134 @@ -1197,6 +1121,884 @@
   3.135  
   3.136  end
   3.137  
   3.138 +
   3.139 +
   3.140 +subsection {* Building a RBT from a sorted list *}
   3.141 +
   3.142 +text {* 
   3.143 +  These functions have been adapted from 
   3.144 +  Andrew W. Appel, Efficient Verified Red-Black Trees (September 2011) 
   3.145 +*}
   3.146 +
   3.147 +fun rbtreeify_f :: "nat \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('a, 'b) rbt \<times> ('a \<times> 'b) list"
   3.148 +  and rbtreeify_g :: "nat \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('a, 'b) rbt \<times> ('a \<times> 'b) list"
   3.149 +where
   3.150 +  "rbtreeify_f n kvs =
   3.151 +   (if n = 0 then (Empty, kvs)
   3.152 +    else if n = 1 then
   3.153 +      case kvs of (k, v) # kvs' \<Rightarrow> (Branch R Empty k v Empty, kvs')
   3.154 +    else if (n mod 2 = 0) then
   3.155 +      case rbtreeify_f (n div 2) kvs of (t1, (k, v) # kvs') \<Rightarrow>
   3.156 +        apfst (Branch B t1 k v) (rbtreeify_g (n div 2) kvs')
   3.157 +    else case rbtreeify_f (n div 2) kvs of (t1, (k, v) # kvs') \<Rightarrow>
   3.158 +        apfst (Branch B t1 k v) (rbtreeify_f (n div 2) kvs'))"
   3.159 +
   3.160 +| "rbtreeify_g n kvs =
   3.161 +   (if n = 0 \<or> n = 1 then (Empty, kvs)
   3.162 +    else if n mod 2 = 0 then
   3.163 +      case rbtreeify_g (n div 2) kvs of (t1, (k, v) # kvs') \<Rightarrow>
   3.164 +        apfst (Branch B t1 k v) (rbtreeify_g (n div 2) kvs')
   3.165 +    else case rbtreeify_f (n div 2) kvs of (t1, (k, v) # kvs') \<Rightarrow>
   3.166 +        apfst (Branch B t1 k v) (rbtreeify_g (n div 2) kvs'))"
   3.167 +
   3.168 +definition rbtreeify :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) rbt"
   3.169 +where "rbtreeify kvs = fst (rbtreeify_g (Suc (length kvs)) kvs)"
   3.170 +
   3.171 +declare rbtreeify_f.simps [simp del] rbtreeify_g.simps [simp del]
   3.172 +
   3.173 +lemma rbtreeify_f_code [code]:
   3.174 +  "rbtreeify_f n kvs =
   3.175 +   (if n = 0 then (Empty, kvs)
   3.176 +    else if n = 1 then
   3.177 +      case kvs of (k, v) # kvs' \<Rightarrow> 
   3.178 +        (Branch R Empty k v Empty, kvs')
   3.179 +    else let (n', r) = divmod_nat n 2 in
   3.180 +      if r = 0 then
   3.181 +        case rbtreeify_f n' kvs of (t1, (k, v) # kvs') \<Rightarrow>
   3.182 +          apfst (Branch B t1 k v) (rbtreeify_g n' kvs')
   3.183 +      else case rbtreeify_f n' kvs of (t1, (k, v) # kvs') \<Rightarrow>
   3.184 +          apfst (Branch B t1 k v) (rbtreeify_f n' kvs'))"
   3.185 +by(subst rbtreeify_f.simps)(simp only: Let_def divmod_nat_div_mod prod.simps)
   3.186 +
   3.187 +lemma rbtreeify_g_code [code]:
   3.188 +  "rbtreeify_g n kvs =
   3.189 +   (if n = 0 \<or> n = 1 then (Empty, kvs)
   3.190 +    else let (n', r) = divmod_nat n 2 in
   3.191 +      if r = 0 then
   3.192 +        case rbtreeify_g n' kvs of (t1, (k, v) # kvs') \<Rightarrow>
   3.193 +          apfst (Branch B t1 k v) (rbtreeify_g n' kvs')
   3.194 +      else case rbtreeify_f n' kvs of (t1, (k, v) # kvs') \<Rightarrow>
   3.195 +          apfst (Branch B t1 k v) (rbtreeify_g n' kvs'))"
   3.196 +by(subst rbtreeify_g.simps)(simp only: Let_def divmod_nat_div_mod prod.simps)
   3.197 +
   3.198 +lemma Suc_double_half: "Suc (2 * n) div 2 = n"
   3.199 +by simp
   3.200 +
   3.201 +lemma div2_plus_div2: "n div 2 + n div 2 = (n :: nat) - n mod 2"
   3.202 +by arith
   3.203 +
   3.204 +lemma rbtreeify_f_rec_aux_lemma:
   3.205 +  "\<lbrakk>k - n div 2 = Suc k'; n \<le> k; n mod 2 = Suc 0\<rbrakk>
   3.206 +  \<Longrightarrow> k' - n div 2 = k - n"
   3.207 +apply(rule add_right_imp_eq[where a = "n - n div 2"])
   3.208 +apply(subst add_diff_assoc2, arith)
   3.209 +apply(simp add: div2_plus_div2)
   3.210 +done
   3.211 +
   3.212 +lemma rbtreeify_f_simps:
   3.213 +  "rbtreeify_f 0 kvs = (RBT_Impl.Empty, kvs)"
   3.214 +  "rbtreeify_f (Suc 0) ((k, v) # kvs) = 
   3.215 +  (Branch R Empty k v Empty, kvs)"
   3.216 +  "0 < n \<Longrightarrow> rbtreeify_f (2 * n) kvs =
   3.217 +   (case rbtreeify_f n kvs of (t1, (k, v) # kvs') \<Rightarrow>
   3.218 +     apfst (Branch B t1 k v) (rbtreeify_g n kvs'))"
   3.219 +  "0 < n \<Longrightarrow> rbtreeify_f (Suc (2 * n)) kvs =
   3.220 +   (case rbtreeify_f n kvs of (t1, (k, v) # kvs') \<Rightarrow> 
   3.221 +     apfst (Branch B t1 k v) (rbtreeify_f n kvs'))"
   3.222 +by(subst (1) rbtreeify_f.simps, simp add: Suc_double_half)+
   3.223 +
   3.224 +lemma rbtreeify_g_simps:
   3.225 +  "rbtreeify_g 0 kvs = (Empty, kvs)"
   3.226 +  "rbtreeify_g (Suc 0) kvs = (Empty, kvs)"
   3.227 +  "0 < n \<Longrightarrow> rbtreeify_g (2 * n) kvs =
   3.228 +   (case rbtreeify_g n kvs of (t1, (k, v) # kvs') \<Rightarrow> 
   3.229 +     apfst (Branch B t1 k v) (rbtreeify_g n kvs'))"
   3.230 +  "0 < n \<Longrightarrow> rbtreeify_g (Suc (2 * n)) kvs =
   3.231 +   (case rbtreeify_f n kvs of (t1, (k, v) # kvs') \<Rightarrow> 
   3.232 +     apfst (Branch B t1 k v) (rbtreeify_g n kvs'))"
   3.233 +by(subst (1) rbtreeify_g.simps, simp add: Suc_double_half)+
   3.234 +
   3.235 +declare rbtreeify_f_simps[simp] rbtreeify_g_simps[simp]
   3.236 +
   3.237 +lemma length_rbtreeify_f: "n \<le> length kvs
   3.238 +  \<Longrightarrow> length (snd (rbtreeify_f n kvs)) = length kvs - n"
   3.239 +  and length_rbtreeify_g:"\<lbrakk> 0 < n; n \<le> Suc (length kvs) \<rbrakk>
   3.240 +  \<Longrightarrow> length (snd (rbtreeify_g n kvs)) = Suc (length kvs) - n"
   3.241 +proof(induction n kvs and n kvs rule: rbtreeify_f_rbtreeify_g.induct)
   3.242 +  case (1 n kvs)
   3.243 +  show ?case
   3.244 +  proof(cases "n \<le> 1")
   3.245 +    case True thus ?thesis using "1.prems"
   3.246 +      by(cases n kvs rule: nat.exhaust[case_product list.exhaust]) auto
   3.247 +  next
   3.248 +    case False
   3.249 +    hence "n \<noteq> 0" "n \<noteq> 1" by simp_all
   3.250 +    note IH = "1.IH"[OF this]
   3.251 +    show ?thesis
   3.252 +    proof(cases "n mod 2 = 0")
   3.253 +      case True
   3.254 +      hence "length (snd (rbtreeify_f n kvs)) = 
   3.255 +        length (snd (rbtreeify_f (2 * (n div 2)) kvs))"
   3.256 +        by(metis minus_nat.diff_0 mult_div_cancel)
   3.257 +      also from "1.prems" False obtain k v kvs' 
   3.258 +        where kvs: "kvs = (k, v) # kvs'" by(cases kvs) auto
   3.259 +      also have "0 < n div 2" using False by(simp) 
   3.260 +      note rbtreeify_f_simps(3)[OF this]
   3.261 +      also note kvs[symmetric] 
   3.262 +      also let ?rest1 = "snd (rbtreeify_f (n div 2) kvs)"
   3.263 +      from "1.prems" have "n div 2 \<le> length kvs" by simp
   3.264 +      with True have len: "length ?rest1 = length kvs - n div 2" by(rule IH)
   3.265 +      with "1.prems" False obtain t1 k' v' kvs''
   3.266 +        where kvs'': "rbtreeify_f (n div 2) kvs = (t1, (k', v') # kvs'')"
   3.267 +         by(cases ?rest1)(auto simp add: snd_def split: prod.split_asm)
   3.268 +      note this also note prod.simps(2) also note list.simps(5) 
   3.269 +      also note prod.simps(2) also note snd_apfst
   3.270 +      also have "0 < n div 2" "n div 2 \<le> Suc (length kvs'')" 
   3.271 +        using len "1.prems" False unfolding kvs'' by simp_all
   3.272 +      with True kvs''[symmetric] refl refl
   3.273 +      have "length (snd (rbtreeify_g (n div 2) kvs'')) = 
   3.274 +        Suc (length kvs'') - n div 2" by(rule IH)
   3.275 +      finally show ?thesis using len[unfolded kvs''] "1.prems" True
   3.276 +        by(simp add: Suc_diff_le[symmetric] mult_2[symmetric] mult_div_cancel)
   3.277 +    next
   3.278 +      case False
   3.279 +      hence "length (snd (rbtreeify_f n kvs)) = 
   3.280 +        length (snd (rbtreeify_f (Suc (2 * (n div 2))) kvs))"
   3.281 +        by(metis Suc_eq_plus1_left comm_semiring_1_class.normalizing_semiring_rules(7)
   3.282 +             mod_2_not_eq_zero_eq_one_nat semiring_div_class.mod_div_equality')
   3.283 +      also from "1.prems" `\<not> n \<le> 1` obtain k v kvs' 
   3.284 +        where kvs: "kvs = (k, v) # kvs'" by(cases kvs) auto
   3.285 +      also have "0 < n div 2" using `\<not> n \<le> 1` by(simp) 
   3.286 +      note rbtreeify_f_simps(4)[OF this]
   3.287 +      also note kvs[symmetric] 
   3.288 +      also let ?rest1 = "snd (rbtreeify_f (n div 2) kvs)"
   3.289 +      from "1.prems" have "n div 2 \<le> length kvs" by simp
   3.290 +      with False have len: "length ?rest1 = length kvs - n div 2" by(rule IH)
   3.291 +      with "1.prems" `\<not> n \<le> 1` obtain t1 k' v' kvs''
   3.292 +        where kvs'': "rbtreeify_f (n div 2) kvs = (t1, (k', v') # kvs'')"
   3.293 +        by(cases ?rest1)(auto simp add: snd_def split: prod.split_asm)
   3.294 +      note this also note prod.simps(2) also note list.simps(5) 
   3.295 +      also note prod.simps(2) also note snd_apfst
   3.296 +      also have "n div 2 \<le> length kvs''" 
   3.297 +        using len "1.prems" False unfolding kvs'' by simp arith
   3.298 +      with False kvs''[symmetric] refl refl
   3.299 +      have "length (snd (rbtreeify_f (n div 2) kvs'')) = length kvs'' - n div 2"
   3.300 +        by(rule IH)
   3.301 +      finally show ?thesis using len[unfolded kvs''] "1.prems" False
   3.302 +        by simp(rule rbtreeify_f_rec_aux_lemma[OF sym])
   3.303 +    qed
   3.304 +  qed
   3.305 +next
   3.306 +  case (2 n kvs)
   3.307 +  show ?case
   3.308 +  proof(cases "n > 1")
   3.309 +    case False with `0 < n` show ?thesis
   3.310 +      by(cases n kvs rule: nat.exhaust[case_product list.exhaust]) simp_all
   3.311 +  next
   3.312 +    case True
   3.313 +    hence "\<not> (n = 0 \<or> n = 1)" by simp
   3.314 +    note IH = "2.IH"[OF this]
   3.315 +    show ?thesis
   3.316 +    proof(cases "n mod 2 = 0")
   3.317 +      case True
   3.318 +      hence "length (snd (rbtreeify_g n kvs)) =
   3.319 +        length (snd (rbtreeify_g (2 * (n div 2)) kvs))"
   3.320 +        by(metis minus_nat.diff_0 mult_div_cancel)
   3.321 +      also from "2.prems" True obtain k v kvs' 
   3.322 +        where kvs: "kvs = (k, v) # kvs'" by(cases kvs) auto
   3.323 +      also have "0 < n div 2" using `1 < n` by(simp) 
   3.324 +      note rbtreeify_g_simps(3)[OF this]
   3.325 +      also note kvs[symmetric] 
   3.326 +      also let ?rest1 = "snd (rbtreeify_g (n div 2) kvs)"
   3.327 +      from "2.prems" `1 < n`
   3.328 +      have "0 < n div 2" "n div 2 \<le> Suc (length kvs)" by simp_all
   3.329 +      with True have len: "length ?rest1 = Suc (length kvs) - n div 2" by(rule IH)
   3.330 +      with "2.prems" obtain t1 k' v' kvs''
   3.331 +        where kvs'': "rbtreeify_g (n div 2) kvs = (t1, (k', v') # kvs'')"
   3.332 +        by(cases ?rest1)(auto simp add: snd_def split: prod.split_asm)
   3.333 +      note this also note prod.simps(2) also note list.simps(5) 
   3.334 +      also note prod.simps(2) also note snd_apfst
   3.335 +      also have "n div 2 \<le> Suc (length kvs'')" 
   3.336 +        using len "2.prems" unfolding kvs'' by simp
   3.337 +      with True kvs''[symmetric] refl refl `0 < n div 2`
   3.338 +      have "length (snd (rbtreeify_g (n div 2) kvs'')) = Suc (length kvs'') - n div 2"
   3.339 +        by(rule IH)
   3.340 +      finally show ?thesis using len[unfolded kvs''] "2.prems" True
   3.341 +        by(simp add: Suc_diff_le[symmetric] mult_2[symmetric] mult_div_cancel)
   3.342 +    next
   3.343 +      case False
   3.344 +      hence "length (snd (rbtreeify_g n kvs)) = 
   3.345 +        length (snd (rbtreeify_g (Suc (2 * (n div 2))) kvs))"
   3.346 +        by(metis Suc_eq_plus1_left comm_semiring_1_class.normalizing_semiring_rules(7) 
   3.347 +            mod_2_not_eq_zero_eq_one_nat semiring_div_class.mod_div_equality')
   3.348 +      also from "2.prems" `1 < n` obtain k v kvs'
   3.349 +        where kvs: "kvs = (k, v) # kvs'" by(cases kvs) auto
   3.350 +      also have "0 < n div 2" using `1 < n` by(simp)
   3.351 +      note rbtreeify_g_simps(4)[OF this]
   3.352 +      also note kvs[symmetric] 
   3.353 +      also let ?rest1 = "snd (rbtreeify_f (n div 2) kvs)"
   3.354 +      from "2.prems" have "n div 2 \<le> length kvs" by simp
   3.355 +      with False have len: "length ?rest1 = length kvs - n div 2" by(rule IH)
   3.356 +      with "2.prems" `1 < n` False obtain t1 k' v' kvs'' 
   3.357 +        where kvs'': "rbtreeify_f (n div 2) kvs = (t1, (k', v') # kvs'')"
   3.358 +        by(cases ?rest1)(auto simp add: snd_def split: prod.split_asm, arith)
   3.359 +      note this also note prod.simps(2) also note list.simps(5) 
   3.360 +      also note prod.simps(2) also note snd_apfst
   3.361 +      also have "n div 2 \<le> Suc (length kvs'')" 
   3.362 +        using len "2.prems" False unfolding kvs'' by simp arith
   3.363 +      with False kvs''[symmetric] refl refl `0 < n div 2`
   3.364 +      have "length (snd (rbtreeify_g (n div 2) kvs'')) = Suc (length kvs'') - n div 2"
   3.365 +        by(rule IH)
   3.366 +      finally show ?thesis using len[unfolded kvs''] "2.prems" False
   3.367 +        by(simp add: div2_plus_div2)
   3.368 +    qed
   3.369 +  qed
   3.370 +qed
   3.371 +
   3.372 +lemma rbtreeify_induct [consumes 1, case_names f_0 f_1 f_even f_odd g_0 g_1 g_even g_odd]:
   3.373 +  fixes P Q
   3.374 +  defines "f0 == (\<And>kvs. P 0 kvs)"
   3.375 +  and "f1 == (\<And>k v kvs. P (Suc 0) ((k, v) # kvs))"
   3.376 +  and "feven ==
   3.377 +    (\<And>n kvs t k v kvs'. \<lbrakk> n > 0; n \<le> length kvs; P n kvs; 
   3.378 +       rbtreeify_f n kvs = (t, (k, v) # kvs'); n \<le> Suc (length kvs'); Q n kvs' \<rbrakk> 
   3.379 +     \<Longrightarrow> P (2 * n) kvs)"
   3.380 +  and "fodd == 
   3.381 +    (\<And>n kvs t k v kvs'. \<lbrakk> n > 0; n \<le> length kvs; P n kvs;
   3.382 +       rbtreeify_f n kvs = (t, (k, v) # kvs'); n \<le> length kvs'; P n kvs' \<rbrakk> 
   3.383 +    \<Longrightarrow> P (Suc (2 * n)) kvs)"
   3.384 +  and "g0 == (\<And>kvs. Q 0 kvs)"
   3.385 +  and "g1 == (\<And>kvs. Q (Suc 0) kvs)"
   3.386 +  and "geven == 
   3.387 +    (\<And>n kvs t k v kvs'. \<lbrakk> n > 0; n \<le> Suc (length kvs); Q n kvs; 
   3.388 +       rbtreeify_g n kvs = (t, (k, v) # kvs'); n \<le> Suc (length kvs'); Q n kvs' \<rbrakk>
   3.389 +    \<Longrightarrow> Q (2 * n) kvs)"
   3.390 +  and "godd == 
   3.391 +    (\<And>n kvs t k v kvs'. \<lbrakk> n > 0; n \<le> length kvs; P n kvs;
   3.392 +       rbtreeify_f n kvs = (t, (k, v) # kvs'); n \<le> Suc (length kvs'); Q n kvs' \<rbrakk>
   3.393 +    \<Longrightarrow> Q (Suc (2 * n)) kvs)"
   3.394 +  shows "\<lbrakk> n \<le> length kvs; 
   3.395 +           PROP f0; PROP f1; PROP feven; PROP fodd; 
   3.396 +           PROP g0; PROP g1; PROP geven; PROP godd \<rbrakk>
   3.397 +         \<Longrightarrow> P n kvs"
   3.398 +  and "\<lbrakk> n \<le> Suc (length kvs);
   3.399 +          PROP f0; PROP f1; PROP feven; PROP fodd; 
   3.400 +          PROP g0; PROP g1; PROP geven; PROP godd \<rbrakk>
   3.401 +       \<Longrightarrow> Q n kvs"
   3.402 +proof -
   3.403 +  assume f0: "PROP f0" and f1: "PROP f1" and feven: "PROP feven" and fodd: "PROP fodd"
   3.404 +    and g0: "PROP g0" and g1: "PROP g1" and geven: "PROP geven" and godd: "PROP godd"
   3.405 +  show "n \<le> length kvs \<Longrightarrow> P n kvs" and "n \<le> Suc (length kvs) \<Longrightarrow> Q n kvs"
   3.406 +  proof(induction rule: rbtreeify_f_rbtreeify_g.induct)
   3.407 +    case (1 n kvs)
   3.408 +    show ?case
   3.409 +    proof(cases "n \<le> 1")
   3.410 +      case True thus ?thesis using "1.prems"
   3.411 +        by(cases n kvs rule: nat.exhaust[case_product list.exhaust])
   3.412 +          (auto simp add: f0[unfolded f0_def] f1[unfolded f1_def])
   3.413 +    next
   3.414 +      case False 
   3.415 +      hence ns: "n \<noteq> 0" "n \<noteq> 1" by simp_all
   3.416 +      hence ge0: "n div 2 > 0" by simp
   3.417 +      note IH = "1.IH"[OF ns]
   3.418 +      show ?thesis
   3.419 +      proof(cases "n mod 2 = 0")
   3.420 +        case True note ge0 
   3.421 +        moreover from "1.prems" have n2: "n div 2 \<le> length kvs" by simp
   3.422 +        moreover with True have "P (n div 2) kvs" by(rule IH)
   3.423 +        moreover from length_rbtreeify_f[OF n2] ge0 "1.prems" obtain t k v kvs' 
   3.424 +          where kvs': "rbtreeify_f (n div 2) kvs = (t, (k, v) # kvs')"
   3.425 +          by(cases "snd (rbtreeify_f (n div 2) kvs)")
   3.426 +            (auto simp add: snd_def split: prod.split_asm)
   3.427 +        moreover from "1.prems" length_rbtreeify_f[OF n2] ge0
   3.428 +        have "n div 2 \<le> Suc (length kvs')" by(simp add: kvs')
   3.429 +        moreover with True kvs'[symmetric] refl refl
   3.430 +        have "Q (n div 2) kvs'" by(rule IH)
   3.431 +        moreover note feven[unfolded feven_def]
   3.432 +          (* FIXME: why does by(rule feven[unfolded feven_def]) not work? *)
   3.433 +        ultimately have "P (2 * (n div 2)) kvs" by -
   3.434 +        thus ?thesis using True by (metis div_mod_equality' minus_nat.diff_0 nat_mult_commute)
   3.435 +      next
   3.436 +        case False note ge0
   3.437 +        moreover from "1.prems" have n2: "n div 2 \<le> length kvs" by simp
   3.438 +        moreover with False have "P (n div 2) kvs" by(rule IH)
   3.439 +        moreover from length_rbtreeify_f[OF n2] ge0 "1.prems" obtain t k v kvs' 
   3.440 +          where kvs': "rbtreeify_f (n div 2) kvs = (t, (k, v) # kvs')"
   3.441 +          by(cases "snd (rbtreeify_f (n div 2) kvs)")
   3.442 +            (auto simp add: snd_def split: prod.split_asm)
   3.443 +        moreover from "1.prems" length_rbtreeify_f[OF n2] ge0 False
   3.444 +        have "n div 2 \<le> length kvs'" by(simp add: kvs') arith
   3.445 +        moreover with False kvs'[symmetric] refl refl have "P (n div 2) kvs'" by(rule IH)
   3.446 +        moreover note fodd[unfolded fodd_def]
   3.447 +        ultimately have "P (Suc (2 * (n div 2))) kvs" by -
   3.448 +        thus ?thesis using False 
   3.449 +          by simp (metis One_nat_def Suc_eq_plus1_left le_add_diff_inverse mod_less_eq_dividend mult_div_cancel)
   3.450 +      qed
   3.451 +    qed
   3.452 +  next
   3.453 +    case (2 n kvs)
   3.454 +    show ?case
   3.455 +    proof(cases "n \<le> 1")
   3.456 +      case True thus ?thesis using "2.prems"
   3.457 +        by(cases n kvs rule: nat.exhaust[case_product list.exhaust])
   3.458 +          (auto simp add: g0[unfolded g0_def] g1[unfolded g1_def])
   3.459 +    next
   3.460 +      case False 
   3.461 +      hence ns: "\<not> (n = 0 \<or> n = 1)" by simp
   3.462 +      hence ge0: "n div 2 > 0" by simp
   3.463 +      note IH = "2.IH"[OF ns]
   3.464 +      show ?thesis
   3.465 +      proof(cases "n mod 2 = 0")
   3.466 +        case True note ge0
   3.467 +        moreover from "2.prems" have n2: "n div 2 \<le> Suc (length kvs)" by simp
   3.468 +        moreover with True have "Q (n div 2) kvs" by(rule IH)
   3.469 +        moreover from length_rbtreeify_g[OF ge0 n2] ge0 "2.prems" obtain t k v kvs' 
   3.470 +          where kvs': "rbtreeify_g (n div 2) kvs = (t, (k, v) # kvs')"
   3.471 +          by(cases "snd (rbtreeify_g (n div 2) kvs)")
   3.472 +            (auto simp add: snd_def split: prod.split_asm)
   3.473 +        moreover from "2.prems" length_rbtreeify_g[OF ge0 n2] ge0
   3.474 +        have "n div 2 \<le> Suc (length kvs')" by(simp add: kvs')
   3.475 +        moreover with True kvs'[symmetric] refl refl 
   3.476 +        have "Q (n div 2) kvs'" by(rule IH)
   3.477 +        moreover note geven[unfolded geven_def]
   3.478 +        ultimately have "Q (2 * (n div 2)) kvs" by -
   3.479 +        thus ?thesis using True 
   3.480 +          by(metis div_mod_equality' minus_nat.diff_0 nat_mult_commute)
   3.481 +      next
   3.482 +        case False note ge0
   3.483 +        moreover from "2.prems" have n2: "n div 2 \<le> length kvs" by simp
   3.484 +        moreover with False have "P (n div 2) kvs" by(rule IH)
   3.485 +        moreover from length_rbtreeify_f[OF n2] ge0 "2.prems" False obtain t k v kvs' 
   3.486 +          where kvs': "rbtreeify_f (n div 2) kvs = (t, (k, v) # kvs')"
   3.487 +          by(cases "snd (rbtreeify_f (n div 2) kvs)")
   3.488 +            (auto simp add: snd_def split: prod.split_asm, arith)
   3.489 +        moreover from "2.prems" length_rbtreeify_f[OF n2] ge0 False
   3.490 +        have "n div 2 \<le> Suc (length kvs')" by(simp add: kvs') arith
   3.491 +        moreover with False kvs'[symmetric] refl refl
   3.492 +        have "Q (n div 2) kvs'" by(rule IH)
   3.493 +        moreover note godd[unfolded godd_def]
   3.494 +        ultimately have "Q (Suc (2 * (n div 2))) kvs" by -
   3.495 +        thus ?thesis using False 
   3.496 +          by simp (metis One_nat_def Suc_eq_plus1_left le_add_diff_inverse mod_less_eq_dividend mult_div_cancel)
   3.497 +      qed
   3.498 +    qed
   3.499 +  qed
   3.500 +qed
   3.501 +
   3.502 +lemma inv1_rbtreeify_f: "n \<le> length kvs 
   3.503 +  \<Longrightarrow> inv1 (fst (rbtreeify_f n kvs))"
   3.504 +  and inv1_rbtreeify_g: "n \<le> Suc (length kvs)
   3.505 +  \<Longrightarrow> inv1 (fst (rbtreeify_g n kvs))"
   3.506 +by(induct n kvs and n kvs rule: rbtreeify_induct) simp_all
   3.507 +
   3.508 +fun plog2 :: "nat \<Rightarrow> nat" 
   3.509 +where "plog2 n = (if n \<le> 1 then 0 else plog2 (n div 2) + 1)"
   3.510 +
   3.511 +declare plog2.simps [simp del]
   3.512 +
   3.513 +lemma plog2_simps [simp]:
   3.514 +  "plog2 0 = 0" "plog2 (Suc 0) = 0"
   3.515 +  "0 < n \<Longrightarrow> plog2 (2 * n) = 1 + plog2 n"
   3.516 +  "0 < n \<Longrightarrow> plog2 (Suc (2 * n)) = 1 + plog2 n"
   3.517 +by(subst plog2.simps, simp add: Suc_double_half)+
   3.518 +
   3.519 +lemma bheight_rbtreeify_f: "n \<le> length kvs
   3.520 +  \<Longrightarrow> bheight (fst (rbtreeify_f n kvs)) = plog2 n"
   3.521 +  and bheight_rbtreeify_g: "n \<le> Suc (length kvs)
   3.522 +  \<Longrightarrow> bheight (fst (rbtreeify_g n kvs)) = plog2 n"
   3.523 +by(induct n kvs and n kvs rule: rbtreeify_induct) simp_all
   3.524 +
   3.525 +lemma bheight_rbtreeify_f_eq_plog2I:
   3.526 +  "\<lbrakk> rbtreeify_f n kvs = (t, kvs'); n \<le> length kvs \<rbrakk> 
   3.527 +  \<Longrightarrow> bheight t = plog2 n"
   3.528 +using bheight_rbtreeify_f[of n kvs] by simp
   3.529 +
   3.530 +lemma bheight_rbtreeify_g_eq_plog2I: 
   3.531 +  "\<lbrakk> rbtreeify_g n kvs = (t, kvs'); n \<le> Suc (length kvs) \<rbrakk>
   3.532 +  \<Longrightarrow> bheight t = plog2 n"
   3.533 +using bheight_rbtreeify_g[of n kvs] by simp
   3.534 +
   3.535 +hide_const (open) plog2
   3.536 +
   3.537 +lemma inv2_rbtreeify_f: "n \<le> length kvs
   3.538 +  \<Longrightarrow> inv2 (fst (rbtreeify_f n kvs))"
   3.539 +  and inv2_rbtreeify_g: "n \<le> Suc (length kvs)
   3.540 +  \<Longrightarrow> inv2 (fst (rbtreeify_g n kvs))"
   3.541 +by(induct n kvs and n kvs rule: rbtreeify_induct)
   3.542 +  (auto simp add: bheight_rbtreeify_f bheight_rbtreeify_g 
   3.543 +        intro: bheight_rbtreeify_f_eq_plog2I bheight_rbtreeify_g_eq_plog2I)
   3.544 +
   3.545 +lemma "n \<le> length kvs \<Longrightarrow> True"
   3.546 +  and color_of_rbtreeify_g:
   3.547 +  "\<lbrakk> n \<le> Suc (length kvs); 0 < n \<rbrakk> 
   3.548 +  \<Longrightarrow> color_of (fst (rbtreeify_g n kvs)) = B"
   3.549 +by(induct n kvs and n kvs rule: rbtreeify_induct) simp_all
   3.550 +
   3.551 +lemma entries_rbtreeify_f_append:
   3.552 +  "n \<le> length kvs 
   3.553 +  \<Longrightarrow> entries (fst (rbtreeify_f n kvs)) @ snd (rbtreeify_f n kvs) = kvs"
   3.554 +  and entries_rbtreeify_g_append: 
   3.555 +  "n \<le> Suc (length kvs) 
   3.556 +  \<Longrightarrow> entries (fst (rbtreeify_g n kvs)) @ snd (rbtreeify_g n kvs) = kvs"
   3.557 +by(induction rule: rbtreeify_induct) simp_all
   3.558 +
   3.559 +lemma length_entries_rbtreeify_f:
   3.560 +  "n \<le> length kvs \<Longrightarrow> length (entries (fst (rbtreeify_f n kvs))) = n"
   3.561 +  and length_entries_rbtreeify_g: 
   3.562 +  "n \<le> Suc (length kvs) \<Longrightarrow> length (entries (fst (rbtreeify_g n kvs))) = n - 1"
   3.563 +by(induct rule: rbtreeify_induct) simp_all
   3.564 +
   3.565 +lemma rbtreeify_f_conv_drop: 
   3.566 +  "n \<le> length kvs \<Longrightarrow> snd (rbtreeify_f n kvs) = drop n kvs"
   3.567 +using entries_rbtreeify_f_append[of n kvs]
   3.568 +by(simp add: append_eq_conv_conj length_entries_rbtreeify_f)
   3.569 +
   3.570 +lemma rbtreeify_g_conv_drop: 
   3.571 +  "n \<le> Suc (length kvs) \<Longrightarrow> snd (rbtreeify_g n kvs) = drop (n - 1) kvs"
   3.572 +using entries_rbtreeify_g_append[of n kvs]
   3.573 +by(simp add: append_eq_conv_conj length_entries_rbtreeify_g)
   3.574 +
   3.575 +lemma entries_rbtreeify_f [simp]:
   3.576 +  "n \<le> length kvs \<Longrightarrow> entries (fst (rbtreeify_f n kvs)) = take n kvs"
   3.577 +using entries_rbtreeify_f_append[of n kvs]
   3.578 +by(simp add: append_eq_conv_conj length_entries_rbtreeify_f)
   3.579 +
   3.580 +lemma entries_rbtreeify_g [simp]:
   3.581 +  "n \<le> Suc (length kvs) \<Longrightarrow> 
   3.582 +  entries (fst (rbtreeify_g n kvs)) = take (n - 1) kvs"
   3.583 +using entries_rbtreeify_g_append[of n kvs]
   3.584 +by(simp add: append_eq_conv_conj length_entries_rbtreeify_g)
   3.585 +
   3.586 +lemma keys_rbtreeify_f [simp]: "n \<le> length kvs
   3.587 +  \<Longrightarrow> keys (fst (rbtreeify_f n kvs)) = take n (map fst kvs)"
   3.588 +by(simp add: keys_def take_map)
   3.589 +
   3.590 +lemma keys_rbtreeify_g [simp]: "n \<le> Suc (length kvs)
   3.591 +  \<Longrightarrow> keys (fst (rbtreeify_g n kvs)) = take (n - 1) (map fst kvs)"
   3.592 +by(simp add: keys_def take_map)
   3.593 +
   3.594 +lemma rbtreeify_fD: 
   3.595 +  "\<lbrakk> rbtreeify_f n kvs = (t, kvs'); n \<le> length kvs \<rbrakk> 
   3.596 +  \<Longrightarrow> entries t = take n kvs \<and> kvs' = drop n kvs"
   3.597 +using rbtreeify_f_conv_drop[of n kvs] entries_rbtreeify_f[of n kvs] by simp
   3.598 +
   3.599 +lemma rbtreeify_gD: 
   3.600 +  "\<lbrakk> rbtreeify_g n kvs = (t, kvs'); n \<le> Suc (length kvs) \<rbrakk>
   3.601 +  \<Longrightarrow> entries t = take (n - 1) kvs \<and> kvs' = drop (n - 1) kvs"
   3.602 +using rbtreeify_g_conv_drop[of n kvs] entries_rbtreeify_g[of n kvs] by simp
   3.603 +
   3.604 +lemma entries_rbtreeify [simp]: "entries (rbtreeify kvs) = kvs"
   3.605 +by(simp add: rbtreeify_def entries_rbtreeify_g)
   3.606 +
   3.607 +context linorder begin
   3.608 +
   3.609 +lemma rbt_sorted_rbtreeify_f: 
   3.610 +  "\<lbrakk> n \<le> length kvs; sorted (map fst kvs); distinct (map fst kvs) \<rbrakk> 
   3.611 +  \<Longrightarrow> rbt_sorted (fst (rbtreeify_f n kvs))"
   3.612 +  and rbt_sorted_rbtreeify_g: 
   3.613 +  "\<lbrakk> n \<le> Suc (length kvs); sorted (map fst kvs); distinct (map fst kvs) \<rbrakk>
   3.614 +  \<Longrightarrow> rbt_sorted (fst (rbtreeify_g n kvs))"
   3.615 +proof(induction n kvs and n kvs rule: rbtreeify_induct)
   3.616 +  case (f_even n kvs t k v kvs')
   3.617 +  from rbtreeify_fD[OF `rbtreeify_f n kvs = (t, (k, v) # kvs')` `n \<le> length kvs`]
   3.618 +  have "entries t = take n kvs"
   3.619 +    and kvs': "drop n kvs = (k, v) # kvs'" by simp_all
   3.620 +  hence unfold: "kvs = take n kvs @ (k, v) # kvs'" by(metis append_take_drop_id)
   3.621 +  from `sorted (map fst kvs)` kvs'
   3.622 +  have "(\<forall>(x, y) \<in> set (take n kvs). x \<le> k) \<and> (\<forall>(x, y) \<in> set kvs'. k \<le> x)"
   3.623 +    by(subst (asm) unfold)(auto simp add: sorted_append sorted_Cons)
   3.624 +  moreover from `distinct (map fst kvs)` kvs'
   3.625 +  have "(\<forall>(x, y) \<in> set (take n kvs). x \<noteq> k) \<and> (\<forall>(x, y) \<in> set kvs'. x \<noteq> k)"
   3.626 +    by(subst (asm) unfold)(auto intro: rev_image_eqI)
   3.627 +  ultimately have "(\<forall>(x, y) \<in> set (take n kvs). x < k) \<and> (\<forall>(x, y) \<in> set kvs'. k < x)"
   3.628 +    by fastforce
   3.629 +  hence "fst (rbtreeify_f n kvs) |\<guillemotleft> k" "k \<guillemotleft>| fst (rbtreeify_g n kvs')"
   3.630 +    using `n \<le> Suc (length kvs')` `n \<le> length kvs` set_take_subset[of "n - 1" kvs']
   3.631 +    by(auto simp add: ord.rbt_greater_prop ord.rbt_less_prop take_map split_def)
   3.632 +  moreover from `sorted (map fst kvs)` `distinct (map fst kvs)`
   3.633 +  have "rbt_sorted (fst (rbtreeify_f n kvs))" by(rule f_even.IH)
   3.634 +  moreover have "sorted (map fst kvs')" "distinct (map fst kvs')"
   3.635 +    using `sorted (map fst kvs)` `distinct (map fst kvs)`
   3.636 +    by(subst (asm) (1 2) unfold, simp add: sorted_append sorted_Cons)+
   3.637 +  hence "rbt_sorted (fst (rbtreeify_g n kvs'))" by(rule f_even.IH)
   3.638 +  ultimately show ?case
   3.639 +    using `0 < n` `rbtreeify_f n kvs = (t, (k, v) # kvs')` by simp
   3.640 +next
   3.641 +  case (f_odd n kvs t k v kvs')
   3.642 +  from rbtreeify_fD[OF `rbtreeify_f n kvs = (t, (k, v) # kvs')` `n \<le> length kvs`]
   3.643 +  have "entries t = take n kvs" 
   3.644 +    and kvs': "drop n kvs = (k, v) # kvs'" by simp_all
   3.645 +  hence unfold: "kvs = take n kvs @ (k, v) # kvs'" by(metis append_take_drop_id)
   3.646 +  from `sorted (map fst kvs)` kvs'
   3.647 +  have "(\<forall>(x, y) \<in> set (take n kvs). x \<le> k) \<and> (\<forall>(x, y) \<in> set kvs'. k \<le> x)"
   3.648 +    by(subst (asm) unfold)(auto simp add: sorted_append sorted_Cons)
   3.649 +  moreover from `distinct (map fst kvs)` kvs'
   3.650 +  have "(\<forall>(x, y) \<in> set (take n kvs). x \<noteq> k) \<and> (\<forall>(x, y) \<in> set kvs'. x \<noteq> k)"
   3.651 +    by(subst (asm) unfold)(auto intro: rev_image_eqI)
   3.652 +  ultimately have "(\<forall>(x, y) \<in> set (take n kvs). x < k) \<and> (\<forall>(x, y) \<in> set kvs'. k < x)"
   3.653 +    by fastforce
   3.654 +  hence "fst (rbtreeify_f n kvs) |\<guillemotleft> k" "k \<guillemotleft>| fst (rbtreeify_f n kvs')"
   3.655 +    using `n \<le> length kvs'` `n \<le> length kvs` set_take_subset[of n kvs']
   3.656 +    by(auto simp add: rbt_greater_prop rbt_less_prop take_map split_def)
   3.657 +  moreover from `sorted (map fst kvs)` `distinct (map fst kvs)`
   3.658 +  have "rbt_sorted (fst (rbtreeify_f n kvs))" by(rule f_odd.IH)
   3.659 +  moreover have "sorted (map fst kvs')" "distinct (map fst kvs')"
   3.660 +    using `sorted (map fst kvs)` `distinct (map fst kvs)`
   3.661 +    by(subst (asm) (1 2) unfold, simp add: sorted_append sorted_Cons)+
   3.662 +  hence "rbt_sorted (fst (rbtreeify_f n kvs'))" by(rule f_odd.IH)
   3.663 +  ultimately show ?case 
   3.664 +    using `0 < n` `rbtreeify_f n kvs = (t, (k, v) # kvs')` by simp
   3.665 +next
   3.666 +  case (g_even n kvs t k v kvs')
   3.667 +  from rbtreeify_gD[OF `rbtreeify_g n kvs = (t, (k, v) # kvs')` `n \<le> Suc (length kvs)`]
   3.668 +  have t: "entries t = take (n - 1) kvs" 
   3.669 +    and kvs': "drop (n - 1) kvs = (k, v) # kvs'" by simp_all
   3.670 +  hence unfold: "kvs = take (n - 1) kvs @ (k, v) # kvs'" by(metis append_take_drop_id)
   3.671 +  from `sorted (map fst kvs)` kvs'
   3.672 +  have "(\<forall>(x, y) \<in> set (take (n - 1) kvs). x \<le> k) \<and> (\<forall>(x, y) \<in> set kvs'. k \<le> x)"
   3.673 +    by(subst (asm) unfold)(auto simp add: sorted_append sorted_Cons)
   3.674 +  moreover from `distinct (map fst kvs)` kvs'
   3.675 +  have "(\<forall>(x, y) \<in> set (take (n - 1) kvs). x \<noteq> k) \<and> (\<forall>(x, y) \<in> set kvs'. x \<noteq> k)"
   3.676 +    by(subst (asm) unfold)(auto intro: rev_image_eqI)
   3.677 +  ultimately have "(\<forall>(x, y) \<in> set (take (n - 1) kvs). x < k) \<and> (\<forall>(x, y) \<in> set kvs'. k < x)"
   3.678 +    by fastforce
   3.679 +  hence "fst (rbtreeify_g n kvs) |\<guillemotleft> k" "k \<guillemotleft>| fst (rbtreeify_g n kvs')"
   3.680 +    using `n \<le> Suc (length kvs')` `n \<le> Suc (length kvs)` set_take_subset[of "n - 1" kvs']
   3.681 +    by(auto simp add: rbt_greater_prop rbt_less_prop take_map split_def)
   3.682 +  moreover from `sorted (map fst kvs)` `distinct (map fst kvs)`
   3.683 +  have "rbt_sorted (fst (rbtreeify_g n kvs))" by(rule g_even.IH)
   3.684 +  moreover have "sorted (map fst kvs')" "distinct (map fst kvs')"
   3.685 +    using `sorted (map fst kvs)` `distinct (map fst kvs)`
   3.686 +    by(subst (asm) (1 2) unfold, simp add: sorted_append sorted_Cons)+
   3.687 +  hence "rbt_sorted (fst (rbtreeify_g n kvs'))" by(rule g_even.IH)
   3.688 +  ultimately show ?case using `0 < n` `rbtreeify_g n kvs = (t, (k, v) # kvs')` by simp
   3.689 +next
   3.690 +  case (g_odd n kvs t k v kvs')
   3.691 +  from rbtreeify_fD[OF `rbtreeify_f n kvs = (t, (k, v) # kvs')` `n \<le> length kvs`]
   3.692 +  have "entries t = take n kvs"
   3.693 +    and kvs': "drop n kvs = (k, v) # kvs'" by simp_all
   3.694 +  hence unfold: "kvs = take n kvs @ (k, v) # kvs'" by(metis append_take_drop_id)
   3.695 +  from `sorted (map fst kvs)` kvs'
   3.696 +  have "(\<forall>(x, y) \<in> set (take n kvs). x \<le> k) \<and> (\<forall>(x, y) \<in> set kvs'. k \<le> x)"
   3.697 +    by(subst (asm) unfold)(auto simp add: sorted_append sorted_Cons)
   3.698 +  moreover from `distinct (map fst kvs)` kvs'
   3.699 +  have "(\<forall>(x, y) \<in> set (take n kvs). x \<noteq> k) \<and> (\<forall>(x, y) \<in> set kvs'. x \<noteq> k)"
   3.700 +    by(subst (asm) unfold)(auto intro: rev_image_eqI)
   3.701 +  ultimately have "(\<forall>(x, y) \<in> set (take n kvs). x < k) \<and> (\<forall>(x, y) \<in> set kvs'. k < x)"
   3.702 +    by fastforce
   3.703 +  hence "fst (rbtreeify_f n kvs) |\<guillemotleft> k" "k \<guillemotleft>| fst (rbtreeify_g n kvs')"
   3.704 +    using `n \<le> Suc (length kvs')` `n \<le> length kvs` set_take_subset[of "n - 1" kvs']
   3.705 +    by(auto simp add: rbt_greater_prop rbt_less_prop take_map split_def)
   3.706 +  moreover from `sorted (map fst kvs)` `distinct (map fst kvs)`
   3.707 +  have "rbt_sorted (fst (rbtreeify_f n kvs))" by(rule g_odd.IH)
   3.708 +  moreover have "sorted (map fst kvs')" "distinct (map fst kvs')"
   3.709 +    using `sorted (map fst kvs)` `distinct (map fst kvs)`
   3.710 +    by(subst (asm) (1 2) unfold, simp add: sorted_append sorted_Cons)+
   3.711 +  hence "rbt_sorted (fst (rbtreeify_g n kvs'))" by(rule g_odd.IH)
   3.712 +  ultimately show ?case
   3.713 +    using `0 < n` `rbtreeify_f n kvs = (t, (k, v) # kvs')` by simp
   3.714 +qed simp_all
   3.715 +
   3.716 +lemma rbt_sorted_rbtreeify: 
   3.717 +  "\<lbrakk> sorted (map fst kvs); distinct (map fst kvs) \<rbrakk> \<Longrightarrow> rbt_sorted (rbtreeify kvs)"
   3.718 +by(simp add: rbtreeify_def rbt_sorted_rbtreeify_g)
   3.719 +
   3.720 +lemma is_rbt_rbtreeify: 
   3.721 +  "\<lbrakk> sorted (map fst kvs); distinct (map fst kvs) \<rbrakk>
   3.722 +  \<Longrightarrow> is_rbt (rbtreeify kvs)"
   3.723 +by(simp add: is_rbt_def rbtreeify_def inv1_rbtreeify_g inv2_rbtreeify_g rbt_sorted_rbtreeify_g color_of_rbtreeify_g)
   3.724 +
   3.725 +lemma rbt_lookup_rbtreeify:
   3.726 +  "\<lbrakk> sorted (map fst kvs); distinct (map fst kvs) \<rbrakk> \<Longrightarrow> 
   3.727 +  rbt_lookup (rbtreeify kvs) = map_of kvs"
   3.728 +by(simp add: map_of_entries[symmetric] rbt_sorted_rbtreeify)
   3.729 +
   3.730 +end
   3.731 +
   3.732 +text {* 
   3.733 +  Functions to compare the height of two rbt trees, taken from 
   3.734 +  Andrew W. Appel, Efficient Verified Red-Black Trees (September 2011)
   3.735 +*}
   3.736 +
   3.737 +fun skip_red :: "('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
   3.738 +where
   3.739 +  "skip_red (Branch color.R l k v r) = l"
   3.740 +| "skip_red t = t"
   3.741 +
   3.742 +fun skip_black :: "('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
   3.743 +where
   3.744 +  "skip_black (Branch color.B l k v r) = l"
   3.745 +| "skip_black t = t"
   3.746 +
   3.747 +datatype compare = LT | GT | EQ
   3.748 +
   3.749 +partial_function (tailrec) compare_height :: "('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt \<Rightarrow> compare"
   3.750 +where
   3.751 +  "compare_height sx s t tx =
   3.752 +  (case (skip_red sx, skip_red s, skip_red t, skip_red tx) of
   3.753 +     (Branch _ sx' _ _ _, Branch _ s' _ _ _, Branch _ t' _ _ _, Branch _ tx' _ _ _) \<Rightarrow> 
   3.754 +       compare_height (skip_black sx') s' t' (skip_black tx')
   3.755 +   | (_, rbt.Empty, _, Branch _ _ _ _ _) \<Rightarrow> LT
   3.756 +   | (Branch _ _ _ _ _, _, rbt.Empty, _) \<Rightarrow> GT
   3.757 +   | (Branch _ sx' _ _ _, Branch _ s' _ _ _, Branch _ t' _ _ _, rbt.Empty) \<Rightarrow>
   3.758 +       compare_height (skip_black sx') s' t' rbt.Empty
   3.759 +   | (rbt.Empty, Branch _ s' _ _ _, Branch _ t' _ _ _, Branch _ tx' _ _ _) \<Rightarrow>
   3.760 +       compare_height rbt.Empty s' t' (skip_black tx')
   3.761 +   | _ \<Rightarrow> EQ)"
   3.762 +
   3.763 +declare compare_height.simps [code]
   3.764 +
   3.765 +hide_type (open) compare
   3.766 +hide_const (open)
   3.767 +  compare_height skip_black skip_red LT GT EQ compare_case compare_rec 
   3.768 +  Abs_compare Rep_compare compare_rep_set
   3.769 +hide_fact (open)
   3.770 +  Abs_compare_cases Abs_compare_induct Abs_compare_inject Abs_compare_inverse
   3.771 +  Rep_compare Rep_compare_cases Rep_compare_induct Rep_compare_inject Rep_compare_inverse
   3.772 +  compare.simps compare.exhaust compare.induct compare.recs compare.simps
   3.773 +  compare.size compare.case_cong compare.weak_case_cong compare.cases 
   3.774 +  compare.nchotomy compare.split compare.split_asm compare_rec_def
   3.775 +  compare.eq.refl compare.eq.simps
   3.776 +  compare.EQ_def compare.GT_def compare.LT_def
   3.777 +  equal_compare_def
   3.778 +  skip_red_def skip_red.simps skip_red.induct 
   3.779 +  skip_black_def skip_black.simps skip_black.induct
   3.780 +  compare_height.simps
   3.781 +
   3.782 +subsection {* union and intersection of sorted associative lists *}
   3.783 +
   3.784 +context ord begin
   3.785 +
   3.786 +function sunion_with :: "('a \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('a \<times> 'b) list" 
   3.787 +where
   3.788 +  "sunion_with f ((k, v) # as) ((k', v') # bs) =
   3.789 +   (if k > k' then (k', v') # sunion_with f ((k, v) # as) bs
   3.790 +    else if k < k' then (k, v) # sunion_with f as ((k', v') # bs)
   3.791 +    else (k, f k v v') # sunion_with f as bs)"
   3.792 +| "sunion_with f [] bs = bs"
   3.793 +| "sunion_with f as [] = as"
   3.794 +by pat_completeness auto
   3.795 +termination by lexicographic_order
   3.796 +
   3.797 +function sinter_with :: "('a \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('a \<times> 'b) list"
   3.798 +where
   3.799 +  "sinter_with f ((k, v) # as) ((k', v') # bs) =
   3.800 +  (if k > k' then sinter_with f ((k, v) # as) bs
   3.801 +   else if k < k' then sinter_with f as ((k', v') # bs)
   3.802 +   else (k, f k v v') # sinter_with f as bs)"
   3.803 +| "sinter_with f [] _ = []"
   3.804 +| "sinter_with f _ [] = []"
   3.805 +by pat_completeness auto
   3.806 +termination by lexicographic_order
   3.807 +
   3.808 +end
   3.809 +
   3.810 +declare ord.sunion_with.simps [code] ord.sinter_with.simps[code]
   3.811 +
   3.812 +context linorder begin
   3.813 +
   3.814 +lemma set_fst_sunion_with: 
   3.815 +  "set (map fst (sunion_with f xs ys)) = set (map fst xs) \<union> set (map fst ys)"
   3.816 +by(induct f xs ys rule: sunion_with.induct) auto
   3.817 +
   3.818 +lemma sorted_sunion_with [simp]:
   3.819 +  "\<lbrakk> sorted (map fst xs); sorted (map fst ys) \<rbrakk> 
   3.820 +  \<Longrightarrow> sorted (map fst (sunion_with f xs ys))"
   3.821 +by(induct f xs ys rule: sunion_with.induct)
   3.822 +  (auto simp add: sorted_Cons set_fst_sunion_with simp del: set_map)
   3.823 +
   3.824 +lemma distinct_sunion_with [simp]:
   3.825 +  "\<lbrakk> distinct (map fst xs); distinct (map fst ys); sorted (map fst xs); sorted (map fst ys) \<rbrakk>
   3.826 +  \<Longrightarrow> distinct (map fst (sunion_with f xs ys))"
   3.827 +proof(induct f xs ys rule: sunion_with.induct)
   3.828 +  case (1 f k v xs k' v' ys)
   3.829 +  have "\<lbrakk> \<not> k < k'; \<not> k' < k \<rbrakk> \<Longrightarrow> k = k'" by simp
   3.830 +  thus ?case using "1"
   3.831 +    by(auto simp add: set_fst_sunion_with sorted_Cons simp del: set_map)
   3.832 +qed simp_all
   3.833 +
   3.834 +lemma map_of_sunion_with: 
   3.835 +  "\<lbrakk> sorted (map fst xs); sorted (map fst ys) \<rbrakk>
   3.836 +  \<Longrightarrow> map_of (sunion_with f xs ys) k = 
   3.837 +  (case map_of xs k of None \<Rightarrow> map_of ys k 
   3.838 +  | Some v \<Rightarrow> case map_of ys k of None \<Rightarrow> Some v 
   3.839 +              | Some w \<Rightarrow> Some (f k v w))"
   3.840 +by(induct f xs ys rule: sunion_with.induct)(auto simp add: sorted_Cons split: option.split dest: map_of_SomeD bspec)
   3.841 +
   3.842 +lemma set_fst_sinter_with [simp]:
   3.843 +  "\<lbrakk> sorted (map fst xs); sorted (map fst ys) \<rbrakk>
   3.844 +  \<Longrightarrow> set (map fst (sinter_with f xs ys)) = set (map fst xs) \<inter> set (map fst ys)"
   3.845 +by(induct f xs ys rule: sinter_with.induct)(auto simp add: sorted_Cons simp del: set_map)
   3.846 +
   3.847 +lemma set_fst_sinter_with_subset1:
   3.848 +  "set (map fst (sinter_with f xs ys)) \<subseteq> set (map fst xs)"
   3.849 +by(induct f xs ys rule: sinter_with.induct) auto
   3.850 +
   3.851 +lemma set_fst_sinter_with_subset2:
   3.852 +  "set (map fst (sinter_with f xs ys)) \<subseteq> set (map fst ys)"
   3.853 +by(induct f xs ys rule: sinter_with.induct)(auto simp del: set_map)
   3.854 +
   3.855 +lemma sorted_sinter_with [simp]:
   3.856 +  "\<lbrakk> sorted (map fst xs); sorted (map fst ys) \<rbrakk>
   3.857 +  \<Longrightarrow> sorted (map fst (sinter_with f xs ys))"
   3.858 +by(induct f xs ys rule: sinter_with.induct)(auto simp add: sorted_Cons simp del: set_map)
   3.859 +
   3.860 +lemma distinct_sinter_with [simp]:
   3.861 +  "\<lbrakk> distinct (map fst xs); distinct (map fst ys) \<rbrakk>
   3.862 +  \<Longrightarrow> distinct (map fst (sinter_with f xs ys))"
   3.863 +proof(induct f xs ys rule: sinter_with.induct)
   3.864 +  case (1 f k v as k' v' bs)
   3.865 +  have "\<lbrakk> \<not> k < k'; \<not> k' < k \<rbrakk> \<Longrightarrow> k = k'" by simp
   3.866 +  thus ?case using "1" set_fst_sinter_with_subset1[of f as bs]
   3.867 +    set_fst_sinter_with_subset2[of f as bs]
   3.868 +    by(auto simp del: set_map)
   3.869 +qed simp_all
   3.870 +
   3.871 +lemma map_of_sinter_with:
   3.872 +  "\<lbrakk> sorted (map fst xs); sorted (map fst ys) \<rbrakk>
   3.873 +  \<Longrightarrow> map_of (sinter_with f xs ys) k = 
   3.874 +  (case map_of xs k of None \<Rightarrow> None | Some v \<Rightarrow> Option.map (f k v) (map_of ys k))"
   3.875 +apply(induct f xs ys rule: sinter_with.induct)
   3.876 +apply(auto simp add: sorted_Cons Option.map_def split: option.splits dest: map_of_SomeD bspec)
   3.877 +done
   3.878 +
   3.879 +end
   3.880 +
   3.881 +lemma distinct_map_of_rev: "distinct (map fst xs) \<Longrightarrow> map_of (rev xs) = map_of xs"
   3.882 +by(induct xs)(auto 4 3 simp add: map_add_def intro!: ext split: option.split intro: rev_image_eqI)
   3.883 +
   3.884 +lemma map_map_filter: 
   3.885 +  "map f (List.map_filter g xs) = List.map_filter (Option.map f \<circ> g) xs"
   3.886 +by(auto simp add: List.map_filter_def)
   3.887 +
   3.888 +lemma map_filter_option_map_const: 
   3.889 +  "List.map_filter (\<lambda>x. Option.map (\<lambda>y. f x) (g (f x))) xs = filter (\<lambda>x. g x \<noteq> None) (map f xs)"
   3.890 +by(auto simp add: map_filter_def filter_map o_def)
   3.891 +
   3.892 +lemma set_map_filter: "set (List.map_filter P xs) = the ` (P ` set xs - {None})"
   3.893 +by(auto simp add: List.map_filter_def intro: rev_image_eqI)
   3.894 +
   3.895 +context ord begin
   3.896 +
   3.897 +definition rbt_union_with_key :: "('a \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
   3.898 +where
   3.899 +  "rbt_union_with_key f t1 t2 =
   3.900 +  (case RBT_Impl.compare_height t1 t1 t2 t2
   3.901 +   of compare.EQ \<Rightarrow> rbtreeify (sunion_with f (entries t1) (entries t2))
   3.902 +    | compare.LT \<Rightarrow> fold (rbt_insert_with_key (\<lambda>k v w. f k w v)) t1 t2
   3.903 +    | compare.GT \<Rightarrow> fold (rbt_insert_with_key f) t2 t1)"
   3.904 +
   3.905 +definition rbt_union_with where
   3.906 +  "rbt_union_with f = rbt_union_with_key (\<lambda>_. f)"
   3.907 +
   3.908 +definition rbt_union where
   3.909 +  "rbt_union = rbt_union_with_key (%_ _ rv. rv)"
   3.910 +
   3.911 +definition rbt_inter_with_key :: "('a \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
   3.912 +where
   3.913 +  "rbt_inter_with_key f t1 t2 =
   3.914 +  (case RBT_Impl.compare_height t1 t1 t2 t2 
   3.915 +   of compare.EQ \<Rightarrow> rbtreeify (sinter_with f (entries t1) (entries t2))
   3.916 +    | compare.LT \<Rightarrow> rbtreeify (List.map_filter (\<lambda>(k, v). Option.map (\<lambda>w. (k, f k v w)) (rbt_lookup t2 k)) (entries t1))
   3.917 +    | compare.GT \<Rightarrow> rbtreeify (List.map_filter (\<lambda>(k, v). Option.map (\<lambda>w. (k, f k w v)) (rbt_lookup t1 k)) (entries t2)))"
   3.918 +
   3.919 +definition rbt_inter_with where
   3.920 +  "rbt_inter_with f = rbt_inter_with_key (\<lambda>_. f)"
   3.921 +
   3.922 +definition rbt_inter where
   3.923 +  "rbt_inter = rbt_inter_with_key (\<lambda>_ _ rv. rv)"
   3.924 +
   3.925 +end
   3.926 +
   3.927 +context linorder begin
   3.928 +
   3.929 +lemma rbt_sorted_entries_right_unique:
   3.930 +  "\<lbrakk> (k, v) \<in> set (entries t); (k, v') \<in> set (entries t); 
   3.931 +     rbt_sorted t \<rbrakk> \<Longrightarrow> v = v'"
   3.932 +by(auto dest!: distinct_entries inj_onD[where x="(k, v)" and y="(k, v')"] simp add: distinct_map)
   3.933 +
   3.934 +lemma rbt_sorted_fold_rbt_insertwk:
   3.935 +  "rbt_sorted t \<Longrightarrow> rbt_sorted (List.fold (\<lambda>(k, v). rbt_insert_with_key f k v) xs t)"
   3.936 +by(induct xs rule: rev_induct)(auto simp add: rbt_insertwk_rbt_sorted)
   3.937 +
   3.938 +lemma is_rbt_fold_rbt_insertwk:
   3.939 +  assumes "is_rbt t1"
   3.940 +  shows "is_rbt (fold (rbt_insert_with_key f) t2 t1)"
   3.941 +proof -
   3.942 +  def xs \<equiv> "entries t2"
   3.943 +  from assms show ?thesis unfolding fold_def xs_def[symmetric]
   3.944 +    by(induct xs rule: rev_induct)(auto simp add: rbt_insertwk_is_rbt)
   3.945 +qed
   3.946 +
   3.947 +lemma rbt_lookup_fold_rbt_insertwk:
   3.948 +  assumes t1: "rbt_sorted t1" and t2: "rbt_sorted t2"
   3.949 +  shows "rbt_lookup (fold (rbt_insert_with_key f) t1 t2) k =
   3.950 +  (case rbt_lookup t1 k of None \<Rightarrow> rbt_lookup t2 k
   3.951 +   | Some v \<Rightarrow> case rbt_lookup t2 k of None \<Rightarrow> Some v
   3.952 +               | Some w \<Rightarrow> Some (f k w v))"
   3.953 +proof -
   3.954 +  def xs \<equiv> "entries t1"
   3.955 +  hence dt1: "distinct (map fst xs)" using t1 by(simp add: distinct_entries)
   3.956 +  with t2 show ?thesis
   3.957 +    unfolding fold_def map_of_entries[OF t1, symmetric]
   3.958 +      xs_def[symmetric] distinct_map_of_rev[OF dt1, symmetric]
   3.959 +    apply(induct xs rule: rev_induct)
   3.960 +    apply(auto simp add: rbt_lookup_rbt_insertwk rbt_sorted_fold_rbt_insertwk split: option.splits)
   3.961 +    apply(auto simp add: distinct_map_of_rev intro: rev_image_eqI)
   3.962 +    done
   3.963 +qed
   3.964 +
   3.965 +lemma is_rbt_rbt_unionwk [simp]:
   3.966 +  "\<lbrakk> is_rbt t1; is_rbt t2 \<rbrakk> \<Longrightarrow> is_rbt (rbt_union_with_key f t1 t2)"
   3.967 +by(simp add: rbt_union_with_key_def Let_def is_rbt_fold_rbt_insertwk is_rbt_rbtreeify rbt_sorted_entries distinct_entries split: compare.split)
   3.968 +
   3.969 +lemma rbt_lookup_rbt_unionwk:
   3.970 +  "\<lbrakk> rbt_sorted t1; rbt_sorted t2 \<rbrakk> 
   3.971 +  \<Longrightarrow> rbt_lookup (rbt_union_with_key f t1 t2) k = 
   3.972 +  (case rbt_lookup t1 k of None \<Rightarrow> rbt_lookup t2 k 
   3.973 +   | Some v \<Rightarrow> case rbt_lookup t2 k of None \<Rightarrow> Some v 
   3.974 +              | Some w \<Rightarrow> Some (f k v w))"
   3.975 +by(auto simp add: rbt_union_with_key_def Let_def rbt_lookup_fold_rbt_insertwk rbt_sorted_entries distinct_entries map_of_sunion_with map_of_entries rbt_lookup_rbtreeify split: option.split compare.split)
   3.976 +
   3.977 +lemma rbt_unionw_is_rbt: "\<lbrakk> is_rbt lt; is_rbt rt \<rbrakk> \<Longrightarrow> is_rbt (rbt_union_with f lt rt)"
   3.978 +by(simp add: rbt_union_with_def)
   3.979 +
   3.980 +lemma rbt_union_is_rbt: "\<lbrakk> is_rbt lt; is_rbt rt \<rbrakk> \<Longrightarrow> is_rbt (rbt_union lt rt)"
   3.981 +by(simp add: rbt_union_def)
   3.982 +
   3.983 +lemma rbt_lookup_rbt_union:
   3.984 +  "\<lbrakk> rbt_sorted s; rbt_sorted t \<rbrakk> \<Longrightarrow>
   3.985 +  rbt_lookup (rbt_union s t) = rbt_lookup s ++ rbt_lookup t"
   3.986 +by(rule ext)(simp add: rbt_lookup_rbt_unionwk rbt_union_def map_add_def split: option.split)
   3.987 +
   3.988 +lemma rbt_interwk_is_rbt [simp]:
   3.989 +  "\<lbrakk> rbt_sorted t1; rbt_sorted t2 \<rbrakk> \<Longrightarrow> is_rbt (rbt_inter_with_key f t1 t2)"
   3.990 +by(auto simp add: rbt_inter_with_key_def Let_def map_map_filter split_def o_def option_map_comp map_filter_option_map_const sorted_filter[where f=id, simplified] rbt_sorted_entries distinct_entries intro: is_rbt_rbtreeify split: compare.split)
   3.991 +
   3.992 +lemma rbt_interw_is_rbt:
   3.993 +  "\<lbrakk> rbt_sorted t1; rbt_sorted t2 \<rbrakk> \<Longrightarrow> is_rbt (rbt_inter_with f t1 t2)"
   3.994 +by(simp add: rbt_inter_with_def)
   3.995 +
   3.996 +lemma rbt_inter_is_rbt:
   3.997 +  "\<lbrakk> rbt_sorted t1; rbt_sorted t2 \<rbrakk> \<Longrightarrow> is_rbt (rbt_inter t1 t2)"
   3.998 +by(simp add: rbt_inter_def)
   3.999 +
  3.1000 +lemma rbt_lookup_rbt_interwk:
  3.1001 +  "\<lbrakk> rbt_sorted t1; rbt_sorted t2 \<rbrakk>
  3.1002 +  \<Longrightarrow> rbt_lookup (rbt_inter_with_key f t1 t2) k =
  3.1003 +  (case rbt_lookup t1 k of None \<Rightarrow> None 
  3.1004 +   | Some v \<Rightarrow> case rbt_lookup t2 k of None \<Rightarrow> None
  3.1005 +               | Some w \<Rightarrow> Some (f k v w))"
  3.1006 +by(auto 4 3 simp add: rbt_inter_with_key_def Let_def map_of_entries[symmetric] rbt_lookup_rbtreeify map_map_filter split_def o_def option_map_comp map_filter_option_map_const sorted_filter[where f=id, simplified] rbt_sorted_entries distinct_entries map_of_sinter_with map_of_eq_None_iff set_map_filter split: option.split compare.split intro: rev_image_eqI dest: rbt_sorted_entries_right_unique)
  3.1007 +
  3.1008 +lemma rbt_lookup_rbt_inter:
  3.1009 +  "\<lbrakk> rbt_sorted t1; rbt_sorted t2 \<rbrakk>
  3.1010 +  \<Longrightarrow> rbt_lookup (rbt_inter t1 t2) = rbt_lookup t2 |` dom (rbt_lookup t1)"
  3.1011 +by(auto simp add: rbt_inter_def rbt_lookup_rbt_interwk restrict_map_def split: option.split)
  3.1012 +
  3.1013 +end
  3.1014 +
  3.1015 +
  3.1016  subsection {* Code generator setup *}
  3.1017  
  3.1018  lemmas [code] =
  3.1019 @@ -1213,9 +2015,14 @@
  3.1020    ord.rbt_del_from_right.simps
  3.1021    ord.rbt_del.simps
  3.1022    ord.rbt_delete_def
  3.1023 -  ord.rbt_union_with_key.simps
  3.1024 +  ord.sunion_with.simps
  3.1025 +  ord.sinter_with.simps
  3.1026 +  ord.rbt_union_with_key_def
  3.1027    ord.rbt_union_with_def
  3.1028    ord.rbt_union_def
  3.1029 +  ord.rbt_inter_with_key_def
  3.1030 +  ord.rbt_inter_with_def
  3.1031 +  ord.rbt_inter_def
  3.1032    ord.rbt_map_entry.simps
  3.1033    ord.rbt_bulkload_def
  3.1034  
  3.1035 @@ -1224,7 +2031,7 @@
  3.1036  definition gen_entries :: 
  3.1037    "(('a \<times> 'b) \<times> ('a, 'b) rbt) list \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a \<times> 'b) list"
  3.1038  where
  3.1039 -  "gen_entries kvts t = entries t @ concat (List.map (\<lambda>(kv, t). kv # entries t) kvts)"
  3.1040 +  "gen_entries kvts t = entries t @ concat (map (\<lambda>(kv, t). kv # entries t) kvts)"
  3.1041  
  3.1042  lemma gen_entries_simps [simp, code]:
  3.1043    "gen_entries [] Empty = []"
  3.1044 @@ -1272,6 +2079,6 @@
  3.1045       (@{const_name rbt_bulkload}, SOME @{typ "('a \<times> 'b) list \<Rightarrow> ('a\<Colon>linorder,'b) rbt"})]
  3.1046  *}
  3.1047  
  3.1048 -hide_const (open) R B Empty entries keys map fold gen_keys gen_entries
  3.1049 +hide_const (open) R B Empty entries keys fold gen_keys gen_entries
  3.1050  
  3.1051  end