Theory Refine_Imperative_HOL.IICF_Map

```section ‹Map Interface›
theory IICF_Map
imports "../../Sepref"
begin

subsection ‹Parametricity for Maps›
definition [to_relAPP]: "map_rel K V ≡ (K → ⟨V⟩option_rel)
∩ { (mi,m). dom mi ⊆ Domain K ∧ dom m ⊆ Range K }"
(*
definition [to_relAPP]: "map_rel K V ≡ (K → ⟨V⟩option_rel)
∩ { (mi,m). dom mi ⊆ Domain K ∧ dom m ⊆ Range K
∧ ran mi ⊆ Domain V ∧ ran m ⊆ Range V }"
*)

lemma bi_total_map_rel_eq:
"⟦IS_RIGHT_TOTAL K; IS_LEFT_TOTAL K⟧ ⟹ ⟨K,V⟩map_rel = K → ⟨V⟩option_rel"
unfolding map_rel_def IS_RIGHT_TOTAL_def IS_LEFT_TOTAL_def
by (auto dest: fun_relD)

lemma map_rel_Id[simp]: "⟨Id,Id⟩map_rel = Id"
unfolding map_rel_def by auto

lemma map_rel_empty1_simp[simp]:
"(Map.empty,m)∈⟨K,V⟩map_rel ⟷ m=Map.empty"
apply (auto simp: map_rel_def)
by (meson RangeE domIff option_rel_simp(1) subsetCE tagged_fun_relD_none)

lemma map_rel_empty2_simp[simp]:
"(m,Map.empty)∈⟨K,V⟩map_rel ⟷ m=Map.empty"
apply (auto simp: map_rel_def)
by (meson Domain.cases domIff fun_relD2 option_rel_simp(2) subset_eq)

lemma map_rel_obtain1:
assumes 1: "(m,n)∈⟨K,V⟩map_rel"
assumes 2: "n l = Some w"
obtains k v where "m k = Some v" "(k,l)∈K" "(v,w)∈V"
using 1 unfolding map_rel_def
proof clarsimp
assume R: "(m, n) ∈ K → ⟨V⟩option_rel"
assume "dom n ⊆ Range K"
with 2 obtain k where "(k,l)∈K" by auto
moreover from fun_relD[OF R this] have "(m k, n l) ∈ ⟨V⟩option_rel" .
with 2 obtain v where "m k = Some v" "(v,w)∈V" by (cases "m k"; auto)
ultimately show thesis by - (rule that)
qed

lemma map_rel_obtain2:
assumes 1: "(m,n)∈⟨K,V⟩map_rel"
assumes 2: "m k = Some v"
obtains l w where "n l = Some w" "(k,l)∈K" "(v,w)∈V"
using 1 unfolding map_rel_def
proof clarsimp
assume R: "(m, n) ∈ K → ⟨V⟩option_rel"
assume "dom m ⊆ Domain K"
with 2 obtain l where "(k,l)∈K" by auto
moreover from fun_relD[OF R this] have "(m k, n l) ∈ ⟨V⟩option_rel" .
with 2 obtain w where "n l = Some w" "(v,w)∈V" by (cases "n l"; auto)
ultimately show thesis by - (rule that)
qed

lemma param_dom[param]: "(dom,dom)∈⟨K,V⟩map_rel → ⟨K⟩set_rel"
apply (clarsimp simp: set_rel_def; safe)
apply (erule (1) map_rel_obtain2; auto)
apply (erule (1) map_rel_obtain1; auto)
done

subsection ‹Interface Type›

sepref_decl_intf ('k,'v) i_map is "'k ⇀ 'v"

lemma [synth_rules]: "⟦INTF_OF_REL K TYPE('k); INTF_OF_REL V TYPE('v)⟧
⟹ INTF_OF_REL (⟨K,V⟩map_rel) TYPE(('k,'v) i_map)" by simp

subsection ‹Operations›
sepref_decl_op map_empty: "Map.empty" :: "⟨K,V⟩map_rel" .

sepref_decl_op map_is_empty: "(=) Map.empty" :: "⟨K,V⟩map_rel → bool_rel"
apply (rule fref_ncI)
apply parametricity
apply (rule fun_relI; auto)
done

sepref_decl_op map_update: "λk v m. m(k↦v)" :: "K → V → ⟨K,V⟩map_rel → ⟨K,V⟩map_rel"
where "single_valued K" "single_valued (K¯)"
apply (rule fref_ncI)
apply parametricity
unfolding map_rel_def
apply (intro fun_relI)
apply (elim IntE; rule IntI)
apply (intro fun_relI)
apply parametricity
apply auto
done

sepref_decl_op map_delete: "λk m. fun_upd m k None" :: "K → ⟨K,V⟩map_rel → ⟨K,V⟩map_rel"
where "single_valued K" "single_valued (K¯)"
apply (rule fref_ncI)
apply parametricity
unfolding map_rel_def
apply (intro fun_relI)
apply (elim IntE; rule IntI)
apply (intro fun_relI)
apply parametricity
apply auto
done

sepref_decl_op map_lookup: "λk (m::'k⇀'v). m k" :: "K → ⟨K,V⟩map_rel → ⟨V⟩option_rel"
apply (rule fref_ncI)
apply parametricity
unfolding map_rel_def
apply (intro fun_relI)
apply (elim IntE)
apply parametricity
done

lemma in_dom_alt: "k∈dom m ⟷ ¬is_None (m k)" by (auto split: option.split)

sepref_decl_op map_contains_key: "λk m. k∈dom m" :: "K → ⟨K,V⟩map_rel → bool_rel"
unfolding in_dom_alt
apply (rule fref_ncI)
apply parametricity
unfolding map_rel_def
apply (elim IntE)
apply parametricity
done

subsection ‹Patterns›

lemma pat_map_empty[pat_rules]: "λ⇩2_. None ≡ op_map_empty" by simp

lemma pat_map_is_empty[pat_rules]:
"(=) \$m\$(λ⇩2_. None) ≡ op_map_is_empty\$m"
"(=) \$(λ⇩2_. None)\$m ≡ op_map_is_empty\$m"
"(=) \$(dom\$m)\${} ≡ op_map_is_empty\$m"
"(=) \${}\$(dom\$m) ≡ op_map_is_empty\$m"
unfolding atomize_eq
by (auto dest: sym)

lemma pat_map_update[pat_rules]:
"fun_upd\$m\$k\$(Some\$v) ≡ op_map_update\$'k\$'v\$'m"
by simp
lemma pat_map_lookup[pat_rules]: "m\$k ≡ op_map_lookup\$'k\$'m"
by simp

lemma op_map_delete_pat[pat_rules]:
"(|`) \$ m \$ (uminus \$ (insert \$ k \$ {})) ≡ op_map_delete\$'k\$'m"
"fun_upd\$m\$k\$None ≡ op_map_delete\$'k\$'m"

lemma op_map_contains_key[pat_rules]:
"(∈) \$ k \$ (dom\$m) ≡ op_map_contains_key\$'k\$'m"
"Not\$((=) \$(m\$k)\$None) ≡ op_map_contains_key\$'k\$'m"
by (auto intro!: eq_reflection)

subsection ‹Parametricity›

locale map_custom_empty =
fixes op_custom_empty :: "'k⇀'v"
assumes op_custom_empty_def: "op_custom_empty = op_map_empty"
begin
sepref_register op_custom_empty :: "('kx,'vx) i_map"

lemma fold_custom_empty:
"Map.empty = op_custom_empty"
"op_map_empty = op_custom_empty"
"mop_map_empty = RETURN op_custom_empty"
unfolding op_custom_empty_def by simp_all
end

end
```