Theory IICF_Impl_Heap
section ‹Implementation of Heaps with Arrays›
theory IICF_Impl_Heap
imports
IICF_Abs_Heap
"../IICF_Array"
"../IICF_Array_List"
begin
term al_assn
lemma size_mset_param[param]: "(size,size)∈⟨A⟩mset_rel → nat_rel"
by (auto simp: mset_rel_def p2rel_def rel_mset_size)
lemma rdomp_ref_mk_assn_iff[simp]: "rdomp ↿(mk_assn A) = rdomp A"
by (auto simp: rdomp_def)
thm vcg_prep_ext_rules
find_theorems pure_part
lemma rdomp_arl_assn_len:
assumes "rdomp ↿(arl_assn:: ('a::llvm_rep list, 'l::len2 word × 'l word × 'a ptr) dr_assn) xs"
shows "length xs < max_snat LENGTH('l)"
using assms
by (auto
simp: rdomp_def arl_assn_def arl_assn'_def sep_algebra_simps pred_lift_extract_simps
simp: snat.assn_def
)
find_theorems vassn_tag hn_refine
lemma workaround_invalid_recombine_pure2: "is_pure B ⟹ hn_ctxt (invalid_assn A ×⇩a B) ax px ⊢ hn_invalid (A ×⇩a B) ax px"
unfolding hn_ctxt_def invalid_assn_def prod_assn_def entails_def
by (auto split: prod.split elim!: is_pureE
simp: sep_algebra_simps pure_part_pure_conj_eq)
lemma mop_list_swap_unfold: "mop_list_swap xs i j = do {
xi ← mop_list_get xs i;
xj ← mop_list_get xs j;
xs ← mop_list_set xs i xj;
mop_list_set xs j xi
}"
by (auto simp: pw_eq_iff refine_pw_simps swap_def)
text ‹We implement the heap data structure by an array.
The implementation is automatically synthesized by the Sepref-tool.
›
subsection ‹Setup of the Sepref-Tool›
lemma mset_rel_id: "⟨Id⟩mset_rel = Id"
unfolding mset_rel_def apply (simp add: rel2p multiset.rel_eq)
by (simp only: p2rel)
locale heap_impl = heapstruct prio for prio :: "'e ⇒ 'p::linorder" +
fixes prio_assn :: "'p ⇒ 'pi::llvm_rep ⇒ assn"
and elem_assn :: "'e ⇒ 'ei::llvm_rep ⇒ assn"
and prio_impl le_prio_impl lt_prio_impl
and ltype :: "'l::len2 itself"
assumes prio_is_pure[safe_constraint_rules]: "is_pure prio_assn"
assumes elem_is_pure[safe_constraint_rules]: "is_pure elem_assn"
assumes prio_impl_refine[sepref_fr_rules]: "(prio_impl, RETURN o prio)∈elem_assn⇧k →⇩a prio_assn"
assumes le_prio_impl_refine[sepref_fr_rules]:
"(uncurry le_prio_impl, uncurry (RETURN oo (≤))) ∈ prio_assn⇧k *⇩a prio_assn⇧k →⇩a bool1_assn"
assumes lt_prio_impl_refine[sepref_fr_rules]:
"(uncurry lt_prio_impl, uncurry (RETURN oo (<))) ∈ prio_assn⇧k *⇩a prio_assn⇧k →⇩a bool1_assn"
fixes N defines "N≡LENGTH('l)"
begin
abbreviation "assn ≡ al_assn' TYPE('l) elem_assn"
abbreviation "idx_assn ≡ snat_assn' TYPE('l)"
definition "heap_assn ≡ hr_comp (al_assn elem_assn) heap_rel1"
lemma mk_free_heap_assn[sepref_frame_free_rules]: "MK_FREE heap_assn arl_free"
unfolding heap_assn_def
by (rule sepref_frame_free_rules)+
sepref_register prio
sepref_register "(≤) :: 'p ⇒ 'p ⇒ bool"
sepref_register "(<) :: 'p ⇒ 'p ⇒ bool"
lemmas [sepref_frame_free_rules] =
mk_free_is_pure[OF prio_is_pure]
mk_free_is_pure[OF elem_is_pure]
sepref_register update_op
sepref_definition update_impl is "uncurry2 update_op"
:: "assn⇧d *⇩a idx_assn⇧k *⇩a elem_assn⇧k →⇩a assn"
unfolding update_op_def[abs_def]
apply (annot_snat_const "TYPE('l)")
by sepref
lemmas [sepref_fr_rules] = update_impl.refine
sepref_register val_of_op
sepref_definition val_of_impl is "uncurry val_of_op" :: "assn⇧k *⇩a idx_assn⇧k →⇩a elem_assn"
unfolding val_of_op_def[abs_def]
apply (annot_snat_const "TYPE('l)")
by sepref
lemmas [sepref_fr_rules] = val_of_impl.refine
sepref_register exch_op
sepref_definition exch_impl is "uncurry2 exch_op" :: "assn⇧d *⇩a idx_assn⇧k *⇩a idx_assn⇧k →⇩a assn"
unfolding exch_op_def[abs_def] mop_list_swap_unfold
apply (annot_snat_const "TYPE('l)")
by sepref
lemmas [sepref_fr_rules] = exch_impl.refine
sepref_register valid
sepref_definition valid_impl is "uncurry (RETURN oo valid)" :: "assn⇧k *⇩a idx_assn⇧k →⇩a bool1_assn"
unfolding valid_def[abs_def]
apply (annot_snat_const "TYPE('l)")
by sepref
lemmas [sepref_fr_rules] = valid_impl.refine
sepref_register prio_of_op
sepref_definition prio_of_impl is "uncurry (PR_CONST prio_of_op)" :: "assn⇧k *⇩a idx_assn⇧k →⇩a prio_assn"
unfolding prio_of_op_def[abs_def] PR_CONST_def
by sepref
lemmas [sepref_fr_rules] = prio_of_impl.refine
sepref_definition append_impl is "uncurry mop_list_append"
:: "[λ(xs,_). length xs + 1 < max_snat LENGTH('l)]⇩a assn⇧d *⇩a elem_assn⇧k → assn"
by sepref
lemmas [sepref_fr_rules] = append_impl.refine
sepref_register swim_op
sepref_definition swim_impl is
"uncurry (PR_CONST swim_op)" :: "[λ_. 4<LENGTH('l)]⇩a assn⇧d *⇩a idx_assn⇧k → assn"
unfolding swim_op_def[abs_def] parent_def PR_CONST_def
apply (annot_snat_const "TYPE('l)")
supply [sepref_frame_match_rules] = workaround_invalid_recombine_pure2[where B=snat_assn, simplified]
by sepref_dbg_keep
lemmas [sepref_fr_rules] = swim_impl.refine
lemma overflow_safe_hbound_check: "2*k≤n ⟷ k≤n div 2" for k n :: nat by auto
sepref_register sink_op
sepref_definition sink_impl is "uncurry (PR_CONST sink_op)" :: "[λ_. 4<LENGTH('l)]⇩a assn⇧d *⇩a idx_assn⇧k → assn"
unfolding sink_op_opt_def[abs_def] sink_op_opt_eq[symmetric,abs_def] PR_CONST_def
unfolding overflow_safe_hbound_check Suc_eq_plus1
supply [sepref_frame_match_rules] = workaround_invalid_recombine_pure2[where B=snat_assn, simplified]
apply (annot_snat_const "TYPE('l)")
by sepref
lemmas [sepref_fr_rules] = sink_impl.refine
lemma prenorm_heaprel1_len: "(h,m)∈heap_rel1 ⟹ length h = size m"
unfolding heap_rel1_def in_br_conv
by auto
lemma max_snat_param: "(max_snat,max_snat)∈nat_rel → nat_rel" by simp
context
notes [fcomp_norm_unfold] = heap_assn_def[symmetric] list_rel_id_simp mset_rel_id
notes [fcomp_prenorm_simps] = prenorm_heaprel1_len
notes [param] = IdI[of N] max_snat_param
begin
sepref_definition empty_impl is "uncurry0 empty_op" :: "[λ_. 4<N]⇩a unit_assn⇧k → assn"
unfolding empty_op_def N_def
apply (rewrite al_fold_custom_empty[where 'l='l])
by sepref
sepref_decl_impl (no_register) heap_empty: empty_impl.refine[FCOMP empty_op_refine]
uses op_mset_empty.fref[of Id] .
sepref_definition is_empty_impl is "is_empty_op" :: "assn⇧k →⇩a bool1_assn"
unfolding is_empty_op_def[abs_def]
apply (annot_snat_const "TYPE('l)")
by sepref
sepref_decl_impl heap_is_empty: is_empty_impl.refine[FCOMP is_empty_op_refine]
uses op_mset_is_empty.fref[of Id] .
sepref_definition insert_impl
is "uncurry insert_op" :: "[λ(_,xs). 4<N ∧ length xs+1 < max_snat N]⇩a elem_assn⇧k *⇩a assn⇧d → assn"
unfolding insert_op_def[abs_def] append_op_def N_def
by sepref
sepref_decl_impl heap_insert: insert_impl.refine[FCOMP insert_op_refine]
uses op_mset_insert.fref[of Id] .
sepref_definition pop_min_impl is "pop_min_op" :: "[λ_. 4<N]⇩a assn⇧d → elem_assn ×⇩a assn"
unfolding pop_min_op_def[abs_def] butlast_op_def N_def
apply (annot_snat_const "TYPE('l)")
by sepref
sepref_decl_impl (no_mop) heap_pop_min: pop_min_impl.refine[FCOMP pop_min_op_refine]
uses op_prio_pop_min.fref[of Id] .
sepref_definition peek_min_impl is "peek_min_op" :: "assn⇧k →⇩a elem_assn"
unfolding peek_min_op_def[abs_def]
apply (annot_snat_const "TYPE('l)")
by sepref
sepref_decl_impl (no_mop) heap_peek_min: peek_min_impl.refine[FCOMP peek_min_op_refine]
uses op_prio_peek_min.fref[of Id] .
end
end