Theory Pointer_Map_Impl
section‹Imparative implementation for Pointermap›
theory Pointer_Map_Impl
imports Array_List
Separation_Logic_Imperative_HOL.Sep_Main
Separation_Logic_Imperative_HOL.Hash_Map_Impl
Pointer_Map
begin
record 'a pointermap_impl =
entriesi :: "'a array_list"
getentryi :: "('a,nat) hashtable"
lemma pointermapieq_exhaust: "entries a = entries b ⟹ getentry a = getentry b ⟹ a = (b :: 'a pointermap)" by simp
definition is_pointermap_impl :: "('a::{hashable,heap}) pointermap ⇒ 'a pointermap_impl ⇒ assn" where
"is_pointermap_impl b bi ≡
is_array_list (entries b) (entriesi bi)
* is_hashmap (getentry b) (getentryi bi)"
lemma is_pointermap_impl_prec: "precise is_pointermap_impl"
unfolding is_pointermap_impl_def[abs_def]
apply(rule preciseI)
apply(clarsimp)
apply(rename_tac a a' x y p F F')
apply(rule pointermapieq_exhaust)
apply(rule_tac p = "entriesi p" and h = "(x,y)" in preciseD[OF is_array_list_prec])
apply(unfold star_aci(1))
apply blast
apply(rule_tac p = "getentryi p" and h = "(x,y)" in preciseD[OF is_hashmap_prec])
apply(simp only: star_aci(2)[symmetric])
apply(simp only: star_aci(1)[symmetric])
apply(simp only: star_aci(2)[symmetric])
done
definition pointermap_empty where
"pointermap_empty ≡ do {
hm ← hm_new;
arl ← arl_empty;
return ⦇entriesi = arl, getentryi = hm ⦈
}"
lemma [sep_heap_rules]: "< emp > pointermap_empty <is_pointermap_impl empty_pointermap>⇩t"
unfolding is_pointermap_impl_def
by (sep_auto simp: pointermap_empty_def empty_pointermap_def)
definition pm_pthi where
"pm_pthi m p ≡ arl_nth (entriesi m) p"
lemma [sep_heap_rules]: "pointermap_sane m ⟹ pointermap_p_valid p m ⟹
< is_pointermap_impl m mi > pm_pthi mi p <λai. is_pointermap_impl m mi * ↑(ai = pm_pth m p)>"
by (sep_auto simp: pm_pthi_def pm_pth_def is_pointermap_impl_def pointermap_p_valid_def)
definition pointermap_getmki where
"pointermap_getmki a m ≡ do {
lo ← ht_lookup a (getentryi m);
(case lo of
Some l ⇒ return (l,m) |
None ⇒ do {
p ← return (snd (entriesi m));
ent ← arl_append (entriesi m) a;
lut ← hm_update a p (getentryi m);
u ← return ⦇entriesi = ent, getentryi = lut⦈;
return (p,u)
}
)
}"
lemmas pointermap_getmki_defs = pointermap_getmki_def pointermap_getmk_def pointermap_insert_def is_pointermap_impl_def
lemma [sep_heap_rules]: "pointermap_sane m ⟹ pointermap_getmk a m = (p,u) ⟹
< is_pointermap_impl m mi >
pointermap_getmki a mi
<λ(pi,ui). is_pointermap_impl u ui * ↑(pi = p)>⇩t"
apply(cases "getentry m a")
apply(unfold pointermap_getmki_def)
apply(unfold return_bind)
apply(rule bind_rule[where R = "λr. is_pointermap_impl m mi * ↑(r = None ∧ (snd (entriesi mi) = p)) * true"])
apply(sep_auto simp: pointermap_getmki_defs is_array_list_def split: prod.splits;fail)
apply(sep_auto simp: pointermap_getmki_defs)+
done
end