theory Sepref_IICF_Bindings
imports Sepref_Tool
"Sepref_HOL_Bindings"
"../Collections/Examples/Autoref/Succ_Graph"
"../Separation_Logic_Imperative_HOL/Sep_Examples"
"../Collections/Refine_Dflt_ICF"
begin
subsubsection {* List-Set *}
lemmas [sepref_import_param] =
list_set_autoref_empty
list_set_autoref_member
list_set_autoref_insert
list_set_autoref_delete
subsubsection {* Imperative Set *}
lemma (in imp_set_empty) hn_set_empty:
shows "hn_refine emp (empty) emp (is_set) (RETURN${})"
unfolding hn_refine_def
by (sep_auto simp: hn_ctxt_def)
lemma (in imp_set_ins) hn_set_ins:
shows
"hn_refine (hn_ctxt is_set s s' * hn_val Id x x') (ins x' s')
(hn_invalid s s' * hn_val Id x x') is_set (RETURN$(insert$x$s))"
unfolding hn_refine_def hn_ctxt_def pure_def
by sep_auto
lemma (in imp_set_memb) hn_set_memb:
"hn_refine (hn_ctxt is_set s s' * hn_val Id x x') (memb x' s')
(hn_ctxt is_set s s' * hn_val Id x x') (pure bool_rel)
(RETURN$(op ∈$x$s))"
unfolding hn_refine_def hn_ctxt_def pure_def
by sep_auto
lemma (in imp_set_delete) hn_set_delete:
shows
"hn_refine (hn_ctxt is_set s s' * hn_val Id x x') (delete x' s')
(hn_invalid s s' * hn_val Id x x') is_set (RETURN$(op_set_delete$x$s))"
unfolding hn_refine_def hn_ctxt_def pure_def
by sep_auto
lemmas (in imp_set) [constraint_rules] = precise
text {* Empty set with initial size hint *}
definition empty_set_sz :: "nat => 'a set"
where [simp]: "empty_set_sz n == {}"
lemma hn_ias_empty_sz[sepref_fr_rules]: "hn_refine
(hn_val nat_rel s s') (ias_new_sz s') (hn_val nat_rel s s') is_ias
(RETURN$(empty_set_sz$s))"
by rule sep_auto
lemmas [sepref_fr_rules] =
hs.hn_set_empty hs.hn_set_ins hs.hn_set_memb hs.hn_set_delete
lemmas [sepref_fr_rules] =
ias.hn_set_empty ias.hn_set_ins ias.hn_set_memb ias.hn_set_delete
lemma pat_set_delete[pat_rules]: "op-$s$(insert$x${}) ≡ op_set_delete$x$s"
by simp
subsubsection {* Imperative Map *}
context imp_map begin
definition "is_map_rel Rk Rv m mi ≡ is_map m mi * \<up>(Rk=pure Id ∧ Rv=pure Id)"
lemma is_map_rel_eq[simp]:
"IS_PURE_ID Rk ==> IS_PURE_ID Rv ==> is_map_rel Rk Rv = is_map"
apply (intro ext)
unfolding is_map_rel_def pure_def IS_PURE_ID_alt_def
by auto
lemma precise_rel: "precise (is_map_rel Rk Rv)"
using precise
by (simp add: is_map_rel_def[abs_def] precise_def)
end
lemma (in imp_map_empty) hn_map_empty:
assumes "INDEP Rk" "INDEP Rv"
assumes "CONSTRAINT IS_PURE_ID Rk"
assumes "CONSTRAINT IS_PURE_ID Rv"
shows "hn_refine emp (empty) emp (is_map_rel Rk Rv) (RETURN$op_map_empty)"
unfolding hn_refine_def
using assms
by (sep_auto simp: hn_ctxt_def)
lemma (in imp_map_is_empty) hn_map_is_empty:
shows "hn_refine (hn_ctxt (is_map_rel Rk Rv) m mi) (is_empty mi) (hn_ctxt (is_map_rel Rk Rv) m mi) (pure bool_rel) (RETURN$(op_map_is_empty$m))"
apply rule
unfolding hn_ctxt_def pure_def is_map_rel_def
by sep_auto
lemma (in imp_map_lookup) hn_map_lookup:
shows "hn_refine
(hn_ctxt (is_map_rel Rk Rv) m mi * hn_ctxt Rk k ki)
(lookup ki mi)
(hn_ctxt (is_map_rel Rk Rv) m mi * hn_ctxt Rk k ki)
(hn_option_aux Rv)
(RETURN$(op_map_lookup$k$m))"
apply rule
using assms
unfolding hn_ctxt_def is_map_rel_def
apply (simp add: hn_option_pure_conv)
by (sep_auto simp: pure_def)
lemma (in imp_map_update) hn_map_update:
shows "hn_refine
(hn_ctxt (is_map_rel Rk Rv) m mi * hn_ctxt Rk k ki * hn_ctxt Rv v vi)
(update ki vi mi)
(hn_invalid m mi * hn_ctxt Rk k ki * hn_ctxt Rv v vi)
(is_map_rel Rk Rv)
(RETURN$(op_map_update$k$v$m))"
apply rule
using assms
unfolding hn_ctxt_def pure_def is_map_rel_def
by sep_auto
lemma (in imp_map_delete) hn_map_delete:
shows "hn_refine
(hn_ctxt (is_map_rel Rk Rv) m mi * hn_ctxt Rk k ki)
(delete k mi)
(hn_invalid m mi * hn_ctxt Rk k ki)
(is_map_rel Rk Rv)
(RETURN$(op_map_delete$k$m))"
apply rule
using assms
unfolding hn_ctxt_def pure_def is_map_rel_def
by sep_auto
lemma (in imp_map_add) hn_map_add:
"hn_refine
(hn_ctxt (is_map_rel Rk Rv) m1 mi1 * hn_ctxt (is_map_rel Rk Rv) m2 mi2)
(add mi1 mi2)
(hn_ctxt (is_map_rel Rk Rv) m1 mi1 * hn_ctxt (is_map_rel Rk Rv) m2 mi2)
(is_map_rel Rk Rv)
(RETURN$(op++$m1$m2))"
apply rule
unfolding hn_ctxt_def pure_def is_map_rel_def
by sep_auto
lemmas [sepref_fr_rules] =
hm.hn_map_empty hm.hn_map_is_empty hm.hn_map_lookup hm.hn_map_delete hm.hn_map_update
iam.hn_map_empty iam.hn_map_lookup iam.hn_map_delete iam.hn_map_update
lemmas (in imp_map) [constraint_rules] = precise precise_rel
subsection "Graphs"
typedecl 'v i_slg
lemma pat_slg_succs[pat_rules]:
"op``$E$(insert$v${}) == slg_succs$E$v" by simp
lemma id_slg_succs[id_rules]:
"slg_succs ::⇩i TYPE('v i_slg => 'v => 'v set)" by simp
lemmas [sepref_import_param] = refine_slg_succs
subsection ‹Unique priority queues (from functional ICF)›
typedecl ('e,'a) i_uprio
lemma [sepref_la_skel]:
"SKEL (prio_pop_min$a) = la_op a" by simp
lemmas [id_rules] =
itypeI[of op_uprio_empty "TYPE(('a,'b)i_uprio)"]
itypeI[of op_uprio_insert "TYPE(('a,'b)i_uprio => 'a => 'b => ('a,'b)i_uprio)"]
itypeI[of prio_pop_min "TYPE(('a,'b)i_uprio => ('a×'b×('a,'b)i_uprio) nres)"]
itypeI[of op_uprio_is_empty "TYPE(('a,'b)i_uprio => bool)"]
itypeI[of op_uprio_prio "TYPE(('a,'b)i_uprio => 'a => 'b option)"]
lemma pat_uprio_empty[pat_rules]:
"(λ⇩2_. None)::('e \<rightharpoonup> 'a::linorder) ≡ op_uprio_empty"
by simp
lemma pat_uprio_insert[pat_rules]:
"fun_upd$m$k$(Some$v) ≡ op_uprio_insert$'m$'k$'v"
by simp
lemma pat_uprio_lookup[pat_rules]:
"m$k ≡ op_uprio_prio$'m$'k"
by simp
lemma pat_uprio_is_empty[pat_rules]:
"op =$m$(λ⇩2_. None) ≡ op_uprio_is_empty$m"
"op =$(λ⇩2_. None)$m ≡ op_uprio_is_empty$m"
"op =$(dom$m)${} ≡ op_uprio_is_empty$m"
"op =${}$(dom$m) ≡ op_uprio_is_empty$m"
unfolding atomize_eq
by auto
context uprio begin
definition "is_uprio Rk Rv c ci ≡ \<up>(Rk=pure Id ∧ Rv=pure Id ∧ c=α ci ∧ invar ci)"
lemma is_uprio_alt_def: "is_uprio Rk Rv c ci
= \<up>(Rk=pure Id ∧ Rv=pure Id) * pure (br α invar) c ci"
unfolding is_uprio_def pure_def
apply (auto simp: br_def)
done
lemma [constraint_rules]: "precise (is_uprio Rk Rv)"
unfolding is_uprio_alt_def[abs_def]
by (simp add: precise_pure)
end
lemma (in uprio_empty) sepref_empty[sepref_fr_rules]:
assumes "CONSTRAINT IS_PURE_ID Rk"
assumes "CONSTRAINT IS_PURE_ID Rv"
shows
"hn_refine emp (return (empty ())) emp (is_uprio Rk Rv) (RETURN$op_uprio_empty)"
apply rule
using assms
apply (simp add: IS_PURE_ID_alt_def is_uprio_def)
apply (sep_auto simp: empty_correct)
done
lemma (in uprio_insert) sepref_insert[sepref_fr_rules]:
shows
"hn_refine
(hn_ctxt (is_uprio Rk Rv) m mi * hn_ctxt Rk k ki * hn_ctxt Rv v vi)
(return (insert mi ki vi))
(hn_ctxt (is_uprio Rk Rv) m mi * hn_ctxt Rk k ki * hn_ctxt Rv v vi)
(is_uprio Rk Rv)
(RETURN$(op_uprio_insert$m$k$v))"
apply rule
using assms
apply (simp add: hn_ctxt_def is_uprio_def pure_def)
by (sep_auto simp: insert_correct)
lemma (in uprio_isEmpty) sepref_is_empty[sepref_fr_rules]:
"hn_refine
(hn_ctxt (is_uprio Rk Rv) m mi)
(return (isEmpty mi))
(hn_ctxt (is_uprio Rk Rv) m mi)
(pure bool_rel)
(RETURN$(op_uprio_is_empty$m))"
apply rule
using assms
apply (simp add: hn_ctxt_def is_uprio_def pure_def)
by (sep_auto simp: isEmpty_correct)
lemma (in uprio_prio) sepref_prio[sepref_fr_rules]:
shows
"hn_refine
(hn_ctxt (is_uprio Rk Rv) m mi * hn_ctxt Rk k ki)
(return (prio mi ki))
(hn_ctxt (is_uprio Rk Rv) m mi * hn_ctxt Rk k ki)
(hn_option_aux Rv)
(RETURN$(op_uprio_prio$m$k))"
apply rule
apply (simp add: hn_ctxt_def is_uprio_def)
apply (simp add: hn_option_pure_conv)
by (sep_auto simp: prio_correct pure_def)
lemma (in uprio_pop) sepref_prio_pop_min[sepref_fr_rules]:
"hn_refine
(hn_ctxt (is_uprio Rk Rv) m mi)
(return (pop mi))
(hn_ctxt (is_uprio Rk Rv) m mi)
(hn_prod_aux Rk (hn_prod_aux Rv (is_uprio Rk Rv)))
(prio_pop_min$m)"
apply (rule)
apply (simp add: hn_ctxt_def is_uprio_alt_def[abs_def])
apply (simp add: hn_prod_pure_conv)
apply (clarsimp simp: pure_def)
apply (erule (1) return_refine_prop_return[OF _ prio_pop_min_refine])
apply (sep_auto)
done
end