diff --git a/thys/Containers/AssocList.thy b/thys/Containers/AssocList.thy
--- a/thys/Containers/AssocList.thy
+++ b/thys/Containers/AssocList.thy
@@ -1,159 +1,191 @@
 (*  Title:      Containers/AssocList.thy
     Author:     Andreas Lochbihler, KIT *)
 
 theory AssocList imports
   "HOL-Library.DAList" 
 begin
 
 section \<open>Additional operations for associative lists\<close>
 
 subsection \<open>Operations on the raw type\<close>
 
 primrec update_with_aux :: "'val \<Rightarrow> 'key \<Rightarrow> ('val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
 where
   "update_with_aux v k f [] = [(k, f v)]"
 | "update_with_aux v k f (p # ps) = (if (fst p = k) then (k, f (snd p)) # ps else p # update_with_aux v k f ps)"
 
 text \<open>
   Do not use @{term "AList.delete"} because this traverses all the list even if it has found the key.
   We do not have to keep going because we use the invariant that keys are distinct.
 \<close>
 fun delete_aux :: "'key \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
 where
   "delete_aux k [] = []"
 | "delete_aux k ((k', v) # xs) = (if k = k' then xs else (k', v) # delete_aux k xs)"
 
+definition zip_with_index_from :: "nat \<Rightarrow> 'a list \<Rightarrow> (nat \<times> 'a) list" where
+  "zip_with_index_from n xs = zip [n..<n + length xs] xs"
+
+abbreviation zip_with_index :: "'a list \<Rightarrow> (nat \<times> 'a) list" where
+  "zip_with_index \<equiv> zip_with_index_from 0"
+
 lemma update_conv_update_with_aux:
   "AList.update k v xs = update_with_aux v k (\<lambda>_. v) xs"
 by(induct xs) simp_all
 
 lemma map_of_update_with_aux':
   "map_of (update_with_aux v k f ps) k' = ((map_of ps)(k \<mapsto> (case map_of ps k of None \<Rightarrow> f v | Some v \<Rightarrow> f v))) k'"
 by(induct ps) auto
 
 lemma map_of_update_with_aux:
   "map_of (update_with_aux v k f ps) = (map_of ps)(k \<mapsto> (case map_of ps k of None \<Rightarrow> f v | Some v \<Rightarrow> f v))"
 by(simp add: fun_eq_iff map_of_update_with_aux')
 
 lemma dom_update_with_aux: "fst ` set (update_with_aux v k f ps) = {k} \<union> fst ` set ps"
   by (induct ps) auto
 
 lemma distinct_update_with_aux [simp]:
   "distinct (map fst (update_with_aux v k f ps)) = distinct (map fst ps)"
 by(induct ps)(auto simp add: dom_update_with_aux)
 
 lemma set_update_with_aux:
   "distinct (map fst xs) 
   \<Longrightarrow> set (update_with_aux v k f xs) = (set xs - {k} \<times> UNIV \<union> {(k, f (case map_of xs k of None \<Rightarrow> v | Some v \<Rightarrow> v))})"
 by(induct xs)(auto intro: rev_image_eqI)
 
 lemma set_delete_aux: "distinct (map fst xs) \<Longrightarrow> set (delete_aux k xs) = set xs - {k} \<times> UNIV"
 apply(induct xs)
 apply simp_all
 apply clarsimp
 apply(fastforce intro: rev_image_eqI)
 done
 
 lemma dom_delete_aux: "distinct (map fst ps) \<Longrightarrow> fst ` set (delete_aux k ps) = fst ` set ps - {k}"
 by(auto simp add: set_delete_aux)
 
 lemma distinct_delete_aux [simp]:
   "distinct (map fst ps) \<Longrightarrow> distinct (map fst (delete_aux k ps))"
 proof(induct ps)
   case Nil thus ?case by simp
 next
   case (Cons a ps)
   obtain k' v where a: "a = (k', v)" by(cases a)
   show ?case
   proof(cases "k' = k")
     case True with Cons a show ?thesis by simp
   next
     case False
     with Cons a have "k' \<notin> fst ` set ps" "distinct (map fst ps)" by simp_all
     with False a have "k' \<notin> fst ` set (delete_aux k ps)"
       by(auto dest!: dom_delete_aux[where k=k])
     with Cons a show ?thesis by simp
   qed
 qed
 
 lemma map_of_delete_aux':
   "distinct (map fst xs) \<Longrightarrow> map_of (delete_aux k xs) = (map_of xs)(k := None)"
 by(induct xs)(fastforce simp add: map_of_eq_None_iff fun_upd_twist)+
 
 lemma map_of_delete_aux:
   "distinct (map fst xs) \<Longrightarrow> map_of (delete_aux k xs) k' = ((map_of xs)(k := None)) k'"
 by(simp add: map_of_delete_aux')
 
 lemma delete_aux_eq_Nil_conv: "delete_aux k ts = [] \<longleftrightarrow> ts = [] \<or> (\<exists>v. ts = [(k, v)])"
 by(cases ts)(auto split: if_split_asm)
 
+lemma zip_with_index_from_simps [simp, code]:
+  "zip_with_index_from n [] = []"
+  "zip_with_index_from n (x # xs) = (n, x) # zip_with_index_from (Suc n) xs"
+  by(simp_all add: zip_with_index_from_def upt_rec del: upt.upt_Suc)
+
+lemma zip_with_index_from_append [simp]:
+  "zip_with_index_from n (xs @ ys) = zip_with_index_from n xs @ zip_with_index_from (n + length xs) ys"
+  by(simp add: zip_with_index_from_def zip_append[symmetric] upt_add_eq_append[symmetric] del: zip_append)
+    (simp add: add.assoc)
+
+lemma zip_with_index_from_conv_nth:
+  "zip_with_index_from n xs = map (\<lambda>i. (n + i, xs ! i)) [0..<length xs]"
+  by(induction xs rule: rev_induct)(auto simp add: nth_append)
+
+lemma map_of_zip_with_index_from [simp]:
+  "map_of (zip_with_index_from n xs) i = (if i \<ge> n \<and> i < n + length xs then Some (xs ! (i - n)) else None)"
+  by(auto simp add: zip_with_index_from_def set_zip intro: exI[where x="i - n"])
+
+lemma map_of_map': "map_of (map (\<lambda>(k, v). (k, f k v)) xs) x = map_option (f x) (map_of xs x)"
+  by (induct xs)(auto)
+
+
 subsection \<open>Operations on the abstract type @{typ "('a, 'b) alist"}\<close>
 
 lift_definition update_with :: "'v \<Rightarrow> 'k \<Rightarrow> ('v \<Rightarrow> 'v) \<Rightarrow> ('k, 'v) alist \<Rightarrow> ('k, 'v) alist"
   is "update_with_aux" by simp
 
 lift_definition delete :: "'k \<Rightarrow> ('k, 'v) alist \<Rightarrow> ('k, 'v) alist" is "delete_aux"
 by simp
 
 lift_definition keys :: "('k, 'v) alist \<Rightarrow> 'k set" is "set \<circ> map fst" .
 
 lift_definition set :: "('key, 'val) alist \<Rightarrow> ('key \<times> 'val) set"
 is "List.set" .
 
+lift_definition map_values :: "('key \<Rightarrow> 'val \<Rightarrow> 'val') \<Rightarrow> ('key, 'val) alist \<Rightarrow> ('key, 'val') alist" is
+  "\<lambda>f. map (\<lambda>(x,y). (x, f x y))"
+  by(simp add: o_def split_def)
+
 lemma lookup_update_with [simp]: 
   "DAList.lookup (update_with v k f al) = (DAList.lookup al)(k \<mapsto> case DAList.lookup al k of None \<Rightarrow> f v | Some v \<Rightarrow> f v)"
 by transfer(simp add: map_of_update_with_aux)
 
 lemma lookup_delete [simp]: "DAList.lookup (delete k al) = (DAList.lookup al)(k := None)"
 by transfer(simp add: map_of_delete_aux')
 
 lemma finite_dom_lookup [simp, intro!]: "finite (dom (DAList.lookup m))"
 by transfer(simp add: finite_dom_map_of)
 
 lemma update_conv_update_with: "DAList.update k v = update_with v k (\<lambda>_. v)"
 by(rule ext)(transfer, simp add: update_conv_update_with_aux)
 
 lemma lookup_update [simp]: "DAList.lookup (DAList.update k v al) = (DAList.lookup al)(k \<mapsto> v)"
 by(simp add: update_conv_update_with split: option.split)
 
 lemma dom_lookup_keys: "dom (DAList.lookup al) = keys al"
 by transfer(simp add: dom_map_of_conv_image_fst)
 
 lemma keys_empty [simp]: "keys DAList.empty = {}"
 by transfer simp
 
 lemma keys_update_with [simp]: "keys (update_with v k f al) = insert k (keys al)"
 by(simp add: dom_lookup_keys[symmetric])
 
 lemma keys_update [simp]: "keys (DAList.update k v al) = insert k (keys al)"
 by(simp add: update_conv_update_with)
 
 lemma keys_delete [simp]: "keys (delete k al) = keys al - {k}"
 by(simp add: dom_lookup_keys[symmetric])
 
 lemma set_empty [simp]: "set DAList.empty = {}"
 by transfer simp
 
 lemma set_update_with:
   "set (update_with v k f al) = 
   (set al - {k} \<times> UNIV \<union> {(k, f (case DAList.lookup al k of None \<Rightarrow> v | Some v \<Rightarrow> v))})"
 by transfer(simp add: set_update_with_aux)
 
 lemma set_update: "set (DAList.update k v al) = (set al - {k} \<times> UNIV \<union> {(k, v)})"
 by(simp add: update_conv_update_with set_update_with)
 
 lemma set_delete: "set (delete k al) = set al - {k} \<times> UNIV"
 by transfer(simp add: set_delete_aux)
 
 lemma size_dalist_transfer [transfer_rule]:
   includes lifting_syntax
   shows "(pcr_alist (=) (=) ===> (=)) length size"
 unfolding size_alist_def[abs_def]
 by transfer_prover
 
 lemma size_eq_card_dom_lookup: "size al = card (dom (DAList.lookup al))"
 by transfer (metis comp_apply distinct_card dom_map_of_conv_image_fst image_set length_map)
 
 hide_const (open) update_with keys set delete
 
 end
diff --git a/thys/Containers/Mapping_Impl.thy b/thys/Containers/Mapping_Impl.thy
--- a/thys/Containers/Mapping_Impl.thy
+++ b/thys/Containers/Mapping_Impl.thy
@@ -1,252 +1,291 @@
 (*  Title:      Containers/Mapping_Impl.thy
     Author:     Andreas Lochbihler, KIT
                 René Thiemann, UIBK *)
 
 theory Mapping_Impl imports 
   RBT_Mapping2
   AssocList
   "HOL-Library.Mapping"
   Set_Impl
   Containers_Generator
 begin
 
 section \<open>Different implementations of maps\<close>
 
 code_identifier
   code_module Mapping \<rightharpoonup> (SML) Mapping_Impl
 | code_module Mapping_Impl \<rightharpoonup> (SML) Mapping_Impl
 
 subsection \<open>Map implementations\<close>
 
 definition Assoc_List_Mapping :: "('a, 'b) alist \<Rightarrow> ('a, 'b) mapping"
 where [simp]: "Assoc_List_Mapping al = Mapping.Mapping (DAList.lookup al)"
 
 definition RBT_Mapping :: "('a :: ccompare, 'b) mapping_rbt \<Rightarrow> ('a, 'b) mapping"
 where [simp]: "RBT_Mapping t = Mapping.Mapping (RBT_Mapping2.lookup t)"
 
 code_datatype Assoc_List_Mapping RBT_Mapping Mapping
 
 subsection \<open>Map operations\<close>
 
 declare [[code drop: Mapping.lookup]]
 
 lemma lookup_Mapping_code [code]:
   "Mapping.lookup (Assoc_List_Mapping al) = DAList.lookup al"
   "Mapping.lookup (RBT_Mapping t) = RBT_Mapping2.lookup t"
 by(simp_all)(transfer, rule)+
 
 declare [[code drop: Mapping.is_empty]]
 
 lemma is_empty_transfer [transfer_rule]:
   includes lifting_syntax
   shows "(pcr_mapping (=) (=) ===> (=)) (\<lambda>m. m = Map.empty) Mapping.is_empty"
 unfolding mapping.pcr_cr_eq
 apply(rule rel_funI)
 apply(case_tac y)
 apply(simp add: Mapping.is_empty_def cr_mapping_def Mapping_inverse Mapping.keys.rep_eq)
 done
 
 lemma is_empty_Mapping [code]:
   fixes t :: "('a :: ccompare, 'b) mapping_rbt" shows
   "Mapping.is_empty (Assoc_List_Mapping al) \<longleftrightarrow> al = DAList.empty"
   "Mapping.is_empty (RBT_Mapping t) \<longleftrightarrow>
   (case ID CCOMPARE('a) of None \<Rightarrow> Code.abort (STR ''is_empty RBT_Mapping: ccompare = None'') (\<lambda>_. Mapping.is_empty (RBT_Mapping t))
                      | Some _ \<Rightarrow> RBT_Mapping2.is_empty t)"
 apply(simp_all split: option.split)
  apply(transfer, case_tac al, simp_all)
 apply(transfer, simp)
 done
 
 declare [[code drop: Mapping.update]]
 
 lemma update_Mapping [code]:
   fixes t :: "('a :: ccompare, 'b) mapping_rbt" shows
   "Mapping.update k v (Mapping m) = Mapping (m(k \<mapsto> v))"
   "Mapping.update k v (Assoc_List_Mapping al) = Assoc_List_Mapping (DAList.update k v al)"
   "Mapping.update k v (RBT_Mapping t) =
   (case ID CCOMPARE('a) of None \<Rightarrow> Code.abort (STR ''update RBT_Mapping: ccompare = None'') (\<lambda>_. Mapping.update k v (RBT_Mapping t))
                      | Some _ \<Rightarrow> RBT_Mapping (RBT_Mapping2.insert k v t))" (is ?RBT)
 by(simp_all split: option.split)(transfer, simp)+
 
 declare [[code drop: Mapping.delete]]
 
 lemma delete_Mapping [code]:
   fixes t :: "('a :: ccompare, 'b) mapping_rbt" shows
   "Mapping.delete k (Mapping m) = Mapping (m(k := None))"
   "Mapping.delete k (Assoc_List_Mapping al) = Assoc_List_Mapping (AssocList.delete k al)"
   "Mapping.delete k (RBT_Mapping t) = 
   (case ID CCOMPARE('a) of None \<Rightarrow> Code.abort (STR ''delete RBT_Mapping: ccompare = None'') (\<lambda>_. Mapping.delete k (RBT_Mapping t))
                      | Some _ \<Rightarrow> RBT_Mapping (RBT_Mapping2.delete k t))"
 by(simp_all split: option.split)(transfer, simp)+
 
 declare [[code drop: Mapping.keys]]
 
 theorem rbt_comp_lookup_map_const: "rbt_comp_lookup c (RBT_Impl.map (\<lambda>_. f) t) = map_option f \<circ> rbt_comp_lookup c t"
 by(induct t)(auto simp: fun_eq_iff split: order.split)
 
 lemma keys_Mapping [code]:
   fixes t :: "('a :: ccompare, 'b) mapping_rbt" shows
   "Mapping.keys (Mapping m) = Collect (\<lambda>k. m k \<noteq> None)" (is "?Mapping")
   "Mapping.keys (Assoc_List_Mapping al) = AssocList.keys al" (is "?Assoc_List")
   "Mapping.keys (RBT_Mapping t) = RBT_set (RBT_Mapping2.map (\<lambda>_ _. ()) t)" (is "?RBT")
 proof -
   show ?Mapping by transfer auto
   show ?Assoc_List by simp(transfer, auto intro: rev_image_eqI)
   show ?RBT
     by(simp add: RBT_set_def, transfer, auto simp add: rbt_comp_lookup_map_const o_def)
 qed
 
 declare [[code drop: Mapping.size]]
 
 lemma Mapping_size_transfer [transfer_rule]:
   includes lifting_syntax
   shows "(pcr_mapping (=) (=) ===> (=)) (card \<circ> dom) Mapping.size"
 apply(rule rel_funI)
 apply(case_tac y)
 apply(simp add: Mapping.size_def Mapping.keys.rep_eq Mapping_inverse mapping.pcr_cr_eq cr_mapping_def)
 done
 
 lemma size_Mapping [code]:
   fixes t :: "('a :: ccompare, 'b) mapping_rbt" shows
   "Mapping.size (Assoc_List_Mapping al) = size al"
   "Mapping.size (RBT_Mapping t) =
   (case ID CCOMPARE('a) of None \<Rightarrow> Code.abort (STR ''size RBT_Mapping: ccompare = None'') (\<lambda>_. Mapping.size (RBT_Mapping t))
                      | Some _ \<Rightarrow> length (RBT_Mapping2.entries t))"
 apply(simp_all split: option.split)
 apply(transfer, simp add: dom_map_of_conv_image_fst set_map[symmetric] distinct_card del: set_map)
 apply transfer
 apply(clarsimp simp add: size_eq_card_dom_lookup)
 apply(simp add: linorder.rbt_lookup_keys[OF ID_ccompare] ord.is_rbt_rbt_sorted RBT_Impl.keys_def distinct_card linorder.distinct_entries[OF ID_ccompare] del: set_map)
 done
 
-
 declare [[code drop: Mapping.tabulate]]
 declare tabulate_fold [code]
 
+declare [[code drop: Mapping.ordered_keys]]
+declare ordered_keys_def[code]
+
+declare [[code drop: Mapping.lookup_default]]
+declare Mapping.lookup_default_def[code]
+
+declare [[code drop: Mapping.filter]]
+lemma filter_code [code]:
+  fixes t :: "('a :: ccompare, 'b) mapping_rbt" shows
+  "Mapping.filter P (Mapping m) = Mapping (\<lambda>k. case m k of None \<Rightarrow> None | Some v \<Rightarrow> if P k v then Some v else None)"
+  "Mapping.filter P (Assoc_List_Mapping al) = Assoc_List_Mapping (DAList.filter (\<lambda>(k, v). P k v) al)"
+  "Mapping.filter P (RBT_Mapping t) =
+  (case ID CCOMPARE('a) of None \<Rightarrow> Code.abort (STR ''filter RBT_Mapping: ccompare = None'') (\<lambda>_. Mapping.filter P (RBT_Mapping t))
+                         | Some _ \<Rightarrow> RBT_Mapping (RBT_Mapping2.filter (\<lambda>(k, v). P k v) t))"
+  subgoal by transfer simp
+  subgoal by (simp, transfer)(simp add: map_of_filter_apply fun_eq_iff cong: if_cong option.case_cong)
+  subgoal by(clarsimp simp add: Mapping_inject Mapping.filter.abs_eq fun_eq_iff split: option.split)
+  done
+
+declare [[code drop: Mapping.map]]
+lemma map_values_code [code]:
+  fixes t :: "('a :: ccompare, 'b) mapping_rbt" shows
+  "Mapping.map_values f (Mapping m) = Mapping (\<lambda>k. map_option (f k) (m k))"
+  "Mapping.map_values f (Assoc_List_Mapping al) = Assoc_List_Mapping (AssocList.map_values f al)"
+  "Mapping.map_values f (RBT_Mapping t) = 
+  (case ID CCOMPARE('a) of None \<Rightarrow> Code.abort (STR ''map_values RBT_Mapping: ccompare = None'') (\<lambda>_. Mapping.map_values f (RBT_Mapping t))
+                         | Some _ \<Rightarrow> RBT_Mapping (RBT_Mapping2.map f t))"
+  subgoal by transfer simp
+  subgoal by(simp, transfer)(simp add: fun_eq_iff map_of_map')
+  subgoal by(clarsimp simp add: Mapping_inject Mapping.map_values.abs_eq fun_eq_iff split: option.split)
+  done
+
+declare [[code drop: Mapping.combine_with_key]]
+declare [[code drop: Mapping.combine]]
+
 datatype mapping_impl = Mapping_IMPL
 declare
   mapping_impl.eq.simps [code del]
   mapping_impl.rec [code del]
   mapping_impl.case [code del]
 
 lemma [code]:
   fixes x :: mapping_impl
   shows "size x = 0"
   and "size_mapping_impl x = 0"
 by(case_tac [!] x) simp_all
 
 definition mapping_Choose :: mapping_impl where [simp]: "mapping_Choose = Mapping_IMPL"
 definition mapping_Assoc_List :: mapping_impl where [simp]: "mapping_Assoc_List = Mapping_IMPL"
 definition mapping_RBT :: mapping_impl where [simp]: "mapping_RBT = Mapping_IMPL"
 definition mapping_Mapping :: mapping_impl where [simp]: "mapping_Mapping = Mapping_IMPL"
 
 code_datatype mapping_Choose mapping_Assoc_List mapping_RBT mapping_Mapping
 
 definition mapping_empty_choose :: "('a, 'b) mapping" 
 where [simp]: "mapping_empty_choose = Mapping.empty"
 
 lemma mapping_empty_choose_code [code]:
   "(mapping_empty_choose :: ('a :: ccompare, 'b) mapping) =
    (case ID CCOMPARE('a) of Some _  \<Rightarrow> RBT_Mapping RBT_Mapping2.empty
     | None \<Rightarrow> Assoc_List_Mapping DAList.empty)"
 by(auto split: option.split simp add: DAList.lookup_empty[abs_def] Mapping.empty_def)
 
 definition mapping_impl_choose2 :: "mapping_impl \<Rightarrow> mapping_impl \<Rightarrow> mapping_impl"
 where [simp]: "mapping_impl_choose2 = (\<lambda>_ _. Mapping_IMPL)"
 
 lemma mapping_impl_choose2_code [code]:
   "mapping_impl_choose2 x y = mapping_Choose"
   "mapping_impl_choose2 mapping_Mapping mapping_Mapping = mapping_Mapping"
   "mapping_impl_choose2 mapping_Assoc_List mapping_Assoc_List = mapping_Assoc_List"
   "mapping_impl_choose2 mapping_RBT mapping_RBT = mapping_RBT"
 by(simp_all)
 
 definition mapping_empty :: "mapping_impl \<Rightarrow> ('a, 'b) mapping"
 where [simp]: "mapping_empty = (\<lambda>_. Mapping.empty)"
 
 lemma mapping_empty_code [code]:
   "mapping_empty mapping_Choose = mapping_empty_choose"
   "mapping_empty mapping_Mapping = Mapping (\<lambda>_. None)"
   "mapping_empty mapping_Assoc_List = Assoc_List_Mapping DAList.empty"
   "mapping_empty mapping_RBT = RBT_Mapping RBT_Mapping2.empty"
 by(simp_all add: Mapping.empty_def DAList.lookup_empty[abs_def])
 
 subsection \<open>Type classes\<close>
 
 class mapping_impl = 
   fixes mapping_impl :: "('a, mapping_impl) phantom"
 
 syntax (input)
   "_MAPPING_IMPL" :: "type => logic"  ("(1MAPPING'_IMPL/(1'(_')))")
 
 parse_translation \<open>
 let
   fun mapping_impl_tr [ty] =
      (Syntax.const @{syntax_const "_constrain"} $ Syntax.const @{const_syntax "mapping_impl"} $
        (Syntax.const @{type_syntax phantom} $ ty $ Syntax.const @{type_syntax mapping_impl}))
     | mapping_impl_tr ts = raise TERM ("mapping_impl_tr", ts);
 in [(@{syntax_const "_MAPPING_IMPL"}, K mapping_impl_tr)] end
 \<close>
 
 declare [[code drop: Mapping.empty]]
 
 lemma Mapping_empty_code [code, code_unfold]: 
   "(Mapping.empty :: ('a :: mapping_impl, 'b) mapping) =
    mapping_empty (of_phantom MAPPING_IMPL('a))"
 by simp
 
 subsection \<open>Generator for the @{class mapping_impl}-class\<close>
 
 text \<open>
 This generator registers itself at the derive-manager for the classes @{class mapping_impl}.
 Here, one can choose
 the desired implementation via the parameter. 
 
 \begin{itemize}
 \item \texttt{instantiation type :: (type,\ldots,type) (rbt,assoclist,mapping,choose, or arbitrary constant name) mapping-impl}
 \end{itemize}
 \<close>
 
 
 text \<open>
 This generator can be used for arbitrary types, not just datatypes. 
 \<close>
 
 ML_file \<open>mapping_impl_generator.ML\<close> 
 
 derive (assoclist) mapping_impl unit bool
 derive (rbt) mapping_impl nat
 derive (mapping_RBT) mapping_impl int (* shows usage of constant names *)
 derive (assoclist) mapping_impl Enum.finite_1 Enum.finite_2 Enum.finite_3
 derive (rbt) mapping_impl integer natural
 derive (rbt) mapping_impl char
 
 instantiation sum :: (mapping_impl, mapping_impl) mapping_impl begin
 definition "MAPPING_IMPL('a + 'b) = Phantom('a + 'b) 
   (mapping_impl_choose2 (of_phantom MAPPING_IMPL('a)) (of_phantom MAPPING_IMPL('b)))"
 instance ..
 end
 
 instantiation prod :: (mapping_impl, mapping_impl) mapping_impl begin
 definition "MAPPING_IMPL('a * 'b) = Phantom('a * 'b) 
   (mapping_impl_choose2 (of_phantom MAPPING_IMPL('a)) (of_phantom MAPPING_IMPL('b)))"
 instance ..
 end
 
 derive (choose) mapping_impl list
 derive (rbt) mapping_impl String.literal
 
 instantiation option :: (mapping_impl) mapping_impl begin
 definition "MAPPING_IMPL('a option) = Phantom('a option) (of_phantom MAPPING_IMPL('a))"
 instance ..
 end
 
 derive (choose) mapping_impl set
 
 instantiation phantom :: (type, mapping_impl) mapping_impl begin
 definition "MAPPING_IMPL(('a, 'b) phantom) = Phantom (('a, 'b) phantom) 
   (of_phantom MAPPING_IMPL('b))"
 instance ..
 end
 
+declare [[code drop: Mapping.bulkload]]
+lemma bulkload_code [code]:
+  "Mapping.bulkload vs = RBT_Mapping (RBT_Mapping2.bulkload (zip_with_index vs))"
+  by(simp add: Mapping.bulkload.abs_eq Mapping_inject ccompare_nat_def ID_def fun_eq_iff)
+
 end