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, Vfmap_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,Vfmap_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,Vfmap_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,Vfmap_rel) TYPE(('k,'v) f_map)" by simp


subsection ‹Operations›
sepref_decl_op fmap_empty: "fmempty" :: "K,Vfmap_rel" .


sepref_decl_op fmap_is_empty: "(=) fmempty" :: "K,Vfmap_rel  bool_rel"
  apply (rule fref_ncI)
  apply parametricity
  apply (rule fun_relI; auto)
  done


lemma fmap_rel_fmupd_fmap_rel:
  (A, B)  K, Rfmap_rel  (p, p')  K  (q, q')  R 
   (fmupd p q A, fmupd p' q' B)  K, Rfmap_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,Vfmap_rel  K,Vfmap_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, Rfmap_rel
  if single: "single_valued K" "single_valued (K¯)" and
    H0: (A, B)  K, Rfmap_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, Rfmap_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,Vfmap_rel  K,Vfmap_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, Rfmap_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, Vfmap_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, Vfmap_rel 
         (fmlookup aa a, fmlookup a'a a')  Voption_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,Vfmap_rel  K   Voption_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,Vfmap_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  Idoption_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_relnres_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_relnres_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 Voption_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, Rfmap_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