Skip to content
Snippets Groups Projects
Commit b5b8255ae4c4 authored by Andreas Lochbihler's avatar Andreas Lochbihler
Browse files

more operations for maps

parent f90f9d593a88
No related branches found
No related tags found
No related merge requests found
......@@ -23,6 +23,12 @@
"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
......@@ -87,6 +93,28 @@
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"
......@@ -100,6 +128,10 @@
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)
......
......@@ -119,7 +119,6 @@
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]
......@@ -123,6 +122,41 @@
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]
......@@ -249,4 +283,9 @@
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
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment