# Theory PAC_Map_Rel

```(*
File:         PAC_Map_Rel.thy
Author:       Mathias Fleury, Daniela Kaufmann, JKU
Maintainer:   Mathias Fleury, JKU
*)
theory PAC_Map_Rel
imports
Refine_Imperative_HOL.IICF Finite_Map_Multiset
begin

section ‹Hash-Map for finite mappings›

text ‹

This function declares hash-maps for \<^typ>‹('a, 'b)fmap›, that are nicer
to use especially here where everything is finite.

›
definition fmap_rel where
[to_relAPP]:
"fmap_rel K V ≡ {(m1, m2).
(∀i j. i |∈| fmdom m2 ⟶ (j, i) ∈ K ⟶ (the (fmlookup m1 j), the (fmlookup m2 i)) ∈ V) ∧
fset (fmdom m1) ⊆ Domain K ∧ fset (fmdom m2) ⊆ Range K ∧
(∀i j. (i, j) ∈ K ⟶ j |∈| fmdom m2 ⟷ i |∈| fmdom m1)}"

lemma fmap_rel_alt_def:
‹⟨K, V⟩fmap_rel ≡
{(m1, m2).
(∀i j. i ∈# dom_m m2 ⟶
(j, i) ∈ K ⟶ (the (fmlookup m1 j), the (fmlookup m2 i)) ∈ V) ∧
fset (fmdom m1) ⊆ Domain K ∧
fset (fmdom m2) ⊆ Range K ∧
(∀i j. (i, j) ∈ K ⟶ (j ∈# dom_m m2) = (i ∈# dom_m m1))}
›
unfolding fmap_rel_def dom_m_def
by auto

lemma fmdom_empty_fmempty_iff[simp]: ‹fmdom m = {||} ⟷ m = fmempty›
by (metis fmdom_empty fmdrop_fset_fmdom fmdrop_fset_null)

lemma fmap_rel_empty1_simp[simp]:
"(fmempty,m)∈⟨K,V⟩fmap_rel ⟷ m=fmempty"
apply (cases ‹fmdom m = {||}›)
apply (auto simp: fmap_rel_def)[]
by (auto simp add: fmap_rel_def simp del: fmdom_empty_fmempty_iff)

lemma fmap_rel_empty2_simp[simp]:
"(m,fmempty)∈⟨K,V⟩fmap_rel ⟷ m=fmempty"
apply (cases ‹fmdom m = {||}›)
apply (auto simp: fmap_rel_def)[]
by (fastforce simp add: fmap_rel_def simp del: fmdom_empty_fmempty_iff)

sepref_decl_intf ('k,'v) f_map is "('k, 'v) fmap"

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

subsection ‹Operations›
sepref_decl_op fmap_empty: "fmempty" :: "⟨K,V⟩fmap_rel" .

sepref_decl_op fmap_is_empty: "(=) fmempty" :: "⟨K,V⟩fmap_rel → bool_rel"
apply (rule fref_ncI)
apply parametricity
apply (rule fun_relI; auto)
done

lemma fmap_rel_fmupd_fmap_rel:
‹(A, B) ∈ ⟨K, R⟩fmap_rel ⟹ (p, p') ∈ K ⟹ (q, q') ∈ R ⟹
(fmupd p q A, fmupd p' q' B) ∈ ⟨K, R⟩fmap_rel›
if "single_valued K" "single_valued (K¯)"
using that
unfolding fmap_rel_alt_def
apply (case_tac ‹p' ∈# dom_m B›)
apply (auto simp add: all_conj_distrib IS_RIGHT_UNIQUED dest!: multi_member_split)
done

sepref_decl_op fmap_update: "fmupd" :: "K → V → ⟨K,V⟩fmap_rel → ⟨K,V⟩fmap_rel"
where "single_valued K" "single_valued (K¯)"
apply (rule fref_ncI)
apply parametricity
apply (intro fun_relI)
by (rule fmap_rel_fmupd_fmap_rel)

lemma fmap_rel_fmdrop_fmap_rel:
‹(fmdrop p A, fmdrop p' B) ∈ ⟨K, R⟩fmap_rel›
if single: "single_valued K" "single_valued (K¯)" and
H0: ‹(A, B) ∈ ⟨K, R⟩fmap_rel› ‹(p, p') ∈ K›
proof -
have H: ‹⋀Aa j.
∀i. i ∈# dom_m B ⟶ (∀j. (j, i) ∈ K ⟶ (the (fmlookup A j), the (fmlookup B i)) ∈ R) ⟹
remove1_mset p' (dom_m B) = add_mset p' Aa ⟹ (j, p') ∈ K ⟹ False›
by (metis dom_m_fmdrop fmlookup_drop in_dom_m_lookup_iff union_single_eq_member)
have H2: ‹⋀i Aa j.
(p, p') ∈ K ⟹
∀i. i ∈# dom_m B ⟶ (∀j. (j, i) ∈ K ⟶ (the (fmlookup A j), the (fmlookup B i)) ∈ R) ⟹
∀i j. (i, j) ∈ K ⟶ (j ∈# dom_m B) = (i ∈# dom_m A) ⟹
remove1_mset p' (dom_m B) = add_mset i Aa ⟹
(j, i) ∈ K ⟹
(the (fmlookup A j), the (fmlookup B i)) ∈ R ∧ j ∈# remove1_mset p (dom_m A) ∧
i ∈# remove1_mset p' (dom_m B)›
‹⋀i j Aa.
(p, p') ∈ K ⟹
single_valued K ⟹
single_valued (K¯) ⟹
∀i. i ∈# dom_m B ⟶ (∀j. (j, i) ∈ K ⟶ (the (fmlookup A j), the (fmlookup B i)) ∈ R) ⟹
fset (fmdom A) ⊆ Domain K ⟹
fset (fmdom B) ⊆ Range K ⟹
∀i j. (i, j) ∈ K ⟶ (j ∈# dom_m B) = (i ∈# dom_m A) ⟹
(i, j) ∈ K ⟹ remove1_mset p (dom_m A) = add_mset i Aa ⟹ j ∈# remove1_mset p' (dom_m B)›
using single
by (metis IS_RIGHT_UNIQUED converse.intros dom_m_fmdrop fmlookup_drop in_dom_m_lookup_iff
union_single_eq_member)+
show ‹(fmdrop p A, fmdrop p' B) ∈ ⟨K, R⟩fmap_rel›
using that
unfolding fmap_rel_alt_def
by (auto simp add: all_conj_distrib IS_RIGHT_UNIQUED
dest!: multi_member_split dest: H H2)
qed

sepref_decl_op fmap_delete: "fmdrop" :: "K → ⟨K,V⟩fmap_rel → ⟨K,V⟩fmap_rel"
where "single_valued K" "single_valued (K¯)"
apply (rule fref_ncI)
apply parametricity

lemma fmap_rel_nat_the_fmlookup[intro]:
‹(A, B) ∈ ⟨S, R⟩fmap_rel ⟹ (p, p') ∈ S ⟹ p' ∈# dom_m B ⟹
(the (fmlookup A p), the (fmlookup B p')) ∈ R›
by (auto simp: fmap_rel_alt_def distinct_mset_dom)

lemma fmap_rel_in_dom_iff:
‹(aa, a'a) ∈ ⟨K, V⟩fmap_rel ⟹
(a, a') ∈ K ⟹
a' ∈# dom_m a'a ⟷
a ∈# dom_m aa›
unfolding fmap_rel_alt_def
by auto

lemma fmap_rel_fmlookup_rel:
‹(a, a') ∈ K ⟹ (aa, a'a) ∈ ⟨K, V⟩fmap_rel ⟹
(fmlookup aa a, fmlookup a'a a') ∈ ⟨V⟩option_rel›
using fmap_rel_nat_the_fmlookup[of aa a'a K V a a']
fmap_rel_in_dom_iff[of aa a'a K V a a']
in_dom_m_lookup_iff[of a' a'a]
in_dom_m_lookup_iff[of a aa]
by (cases ‹a' ∈# dom_m a'a›)
(auto simp del: fmap_rel_nat_the_fmlookup)

sepref_decl_op fmap_lookup: "fmlookup" :: "⟨K,V⟩fmap_rel → K →  ⟨V⟩option_rel"
apply (rule fref_ncI)
apply parametricity
apply (intro fun_relI)
apply (rule fmap_rel_fmlookup_rel; assumption)
done

lemma in_fdom_alt: "k∈#dom_m m ⟷ ¬is_None (fmlookup m k)"
by (auto split: option.split intro: fmdom_notI fmdomI simp: dom_m_def)

sepref_decl_op fmap_contains_key: "λk m. k∈#dom_m m" :: "K → ⟨K,V⟩fmap_rel → bool_rel"
unfolding in_fdom_alt
apply (rule fref_ncI)
apply parametricity
apply (rule fmap_rel_fmlookup_rel; assumption)
done

subsection ‹Patterns›

lemma pat_fmap_empty[pat_rules]: "fmempty ≡ op_fmap_empty" by simp

lemma pat_map_is_empty[pat_rules]:
"(=) \$m\$fmempty ≡ op_fmap_is_empty\$m"
"(=) \$fmempty\$m ≡ op_fmap_is_empty\$m"
"(=) \$(dom_m\$m)\${#} ≡ op_fmap_is_empty\$m"
"(=) \${#}\$(dom_m\$m) ≡ op_fmap_is_empty\$m"
unfolding atomize_eq
by (auto dest: sym)

lemma op_map_contains_key[pat_rules]:
"(∈#) \$ k \$ (dom_m\$m) ≡ op_fmap_contains_key\$'k\$'m"
by (auto intro!: eq_reflection)

subsection ‹Mapping to Normal Hashmaps›

abbreviation map_of_fmap :: ‹('k ⇒ 'v option) ⇒ ('k, 'v) fmap› where
‹map_of_fmap h ≡ Abs_fmap h›

definition map_fmap_rel where
‹map_fmap_rel = br map_of_fmap (λa. finite (dom a))›

lemma fmdrop_set_None:
‹(op_map_delete, fmdrop) ∈ Id → map_fmap_rel → map_fmap_rel›
apply (auto simp: map_fmap_rel_def br_def)
apply (subst fmdrop.abs_eq)
apply (auto simp: eq_onp_def fmap.Abs_fmap_inject
map_drop_def map_filter_finite
intro!: ext)
apply (auto simp: map_filter_def)
done

lemma map_upd_fmupd:
‹(op_map_update, fmupd) ∈ Id → Id → map_fmap_rel → map_fmap_rel›
apply (auto simp: map_fmap_rel_def br_def)
apply (subst fmupd.abs_eq)
apply (auto simp: eq_onp_def fmap.Abs_fmap_inject
map_drop_def map_filter_finite map_upd_def
intro!: ext)
done

text ‹Technically @{term op_map_lookup} has the arguments in the wrong direction.›
definition fmlookup' where
[simp]: ‹fmlookup' A k = fmlookup k A›

lemma [def_pat_rules]:
‹((∈#)\$k\$(dom_m\$A)) ≡ Not\$(is_None\$(fmlookup'\$k\$A))›

lemma op_map_lookup_fmlookup:
‹(op_map_lookup, fmlookup') ∈ Id → map_fmap_rel → ⟨Id⟩option_rel›
by (auto simp: map_fmap_rel_def br_def fmap.Abs_fmap_inverse)

abbreviation hm_fmap_assn where
‹hm_fmap_assn K V ≡ hr_comp (hm.assn K V) map_fmap_rel›

lemmas fmap_delete_hnr [sepref_fr_rules] =
hm.delete_hnr[FCOMP fmdrop_set_None]

lemmas fmap_update_hnr [sepref_fr_rules] =
hm.update_hnr[FCOMP map_upd_fmupd]

lemmas fmap_lookup_hnr [sepref_fr_rules] =
hm.lookup_hnr[FCOMP op_map_lookup_fmlookup]

lemma fmempty_empty:
‹(uncurry0 (RETURN op_map_empty), uncurry0 (RETURN fmempty)) ∈ unit_rel →⇩f ⟨map_fmap_rel⟩nres_rel›
by (auto simp: map_fmap_rel_def br_def fmempty_def frefI nres_relI)

lemmas [sepref_fr_rules] =
hm.empty_hnr[FCOMP fmempty_empty, unfolded op_fmap_empty_def[symmetric]]

abbreviation iam_fmap_assn where
‹iam_fmap_assn K V ≡ hr_comp (iam.assn K V) map_fmap_rel›

lemmas iam_fmap_delete_hnr [sepref_fr_rules] =
iam.delete_hnr[FCOMP fmdrop_set_None]

lemmas iam_ffmap_update_hnr [sepref_fr_rules] =
iam.update_hnr[FCOMP map_upd_fmupd]

lemmas iam_ffmap_lookup_hnr [sepref_fr_rules] =
iam.lookup_hnr[FCOMP op_map_lookup_fmlookup]

definition op_iam_fmap_empty where
‹op_iam_fmap_empty = fmempty›

lemma iam_fmempty_empty:
‹(uncurry0 (RETURN op_map_empty), uncurry0 (RETURN op_iam_fmap_empty)) ∈ unit_rel →⇩f ⟨map_fmap_rel⟩nres_rel›
by (auto simp: map_fmap_rel_def br_def fmempty_def frefI nres_relI op_iam_fmap_empty_def)

lemmas [sepref_fr_rules] =
iam.empty_hnr[FCOMP fmempty_empty, unfolded op_iam_fmap_empty_def[symmetric]]

definition upper_bound_on_dom where
‹upper_bound_on_dom A = SPEC(λn. ∀i ∈#(dom_m A). i < n)›

lemma [sepref_fr_rules]:
‹((Array.len), upper_bound_on_dom) ∈ (iam_fmap_assn nat_assn V)⇧k →⇩a nat_assn›
proof -
have [simp]: ‹finite (dom b) ⟹ i ∈ fset (fmdom (map_of_fmap b)) ⟷ i ∈ dom b› for i b
by (subst fmdom.abs_eq)
(auto simp: eq_onp_def fset.Abs_fset_inverse)
have 2: ‹nat_rel = the_pure (nat_assn)› and
3: ‹nat_assn = pure nat_rel›
by auto
have [simp]: ‹the_pure (λa c :: nat. ↑ (c = a)) = nat_rel›
apply (subst 2)
apply (subst 3)
apply (subst pure_def)
apply auto
done

have [simp]: ‹(iam_of_list l, b) ∈ the_pure (λa c :: nat. ↑ (c = a)) → ⟨the_pure V⟩option_rel ⟹
b i = Some y ⟹ i < length l›  for i b l y
by (auto dest!: fun_relD[of _ _ _ _ i i] simp: option_rel_def
iam_of_list_def split: if_splits)
show ?thesis
by sepref_to_hoare
(sep_auto simp: upper_bound_on_dom_def hr_comp_def iam.assn_def map_rel_def
map_fmap_rel_def is_iam_def br_def dom_m_def)
qed

lemma fmap_rel_nat_rel_dom_m[simp]:
‹(A, B) ∈ ⟨nat_rel, R⟩fmap_rel ⟹ dom_m A = dom_m B›
by (subst distinct_set_mset_eq_iff[symmetric])
(auto simp: fmap_rel_alt_def distinct_mset_dom
simp del: fmap_rel_nat_the_fmlookup)

lemma ref_two_step':
‹A ≤ B ⟹  ⇓ R A ≤ ⇓ R B›
using ref_two_step by auto

end
```