# Theory Refine_Imperative_HOL.IICF_Prio_Bag

```section ‹Priority Bag Interface›
theory IICF_Prio_Bag
imports IICF_Multiset
begin
subsection ‹Operations›

text ‹We prove quite general parametricity lemmas, but restrict
them to relations below identity when we register the operations.

This restriction, although not strictly necessary, makes usage of the tool
much simpler, as we do not need to handle different prio-functions for
abstract and concrete types.
›

context
fixes prio:: "'a ⇒ 'b::linorder"
begin
definition "mop_prio_pop_min b = ASSERT (b≠{#}) ⪢ SPEC (λ(v,b').
v ∈# b
∧ b'=b - {#v#}
∧ (∀v'∈set_mset b. prio v ≤ prio v'))"

definition "mop_prio_peek_min b ≡ ASSERT (b≠{#}) ⪢ SPEC (λv.
v ∈# b
∧ (∀v'∈set_mset b. prio v ≤ prio v'))"

end

lemma param_mop_prio_pop_min[param]:
assumes [param]: "(prio',prio) ∈ A → B"
assumes [param]: "((≤),(≤)) ∈ B → B → bool_rel"
shows "(mop_prio_pop_min prio',mop_prio_pop_min prio) ∈ ⟨A⟩mset_rel → ⟨A ×⇩r ⟨A⟩mset_rel⟩nres_rel"
unfolding mop_prio_pop_min_def[abs_def]
apply (clarsimp simp: mop_prio_pop_min_def nres_rel_def pw_le_iff refine_pw_simps)
apply (safe; simp)
proof goal_cases
case (1 m n x)
(*fix m n x*)
assume "(m,n)∈⟨A⟩mset_rel"
and "x∈#m"
and P': "∀x'∈set_mset m. prio' x ≤ prio' x'"
hence R: "rel_mset (rel2p A) m n" by (simp add: mset_rel_def p2rel_def)
from multi_member_split[OF ‹x∈#m›] obtain m' where [simp]: "m=m'+{#x#}" by auto

from msed_rel_invL[OF R[simplified]] obtain n' y where
[simp]: "n=n'+{#y#}" and [param, simp]: "(x,y)∈A" and R': "(m',n')∈⟨A⟩mset_rel"
by (auto simp: rel2p_def mset_rel_def p2rel_def)
have "∀y'∈set_mset n. prio y ≤ prio y'"
proof
fix y' assume "y'∈set_mset n"
then obtain x' where [param]: "(x',y')∈A" and "x'∈set_mset m"
using R
by (metis insert_DiffM msed_rel_invR rel2pD union_single_eq_member)
with P' have "prio' x ≤ prio' x'" by blast
moreover have "(prio' x ≤ prio' x', prio y ≤ prio y') ∈ bool_rel"
by parametricity
ultimately show "prio y ≤ prio y'" by simp
qed
thus
"∃a. (x, a) ∈ A ∧ (m - {#x#}, n - {#a#}) ∈ ⟨A⟩mset_rel ∧ a ∈# n ∧ (∀v'∈set_mset n. prio a ≤ prio v')"
using R' by (auto intro!: exI[where x=n'] exI[where x=y])
qed

lemma param_mop_prio_peek_min[param]:
assumes [param]: "(prio',prio) ∈ A → B"
assumes [param]: "((≤),(≤)) ∈ B → B → bool_rel"
shows "(mop_prio_peek_min prio',mop_prio_peek_min prio) ∈ ⟨A⟩mset_rel → ⟨A⟩nres_rel"
unfolding mop_prio_peek_min_def[abs_def]
apply (clarsimp
simp: mop_prio_pop_min_def nres_rel_def pw_le_iff refine_pw_simps
)
apply (safe; simp?)
proof -
fix m n x
assume "(m,n)∈⟨A⟩mset_rel"
and "x∈#m"
and P': "∀x'∈set_mset m. prio' x ≤ prio' x'"
hence R: "rel_mset (rel2p A) m n" by (simp add: mset_rel_def p2rel_def)
from multi_member_split[OF ‹x∈#m›] obtain m' where [simp]: "m=m'+{#x#}" by auto

from msed_rel_invL[OF R[simplified]] obtain n' y where
[simp]: "n=n'+{#y#}" and [param, simp]: "(x,y)∈A" and R': "(m',n')∈⟨A⟩mset_rel"
by (auto simp: rel2p_def mset_rel_def p2rel_def)

have "∀y'∈set_mset n. prio y ≤ prio y'"
proof
fix y' assume "y'∈set_mset n"
then obtain x' where [param]: "(x',y')∈A" and "x'∈set_mset m"
using R
by (metis msed_rel_invR mset_contains_eq rel2pD union_mset_add_mset_left union_single_eq_member)
with P' have "prio' x ≤ prio' x'" by blast
moreover have "(prio' x ≤ prio' x', prio y ≤ prio y') ∈ bool_rel"
by parametricity
ultimately show "prio y ≤ prio y'" by simp
qed
thus "∃y. (x, y) ∈ A ∧ y ∈# n ∧ (∀v'∈set_mset n. prio y ≤ prio v')"
using R' by (auto intro!: exI[where x=y])
qed

context fixes prio :: "'a ⇒ 'b::linorder" and A :: "('a×'a) set" begin
sepref_decl_op (no_def,no_mop) prio_pop_min:
"PR_CONST (mop_prio_pop_min prio)" :: "⟨A⟩mset_rel →⇩f ⟨A ×⇩r ⟨A⟩mset_rel⟩nres_rel"
where "IS_BELOW_ID A"
proof goal_cases
case 1
hence [param]: "(prio,prio)∈A → Id"
by (auto simp: IS_BELOW_ID_def)
show ?case
apply (rule fref_ncI)
apply parametricity
by auto
qed

sepref_decl_op (no_def,no_mop) prio_peek_min:
"PR_CONST (mop_prio_peek_min prio)" :: "⟨A⟩mset_rel →⇩f ⟨A⟩nres_rel"
where "IS_BELOW_ID A"
proof goal_cases
case 1
hence [param]: "(prio,prio)∈A → Id"
by (auto simp: IS_BELOW_ID_def)
show ?case
apply (rule fref_ncI)
apply parametricity
by auto
qed
end

subsection ‹Patterns›

lemma [def_pat_rules]:
"mop_prio_pop_min\$prio ≡ UNPROTECT (mop_prio_pop_min prio)"
"mop_prio_peek_min\$prio ≡ UNPROTECT (mop_prio_peek_min prio)"
by auto

end
```