Theory 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›


context
  fixes t ::  " nat"
begin
  definition "mop_map_empty  = SPECT [ Map.empty ↦ t]"


  lemma  mop_map_empty: "tt ≤ lst (SPECT [ Map.empty ↦ t  ]) Q 
        ⟹ tt ≤ lst (mop_map_empty ) Q" unfolding mop_map_empty_def by simp

  sepref_register "mop_map_empty" 
  print_theorems 
end


context
  fixes t ::  "('a ⇒ 'b option) ⇒ nat"
begin
  definition "mop_map_update m k v = SPECT [ m(k ↦ v) ↦ t m]"


  lemma  mop_map_update: "tt ≤ lst (SPECT [ m(k ↦ v) ↦ t m])  Q
        ⟹ tt ≤ lst (mop_map_update m k v) Q" unfolding mop_map_update_def by simp

  sepref_register "mop_map_update" 
  print_theorems 
end


context
  fixes t ::  "('a ⇒ 'b option) ⇒ nat"
begin
  definition "mop_map_dom_member m x = SPECT (emb (λb. b ⟷ x∈dom m) (t m))"


  lemma  mop_map_dom_member: "tt ≤ lst (SPECT (emb (λb. b ⟷ x∈dom m) (t m)))  Q
        ⟹ tt ≤ lst (mop_map_dom_member m x) Q" unfolding mop_map_dom_member_def by simp

  sepref_register "mop_map_dom_member" 
  print_theorems 
end

context
  fixes t ::  "('a ⇒ 'b option) ⇒ nat"
begin
definition "mop_map_lookup m x = do {
        ASSERT (x∈dom m);
        SPECT [  (the (m x)) ↦ t m]
      }"


lemma  mop_map_lookup: "tt ≤ lst (SPECT [  (the (m x)) ↦ t m]) Q
        ⟹ x : dom m 
        ⟹ tt ≤ lst (mop_map_lookup m x) Q" unfolding mop_map_lookup_def by simp

  lemma progress_mop_map_lookup[progress_rules]: "t m > 0 ⟹ progress (mop_map_lookup m x)"
      unfolding mop_map_lookup_def by (auto intro!: progress_rules simp add:   zero_enat_def) 
  sepref_register "mop_map_lookup" 
  print_theorems 
end


(*
  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 (simp add: pres_eq_iff_svb)
    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 (simp add: pres_eq_iff_svb)
    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"
  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 = RETURNT op_custom_empty"
    unfolding op_custom_empty_def by simp_all
end
*)


end