# Theory Refine_Imperative_HOL.IICF_Prio_Map

```section ‹Priority Maps›
theory IICF_Prio_Map
imports IICF_Map
begin
text ‹This interface inherits from maps, and adds some operations›

(* TODO: Hack! *)
lemma uncurry_fun_rel_conv:
"(uncurry f, uncurry g) ∈ A×⇩rB → R ⟷ (f,g)∈A→B→R"
by (auto simp: uncurry_def dest!: fun_relD intro: prod_relI)

lemma uncurry0_fun_rel_conv:
"(uncurry0 f, uncurry0 g) ∈ unit_rel → R ⟷ (f,g)∈R"
by (auto dest!: fun_relD)

lemma RETURN_rel_conv0: "(RETURN f, RETURN g)∈⟨A⟩nres_rel ⟷ (f,g)∈A"
by (auto simp: nres_rel_def)

lemma RETURN_rel_conv1: "(RETURN o f, RETURN o g)∈A → ⟨B⟩nres_rel ⟷ (f,g)∈A→B"
by (auto simp: nres_rel_def dest!: fun_relD)

lemma RETURN_rel_conv2: "(RETURN oo f, RETURN oo g)∈A → B → ⟨R⟩nres_rel ⟷ (f,g)∈A→B→R"
by (auto simp: nres_rel_def dest!: fun_relD)

lemma RETURN_rel_conv3: "(RETURN ooo f, RETURN ooo g)∈A→B→C → ⟨R⟩nres_rel ⟷ (f,g)∈A→B→C→R"
by (auto simp: nres_rel_def dest!: fun_relD)

lemmas fref2param_unfold =
uncurry_fun_rel_conv uncurry0_fun_rel_conv
RETURN_rel_conv0 RETURN_rel_conv1 RETURN_rel_conv2 RETURN_rel_conv3

(* TODO: Generate these lemmas in sepref_decl_op! *)
lemmas param_op_map_update[param] = op_map_update.fref[THEN fref_ncD, unfolded fref2param_unfold]
lemmas param_op_map_delete[param] = op_map_delete.fref[THEN fref_ncD, unfolded fref2param_unfold]
lemmas param_op_map_is_empty[param] = op_map_is_empty.fref[THEN fref_ncD, unfolded fref2param_unfold]

sepref_decl_op map_update_new: "op_map_update" :: "[λ((k,v),m). k∉dom m]⇩f (K×⇩rV)×⇩r⟨K,V⟩map_rel → ⟨K,V⟩map_rel"
where "single_valued K" "single_valued (K¯)" .

sepref_decl_op map_update_ex: "op_map_update" :: "[λ((k,v),m). k∈dom m]⇩f (K×⇩rV)×⇩r⟨K,V⟩map_rel → ⟨K,V⟩map_rel"
where "single_valued K" "single_valued (K¯)" .

sepref_decl_op map_delete_ex: "op_map_delete" :: "[λ(k,m). k∈dom m]⇩f K×⇩r⟨K,V⟩map_rel → ⟨K,V⟩map_rel"
where "single_valued K" "single_valued (K¯)" .

context
fixes prio :: "'v ⇒ 'p::linorder"
begin
sepref_decl_op pm_decrease_key: "op_map_update"
:: "[λ((k,v),m). k∈dom m ∧ prio v ≤ prio (the (m k))]⇩f (K×⇩rV)×⇩r⟨K,V⟩map_rel → ⟨K,(V::('v×'v) set)⟩map_rel"
where "single_valued K" "single_valued (K¯)" "IS_BELOW_ID V"
proof goal_cases
case 1
have [param]: "((≤),(≤))∈Id→Id→bool_rel" by simp
from 1 show ?case
apply (auto simp: IS_BELOW_ID_def map_rel_def dest!: fun_relD)
done
qed

sepref_decl_op pm_increase_key: "op_map_update"
:: "[λ((k,v),m). k∈dom m ∧ prio v ≥ prio (the (m k))]⇩f (K×⇩rV)×⇩r⟨K,V⟩map_rel → ⟨K,(V::('v×'v) set)⟩map_rel"
where "single_valued K" "single_valued (K¯)" "IS_BELOW_ID V"
proof goal_cases
case 1
have [param]: "((≤),(≤))∈Id→Id→bool_rel" by simp
from 1 show ?case
apply (auto simp: IS_BELOW_ID_def map_rel_def dest!: fun_relD)
done
qed

lemma IS_BELOW_ID_D: "(a,b)∈R ⟹ IS_BELOW_ID R ⟹ a=b" by (auto simp: IS_BELOW_ID_def)

sepref_decl_op pm_peek_min: "λm. SPEC (λ(k,v).
m k = Some v ∧ (∀k' v'. m k' = Some v' ⟶ prio v ≤ prio v'))"
:: "[Not o op_map_is_empty]⇩f ⟨K,V⟩map_rel → K×⇩r(V::('v×'v) set)"
where "IS_BELOW_ID V"
apply (rule frefI)
apply (intro nres_relI)
apply (clarsimp simp: pw_le_iff refine_pw_simps)
apply (rule map_rel_obtain2, assumption, assumption)
apply1 (intro exI conjI allI impI; assumption?)
proof -
fix x y k' v' b w
assume "(x, y) ∈ ⟨K, V⟩map_rel" "y k' = Some v'"
then obtain k v where "(k,k')∈K" "(v,v')∈V" "x k = Some v"
by (rule map_rel_obtain1)

assume "IS_BELOW_ID V" "(b, w) ∈ V"
with ‹(v,v')∈V› have [simp]: "b=w" "v=v'" by (auto simp: IS_BELOW_ID_def)

assume "∀k' v'. x k' = Some v' ⟶ prio b ≤ prio v'"
with ‹x k = Some v› show "prio w ≤ prio v'"
by auto
qed

sepref_decl_op pm_pop_min: "λm. SPEC (λ((k,v),m').
m k = Some v
∧ m' = op_map_delete k m
∧ (∀k' v'. m k' = Some v' ⟶ prio v ≤ prio v')
)" :: "[Not o op_map_is_empty]⇩f ⟨K,V⟩map_rel → (K×⇩r(V::('v×'v) set))×⇩r⟨K,V⟩map_rel"
where "single_valued K" "single_valued (K¯)" "IS_BELOW_ID V"
apply (rule frefI)
apply (intro nres_relI)
apply (clarsimp simp: pw_le_iff refine_pw_simps simp del: op_map_delete_def)
apply (rule map_rel_obtain2, assumption, assumption)
apply (intro exI conjI allI impI; assumption?)
applyS parametricity
proof -
fix x y k' v' b w
assume "(x, y) ∈ ⟨K, V⟩map_rel" "y k' = Some v'"
then obtain k v where "(k,k')∈K" "(v,v')∈V" "x k = Some v"
by (rule map_rel_obtain1)

assume "IS_BELOW_ID V" "(b, w) ∈ V"
with ‹(v,v')∈V› have [simp]: "b=w" "v=v'" by (auto simp: IS_BELOW_ID_def)

assume "∀k' v'. x k' = Some v' ⟶ prio b ≤ prio v'"
with ‹x k = Some v› show "prio w ≤ prio v'"
by auto
qed
end

end
```