header {* \isaheader{Array Based Hash-Maps} *}
theory Impl_Array_Hash_Map imports
"../../../Automatic_Refinement/Automatic_Refinement"
"../../Iterator/Array_Iterator"
"../Gen/Gen_Map"
"../Intf/Intf_Hash"
"../Intf/Intf_Map"
"../../Lib/HashCode"
"../../Lib/Diff_Array"
Impl_List_Map
begin
subsection {* Type definition and primitive operations *}
definition load_factor :: nat -- "in percent"
where "load_factor = 75"
datatype ('key, 'val) hashmap =
HashMap "('key,'val) list_map array" "nat"
subsection {* Operations *}
definition new_hashmap_with :: "nat => ('k, 'v) hashmap"
where "!!size. new_hashmap_with size =
HashMap (new_array [] size) 0"
definition ahm_empty :: "nat => ('k, 'v) hashmap"
where "ahm_empty def_size ≡ new_hashmap_with def_size"
definition bucket_ok :: "'k bhc => nat => nat => ('k×'v) list => bool"
where "bucket_ok bhc len h kvs = (∀k ∈ fst ` set kvs. bhc len k = h)"
definition ahm_invar_aux :: "'k bhc => nat => ('k×'v) list array => bool"
where
"ahm_invar_aux bhc n a <->
(∀h. h < array_length a --> bucket_ok bhc (array_length a) h
(array_get a h) ∧ list_map_invar (array_get a h)) ∧
array_foldl (λ_ n kvs. n + size kvs) 0 a = n ∧
array_length a > 1"
primrec ahm_invar :: "'k bhc => ('k, 'v) hashmap => bool"
where "ahm_invar bhc (HashMap a n) = ahm_invar_aux bhc n a"
definition ahm_lookup_aux :: "'k eq => 'k bhc =>
'k => ('k, 'v) list_map array => 'v option"
where [simp]: "ahm_lookup_aux eq bhc k a = list_map_lookup eq k (array_get a (bhc (array_length a) k))"
primrec ahm_lookup where
"ahm_lookup eq bhc k (HashMap a _) = ahm_lookup_aux eq bhc k a"
definition "ahm_α bhc m ≡ λk. ahm_lookup op= bhc k m"
definition ahm_map_rel_def_internal:
"ahm_map_rel Rk Rv ≡ {(HashMap a n, HashMap a' n)| a a' n n'.
(a,a') ∈ ⟨⟨⟨Rk,Rv⟩prod_rel⟩list_rel⟩array_rel ∧ (n,n') ∈ Id}"
lemma ahm_map_rel_def: "⟨Rk,Rv⟩ ahm_map_rel ≡
{(HashMap a n, HashMap a' n)| a a' n n'.
(a,a') ∈ ⟨⟨⟨Rk,Rv⟩prod_rel⟩list_rel⟩array_rel ∧ (n,n') ∈ Id}"
unfolding relAPP_def ahm_map_rel_def_internal .
definition ahm_map_rel'_def:
"ahm_map_rel' bhc ≡ br (ahm_α bhc) (ahm_invar bhc)"
definition ahm_rel_def_internal: "ahm_rel bhc Rk Rv =
⟨Rk,Rv⟩ ahm_map_rel O ahm_map_rel' (abstract_bounded_hashcode Rk bhc)"
lemma ahm_rel_def: "⟨Rk, Rv⟩ ahm_rel bhc ≡
⟨Rk,Rv⟩ ahm_map_rel O ahm_map_rel' (abstract_bounded_hashcode Rk bhc)"
unfolding relAPP_def ahm_rel_def_internal .
lemmas [autoref_rel_intf] = REL_INTFI[of "ahm_rel bhc" i_map] for bhc
abbreviation "dflt_ahm_rel ≡ ahm_rel bounded_hashcode_nat"
primrec ahm_iteratei_aux :: "(('k×'v) list array) => ('k×'v, 'σ) set_iterator"
where "ahm_iteratei_aux (Array xs) c f = foldli (concat xs) c f"
primrec ahm_iteratei :: "(('k, 'v) hashmap) => (('k×'v), 'σ) set_iterator"
where
"ahm_iteratei (HashMap a n) = ahm_iteratei_aux a"
definition ahm_rehash_aux' :: "'k bhc => nat => 'k×'v =>
('k×'v) list array => ('k×'v) list array"
where
"ahm_rehash_aux' bhc n kv a =
(let h = bhc n (fst kv)
in array_set a h (kv # array_get a h))"
definition ahm_rehash_aux :: "'k bhc => ('k×'v) list array => nat =>
('k×'v) list array"
where
"ahm_rehash_aux bhc a sz = ahm_iteratei_aux a (λx. True)
(ahm_rehash_aux' bhc sz) (new_array [] sz)"
primrec ahm_rehash :: "'k bhc => ('k,'v) hashmap => nat => ('k,'v) hashmap"
where "ahm_rehash bhc (HashMap a n) sz = HashMap (ahm_rehash_aux bhc a sz) n"
primrec hm_grow :: "('k,'v) hashmap => nat"
where "hm_grow (HashMap a n) = 2 * array_length a + 3"
primrec ahm_filled :: "('k,'v) hashmap => bool"
where "ahm_filled (HashMap a n) = (array_length a * load_factor ≤ n * 100)"
primrec ahm_update_aux :: "'k eq => 'k bhc => ('k,'v) hashmap =>
'k => 'v => ('k, 'v) hashmap"
where
"ahm_update_aux eq bhc (HashMap a n) k v =
(let h = bhc (array_length a) k;
m = array_get a h;
insert = list_map_lookup eq k m = None
in HashMap (array_set a h (list_map_update eq k v m))
(if insert then n + 1 else n))"
definition ahm_update :: "'k eq => 'k bhc => 'k => 'v =>
('k, 'v) hashmap => ('k, 'v) hashmap"
where
"ahm_update eq bhc k v hm =
(let hm' = ahm_update_aux eq bhc hm k v
in (if ahm_filled hm' then ahm_rehash bhc hm' (hm_grow hm') else hm'))"
primrec ahm_delete :: "'k eq => 'k bhc => 'k =>
('k,'v) hashmap => ('k,'v) hashmap"
where
"ahm_delete eq bhc k (HashMap a n) =
(let h = bhc (array_length a) k;
m = array_get a h;
deleted = (list_map_lookup eq k m ≠ None)
in HashMap (array_set a h (list_map_delete eq k m)) (if deleted then n - 1 else n))"
primrec ahm_isEmpty :: "('k,'v) hashmap => bool" where
"ahm_isEmpty (HashMap _ n) = (n = 0)"
primrec ahm_isSng :: "('k,'v) hashmap => bool" where
"ahm_isSng (HashMap _ n) = (n = 1)"
primrec ahm_size :: "('k,'v) hashmap => nat" where
"ahm_size (HashMap _ n) = n"
lemma hm_grow_gt_1 [iff]:
"Suc 0 < hm_grow hm"
by(cases hm)(simp)
lemma bucket_ok_Nil [simp]: "bucket_ok bhc len h [] = True"
by(simp add: bucket_ok_def)
lemma bucket_okD:
"[| bucket_ok bhc len h xs; (k, v) ∈ set xs |]
==> bhc len k = h"
by(auto simp add: bucket_ok_def)
lemma bucket_okI:
"(!!k. k ∈ fst ` set kvs ==> bhc len k = h) ==> bucket_ok bhc len h kvs"
by(simp add: bucket_ok_def)
subsection {* Parametricity *}
lemma param_HashMap[param]: "(HashMap, HashMap) ∈
⟨⟨⟨Rk,Rv⟩prod_rel⟩list_rel⟩array_rel -> nat_rel -> ⟨Rk,Rv⟩ahm_map_rel"
unfolding ahm_map_rel_def by force
lemma param_case_hashmap[param]: "(case_hashmap, case_hashmap) ∈
(⟨⟨⟨Rk,Rv⟩prod_rel⟩list_rel⟩array_rel -> nat_rel -> R) ->
⟨Rk,Rv⟩ahm_map_rel -> R"
unfolding ahm_map_rel_def[abs_def]
by (force split: hashmap.split dest: fun_relD)
lemma rec_hashmap_is_case[simp]: "rec_hashmap = case_hashmap"
by (intro ext, simp split: hashmap.split)
subsection {* @{term ahm_invar} *}
lemma ahm_invar_auxD:
assumes "ahm_invar_aux bhc n a"
shows "!!h. h < array_length a ==>
bucket_ok bhc (array_length a) h (array_get a h)" and
"!!h. h < array_length a ==>
list_map_invar (array_get a h)" and
"n = array_foldl (λ_ n kvs. n + length kvs) 0 a" and
"array_length a > 1"
using assms unfolding ahm_invar_aux_def by auto
lemma ahm_invar_auxE:
assumes "ahm_invar_aux bhc n a"
obtains "∀h. h < array_length a -->
bucket_ok bhc (array_length a) h (array_get a h) ∧
list_map_invar (array_get a h)" and
"n = array_foldl (λ_ n kvs. n + length kvs) 0 a" and
"array_length a > 1"
using assms unfolding ahm_invar_aux_def by blast
lemma ahm_invar_auxI:
"[| !!h. h < array_length a ==>
bucket_ok bhc (array_length a) h (array_get a h);
!!h. h < array_length a ==> list_map_invar (array_get a h);
n = array_foldl (λ_ n kvs. n + length kvs) 0 a; array_length a > 1 |]
==> ahm_invar_aux bhc n a"
unfolding ahm_invar_aux_def by blast
lemma ahm_invar_distinct_fst_concatD:
assumes inv: "ahm_invar_aux bhc n (Array xs)"
shows "distinct (map fst (concat xs))"
proof -
{ fix h
assume "h < length xs"
with inv have "bucket_ok bhc (length xs) h (xs ! h)" and
"list_map_invar (xs ! h)"
by(simp_all add: ahm_invar_aux_def) }
note no_junk = this
show ?thesis unfolding map_concat
proof(rule distinct_concat')
have "distinct [x\<leftarrow>xs . x ≠ []]" unfolding distinct_conv_nth
proof(intro allI ballI impI)
fix i j
assume "i < length [x\<leftarrow>xs . x ≠ []]" "j < length [x\<leftarrow>xs . x ≠ []]" "i ≠ j"
from filter_nth_ex_nth[OF `i < length [x\<leftarrow>xs . x ≠ []]`]
obtain i' where "i' ≥ i" "i' < length xs" and ith: "[x\<leftarrow>xs . x ≠ []] ! i = xs ! i'"
and eqi: "[x\<leftarrow>take i' xs . x ≠ []] = take i [x\<leftarrow>xs . x ≠ []]" by blast
from filter_nth_ex_nth[OF `j < length [x\<leftarrow>xs . x ≠ []]`]
obtain j' where "j' ≥ j" "j' < length xs" and jth: "[x\<leftarrow>xs . x ≠ []] ! j = xs ! j'"
and eqj: "[x\<leftarrow>take j' xs . x ≠ []] = take j [x\<leftarrow>xs . x ≠ []]" by blast
show "[x\<leftarrow>xs . x ≠ []] ! i ≠ [x\<leftarrow>xs . x ≠ []] ! j"
proof
assume "[x\<leftarrow>xs . x ≠ []] ! i = [x\<leftarrow>xs . x ≠ []] ! j"
hence eq: "xs ! i' = xs ! j'" using ith jth by simp
from `i < length [x\<leftarrow>xs . x ≠ []]`
have "[x\<leftarrow>xs . x ≠ []] ! i ∈ set [x\<leftarrow>xs . x ≠ []]" by(rule nth_mem)
with ith have "xs ! i' ≠ []" by simp
then obtain kv where "kv ∈ set (xs ! i')" by(fastforce simp add: neq_Nil_conv)
with no_junk[OF `i' < length xs`] have "bhc (length xs) (fst kv) = i'"
by(simp add: bucket_ok_def)
moreover from eq `kv ∈ set (xs ! i')` have "kv ∈ set (xs ! j')" by simp
with no_junk[OF `j' < length xs`] have "bhc (length xs) (fst kv) = j'"
by(simp add: bucket_ok_def)
ultimately have [simp]: "i' = j'" by simp
from `i < length [x\<leftarrow>xs . x ≠ []]` have "i = length (take i [x\<leftarrow>xs . x ≠ []])" by simp
also from eqi eqj have "take i [x\<leftarrow>xs . x ≠ []] = take j [x\<leftarrow>xs . x ≠ []]" by simp
finally show False using `i ≠ j` `j < length [x\<leftarrow>xs . x ≠ []]` by simp
qed
qed
moreover have "inj_on (map fst) {x ∈ set xs. x ≠ []}"
proof(rule inj_onI)
fix x y
assume "x ∈ {x ∈ set xs. x ≠ []}" "y ∈ {x ∈ set xs. x ≠ []}" "map fst x = map fst y"
hence "x ∈ set xs" "y ∈ set xs" "x ≠ []" "y ≠ []" by auto
from `x ∈ set xs` obtain i where "xs ! i = x" "i < length xs" unfolding set_conv_nth by fastforce
from `y ∈ set xs` obtain j where "xs ! j = y" "j < length xs" unfolding set_conv_nth by fastforce
from `x ≠ []` obtain k v x' where "x = (k, v) # x'" by(cases x) auto
with no_junk[OF `i < length xs`] `xs ! i = x`
have "bhc (length xs) k = i" by(auto simp add: bucket_ok_def)
moreover from `map fst x = map fst y` `x = (k, v) # x'` obtain v' where "(k, v') ∈ set y" by fastforce
with no_junk[OF `j < length xs`] `xs ! j = y`
have "bhc (length xs) k = j" by(auto simp add: bucket_ok_def)
ultimately have "i = j" by simp
with `xs ! i = x` `xs ! j = y` show "x = y" by simp
qed
ultimately show "distinct [ys\<leftarrow>map (map fst) xs . ys ≠ []]"
by(simp add: filter_map o_def distinct_map)
next
fix ys
have A: "!!xs. distinct (map fst xs) = list_map_invar xs"
by (simp add: list_map_invar_def)
assume "ys ∈ set (map (map fst) xs)"
thus "distinct ys"
by(clarsimp simp add: set_conv_nth A) (erule no_junk(2))
next
fix ys zs
assume "ys ∈ set (map (map fst) xs)" "zs ∈ set (map (map fst) xs)" "ys ≠ zs"
then obtain ys' zs' where [simp]: "ys = map fst ys'" "zs = map fst zs'"
and "ys' ∈ set xs" "zs' ∈ set xs" by auto
have "fst ` set ys' ∩ fst ` set zs' = {}"
proof(rule equals0I)
fix k
assume "k ∈ fst ` set ys' ∩ fst ` set zs'"
then obtain v v' where "(k, v) ∈ set ys'" "(k, v') ∈ set zs'" by(auto)
from `ys' ∈ set xs` obtain i where "xs ! i = ys'" "i < length xs" unfolding set_conv_nth by fastforce
with `(k, v) ∈ set ys'` have "bhc (length xs) k = i" by(auto dest: no_junk bucket_okD)
moreover
from `zs' ∈ set xs` obtain j where "xs ! j = zs'" "j < length xs" unfolding set_conv_nth by fastforce
with `(k, v') ∈ set zs'` have "bhc (length xs) k = j" by(auto dest: no_junk bucket_okD)
ultimately have "i = j" by simp
with `xs ! i = ys'` `xs ! j = zs'` have "ys' = zs'" by simp
with `ys ≠ zs` show False by simp
qed
thus "set ys ∩ set zs = {}" by simp
qed
qed
subsection {* @{term "ahm_α"} *}
lemma list_map_lookup_is_map_of:
"list_map_lookup op= k l = map_of l k"
using list_map_autoref_lookup_aux[where eq="op=" and
Rk=Id and Rv=Id] by force
definition "ahm_α_aux bhc a ≡
(λk. ahm_lookup_aux op= bhc k a)"
lemma ahm_α_aux_def2: "ahm_α_aux bhc a = (λk. map_of (array_get a
(bhc (array_length a) k)) k)"
unfolding ahm_α_aux_def ahm_lookup_aux_def
by (simp add: list_map_lookup_is_map_of)
lemma ahm_α_def2: "ahm_α bhc (HashMap a n) = ahm_α_aux bhc a"
unfolding ahm_α_def ahm_α_aux_def by simp
lemma finite_dom_ahm_α_aux:
assumes "is_bounded_hashcode Id op= bhc" "ahm_invar_aux bhc n a"
shows "finite (dom (ahm_α_aux bhc a))"
proof -
have "dom (ahm_α_aux bhc a) ⊆ (\<Union>h ∈ range (bhc (array_length a) :: 'a => nat). dom (map_of (array_get a h)))"
unfolding ahm_α_aux_def2
by(force simp add: dom_map_of_conv_image_fst dest: map_of_SomeD)
moreover have "finite …"
proof(rule finite_UN_I)
from `ahm_invar_aux bhc n a` have "array_length a > 1" by(simp add: ahm_invar_aux_def)
hence "range (bhc (array_length a) :: 'a => nat) ⊆ {0..<array_length a}"
using assms by force
thus "finite (range (bhc (array_length a) :: 'a => nat))"
by(rule finite_subset) simp
qed(rule finite_dom_map_of)
ultimately show ?thesis by(rule finite_subset)
qed
lemma ahm_α_aux_new_array[simp]:
assumes bhc: "is_bounded_hashcode Id op= bhc" "1 < sz"
shows "ahm_α_aux bhc (new_array [] sz) k = None"
using is_bounded_hashcodeD(3)[OF assms]
unfolding ahm_α_aux_def ahm_lookup_aux_def by simp
lemma ahm_α_aux_conv_map_of_concat:
assumes bhc: "is_bounded_hashcode Id op= bhc"
assumes inv: "ahm_invar_aux bhc n (Array xs)"
shows "ahm_α_aux bhc (Array xs) = map_of (concat xs)"
proof
fix k
show "ahm_α_aux bhc (Array xs) k = map_of (concat xs) k"
proof(cases "map_of (concat xs) k")
case None
hence "k ∉ fst ` set (concat xs)" by(simp add: map_of_eq_None_iff)
hence "k ∉ fst ` set (xs ! bhc (length xs) k)"
proof(rule contrapos_nn)
assume "k ∈ fst ` set (xs ! bhc (length xs) k)"
then obtain v where "(k, v) ∈ set (xs ! bhc (length xs) k)" by auto
moreover from inv have "bhc (length xs) k < length xs"
using bhc by (force simp: ahm_invar_aux_def)
ultimately show "k ∈ fst ` set (concat xs)"
by (force intro: rev_image_eqI)
qed
thus ?thesis unfolding None ahm_α_aux_def2
by (simp add: map_of_eq_None_iff)
next
case (Some v)
hence "(k, v) ∈ set (concat xs)" by(rule map_of_SomeD)
then obtain ys where "ys ∈ set xs" "(k, v) ∈ set ys"
unfolding set_concat by blast
from `ys ∈ set xs` obtain i j where "i < length xs" "xs ! i = ys"
unfolding set_conv_nth by auto
with inv `(k, v) ∈ set ys`
show ?thesis unfolding Some
unfolding ahm_α_aux_def2
by(force dest: bucket_okD simp add: ahm_invar_aux_def list_map_invar_def)
qed
qed
lemma ahm_invar_aux_card_dom_ahm_α_auxD:
assumes bhc: "is_bounded_hashcode Id op= bhc"
assumes inv: "ahm_invar_aux bhc n a"
shows "card (dom (ahm_α_aux bhc a)) = n"
proof(cases a)
case (Array xs)[simp]
from inv have "card (dom (ahm_α_aux bhc (Array xs))) = card (dom (map_of (concat xs)))"
by(simp add: ahm_α_aux_conv_map_of_concat[OF bhc])
also from inv have "distinct (map fst (concat xs))"
by(simp add: ahm_invar_distinct_fst_concatD)
hence "card (dom (map_of (concat xs))) = length (concat xs)"
by(rule card_dom_map_of)
also have "length (concat xs) = foldl op + 0 (map length xs)"
by (simp add: length_concat foldl_conv_fold add.commute fold_plus_listsum_rev)
also from inv
have "… = n" unfolding foldl_map by(simp add: ahm_invar_aux_def array_foldl_foldl)
finally show ?thesis by(simp)
qed
lemma finite_dom_ahm_α:
assumes "is_bounded_hashcode Id op= bhc" "ahm_invar bhc hm"
shows "finite (dom (ahm_α bhc hm))"
using assms by (cases hm, force intro: finite_dom_ahm_α_aux
simp: ahm_α_def2)
subsection {* @{term ahm_empty} *}
lemma ahm_invar_aux_new_array:
assumes "n > 1"
shows "ahm_invar_aux bhc 0 (new_array [] n)"
proof -
have "foldl (λb (k, v). b + length v) 0 (zip [0..<n] (replicate n [])) = 0"
by(induct n)(simp_all add: replicate_Suc_conv_snoc del: replicate_Suc)
with assms show ?thesis by(simp add: ahm_invar_aux_def array_foldl_new_array list_map_invar_def)
qed
lemma ahm_invar_new_hashmap_with:
"n > 1 ==> ahm_invar bhc (new_hashmap_with n)"
by(auto simp add: ahm_invar_def new_hashmap_with_def intro: ahm_invar_aux_new_array)
lemma ahm_α_new_hashmap_with:
assumes "is_bounded_hashcode Id op= bhc" and "n > 1"
shows "Map.empty = ahm_α bhc (new_hashmap_with n)"
unfolding new_hashmap_with_def ahm_α_def
using is_bounded_hashcodeD(3)[OF assms] by force
lemma ahm_empty_impl:
assumes bhc: "is_bounded_hashcode Id op= bhc"
assumes def_size: "def_size > 1"
shows "(ahm_empty def_size, Map.empty) ∈ ahm_map_rel' bhc"
proof-
from def_size and ahm_α_new_hashmap_with[OF bhc def_size] and
ahm_invar_new_hashmap_with[OF def_size]
show ?thesis unfolding ahm_empty_def ahm_map_rel'_def br_def by force
qed
lemma param_ahm_empty[param]:
assumes def_size: "(def_size, def_size') ∈ nat_rel"
shows "(ahm_empty def_size ,ahm_empty def_size') ∈
⟨Rk,Rv⟩ahm_map_rel"
unfolding ahm_empty_def[abs_def] new_hashmap_with_def[abs_def]
new_array_def[abs_def]
using assms by parametricity
lemma autoref_ahm_empty[autoref_rules]:
fixes Rk :: "('kc×'ka) set"
assumes bhc: "SIDE_GEN_ALGO (is_bounded_hashcode Rk eq bhc)"
assumes def_size: "SIDE_GEN_ALGO (is_valid_def_hm_size TYPE('kc) def_size)"
shows "(ahm_empty def_size, op_map_empty) ∈ ⟨Rk, Rv⟩ahm_rel bhc"
proof-
from bhc have eq': "(eq,op=) ∈ Rk -> Rk -> bool_rel"
by (simp add: is_bounded_hashcodeD)
with bhc have "is_bounded_hashcode Id op=
(abstract_bounded_hashcode Rk bhc)"
unfolding autoref_tag_defs
by blast
thus ?thesis using assms
unfolding op_map_empty_def
unfolding ahm_rel_def is_valid_def_hm_size_def autoref_tag_defs
apply (intro relcompI)
apply (rule param_ahm_empty[of def_size def_size], simp)
apply (blast intro: ahm_empty_impl)
done
qed
subsection {* @{term "ahm_lookup"} *}
lemma param_ahm_lookup[param]:
assumes bhc: "is_bounded_hashcode Rk eq bhc"
defines bhc'_def: "bhc' ≡ abstract_bounded_hashcode Rk bhc"
assumes inv: "ahm_invar bhc' m'"
assumes K: "(k,k') ∈ Rk"
assumes M: "(m,m') ∈ ⟨Rk,Rv⟩ahm_map_rel"
shows "(ahm_lookup eq bhc k m, ahm_lookup op= bhc' k' m') ∈
⟨Rv⟩option_rel"
proof-
from bhc have eq': "(eq,op=) ∈ Rk -> Rk -> bool_rel" by (simp add: is_bounded_hashcodeD)
moreover from abstract_bhc_correct[OF bhc]
have bhc': "(bhc,bhc') ∈ nat_rel -> Rk -> nat_rel" unfolding bhc'_def .
moreover from M obtain a a' n n' where
[simp]: "m = HashMap a n" and [simp]: "m' = HashMap a' n'" and
A: "(a,a') ∈ ⟨⟨⟨Rk,Rv⟩prod_rel⟩list_rel⟩array_rel" and N: "(n,n') ∈ Id"
by (cases m, cases m', unfold ahm_map_rel_def, auto)
moreover from inv and array_rel_imp_same_length[OF A]
have "array_length a > 1" by (simp add: ahm_invar_aux_def)
with abstract_bhc_is_bhc[OF bhc]
have "bhc' (array_length a) k' < array_length a"
unfolding bhc'_def by blast
with bhc'[param_fo, OF _ K]
have "bhc (array_length a) k < array_length a" by simp
ultimately show ?thesis using K
unfolding ahm_lookup_def[abs_def] rec_hashmap_is_case
by (simp, parametricity)
qed
lemma ahm_lookup_impl:
assumes bhc: "is_bounded_hashcode Id op= bhc"
shows "(ahm_lookup op= bhc, op_map_lookup) ∈ Id -> ahm_map_rel' bhc -> Id"
unfolding ahm_map_rel'_def br_def ahm_α_def by force
lemma autoref_ahm_lookup[autoref_rules]:
assumes
bhc[unfolded autoref_tag_defs]: "SIDE_GEN_ALGO (is_bounded_hashcode Rk eq bhc)"
shows "(ahm_lookup eq bhc, op_map_lookup)
∈ Rk -> ⟨Rk,Rv⟩ahm_rel bhc -> ⟨Rv⟩option_rel"
proof (intro fun_relI)
let ?bhc' = "abstract_bounded_hashcode Rk bhc"
fix k k' a m'
assume K: "(k,k') ∈ Rk"
assume M: "(a,m') ∈ ⟨Rk,Rv⟩ahm_rel bhc"
from bhc have bhc': "is_bounded_hashcode Id op= ?bhc'"
by blast
from M obtain a' where M1: "(a,a') ∈ ⟨Rk,Rv⟩ahm_map_rel" and
M2: "(a',m') ∈ ahm_map_rel' ?bhc'" unfolding ahm_rel_def by blast
hence inv: "ahm_invar ?bhc' a'"
unfolding ahm_map_rel'_def br_def by simp
from relcompI[OF param_ahm_lookup[OF bhc inv K M1]
ahm_lookup_impl[param_fo, OF bhc' _ M2]]
show "(ahm_lookup eq bhc k a, op_map_lookup k' m') ∈ ⟨Rv⟩option_rel"
by simp
qed
subsection {* @{term "ahm_iteratei"} *}
abbreviation "ahm_to_list ≡ it_to_list ahm_iteratei"
lemma param_ahm_iteratei_aux[param]:
"(ahm_iteratei_aux,ahm_iteratei_aux) ∈ ⟨⟨Ra⟩list_rel⟩array_rel ->
(Rb -> bool_rel) -> (Ra -> Rb -> Rb) -> Rb -> Rb"
unfolding ahm_iteratei_aux_def[abs_def] by parametricity
lemma param_ahm_iteratei[param]:
"(ahm_iteratei,ahm_iteratei) ∈ ⟨Rk,Rv⟩ahm_map_rel ->
(Rb -> bool_rel) -> (⟨Rk,Rv⟩prod_rel -> Rb -> Rb) -> Rb -> Rb"
unfolding ahm_iteratei_def[abs_def] rec_hashmap_is_case by parametricity
lemma param_ahm_to_list[param]:
"(ahm_to_list,ahm_to_list) ∈
⟨Rk, Rv⟩ahm_map_rel -> ⟨⟨Rk,Rv⟩prod_rel⟩list_rel"
unfolding it_to_list_def[abs_def] by parametricity
lemma ahm_to_list_distinct[simp,intro]:
assumes bhc: "is_bounded_hashcode Id op= bhc"
assumes inv: "ahm_invar bhc m"
shows "distinct (ahm_to_list m)"
proof-
obtain n a where [simp]: "m = HashMap a n" by (cases m)
obtain l where [simp]: "a = Array l" by (cases a)
from inv show "distinct (ahm_to_list m)" unfolding it_to_list_def
by (force intro: distinct_mapI dest: ahm_invar_distinct_fst_concatD)
qed
lemma set_ahm_to_list:
assumes bhc: "is_bounded_hashcode Id op= bhc"
assumes ref: "(m,m') ∈ ahm_map_rel' bhc"
shows "map_to_set m' = set (ahm_to_list m)"
proof-
obtain n a where [simp]: "m = HashMap a n" by (cases m)
obtain l where [simp]: "a = Array l" by (cases a)
from ref have α[simp]: "m' = ahm_α bhc m" and
inv: "ahm_invar bhc m"
unfolding ahm_map_rel'_def br_def by auto
from inv have length: "length l > 1"
unfolding ahm_invar_def ahm_invar_aux_def by force
from inv have buckets_ok: "!!h x. h < length l ==> x ∈ set (l!h) ==>
bhc (length l) (fst x) = h"
"!!h. h < length l ==> distinct (map fst (l!h))"
by (simp_all add: ahm_invar_def ahm_invar_aux_def
bucket_ok_def list_map_invar_def)
show ?thesis unfolding it_to_list_def α ahm_α_def ahm_iteratei_def
apply (simp add: list_map_lookup_is_map_of)
proof (intro equalityI subsetI)
case (goal1 x)
let ?m = "λk. map_of (l ! bhc (length l) k) k"
obtain k v where [simp]: "x = (k, v)" by (cases x)
from goal1 have "set_to_map (map_to_set ?m) k = Some v"
by (simp add: set_to_map_simp inj_on_fst_map_to_set)
also note map_to_set_inverse
finally have "map_of (l ! bhc (length l) k) k = Some v" .
hence "(k,v) ∈ set (l ! bhc (length l) k)"
by (simp add: map_of_is_SomeD)
moreover have "bhc (length l) k < length l" using bhc length ..
ultimately show ?case by force
next
case (goal2 x)
obtain k v where [simp]: "x = (k, v)" by (cases x)
from goal2 obtain h where h_props: "(k,v) ∈ set (l!h)" "h < length l"
by (force simp: set_conv_nth)
moreover from h_props and buckets_ok
have "bhc (length l) k = h" "distinct (map fst (l!h))" by auto
ultimately have "map_of (l ! bhc (length l) k) k = Some v"
by (force intro: map_of_is_SomeI)
thus ?case by simp
qed
qed
lemma ahm_iteratei_aux_impl:
assumes inv: "ahm_invar_aux bhc n a"
and bhc: "is_bounded_hashcode Id op= bhc"
shows "map_iterator (ahm_iteratei_aux a) (ahm_α_aux bhc a)"
proof (cases a, rule)
fix xs assume [simp]: "a = Array xs"
show "ahm_iteratei_aux a = foldli (concat xs)"
by (intro ext, simp)
from ahm_invar_distinct_fst_concatD and inv
show "distinct (map fst (concat xs))" by simp
from ahm_α_aux_conv_map_of_concat and assms
show "ahm_α_aux bhc a = map_of (concat xs)" by simp
qed
lemma ahm_iteratei_impl:
assumes inv: "ahm_invar bhc m"
and bhc: "is_bounded_hashcode Id op= bhc"
shows "map_iterator (ahm_iteratei m) (ahm_α bhc m)"
by (insert assms, cases m, simp add: ahm_α_def2,
erule (1) ahm_iteratei_aux_impl)
lemma autoref_ahm_is_iterator[autoref_ga_rules]:
assumes bhc: "GEN_ALGO_tag (is_bounded_hashcode Rk eq bhc)"
shows "is_map_to_list Rk Rv (ahm_rel bhc) ahm_to_list"
unfolding is_map_to_list_def is_map_to_sorted_list_def
proof (intro allI impI)
let ?bhc' = "abstract_bounded_hashcode Rk bhc"
fix a m' assume M: "(a,m') ∈ ⟨Rk,Rv⟩ahm_rel bhc"
from bhc have bhc': "is_bounded_hashcode Id op= ?bhc'"
unfolding autoref_tag_defs
apply (rule_tac abstract_bhc_is_bhc)
by simp_all
from M obtain a' where M1: "(a,a') ∈ ⟨Rk,Rv⟩ahm_map_rel" and
M2: "(a',m') ∈ ahm_map_rel' ?bhc'" unfolding ahm_rel_def by blast
hence inv: "ahm_invar ?bhc' a'"
unfolding ahm_map_rel'_def br_def by simp
let ?l' = "ahm_to_list a'"
from param_ahm_to_list[param_fo, OF M1]
have "(ahm_to_list a, ?l') ∈ ⟨⟨Rk,Rv⟩prod_rel⟩list_rel" .
moreover from ahm_to_list_distinct[OF bhc' inv]
have "distinct (ahm_to_list a')" .
moreover from set_ahm_to_list[OF bhc' M2]
have "map_to_set m' = set (ahm_to_list a')" .
ultimately show "∃l'. (ahm_to_list a, l') ∈ ⟨⟨Rk,Rv⟩prod_rel⟩list_rel ∧
RETURN l' ≤ it_to_sorted_list
(key_rel (λ_ _. True)) (map_to_set m')"
by (force simp: it_to_sorted_list_def key_rel_def[abs_def])
qed
lemma ahm_iteratei_aux_code[code]:
"ahm_iteratei_aux a c f σ = idx_iteratei array_get array_length a c
(λx. foldli x c f) σ"
proof(cases a)
case (Array xs)[simp]
have "ahm_iteratei_aux a c f σ = foldli (concat xs) c f σ" by simp
also have "… = foldli xs c (λx. foldli x c f) σ" by (simp add: foldli_concat)
also have "… = idx_iteratei op ! length xs c (λx. foldli x c f) σ"
by (simp add: idx_iteratei_nth_length_conv_foldli)
also have "… = idx_iteratei array_get array_length a c (λx. foldli x c f) σ"
by(simp add: idx_iteratei_array_get_Array_conv_nth)
finally show ?thesis .
qed
subsection {* @{term "ahm_rehash"} *}
lemma array_length_ahm_rehash_aux':
"array_length (ahm_rehash_aux' bhc n kv a) = array_length a"
by(simp add: ahm_rehash_aux'_def Let_def)
lemma ahm_rehash_aux'_preserves_ahm_invar_aux:
assumes inv: "ahm_invar_aux bhc n a"
and bhc: "is_bounded_hashcode Id op= bhc"
and fresh: "k ∉ fst ` set (array_get a (bhc (array_length a) k))"
shows "ahm_invar_aux bhc (Suc n) (ahm_rehash_aux' bhc (array_length a) (k, v) a)"
(is "ahm_invar_aux bhc _ ?a")
proof(rule ahm_invar_auxI)
note invD = ahm_invar_auxD[OF inv]
let ?l = "array_length a"
fix h
assume "h < array_length ?a"
hence hlen: "h < ?l" by(simp add: array_length_ahm_rehash_aux')
from invD(1,2)[OF this] have bucket: "bucket_ok bhc ?l h (array_get a h)"
and dist: "distinct (map fst (array_get a h))"
by (simp_all add: list_map_invar_def)
let ?h = "bhc (array_length a) k"
from hlen bucket show "bucket_ok bhc (array_length ?a) h (array_get ?a h)"
by(cases "h = ?h")(auto simp add: ahm_rehash_aux'_def Let_def array_length_ahm_rehash_aux' array_get_array_set_other dest: bucket_okD intro!: bucket_okI)
from dist hlen fresh
show "list_map_invar (array_get ?a h)"
unfolding list_map_invar_def
by(cases "h = ?h")(auto simp add: ahm_rehash_aux'_def Let_def array_get_array_set_other)
next
let ?f = "λn kvs. n + length kvs"
{ fix n :: nat and xs :: "('a × 'b) list list"
have "foldl ?f n xs = n + foldl ?f 0 xs"
by(induct xs arbitrary: rule: rev_induct) simp_all }
note fold = this
let ?h = "bhc (array_length a) k"
obtain xs where a [simp]: "a = Array xs" by(cases a)
from inv and bhc have [simp]: "bhc (length xs) k < length xs"
by (force simp add: ahm_invar_aux_def)
have xs: "xs = take ?h xs @ (xs ! ?h) # drop (Suc ?h) xs" by(simp add: nth_drop')
from inv have "n = array_foldl (λ_ n kvs. n + length kvs) 0 a"
by(auto elim: ahm_invar_auxE)
hence "n = foldl ?f 0 (take ?h xs) + length (xs ! ?h) + foldl ?f 0 (drop (Suc ?h) xs)"
by(simp add: array_foldl_foldl)(subst xs, simp, subst (1 2 3 4) fold, simp)
thus "Suc n = array_foldl (λ_ n kvs. n + length kvs) 0 ?a"
by(simp add: ahm_rehash_aux'_def Let_def array_foldl_foldl foldl_list_update)(subst (1 2 3 4) fold, simp)
next
from inv have "1 < array_length a" by(auto elim: ahm_invar_auxE)
thus "1 < array_length ?a" by(simp add: array_length_ahm_rehash_aux')
qed
lemma ahm_rehash_aux_correct:
fixes a :: "('k×'v) list array"
assumes bhc: "is_bounded_hashcode Id op= bhc"
and inv: "ahm_invar_aux bhc n a"
and "sz > 1"
shows "ahm_invar_aux bhc n (ahm_rehash_aux bhc a sz)" (is "?thesis1")
and "ahm_α_aux bhc (ahm_rehash_aux bhc a sz) = ahm_α_aux bhc a" (is "?thesis2")
proof -
thm ahm_rehash_aux'_def
let ?a = "ahm_rehash_aux bhc a sz"
def I ≡ "λit a'.
ahm_invar_aux bhc (n - card it) a'
∧ array_length a' = sz
∧ (∀k. if k ∈ it then
ahm_α_aux bhc a' k = None
else ahm_α_aux bhc a' k = ahm_α_aux bhc a k)"
note iterator_rule = map_iterator_no_cond_rule_P[
OF ahm_iteratei_aux_impl[OF inv bhc],
of I "new_array [] sz" "ahm_rehash_aux' bhc sz" "I {}"]
from inv have "I {} ?a" unfolding ahm_rehash_aux_def
proof(intro iterator_rule)
from ahm_invar_aux_card_dom_ahm_α_auxD[OF bhc inv]
have "card (dom (ahm_α_aux bhc a)) = n" .
moreover from ahm_invar_aux_new_array[OF `1 < sz`]
have "ahm_invar_aux bhc 0 (new_array ([]::('k×'v) list) sz)" .
moreover {
fix k
assume "k ∉ dom (ahm_α_aux bhc a)"
hence "ahm_α_aux bhc a k = None" by auto
hence "ahm_α_aux bhc (new_array [] sz) k = ahm_α_aux bhc a k"
using assms by simp
}
ultimately show "I (dom (ahm_α_aux bhc a)) (new_array [] sz)"
using assms by (simp add: I_def)
next
fix k :: 'k
and v :: 'v
and it a'
assume "k ∈ it" "ahm_α_aux bhc a k = Some v"
and it_sub: "it ⊆ dom (ahm_α_aux bhc a)"
and I: "I it a'"
from I have inv': "ahm_invar_aux bhc (n - card it) a'"
and a'_eq_a: "!!k. k ∉ it ==> ahm_α_aux bhc a' k = ahm_α_aux bhc a k"
and a'_None: "!!k. k ∈ it ==> ahm_α_aux bhc a' k = None"
and [simp]: "sz = array_length a'"
by (auto split: split_if_asm simp: I_def)
from it_sub finite_dom_ahm_α_aux[OF bhc inv]
have "finite it" by(rule finite_subset)
moreover with `k ∈ it` have "card it > 0" by (auto simp add: card_gt_0_iff)
moreover from finite_dom_ahm_α_aux[OF bhc inv] it_sub
have "card it ≤ card (dom (ahm_α_aux bhc a))" by (rule card_mono)
moreover have "… = n" using inv
by(simp add: ahm_invar_aux_card_dom_ahm_α_auxD[OF bhc])
ultimately have "n - card (it - {k}) = (n - card it) + 1"
using `k ∈ it` by auto
moreover from `k ∈ it` have "ahm_α_aux bhc a' k = None" by (rule a'_None)
hence "k ∉ fst ` set (array_get a' (bhc (array_length a') k))"
by (simp add: ahm_α_aux_def2 map_of_eq_None_iff)
ultimately have "ahm_invar_aux bhc (n - card (it - {k}))
(ahm_rehash_aux' bhc sz (k, v) a')"
using ahm_rehash_aux'_preserves_ahm_invar_aux[OF inv' bhc] by simp
moreover have "array_length (ahm_rehash_aux' bhc sz (k, v) a') = sz"
by (simp add: array_length_ahm_rehash_aux')
moreover {
fix k'
assume "k' ∈ it - {k}"
with is_bounded_hashcodeD(3)[OF bhc `1 < sz`, of k'] a'_None[of k']
have "ahm_α_aux bhc (ahm_rehash_aux' bhc sz (k, v) a') k' = None"
unfolding ahm_α_aux_def2
by (cases "bhc sz k = bhc sz k'") (simp_all add:
array_get_array_set_other ahm_rehash_aux'_def Let_def)
} moreover {
fix k'
assume "k' ∉ it - {k}"
with is_bounded_hashcodeD(3)[OF bhc `1 < sz`, of k]
is_bounded_hashcodeD(3)[OF bhc `1 < sz`, of k']
a'_eq_a[of k'] `k ∈ it`
have "ahm_α_aux bhc (ahm_rehash_aux' bhc sz (k, v) a') k' =
ahm_α_aux bhc a k'"
unfolding ahm_rehash_aux'_def Let_def
using `ahm_α_aux bhc a k = Some v`
unfolding ahm_α_aux_def2
by(cases "bhc sz k = bhc sz k'") (case_tac [!] "k' = k",
simp_all add: array_get_array_set_other)
}
ultimately show "I (it - {k}) (ahm_rehash_aux' bhc sz (k, v) a')"
unfolding I_def by simp
qed simp_all
thus ?thesis1 ?thesis2 unfolding ahm_rehash_aux_def I_def by auto
qed
lemma ahm_rehash_correct:
fixes hm :: "('k, 'v) hashmap"
assumes bhc: "is_bounded_hashcode Id op= bhc"
and inv: "ahm_invar bhc hm"
and "sz > 1"
shows "ahm_invar bhc (ahm_rehash bhc hm sz)"
"ahm_α bhc (ahm_rehash bhc hm sz) = ahm_α bhc hm"
proof-
obtain a n where [simp]: "hm = HashMap a n" by (cases hm)
from inv have "ahm_invar_aux bhc n a" by simp
from ahm_rehash_aux_correct[OF bhc this `sz > 1`]
show "ahm_invar bhc (ahm_rehash bhc hm sz)" and
"ahm_α bhc (ahm_rehash bhc hm sz) = ahm_α bhc hm"
by (simp_all add: ahm_α_def2)
qed
subsection {* @{term ahm_update} *}
lemma param_hm_grow[param]:
"(hm_grow, hm_grow) ∈ ⟨Rk,Rv⟩ahm_map_rel -> nat_rel"
unfolding hm_grow_def[abs_def] rec_hashmap_is_case by parametricity
lemma param_ahm_rehash_aux'[param]:
assumes "is_bounded_hashcode Rk eq bhc"
assumes "1 < n"
assumes "(bhc,bhc') ∈ nat_rel -> Rk -> nat_rel"
assumes "(n,n') ∈ nat_rel" and "n = array_length a"
assumes "(kv,kv') ∈ ⟨Rk,Rv⟩prod_rel"
assumes "(a,a') ∈ ⟨⟨⟨Rk,Rv⟩prod_rel⟩list_rel⟩array_rel"
shows "(ahm_rehash_aux' bhc n kv a, ahm_rehash_aux' bhc' n' kv' a') ∈
⟨⟨⟨Rk,Rv⟩prod_rel⟩list_rel⟩array_rel"
proof-
from assms have "bhc n (fst kv) < array_length a" by force
thus ?thesis unfolding ahm_rehash_aux'_def[abs_def]
rec_hashmap_is_case Let_def using assms by parametricity
qed
lemma param_new_array[param]:
"(new_array, new_array) ∈ R -> nat_rel -> ⟨R⟩array_rel"
unfolding new_array_def[abs_def] by parametricity
lemma param_foldli_induct:
assumes l: "(l,l') ∈ ⟨Ra⟩list_rel"
assumes c: "(c,c') ∈ Rb -> bool_rel"
assumes σ: "(σ,σ') ∈ Rb"
assumes Pσ: "P σ σ'"
assumes f: "!!a a' b b'. (a,a')∈Ra ==> (b,b')∈Rb ==> c b ==> c' b' ==>
P b b' ==> (f a b, f' a' b') ∈ Rb ∧
P (f a b) (f' a' b')"
shows "(foldli l c f σ, foldli l' c' f' σ') ∈ Rb"
using c σ Pσ f by (induction arbitrary: σ σ' rule: list_rel_induct[OF l],
auto dest!: fun_relD)
lemma param_foldli_induct_nocond:
assumes l: "(l,l') ∈ ⟨Ra⟩list_rel"
assumes σ: "(σ,σ') ∈ Rb"
assumes Pσ: "P σ σ'"
assumes f: "!!a a' b b'. (a,a')∈Ra ==> (b,b')∈Rb ==> P b b' ==>
(f a b, f' a' b') ∈ Rb ∧ P (f a b) (f' a' b')"
shows "(foldli l (λ_. True) f σ, foldli l' (λ_. True) f' σ') ∈ Rb"
using assms by (blast intro: param_foldli_induct)
lemma param_ahm_rehash_aux[param]:
assumes bhc: "is_bounded_hashcode Rk eq bhc"
assumes bhc_rel: "(bhc,bhc') ∈ nat_rel -> Rk -> nat_rel"
assumes A: "(a,a') ∈ ⟨⟨⟨Rk,Rv⟩prod_rel⟩list_rel⟩array_rel"
assumes N: "(n,n') ∈ nat_rel" "1 < n"
shows "(ahm_rehash_aux bhc a n, ahm_rehash_aux bhc' a' n') ∈
⟨⟨⟨Rk,Rv⟩prod_rel⟩list_rel⟩array_rel"
proof-
obtain l l' where [simp]: "a = Array l" "a' = Array l'"
by (cases a, cases a')
from A have L: "(l,l') ∈ ⟨⟨⟨Rk,Rv⟩prod_rel⟩list_rel⟩list_rel"
unfolding array_rel_def by simp
hence L': "(concat l, concat l') ∈ ⟨⟨Rk,Rv⟩prod_rel⟩list_rel"
by parametricity
let ?P = "λa a'. n = array_length a"
note induct_rule = param_foldli_induct_nocond[OF L', where P="?P"]
show ?thesis unfolding ahm_rehash_aux_def
by (simp, induction rule: induct_rule, insert N bhc bhc_rel,
auto intro: param_new_array[param_fo]
param_ahm_rehash_aux'[param_fo]
simp: array_length_ahm_rehash_aux')
qed
lemma param_ahm_rehash[param]:
assumes bhc: "is_bounded_hashcode Rk eq bhc"
assumes bhc_rel: "(bhc,bhc') ∈ nat_rel -> Rk -> nat_rel"
assumes M: "(m,m') ∈ ⟨Rk,Rv⟩ahm_map_rel"
assumes N: "(n,n') ∈ nat_rel" "1 < n"
shows "(ahm_rehash bhc m n, ahm_rehash bhc' m' n') ∈
⟨Rk,Rv⟩ahm_map_rel"
proof-
obtain a a' k k' where [simp]: "m = HashMap a k" "m' = HashMap a' k'"
by (cases m, cases m')
hence K: "(k,k') ∈ nat_rel" and
A: "(a,a') ∈ ⟨⟨⟨Rk,Rv⟩prod_rel⟩list_rel⟩array_rel"
using M unfolding ahm_map_rel_def by simp_all
show ?thesis unfolding ahm_rehash_def
by (simp, insert K A assms, parametricity)
qed
lemma param_load_factor[param]:
"(load_factor, load_factor) ∈ nat_rel"
unfolding load_factor_def by simp
lemma param_ahm_filled[param]:
"(ahm_filled, ahm_filled) ∈ ⟨Rk,Rv⟩ahm_map_rel -> bool_rel"
unfolding ahm_filled_def[abs_def] rec_hashmap_is_case
by parametricity
lemma param_ahm_update_aux[param]:
assumes bhc: "is_bounded_hashcode Rk eq bhc"
assumes bhc_rel: "(bhc,bhc') ∈ nat_rel -> Rk -> nat_rel"
assumes inv: "ahm_invar bhc' m'"
assumes K: "(k,k') ∈ Rk"
assumes V: "(v,v') ∈ Rv"
assumes M: "(m,m') ∈ ⟨Rk,Rv⟩ahm_map_rel"
shows "(ahm_update_aux eq bhc m k v,
ahm_update_aux op= bhc' m' k' v' ) ∈ ⟨Rk,Rv⟩ahm_map_rel"
proof-
from bhc have eq[param]: "(eq, op=)∈Rk -> Rk -> bool_rel" by (simp add: is_bounded_hashcodeD)
obtain a a' n n' where
[simp]: "m = HashMap a n" and [simp]: "m' = HashMap a' n'"
by (cases m, cases m')
from M have A: "(a,a') ∈ ⟨⟨⟨Rk,Rv⟩prod_rel⟩list_rel⟩array_rel" and
N: "(n,n') ∈ nat_rel"
unfolding ahm_map_rel_def by simp_all
from inv have "1 < array_length a'"
unfolding ahm_invar_def ahm_invar_aux_def by force
hence "1 < array_length a"
by (simp add: array_rel_imp_same_length[OF A])
with bhc have bhc_range: "bhc (array_length a) k < array_length a" by blast
have option_compare: "!!a a'. (a,a') ∈ ⟨Rv⟩option_rel ==>
(a = None,a' = None) ∈ bool_rel" by force
have "(array_get a (bhc (array_length a) k),
array_get a' (bhc' (array_length a') k')) ∈
⟨⟨Rk,Rv⟩prod_rel⟩list_rel"
using A K bhc_rel bhc_range by parametricity
note cmp = option_compare[OF param_list_map_lookup[param_fo, OF eq K this]]
show ?thesis apply simp
unfolding ahm_update_aux_def Let_def rec_hashmap_is_case
using assms A N bhc_range cmp by parametricity
qed
lemma param_ahm_update[param]:
assumes bhc: "is_bounded_hashcode Rk eq bhc"
assumes bhc_rel: "(bhc,bhc') ∈ nat_rel -> Rk -> nat_rel"
assumes inv: "ahm_invar bhc' m'"
assumes K: "(k,k') ∈ Rk"
assumes V: "(v,v') ∈ Rv"
assumes M: "(m,m') ∈ ⟨Rk,Rv⟩ahm_map_rel"
shows "(ahm_update eq bhc k v m, ahm_update op= bhc' k' v' m') ∈
⟨Rk,Rv⟩ahm_map_rel"
proof-
have "1 < hm_grow (ahm_update_aux eq bhc m k v)" by simp
with assms show ?thesis unfolding ahm_update_def[abs_def] Let_def
by parametricity
qed
lemma length_list_map_update:
"length (list_map_update op= k v xs) =
(if list_map_lookup op= k xs = None then Suc (length xs) else length xs)"
(is "?l_new = _")
proof (cases "list_map_lookup op= k xs", simp_all)
case None
hence "k ∉ dom (map_of xs)" by (force simp: list_map_lookup_is_map_of)
hence "!!a. list_map_update_aux op= k v xs a = (k,v) # rev xs @ a"
by (induction xs, auto)
thus "?l_new = Suc (length xs)" unfolding list_map_update_def by simp
next
case (Some v')
hence "(k,v') ∈ set xs" unfolding list_map_lookup_is_map_of
by (rule map_of_is_SomeD)
hence "!!a. length (list_map_update_aux op= k v xs a) =
length xs + length a" by (induction xs, auto)
thus "?l_new = length xs" unfolding list_map_update_def by simp
qed
lemma length_list_map_delete:
"length (list_map_delete op= k xs) =
(if list_map_lookup op= k xs = None then length xs else length xs - 1)"
(is "?l_new = _")
proof (cases "list_map_lookup op= k xs", simp_all)
case None
hence "k ∉ dom (map_of xs)" by (force simp: list_map_lookup_is_map_of)
hence "!!a. list_map_delete_aux op= k xs a = rev xs @ a"
by (induction xs, auto)
thus "?l_new = length xs" unfolding list_map_delete_def by simp
next
case (Some v')
hence "(k,v') ∈ set xs" unfolding list_map_lookup_is_map_of
by (rule map_of_is_SomeD)
hence "!!a. k ∉ fst`set a ==> length (list_map_delete_aux op= k xs a) =
length xs + length a - 1" by (induction xs, auto)
thus "?l_new = length xs - Suc 0" unfolding list_map_delete_def by simp
qed
lemma ahm_update_impl:
assumes bhc: "is_bounded_hashcode Id op= bhc"
shows "(ahm_update op= bhc, op_map_update) ∈ (Id::('k×'k) set) ->
(Id::('v×'v) set) -> ahm_map_rel' bhc -> ahm_map_rel' bhc"
proof (intro fun_relI, clarsimp)
fix k::'k and v::'v and hm::"('k,'v) hashmap" and m::"'k\<rightharpoonup>'v"
assume "(hm,m) ∈ ahm_map_rel' bhc"
hence α: "m = ahm_α bhc hm" and inv: "ahm_invar bhc hm"
unfolding ahm_map_rel'_def br_def by simp_all
obtain a n where [simp]: "hm = HashMap a n" by (cases hm)
have K: "(k,k) ∈ Id" and V: "(v,v) ∈ Id" by simp_all
from inv have [simp]: "1 < array_length a"
unfolding ahm_invar_def ahm_invar_aux_def by simp
hence bhc_range[simp]: "!!k. bhc (array_length a) k < array_length a"
using bhc by blast
let ?l = "array_length a"
let ?h = "bhc (array_length a) k"
let ?a' = "array_set a ?h (list_map_update op= k v (array_get a ?h))"
let ?n' = "if list_map_lookup op= k (array_get a ?h) = None
then n + 1 else n"
let ?list = "array_get a (bhc ?l k)"
let ?list' = "map_of ?list"
have L: "(?list, ?list') ∈ br map_of list_map_invar"
using inv unfolding ahm_invar_def ahm_invar_aux_def br_def by simp
hence list: "list_map_invar ?list" by (simp_all add: br_def)
let ?list_new = "list_map_update op= k v ?list"
let ?list_new' = "op_map_update k v (map_of (?list))"
from list_map_autoref_update2[param_fo, OF K V L]
have list_updated: "map_of ?list_new = ?list_new'"
"list_map_invar ?list_new" unfolding br_def by simp_all
have "ahm_invar bhc (HashMap ?a' ?n')" unfolding ahm_invar.simps
proof(rule ahm_invar_auxI)
fix h
assume "h < array_length ?a'"
hence h_in_range: "h < array_length a" by simp
with inv have bucket_ok: "bucket_ok bhc ?l h (array_get a h)"
by(auto elim: ahm_invar_auxD)
thus "bucket_ok bhc (array_length ?a') h (array_get ?a' h)"
proof (cases "h = bhc (array_length a) k")
case False
with bucket_ok show ?thesis
by (intro bucket_okI, force simp add:
array_get_array_set_other dest: bucket_okD)
next
case True
show ?thesis
proof (insert True, simp, intro bucket_okI)
case (goal1 k')
show ?case
proof (cases "k = k'")
case False
from goal1 have "k' ∈ dom ?list_new'"
by (simp only: dom_map_of_conv_image_fst
list_updated(1)[symmetric])
hence "k' ∈ fst`set ?list" using False
by (simp add: dom_map_of_conv_image_fst)
from imageE[OF this] obtain x where
"fst x = k'" and "x ∈ set ?list" by force
then obtain v' where "(k',v') ∈ set ?list"
by (cases x, simp)
with bucket_okD[OF bucket_ok] and
`h = bhc (array_length a) k`
show ?thesis by simp
qed simp
qed
qed
from `h < array_length a` inv have "list_map_invar (array_get a h)"
by(auto dest: ahm_invar_auxD)
with `h < array_length a`
show "list_map_invar (array_get ?a' h)"
by (cases "h = ?h", simp_all add:
list_updated array_get_array_set_other)
next
obtain xs where a [simp]: "a = Array xs" by(cases a)
let ?f = "λn kvs. n + length kvs"
{ fix n :: nat and xs :: "('k × 'v) list list"
have "foldl ?f n xs = n + foldl ?f 0 xs"
by(induct xs arbitrary: rule: rev_induct) simp_all }
note fold = this
from inv have [simp]: "bhc (length xs) k < length xs"
using bhc_range by simp
have xs: "xs = take ?h xs @ (xs ! ?h) # drop (Suc ?h) xs"
by(simp add: nth_drop')
from inv have "n = array_foldl (λ_ n kvs. n + length kvs) 0 a"
by (force dest: ahm_invar_auxD)
hence "n = foldl ?f 0 (take ?h xs) + length (xs ! ?h) + foldl ?f 0 (drop (Suc ?h) xs)"
apply (simp add: array_foldl_foldl)
apply (subst xs)
apply simp
apply (metis fold)
done
thus "?n' = array_foldl (λ_ n kvs. n + length kvs) 0 ?a'"
apply(simp add: ahm_rehash_aux'_def Let_def array_foldl_foldl foldl_list_update map_of_eq_None_iff)
apply(subst (1 2 3 4 5 6 7 8) fold)
apply(simp add: length_list_map_update)
done
next
from inv have "1 < array_length a" by(auto elim: ahm_invar_auxE)
thus "1 < array_length ?a'" by simp
next
qed
moreover have "ahm_α bhc (ahm_update_aux op= bhc hm k v) =
ahm_α bhc hm(k \<mapsto> v)"
proof
fix k'
show "ahm_α bhc (ahm_update_aux op= bhc hm k v) k' = (ahm_α bhc hm(k \<mapsto> v)) k'"
proof (cases "bhc ?l k = bhc ?l k'")
case False
thus ?thesis by (force simp add: Let_def
ahm_α_def array_get_array_set_other)
next
case True
hence "bhc ?l k' = bhc ?l k" by simp
thus ?thesis by (auto simp add: Let_def ahm_α_def
list_map_lookup_is_map_of list_updated)
qed
qed
ultimately have ref: "(ahm_update_aux op= bhc hm k v,
m(k \<mapsto> v)) ∈ ahm_map_rel' bhc" (is "(?hm',_)∈_")
unfolding ahm_map_rel'_def br_def using α by (auto simp: Let_def)
show "(ahm_update op= bhc k v hm, m(k \<mapsto> v))
∈ ahm_map_rel' bhc"
proof (cases "ahm_filled ?hm'")
case False
with ref show ?thesis unfolding ahm_update_def
by (simp del: ahm_update_aux.simps)
next
case True
from ref have "(ahm_rehash bhc ?hm' (hm_grow ?hm'), m(k \<mapsto> v)) ∈
ahm_map_rel' bhc" unfolding ahm_map_rel'_def br_def
by (simp del: ahm_update_aux.simps
add: ahm_rehash_correct[OF bhc])
thus ?thesis unfolding ahm_update_def using True
by (simp del: ahm_update_aux.simps add: Let_def)
qed
qed
lemma autoref_ahm_update[autoref_rules]:
assumes bhc[unfolded autoref_tag_defs]:
"SIDE_GEN_ALGO (is_bounded_hashcode Rk eq bhc)"
shows "(ahm_update eq bhc, op_map_update) ∈
Rk -> Rv -> ⟨Rk,Rv⟩ahm_rel bhc -> ⟨Rk,Rv⟩ahm_rel bhc"
proof (intro fun_relI)
let ?bhc' = "abstract_bounded_hashcode Rk bhc"
fix k k' v v' a m'
assume K: "(k,k') ∈ Rk" and V: "(v,v') ∈ Rv"
assume M: "(a,m') ∈ ⟨Rk,Rv⟩ahm_rel bhc"
with bhc have bhc': "is_bounded_hashcode Id op= ?bhc'" by blast
from abstract_bhc_correct[OF bhc]
have bhc_rel: "(bhc,?bhc') ∈ nat_rel -> Rk -> nat_rel" .
from M obtain a' where M1: "(a,a') ∈ ⟨Rk,Rv⟩ahm_map_rel" and
M2: "(a',m') ∈ ahm_map_rel' ?bhc'" unfolding ahm_rel_def by blast
hence inv: "ahm_invar ?bhc' a'"
unfolding ahm_map_rel'_def br_def by simp
from relcompI[OF param_ahm_update[OF bhc bhc_rel inv K V M1]
ahm_update_impl[param_fo, OF bhc' _ _ M2]]
show "(ahm_update eq bhc k v a, op_map_update k' v' m') ∈
⟨Rk,Rv⟩ahm_rel bhc" unfolding ahm_rel_def by simp
qed
subsection {* @{term "ahm_delete"} *}
lemma param_ahm_delete[param]:
assumes isbhc: "is_bounded_hashcode Rk eq bhc"
assumes bhc: "(bhc,bhc') ∈ nat_rel -> Rk -> nat_rel"
assumes inv: "ahm_invar bhc' m'"
assumes K: "(k,k') ∈ Rk"
assumes M: "(m,m') ∈ ⟨Rk,Rv⟩ahm_map_rel"
shows
"(ahm_delete eq bhc k m, ahm_delete op= bhc' k' m') ∈
⟨Rk,Rv⟩ahm_map_rel"
proof-
from isbhc have eq: "(eq,op=)∈Rk->Rk->bool_rel" by (simp add: is_bounded_hashcodeD)
obtain a a' n n' where
[simp]: "m = HashMap a n" and [simp]: "m' = HashMap a' n'"
by (cases m, cases m')
from M have A: "(a,a') ∈ ⟨⟨⟨Rk,Rv⟩prod_rel⟩list_rel⟩array_rel" and
N: "(n,n') ∈ nat_rel"
unfolding ahm_map_rel_def by simp_all
from inv have "1 < array_length a'"
unfolding ahm_invar_def ahm_invar_aux_def by force
hence "1 < array_length a"
by (simp add: array_rel_imp_same_length[OF A])
with isbhc have bhc_range: "bhc (array_length a) k < array_length a" by blast
have option_compare: "!!a a'. (a,a') ∈ ⟨Rv⟩option_rel ==>
(a = None,a' = None) ∈ bool_rel" by force
have "(array_get a (bhc (array_length a) k),
array_get a' (bhc' (array_length a') k')) ∈
⟨⟨Rk,Rv⟩prod_rel⟩list_rel"
using A K bhc bhc_range by parametricity
note cmp = option_compare[OF param_list_map_lookup[param_fo, OF eq K this]]
show ?thesis unfolding `m = HashMap a n` `m' = HashMap a' n'`
by (simp only: ahm_delete.simps Let_def,
insert eq isbhc bhc K A N bhc_range cmp, parametricity)
qed
lemma ahm_delete_impl:
assumes bhc: "is_bounded_hashcode Id op= bhc"
shows "(ahm_delete op= bhc, op_map_delete) ∈ (Id::('k×'k) set) ->
ahm_map_rel' bhc -> ahm_map_rel' bhc"
proof (intro fun_relI, clarsimp)
fix k::'k and hm::"('k,'v) hashmap" and m::"'k\<rightharpoonup>'v"
assume "(hm,m) ∈ ahm_map_rel' bhc"
hence α: "m = ahm_α bhc hm" and inv: "ahm_invar bhc hm"
unfolding ahm_map_rel'_def br_def by simp_all
obtain a n where [simp]: "hm = HashMap a n" by (cases hm)
have K: "(k,k) ∈ Id" by simp
from inv have [simp]: "1 < array_length a"
unfolding ahm_invar_def ahm_invar_aux_def by simp
hence bhc_range[simp]: "!!k. bhc (array_length a) k < array_length a"
using bhc by blast
let ?l = "array_length a"
let ?h = "bhc ?l k"
let ?a' = "array_set a ?h (list_map_delete op= k (array_get a ?h))"
let ?n' = "if list_map_lookup op= k (array_get a ?h) = None then n else n - 1"
let ?list = "array_get a ?h" let ?list' = "map_of ?list"
let ?list_new = "list_map_delete op= k ?list"
let ?list_new' = "?list' |` (-{k})"
from inv have "(?list, ?list') ∈ br map_of list_map_invar"
unfolding br_def ahm_invar_def ahm_invar_aux_def by simp
from list_map_autoref_delete2[param_fo, OF K this]
have list_updated: "map_of ?list_new = ?list_new'"
"list_map_invar ?list_new" by (simp_all add: br_def)
have [simp]: "array_length ?a' = ?l" by simp
have "ahm_invar_aux bhc ?n' ?a'"
proof(rule ahm_invar_auxI)
fix h
assume "h < array_length ?a'"
hence h_in_range[simp]: "h < array_length a" by simp
with inv have inv': "bucket_ok bhc ?l h (array_get a h)" "1 < ?l"
"list_map_invar (array_get a h)" by (auto elim: ahm_invar_auxE)
show "bucket_ok bhc (array_length ?a') h (array_get ?a' h)"
proof (cases "h = bhc ?l k")
case False thus ?thesis using inv'
by (simp add: array_get_array_set_other)
next
case True thus ?thesis
proof (simp, intro bucket_okI)
case (goal1 k')
show ?case
proof (cases "k = k'")
case False
from goal1 have "k' ∈ dom ?list_new'"
by (simp only: dom_map_of_conv_image_fst
list_updated(1)[symmetric])
hence "k' ∈ fst`set ?list" using False
by (simp add: dom_map_of_conv_image_fst)
from imageE[OF this] obtain x where
"fst x = k'" and "x ∈ set ?list" by force
then obtain v' where "(k',v') ∈ set ?list"
by (cases x, simp)
with bucket_okD[OF inv'(1)] and
`h = bhc (array_length a) k`
show ?thesis by blast
qed simp
qed
qed
from inv'(3) `h < array_length a`
show "list_map_invar (array_get ?a' h)"
by (cases "h = ?h", simp_all add:
list_updated array_get_array_set_other)
next
obtain xs where a [simp]: "a = Array xs" by(cases a)
let ?f = "λn kvs. n + length (kvs::('k×'v) list)"
{ fix n :: nat and xs :: "('k×'v) list list"
have "foldl ?f n xs = n + foldl ?f 0 xs"
by(induct xs arbitrary: rule: rev_induct) simp_all }
note fold = this
from bhc_range have [simp]: "bhc (length xs) k < length xs" by simp
moreover
have xs: "xs = take ?h xs @ (xs ! ?h) # drop (Suc ?h) xs" by(simp add: nth_drop')
from inv have "n = array_foldl (λ_ n kvs. n + length kvs) 0 a"
by(auto elim: ahm_invar_auxE)
hence "n = foldl ?f 0 (take ?h xs) + length (xs ! ?h) + foldl ?f 0 (drop (Suc ?h) xs)"
by(simp add: array_foldl_foldl)(subst xs, simp, subst (1 2 3 4) fold, simp)
moreover have "!!v a b. list_map_lookup op= k (xs ! ?h) = Some v
==> a + (length (xs ! ?h) - 1) + b = a + length (xs ! ?h) + b - 1"
by (cases "xs ! ?h", simp_all)
ultimately show "?n' = array_foldl (λ_ n kvs. n + length kvs) 0 ?a'"
apply(simp add: array_foldl_foldl foldl_list_update map_of_eq_None_iff)
apply(subst (1 2 3 4 5 6 7 8) fold)
apply (intro conjI impI)
apply(auto simp add: length_list_map_delete)
done
next
from inv show "1 < array_length ?a'" by(auto elim: ahm_invar_auxE)
qed
hence "ahm_invar bhc (HashMap ?a' ?n')" by simp
moreover have "ahm_α_aux bhc ?a' = ahm_α_aux bhc a |` (- {k})"
proof
fix k' :: 'k
show "ahm_α_aux bhc ?a' k' = (ahm_α_aux bhc a |` (- {k})) k'"
proof (cases "bhc ?l k' = ?h")
case False
hence "k ≠ k'" by force
thus ?thesis using False unfolding ahm_α_aux_def
by (simp add: array_get_array_set_other
list_map_lookup_is_map_of)
next
case True
thus ?thesis unfolding ahm_α_aux_def
by (simp add: list_map_lookup_is_map_of
list_updated(1) restrict_map_def)
qed
qed
hence "ahm_α bhc (HashMap ?a' ?n') = op_map_delete k m"
unfolding op_map_delete_def by (simp add: ahm_α_def2 α)
ultimately have "(HashMap ?a' ?n', op_map_delete k m) ∈ ahm_map_rel' bhc"
unfolding ahm_map_rel'_def br_def by simp
thus "(ahm_delete op= bhc k hm, m |` (-{k})) ∈ ahm_map_rel' bhc"
by (simp only: `hm = HashMap a n` ahm_delete.simps Let_def
op_map_delete_def, force)
qed
lemma autoref_ahm_delete[autoref_rules]:
assumes bhc[unfolded autoref_tag_defs]:
"SIDE_GEN_ALGO (is_bounded_hashcode Rk eq bhc)"
shows "(ahm_delete eq bhc, op_map_delete) ∈
Rk -> ⟨Rk,Rv⟩ahm_rel bhc -> ⟨Rk,Rv⟩ahm_rel bhc"
proof (intro fun_relI)
let ?bhc' = "abstract_bounded_hashcode Rk bhc"
fix k k' a m'
assume K: "(k,k') ∈ Rk"
assume M: "(a,m') ∈ ⟨Rk,Rv⟩ahm_rel bhc"
with bhc have bhc': "is_bounded_hashcode Id op= ?bhc'" by blast
from abstract_bhc_correct[OF bhc]
have bhc_rel: "(bhc,?bhc') ∈ nat_rel -> Rk -> nat_rel" .
from M obtain a' where M1: "(a,a') ∈ ⟨Rk,Rv⟩ahm_map_rel" and
M2: "(a',m') ∈ ahm_map_rel' ?bhc'" unfolding ahm_rel_def by blast
hence inv: "ahm_invar ?bhc' a'"
unfolding ahm_map_rel'_def br_def by simp
from relcompI[OF param_ahm_delete[OF bhc bhc_rel inv K M1]
ahm_delete_impl[param_fo, OF bhc' _ M2]]
show "(ahm_delete eq bhc k a, op_map_delete k' m') ∈
⟨Rk,Rv⟩ahm_rel bhc" unfolding ahm_rel_def by simp
qed
subsection {* Various simple operations *}
lemma param_ahm_isEmpty[param]:
"(ahm_isEmpty, ahm_isEmpty) ∈ ⟨Rk,Rv⟩ahm_map_rel -> bool_rel"
unfolding ahm_isEmpty_def[abs_def] rec_hashmap_is_case
by parametricity
lemma param_ahm_isSng[param]:
"(ahm_isSng, ahm_isSng) ∈ ⟨Rk,Rv⟩ahm_map_rel -> bool_rel"
unfolding ahm_isSng_def[abs_def] rec_hashmap_is_case
by parametricity
lemma param_ahm_size[param]:
"(ahm_size, ahm_size) ∈ ⟨Rk,Rv⟩ahm_map_rel -> nat_rel"
unfolding ahm_size_def[abs_def] rec_hashmap_is_case
by parametricity
lemma ahm_isEmpty_impl:
assumes "is_bounded_hashcode Id op= bhc"
shows "(ahm_isEmpty, op_map_isEmpty) ∈ ahm_map_rel' bhc -> bool_rel"
proof (intro fun_relI)
fix hm m assume rel: "(hm,m) ∈ ahm_map_rel' bhc"
obtain a n where [simp]: "hm = HashMap a n" by (cases hm)
from rel have α: "m = ahm_α_aux bhc a" and inv: "ahm_invar_aux bhc n a"
unfolding ahm_map_rel'_def br_def by (simp_all add: ahm_α_def2)
from ahm_invar_aux_card_dom_ahm_α_auxD[OF assms inv,symmetric] and
finite_dom_ahm_α_aux[OF assms inv]
show "(ahm_isEmpty hm, op_map_isEmpty m) ∈ bool_rel"
unfolding ahm_isEmpty_def op_map_isEmpty_def
by (simp add: α card_eq_0_iff)
qed
lemma ahm_isSng_impl:
assumes "is_bounded_hashcode Id op= bhc"
shows "(ahm_isSng, op_map_isSng) ∈ ahm_map_rel' bhc -> bool_rel"
proof (intro fun_relI)
fix hm m assume rel: "(hm,m) ∈ ahm_map_rel' bhc"
obtain a n where [simp]: "hm = HashMap a n" by (cases hm)
from rel have α: "m = ahm_α_aux bhc a" and inv: "ahm_invar_aux bhc n a"
unfolding ahm_map_rel'_def br_def by (simp_all add: ahm_α_def2)
note n_props[simp] = ahm_invar_aux_card_dom_ahm_α_auxD[OF assms inv,symmetric]
note finite_dom[simp] = finite_dom_ahm_α_aux[OF assms inv]
show "(ahm_isSng hm, op_map_isSng m) ∈ bool_rel"
by (force simp add: α[symmetric] dom_eq_singleton_conv
dest!: card_eq_SucD)
qed
lemma ahm_size_impl:
assumes "is_bounded_hashcode Id op= bhc"
shows "(ahm_size, op_map_size) ∈ ahm_map_rel' bhc -> nat_rel"
proof (intro fun_relI)
fix hm m assume rel: "(hm,m) ∈ ahm_map_rel' bhc"
obtain a n where [simp]: "hm = HashMap a n" by (cases hm)
from rel have α: "m = ahm_α_aux bhc a" and inv: "ahm_invar_aux bhc n a"
unfolding ahm_map_rel'_def br_def by (simp_all add: ahm_α_def2)
from ahm_invar_aux_card_dom_ahm_α_auxD[OF assms inv,symmetric]
show "(ahm_size hm, op_map_size m) ∈ nat_rel"
unfolding ahm_isEmpty_def op_map_isEmpty_def
by (simp add: α card_eq_0_iff)
qed
lemma autoref_ahm_isEmpty[autoref_rules]:
assumes bhc[unfolded autoref_tag_defs]:
"SIDE_GEN_ALGO (is_bounded_hashcode Rk eq bhc)"
shows "(ahm_isEmpty, op_map_isEmpty) ∈ ⟨Rk,Rv⟩ahm_rel bhc -> bool_rel"
proof (intro fun_relI)
let ?bhc' = "abstract_bounded_hashcode Rk bhc"
fix k k' a m'
assume M: "(a,m') ∈ ⟨Rk,Rv⟩ahm_rel bhc"
from bhc have bhc': "is_bounded_hashcode Id op= ?bhc'"
by blast
from M obtain a' where M1: "(a,a') ∈ ⟨Rk,Rv⟩ahm_map_rel" and
M2: "(a',m') ∈ ahm_map_rel' ?bhc'" unfolding ahm_rel_def by blast
from relcompI[OF param_ahm_isEmpty[param_fo, OF M1]
ahm_isEmpty_impl[param_fo, OF bhc' M2]]
show "(ahm_isEmpty a, op_map_isEmpty m') ∈ bool_rel" by simp
qed
lemma autoref_ahm_isSng[autoref_rules]:
assumes bhc[unfolded autoref_tag_defs]:
"SIDE_GEN_ALGO (is_bounded_hashcode Rk eq bhc)"
shows "(ahm_isSng, op_map_isSng) ∈ ⟨Rk,Rv⟩ahm_rel bhc -> bool_rel"
proof (intro fun_relI)
let ?bhc' = "abstract_bounded_hashcode Rk bhc"
fix k k' a m'
assume M: "(a,m') ∈ ⟨Rk,Rv⟩ahm_rel bhc"
from bhc have bhc': "is_bounded_hashcode Id op= ?bhc'"
by blast
from M obtain a' where M1: "(a,a') ∈ ⟨Rk,Rv⟩ahm_map_rel" and
M2: "(a',m') ∈ ahm_map_rel' ?bhc'" unfolding ahm_rel_def by blast
from relcompI[OF param_ahm_isSng[param_fo, OF M1]
ahm_isSng_impl[param_fo, OF bhc' M2]]
show "(ahm_isSng a, op_map_isSng m') ∈ bool_rel" by simp
qed
lemma autoref_ahm_size[autoref_rules]:
assumes bhc[unfolded autoref_tag_defs]:
"SIDE_GEN_ALGO (is_bounded_hashcode Rk eq bhc)"
shows "(ahm_size, op_map_size) ∈ ⟨Rk,Rv⟩ahm_rel bhc -> nat_rel"
proof (intro fun_relI)
let ?bhc' = "abstract_bounded_hashcode Rk bhc"
fix k k' a m'
assume M: "(a,m') ∈ ⟨Rk,Rv⟩ahm_rel bhc"
from bhc have bhc': "is_bounded_hashcode Id op= ?bhc'"
by blast
from M obtain a' where M1: "(a,a') ∈ ⟨Rk,Rv⟩ahm_map_rel" and
M2: "(a',m') ∈ ahm_map_rel' ?bhc'" unfolding ahm_rel_def by blast
from relcompI[OF param_ahm_size[param_fo, OF M1]
ahm_size_impl[param_fo, OF bhc' M2]]
show "(ahm_size a, op_map_size m') ∈ nat_rel" by simp
qed
lemma ahm_map_rel_sv[relator_props]:
assumes SK: "single_valued Rk"
assumes SV: "single_valued Rv"
shows "single_valued (⟨Rk, Rv⟩ahm_map_rel)"
proof -
from SK SV have 1: "single_valued (⟨⟨⟨Rk, Rv⟩prod_rel⟩list_rel⟩array_rel)"
by (tagged_solver)
thus ?thesis
unfolding ahm_map_rel_def
by (auto intro: single_valuedI dest: single_valuedD[OF 1])
qed
lemma ahm_rel_sv[relator_props]:
"[|single_valued Rk; single_valued Rv|]
==> single_valued (⟨Rk,Rv⟩ahm_rel bhc)"
unfolding ahm_rel_def ahm_map_rel'_def
by (tagged_solver (keep))
lemma rbt_map_rel_finite[relator_props]:
assumes A[simplified]: "GEN_ALGO_tag (is_bounded_hashcode Rk eq bhc)"
shows "finite_map_rel (⟨Rk,Rv⟩ahm_rel bhc)"
unfolding ahm_rel_def finite_map_rel_def ahm_map_rel'_def br_def
apply auto
apply (case_tac y)
apply (auto simp: ahm_α_def2)
thm finite_dom_ahm_α_aux
apply (rule finite_dom_ahm_α_aux)
apply (rule abstract_bhc_is_bhc)
apply (rule A)
apply assumption
done
subsection {* Proper iterator proofs *}
lemma pi_ahm[icf_proper_iteratorI]:
"proper_it (ahm_iteratei m) (ahm_iteratei m)"
proof-
obtain a n where [simp]: "m = HashMap a n" by (cases m)
then obtain l where [simp]: "a = Array l" by (cases a)
thus ?thesis
unfolding proper_it_def list_map_iteratei_def
by (simp add: ahm_iteratei_aux_def, blast)
qed
lemma pi'_ahm[icf_proper_iteratorI]:
"proper_it' ahm_iteratei ahm_iteratei"
by (rule proper_it'I, rule pi_ahm)
lemmas autoref_ahm_rules =
autoref_ahm_empty
autoref_ahm_lookup
autoref_ahm_update
autoref_ahm_delete
autoref_ahm_isEmpty
autoref_ahm_isSng
autoref_ahm_size
lemmas autoref_ahm_rules_hashable[autoref_rules_raw]
= autoref_ahm_rules[where Rk="Rk"] for Rk :: "(_×_::hashable) set"
end