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 remove1_mset_eq_add_mset_iff:
   ‹remove1_mset a A = add_mset a A' ⟷ A = add_mset a (add_mset a A')›
  by (metis add_mset_add_single add_mset_diff_bothsides diff_zero remove1_mset_eqE)

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
  by (auto simp add: fmap_rel_fmdrop_fmap_rel)

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))›
  by (simp add: fold_is_None in_fdom_alt)

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