src/HOL/Library/RBT_Impl.thy
changeset 49770 cf6a78acf445
parent 49480 4632b867fba7
child 49807 9a0843995fd3
     1.1 --- a/src/HOL/Library/RBT_Impl.thy	Tue Oct 09 17:33:46 2012 +0200
     1.2 +++ b/src/HOL/Library/RBT_Impl.thy	Wed Oct 10 13:03:50 2012 +0200
     1.3 @@ -113,13 +113,13 @@
     1.4  context linorder begin
     1.5  
     1.6  lemma rbt_sorted_entries:
     1.7 -  "rbt_sorted t \<Longrightarrow> List.sorted (List.map fst (entries t))"
     1.8 +  "rbt_sorted t \<Longrightarrow> List.sorted (map fst (entries t))"
     1.9  by (induct t) 
    1.10    (force simp: sorted_append sorted_Cons rbt_ord_props 
    1.11        dest!: entry_in_tree_keys)+
    1.12  
    1.13  lemma distinct_entries:
    1.14 -  "rbt_sorted t \<Longrightarrow> distinct (List.map fst (entries t))"
    1.15 +  "rbt_sorted t \<Longrightarrow> distinct (map fst (entries t))"
    1.16  by (induct t) 
    1.17    (force simp: sorted_append sorted_Cons rbt_ord_props 
    1.18        dest!: entry_in_tree_keys)+
    1.19 @@ -998,89 +998,6 @@
    1.20  
    1.21  end
    1.22  
    1.23 -subsection {* Union *}
    1.24 -
    1.25 -context ord begin
    1.26 -
    1.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"
    1.28 -where
    1.29 -  "rbt_union_with_key f t Empty = t"
    1.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"
    1.31 -
    1.32 -definition rbt_union_with where
    1.33 -  "rbt_union_with f = rbt_union_with_key (\<lambda>_. f)"
    1.34 -
    1.35 -definition rbt_union where
    1.36 -  "rbt_union = rbt_union_with_key (%_ _ rv. rv)"
    1.37 -
    1.38 -end
    1.39 -
    1.40 -context linorder begin
    1.41 -
    1.42 -lemma rbt_unionwk_rbt_sorted: "rbt_sorted lt \<Longrightarrow> rbt_sorted (rbt_union_with_key f lt rt)" 
    1.43 -  by (induct rt arbitrary: lt) (auto simp: rbt_insertwk_rbt_sorted)
    1.44 -theorem rbt_unionwk_is_rbt[simp]: "is_rbt lt \<Longrightarrow> is_rbt (rbt_union_with_key f lt rt)" 
    1.45 -  by (induct rt arbitrary: lt) (simp add: rbt_insertwk_is_rbt)+
    1.46 -
    1.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
    1.48 -
    1.49 -theorem rbt_union_is_rbt: "is_rbt lt \<Longrightarrow> is_rbt (rbt_union lt rt)" unfolding rbt_union_def by simp
    1.50 -
    1.51 -lemma (in ord) rbt_union_Branch[simp]:
    1.52 -  "rbt_union t (Branch c lt k v rt) = rbt_union (rbt_union (rbt_insert k v t) lt) rt"
    1.53 -  unfolding rbt_union_def rbt_insert_def
    1.54 -  by simp
    1.55 -
    1.56 -lemma rbt_lookup_rbt_union:
    1.57 -  assumes "is_rbt s" "rbt_sorted t"
    1.58 -  shows "rbt_lookup (rbt_union s t) = rbt_lookup s ++ rbt_lookup t"
    1.59 -using assms
    1.60 -proof (induct t arbitrary: s)
    1.61 -  case Empty thus ?case by (auto simp: rbt_union_def)
    1.62 -next
    1.63 -  case (Branch c l k v r s)
    1.64 -  then have "rbt_sorted r" "rbt_sorted l" "l |\<guillemotleft> k" "k \<guillemotleft>| r" by auto
    1.65 -
    1.66 -  have meq: "rbt_lookup s(k \<mapsto> v) ++ rbt_lookup l ++ rbt_lookup r =
    1.67 -    rbt_lookup s ++
    1.68 -    (\<lambda>a. if a < k then rbt_lookup l a
    1.69 -    else if k < a then rbt_lookup r a else Some v)" (is "?m1 = ?m2")
    1.70 -  proof (rule ext)
    1.71 -    fix a
    1.72 -
    1.73 -   have "k < a \<or> k = a \<or> k > a" by auto
    1.74 -    thus "?m1 a = ?m2 a"
    1.75 -    proof (elim disjE)
    1.76 -      assume "k < a"
    1.77 -      with `l |\<guillemotleft> k` have "l |\<guillemotleft> a" by (rule rbt_less_trans)
    1.78 -      with `k < a` show ?thesis
    1.79 -        by (auto simp: map_add_def split: option.splits)
    1.80 -    next
    1.81 -      assume "k = a"
    1.82 -      with `l |\<guillemotleft> k` `k \<guillemotleft>| r` 
    1.83 -      show ?thesis by (auto simp: map_add_def)
    1.84 -    next
    1.85 -      assume "a < k"
    1.86 -      from this `k \<guillemotleft>| r` have "a \<guillemotleft>| r" by (rule rbt_greater_trans)
    1.87 -      with `a < k` show ?thesis
    1.88 -        by (auto simp: map_add_def split: option.splits)
    1.89 -    qed
    1.90 -  qed
    1.91 -
    1.92 -  from Branch have is_rbt: "is_rbt (rbt_union (rbt_insert k v s) l)"
    1.93 -    by (auto intro: rbt_union_is_rbt rbt_insert_is_rbt)
    1.94 -  with Branch have IHs:
    1.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"
    1.96 -    "rbt_lookup (rbt_union (rbt_insert k v s) l) = rbt_lookup (rbt_insert k v s) ++ rbt_lookup l"
    1.97 -    by auto
    1.98 -  
    1.99 -  with meq show ?case
   1.100 -    by (auto simp: rbt_lookup_rbt_insert[OF Branch(3)])
   1.101 -
   1.102 -qed
   1.103 -
   1.104 -end
   1.105 -
   1.106  subsection {* Modifying existing entries *}
   1.107  
   1.108  context ord begin
   1.109 @@ -1146,16 +1063,23 @@
   1.110   (* FIXME: simproc "antisym less" does not work for linorder context, only for linorder type class
   1.111      by (induct t) auto *)
   1.112  
   1.113 +hide_const (open) map
   1.114 +
   1.115  subsection {* Folding over entries *}
   1.116  
   1.117  definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c" where
   1.118    "fold f t = List.fold (prod_case f) (entries t)"
   1.119  
   1.120 -lemma fold_simps [simp, code]:
   1.121 +lemma fold_simps [simp]:
   1.122    "fold f Empty = id"
   1.123    "fold f (Branch c lt k v rt) = fold f rt \<circ> f k v \<circ> fold f lt"
   1.124    by (simp_all add: fold_def fun_eq_iff)
   1.125  
   1.126 +lemma fold_code [code]:
   1.127 +  "fold f Empty c = c"
   1.128 +  "fold f (Branch c lt k v rt) c = fold f rt (f k v (fold f lt c))"
   1.129 +by(simp_all)
   1.130 +
   1.131  (* fold with continuation predicate *)
   1.132  
   1.133  fun foldi :: "('c \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a :: linorder, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c" 
   1.134 @@ -1197,6 +1121,884 @@
   1.135  
   1.136  end
   1.137  
   1.138 +
   1.139 +
   1.140 +subsection {* Building a RBT from a sorted list *}
   1.141 +
   1.142 +text {* 
   1.143 +  These functions have been adapted from 
   1.144 +  Andrew W. Appel, Efficient Verified Red-Black Trees (September 2011) 
   1.145 +*}
   1.146 +
   1.147 +fun rbtreeify_f :: "nat \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('a, 'b) rbt \<times> ('a \<times> 'b) list"
   1.148 +  and rbtreeify_g :: "nat \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('a, 'b) rbt \<times> ('a \<times> 'b) list"
   1.149 +where
   1.150 +  "rbtreeify_f n kvs =
   1.151 +   (if n = 0 then (Empty, kvs)
   1.152 +    else if n = 1 then
   1.153 +      case kvs of (k, v) # kvs' \<Rightarrow> (Branch R Empty k v Empty, kvs')
   1.154 +    else if (n mod 2 = 0) then
   1.155 +      case rbtreeify_f (n div 2) kvs of (t1, (k, v) # kvs') \<Rightarrow>
   1.156 +        apfst (Branch B t1 k v) (rbtreeify_g (n div 2) kvs')
   1.157 +    else case rbtreeify_f (n div 2) kvs of (t1, (k, v) # kvs') \<Rightarrow>
   1.158 +        apfst (Branch B t1 k v) (rbtreeify_f (n div 2) kvs'))"
   1.159 +
   1.160 +| "rbtreeify_g n kvs =
   1.161 +   (if n = 0 \<or> n = 1 then (Empty, kvs)
   1.162 +    else if n mod 2 = 0 then
   1.163 +      case rbtreeify_g (n div 2) kvs of (t1, (k, v) # kvs') \<Rightarrow>
   1.164 +        apfst (Branch B t1 k v) (rbtreeify_g (n div 2) kvs')
   1.165 +    else case rbtreeify_f (n div 2) kvs of (t1, (k, v) # kvs') \<Rightarrow>
   1.166 +        apfst (Branch B t1 k v) (rbtreeify_g (n div 2) kvs'))"
   1.167 +
   1.168 +definition rbtreeify :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) rbt"
   1.169 +where "rbtreeify kvs = fst (rbtreeify_g (Suc (length kvs)) kvs)"
   1.170 +
   1.171 +declare rbtreeify_f.simps [simp del] rbtreeify_g.simps [simp del]
   1.172 +
   1.173 +lemma rbtreeify_f_code [code]:
   1.174 +  "rbtreeify_f n kvs =
   1.175 +   (if n = 0 then (Empty, kvs)
   1.176 +    else if n = 1 then
   1.177 +      case kvs of (k, v) # kvs' \<Rightarrow> 
   1.178 +        (Branch R Empty k v Empty, kvs')
   1.179 +    else let (n', r) = divmod_nat n 2 in
   1.180 +      if r = 0 then
   1.181 +        case rbtreeify_f n' kvs of (t1, (k, v) # kvs') \<Rightarrow>
   1.182 +          apfst (Branch B t1 k v) (rbtreeify_g n' kvs')
   1.183 +      else case rbtreeify_f n' kvs of (t1, (k, v) # kvs') \<Rightarrow>
   1.184 +          apfst (Branch B t1 k v) (rbtreeify_f n' kvs'))"
   1.185 +by(subst rbtreeify_f.simps)(simp only: Let_def divmod_nat_div_mod prod.simps)
   1.186 +
   1.187 +lemma rbtreeify_g_code [code]:
   1.188 +  "rbtreeify_g n kvs =
   1.189 +   (if n = 0 \<or> n = 1 then (Empty, kvs)
   1.190 +    else let (n', r) = divmod_nat n 2 in
   1.191 +      if r = 0 then
   1.192 +        case rbtreeify_g n' kvs of (t1, (k, v) # kvs') \<Rightarrow>
   1.193 +          apfst (Branch B t1 k v) (rbtreeify_g n' kvs')
   1.194 +      else case rbtreeify_f n' kvs of (t1, (k, v) # kvs') \<Rightarrow>
   1.195 +          apfst (Branch B t1 k v) (rbtreeify_g n' kvs'))"
   1.196 +by(subst rbtreeify_g.simps)(simp only: Let_def divmod_nat_div_mod prod.simps)
   1.197 +
   1.198 +lemma Suc_double_half: "Suc (2 * n) div 2 = n"
   1.199 +by simp
   1.200 +
   1.201 +lemma div2_plus_div2: "n div 2 + n div 2 = (n :: nat) - n mod 2"
   1.202 +by arith
   1.203 +
   1.204 +lemma rbtreeify_f_rec_aux_lemma:
   1.205 +  "\<lbrakk>k - n div 2 = Suc k'; n \<le> k; n mod 2 = Suc 0\<rbrakk>
   1.206 +  \<Longrightarrow> k' - n div 2 = k - n"
   1.207 +apply(rule add_right_imp_eq[where a = "n - n div 2"])
   1.208 +apply(subst add_diff_assoc2, arith)
   1.209 +apply(simp add: div2_plus_div2)
   1.210 +done
   1.211 +
   1.212 +lemma rbtreeify_f_simps:
   1.213 +  "rbtreeify_f 0 kvs = (RBT_Impl.Empty, kvs)"
   1.214 +  "rbtreeify_f (Suc 0) ((k, v) # kvs) = 
   1.215 +  (Branch R Empty k v Empty, kvs)"
   1.216 +  "0 < n \<Longrightarrow> rbtreeify_f (2 * n) kvs =
   1.217 +   (case rbtreeify_f n kvs of (t1, (k, v) # kvs') \<Rightarrow>
   1.218 +     apfst (Branch B t1 k v) (rbtreeify_g n kvs'))"
   1.219 +  "0 < n \<Longrightarrow> rbtreeify_f (Suc (2 * n)) kvs =
   1.220 +   (case rbtreeify_f n kvs of (t1, (k, v) # kvs') \<Rightarrow> 
   1.221 +     apfst (Branch B t1 k v) (rbtreeify_f n kvs'))"
   1.222 +by(subst (1) rbtreeify_f.simps, simp add: Suc_double_half)+
   1.223 +
   1.224 +lemma rbtreeify_g_simps:
   1.225 +  "rbtreeify_g 0 kvs = (Empty, kvs)"
   1.226 +  "rbtreeify_g (Suc 0) kvs = (Empty, kvs)"
   1.227 +  "0 < n \<Longrightarrow> rbtreeify_g (2 * n) kvs =
   1.228 +   (case rbtreeify_g n kvs of (t1, (k, v) # kvs') \<Rightarrow> 
   1.229 +     apfst (Branch B t1 k v) (rbtreeify_g n kvs'))"
   1.230 +  "0 < n \<Longrightarrow> rbtreeify_g (Suc (2 * n)) kvs =
   1.231 +   (case rbtreeify_f n kvs of (t1, (k, v) # kvs') \<Rightarrow> 
   1.232 +     apfst (Branch B t1 k v) (rbtreeify_g n kvs'))"
   1.233 +by(subst (1) rbtreeify_g.simps, simp add: Suc_double_half)+
   1.234 +
   1.235 +declare rbtreeify_f_simps[simp] rbtreeify_g_simps[simp]
   1.236 +
   1.237 +lemma length_rbtreeify_f: "n \<le> length kvs
   1.238 +  \<Longrightarrow> length (snd (rbtreeify_f n kvs)) = length kvs - n"
   1.239 +  and length_rbtreeify_g:"\<lbrakk> 0 < n; n \<le> Suc (length kvs) \<rbrakk>
   1.240 +  \<Longrightarrow> length (snd (rbtreeify_g n kvs)) = Suc (length kvs) - n"
   1.241 +proof(induction n kvs and n kvs rule: rbtreeify_f_rbtreeify_g.induct)
   1.242 +  case (1 n kvs)
   1.243 +  show ?case
   1.244 +  proof(cases "n \<le> 1")
   1.245 +    case True thus ?thesis using "1.prems"
   1.246 +      by(cases n kvs rule: nat.exhaust[case_product list.exhaust]) auto
   1.247 +  next
   1.248 +    case False
   1.249 +    hence "n \<noteq> 0" "n \<noteq> 1" by simp_all
   1.250 +    note IH = "1.IH"[OF this]
   1.251 +    show ?thesis
   1.252 +    proof(cases "n mod 2 = 0")
   1.253 +      case True
   1.254 +      hence "length (snd (rbtreeify_f n kvs)) = 
   1.255 +        length (snd (rbtreeify_f (2 * (n div 2)) kvs))"
   1.256 +        by(metis minus_nat.diff_0 mult_div_cancel)
   1.257 +      also from "1.prems" False obtain k v kvs' 
   1.258 +        where kvs: "kvs = (k, v) # kvs'" by(cases kvs) auto
   1.259 +      also have "0 < n div 2" using False by(simp) 
   1.260 +      note rbtreeify_f_simps(3)[OF this]
   1.261 +      also note kvs[symmetric] 
   1.262 +      also let ?rest1 = "snd (rbtreeify_f (n div 2) kvs)"
   1.263 +      from "1.prems" have "n div 2 \<le> length kvs" by simp
   1.264 +      with True have len: "length ?rest1 = length kvs - n div 2" by(rule IH)
   1.265 +      with "1.prems" False obtain t1 k' v' kvs''
   1.266 +        where kvs'': "rbtreeify_f (n div 2) kvs = (t1, (k', v') # kvs'')"
   1.267 +         by(cases ?rest1)(auto simp add: snd_def split: prod.split_asm)
   1.268 +      note this also note prod.simps(2) also note list.simps(5) 
   1.269 +      also note prod.simps(2) also note snd_apfst
   1.270 +      also have "0 < n div 2" "n div 2 \<le> Suc (length kvs'')" 
   1.271 +        using len "1.prems" False unfolding kvs'' by simp_all
   1.272 +      with True kvs''[symmetric] refl refl
   1.273 +      have "length (snd (rbtreeify_g (n div 2) kvs'')) = 
   1.274 +        Suc (length kvs'') - n div 2" by(rule IH)
   1.275 +      finally show ?thesis using len[unfolded kvs''] "1.prems" True
   1.276 +        by(simp add: Suc_diff_le[symmetric] mult_2[symmetric] mult_div_cancel)
   1.277 +    next
   1.278 +      case False
   1.279 +      hence "length (snd (rbtreeify_f n kvs)) = 
   1.280 +        length (snd (rbtreeify_f (Suc (2 * (n div 2))) kvs))"
   1.281 +        by(metis Suc_eq_plus1_left comm_semiring_1_class.normalizing_semiring_rules(7)
   1.282 +             mod_2_not_eq_zero_eq_one_nat semiring_div_class.mod_div_equality')
   1.283 +      also from "1.prems" `\<not> n \<le> 1` obtain k v kvs' 
   1.284 +        where kvs: "kvs = (k, v) # kvs'" by(cases kvs) auto
   1.285 +      also have "0 < n div 2" using `\<not> n \<le> 1` by(simp) 
   1.286 +      note rbtreeify_f_simps(4)[OF this]
   1.287 +      also note kvs[symmetric] 
   1.288 +      also let ?rest1 = "snd (rbtreeify_f (n div 2) kvs)"
   1.289 +      from "1.prems" have "n div 2 \<le> length kvs" by simp
   1.290 +      with False have len: "length ?rest1 = length kvs - n div 2" by(rule IH)
   1.291 +      with "1.prems" `\<not> n \<le> 1` obtain t1 k' v' kvs''
   1.292 +        where kvs'': "rbtreeify_f (n div 2) kvs = (t1, (k', v') # kvs'')"
   1.293 +        by(cases ?rest1)(auto simp add: snd_def split: prod.split_asm)
   1.294 +      note this also note prod.simps(2) also note list.simps(5) 
   1.295 +      also note prod.simps(2) also note snd_apfst
   1.296 +      also have "n div 2 \<le> length kvs''" 
   1.297 +        using len "1.prems" False unfolding kvs'' by simp arith
   1.298 +      with False kvs''[symmetric] refl refl
   1.299 +      have "length (snd (rbtreeify_f (n div 2) kvs'')) = length kvs'' - n div 2"
   1.300 +        by(rule IH)
   1.301 +      finally show ?thesis using len[unfolded kvs''] "1.prems" False
   1.302 +        by simp(rule rbtreeify_f_rec_aux_lemma[OF sym])
   1.303 +    qed
   1.304 +  qed
   1.305 +next
   1.306 +  case (2 n kvs)
   1.307 +  show ?case
   1.308 +  proof(cases "n > 1")
   1.309 +    case False with `0 < n` show ?thesis
   1.310 +      by(cases n kvs rule: nat.exhaust[case_product list.exhaust]) simp_all
   1.311 +  next
   1.312 +    case True
   1.313 +    hence "\<not> (n = 0 \<or> n = 1)" by simp
   1.314 +    note IH = "2.IH"[OF this]
   1.315 +    show ?thesis
   1.316 +    proof(cases "n mod 2 = 0")
   1.317 +      case True
   1.318 +      hence "length (snd (rbtreeify_g n kvs)) =
   1.319 +        length (snd (rbtreeify_g (2 * (n div 2)) kvs))"
   1.320 +        by(metis minus_nat.diff_0 mult_div_cancel)
   1.321 +      also from "2.prems" True obtain k v kvs' 
   1.322 +        where kvs: "kvs = (k, v) # kvs'" by(cases kvs) auto
   1.323 +      also have "0 < n div 2" using `1 < n` by(simp) 
   1.324 +      note rbtreeify_g_simps(3)[OF this]
   1.325 +      also note kvs[symmetric] 
   1.326 +      also let ?rest1 = "snd (rbtreeify_g (n div 2) kvs)"
   1.327 +      from "2.prems" `1 < n`
   1.328 +      have "0 < n div 2" "n div 2 \<le> Suc (length kvs)" by simp_all
   1.329 +      with True have len: "length ?rest1 = Suc (length kvs) - n div 2" by(rule IH)
   1.330 +      with "2.prems" obtain t1 k' v' kvs''
   1.331 +        where kvs'': "rbtreeify_g (n div 2) kvs = (t1, (k', v') # kvs'')"
   1.332 +        by(cases ?rest1)(auto simp add: snd_def split: prod.split_asm)
   1.333 +      note this also note prod.simps(2) also note list.simps(5) 
   1.334 +      also note prod.simps(2) also note snd_apfst
   1.335 +      also have "n div 2 \<le> Suc (length kvs'')" 
   1.336 +        using len "2.prems" unfolding kvs'' by simp
   1.337 +      with True kvs''[symmetric] refl refl `0 < n div 2`
   1.338 +      have "length (snd (rbtreeify_g (n div 2) kvs'')) = Suc (length kvs'') - n div 2"
   1.339 +        by(rule IH)
   1.340 +      finally show ?thesis using len[unfolded kvs''] "2.prems" True
   1.341 +        by(simp add: Suc_diff_le[symmetric] mult_2[symmetric] mult_div_cancel)
   1.342 +    next
   1.343 +      case False
   1.344 +      hence "length (snd (rbtreeify_g n kvs)) = 
   1.345 +        length (snd (rbtreeify_g (Suc (2 * (n div 2))) kvs))"
   1.346 +        by(metis Suc_eq_plus1_left comm_semiring_1_class.normalizing_semiring_rules(7) 
   1.347 +            mod_2_not_eq_zero_eq_one_nat semiring_div_class.mod_div_equality')
   1.348 +      also from "2.prems" `1 < n` obtain k v kvs'
   1.349 +        where kvs: "kvs = (k, v) # kvs'" by(cases kvs) auto
   1.350 +      also have "0 < n div 2" using `1 < n` by(simp)
   1.351 +      note rbtreeify_g_simps(4)[OF this]
   1.352 +      also note kvs[symmetric] 
   1.353 +      also let ?rest1 = "snd (rbtreeify_f (n div 2) kvs)"
   1.354 +      from "2.prems" have "n div 2 \<le> length kvs" by simp
   1.355 +      with False have len: "length ?rest1 = length kvs - n div 2" by(rule IH)
   1.356 +      with "2.prems" `1 < n` False obtain t1 k' v' kvs'' 
   1.357 +        where kvs'': "rbtreeify_f (n div 2) kvs = (t1, (k', v') # kvs'')"
   1.358 +        by(cases ?rest1)(auto simp add: snd_def split: prod.split_asm, arith)
   1.359 +      note this also note prod.simps(2) also note list.simps(5) 
   1.360 +      also note prod.simps(2) also note snd_apfst
   1.361 +      also have "n div 2 \<le> Suc (length kvs'')" 
   1.362 +        using len "2.prems" False unfolding kvs'' by simp arith
   1.363 +      with False kvs''[symmetric] refl refl `0 < n div 2`
   1.364 +      have "length (snd (rbtreeify_g (n div 2) kvs'')) = Suc (length kvs'') - n div 2"
   1.365 +        by(rule IH)
   1.366 +      finally show ?thesis using len[unfolded kvs''] "2.prems" False
   1.367 +        by(simp add: div2_plus_div2)
   1.368 +    qed
   1.369 +  qed
   1.370 +qed
   1.371 +
   1.372 +lemma rbtreeify_induct [consumes 1, case_names f_0 f_1 f_even f_odd g_0 g_1 g_even g_odd]:
   1.373 +  fixes P Q
   1.374 +  defines "f0 == (\<And>kvs. P 0 kvs)"
   1.375 +  and "f1 == (\<And>k v kvs. P (Suc 0) ((k, v) # kvs))"
   1.376 +  and "feven ==
   1.377 +    (\<And>n kvs t k v kvs'. \<lbrakk> n > 0; n \<le> length kvs; P n kvs; 
   1.378 +       rbtreeify_f n kvs = (t, (k, v) # kvs'); n \<le> Suc (length kvs'); Q n kvs' \<rbrakk> 
   1.379 +     \<Longrightarrow> P (2 * n) kvs)"
   1.380 +  and "fodd == 
   1.381 +    (\<And>n kvs t k v kvs'. \<lbrakk> n > 0; n \<le> length kvs; P n kvs;
   1.382 +       rbtreeify_f n kvs = (t, (k, v) # kvs'); n \<le> length kvs'; P n kvs' \<rbrakk> 
   1.383 +    \<Longrightarrow> P (Suc (2 * n)) kvs)"
   1.384 +  and "g0 == (\<And>kvs. Q 0 kvs)"
   1.385 +  and "g1 == (\<And>kvs. Q (Suc 0) kvs)"
   1.386 +  and "geven == 
   1.387 +    (\<And>n kvs t k v kvs'. \<lbrakk> n > 0; n \<le> Suc (length kvs); Q n kvs; 
   1.388 +       rbtreeify_g n kvs = (t, (k, v) # kvs'); n \<le> Suc (length kvs'); Q n kvs' \<rbrakk>
   1.389 +    \<Longrightarrow> Q (2 * n) kvs)"
   1.390 +  and "godd == 
   1.391 +    (\<And>n kvs t k v kvs'. \<lbrakk> n > 0; n \<le> length kvs; P n kvs;
   1.392 +       rbtreeify_f n kvs = (t, (k, v) # kvs'); n \<le> Suc (length kvs'); Q n kvs' \<rbrakk>
   1.393 +    \<Longrightarrow> Q (Suc (2 * n)) kvs)"
   1.394 +  shows "\<lbrakk> n \<le> length kvs; 
   1.395 +           PROP f0; PROP f1; PROP feven; PROP fodd; 
   1.396 +           PROP g0; PROP g1; PROP geven; PROP godd \<rbrakk>
   1.397 +         \<Longrightarrow> P n kvs"
   1.398 +  and "\<lbrakk> n \<le> Suc (length kvs);
   1.399 +          PROP f0; PROP f1; PROP feven; PROP fodd; 
   1.400 +          PROP g0; PROP g1; PROP geven; PROP godd \<rbrakk>
   1.401 +       \<Longrightarrow> Q n kvs"
   1.402 +proof -
   1.403 +  assume f0: "PROP f0" and f1: "PROP f1" and feven: "PROP feven" and fodd: "PROP fodd"
   1.404 +    and g0: "PROP g0" and g1: "PROP g1" and geven: "PROP geven" and godd: "PROP godd"
   1.405 +  show "n \<le> length kvs \<Longrightarrow> P n kvs" and "n \<le> Suc (length kvs) \<Longrightarrow> Q n kvs"
   1.406 +  proof(induction rule: rbtreeify_f_rbtreeify_g.induct)
   1.407 +    case (1 n kvs)
   1.408 +    show ?case
   1.409 +    proof(cases "n \<le> 1")
   1.410 +      case True thus ?thesis using "1.prems"
   1.411 +        by(cases n kvs rule: nat.exhaust[case_product list.exhaust])
   1.412 +          (auto simp add: f0[unfolded f0_def] f1[unfolded f1_def])
   1.413 +    next
   1.414 +      case False 
   1.415 +      hence ns: "n \<noteq> 0" "n \<noteq> 1" by simp_all
   1.416 +      hence ge0: "n div 2 > 0" by simp
   1.417 +      note IH = "1.IH"[OF ns]
   1.418 +      show ?thesis
   1.419 +      proof(cases "n mod 2 = 0")
   1.420 +        case True note ge0 
   1.421 +        moreover from "1.prems" have n2: "n div 2 \<le> length kvs" by simp
   1.422 +        moreover with True have "P (n div 2) kvs" by(rule IH)
   1.423 +        moreover from length_rbtreeify_f[OF n2] ge0 "1.prems" obtain t k v kvs' 
   1.424 +          where kvs': "rbtreeify_f (n div 2) kvs = (t, (k, v) # kvs')"
   1.425 +          by(cases "snd (rbtreeify_f (n div 2) kvs)")
   1.426 +            (auto simp add: snd_def split: prod.split_asm)
   1.427 +        moreover from "1.prems" length_rbtreeify_f[OF n2] ge0
   1.428 +        have "n div 2 \<le> Suc (length kvs')" by(simp add: kvs')
   1.429 +        moreover with True kvs'[symmetric] refl refl
   1.430 +        have "Q (n div 2) kvs'" by(rule IH)
   1.431 +        moreover note feven[unfolded feven_def]
   1.432 +          (* FIXME: why does by(rule feven[unfolded feven_def]) not work? *)
   1.433 +        ultimately have "P (2 * (n div 2)) kvs" by -
   1.434 +        thus ?thesis using True by (metis div_mod_equality' minus_nat.diff_0 nat_mult_commute)
   1.435 +      next
   1.436 +        case False note ge0
   1.437 +        moreover from "1.prems" have n2: "n div 2 \<le> length kvs" by simp
   1.438 +        moreover with False have "P (n div 2) kvs" by(rule IH)
   1.439 +        moreover from length_rbtreeify_f[OF n2] ge0 "1.prems" obtain t k v kvs' 
   1.440 +          where kvs': "rbtreeify_f (n div 2) kvs = (t, (k, v) # kvs')"
   1.441 +          by(cases "snd (rbtreeify_f (n div 2) kvs)")
   1.442 +            (auto simp add: snd_def split: prod.split_asm)
   1.443 +        moreover from "1.prems" length_rbtreeify_f[OF n2] ge0 False
   1.444 +        have "n div 2 \<le> length kvs'" by(simp add: kvs') arith
   1.445 +        moreover with False kvs'[symmetric] refl refl have "P (n div 2) kvs'" by(rule IH)
   1.446 +        moreover note fodd[unfolded fodd_def]
   1.447 +        ultimately have "P (Suc (2 * (n div 2))) kvs" by -
   1.448 +        thus ?thesis using False 
   1.449 +          by simp (metis One_nat_def Suc_eq_plus1_left le_add_diff_inverse mod_less_eq_dividend mult_div_cancel)
   1.450 +      qed
   1.451 +    qed
   1.452 +  next
   1.453 +    case (2 n kvs)
   1.454 +    show ?case
   1.455 +    proof(cases "n \<le> 1")
   1.456 +      case True thus ?thesis using "2.prems"
   1.457 +        by(cases n kvs rule: nat.exhaust[case_product list.exhaust])
   1.458 +          (auto simp add: g0[unfolded g0_def] g1[unfolded g1_def])
   1.459 +    next
   1.460 +      case False 
   1.461 +      hence ns: "\<not> (n = 0 \<or> n = 1)" by simp
   1.462 +      hence ge0: "n div 2 > 0" by simp
   1.463 +      note IH = "2.IH"[OF ns]
   1.464 +      show ?thesis
   1.465 +      proof(cases "n mod 2 = 0")
   1.466 +        case True note ge0
   1.467 +        moreover from "2.prems" have n2: "n div 2 \<le> Suc (length kvs)" by simp
   1.468 +        moreover with True have "Q (n div 2) kvs" by(rule IH)
   1.469 +        moreover from length_rbtreeify_g[OF ge0 n2] ge0 "2.prems" obtain t k v kvs' 
   1.470 +          where kvs': "rbtreeify_g (n div 2) kvs = (t, (k, v) # kvs')"
   1.471 +          by(cases "snd (rbtreeify_g (n div 2) kvs)")
   1.472 +            (auto simp add: snd_def split: prod.split_asm)
   1.473 +        moreover from "2.prems" length_rbtreeify_g[OF ge0 n2] ge0
   1.474 +        have "n div 2 \<le> Suc (length kvs')" by(simp add: kvs')
   1.475 +        moreover with True kvs'[symmetric] refl refl 
   1.476 +        have "Q (n div 2) kvs'" by(rule IH)
   1.477 +        moreover note geven[unfolded geven_def]
   1.478 +        ultimately have "Q (2 * (n div 2)) kvs" by -
   1.479 +        thus ?thesis using True 
   1.480 +          by(metis div_mod_equality' minus_nat.diff_0 nat_mult_commute)
   1.481 +      next
   1.482 +        case False note ge0
   1.483 +        moreover from "2.prems" have n2: "n div 2 \<le> length kvs" by simp
   1.484 +        moreover with False have "P (n div 2) kvs" by(rule IH)
   1.485 +        moreover from length_rbtreeify_f[OF n2] ge0 "2.prems" False obtain t k v kvs' 
   1.486 +          where kvs': "rbtreeify_f (n div 2) kvs = (t, (k, v) # kvs')"
   1.487 +          by(cases "snd (rbtreeify_f (n div 2) kvs)")
   1.488 +            (auto simp add: snd_def split: prod.split_asm, arith)
   1.489 +        moreover from "2.prems" length_rbtreeify_f[OF n2] ge0 False
   1.490 +        have "n div 2 \<le> Suc (length kvs')" by(simp add: kvs') arith
   1.491 +        moreover with False kvs'[symmetric] refl refl
   1.492 +        have "Q (n div 2) kvs'" by(rule IH)
   1.493 +        moreover note godd[unfolded godd_def]
   1.494 +        ultimately have "Q (Suc (2 * (n div 2))) kvs" by -
   1.495 +        thus ?thesis using False 
   1.496 +          by simp (metis One_nat_def Suc_eq_plus1_left le_add_diff_inverse mod_less_eq_dividend mult_div_cancel)
   1.497 +      qed
   1.498 +    qed
   1.499 +  qed
   1.500 +qed
   1.501 +
   1.502 +lemma inv1_rbtreeify_f: "n \<le> length kvs 
   1.503 +  \<Longrightarrow> inv1 (fst (rbtreeify_f n kvs))"
   1.504 +  and inv1_rbtreeify_g: "n \<le> Suc (length kvs)
   1.505 +  \<Longrightarrow> inv1 (fst (rbtreeify_g n kvs))"
   1.506 +by(induct n kvs and n kvs rule: rbtreeify_induct) simp_all
   1.507 +
   1.508 +fun plog2 :: "nat \<Rightarrow> nat" 
   1.509 +where "plog2 n = (if n \<le> 1 then 0 else plog2 (n div 2) + 1)"
   1.510 +
   1.511 +declare plog2.simps [simp del]
   1.512 +
   1.513 +lemma plog2_simps [simp]:
   1.514 +  "plog2 0 = 0" "plog2 (Suc 0) = 0"
   1.515 +  "0 < n \<Longrightarrow> plog2 (2 * n) = 1 + plog2 n"
   1.516 +  "0 < n \<Longrightarrow> plog2 (Suc (2 * n)) = 1 + plog2 n"
   1.517 +by(subst plog2.simps, simp add: Suc_double_half)+
   1.518 +
   1.519 +lemma bheight_rbtreeify_f: "n \<le> length kvs
   1.520 +  \<Longrightarrow> bheight (fst (rbtreeify_f n kvs)) = plog2 n"
   1.521 +  and bheight_rbtreeify_g: "n \<le> Suc (length kvs)
   1.522 +  \<Longrightarrow> bheight (fst (rbtreeify_g n kvs)) = plog2 n"
   1.523 +by(induct n kvs and n kvs rule: rbtreeify_induct) simp_all
   1.524 +
   1.525 +lemma bheight_rbtreeify_f_eq_plog2I:
   1.526 +  "\<lbrakk> rbtreeify_f n kvs = (t, kvs'); n \<le> length kvs \<rbrakk> 
   1.527 +  \<Longrightarrow> bheight t = plog2 n"
   1.528 +using bheight_rbtreeify_f[of n kvs] by simp
   1.529 +
   1.530 +lemma bheight_rbtreeify_g_eq_plog2I: 
   1.531 +  "\<lbrakk> rbtreeify_g n kvs = (t, kvs'); n \<le> Suc (length kvs) \<rbrakk>
   1.532 +  \<Longrightarrow> bheight t = plog2 n"
   1.533 +using bheight_rbtreeify_g[of n kvs] by simp
   1.534 +
   1.535 +hide_const (open) plog2
   1.536 +
   1.537 +lemma inv2_rbtreeify_f: "n \<le> length kvs
   1.538 +  \<Longrightarrow> inv2 (fst (rbtreeify_f n kvs))"
   1.539 +  and inv2_rbtreeify_g: "n \<le> Suc (length kvs)
   1.540 +  \<Longrightarrow> inv2 (fst (rbtreeify_g n kvs))"
   1.541 +by(induct n kvs and n kvs rule: rbtreeify_induct)
   1.542 +  (auto simp add: bheight_rbtreeify_f bheight_rbtreeify_g 
   1.543 +        intro: bheight_rbtreeify_f_eq_plog2I bheight_rbtreeify_g_eq_plog2I)
   1.544 +
   1.545 +lemma "n \<le> length kvs \<Longrightarrow> True"
   1.546 +  and color_of_rbtreeify_g:
   1.547 +  "\<lbrakk> n \<le> Suc (length kvs); 0 < n \<rbrakk> 
   1.548 +  \<Longrightarrow> color_of (fst (rbtreeify_g n kvs)) = B"
   1.549 +by(induct n kvs and n kvs rule: rbtreeify_induct) simp_all
   1.550 +
   1.551 +lemma entries_rbtreeify_f_append:
   1.552 +  "n \<le> length kvs 
   1.553 +  \<Longrightarrow> entries (fst (rbtreeify_f n kvs)) @ snd (rbtreeify_f n kvs) = kvs"
   1.554 +  and entries_rbtreeify_g_append: 
   1.555 +  "n \<le> Suc (length kvs) 
   1.556 +  \<Longrightarrow> entries (fst (rbtreeify_g n kvs)) @ snd (rbtreeify_g n kvs) = kvs"
   1.557 +by(induction rule: rbtreeify_induct) simp_all
   1.558 +
   1.559 +lemma length_entries_rbtreeify_f:
   1.560 +  "n \<le> length kvs \<Longrightarrow> length (entries (fst (rbtreeify_f n kvs))) = n"
   1.561 +  and length_entries_rbtreeify_g: 
   1.562 +  "n \<le> Suc (length kvs) \<Longrightarrow> length (entries (fst (rbtreeify_g n kvs))) = n - 1"
   1.563 +by(induct rule: rbtreeify_induct) simp_all
   1.564 +
   1.565 +lemma rbtreeify_f_conv_drop: 
   1.566 +  "n \<le> length kvs \<Longrightarrow> snd (rbtreeify_f n kvs) = drop n kvs"
   1.567 +using entries_rbtreeify_f_append[of n kvs]
   1.568 +by(simp add: append_eq_conv_conj length_entries_rbtreeify_f)
   1.569 +
   1.570 +lemma rbtreeify_g_conv_drop: 
   1.571 +  "n \<le> Suc (length kvs) \<Longrightarrow> snd (rbtreeify_g n kvs) = drop (n - 1) kvs"
   1.572 +using entries_rbtreeify_g_append[of n kvs]
   1.573 +by(simp add: append_eq_conv_conj length_entries_rbtreeify_g)
   1.574 +
   1.575 +lemma entries_rbtreeify_f [simp]:
   1.576 +  "n \<le> length kvs \<Longrightarrow> entries (fst (rbtreeify_f n kvs)) = take n kvs"
   1.577 +using entries_rbtreeify_f_append[of n kvs]
   1.578 +by(simp add: append_eq_conv_conj length_entries_rbtreeify_f)
   1.579 +
   1.580 +lemma entries_rbtreeify_g [simp]:
   1.581 +  "n \<le> Suc (length kvs) \<Longrightarrow> 
   1.582 +  entries (fst (rbtreeify_g n kvs)) = take (n - 1) kvs"
   1.583 +using entries_rbtreeify_g_append[of n kvs]
   1.584 +by(simp add: append_eq_conv_conj length_entries_rbtreeify_g)
   1.585 +
   1.586 +lemma keys_rbtreeify_f [simp]: "n \<le> length kvs
   1.587 +  \<Longrightarrow> keys (fst (rbtreeify_f n kvs)) = take n (map fst kvs)"
   1.588 +by(simp add: keys_def take_map)
   1.589 +
   1.590 +lemma keys_rbtreeify_g [simp]: "n \<le> Suc (length kvs)
   1.591 +  \<Longrightarrow> keys (fst (rbtreeify_g n kvs)) = take (n - 1) (map fst kvs)"
   1.592 +by(simp add: keys_def take_map)
   1.593 +
   1.594 +lemma rbtreeify_fD: 
   1.595 +  "\<lbrakk> rbtreeify_f n kvs = (t, kvs'); n \<le> length kvs \<rbrakk> 
   1.596 +  \<Longrightarrow> entries t = take n kvs \<and> kvs' = drop n kvs"
   1.597 +using rbtreeify_f_conv_drop[of n kvs] entries_rbtreeify_f[of n kvs] by simp
   1.598 +
   1.599 +lemma rbtreeify_gD: 
   1.600 +  "\<lbrakk> rbtreeify_g n kvs = (t, kvs'); n \<le> Suc (length kvs) \<rbrakk>
   1.601 +  \<Longrightarrow> entries t = take (n - 1) kvs \<and> kvs' = drop (n - 1) kvs"
   1.602 +using rbtreeify_g_conv_drop[of n kvs] entries_rbtreeify_g[of n kvs] by simp
   1.603 +
   1.604 +lemma entries_rbtreeify [simp]: "entries (rbtreeify kvs) = kvs"
   1.605 +by(simp add: rbtreeify_def entries_rbtreeify_g)
   1.606 +
   1.607 +context linorder begin
   1.608 +
   1.609 +lemma rbt_sorted_rbtreeify_f: 
   1.610 +  "\<lbrakk> n \<le> length kvs; sorted (map fst kvs); distinct (map fst kvs) \<rbrakk> 
   1.611 +  \<Longrightarrow> rbt_sorted (fst (rbtreeify_f n kvs))"
   1.612 +  and rbt_sorted_rbtreeify_g: 
   1.613 +  "\<lbrakk> n \<le> Suc (length kvs); sorted (map fst kvs); distinct (map fst kvs) \<rbrakk>
   1.614 +  \<Longrightarrow> rbt_sorted (fst (rbtreeify_g n kvs))"
   1.615 +proof(induction n kvs and n kvs rule: rbtreeify_induct)
   1.616 +  case (f_even n kvs t k v kvs')
   1.617 +  from rbtreeify_fD[OF `rbtreeify_f n kvs = (t, (k, v) # kvs')` `n \<le> length kvs`]
   1.618 +  have "entries t = take n kvs"
   1.619 +    and kvs': "drop n kvs = (k, v) # kvs'" by simp_all
   1.620 +  hence unfold: "kvs = take n kvs @ (k, v) # kvs'" by(metis append_take_drop_id)
   1.621 +  from `sorted (map fst kvs)` kvs'
   1.622 +  have "(\<forall>(x, y) \<in> set (take n kvs). x \<le> k) \<and> (\<forall>(x, y) \<in> set kvs'. k \<le> x)"
   1.623 +    by(subst (asm) unfold)(auto simp add: sorted_append sorted_Cons)
   1.624 +  moreover from `distinct (map fst kvs)` kvs'
   1.625 +  have "(\<forall>(x, y) \<in> set (take n kvs). x \<noteq> k) \<and> (\<forall>(x, y) \<in> set kvs'. x \<noteq> k)"
   1.626 +    by(subst (asm) unfold)(auto intro: rev_image_eqI)
   1.627 +  ultimately have "(\<forall>(x, y) \<in> set (take n kvs). x < k) \<and> (\<forall>(x, y) \<in> set kvs'. k < x)"
   1.628 +    by fastforce
   1.629 +  hence "fst (rbtreeify_f n kvs) |\<guillemotleft> k" "k \<guillemotleft>| fst (rbtreeify_g n kvs')"
   1.630 +    using `n \<le> Suc (length kvs')` `n \<le> length kvs` set_take_subset[of "n - 1" kvs']
   1.631 +    by(auto simp add: ord.rbt_greater_prop ord.rbt_less_prop take_map split_def)
   1.632 +  moreover from `sorted (map fst kvs)` `distinct (map fst kvs)`
   1.633 +  have "rbt_sorted (fst (rbtreeify_f n kvs))" by(rule f_even.IH)
   1.634 +  moreover have "sorted (map fst kvs')" "distinct (map fst kvs')"
   1.635 +    using `sorted (map fst kvs)` `distinct (map fst kvs)`
   1.636 +    by(subst (asm) (1 2) unfold, simp add: sorted_append sorted_Cons)+
   1.637 +  hence "rbt_sorted (fst (rbtreeify_g n kvs'))" by(rule f_even.IH)
   1.638 +  ultimately show ?case
   1.639 +    using `0 < n` `rbtreeify_f n kvs = (t, (k, v) # kvs')` by simp
   1.640 +next
   1.641 +  case (f_odd n kvs t k v kvs')
   1.642 +  from rbtreeify_fD[OF `rbtreeify_f n kvs = (t, (k, v) # kvs')` `n \<le> length kvs`]
   1.643 +  have "entries t = take n kvs" 
   1.644 +    and kvs': "drop n kvs = (k, v) # kvs'" by simp_all
   1.645 +  hence unfold: "kvs = take n kvs @ (k, v) # kvs'" by(metis append_take_drop_id)
   1.646 +  from `sorted (map fst kvs)` kvs'
   1.647 +  have "(\<forall>(x, y) \<in> set (take n kvs). x \<le> k) \<and> (\<forall>(x, y) \<in> set kvs'. k \<le> x)"
   1.648 +    by(subst (asm) unfold)(auto simp add: sorted_append sorted_Cons)
   1.649 +  moreover from `distinct (map fst kvs)` kvs'
   1.650 +  have "(\<forall>(x, y) \<in> set (take n kvs). x \<noteq> k) \<and> (\<forall>(x, y) \<in> set kvs'. x \<noteq> k)"
   1.651 +    by(subst (asm) unfold)(auto intro: rev_image_eqI)
   1.652 +  ultimately have "(\<forall>(x, y) \<in> set (take n kvs). x < k) \<and> (\<forall>(x, y) \<in> set kvs'. k < x)"
   1.653 +    by fastforce
   1.654 +  hence "fst (rbtreeify_f n kvs) |\<guillemotleft> k" "k \<guillemotleft>| fst (rbtreeify_f n kvs')"
   1.655 +    using `n \<le> length kvs'` `n \<le> length kvs` set_take_subset[of n kvs']
   1.656 +    by(auto simp add: rbt_greater_prop rbt_less_prop take_map split_def)
   1.657 +  moreover from `sorted (map fst kvs)` `distinct (map fst kvs)`
   1.658 +  have "rbt_sorted (fst (rbtreeify_f n kvs))" by(rule f_odd.IH)
   1.659 +  moreover have "sorted (map fst kvs')" "distinct (map fst kvs')"
   1.660 +    using `sorted (map fst kvs)` `distinct (map fst kvs)`
   1.661 +    by(subst (asm) (1 2) unfold, simp add: sorted_append sorted_Cons)+
   1.662 +  hence "rbt_sorted (fst (rbtreeify_f n kvs'))" by(rule f_odd.IH)
   1.663 +  ultimately show ?case 
   1.664 +    using `0 < n` `rbtreeify_f n kvs = (t, (k, v) # kvs')` by simp
   1.665 +next
   1.666 +  case (g_even n kvs t k v kvs')
   1.667 +  from rbtreeify_gD[OF `rbtreeify_g n kvs = (t, (k, v) # kvs')` `n \<le> Suc (length kvs)`]
   1.668 +  have t: "entries t = take (n - 1) kvs" 
   1.669 +    and kvs': "drop (n - 1) kvs = (k, v) # kvs'" by simp_all
   1.670 +  hence unfold: "kvs = take (n - 1) kvs @ (k, v) # kvs'" by(metis append_take_drop_id)
   1.671 +  from `sorted (map fst kvs)` kvs'
   1.672 +  have "(\<forall>(x, y) \<in> set (take (n - 1) kvs). x \<le> k) \<and> (\<forall>(x, y) \<in> set kvs'. k \<le> x)"
   1.673 +    by(subst (asm) unfold)(auto simp add: sorted_append sorted_Cons)
   1.674 +  moreover from `distinct (map fst kvs)` kvs'
   1.675 +  have "(\<forall>(x, y) \<in> set (take (n - 1) kvs). x \<noteq> k) \<and> (\<forall>(x, y) \<in> set kvs'. x \<noteq> k)"
   1.676 +    by(subst (asm) unfold)(auto intro: rev_image_eqI)
   1.677 +  ultimately have "(\<forall>(x, y) \<in> set (take (n - 1) kvs). x < k) \<and> (\<forall>(x, y) \<in> set kvs'. k < x)"
   1.678 +    by fastforce
   1.679 +  hence "fst (rbtreeify_g n kvs) |\<guillemotleft> k" "k \<guillemotleft>| fst (rbtreeify_g n kvs')"
   1.680 +    using `n \<le> Suc (length kvs')` `n \<le> Suc (length kvs)` set_take_subset[of "n - 1" kvs']
   1.681 +    by(auto simp add: rbt_greater_prop rbt_less_prop take_map split_def)
   1.682 +  moreover from `sorted (map fst kvs)` `distinct (map fst kvs)`
   1.683 +  have "rbt_sorted (fst (rbtreeify_g n kvs))" by(rule g_even.IH)
   1.684 +  moreover have "sorted (map fst kvs')" "distinct (map fst kvs')"
   1.685 +    using `sorted (map fst kvs)` `distinct (map fst kvs)`
   1.686 +    by(subst (asm) (1 2) unfold, simp add: sorted_append sorted_Cons)+
   1.687 +  hence "rbt_sorted (fst (rbtreeify_g n kvs'))" by(rule g_even.IH)
   1.688 +  ultimately show ?case using `0 < n` `rbtreeify_g n kvs = (t, (k, v) # kvs')` by simp
   1.689 +next
   1.690 +  case (g_odd n kvs t k v kvs')
   1.691 +  from rbtreeify_fD[OF `rbtreeify_f n kvs = (t, (k, v) # kvs')` `n \<le> length kvs`]
   1.692 +  have "entries t = take n kvs"
   1.693 +    and kvs': "drop n kvs = (k, v) # kvs'" by simp_all
   1.694 +  hence unfold: "kvs = take n kvs @ (k, v) # kvs'" by(metis append_take_drop_id)
   1.695 +  from `sorted (map fst kvs)` kvs'
   1.696 +  have "(\<forall>(x, y) \<in> set (take n kvs). x \<le> k) \<and> (\<forall>(x, y) \<in> set kvs'. k \<le> x)"
   1.697 +    by(subst (asm) unfold)(auto simp add: sorted_append sorted_Cons)
   1.698 +  moreover from `distinct (map fst kvs)` kvs'
   1.699 +  have "(\<forall>(x, y) \<in> set (take n kvs). x \<noteq> k) \<and> (\<forall>(x, y) \<in> set kvs'. x \<noteq> k)"
   1.700 +    by(subst (asm) unfold)(auto intro: rev_image_eqI)
   1.701 +  ultimately have "(\<forall>(x, y) \<in> set (take n kvs). x < k) \<and> (\<forall>(x, y) \<in> set kvs'. k < x)"
   1.702 +    by fastforce
   1.703 +  hence "fst (rbtreeify_f n kvs) |\<guillemotleft> k" "k \<guillemotleft>| fst (rbtreeify_g n kvs')"
   1.704 +    using `n \<le> Suc (length kvs')` `n \<le> length kvs` set_take_subset[of "n - 1" kvs']
   1.705 +    by(auto simp add: rbt_greater_prop rbt_less_prop take_map split_def)
   1.706 +  moreover from `sorted (map fst kvs)` `distinct (map fst kvs)`
   1.707 +  have "rbt_sorted (fst (rbtreeify_f n kvs))" by(rule g_odd.IH)
   1.708 +  moreover have "sorted (map fst kvs')" "distinct (map fst kvs')"
   1.709 +    using `sorted (map fst kvs)` `distinct (map fst kvs)`
   1.710 +    by(subst (asm) (1 2) unfold, simp add: sorted_append sorted_Cons)+
   1.711 +  hence "rbt_sorted (fst (rbtreeify_g n kvs'))" by(rule g_odd.IH)
   1.712 +  ultimately show ?case
   1.713 +    using `0 < n` `rbtreeify_f n kvs = (t, (k, v) # kvs')` by simp
   1.714 +qed simp_all
   1.715 +
   1.716 +lemma rbt_sorted_rbtreeify: 
   1.717 +  "\<lbrakk> sorted (map fst kvs); distinct (map fst kvs) \<rbrakk> \<Longrightarrow> rbt_sorted (rbtreeify kvs)"
   1.718 +by(simp add: rbtreeify_def rbt_sorted_rbtreeify_g)
   1.719 +
   1.720 +lemma is_rbt_rbtreeify: 
   1.721 +  "\<lbrakk> sorted (map fst kvs); distinct (map fst kvs) \<rbrakk>
   1.722 +  \<Longrightarrow> is_rbt (rbtreeify kvs)"
   1.723 +by(simp add: is_rbt_def rbtreeify_def inv1_rbtreeify_g inv2_rbtreeify_g rbt_sorted_rbtreeify_g color_of_rbtreeify_g)
   1.724 +
   1.725 +lemma rbt_lookup_rbtreeify:
   1.726 +  "\<lbrakk> sorted (map fst kvs); distinct (map fst kvs) \<rbrakk> \<Longrightarrow> 
   1.727 +  rbt_lookup (rbtreeify kvs) = map_of kvs"
   1.728 +by(simp add: map_of_entries[symmetric] rbt_sorted_rbtreeify)
   1.729 +
   1.730 +end
   1.731 +
   1.732 +text {* 
   1.733 +  Functions to compare the height of two rbt trees, taken from 
   1.734 +  Andrew W. Appel, Efficient Verified Red-Black Trees (September 2011)
   1.735 +*}
   1.736 +
   1.737 +fun skip_red :: "('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
   1.738 +where
   1.739 +  "skip_red (Branch color.R l k v r) = l"
   1.740 +| "skip_red t = t"
   1.741 +
   1.742 +fun skip_black :: "('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
   1.743 +where
   1.744 +  "skip_black (Branch color.B l k v r) = l"
   1.745 +| "skip_black t = t"
   1.746 +
   1.747 +datatype compare = LT | GT | EQ
   1.748 +
   1.749 +partial_function (tailrec) compare_height :: "('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt \<Rightarrow> compare"
   1.750 +where
   1.751 +  "compare_height sx s t tx =
   1.752 +  (case (skip_red sx, skip_red s, skip_red t, skip_red tx) of
   1.753 +     (Branch _ sx' _ _ _, Branch _ s' _ _ _, Branch _ t' _ _ _, Branch _ tx' _ _ _) \<Rightarrow> 
   1.754 +       compare_height (skip_black sx') s' t' (skip_black tx')
   1.755 +   | (_, rbt.Empty, _, Branch _ _ _ _ _) \<Rightarrow> LT
   1.756 +   | (Branch _ _ _ _ _, _, rbt.Empty, _) \<Rightarrow> GT
   1.757 +   | (Branch _ sx' _ _ _, Branch _ s' _ _ _, Branch _ t' _ _ _, rbt.Empty) \<Rightarrow>
   1.758 +       compare_height (skip_black sx') s' t' rbt.Empty
   1.759 +   | (rbt.Empty, Branch _ s' _ _ _, Branch _ t' _ _ _, Branch _ tx' _ _ _) \<Rightarrow>
   1.760 +       compare_height rbt.Empty s' t' (skip_black tx')
   1.761 +   | _ \<Rightarrow> EQ)"
   1.762 +
   1.763 +declare compare_height.simps [code]
   1.764 +
   1.765 +hide_type (open) compare
   1.766 +hide_const (open)
   1.767 +  compare_height skip_black skip_red LT GT EQ compare_case compare_rec 
   1.768 +  Abs_compare Rep_compare compare_rep_set
   1.769 +hide_fact (open)
   1.770 +  Abs_compare_cases Abs_compare_induct Abs_compare_inject Abs_compare_inverse
   1.771 +  Rep_compare Rep_compare_cases Rep_compare_induct Rep_compare_inject Rep_compare_inverse
   1.772 +  compare.simps compare.exhaust compare.induct compare.recs compare.simps
   1.773 +  compare.size compare.case_cong compare.weak_case_cong compare.cases 
   1.774 +  compare.nchotomy compare.split compare.split_asm compare_rec_def
   1.775 +  compare.eq.refl compare.eq.simps
   1.776 +  compare.EQ_def compare.GT_def compare.LT_def
   1.777 +  equal_compare_def
   1.778 +  skip_red_def skip_red.simps skip_red.induct 
   1.779 +  skip_black_def skip_black.simps skip_black.induct
   1.780 +  compare_height.simps
   1.781 +
   1.782 +subsection {* union and intersection of sorted associative lists *}
   1.783 +
   1.784 +context ord begin
   1.785 +
   1.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" 
   1.787 +where
   1.788 +  "sunion_with f ((k, v) # as) ((k', v') # bs) =
   1.789 +   (if k > k' then (k', v') # sunion_with f ((k, v) # as) bs
   1.790 +    else if k < k' then (k, v) # sunion_with f as ((k', v') # bs)
   1.791 +    else (k, f k v v') # sunion_with f as bs)"
   1.792 +| "sunion_with f [] bs = bs"
   1.793 +| "sunion_with f as [] = as"
   1.794 +by pat_completeness auto
   1.795 +termination by lexicographic_order
   1.796 +
   1.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"
   1.798 +where
   1.799 +  "sinter_with f ((k, v) # as) ((k', v') # bs) =
   1.800 +  (if k > k' then sinter_with f ((k, v) # as) bs
   1.801 +   else if k < k' then sinter_with f as ((k', v') # bs)
   1.802 +   else (k, f k v v') # sinter_with f as bs)"
   1.803 +| "sinter_with f [] _ = []"
   1.804 +| "sinter_with f _ [] = []"
   1.805 +by pat_completeness auto
   1.806 +termination by lexicographic_order
   1.807 +
   1.808 +end
   1.809 +
   1.810 +declare ord.sunion_with.simps [code] ord.sinter_with.simps[code]
   1.811 +
   1.812 +context linorder begin
   1.813 +
   1.814 +lemma set_fst_sunion_with: 
   1.815 +  "set (map fst (sunion_with f xs ys)) = set (map fst xs) \<union> set (map fst ys)"
   1.816 +by(induct f xs ys rule: sunion_with.induct) auto
   1.817 +
   1.818 +lemma sorted_sunion_with [simp]:
   1.819 +  "\<lbrakk> sorted (map fst xs); sorted (map fst ys) \<rbrakk> 
   1.820 +  \<Longrightarrow> sorted (map fst (sunion_with f xs ys))"
   1.821 +by(induct f xs ys rule: sunion_with.induct)
   1.822 +  (auto simp add: sorted_Cons set_fst_sunion_with simp del: set_map)
   1.823 +
   1.824 +lemma distinct_sunion_with [simp]:
   1.825 +  "\<lbrakk> distinct (map fst xs); distinct (map fst ys); sorted (map fst xs); sorted (map fst ys) \<rbrakk>
   1.826 +  \<Longrightarrow> distinct (map fst (sunion_with f xs ys))"
   1.827 +proof(induct f xs ys rule: sunion_with.induct)
   1.828 +  case (1 f k v xs k' v' ys)
   1.829 +  have "\<lbrakk> \<not> k < k'; \<not> k' < k \<rbrakk> \<Longrightarrow> k = k'" by simp
   1.830 +  thus ?case using "1"
   1.831 +    by(auto simp add: set_fst_sunion_with sorted_Cons simp del: set_map)
   1.832 +qed simp_all
   1.833 +
   1.834 +lemma map_of_sunion_with: 
   1.835 +  "\<lbrakk> sorted (map fst xs); sorted (map fst ys) \<rbrakk>
   1.836 +  \<Longrightarrow> map_of (sunion_with f xs ys) k = 
   1.837 +  (case map_of xs k of None \<Rightarrow> map_of ys k 
   1.838 +  | Some v \<Rightarrow> case map_of ys k of None \<Rightarrow> Some v 
   1.839 +              | Some w \<Rightarrow> Some (f k v w))"
   1.840 +by(induct f xs ys rule: sunion_with.induct)(auto simp add: sorted_Cons split: option.split dest: map_of_SomeD bspec)
   1.841 +
   1.842 +lemma set_fst_sinter_with [simp]:
   1.843 +  "\<lbrakk> sorted (map fst xs); sorted (map fst ys) \<rbrakk>
   1.844 +  \<Longrightarrow> set (map fst (sinter_with f xs ys)) = set (map fst xs) \<inter> set (map fst ys)"
   1.845 +by(induct f xs ys rule: sinter_with.induct)(auto simp add: sorted_Cons simp del: set_map)
   1.846 +
   1.847 +lemma set_fst_sinter_with_subset1:
   1.848 +  "set (map fst (sinter_with f xs ys)) \<subseteq> set (map fst xs)"
   1.849 +by(induct f xs ys rule: sinter_with.induct) auto
   1.850 +
   1.851 +lemma set_fst_sinter_with_subset2:
   1.852 +  "set (map fst (sinter_with f xs ys)) \<subseteq> set (map fst ys)"
   1.853 +by(induct f xs ys rule: sinter_with.induct)(auto simp del: set_map)
   1.854 +
   1.855 +lemma sorted_sinter_with [simp]:
   1.856 +  "\<lbrakk> sorted (map fst xs); sorted (map fst ys) \<rbrakk>
   1.857 +  \<Longrightarrow> sorted (map fst (sinter_with f xs ys))"
   1.858 +by(induct f xs ys rule: sinter_with.induct)(auto simp add: sorted_Cons simp del: set_map)
   1.859 +
   1.860 +lemma distinct_sinter_with [simp]:
   1.861 +  "\<lbrakk> distinct (map fst xs); distinct (map fst ys) \<rbrakk>
   1.862 +  \<Longrightarrow> distinct (map fst (sinter_with f xs ys))"
   1.863 +proof(induct f xs ys rule: sinter_with.induct)
   1.864 +  case (1 f k v as k' v' bs)
   1.865 +  have "\<lbrakk> \<not> k < k'; \<not> k' < k \<rbrakk> \<Longrightarrow> k = k'" by simp
   1.866 +  thus ?case using "1" set_fst_sinter_with_subset1[of f as bs]
   1.867 +    set_fst_sinter_with_subset2[of f as bs]
   1.868 +    by(auto simp del: set_map)
   1.869 +qed simp_all
   1.870 +
   1.871 +lemma map_of_sinter_with:
   1.872 +  "\<lbrakk> sorted (map fst xs); sorted (map fst ys) \<rbrakk>
   1.873 +  \<Longrightarrow> map_of (sinter_with f xs ys) k = 
   1.874 +  (case map_of xs k of None \<Rightarrow> None | Some v \<Rightarrow> Option.map (f k v) (map_of ys k))"
   1.875 +apply(induct f xs ys rule: sinter_with.induct)
   1.876 +apply(auto simp add: sorted_Cons Option.map_def split: option.splits dest: map_of_SomeD bspec)
   1.877 +done
   1.878 +
   1.879 +end
   1.880 +
   1.881 +lemma distinct_map_of_rev: "distinct (map fst xs) \<Longrightarrow> map_of (rev xs) = map_of xs"
   1.882 +by(induct xs)(auto 4 3 simp add: map_add_def intro!: ext split: option.split intro: rev_image_eqI)
   1.883 +
   1.884 +lemma map_map_filter: 
   1.885 +  "map f (List.map_filter g xs) = List.map_filter (Option.map f \<circ> g) xs"
   1.886 +by(auto simp add: List.map_filter_def)
   1.887 +
   1.888 +lemma map_filter_option_map_const: 
   1.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)"
   1.890 +by(auto simp add: map_filter_def filter_map o_def)
   1.891 +
   1.892 +lemma set_map_filter: "set (List.map_filter P xs) = the ` (P ` set xs - {None})"
   1.893 +by(auto simp add: List.map_filter_def intro: rev_image_eqI)
   1.894 +
   1.895 +context ord begin
   1.896 +
   1.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"
   1.898 +where
   1.899 +  "rbt_union_with_key f t1 t2 =
   1.900 +  (case RBT_Impl.compare_height t1 t1 t2 t2
   1.901 +   of compare.EQ \<Rightarrow> rbtreeify (sunion_with f (entries t1) (entries t2))
   1.902 +    | compare.LT \<Rightarrow> fold (rbt_insert_with_key (\<lambda>k v w. f k w v)) t1 t2
   1.903 +    | compare.GT \<Rightarrow> fold (rbt_insert_with_key f) t2 t1)"
   1.904 +
   1.905 +definition rbt_union_with where
   1.906 +  "rbt_union_with f = rbt_union_with_key (\<lambda>_. f)"
   1.907 +
   1.908 +definition rbt_union where
   1.909 +  "rbt_union = rbt_union_with_key (%_ _ rv. rv)"
   1.910 +
   1.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"
   1.912 +where
   1.913 +  "rbt_inter_with_key f t1 t2 =
   1.914 +  (case RBT_Impl.compare_height t1 t1 t2 t2 
   1.915 +   of compare.EQ \<Rightarrow> rbtreeify (sinter_with f (entries t1) (entries t2))
   1.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))
   1.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)))"
   1.918 +
   1.919 +definition rbt_inter_with where
   1.920 +  "rbt_inter_with f = rbt_inter_with_key (\<lambda>_. f)"
   1.921 +
   1.922 +definition rbt_inter where
   1.923 +  "rbt_inter = rbt_inter_with_key (\<lambda>_ _ rv. rv)"
   1.924 +
   1.925 +end
   1.926 +
   1.927 +context linorder begin
   1.928 +
   1.929 +lemma rbt_sorted_entries_right_unique:
   1.930 +  "\<lbrakk> (k, v) \<in> set (entries t); (k, v') \<in> set (entries t); 
   1.931 +     rbt_sorted t \<rbrakk> \<Longrightarrow> v = v'"
   1.932 +by(auto dest!: distinct_entries inj_onD[where x="(k, v)" and y="(k, v')"] simp add: distinct_map)
   1.933 +
   1.934 +lemma rbt_sorted_fold_rbt_insertwk:
   1.935 +  "rbt_sorted t \<Longrightarrow> rbt_sorted (List.fold (\<lambda>(k, v). rbt_insert_with_key f k v) xs t)"
   1.936 +by(induct xs rule: rev_induct)(auto simp add: rbt_insertwk_rbt_sorted)
   1.937 +
   1.938 +lemma is_rbt_fold_rbt_insertwk:
   1.939 +  assumes "is_rbt t1"
   1.940 +  shows "is_rbt (fold (rbt_insert_with_key f) t2 t1)"
   1.941 +proof -
   1.942 +  def xs \<equiv> "entries t2"
   1.943 +  from assms show ?thesis unfolding fold_def xs_def[symmetric]
   1.944 +    by(induct xs rule: rev_induct)(auto simp add: rbt_insertwk_is_rbt)
   1.945 +qed
   1.946 +
   1.947 +lemma rbt_lookup_fold_rbt_insertwk:
   1.948 +  assumes t1: "rbt_sorted t1" and t2: "rbt_sorted t2"
   1.949 +  shows "rbt_lookup (fold (rbt_insert_with_key f) t1 t2) k =
   1.950 +  (case rbt_lookup t1 k of None \<Rightarrow> rbt_lookup t2 k
   1.951 +   | Some v \<Rightarrow> case rbt_lookup t2 k of None \<Rightarrow> Some v
   1.952 +               | Some w \<Rightarrow> Some (f k w v))"
   1.953 +proof -
   1.954 +  def xs \<equiv> "entries t1"
   1.955 +  hence dt1: "distinct (map fst xs)" using t1 by(simp add: distinct_entries)
   1.956 +  with t2 show ?thesis
   1.957 +    unfolding fold_def map_of_entries[OF t1, symmetric]
   1.958 +      xs_def[symmetric] distinct_map_of_rev[OF dt1, symmetric]
   1.959 +    apply(induct xs rule: rev_induct)
   1.960 +    apply(auto simp add: rbt_lookup_rbt_insertwk rbt_sorted_fold_rbt_insertwk split: option.splits)
   1.961 +    apply(auto simp add: distinct_map_of_rev intro: rev_image_eqI)
   1.962 +    done
   1.963 +qed
   1.964 +
   1.965 +lemma is_rbt_rbt_unionwk [simp]:
   1.966 +  "\<lbrakk> is_rbt t1; is_rbt t2 \<rbrakk> \<Longrightarrow> is_rbt (rbt_union_with_key f t1 t2)"
   1.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)
   1.968 +
   1.969 +lemma rbt_lookup_rbt_unionwk:
   1.970 +  "\<lbrakk> rbt_sorted t1; rbt_sorted t2 \<rbrakk> 
   1.971 +  \<Longrightarrow> rbt_lookup (rbt_union_with_key f t1 t2) k = 
   1.972 +  (case rbt_lookup t1 k of None \<Rightarrow> rbt_lookup t2 k 
   1.973 +   | Some v \<Rightarrow> case rbt_lookup t2 k of None \<Rightarrow> Some v 
   1.974 +              | Some w \<Rightarrow> Some (f k v w))"
   1.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)
   1.976 +
   1.977 +lemma rbt_unionw_is_rbt: "\<lbrakk> is_rbt lt; is_rbt rt \<rbrakk> \<Longrightarrow> is_rbt (rbt_union_with f lt rt)"
   1.978 +by(simp add: rbt_union_with_def)
   1.979 +
   1.980 +lemma rbt_union_is_rbt: "\<lbrakk> is_rbt lt; is_rbt rt \<rbrakk> \<Longrightarrow> is_rbt (rbt_union lt rt)"
   1.981 +by(simp add: rbt_union_def)
   1.982 +
   1.983 +lemma rbt_lookup_rbt_union:
   1.984 +  "\<lbrakk> rbt_sorted s; rbt_sorted t \<rbrakk> \<Longrightarrow>
   1.985 +  rbt_lookup (rbt_union s t) = rbt_lookup s ++ rbt_lookup t"
   1.986 +by(rule ext)(simp add: rbt_lookup_rbt_unionwk rbt_union_def map_add_def split: option.split)
   1.987 +
   1.988 +lemma rbt_interwk_is_rbt [simp]:
   1.989 +  "\<lbrakk> rbt_sorted t1; rbt_sorted t2 \<rbrakk> \<Longrightarrow> is_rbt (rbt_inter_with_key f t1 t2)"
   1.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)
   1.991 +
   1.992 +lemma rbt_interw_is_rbt:
   1.993 +  "\<lbrakk> rbt_sorted t1; rbt_sorted t2 \<rbrakk> \<Longrightarrow> is_rbt (rbt_inter_with f t1 t2)"
   1.994 +by(simp add: rbt_inter_with_def)
   1.995 +
   1.996 +lemma rbt_inter_is_rbt:
   1.997 +  "\<lbrakk> rbt_sorted t1; rbt_sorted t2 \<rbrakk> \<Longrightarrow> is_rbt (rbt_inter t1 t2)"
   1.998 +by(simp add: rbt_inter_def)
   1.999 +
  1.1000 +lemma rbt_lookup_rbt_interwk:
  1.1001 +  "\<lbrakk> rbt_sorted t1; rbt_sorted t2 \<rbrakk>
  1.1002 +  \<Longrightarrow> rbt_lookup (rbt_inter_with_key f t1 t2) k =
  1.1003 +  (case rbt_lookup t1 k of None \<Rightarrow> None 
  1.1004 +   | Some v \<Rightarrow> case rbt_lookup t2 k of None \<Rightarrow> None
  1.1005 +               | Some w \<Rightarrow> Some (f k v w))"
  1.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)
  1.1007 +
  1.1008 +lemma rbt_lookup_rbt_inter:
  1.1009 +  "\<lbrakk> rbt_sorted t1; rbt_sorted t2 \<rbrakk>
  1.1010 +  \<Longrightarrow> rbt_lookup (rbt_inter t1 t2) = rbt_lookup t2 |` dom (rbt_lookup t1)"
  1.1011 +by(auto simp add: rbt_inter_def rbt_lookup_rbt_interwk restrict_map_def split: option.split)
  1.1012 +
  1.1013 +end
  1.1014 +
  1.1015 +
  1.1016  subsection {* Code generator setup *}
  1.1017  
  1.1018  lemmas [code] =
  1.1019 @@ -1213,9 +2015,14 @@
  1.1020    ord.rbt_del_from_right.simps
  1.1021    ord.rbt_del.simps
  1.1022    ord.rbt_delete_def
  1.1023 -  ord.rbt_union_with_key.simps
  1.1024 +  ord.sunion_with.simps
  1.1025 +  ord.sinter_with.simps
  1.1026 +  ord.rbt_union_with_key_def
  1.1027    ord.rbt_union_with_def
  1.1028    ord.rbt_union_def
  1.1029 +  ord.rbt_inter_with_key_def
  1.1030 +  ord.rbt_inter_with_def
  1.1031 +  ord.rbt_inter_def
  1.1032    ord.rbt_map_entry.simps
  1.1033    ord.rbt_bulkload_def
  1.1034  
  1.1035 @@ -1224,7 +2031,7 @@
  1.1036  definition gen_entries :: 
  1.1037    "(('a \<times> 'b) \<times> ('a, 'b) rbt) list \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a \<times> 'b) list"
  1.1038  where
  1.1039 -  "gen_entries kvts t = entries t @ concat (List.map (\<lambda>(kv, t). kv # entries t) kvts)"
  1.1040 +  "gen_entries kvts t = entries t @ concat (map (\<lambda>(kv, t). kv # entries t) kvts)"
  1.1041  
  1.1042  lemma gen_entries_simps [simp, code]:
  1.1043    "gen_entries [] Empty = []"
  1.1044 @@ -1272,6 +2079,6 @@
  1.1045       (@{const_name rbt_bulkload}, SOME @{typ "('a \<times> 'b) list \<Rightarrow> ('a\<Colon>linorder,'b) rbt"})]
  1.1046  *}
  1.1047  
  1.1048 -hide_const (open) R B Empty entries keys map fold gen_keys gen_entries
  1.1049 +hide_const (open) R B Empty entries keys fold gen_keys gen_entries
  1.1050  
  1.1051  end