Theory Sepref_ICF_Bindings
theory Sepref_ICF_Bindings
imports Sepref_Tool
Collections.Refine_Dflt_ICF
"IICF/IICF"
begin
subsection ‹Miscellaneous›
lemma (in -) rev_append_hnr[param,sepref_import_param]:
"(rev_append, rev_append) ∈ ⟨A⟩list_rel → ⟨A⟩list_rel → ⟨A⟩list_rel"
unfolding rev_append_def by parametricity
subsection ‹Sets by List›
lemma lsr_finite[simp, intro]: "(l,s)∈⟨R⟩list_set_rel ⟹ finite s"
by (auto simp: list_set_rel_def br_def)
lemma it_to_sorted_list_triv:
assumes "distinct l"
shows "RETURN l ≤ it_to_sorted_list (λ_ _. True) (set l)"
using assms unfolding it_to_sorted_list_def
by refine_vcg auto
lemma [sepref_gen_algo_rules]: "GEN_ALGO (return) (IS_TO_SORTED_LIST (λ_ _. True) (pure (⟨A⟩list_set_rel)) (pure A))"
unfolding GEN_ALGO_def IS_TO_SORTED_LIST_def
apply (simp add: list_assn_pure_conv)
apply rule
apply rule
apply (sep_auto simp: pure_def intro: it_to_sorted_list_triv simp: list_set_rel_def br_def)
done
lemma list_set_rel_compp:
assumes "IS_LEFT_UNIQUE A" "IS_RIGHT_UNIQUE A"
shows "⟨Id⟩list_set_rel O ⟨A⟩set_rel = ⟨A⟩list_set_rel"
unfolding list_set_rel_def
proof (safe; clarsimp simp: in_br_conv)
fix x z
assume "(set x,z)∈⟨A⟩set_rel" "distinct x"
from obtain_list_from_setrel[OF ‹IS_RIGHT_UNIQUE A› this(1)] obtain zl where
[simp]: "z = set zl" and X_ZL: "(x, zl) ∈ ⟨A⟩list_rel" .
have "distinct zl"
using param_distinct[OF assms, THEN fun_relD, OF X_ZL] ‹distinct x›
by auto
show "(x,z) ∈ ⟨A⟩list_rel O br set distinct"
apply (rule relcompI[OF X_ZL])
by (auto simp: in_br_conv ‹distinct zl›)
next
fix x y
assume XY: "(x, y) ∈ ⟨A⟩list_rel" and "distinct y"
have "distinct x"
using param_distinct[OF assms, THEN fun_relD, OF XY] ‹distinct y›
by auto
show "(x, set y) ∈ br set distinct O ⟨A⟩set_rel"
apply (rule relcompI[where b="set x"])
subgoal by (auto simp: in_br_conv ‹distinct x›)
subgoal by (rule param_set[OF ‹IS_RIGHT_UNIQUE A›, THEN fun_relD, OF XY])
done
qed
lemma GEN_OP_EQ_Id: "GEN_OP (=) (=) (Id→Id→bool_rel)" by simp
hide_const (open) Intf_Set.op_set_isEmpty Intf_Set.op_set_delete
lemma autoref_import_set_unfolds:
"{} = op_set_empty"
"uncurry (RETURN oo (∈)) = uncurry (RETURN oo op_set_member)"
"Intf_Set.op_set_isEmpty = IICF_Set.op_set_is_empty"
"Intf_Set.op_set_delete = IICF_Set.op_set_delete"
"insert = IICF_Set.op_set_insert"
by (auto intro!: ext)
context fixes A :: "'a ⇒ 'ai ⇒ assn" begin
private lemma APA: "⟦PROP Q; CONSTRAINT is_pure A⟧ ⟹ PROP Q" .
private lemma APAru: "⟦PROP Q; CONSTRAINT (IS_PURE IS_RIGHT_UNIQUE) A⟧ ⟹ PROP Q" .
private lemma APAlu: "⟦PROP Q; CONSTRAINT (IS_PURE IS_LEFT_UNIQUE) A⟧ ⟹ PROP Q" .
private lemma APAbu: "⟦PROP Q; CONSTRAINT (IS_PURE IS_LEFT_UNIQUE) A; CONSTRAINT (IS_PURE IS_RIGHT_UNIQUE) A⟧ ⟹ PROP Q" .
definition "list_set_assn = pure (⟨Id⟩list_set_rel O ⟨the_pure A⟩set_rel)"
context
notes [fcomp_norm_unfold] = list_set_assn_def[symmetric]
notes [simp] = IS_LEFT_UNIQUE_def
begin
lemmas hnr_op_ls_empty = list_set_autoref_empty[of Id, sepref_param, unfolded autoref_import_set_unfolds,
FCOMP op_set_empty.fref[of "the_pure A"]]
lemmas hnr_mop_ls_empty = hnr_op_ls_empty[FCOMP mk_mop_rl0_np[OF mop_set_empty_alt]]
definition [simp]: "op_ls_empty = op_set_empty"
sepref_register op_ls_empty
lemmas hnr_op_ls_is_empty[sepref_fr_rules] = list_set_autoref_isEmpty[of Id, sepref_param, THEN APA, unfolded autoref_import_set_unfolds,
FCOMP op_set_is_empty.fref[of "the_pure A"]]
lemmas hnr_mop_ls_is_empty[sepref_fr_rules] = hnr_op_ls_is_empty[FCOMP mk_mop_rl1_np[OF mop_set_is_empty_alt]]
lemmas hnr_op_ls_member[sepref_fr_rules] = list_set_autoref_member[OF GEN_OP_EQ_Id, sepref_param, THEN APAlu, unfolded autoref_import_set_unfolds,
FCOMP op_set_member.fref[of "the_pure A"]]
lemmas hnr_mop_ls_member[sepref_fr_rules] = hnr_op_ls_member[FCOMP mk_mop_rl2_np[OF mop_set_member_alt]]
lemmas hnr_op_ls_insert[sepref_fr_rules] = list_set_autoref_insert[OF GEN_OP_EQ_Id, sepref_param, THEN APAru, unfolded autoref_import_set_unfolds,
FCOMP op_set_insert.fref[of "the_pure A"]]
lemmas hnr_mop_ls_insert[sepref_fr_rules] = hnr_op_ls_insert[FCOMP mk_mop_rl2_np[OF mop_set_insert_alt]]
lemmas hnr_op_ls_delete[sepref_fr_rules] = list_set_autoref_delete[OF GEN_OP_EQ_Id, sepref_param, THEN APAbu, unfolded autoref_import_set_unfolds,
FCOMP op_set_delete.fref[of "the_pure A"]]
lemmas hnr_mop_ls_delete[sepref_fr_rules] = hnr_op_ls_delete[FCOMP mk_mop_rl2_np[OF mop_set_delete_alt]]
text ‹Adapting this optimization from Autoref. ›
sepref_decl_op set_insert_dj: "insert" :: "[λ(x,s). x∉s]⇩f K ×⇩r ⟨K⟩set_rel → ⟨K⟩set_rel"
where "IS_RIGHT_UNIQUE K" "IS_LEFT_UNIQUE K" .
lemma fold_set_insert_dj: "Set.insert = op_set_insert_dj" by simp
lemma ls_insert_dj_hnr_aux:
"(uncurry (return oo Cons), uncurry mop_set_insert_dj) ∈ (pure Id)⇧k *⇩a (pure (⟨Id⟩list_set_rel))⇧k →⇩a pure (⟨Id⟩list_set_rel)"
using list_set_autoref_insert_dj[where R=Id,param_fo]
apply (sep_auto intro!: hfrefI hn_refineI simp: pure_def refine_pw_simps eintros del: exI)
apply force
done
lemmas ls_insert_dj_hnr[sepref_fr_rules] = ls_insert_dj_hnr_aux[THEN APAbu, FCOMP mop_set_insert_dj.fref[of "the_pure A"]]
lemmas ls_insert_dj_hnr_mop[sepref_fr_rules]
= ls_insert_dj_hnr[FCOMP mk_op_rl2[OF mop_set_insert_dj_alt]]
private lemma hd_in_set_conv: "hd l ∈ set l ⟷ l≠[]" by auto
lemma ls_pick_hnr_aux: "(return o hd, mop_set_pick) ∈ (pure (⟨Id⟩list_set_rel))⇧k →⇩a id_assn"
apply (sep_auto
intro!: hfrefI hn_refineI
simp: pure_def IS_PURE_def IS_ID_def list_set_rel_def refine_pw_simps
eintros del: exI)
apply (auto simp: in_br_conv hd_in_set_conv)
done
lemmas ls_pick_hnr[sepref_fr_rules] = ls_pick_hnr_aux[THEN APA,FCOMP mop_set_pick.fref[of "the_pure A"]]
lemma ls_pick_hnr_mop[sepref_fr_rules]: "CONSTRAINT is_pure A ⟹ (return ∘ hd, op_set_pick) ∈ [λs. s≠{}]⇩a list_set_assn⇧k → A"
using ls_pick_hnr
by (simp add: hfref_to_ASSERT_conv mop_set_pick_alt[abs_def])
end
end
interpretation ls: set_custom_empty "return []" op_ls_empty
by unfold_locales simp
lemmas [sepref_fr_rules] = hnr_op_ls_empty[folded op_ls_empty_def]
end