# Theory Intf_Map

```section ‹\isaheader{Map Interface}›
theory Intf_Map
begin

consts i_map :: "interface ⇒ interface ⇒ interface"

definition [simp]: "op_map_empty ≡ Map.empty"
definition op_map_lookup :: "'k ⇒ ('k⇀'v) ⇀ 'v"
where [simp]: "op_map_lookup k m ≡ m k"
definition [simp]: "op_map_update k v m ≡ m(k↦v)"
definition [simp]: "op_map_delete k m ≡ m |` (-{k})"
definition [simp]: "op_map_restrict P m ≡ m |` {k∈dom m. P (k, the (m k))}"
definition [simp]: "op_map_isEmpty x ≡ x=Map.empty"
definition [simp]: "op_map_isSng x ≡ ∃k v. x=[k↦v]"
definition [simp]: "op_map_ball m P ≡ Ball (map_to_set m) P"
definition [simp]: "op_map_bex m P ≡ Bex (map_to_set m) P"
definition [simp]: "op_map_size m ≡ card (dom m)"
definition [simp]: "op_map_size_abort n m ≡ min n (card (dom m))"
definition [simp]: "op_map_sel m P ≡ SPEC (λ(k,v). m k = Some v ∧ P k v)"
definition [simp]: "op_map_pick m ≡ SPEC (λ(k,v). m k = Some v)"

definition [simp]: "op_map_pick_remove m ≡
SPEC (λ((k,v),m'). m k = Some v ∧ m' = m |` (-{k}))"

context begin interpretation autoref_syn .

lemma [autoref_op_pat]:
"Map.empty ≡ op_map_empty"
"(m::'k⇀'v) k ≡ op_map_lookup\$k\$m"
"m(k↦v) ≡ op_map_update\$k\$v\$m"
"m |` (-{k}) ≡ op_map_delete\$k\$m"
"m |` {k∈dom m. P (k, the (m k))} ≡ op_map_restrict\$P\$m"

"m=Map.empty ≡ op_map_isEmpty\$m"
"Map.empty=m ≡ op_map_isEmpty\$m"
"dom m = {} ≡ op_map_isEmpty\$m"
"{} = dom m ≡ op_map_isEmpty\$m"

"∃k v. m=[k↦v] ≡ op_map_isSng\$m"
"∃k v. [k↦v]=m ≡ op_map_isSng\$m"
"∃k. dom m={k} ≡ op_map_isSng\$m"
"∃k. {k} = dom m ≡ op_map_isSng\$m"
"1 = card (dom m) ≡ op_map_isSng\$m"

"⋀P. Ball (map_to_set m) P ≡ op_map_ball\$m\$P"
"⋀P. Bex (map_to_set m) P ≡ op_map_bex\$m\$P"

"card (dom m) ≡ op_map_size\$m"

"min n (card (dom m)) ≡ op_map_size_abort\$n\$m"
"min (card (dom m)) n ≡ op_map_size_abort\$n\$m"

"⋀P. SPEC (λ(k,v). m k=Some v ∧ P k v) ≡ op_map_sel\$m\$P"
"⋀P. SPEC (λ(k,v). P k v ∧ m k=Some v) ≡ op_map_sel\$m\$P"

"⋀P. SPEC (λ(k,v). m k = Some v) ≡ op_map_pick\$m"
"⋀P. SPEC (λ(k,v). (k,v) ∈ map_to_set m) ≡ op_map_pick\$m"
by (auto
intro!: eq_reflection ext
simp: restrict_map_def dom_eq_singleton_conv card_Suc_eq map_to_set_def
dest!: sym[of "Suc 0" "card (dom m)"] sym[of _ "dom m"]
)

lemma [autoref_op_pat]:
"SPEC (λ((k,v),m'). m k = Some v ∧ m' = m |` (-{k}))
≡ op_map_pick_remove\$m"
by simp

lemma op_map_pick_remove_alt: "
do {((k,v),m) ← op_map_pick_remove m; f k v m}
= (
do {
(k,v)←SPEC (λ(k,v). m k = Some v);
let m=m |` (-{k});
f k v m
})"
unfolding op_map_pick_remove_def
apply (auto simp: pw_eq_iff refine_pw_simps)
done

lemma [autoref_op_pat]:
"do {
(k,v)←SPEC (λ(k,v). m k = Some v);
let m=m |` (-{k});
f k v m
} ≡ do {((k,v),m) ← op_map_pick_remove m; f k v m}"
unfolding op_map_pick_remove_alt .

end

lemma [autoref_itype]:
"op_map_empty ::⇩i ⟨Ik,Iv⟩⇩ii_map"
"op_map_lookup ::⇩i Ik →⇩i ⟨Ik,Iv⟩⇩ii_map →⇩i ⟨Iv⟩⇩ii_option"
"op_map_update ::⇩i Ik →⇩i Iv →⇩i ⟨Ik,Iv⟩⇩ii_map →⇩i ⟨Ik,Iv⟩⇩ii_map"
"op_map_delete ::⇩i Ik →⇩i ⟨Ik,Iv⟩⇩ii_map →⇩i ⟨Ik,Iv⟩⇩ii_map"
"op_map_restrict
::⇩i (⟨Ik,Iv⟩⇩ii_prod →⇩i i_bool) →⇩i ⟨Ik,Iv⟩⇩ii_map →⇩i ⟨Ik,Iv⟩⇩ii_map"
"op_map_isEmpty ::⇩i ⟨Ik,Iv⟩⇩ii_map →⇩i i_bool"
"op_map_isSng ::⇩i ⟨Ik,Iv⟩⇩ii_map →⇩i i_bool"
"op_map_ball ::⇩i ⟨Ik,Iv⟩⇩ii_map →⇩i (⟨Ik,Iv⟩⇩ii_prod →⇩i i_bool) →⇩i i_bool"
"op_map_bex ::⇩i ⟨Ik,Iv⟩⇩ii_map →⇩i (⟨Ik,Iv⟩⇩ii_prod →⇩i i_bool) →⇩i i_bool"
"op_map_size ::⇩i ⟨Ik,Iv⟩⇩ii_map →⇩i i_nat"
"op_map_size_abort ::⇩i i_nat →⇩i ⟨Ik,Iv⟩⇩ii_map →⇩i i_nat"
"(++) ::⇩i ⟨Ik,Iv⟩⇩ii_map →⇩i ⟨Ik,Iv⟩⇩ii_map →⇩i ⟨Ik,Iv⟩⇩ii_map"
"map_of ::⇩i ⟨⟨Ik,Iv⟩⇩ii_prod⟩⇩ii_list →⇩i ⟨Ik,Iv⟩⇩ii_map"

"op_map_sel ::⇩i ⟨Ik,Iv⟩⇩ii_map →⇩i (Ik →⇩i Iv →⇩i i_bool)
→⇩i ⟨⟨Ik,Iv⟩⇩ii_prod⟩⇩ii_nres"
"op_map_pick ::⇩i ⟨Ik,Iv⟩⇩ii_map →⇩i ⟨⟨Ik,Iv⟩⇩ii_prod⟩⇩ii_nres"
"op_map_pick_remove
::⇩i ⟨Ik,Iv⟩⇩ii_map →⇩i ⟨⟨⟨Ik,Iv⟩⇩ii_prod,⟨Ik,Iv⟩⇩ii_map⟩⇩ii_prod⟩⇩ii_nres"
by simp_all

lemma hom_map1[autoref_hom]:
"CONSTRAINT Map.empty (⟨Rk,Rv⟩Rm)"
"CONSTRAINT map_of (⟨⟨Rk,Rv⟩prod_rel⟩list_rel → ⟨Rk,Rv⟩Rm)"
"CONSTRAINT (++) (⟨Rk,Rv⟩Rm → ⟨Rk,Rv⟩Rm → ⟨Rk,Rv⟩Rm)"
by simp_all

term op_map_restrict
lemma hom_map2[autoref_hom]:
"CONSTRAINT op_map_lookup (Rk→⟨Rk,Rv⟩Rm→⟨Rv⟩option_rel)"
"CONSTRAINT op_map_update (Rk→Rv→⟨Rk,Rv⟩Rm→⟨Rk,Rv⟩Rm)"
"CONSTRAINT op_map_delete (Rk→⟨Rk,Rv⟩Rm→⟨Rk,Rv⟩Rm)"
"CONSTRAINT op_map_restrict ((⟨Rk,Rv⟩prod_rel → Id) → ⟨Rk,Rv⟩Rm → ⟨Rk,Rv⟩Rm)"
"CONSTRAINT op_map_isEmpty (⟨Rk,Rv⟩Rm→Id)"
"CONSTRAINT op_map_isSng (⟨Rk,Rv⟩Rm→Id)"
"CONSTRAINT op_map_ball (⟨Rk,Rv⟩Rm→(⟨Rk,Rv⟩prod_rel→Id)→Id)"
"CONSTRAINT op_map_bex (⟨Rk,Rv⟩Rm→(⟨Rk,Rv⟩prod_rel→Id)→Id)"
"CONSTRAINT op_map_size (⟨Rk,Rv⟩Rm→Id)"
"CONSTRAINT op_map_size_abort (Id→⟨Rk,Rv⟩Rm→Id)"

"CONSTRAINT op_map_sel (⟨Rk,Rv⟩Rm→(Rk → Rv → bool_rel)→⟨Rk×⇩rRv⟩nres_rel)"
"CONSTRAINT op_map_pick (⟨Rk,Rv⟩Rm → ⟨Rk×⇩rRv⟩nres_rel)"
"CONSTRAINT op_map_pick_remove (⟨Rk,Rv⟩Rm → ⟨(Rk×⇩rRv)×⇩r⟨Rk,Rv⟩Rm⟩nres_rel)"
by simp_all

definition "finite_map_rel R ≡ Range R ⊆ Collect (finite ∘ dom)"
lemma finite_map_rel_trigger: "finite_map_rel R ⟹ finite_map_rel R" .

"Relators.relator_props_solver" @{thms finite_map_rel_trigger}›

end
```