# Theory Separation_Logic_Imperative_HOL.Hash_Map

```section "Hash-Maps"
theory Hash_Map
imports Hash_Table
begin

subsection ‹Auxiliary Lemmas›
lemma map_of_ls_update:
"map_of (fst (ls_update k v l)) = (map_of l)(k ↦ v)"
apply (induct l rule: ls_update.induct)
by (auto simp add: ext Let_def)

lemma map_of_concat:
"k ∈ dom (map_of(concat l))
⟹ ∃i. k ∈ dom (map_of(l!i)) ∧ i < length l"
apply (induct l)
apply simp
apply auto
apply (rule_tac x = 0 in exI)
apply auto
by (metis Suc_mono domI nth_Cons_Suc)

lemma map_of_concat':
"k ∈ dom (map_of(l!i)) ∧ i < length l ⟹ k ∈ dom (map_of(concat l))"
apply (induct l arbitrary: i)
apply simp
apply auto
apply (case_tac i)
apply auto
done

lemma map_of_concat''':
assumes "∃i. k ∈ dom (map_of(l!i)) ∧ i < length l"
shows "k ∈ dom (map_of(concat l))"
proof -
from assms obtain i where "k ∈ dom (map_of (l ! i)) ∧ i < length l" by blast
from map_of_concat'[OF this] show ?thesis .
qed

lemma map_of_concat'':
"(k ∈ dom (map_of(concat l)))
⟷ (∃i. k ∈ dom (map_of(l!i)) ∧ i < length l)"
apply rule
using map_of_concat[of k l]
apply simp
using map_of_concat'[of k l]
by blast

lemma abs_update_length: "length (abs_update k v l) = length l"
by (simp add: abs_update_def)

lemma ls_update_map_of_eq:
"map_of (fst (ls_update k v ls)) k = Some v"
apply (induct ls rule: ls_update.induct)
by (simp_all add: Let_def)

lemma ls_update_map_of_neq:
"x ≠ k ⟹ map_of (fst (ls_update k v ls)) x = map_of ls x"
apply (induct ls rule: ls_update.induct)
by (auto simp add: Let_def)

subsection ‹Main Definitions and Lemmas›

definition is_hashmap'
:: "('k, 'v) map
⇒ ('k × 'v) list list
⇒ ('k::{heap,hashable}, 'v::heap) hashtable
⇒ assn"
where
"is_hashmap' m l ht = is_hashtable l ht * ↑ (map_of (concat l) = m)"

definition is_hashmap
:: "('k, 'v) map ⇒ ('k::{heap,hashable}, 'v::heap) hashtable ⇒ assn"
where
"is_hashmap m ht = (∃⇩Al. is_hashmap' m l ht)"

lemma is_hashmap'_prec:
"∀s s'. h⊨(is_hashmap' m l ht * F1) ∧⇩A (is_hashmap' m' l' ht * F2)
⟶ l=l' ∧ m=m'"
unfolding is_hashmap'_def
apply (auto simp add: preciseD[OF is_hashtable_prec])
apply (subgoal_tac "l = l'")
by (auto simp add: preciseD[OF is_hashtable_prec])

lemma is_hashmap_prec: "precise is_hashmap"
unfolding is_hashmap_def[abs_def]
apply rule
by (auto simp add: is_hashmap'_prec)

abbreviation "hm_new ≡ ht_new"
lemma hm_new_rule':
"<emp>
hm_new::('k::{heap,hashable}, 'v::heap) hashtable Heap
<is_hashmap' Map.empty (replicate (def_hashmap_size TYPE('k)) [])>"
apply (rule cons_post_rule)
using complete_ht_new
apply simp
apply (simp add: is_hashmap'_def)
done

lemma hm_new_rule:
"<emp> hm_new <is_hashmap Map.empty>"
apply (rule cons_post_rule)
using complete_ht_new
apply simp
apply (simp add: is_hashmap_def is_hashmap'_def)
apply sep_auto
done

lemma ht_hash_distinct:
"ht_hash l
⟹ ∀i j . i≠j ∧ i < length l ∧ j < length l
⟶ set (l!i) ∩ set (l!j) = {}"
apply (auto simp add: ht_hash_def)
apply metis
done

lemma ht_hash_in_dom_in_dom_bounded_hashcode_nat:
assumes "ht_hash l"
assumes "k ∈ dom (map_of(concat l))"
shows "k ∈ dom (map_of(l!bounded_hashcode_nat (length l) k))"
proof -
from map_of_concat[OF assms(2)] obtain i
where i: "k ∈ dom (map_of (l ! i)) ∧ i < length l"
by blast
thm ht_hash_def
hence "∃v. (k,v)∈set(l!i)" by (auto dest: map_of_SomeD)
from this obtain v where v: "(k,v)∈set(l!i)" by blast
from assms(1)[unfolded ht_hash_def] i v bounded_hashcode_nat_bounds
have "bounded_hashcode_nat (length l) k = i"
by (metis fst_conv)
with i show ?thesis by simp
qed

lemma ht_hash_in_dom_bounded_hashcode_nat_in_dom:
assumes "ht_hash l"
assumes "1 < length l"
assumes "k ∈ dom (map_of(l!bounded_hashcode_nat (length l) k))"
shows "k ∈ dom (map_of(concat l))"
using map_of_concat'[of k l "bounded_hashcode_nat (length l) k"]
assms(2,3) bounded_hashcode_nat_bounds[of "length l" k]
by simp

lemma ht_hash_in_dom_in_dom_bounded_hashcode_nat_eq:
assumes "ht_hash l"
assumes "1 < length l"
shows "(k ∈ dom (map_of(concat l)))
= (k ∈ dom (map_of(l!bounded_hashcode_nat (length l) k)))"
apply rule
using ht_hash_in_dom_in_dom_bounded_hashcode_nat[OF assms(1)]
ht_hash_in_dom_bounded_hashcode_nat_in_dom[OF assms]
by simp_all

lemma ht_hash_in_dom_i_bounded_hashcode_nat_i:
assumes "ht_hash l"
assumes "1 < length l"
assumes "i < length l"
assumes "k ∈ dom (map_of (l!i))"
shows "i = bounded_hashcode_nat (length l) k"
using assms
using bounded_hashcode_nat_bounds
by (auto simp add: ht_hash_def ht_distinct_def dom_map_of_conv_image_fst)

lemma ht_hash_in_bounded_hashcode_nat_not_i_not_in_dom_i:
assumes "ht_hash l"
assumes "1 < length l"
assumes "i < length l"
assumes "i ≠ bounded_hashcode_nat (length l) k"
shows "k ∉ dom (map_of (l!i))"
using assms
using bounded_hashcode_nat_bounds
by (auto simp add: ht_hash_def ht_distinct_def dom_map_of_conv_image_fst)

lemma ht_hash_ht_distinct_in_dom_unique_value:
assumes "ht_hash l"
assumes "ht_distinct l"
assumes "1 < length l"
assumes "k ∈ dom (map_of (concat l))"
shows "∃!v. (k,v) ∈ set (concat l)"
proof -
from assms(4) have ex: "∃v. (k,v) ∈ set (concat l)"
by (auto dest!: map_of_SomeD)
have "v = w" if kv: "(k,v) ∈ set (concat l)" and kw: "(k,w) ∈ set (concat l)" for v w
proof -
from ht_hash_in_dom_in_dom_bounded_hashcode_nat[OF assms(1,4)]
have a: "k ∈ dom (map_of (l ! bounded_hashcode_nat (length l) k))" .
have "k ∉ dom(map_of(l!i))"
if "i < length l" and "i ≠ bounded_hashcode_nat (length l) k" for i
proof -
from ht_hash_in_bounded_hashcode_nat_not_i_not_in_dom_i[OF assms(1,3) that]
show ?thesis .
qed
have v: "(k,v) ∈ set (l ! bounded_hashcode_nat (length l) k)"
proof -
from kv have "∃i. i < length l ∧ (k, v) ∈ set (l!i)"
by auto (metis in_set_conv_nth)
from this obtain i where i: "i < length l ∧ (k, v) ∈ set (l!i)"
by blast
hence "k ∈ dom (map_of (l!i))"
by (metis (no_types) prod.exhaust a assms(1) fst_conv ht_hash_def)
from i ht_hash_in_dom_i_bounded_hashcode_nat_i[OF assms(1,3) _ this]
have "i = bounded_hashcode_nat (length l) k" by simp
with i show ?thesis by simp
qed
have w: "(k,w) ∈ set (l ! bounded_hashcode_nat (length l) k)"
proof -
from kw have "∃i. i < length l ∧ (k, w) ∈ set (l!i)"
by auto (metis in_set_conv_nth)
from this obtain i where i: "i < length l ∧ (k, w) ∈ set (l!i)"
by blast
hence "k ∈ dom (map_of (l!i))"
by (metis (no_types) prod.exhaust a assms(1) fst_conv ht_hash_def)
from i ht_hash_in_dom_i_bounded_hashcode_nat_i[OF assms(1,3) _ this]
have "i = bounded_hashcode_nat (length l) k" by simp
with i show ?thesis by simp
qed
from assms(2,3) have
"distinct (map fst (l ! bounded_hashcode_nat (length l) k))"
by (simp add: ht_distinct_def bounded_hashcode_nat_bounds)
from Map.map_of_is_SomeI[OF this v] Map.map_of_is_SomeI[OF this w]
show "v = w" by simp
qed
with ex show ?thesis by blast
qed

lemma ht_hash_ht_distinct_map_of:
assumes "ht_hash l"
assumes "ht_distinct l"
assumes "1 < length l"
shows "map_of (concat l) k
= map_of(l!bounded_hashcode_nat (length l) k) k"
proof (cases "k ∈ dom (map_of(concat l))")
case False
hence a: "map_of (concat l) k = None" by auto
from ht_hash_in_dom_in_dom_bounded_hashcode_nat_eq[OF assms(1,3)] False
have "k ∉ dom (map_of (l ! bounded_hashcode_nat (length l) k))" by simp
hence "map_of(l!bounded_hashcode_nat (length l) k) k = None" by auto
with a show ?thesis by simp
next
case True
from True obtain y where y: "map_of (concat l) k = Some y" by auto
hence a: "(k,y) ∈ set (concat l)" by (metis map_of_SomeD)
from ht_hash_in_dom_in_dom_bounded_hashcode_nat_eq[OF assms(1,3)] True
have "k ∈ dom (map_of (l ! bounded_hashcode_nat (length l) k))" by simp
from this obtain z where
z: "map_of(l!bounded_hashcode_nat (length l) k) k = Some z" by auto
hence "(k,z) ∈ set (l ! bounded_hashcode_nat (length l) k)"
by (metis map_of_SomeD)
with bounded_hashcode_nat_bounds[OF assms(3), of k]
have b: "(k,z) ∈ set (concat l)" by auto
from ht_hash_ht_distinct_in_dom_unique_value[OF assms True] a b
have "y = z" by auto
with y z show ?thesis by simp
qed

lemma ls_lookup_map_of_pre:
"distinct (map fst l) ⟹ ls_lookup k l = map_of l k"
apply (induct l)
apply simp
apply (case_tac a)
by simp

lemma ls_lookup_map_of:
assumes "ht_hash l"
assumes "ht_distinct l"
assumes "1 < length l"
shows "ls_lookup k (l ! bounded_hashcode_nat (length l) k)
= map_of (concat l) k"
proof -
from assms(2,3)
have "distinct (map fst (l ! bounded_hashcode_nat (length l) k))"
by (simp add: ht_distinct_def bounded_hashcode_nat_bounds)
from ls_lookup_map_of_pre[OF this]
have "ls_lookup k (l ! bounded_hashcode_nat (length l) k)
= map_of (l ! bounded_hashcode_nat (length l) k) k" .
also from ht_hash_ht_distinct_map_of[OF assms]
have "map_of (l ! bounded_hashcode_nat (length l) k) k
= map_of (concat l) k"
by simp
finally show ?thesis .
qed

abbreviation "hm_lookup ≡ ht_lookup"
lemma hm_lookup_rule':
"<is_hashmap' m l ht> hm_lookup k ht
<λr. is_hashmap' m l ht *
↑(r = m k)>"
unfolding is_hashmap'_def
apply sep_auto
apply (rule cons_post_rule)
using complete_ht_lookup[of l ht k]
apply simp
apply sep_auto
by (simp add: ls_lookup_map_of is_hashtable_def)

lemma hm_lookup_rule:
"<is_hashmap m ht> hm_lookup k ht
<λr. is_hashmap m ht *
↑(r = m k)>"
unfolding is_hashmap_def
apply sep_auto
apply (rule cons_post_rule[OF hm_lookup_rule'])
by sep_auto

lemma abs_update_map_of'':
assumes "ht_hash l"
assumes "ht_distinct l"
assumes "1 < length l"
shows "map_of (concat (abs_update k v l)) k = Some v"
proof -
from ht_hash_ht_distinct_map_of[
OF ht_hash_update[OF assms(1)]
ht_distinct_update[OF assms(2)]
length_update[OF assms(3)],
of k v k]
have "map_of (concat (abs_update k v l)) k
= map_of ((abs_update k v l) ! bounded_hashcode_nat (length l) k) k"
by (simp add: abs_update_length)
also have
"… = map_of (fst (ls_update k v
(l ! bounded_hashcode_nat (length l) k))) k"
by (simp add: abs_update_def bounded_hashcode_nat_bounds[OF assms(3)])
also have "... = Some v" by (simp add: ls_update_map_of_eq)
finally show ?thesis .
qed

lemma abs_update_map_of_hceq:
assumes "ht_hash l"
assumes "ht_distinct l"
assumes "1 < length l"
assumes "x ≠ k"
assumes "bounded_hashcode_nat (length l) x
= bounded_hashcode_nat (length l) k"
shows "map_of (concat (abs_update k v l)) x = map_of (concat l) x"
proof -
from ht_hash_ht_distinct_map_of[
OF ht_hash_update[OF assms(1)]
ht_distinct_update[OF assms(2)]
length_update[OF assms(3)],
of k v x]
have "map_of (concat (abs_update k v l)) x
= map_of ((abs_update k v l) ! bounded_hashcode_nat (length l) x) x"
by (simp add: abs_update_length)
also from assms(5) have
"… = map_of (fst (ls_update k v
(l ! bounded_hashcode_nat (length l) k))) x"
by (simp add: abs_update_def bounded_hashcode_nat_bounds[OF assms(3)])
also have
"… = map_of (l ! bounded_hashcode_nat (length l) x) x"
by (simp add: ls_update_map_of_neq[OF assms(4)] assms(5))
also from ht_hash_ht_distinct_map_of[OF assms(1-3)] have
"… = map_of (concat l) x"
by simp
finally show ?thesis .
qed

lemma abs_update_map_of_hcneq:
assumes "ht_hash l"
assumes "ht_distinct l"
assumes "1 < length l"
assumes "x ≠ k"
assumes "bounded_hashcode_nat (length l) x
≠ bounded_hashcode_nat (length l) k"
shows "map_of (concat (abs_update k v l)) x = map_of (concat l) x"
proof -
from ht_hash_ht_distinct_map_of[
OF ht_hash_update[OF assms(1)]
ht_distinct_update[OF assms(2)]
length_update[OF assms(3)],
of k v x]
have "map_of (concat (abs_update k v l)) x
= map_of ((abs_update k v l) ! bounded_hashcode_nat (length l) x) x"
by (simp add: abs_update_length)
also from assms(5)
have "… = map_of (l ! bounded_hashcode_nat (length l) x) x"
by (simp add: abs_update_def bounded_hashcode_nat_bounds[OF assms(3)])
also from ht_hash_ht_distinct_map_of[OF assms(1-3)]
have "… = map_of (concat l) x"
by simp
finally show ?thesis .
qed

lemma abs_update_map_of''':
assumes "ht_hash l"
assumes "ht_distinct l"
assumes "1 < length l"
assumes "x ≠ k"
shows "map_of (concat (abs_update k v l)) x = map_of (concat l) x"
apply (cases
"bounded_hashcode_nat (length l) x = bounded_hashcode_nat (length l) k")
by (auto simp add: abs_update_map_of_hceq[OF assms]
abs_update_map_of_hcneq[OF assms])

lemma abs_update_map_of':
assumes "ht_hash l"
assumes "ht_distinct l"
assumes "1 < length l"
shows "map_of (concat (abs_update k v l)) x
= ((map_of (concat l))(k ↦ v)) x"
apply (cases "x = k")
apply (simp add: abs_update_map_of''[OF assms])
by (simp add: abs_update_map_of'''[OF assms])

lemma abs_update_map_of:
assumes "ht_hash l"
assumes "ht_distinct l"
assumes "1 < length l"
shows "map_of (concat (abs_update k v l))
= (map_of (concat l))(k ↦ v) "
apply (rule ext)
by (simp add: abs_update_map_of'[OF assms])

lemma ls_insls_map_of:
assumes "ht_hash ld"
assumes "ht_distinct ld"
assumes "1 < length ld"
assumes "distinct (map fst xs)"
shows "map_of (concat (ls_insls xs ld)) = map_of (concat ld) ++ map_of xs"
using assms
apply (induct xs arbitrary: ld)
apply simp
apply (case_tac a)
apply (simp only: ls_insls.simps)
subgoal premises prems
proof -
from prems(5) prems(1)[OF ht_hash_update[OF prems(2)]
ht_distinct_update[OF prems(3)]
length_update[OF prems(4)]]
abs_update_map_of[OF prems(2-4)]
show ?thesis
apply simp
apply (rule map_add_upd_left)
apply (metis dom_map_of_conv_image_fst)
done
qed
done

lemma ls_insls_map_of':
assumes "ht_hash ls"
assumes "ht_distinct ls"
assumes "ht_hash ld"
assumes "ht_distinct ld"
assumes "1 < length ld"
assumes "n < length ls"
shows "map_of (concat (ls_insls (ls ! n) ld))
++ map_of (concat (take n ls))
= map_of (concat ld) ++ map_of (concat (take (Suc n) ls))"
proof -
from assms(2,6) have "distinct (map fst (ls ! n))"
by (simp add: ht_distinct_def)
from ls_insls_map_of[OF assms(3-5) this] assms(6) show ?thesis
by (simp add: List.take_Suc_conv_app_nth)
qed

lemma ls_copy_map_of:
assumes "ht_hash ls"
assumes "ht_distinct ls"
assumes "ht_hash ld"
assumes "ht_distinct ld"
assumes "1 < length ld"
assumes "n ≤ length ls"
shows "map_of (concat (ls_copy n ls ld)) = map_of (concat ld) ++ map_of (concat (take n ls))"
using assms
apply (induct n arbitrary: ld)
apply simp
subgoal premises prems for n ld
proof -
note a = ht_hash_ls_insls[OF prems(4), of "ls ! n"]
note b = ht_distinct_ls_insls[OF prems(5), of "ls ! n"]
note c = length_ls_insls[OF prems(6), of "ls ! n"]
from prems have "n < length ls" by simp
with
ls_insls_map_of'[OF prems(2-6) this]
prems(1)[OF assms(1,2) a b c]
show ?thesis by simp
qed
done

lemma ls_rehash_map_of:
assumes "ht_hash l"
assumes "ht_distinct l"
assumes "1 < length l"
shows "map_of (concat (ls_rehash l)) = map_of (concat l)"
using assms(3) ls_copy_map_of[OF assms(1,2)
ht_hash_replicate ht_distinct_replicate]
by (simp add: ls_rehash_def)

lemma abs_update_rehash_map_of:
assumes "ht_hash l"
assumes "ht_distinct l"
assumes "1 < length l"
shows "map_of (concat (abs_update k v (ls_rehash l)))
= (map_of (concat l))(k ↦ v)"
proof -
note a = ht_hash_ls_rehash[of l]
note b = ht_distinct_ls_rehash[of l]
note c = length_ls_rehash[OF assms(3)]
from abs_update_map_of[OF a b c] ls_rehash_map_of[OF assms]
show ?thesis by simp
qed

abbreviation "hm_update ≡ ht_update"
lemma hm_update_rule':
"<is_hashmap' m l ht>
hm_update k v ht
<λr. is_hashmap (m(k ↦ v)) r * true>"
proof (cases "length l * load_factor ≤ the_size ht * 100")
case True
show ?thesis
unfolding is_hashmap'_def
apply sep_auto
apply (rule cons_post_rule[OF complete_ht_update_rehash[OF True]])
unfolding is_hashmap_def is_hashmap'_def
apply sep_auto
apply (simp add: abs_update_rehash_map_of is_hashtable_def)
done
next
case False
show ?thesis
unfolding is_hashmap'_def is_hashtable_def
apply sep_auto
apply (rule cons_post_rule)
using complete_ht_update_normal[OF False, simplified is_hashtable_def,
simplified, of k v]
apply auto
unfolding is_hashmap_def is_hashmap'_def
apply sep_auto
by (simp add: abs_update_map_of is_hashtable_def)
qed

lemma hm_update_rule:
"<is_hashmap m ht>
hm_update k v ht
<λr. is_hashmap (m(k ↦ v)) r * true>"
unfolding is_hashmap_def[of m]
by (sep_auto heap add: hm_update_rule')

lemma ls_delete_map_of:
assumes "distinct (map fst l)"
shows "map_of (fst (ls_delete k l)) x = ((map_of l) |` (- {k})) x"
using assms
apply (induct l rule: ls_delete.induct)
apply simp
apply (auto simp add: map_of_eq_None_iff Let_def)
by (metis ComplD ComplI Compl_insert option.set(2)
insertE insertI2 map_upd_eq_restrict restrict_map_def)

lemma update_ls_delete_map_of:
assumes "ht_hash l"
assumes "ht_distinct l"
assumes "ht_hash (l[bounded_hashcode_nat (length l) k
:= fst (ls_delete k (l ! bounded_hashcode_nat (length l) k))])"
assumes "ht_distinct (l[bounded_hashcode_nat (length l) k
:= fst (ls_delete k (l ! bounded_hashcode_nat (length l) k))])"
assumes "1 < length l"
shows "map_of (concat (l[bounded_hashcode_nat (length l) k
:= fst (ls_delete k (l ! bounded_hashcode_nat (length l) k))])) x
= ((map_of (concat l)) |` (- {k})) x"
proof -
from assms(2) bounded_hashcode_nat_bounds[OF assms(5)] have
distinct: "distinct (map fst (l ! bounded_hashcode_nat (length l) k))"
by (auto simp add: ht_distinct_def)
note id1 = ht_hash_ht_distinct_map_of[OF assms(3,4), simplified,
OF assms(5)[simplified], of x]
note id2 = ht_hash_ht_distinct_map_of[OF assms(1,2,5), of x]
show ?thesis
proof (cases
"bounded_hashcode_nat (length l) x = bounded_hashcode_nat (length l) k")
case True
with id1
have "map_of (concat (l[bounded_hashcode_nat (length l) k
:= fst (ls_delete k (l ! bounded_hashcode_nat (length l) k))])) x
=
map_of (l[bounded_hashcode_nat (length l) k
:= fst (ls_delete k (l ! bounded_hashcode_nat (length l) k))]
! bounded_hashcode_nat (length l) k) x"
by simp
also have
"… = map_of (fst (ls_delete k
(l ! bounded_hashcode_nat (length l) k))) x"
by (simp add: bounded_hashcode_nat_bounds[OF assms(5)])
also from ls_delete_map_of[OF distinct] have
"… = (map_of (l ! bounded_hashcode_nat (length l) k) |` (- {k})) x"
by simp
finally show ?thesis
by (cases "x = k") (simp_all add: id2 True)
next
case False
with bounded_hashcode_nat_bounds[OF assms(5)] id1 id2[symmetric]
show ?thesis
by (cases "x = k") simp_all
qed
qed

abbreviation "hm_delete ≡ ht_delete"
lemma hm_delete_rule':
"<is_hashmap' m l ht> hm_delete k ht <is_hashmap (m |` (-{k}))>"
apply (simp only: is_hashmap'_def[of m] is_hashtable_def)
apply sep_auto
apply (rule cons_post_rule)
using complete_ht_delete[simplified is_hashtable_def]
apply sep_auto
apply (simp add: is_hashmap_def is_hashmap'_def)
apply (sep_auto)
apply (simp add: is_hashtable_def)
apply (sep_auto)
by (auto simp add: update_ls_delete_map_of)

lemma hm_delete_rule:
"<is_hashmap m ht> hm_delete k ht <is_hashmap (m |` (-{k}))>"
unfolding is_hashmap_def[of m]
by (sep_auto heap add: hm_delete_rule')

definition hm_isEmpty :: "('k, 'v) hashtable ⇒ bool Heap" where
"hm_isEmpty ht ≡ return (the_size ht = 0)"

lemma hm_isEmpty_rule':
"<is_hashmap' m l ht>
hm_isEmpty ht
<λr. is_hashmap' m l ht * ↑(r ⟷ m=Map.empty)>"
unfolding hm_isEmpty_def
unfolding is_hashmap_def is_hashmap'_def is_hashtable_def ht_size_def
apply (cases ht, simp)
apply sep_auto
done

lemma hm_isEmpty_rule:
"<is_hashmap m ht> hm_isEmpty ht <λr. is_hashmap m ht * ↑(r ⟷ m=Map.empty)>"
unfolding is_hashmap_def
apply (sep_auto heap: hm_isEmpty_rule')
done

definition hm_size :: "('k, 'v) hashtable ⇒ nat Heap" where
"hm_size ht ≡ return (the_size ht)"

lemma length_card_dom_map_of:
assumes "distinct (map fst l)"
shows "length l = card (dom (map_of l))"
using assms
apply (induct l)
apply simp
apply simp
apply (case_tac a)
apply (auto intro!: fst_conv map_of_SomeD)
apply (subgoal_tac "aa ∉ dom (map_of l)")
apply simp
by (metis dom_map_of_conv_image_fst)

lemma ht_hash_dom_map_of_disj:
assumes "ht_hash l"
assumes "i < length l"
assumes "j < length l"
assumes "i ≠ j"
shows "dom (map_of (l!i)) ∩ dom (map_of(l!j)) = {}"
using assms
unfolding ht_hash_def
apply auto
by (metis fst_conv map_of_SomeD)

lemma ht_hash_dom_map_of_disj_drop:
assumes "ht_hash l"
assumes "i < length l"
shows "dom (map_of (l!i)) ∩ dom (map_of (concat (drop (Suc i) l))) = {}"
apply auto
subgoal premises prems for x y z
proof -
from prems(2) have "x ∈ dom (map_of (concat (drop (Suc i) l)))"
by auto
hence "∃j. j < length (drop (Suc i) l)
∧ x ∈ dom (map_of ((drop (Suc i) l)!j))"
by (metis Hash_Map.map_of_concat
‹x ∈ dom (map_of (concat (drop (Suc i) l)))› length_drop)
from this obtain j where
j: "j < length (drop (Suc i) l)
∧ x ∈ dom (map_of ((drop (Suc i) l)!j))"
by blast
hence length: "(Suc i + j) < length l" by auto
from j have neq: "i ≠ (Suc i + j)" by simp
from j have in_dom: "x ∈ dom (map_of (l!(Suc i + j)))" by auto
from prems(1) have in_dom2: "x ∈ dom (map_of (l ! i))" by auto
from ht_hash_dom_map_of_disj[OF assms length neq] in_dom in_dom2
show ?thesis by auto
qed
done

lemma sum_list_length_card_dom_map_of_concat:
assumes "ht_hash l"
assumes "ht_distinct l"
shows "sum_list (map length l) = card (dom (map_of (concat l)))"
using assms
proof -
from ht_hash_dom_map_of_disj_drop[OF assms(1)]
have "∀i. i < length l
⟶ dom (map_of (l ! i)) ∩ dom (map_of (concat (drop (Suc i) l)))
= {}"
by auto
with assms(2) show ?thesis
proof (induct l)
case Nil
thus ?case by simp
next
case (Cons l ls)
from Cons(2) have a: "ht_distinct ls" by (auto simp add: ht_distinct_def)
from Cons(3) have b: "∀i < length ls. dom (map_of (ls ! i))
∩ dom (map_of (concat (drop (Suc i) ls))) = {}"
apply simp
apply (rule allI)
apply (rule_tac x="Suc i" and P="(λi. i<Suc (length ls) ⟶
dom (map_of ((l # ls) ! i)) ∩ dom (map_of (concat (drop i ls))) =
{})" in allE)
by simp_all
from Cons(2) have "distinct (map fst l)" by (auto simp add: ht_distinct_def)
note l = length_card_dom_map_of[OF this]
from Cons(3) have c: "dom (map_of l) ∩ dom (map_of (concat ls)) = {}"
apply (rule_tac x="0" and P="(λi. i<Suc (length ls) ⟶
dom (map_of ((l # ls) ! i))
∩ dom (map_of (concat (drop i ls)))
= {})" in allE)
by simp_all
from Cons(1)[OF a b] l c show ?case by (simp add: card_Un_disjoint)
qed
qed

lemma hm_size_rule':
"<is_hashmap' m l ht>
hm_size ht
<λr. is_hashmap' m l ht * ↑(r = card (dom m))>"
unfolding hm_size_def is_hashmap_def is_hashmap'_def is_hashtable_def
apply sep_auto
apply (cases ht)
apply (simp add: ht_size_def)
apply sep_auto
by (simp add: sum_list_length_card_dom_map_of_concat)

lemma hm_size_rule:
"<is_hashmap m ht>
hm_size ht
<λr. is_hashmap m ht * ↑(r = card (dom m))>"
unfolding is_hashmap_def
by (sep_auto heap: hm_size_rule')

subsection ‹Iterators›

subsubsection ‹Definitions›
type_synonym ('k,'v) hm_it = "(nat × ('k×'v) list × ('k,'v) hashtable)"

fun hm_it_adjust
:: "nat ⇒ ('k::{heap,hashable},'v::heap) hashtable ⇒ nat Heap"
where
"hm_it_adjust 0 ht = return 0"
| "hm_it_adjust n ht = do {
l ← Array.nth (the_array ht) n;
case l of
[] ⇒ hm_it_adjust (n - 1) ht
| _ ⇒  return n
}"

definition hm_it_init
:: "('k::{heap,hashable},'v::heap) hashtable ⇒ ('k,'v) hm_it Heap"
where
"hm_it_init ht ≡ do {
n←Array.len (the_array ht);
if n = 0 then return (0,[],ht)
else do {
i←hm_it_adjust (n - 1) ht;
l←Array.nth (the_array ht) i;
return (i,l,ht)
}
}"

definition hm_it_has_next
:: "('k::{heap,hashable},'v::heap) hm_it ⇒ bool Heap"
where "hm_it_has_next it
≡ return (case it of (0,[],_) ⇒ False | _ ⇒ True)"

definition hm_it_next ::
"('k::{heap,hashable},'v::heap) hm_it
⇒ (('k×'v)×('k,'v) hm_it) Heap"
where "hm_it_next it ≡ case it of
(i,a#b#l,ht) ⇒ return (a,(i,b#l,ht))
| (0,[a],ht) ⇒ return (a,(0,[],ht))
| (Suc i,[a],ht) ⇒ do {
i ← hm_it_adjust i ht;
l ← Array.nth (the_array ht) i;
return (a,(i,rev l,ht))
}
"

definition "hm_is_it' l ht l' it ≡
is_hashtable l ht *
↑(let (i,r,ht')=it in
ht = ht'
∧ l' = (concat (take i l) @ rev r)
∧ distinct (map fst (l'))
∧ i ≤ length l ∧ (r=[] ⟶ i=0)
)"

definition "hm_is_it m ht m' it ≡ ∃⇩Al l'.
hm_is_it' l ht l' it
* ↑(map_of (concat l) = m ∧ map_of l' = m')
"

subsubsection ‹Auxiliary Lemmas›
lemma concat_take_Suc_empty: "⟦ n < length l; l!n=[] ⟧
⟹ concat (take (Suc n) l) = concat (take n l)"
apply (induct n arbitrary: l)
apply (case_tac l)
apply auto [2]
apply (case_tac l)
apply auto [2]
done

lemma nth_concat_splitE:
assumes "i<length (concat ls)"
obtains j k where
"j < length ls"
and "k < length (ls!j)"
and "concat ls ! i = ls!j!k"
and "i = length (concat (take j ls)) + k"
using assms
proof (induct ls arbitrary: i thesis)
case Nil thus ?case by auto
next
case (Cons l ls)
show ?case proof (cases)
assume L: "i < length l"
hence "concat (l#ls) ! i = (l#ls)!0!i" by (auto simp: nth_append)
thus ?thesis
apply (rule_tac Cons.prems(1)[of 0 i])
apply (simp_all add: L)
done
next
assume L: "¬(i < length l)"
hence 1: "concat (l#ls)!i = concat ls ! (i - length l)"
by (auto simp: nth_append)
obtain j k where
"j < length ls" and "k < length (ls!j)"
and "concat ls ! (i - length l) = ls!j!k"
and "i - length l = length (concat (take j ls)) + k"
apply (rule Cons.hyps[of "i - length l"])
using Cons.prems L
by auto
thus ?case using L
apply (rule_tac Cons.prems(1)[of "Suc j" k])
apply (auto simp: nth_append)
done
qed
qed

lemma is_hashmap'_distinct:
"is_hashtable l ht
⟹⇩A is_hashtable l ht * ↑(distinct (map fst (concat l)))"
apply (simp add: distinct_conv_nth)
proof (intro allI impI, elim exE)
fix i j a b
assume 1: "i < length (concat l)"
assume 2: "j < length (concat l)"
assume 3: "i≠j"

assume HM: "(a,b) ⊨ is_hashtable l ht"

from 1 obtain ji ki where
IFMT: "i = length (concat (take ji l)) + ki"
and JI_LEN: "ji < length l"
and KI_LEN: "ki < length (l!ji)"
and [simp]: "concat l ! i = l!ji!ki"
by (blast elim: nth_concat_splitE)

from 2 obtain jj kj where
JFMT: "j = length (concat (take jj l)) + kj"
and JJ_LEN: "jj < length l"
and KJ_LEN: "kj < length (l!jj)"
and [simp]: "concat l ! j = l!jj!kj"
by (blast elim: nth_concat_splitE)

show "fst (concat l ! i) ≠ fst (concat l ! j)"
proof cases
assume [simp]: "ji=jj"
with IFMT JFMT ‹i≠j› have "ki≠kj" by auto
moreover from HM JJ_LEN have "distinct (map fst (l!jj))"
unfolding is_hashmap'_def is_hashtable_def ht_distinct_def
by auto
ultimately show ?thesis using KI_LEN KJ_LEN
by (simp add: distinct_conv_nth)
next
assume NE: "ji≠jj"
from HM have
"∀x∈set (l!ji). bounded_hashcode_nat (length l) (fst x) = ji"
"∀x∈set (l!jj). bounded_hashcode_nat (length l) (fst x) = jj"
unfolding is_hashmap'_def is_hashtable_def ht_hash_def
using JI_LEN JJ_LEN
by auto
with KI_LEN KJ_LEN NE show ?thesis
apply (auto) by (metis nth_mem)
qed
qed

lemma take_set: "set (take n l) = { l!i | i. i<n ∧ i<length l }"
apply (auto simp add: set_conv_nth)
apply (rule_tac x=i in exI)
apply auto
done

lemma skip_empty_aux:
assumes A: "concat (take (Suc n) l) = concat (take (Suc x) l)"
assumes L[simp]: "Suc n ≤ length l" "x ≤ n"
shows "∀i. x<i ∧ i≤n ⟶ l!i=[]"
proof -
have "take (Suc n) l = take (Suc x + (n - x)) l"
by simp
also have "… = take (Suc x) l @ take (n - x) (drop (Suc x) l)"
by (simp only: take_add)
finally   have
"concat (take (Suc x) l) =
concat (take (Suc x) l) @ concat (take (n - x) (drop (Suc x) l))"
using A by simp
hence 1: "∀l∈set (take (n - x) (drop (Suc x) l)). l=[]" by simp
show ?thesis
proof safe
fix i
assume "x<i" and "i≤n"
hence "l!i ∈ set (take (n - x) (drop (Suc x) l))"
using L[simp del]
apply (auto simp: take_set)
apply (rule_tac x="i - Suc x" in exI)
apply auto
done
with 1 show "l!i=[]" by blast
qed
qed

lemma take_Suc0:
"l≠[] ⟹ take (Suc 0) l = [l!0]"
"0 < length l ⟹ take (Suc 0) l = [l!0]"
"Suc n ≤ length l ⟹ take (Suc 0) l = [l!0]"
by (cases l, auto)+

lemma concat_take_Suc_app_nth:
assumes "x < length l"
shows "concat (take (Suc x) l) = concat (take x l) @ l ! x"
using assms
by (auto simp: take_Suc_conv_app_nth)

lemma hm_hashcode_eq:
assumes "j < length (l!i)"
assumes "i < length l"
assumes "h ⊨ is_hashtable l ht"
shows "bounded_hashcode_nat (length l) (fst (l!i!j)) = i"
using assms
unfolding is_hashtable_def ht_hash_def
apply (cases "l!i!j")
apply (force simp: set_conv_nth)
done

lemma distinct_imp_distinct_take:
"distinct (map fst (concat l))
⟹ distinct (map fst (concat (take x l)))"
apply (subst (asm) append_take_drop_id[of x l,symmetric])
apply (simp del: append_take_drop_id)
done

lemma hm_it_adjust_rule:
"i<length l ⟹ <is_hashtable l ht>
hm_it_adjust i ht
<λj. is_hashtable l ht * ↑(
j≤i ∧
(concat (take (Suc i) l) = concat (take (Suc j) l)) ∧
(j=0 ∨ l!j ≠ [])
)
>"
proof (induct i)
case 0 thus ?case by sep_auto
next
case (Suc n)
show ?case using Suc.prems
by (sep_auto
heap add: Suc.hyps
simp: concat_take_Suc_empty
split: list.split)
qed

lemma hm_it_next_rule': "l'≠[] ⟹
<hm_is_it' l ht l' it>
hm_it_next it
<λ((k,v),it').
hm_is_it' l ht (butlast l') it'
* ↑(last l' = (k,v) ∧ distinct (map fst l') )>"
unfolding hm_it_next_def hm_is_it'_def is_hashmap'_def
using [[hypsubst_thin = true]]
apply (sep_auto (plain)
split: nat.split list.split
heap: hm_it_adjust_rule
simp: take_Suc0)
apply (simp split: prod.split nat.split list.split)
apply (intro allI impI conjI)
apply auto []
apply auto []
apply sep_auto []

apply (sep_auto (plain)
heap: hm_it_adjust_rule)
apply auto []
apply sep_auto

apply (cases l, auto) []
apply (metis SUP_upper fst_image_mp image_mono set_concat)

apply (drule skip_empty_aux, simp_all) []
defer
apply (auto simp: concat_take_Suc_app_nth) []

apply auto []
apply sep_auto

apply (auto simp: butlast_append) []
apply (auto simp: butlast_append) []

apply sep_auto
apply (auto simp: butlast_append) []
apply (auto simp: butlast_append) []
by (metis Ex_list_of_length Suc_leD concat_take_Suc_app_nth le_neq_implies_less le_trans nat.inject not_less_eq_eq)

subsubsection ‹Main Lemmas›

lemma hm_it_next_rule: "m'≠Map.empty ⟹
<hm_is_it m ht m' it>
hm_it_next it
<λ((k,v),it'). hm_is_it m ht (m' |` (-{k})) it' * ↑(m' k = Some v)>"
proof -
{ fix ys a
have aux3: "
⟦distinct (map fst ys); a ∉ fst ` set ys⟧ ⟹ map_of ys a = None"
by (induct ys) auto
} note aux3 = this

assume "m'≠Map.empty"
thus ?thesis
unfolding hm_is_it_def
apply (sep_auto heap: hm_it_next_rule')
apply (case_tac l' rule: rev_cases,
auto simp: restrict_map_def aux3 intro!: ext) []
apply (case_tac l' rule: rev_cases, auto)
done
qed

lemma hm_it_init_rule:
fixes ht :: "('k::{heap,hashable},'v::heap) hashtable"
shows "<is_hashmap m ht> hm_it_init ht <hm_is_it m ht m>⇩t"
unfolding hm_it_init_def is_hashmap_def is_hashmap'_def
hm_is_it_def hm_is_it'_def
apply (sep_auto simp del: map_of_append heap add: hm_it_adjust_rule)
apply (case_tac l, auto) []
apply (sep_auto simp del: concat_eq_Nil_conv map_of_append)
apply (auto simp: distinct_imp_distinct_take
dest: ent_fwd[OF _ is_hashmap'_distinct]) []

apply (drule sym)
apply (auto
simp: is_hashtable_def ht_distinct_def rev_map[symmetric]) []

apply (auto simp: set_conv_nth) []
apply (hypsubst_thin)
apply (drule_tac j=ia in hm_hashcode_eq, simp_all) []
apply (drule_tac j=ib in hm_hashcode_eq, simp_all) []

apply (auto
simp: is_hashmap'_def is_hashtable_def ht_distinct_def) []

apply (clarsimp)
apply (drule ent_fwd[OF _ is_hashmap'_distinct])
apply clarsimp
apply (subst concat_take_Suc_app_nth)
apply (case_tac l,auto) []
apply (simp)
apply (hypsubst_thin)
apply (subst (asm) (2) concat_take_Suc_app_nth)
apply (case_tac l,auto) []
apply (subst map_of_rev_distinct)
apply auto
done

lemma hm_it_has_next_rule:
"<hm_is_it m ht m' it> hm_it_has_next it
<λr. hm_is_it m ht m' it * ↑(r⟷m'≠Map.empty)>"
unfolding is_hashmap'_def hm_is_it_def hm_is_it'_def hm_it_has_next_def
by (sep_auto split: nat.split list.split)

lemma hm_it_finish: "hm_is_it m p m' it ⟹⇩A is_hashmap m p"
unfolding hm_is_it_def hm_is_it'_def is_hashmap_def is_hashmap'_def
by sep_auto

end
```