Theory IICF_Map

section ‹Map Interface›
theory IICF_Map
imports "../../Sepref"
begin
  
subsection ‹Parametricity for Maps›
definition [to_relAPP]: "map_rel K V  (K  Voption_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,Vmap_rel = K  Voption_rel"
  unfolding map_rel_def IS_RIGHT_TOTAL_def IS_LEFT_TOTAL_def
  by (auto dest: fun_relD)
  
lemma map_rel_Id[simp]: "Id,Idmap_rel = Id" 
  unfolding map_rel_def by auto

lemma map_rel_empty1_simp[simp]: 
  "(Map.empty,m)K,Vmap_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,Vmap_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,Vmap_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  Voption_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)  Voption_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,Vmap_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  Voption_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)  Voption_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,Vmap_rel  Kset_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,Vmap_rel) TYPE(('k,'v) i_map)" by simp

subsection ‹Operations›
  sepref_decl_op map_empty: "Map.empty" :: "K,Vmap_rel" .
  
  sepref_decl_op map_is_empty: "(=) Map.empty" :: "K,Vmap_rel  bool_rel"
    apply (rule fref_ncI)
    apply parametricity
    apply (rule fun_relI; auto)
    done

  sepref_decl_op map_update: "λk v m. m(kv)" :: "K  V  K,Vmap_rel  K,Vmap_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 (simp add: pres_eq_iff_svb)
    apply auto
    done
    
  sepref_decl_op map_delete: "λk m. fun_upd m k None" :: "K  K,Vmap_rel  K,Vmap_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 (simp add: pres_eq_iff_svb)
    apply auto
    done

  sepref_decl_op map_lookup: "λk (m::'k'v). m k" :: "K  K,Vmap_rel  Voption_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: "kdom m  ¬is_None (m k)" by (auto split: option.split)

  sepref_decl_op map_contains_key: "λk m. kdom m" :: "K  K,Vmap_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"
  by (simp_all add: map_upd_eq_restrict)

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