Theory IICF_Abs_Heapmap
section ‹Priority Maps implemented with List and Map›
theory IICF_Abs_Heapmap
imports IICF_Abs_Heap "HOL-Library.Rewrite" "../../Intf/IICF_Prio_Map"
begin
type_synonym ('k,'v) ahm = "'k list × ('k ⇀ 'v)"
subsection ‹Basic Setup›
text ‹First, we define a mapping to list-based heaps›
definition hmr_α :: "('k,'v) ahm ⇒ 'v heap" where
"hmr_α ≡ λ(pq,m). map (the o m) pq"
definition "hmr_invar ≡ λ(pq,m). distinct pq ∧ dom m = set pq"
definition "hmr_rel ≡ br hmr_α hmr_invar"
lemmas hmr_rel_defs = hmr_rel_def br_def hmr_α_def hmr_invar_def
lemma hmr_empty_invar[simp]: "hmr_invar ([],Map.empty)"
by (auto simp: hmr_invar_def)
locale hmstruct = h: heapstruct prio for prio :: "'v ⇒ 'b::linorder"
begin
text ‹Next, we define a mapping to priority maps.›
definition heapmap_α :: "('k,'v) ahm ⇒ ('k ⇀ 'v)" where
"heapmap_α ≡ λ(pq,m). m"
definition heapmap_invar :: "('k,'v) ahm ⇒ bool" where
"heapmap_invar ≡ λhm. hmr_invar hm ∧ h.heap_invar (hmr_α hm)"
definition "heapmap_rel ≡ br heapmap_α heapmap_invar"
lemmas heapmap_rel_defs = heapmap_rel_def br_def heapmap_α_def heapmap_invar_def
lemma [refine_dref_RELATES]: "RELATES hmr_rel" by (simp add: RELATES_def)
lemma h_heap_invarI[simp]: "heapmap_invar hm ⟹ h.heap_invar (hmr_α hm)"
by (simp add: heapmap_invar_def)
lemma hmr_invarI[simp]: "heapmap_invar hm ⟹ hmr_invar hm"
unfolding heapmap_invar_def by blast
lemma set_hmr_α[simp]: "hmr_invar hm ⟹ set (hmr_α hm) = ran (heapmap_α hm)"
apply (clarsimp simp: hmr_α_def hmr_invar_def heapmap_α_def
eq_commute[of "dom _" "set _"] ran_def)
apply force
done
lemma in_h_hmr_α_conv[simp]: "hmr_invar hm ⟹ x ∈# h.α (hmr_α hm) ⟷ x ∈ ran (heapmap_α hm)"
by (force simp: hmr_α_def hmr_invar_def heapmap_α_def in_multiset_in_set ran_is_image)
subsection ‹Basic Operations›
text ‹In this section, we define the basic operations on heapmaps,
and their relations to heaps and maps.›
subsubsection ‹Length›
text ‹Length of the list that represents the heap›
definition hm_length :: "('k,'v) ahm ⇒ nat" where
"hm_length ≡ λ(pq,_). length pq"
lemma hm_length_refine: "(hm_length, length) ∈ hmr_rel → nat_rel"
apply (intro fun_relI)
unfolding hm_length_def
by (auto simp: hmr_rel_defs)
lemma hm_length_hmr_α[simp]: "length (hmr_α hm) = hm_length hm"
by (auto simp: hm_length_def hmr_α_def split: prod.splits)
lemmas [refine] = hm_length_refine[param_fo]
subsubsection ‹Valid›
text ‹Check whether index is valid›
definition "hm_valid hm i ≡ i>0 ∧ i≤ hm_length hm"
lemma hm_valid_refine: "(hm_valid,h.valid)∈hmr_rel → nat_rel → bool_rel"
apply (intro fun_relI)
unfolding hm_valid_def h.valid_def
by (parametricity add: hm_length_refine)
lemma hm_valid_hmr_α[simp]: "h.valid (hmr_α hm) = hm_valid hm"
by (intro ext) (auto simp: h.valid_def hm_valid_def)
subsubsection ‹Key-Of›
definition hm_key_of :: "('k,'v) ahm ⇒ nat ⇒ 'k" where
"hm_key_of ≡ λ(pq,m) i. pq!(i - 1)"
definition hm_key_of_op :: "('k,'v) ahm ⇒ nat ⇒ 'k nres" where
"hm_key_of_op ≡ λ(pq,m) i. ASSERT (i>0) ⪢ mop_list_get pq (i - 1)"
lemma hm_key_of_op_unfold:
shows "hm_key_of_op hm i = ASSERT (hm_valid hm i) ⪢ RETURN (hm_key_of hm i)"
unfolding hm_valid_def hm_length_def hm_key_of_op_def hm_key_of_def
by (auto split: prod.splits simp: pw_eq_iff refine_pw_simps)
lemma val_of_hmr_α[simp]: "hm_valid hm i ⟹ h.val_of (hmr_α hm) i
= the (heapmap_α hm (hm_key_of hm i))"
by (auto
simp: hmr_α_def h.val_of_def heapmap_α_def hm_key_of_def hm_valid_def hm_length_def
split: prod.splits)
lemma hm_α_key_ex[simp]:
"⟦hmr_invar hm; hm_valid hm i⟧ ⟹ (heapmap_α hm (hm_key_of hm i) ≠ None)"
unfolding heapmap_invar_def hmr_invar_def hm_valid_def heapmap_α_def
hm_key_of_def hm_length_def
by (auto split: prod.splits)
subsubsection ‹Lookup›
abbreviation (input) hm_lookup where "hm_lookup ≡ heapmap_α"
definition "hm_the_lookup_op hm k ≡
ASSERT (heapmap_α hm k ≠ None ∧ hmr_invar hm)
⪢ RETURN (the (heapmap_α hm k))"
subsubsection ‹Exchange›
text ‹Exchange two indices›
definition "hm_exch_op ≡ λ(pq,m) i j. do {
ASSERT (hm_valid (pq,m) i);
ASSERT (hm_valid (pq,m) j);
ASSERT (hmr_invar (pq,m));
pq ← mop_list_swap pq (i - 1) (j - 1);
RETURN (pq,m)
}"
lemma hm_exch_op_invar: "hm_exch_op hm i j ≤⇩n SPEC hmr_invar"
unfolding hm_exch_op_def h.exch_op_def h.val_of_op_def h.update_op_def
apply simp
apply refine_vcg
apply (auto simp: hm_valid_def map_swap hm_length_def hmr_rel_defs)
done
lemma hm_exch_op_refine: "(hm_exch_op,h.exch_op) ∈ hmr_rel → nat_rel → nat_rel → ⟨hmr_rel⟩nres_rel"
apply (intro fun_relI nres_relI)
unfolding hm_exch_op_def h.exch_op_def h.val_of_op_def h.update_op_def
apply simp
apply refine_vcg
apply (auto simp: hm_valid_def map_swap hm_length_def hmr_rel_defs)
done
lemmas hm_exch_op_refine'[refine] = hm_exch_op_refine[param_fo, THEN nres_relD]
definition hm_exch :: "('k,'v) ahm ⇒ nat ⇒ nat ⇒ ('k,'v) ahm"
where "hm_exch ≡ λ(pq,m) i j. (swap pq (i-1) (j-1),m)"
lemma hm_exch_op_α_correct: "hm_exch_op hm i j ≤⇩n SPEC (λhm'.
hm_valid hm i ∧ hm_valid hm j ∧ hm'=hm_exch hm i j
)"
unfolding hm_exch_op_def
apply refine_vcg
apply (vc_solve simp: hm_valid_def hm_length_def heapmap_α_def solve: asm_rl)
apply (auto simp add: hm_key_of_def hm_exch_def swap_def) []
done
lemma hm_exch_α[simp]: "heapmap_α (hm_exch hm i j) = (heapmap_α hm)"
by (auto simp: heapmap_α_def hm_exch_def split: prod.splits)
lemma hm_exch_valid[simp]: "hm_valid (hm_exch hm i j) = hm_valid hm"
by (intro ext) (auto simp: hm_valid_def hm_length_def hm_exch_def split: prod.splits)
lemma hm_exch_length[simp]: "hm_length (hm_exch hm i j) = hm_length hm"
by (auto simp: hm_length_def hm_exch_def split: prod.splits)
lemma hm_exch_same[simp]: "hm_exch hm i i = hm"
by (auto simp: hm_exch_def split: prod.splits)
lemma hm_key_of_exch_conv[simp]:
"⟦hm_valid hm i; hm_valid hm j; hm_valid hm k⟧ ⟹
hm_key_of (hm_exch hm i j) k = (
if k=i then hm_key_of hm j
else if k=j then hm_key_of hm i
else hm_key_of hm k
)"
unfolding hm_exch_def hm_valid_def hm_length_def hm_key_of_def
by (auto split: prod.splits)
lemma hm_key_of_exch_matching[simp]:
"⟦hm_valid hm i; hm_valid hm j⟧ ⟹ hm_key_of (hm_exch hm i j) i = hm_key_of hm j"
"⟦hm_valid hm i; hm_valid hm j⟧ ⟹ hm_key_of (hm_exch hm i j) j = hm_key_of hm i"
by simp_all
subsubsection ‹Index›
text ‹Obtaining the index of a key›
definition "hm_index ≡ λ(pq,m) k. index pq k + 1"
lemma hm_index_valid[simp]: "⟦hmr_invar hm; heapmap_α hm k ≠ None⟧ ⟹ hm_valid hm (hm_index hm k)"
by (force simp: hm_valid_def heapmap_α_def hmr_invar_def hm_index_def hm_length_def Suc_le_eq)
lemma hm_index_key_of[simp]: "⟦hmr_invar hm; heapmap_α hm k ≠ None⟧ ⟹ hm_key_of hm (hm_index hm k) = k"
by (force
simp: hm_valid_def heapmap_α_def hmr_invar_def hm_index_def hm_length_def hm_key_of_def Suc_le_eq)
definition "hm_index_op ≡ λ(pq,m) k.
do {
ASSERT (hmr_invar (pq,m) ∧ heapmap_α (pq,m) k ≠ None);
i ← mop_list_index pq k;
RETURN (i+1)
}"
lemma hm_index_op_correct:
assumes "hmr_invar hm"
assumes "heapmap_α hm k ≠ None"
shows "hm_index_op hm k ≤ SPEC (λr. r= hm_index hm k)"
using assms unfolding hm_index_op_def
apply refine_vcg
apply (auto simp: heapmap_α_def hmr_invar_def hm_index_def index_nth_id)
done
lemmas [refine_vcg] = hm_index_op_correct
subsubsection ‹Update›
text ‹Updating the heap at an index›
definition hm_update_op :: "('k,'v) ahm ⇒ nat ⇒ 'v ⇒ ('k,'v) ahm nres" where
"hm_update_op ≡ λ(pq,m) i v. do {
ASSERT (hm_valid (pq,m) i ∧ hmr_invar (pq,m));
k ← mop_list_get pq (i - 1);
RETURN (pq, m(k ↦ v))
}"
lemma hm_update_op_invar: "hm_update_op hm k v ≤⇩n SPEC hmr_invar"
unfolding hm_update_op_def h.update_op_def
apply refine_vcg
by (auto simp: hmr_rel_defs map_distinct_upd_conv hm_valid_def hm_length_def)
lemma hm_update_op_refine: "(hm_update_op, h.update_op) ∈ hmr_rel → nat_rel → Id → ⟨hmr_rel⟩nres_rel"
apply (intro fun_relI nres_relI)
unfolding hm_update_op_def h.update_op_def mop_list_get_alt mop_list_set_alt
apply refine_vcg
apply (auto simp: hmr_rel_defs map_distinct_upd_conv hm_valid_def hm_length_def)
done
lemmas [refine] = hm_update_op_refine[param_fo, THEN nres_relD]
lemma hm_update_op_α_correct:
assumes "hmr_invar hm"
assumes "heapmap_α hm k ≠ None"
shows "hm_update_op hm (hm_index hm k) v ≤⇩n SPEC (λhm'. heapmap_α hm' = (heapmap_α hm)(k↦v))"
using assms
unfolding hm_update_op_def
apply refine_vcg
apply (force simp: heapmap_rel_defs hmr_rel_defs hm_index_def)
done
subsubsection ‹Butlast›
text ‹Remove last element›
definition hm_butlast_op :: "('k,'v) ahm ⇒ ('k,'v) ahm nres" where
"hm_butlast_op ≡ λ(pq,m). do {
ASSERT (hmr_invar (pq,m));
k ← mop_list_get pq (length pq - 1);
pq ← mop_list_butlast pq;
let m = m(k:=None);
RETURN (pq,m)
}"
lemma hm_butlast_op_refine: "(hm_butlast_op, h.butlast_op) ∈ hmr_rel → ⟨hmr_rel⟩nres_rel"
supply [simp del] = map_upd_eq_restrict
apply (intro fun_relI nres_relI)
unfolding hm_butlast_op_def h.butlast_op_def
apply simp
apply refine_vcg
apply (clarsimp_all simp: hmr_rel_defs map_butlast distinct_butlast)
apply (auto simp: neq_Nil_rev_conv) []
done
lemmas [refine] = hm_butlast_op_refine[param_fo, THEN nres_relD]
lemma hm_butlast_op_α_correct: "hm_butlast_op hm ≤⇩n SPEC (
λhm'. heapmap_α hm' = (heapmap_α hm)( hm_key_of hm (hm_length hm) := None ))"
unfolding hm_butlast_op_def
apply refine_vcg
apply (auto simp: heapmap_α_def hm_key_of_def hm_length_def)
done
subsubsection ‹Append›
text ‹Append new element at end of heap›
definition hm_append_op :: "('k,'v) ahm ⇒ 'k ⇒ 'v ⇒ ('k,'v) ahm nres"
where "hm_append_op ≡ λ(pq,m) k v. do {
ASSERT (k ∉ dom m);
ASSERT (hmr_invar (pq,m));
pq ← mop_list_append pq k;
let m = m (k ↦ v);
RETURN (pq,m)
}"
lemma hm_append_op_invar: "hm_append_op hm k v ≤⇩n SPEC hmr_invar"
unfolding hm_append_op_def h.append_op_def
apply refine_vcg
unfolding heapmap_α_def hmr_rel_defs
apply auto
done
lemma hm_append_op_refine: "⟦ heapmap_α hm k = None; (hm,h)∈hmr_rel ⟧
⟹ (hm_append_op hm k v, h.append_op h v) ∈ ⟨hmr_rel⟩nres_rel"
apply (intro fun_relI nres_relI)
unfolding hm_append_op_def h.append_op_def
apply refine_vcg
unfolding heapmap_α_def hmr_rel_defs
apply auto
done
lemmas hm_append_op_refine'[refine] = hm_append_op_refine[param_fo, THEN nres_relD]
lemma hm_append_op_α_correct:
"hm_append_op hm k v ≤⇩n SPEC (λhm'. heapmap_α hm' = (heapmap_α hm) (k ↦ v))"
unfolding hm_append_op_def
apply refine_vcg
by (auto simp: heapmap_α_def)
subsection ‹Auxiliary Operations›
text ‹Auxiliary operations on heapmaps, which are derived
from the basic operations, but do not correspond to
operations of the priority map interface›
text ‹We start with some setup›
lemma heapmap_hmr_relI: "(hm,h)∈heapmap_rel ⟹ (hm,hmr_α hm) ∈ hmr_rel"
by (auto simp: heapmap_rel_defs hmr_rel_defs)
lemma heapmap_hmr_relI': "heapmap_invar hm ⟹ (hm,hmr_α hm) ∈ hmr_rel"
by (auto simp: heapmap_rel_defs hmr_rel_defs)
text ‹The basic principle how we prove correctness of our operations:
Invariant preservation is shown by relating the operations to
operations on heaps. Then, only correctness on the abstraction
remains to be shown, assuming the operation does not fail.
›
lemma heapmap_nres_relI':
assumes "hm ≤ ⇓hmr_rel h'"
assumes "h' ≤ SPEC (h.heap_invar)"
assumes "hm ≤⇩n SPEC (λhm'. RETURN (heapmap_α hm') ≤ h)"
shows "hm ≤ ⇓heapmap_rel h"
using assms
unfolding heapmap_rel_defs hmr_rel_def
by (auto simp: pw_le_iff pw_leof_iff refine_pw_simps)
lemma heapmap_nres_relI'':
assumes "hm ≤ ⇓hmr_rel h'"
assumes "h' ≤ SPEC Φ"
assumes "⋀h'. Φ h' ⟹ h.heap_invar h'"
assumes "hm ≤⇩n SPEC (λhm'. RETURN (heapmap_α hm') ≤ h)"
shows "hm ≤ ⇓heapmap_rel h"
apply (rule heapmap_nres_relI')
apply fact
apply (rule order_trans, fact)
apply (clarsimp; fact)
apply fact
done
subsubsection ‹Val-of›
text ‹Indexing into the heap›
definition hm_val_of_op :: "('k,'v) ahm ⇒ nat ⇒ 'v nres" where
"hm_val_of_op ≡ λhm i. do {
k ← hm_key_of_op hm i;
v ← hm_the_lookup_op hm k;
RETURN v
}"
lemma hm_val_of_op_refine: "(hm_val_of_op,h.val_of_op) ∈ (hmr_rel → nat_rel → ⟨Id⟩nres_rel)"
apply (intro fun_relI nres_relI)
unfolding hm_val_of_op_def h.val_of_op_def
hm_key_of_op_def hm_key_of_def hm_valid_def hm_length_def
hm_the_lookup_op_def
apply clarsimp
apply (rule refine_IdD)
apply refine_vcg
apply (auto simp: hmr_rel_defs heapmap_α_def)
done
lemmas [refine] = hm_val_of_op_refine[param_fo, THEN nres_relD]
subsubsection ‹Prio-of›
text ‹Priority of key›
definition "hm_prio_of_op h i ≡ do {v ← hm_val_of_op h i; RETURN (prio v)}"
lemma hm_prio_of_op_refine: "(hm_prio_of_op, h.prio_of_op) ∈ hmr_rel → nat_rel → ⟨Id⟩nres_rel"
apply (intro fun_relI nres_relI)
unfolding hm_prio_of_op_def h.prio_of_op_def
apply refine_rcg
by auto
lemmas hm_prio_of_op_refine'[refine] = hm_prio_of_op_refine[param_fo, THEN nres_relD]
subsubsection ‹Swim›
definition hm_swim_op :: "('k,'v) ahm ⇒ nat ⇒ ('k,'v) ahm nres" where
"hm_swim_op h i ≡ do {
RECT (λswim (h,i). do {
ASSERT (hm_valid h i ∧ h.swim_invar (hmr_α h) i);
if hm_valid h (h.parent i) then do {
ppi ← hm_prio_of_op h (h.parent i);
pi ← hm_prio_of_op h i;
if (¬ppi ≤ pi) then do {
h ← hm_exch_op h i (h.parent i);
swim (h, h.parent i)
} else
RETURN h
} else
RETURN h
}) (h,i)
}"
lemma hm_swim_op_refine: "(hm_swim_op, h.swim_op) ∈ hmr_rel → nat_rel → ⟨hmr_rel⟩nres_rel"
apply (intro fun_relI nres_relI)
unfolding hm_swim_op_def h.swim_op_def
apply refine_rcg
apply refine_dref_type
apply (clarsimp_all simp: hm_valid_refine[param_fo, THEN IdD])
apply (simp add: hmr_rel_def in_br_conv)
done
lemmas hm_swim_op_refine'[refine] = hm_swim_op_refine[param_fo, THEN nres_relD]
lemma hm_swim_op_nofail_imp_valid:
"nofail (hm_swim_op hm i) ⟹ hm_valid hm i ∧ h.swim_invar (hmr_α hm) i"
unfolding hm_swim_op_def
apply (subst (asm) RECT_unfold, refine_mono)
by (auto simp: refine_pw_simps)
lemma hm_swim_op_α_correct: "hm_swim_op hm i ≤⇩n SPEC (λhm'. heapmap_α hm' = heapmap_α hm)"
apply (rule leof_add_nofailI)
apply (drule hm_swim_op_nofail_imp_valid)
unfolding hm_swim_op_def
apply (rule RECT_rule_leof[where
pre="λ(hm',i). hm_valid hm' i ∧ heapmap_α hm' = heapmap_α hm"
and V = "inv_image less_than snd"
])
apply simp
apply simp
unfolding hm_prio_of_op_def hm_val_of_op_def
hm_exch_op_def hm_key_of_op_def hm_the_lookup_op_def
apply (refine_vcg)
apply (vc_solve simp add: hm_valid_def hm_length_def)
apply rprems
apply (vc_solve simp: heapmap_α_def h.parent_def)
done
subsubsection ‹Sink›
definition hm_sink_op
where
"hm_sink_op h k ≡ RECT (λD (h,k). do {
ASSERT (k>0 ∧ k≤hm_length h);
let len = hm_length h;
if (2*k ≤ len) then do {
let j = 2*k;
pj ← hm_prio_of_op h j;
j ← (
if j<len then do {
psj ← hm_prio_of_op h (Suc j);
if pj>psj then RETURN (j+1) else RETURN j
} else RETURN j);
pj ← hm_prio_of_op h j;
pk ← hm_prio_of_op h k;
if (pk > pj) then do {
h ← hm_exch_op h k j;
D (h,j)
} else
RETURN h
} else RETURN h
}) (h,k)"
lemma hm_sink_op_refine: "(hm_sink_op, h.sink_op) ∈ hmr_rel → nat_rel → ⟨hmr_rel⟩nres_rel"
apply (intro fun_relI nres_relI)
unfolding hm_sink_op_def h.sink_op_opt_eq[symmetric] h.sink_op_opt_def
apply refine_rcg
apply refine_dref_type
unfolding hmr_rel_def heapmap_rel_def
apply (clarsimp_all simp: in_br_conv)
done
lemmas hm_sink_op_refine'[refine] = hm_sink_op_refine[param_fo, THEN nres_relD]
lemma hm_sink_op_nofail_imp_valid: "nofail (hm_sink_op hm i) ⟹ hm_valid hm i"
unfolding hm_sink_op_def
apply (subst (asm) RECT_unfold, refine_mono)
by (auto simp: refine_pw_simps hm_valid_def)
lemma hm_sink_op_α_correct: "hm_sink_op hm i ≤⇩n SPEC (λhm'. heapmap_α hm' = heapmap_α hm)"
apply (rule leof_add_nofailI)
apply (drule hm_sink_op_nofail_imp_valid)
unfolding hm_sink_op_def
apply (rule RECT_rule_leof[where
pre="λ(hm',i). hm_valid hm' i ∧ heapmap_α hm' = heapmap_α hm ∧ hm_length hm' = hm_length hm"
and V = "measure (λ(hm',i). hm_length hm' - i)"
])
apply simp
apply simp
unfolding hm_prio_of_op_def hm_val_of_op_def hm_exch_op_def
hm_key_of_op_def hm_the_lookup_op_def
apply (refine_vcg)
apply (vc_solve simp add: hm_valid_def hm_length_def)
apply rprems
apply (vc_solve simp: heapmap_α_def h.parent_def split: prod.splits)
apply (auto)
done
subsubsection ‹Repair›
definition "hm_repair_op hm i ≡ do {
hm ← hm_sink_op hm i;
hm ← hm_swim_op hm i;
RETURN hm
}"
lemma hm_repair_op_refine: "(hm_repair_op, h.repair_op) ∈ hmr_rel → nat_rel → ⟨hmr_rel⟩nres_rel"
apply (intro fun_relI nres_relI)
unfolding hm_repair_op_def h.repair_op_def
by refine_rcg
lemmas hm_repair_op_refine'[refine] = hm_repair_op_refine[param_fo, THEN nres_relD]
lemma hm_repair_op_α_correct: "hm_repair_op hm i ≤⇩n SPEC (λhm'. heapmap_α hm' = heapmap_α hm)"
unfolding hm_repair_op_def
apply (refine_vcg
hm_swim_op_α_correct[THEN leof_trans]
hm_sink_op_α_correct[THEN leof_trans])
by auto
subsection ‹Operations›
text ‹In this section, we define the operations that implement the priority-map interface›
subsubsection ‹Empty›
definition hm_empty_op :: "('k,'v) ahm nres"
where "hm_empty_op ≡ RETURN ([],Map.empty)"
lemma hm_empty_aref: "(hm_empty_op,RETURN op_map_empty) ∈ ⟨heapmap_rel⟩nres_rel"
unfolding hm_empty_op_def
by (auto simp: heapmap_rel_defs hmr_rel_defs intro: nres_relI)
subsubsection ‹Insert›
definition hm_insert_op :: "'k ⇒ 'v ⇒ ('k,'v) ahm ⇒ ('k,'v) ahm nres" where
"hm_insert_op ≡ λk v h. do {
ASSERT (h.heap_invar (hmr_α h));
h ← hm_append_op h k v;
let l = hm_length h;
h ← hm_swim_op h l;
RETURN h
}"
lemma hm_insert_op_refine[refine]: "⟦ heapmap_α hm k = None; (hm,h)∈hmr_rel ⟧ ⟹
hm_insert_op k v hm ≤ ⇓hmr_rel (h.insert_op v h)"
unfolding hm_insert_op_def h.insert_op_def
apply refine_rcg
by (auto simp: hmr_rel_def br_def)
lemma hm_insert_op_aref:
"(hm_insert_op,mop_map_update_new) ∈ Id → Id → heapmap_rel → ⟨heapmap_rel⟩nres_rel"
apply (intro fun_relI nres_relI)
unfolding mop_map_update_new_alt
apply (rule ASSERT_refine_right)
apply (rule heapmap_nres_relI''[OF hm_insert_op_refine h.insert_op_correct])
apply (unfold heapmap_rel_def in_br_conv; clarsimp)
apply (erule heapmap_hmr_relI)
apply (unfold heapmap_rel_def in_br_conv; clarsimp)
apply (unfold heapmap_rel_def in_br_conv; clarsimp)
unfolding hm_insert_op_def
apply (refine_vcg
hm_append_op_α_correct[THEN leof_trans]
hm_swim_op_α_correct[THEN leof_trans])
apply (unfold heapmap_rel_def in_br_conv; clarsimp)
done
subsubsection ‹Is-Empty›
lemma hmr_α_empty_iff[simp]:
"hmr_invar hm ⟹ hmr_α hm = [] ⟷ heapmap_α hm = Map.empty"
by (auto
simp: hmr_α_def heapmap_invar_def heapmap_α_def hmr_invar_def
split: prod.split)
definition hm_is_empty_op :: "('k,'v) ahm ⇒ bool nres" where
"hm_is_empty_op ≡ λhm. do {
ASSERT (hmr_invar hm);
let l = hm_length hm;
RETURN (l=0)
}"
lemma hm_is_empty_op_refine: "(hm_is_empty_op, h.is_empty_op) ∈ hmr_rel → ⟨bool_rel⟩nres_rel"
apply (intro fun_relI nres_relI)
unfolding hm_is_empty_op_def h.is_empty_op_def
apply refine_rcg
apply (auto simp: hmr_rel_defs) []
apply (parametricity add: hm_length_refine)
done
lemma hm_is_empty_op_aref: "(hm_is_empty_op, RETURN o op_map_is_empty) ∈ heapmap_rel → ⟨bool_rel⟩nres_rel"
apply (intro fun_relI nres_relI)
unfolding hm_is_empty_op_def
apply refine_vcg
apply (auto simp: hmr_rel_defs heapmap_rel_defs hm_length_def)
done
subsubsection ‹Lookup›
definition hm_lookup_op :: "'k ⇒ ('k,'v) ahm ⇒ 'v option nres"
where "hm_lookup_op ≡ λk hm. ASSERT (heapmap_invar hm) ⪢ RETURN (hm_lookup hm k)"
lemma hm_lookup_op_aref: "(hm_lookup_op,RETURN oo op_map_lookup) ∈ Id → heapmap_rel → ⟨⟨Id⟩option_rel⟩nres_rel"
apply (intro fun_relI nres_relI)
unfolding hm_lookup_op_def heapmap_rel_def in_br_conv
apply refine_vcg
apply simp_all
done
subsubsection ‹Contains-Key›
definition "hm_contains_key_op ≡ λk (pq,m). ASSERT (heapmap_invar (pq,m)) ⪢ RETURN (k∈dom m)"
lemma hm_contains_key_op_aref: "(hm_contains_key_op,RETURN oo op_map_contains_key) ∈ Id → heapmap_rel → ⟨bool_rel⟩nres_rel"
apply (intro fun_relI nres_relI)
unfolding hm_contains_key_op_def heapmap_rel_defs
apply refine_vcg
by (auto)
subsubsection ‹Decrease-Key›
definition "hm_decrease_key_op ≡ λk v hm. do {
ASSERT (heapmap_invar hm);
ASSERT (heapmap_α hm k ≠ None ∧ prio v ≤ prio (the (heapmap_α hm k)));
i ← hm_index_op hm k;
hm ← hm_update_op hm i v;
hm_swim_op hm i
}"
definition (in heapstruct) "decrease_key_op i v h ≡ do {
ASSERT (valid h i ∧ prio v ≤ prio_of h i);
h ← update_op h i v;
swim_op h i
}"
lemma (in heapstruct) decrease_key_op_invar:
"⟦heap_invar h; valid h i; prio v ≤ prio_of h i⟧ ⟹ decrease_key_op i v h ≤ SPEC heap_invar"
unfolding decrease_key_op_def
apply refine_vcg
by (auto simp: swim_invar_decr)
lemma index_op_inline_refine:
assumes "heapmap_invar hm"
assumes "heapmap_α hm k ≠ None"
assumes "f (hm_index hm k) ≤ m"
shows "do {i ← hm_index_op hm k; f i} ≤ m"
using hm_index_op_correct[of hm k] assms
by (auto simp: pw_le_iff refine_pw_simps)
lemma hm_decrease_key_op_refine:
"⟦(hm,h)∈hmr_rel; (hm,m)∈heapmap_rel; m k = Some v'⟧
⟹ hm_decrease_key_op k v hm ≤⇓hmr_rel (h.decrease_key_op (hm_index hm k) v h)"
unfolding hm_decrease_key_op_def h.decrease_key_op_def
apply (refine_rcg index_op_inline_refine)
unfolding hmr_rel_def heapmap_rel_def in_br_conv
apply (clarsimp_all)
done
lemma hm_index_op_inline_leof:
assumes "f (hm_index hm k) ≤⇩n m"
shows "do {i ← hm_index_op hm k; f i} ≤⇩n m"
using hm_index_op_correct[of hm k] assms unfolding hm_index_op_def
by (auto simp: pw_le_iff pw_leof_iff refine_pw_simps split: prod.splits)
lemma hm_decrease_key_op_α_correct:
"heapmap_invar hm ⟹ hm_decrease_key_op k v hm ≤⇩n SPEC (λhm'. heapmap_α hm' = (heapmap_α hm)(k↦v))"
unfolding hm_decrease_key_op_def
apply (refine_vcg
hm_update_op_α_correct[THEN leof_trans]
hm_swim_op_α_correct[THEN leof_trans]
hm_index_op_inline_leof
)
apply simp_all
done
lemma hm_decrease_key_op_aref:
"(hm_decrease_key_op, PR_CONST (mop_pm_decrease_key prio)) ∈ Id → Id → heapmap_rel → ⟨heapmap_rel⟩nres_rel"
unfolding PR_CONST_def
apply (intro fun_relI nres_relI)
apply (frule heapmap_hmr_relI)
unfolding mop_pm_decrease_key_alt
apply (rule ASSERT_refine_right; clarsimp)
apply (rule heapmap_nres_relI')
apply (rule hm_decrease_key_op_refine; assumption)
unfolding heapmap_rel_def hmr_rel_def in_br_conv
apply (rule h.decrease_key_op_invar; simp; fail )
apply (refine_vcg hm_decrease_key_op_α_correct[THEN leof_trans]; simp; fail)
done
subsubsection ‹Increase-Key›
definition "hm_increase_key_op ≡ λk v hm. do {
ASSERT (heapmap_invar hm);
ASSERT (heapmap_α hm k ≠ None ∧ prio v ≥ prio (the (heapmap_α hm k)));
i ← hm_index_op hm k;
hm ← hm_update_op hm i v;
hm_sink_op hm i
}"
definition (in heapstruct) "increase_key_op i v h ≡ do {
ASSERT (valid h i ∧ prio v ≥ prio_of h i);
h ← update_op h i v;
sink_op h i
}"
lemma (in heapstruct) increase_key_op_invar:
"⟦heap_invar h; valid h i; prio v ≥ prio_of h i⟧ ⟹ increase_key_op i v h ≤ SPEC heap_invar"
unfolding increase_key_op_def
apply refine_vcg
by (auto simp: sink_invar_incr)
lemma hm_increase_key_op_refine:
"⟦(hm,h)∈hmr_rel; (hm,m)∈heapmap_rel; m k = Some v'⟧
⟹ hm_increase_key_op k v hm ≤⇓hmr_rel (h.increase_key_op (hm_index hm k) v h)"
unfolding hm_increase_key_op_def h.increase_key_op_def
apply (refine_rcg index_op_inline_refine)
unfolding hmr_rel_def heapmap_rel_def in_br_conv
apply (clarsimp_all)
done
lemma hm_increase_key_op_α_correct:
"heapmap_invar hm ⟹ hm_increase_key_op k v hm ≤⇩n SPEC (λhm'. heapmap_α hm' = (heapmap_α hm)(k↦v))"
unfolding hm_increase_key_op_def
apply (refine_vcg
hm_update_op_α_correct[THEN leof_trans]
hm_sink_op_α_correct[THEN leof_trans]
hm_index_op_inline_leof)
apply simp_all
done
lemma hm_increase_key_op_aref:
"(hm_increase_key_op, PR_CONST (mop_pm_increase_key prio)) ∈ Id → Id → heapmap_rel → ⟨heapmap_rel⟩nres_rel"
unfolding PR_CONST_def
apply (intro fun_relI nres_relI)
apply (frule heapmap_hmr_relI)
unfolding mop_pm_increase_key_alt
apply (rule ASSERT_refine_right; clarsimp)
apply (rule heapmap_nres_relI')
apply (rule hm_increase_key_op_refine; assumption)
unfolding heapmap_rel_def hmr_rel_def in_br_conv
apply (rule h.increase_key_op_invar; simp; fail )
apply (refine_vcg hm_increase_key_op_α_correct[THEN leof_trans]; simp)
done
subsubsection ‹Change-Key›
definition "hm_change_key_op ≡ λk v hm. do {
ASSERT (heapmap_invar hm);
ASSERT (heapmap_α hm k ≠ None);
i ← hm_index_op hm k;
hm ← hm_update_op hm i v;
hm_repair_op hm i
}"
definition (in heapstruct) "change_key_op i v h ≡ do {
ASSERT (valid h i);
h ← update_op h i v;
repair_op h i
}"
lemma (in heapstruct) change_key_op_invar:
"⟦heap_invar h; valid h i⟧ ⟹ change_key_op i v h ≤ SPEC heap_invar"
unfolding change_key_op_def
apply (refine_vcg)
apply hypsubst
apply refine_vcg
by (auto simp: sink_invar_incr)
lemma hm_change_key_op_refine:
"⟦(hm,h)∈hmr_rel; (hm,m)∈heapmap_rel; m k = Some v'⟧
⟹ hm_change_key_op k v hm ≤⇓hmr_rel (h.change_key_op (hm_index hm k) v h)"
unfolding hm_change_key_op_def h.change_key_op_def
apply (refine_rcg index_op_inline_refine)
unfolding hmr_rel_def heapmap_rel_def in_br_conv
apply (clarsimp_all)
done
lemma hm_change_key_op_α_correct:
"heapmap_invar hm ⟹ hm_change_key_op k v hm ≤⇩n SPEC (λhm'. heapmap_α hm' = (heapmap_α hm)(k↦v))"
unfolding hm_change_key_op_def
apply (refine_vcg
hm_update_op_α_correct[THEN leof_trans]
hm_repair_op_α_correct[THEN leof_trans]
hm_index_op_inline_leof)
unfolding heapmap_rel_def in_br_conv
apply simp
apply simp
done
lemma hm_change_key_op_aref:
"(hm_change_key_op, mop_map_update_ex) ∈ Id → Id → heapmap_rel → ⟨heapmap_rel⟩nres_rel"
apply (intro fun_relI nres_relI)
apply (frule heapmap_hmr_relI)
unfolding mop_map_update_ex_alt
apply (rule ASSERT_refine_right; clarsimp)
apply (rule heapmap_nres_relI')
apply (rule hm_change_key_op_refine; assumption)
unfolding heapmap_rel_def hmr_rel_def in_br_conv
apply (rule h.change_key_op_invar; simp; fail )
apply ((refine_vcg hm_change_key_op_α_correct[THEN leof_trans]; simp))
done
subsubsection ‹Set›
text ‹Realized as generic algorithm!›
lemma (in -) op_pm_set_gen_impl: "RETURN ooo op_map_update = (λk v m. do {
c ← RETURN (op_map_contains_key k m);
if c then
mop_map_update_ex k v m
else
mop_map_update_new k v m
})"
apply (intro ext)
unfolding op_map_contains_key_def mop_map_update_ex_def mop_map_update_new_def
by simp
definition "hm_set_op k v hm ≡ do {
c ← hm_contains_key_op k hm;
if c then
hm_change_key_op k v hm
else
hm_insert_op k v hm
}"
lemma hm_set_op_aref:
"(hm_set_op, RETURN ooo op_map_update) ∈ Id → Id → heapmap_rel → ⟨heapmap_rel⟩nres_rel"
unfolding op_pm_set_gen_impl
apply (intro fun_relI nres_relI)
unfolding hm_set_op_def o_def
apply (refine_rcg
hm_contains_key_op_aref[param_fo, unfolded o_def, THEN nres_relD]
hm_change_key_op_aref[param_fo, THEN nres_relD]
hm_insert_op_aref[param_fo, THEN nres_relD]
)
by auto
subsubsection ‹Pop-Min›
definition hm_pop_min_op :: "('k,'v) ahm ⇒ (('k×'v) × ('k,'v) ahm) nres" where
"hm_pop_min_op hm ≡ do {
ASSERT (heapmap_invar hm);
ASSERT (hm_valid hm 1);
k ← hm_key_of_op hm 1;
v ← hm_the_lookup_op hm k;
let l = hm_length hm;
hm ← hm_exch_op hm 1 l;
hm ← hm_butlast_op hm;
if (l≠1) then do {
hm ← hm_sink_op hm 1;
RETURN ((k,v),hm)
} else RETURN ((k,v),hm)
}"
lemma hm_pop_min_op_refine:
"(hm_pop_min_op, h.pop_min_op) ∈ hmr_rel → ⟨UNIV ×⇩r hmr_rel⟩nres_rel"
apply (intro fun_relI nres_relI)
unfolding hm_pop_min_op_def h.pop_min_op_def
unfolding ignore_snd_refine_conv hm_the_lookup_op_def hm_key_of_op_unfold
apply (simp cong: if_cong add: Let_def)
apply (simp add: unused_bind_conv h.val_of_op_def refine_pw_simps)
apply refine_rcg
unfolding hmr_rel_def in_br_conv
apply (unfold heapmap_invar_def;simp)
apply (auto simp: in_br_conv)
done
text ‹We demonstrate two different approaches for proving correctness
here.
The first approach uses the relation to plain heaps only to establish
the invariant.
The second approach also uses the relation to heaps to establish
correctness of the result.
The first approach seems to be more robust against badly set
up simpsets, which may be the case in early stages of development.
Assuming a working simpset, the second approach may be less work,
and the proof may look more elegant.
›
text_raw ‹\paragraph{First approach}›
text ‹Transfer heapmin-property to heapmap-domain›
lemma heapmap_min_prop:
assumes INV: "heapmap_invar hm"
assumes V': "heapmap_α hm k = Some v'"
assumes NE: "hm_valid hm (Suc 0)"
shows "prio (the (heapmap_α hm (hm_key_of hm (Suc 0)))) ≤ prio v'"
proof -
obtain pq m where [simp]: "hm=(pq,m)" by (cases hm)
from NE have [simp]: "pq≠[]" by (auto simp: hm_valid_def hm_length_def)
have CNV_LHS: "prio (the (heapmap_α hm (hm_key_of hm (Suc 0))))
= h.prio_of (hmr_α hm) (Suc 0)"
by (auto simp: heapmap_α_def hm_key_of_def hmr_α_def h.val_of_def)
from INV have INV': "h.heap_invar (hmr_α hm)"
unfolding heapmap_invar_def by auto
from V' INV obtain i where IDX: "h.valid (hmr_α hm) i"
and CNV_RHS: "prio v' = h.prio_of (hmr_α hm) i"
apply (clarsimp simp: heapmap_α_def heapmap_invar_def hmr_invar_def hmr_α_def
h.valid_def h.val_of_def)
by (metis (no_types, opaque_lifting) Suc_leI comp_apply diff_Suc_Suc
diff_zero domI index_less_size_conv neq0_conv nth_index nth_map
old.nat.distinct(2) option.sel)
from h.heap_min_prop[OF INV' IDX] show ?thesis
unfolding CNV_LHS CNV_RHS .
qed
text ‹With the above lemma, the correctness proof is straightforward›
lemma hm_pop_min_α_correct: "hm_pop_min_op hm ≤⇩n SPEC (λ((k,v),hm').
heapmap_α hm k = Some v
∧ heapmap_α hm' = (heapmap_α hm)(k:=None)
∧ (∀k' v'. heapmap_α hm k' = Some v' ⟶ prio v ≤ prio v'))"
unfolding hm_pop_min_op_def hm_key_of_op_unfold hm_the_lookup_op_def
apply (refine_vcg
hm_exch_op_α_correct[THEN leof_trans]
hm_butlast_op_α_correct[THEN leof_trans]
hm_sink_op_α_correct[THEN leof_trans]
)
apply (auto simp: heapmap_min_prop)
done
lemma heapmap_nres_rel_prodI:
assumes "hmx ≤ ⇓(UNIV ×⇩r hmr_rel) h'x"
assumes "h'x ≤ SPEC (λ(_,h'). h.heap_invar h')"
assumes "hmx ≤⇩n SPEC (λ(r,hm'). RETURN (r,heapmap_α hm') ≤ ⇓(R×⇩rId) hx)"
shows "hmx ≤ ⇓(R×⇩rheapmap_rel) hx"
using assms
unfolding heapmap_rel_def hmr_rel_def br_def heapmap_invar_def
apply (auto simp: pw_le_iff pw_leof_iff refine_pw_simps; blast)
done
lemma hm_pop_min_op_aref: "(hm_pop_min_op, PR_CONST (mop_pm_pop_min prio)) ∈ heapmap_rel → ⟨(Id×⇩rId)×⇩rheapmap_rel⟩nres_rel"
unfolding PR_CONST_def
apply (intro fun_relI nres_relI)
apply (frule heapmap_hmr_relI)
unfolding mop_pm_pop_min_alt
apply (intro ASSERT_refine_right)
apply (rule heapmap_nres_rel_prodI)
apply (rule hm_pop_min_op_refine[param_fo, THEN nres_relD]; assumption)
unfolding heapmap_rel_def hmr_rel_def in_br_conv
apply (refine_vcg; simp)
apply (refine_vcg hm_pop_min_α_correct[THEN leof_trans]; simp split: prod.splits)
done
text_raw ‹\paragraph{Second approach}›
definition "hm_kv_of_op hm i ≡ do {
ASSERT (hm_valid hm i ∧ hmr_invar hm);
k ← hm_key_of_op hm i;
v ← hm_the_lookup_op hm k;
RETURN (k, v)
}"
definition "kvi_rel hm i ≡ {((k,v),v) | k v. hm_key_of hm i = k}"
lemma hm_kv_op_refine[refine]:
assumes "(hm,h)∈hmr_rel"
shows "hm_kv_of_op hm i ≤ ⇓(kvi_rel hm i) (h.val_of_op h i)"
unfolding hm_kv_of_op_def h.val_of_op_def kvi_rel_def
hm_key_of_op_unfold hm_the_lookup_op_def
apply simp
apply refine_vcg
using assms
by (auto
simp: hm_valid_def hm_length_def hmr_rel_defs heapmap_α_def hm_key_of_def
split: prod.splits)
definition hm_pop_min_op' :: "('k,'v) ahm ⇒ (('k×'v) × ('k,'v) ahm) nres" where
"hm_pop_min_op' hm ≡ do {
ASSERT (heapmap_invar hm);
ASSERT (hm_valid hm 1);
kv ← hm_kv_of_op hm 1;
let l = hm_length hm;
hm ← hm_exch_op hm 1 l;
hm ← hm_butlast_op hm;
if (l≠1) then do {
hm ← hm_sink_op hm 1;
RETURN (kv,hm)
} else RETURN (kv,hm)
}"
lemma hm_pop_min_op_refine':
"⟦ (hm,h)∈hmr_rel ⟧ ⟹ hm_pop_min_op' hm ≤ ⇓(kvi_rel hm 1 ×⇩r hmr_rel) (h.pop_min_op h)"
unfolding hm_pop_min_op'_def h.pop_min_op_def
unfolding ignore_snd_refine_conv
apply refine_rcg
unfolding hmr_rel_def heapmap_rel_def
apply (unfold heapmap_invar_def; simp add: in_br_conv)
apply (simp_all add: in_br_conv)
done
lemma heapmap_nres_rel_prodI':
assumes "hmx ≤ ⇓(S ×⇩r hmr_rel) h'x"
assumes "h'x ≤ SPEC Φ"
assumes "⋀h' r. Φ (r,h') ⟹ h.heap_invar h'"
assumes "hmx ≤⇩n SPEC (λ(r,hm'). (∃r'. (r,r')∈S ∧ Φ (r',hmr_α hm')) ∧ hmr_invar hm' ⟶ RETURN (r,heapmap_α hm') ≤ ⇓(R×⇩rId) hx)"
shows "hmx ≤ ⇓(R×⇩rheapmap_rel) hx"
using assms
unfolding heapmap_rel_def hmr_rel_def heapmap_invar_def
apply (auto
simp: pw_le_iff pw_leof_iff refine_pw_simps in_br_conv
)
by meson
lemma ex_in_kvi_rel_conv:
"(∃r'. (r,r')∈kvi_rel hm i ∧ Φ r') ⟷ (fst r = hm_key_of hm i ∧ Φ (snd r))"
unfolding kvi_rel_def
apply (cases r)
apply auto
done
lemma hm_pop_min_aref': "(hm_pop_min_op', mop_pm_pop_min prio) ∈ heapmap_rel → ⟨(Id×⇩rId) ×⇩r heapmap_rel⟩nres_rel"
apply (intro fun_relI nres_relI)
apply (frule heapmap_hmr_relI)
unfolding mop_pm_pop_min_alt
apply (intro ASSERT_refine_right)
apply (rule heapmap_nres_rel_prodI')
apply (erule hm_pop_min_op_refine')
apply (unfold heapmap_rel_def hmr_rel_def in_br_conv) []
apply (rule h.pop_min_op_correct)
apply simp
apply simp
apply simp
apply (clarsimp simp: ex_in_kvi_rel_conv split: prod.splits)
unfolding hm_pop_min_op'_def hm_kv_of_op_def hm_key_of_op_unfold
hm_the_lookup_op_def
apply (refine_vcg
hm_exch_op_α_correct[THEN leof_trans]
hm_butlast_op_α_correct[THEN leof_trans]
hm_sink_op_α_correct[THEN leof_trans]
)
unfolding heapmap_rel_def hmr_rel_def in_br_conv
apply (auto intro: ranI)
done
subsubsection ‹Remove›
definition "hm_remove_op k hm ≡ do {
ASSERT (heapmap_invar hm);
ASSERT (k ∈ dom (heapmap_α hm));
i ← hm_index_op hm k;
let l = hm_length hm;
hm ← hm_exch_op hm i l;
hm ← hm_butlast_op hm;
if i ≠ l then
hm_repair_op hm i
else
RETURN hm
}"
definition (in heapstruct) "remove_op i h ≡ do {
ASSERT (heap_invar h);
ASSERT (valid h i);
let l = length h;
h ← exch_op h i l;
h ← butlast_op h;
if i ≠ l then
repair_op h i
else
RETURN h
}"
lemma (in -) swap_empty_iff[iff]: "swap l i j = [] ⟷ l=[]"
by (auto simp: swap_def)
lemma (in heapstruct)
butlast_exch_last: "butlast (exch h i (length h)) = update (butlast h) i (last h)"
unfolding exch_def update_def
apply (cases h rule: rev_cases)
apply (auto simp: swap_def butlast_list_update)
done
lemma (in heapstruct) remove_op_invar:
"⟦ heap_invar h; valid h i ⟧ ⟹ remove_op i h ≤ SPEC heap_invar"
unfolding remove_op_def
apply refine_vcg
apply (auto simp: valid_def) []
apply (auto simp: valid_def exch_def) []
apply (simp add: butlast_exch_last)
apply refine_vcg
apply auto []
apply auto []
apply (auto simp: valid_def) []
apply auto []
apply auto []
done
lemma hm_remove_op_refine[refine]:
"⟦ (hm,m)∈heapmap_rel; (hm,h)∈hmr_rel; heapmap_α hm k ≠ None⟧ ⟹
hm_remove_op k hm ≤ ⇓hmr_rel (h.remove_op (hm_index hm k) h)"
unfolding hm_remove_op_def h.remove_op_def heapmap_rel_def
apply (refine_rcg index_op_inline_refine)
unfolding hmr_rel_def
apply (auto simp: in_br_conv)
done
lemma hm_remove_op_α_correct:
"hm_remove_op k hm ≤⇩n SPEC (λhm'. heapmap_α hm' = (heapmap_α hm)(k:=None))"
unfolding hm_remove_op_def
apply (refine_vcg
hm_exch_op_α_correct[THEN leof_trans]
hm_butlast_op_α_correct[THEN leof_trans]
hm_repair_op_α_correct[THEN leof_trans]
hm_index_op_inline_leof
)
apply (auto; fail)
apply clarsimp
apply (rewrite at "hm_index _ k = hm_length _" in asm eq_commute)
apply (auto; fail)
done
lemma hm_remove_op_aref:
"(hm_remove_op,mop_map_delete_ex) ∈ Id → heapmap_rel → ⟨heapmap_rel⟩nres_rel"
apply (intro fun_relI nres_relI)
unfolding mop_map_delete_ex_alt
apply (rule ASSERT_refine_right)
apply (frule heapmap_hmr_relI)
apply (rule heapmap_nres_relI')
apply (rule hm_remove_op_refine; assumption?)
apply (unfold heapmap_rel_def in_br_conv; auto)
unfolding heapmap_rel_def hmr_rel_def in_br_conv
apply (refine_vcg h.remove_op_invar; clarsimp; fail)
apply (refine_vcg hm_remove_op_α_correct[THEN leof_trans]; simp; fail)
done
subsubsection ‹Peek-Min›
definition hm_peek_min_op :: "('k,'v) ahm ⇒ ('k×'v) nres" where
"hm_peek_min_op hm ≡ hm_kv_of_op hm 1"
lemma hm_peek_min_op_aref:
"(hm_peek_min_op, PR_CONST (mop_pm_peek_min prio)) ∈ heapmap_rel → ⟨Id×⇩rId⟩nres_rel"
unfolding PR_CONST_def
apply (intro fun_relI nres_relI)
proof -
fix hm and m :: "'k ⇀ 'v"
assume A: "(hm,m)∈heapmap_rel"
from A have [simp]: "h.heap_invar (hmr_α hm)" "hmr_invar hm" "m=heapmap_α hm"
unfolding heapmap_rel_def in_br_conv heapmap_invar_def
by simp_all
have "hm_peek_min_op hm ≤ ⇓ (kvi_rel hm 1) (h.peek_min_op (hmr_α hm))"
unfolding hm_peek_min_op_def h.peek_min_op_def
apply (refine_rcg hm_kv_op_refine)
using A
apply (simp add: heapmap_hmr_relI)
done
also have "⟦hmr_α hm ≠ []⟧ ⟹ (h.peek_min_op (hmr_α hm))
≤ SPEC (λv. v∈ran (heapmap_α hm) ∧ (∀v'∈ran (heapmap_α hm). prio v ≤ prio v'))"
apply refine_vcg
by simp_all
finally show "hm_peek_min_op hm ≤ ⇓ (Id ×⇩r Id) (mop_pm_peek_min prio m)"
unfolding mop_pm_peek_min_alt
apply (simp add: pw_le_iff refine_pw_simps hm_peek_min_op_def hm_kv_of_op_def
hm_key_of_op_unfold hm_the_lookup_op_def)
apply (fastforce simp: kvi_rel_def ran_def)
done
qed
end
end