Theory Intf_Map

theory Intf_Map
imports Refine_Monadic
header {*\isaheader{Map Interface}*}
theory Intf_Map
imports "../../../Refine_Monadic/Refine_Monadic"
begin

consts i_map :: "interface => interface => interface"

definition [simp]: "op_map_empty ≡ Map.empty"
definition op_map_lookup :: "'k => ('k\<rightharpoonup>'v) \<rightharpoonup> 'v"
  where [simp]: "op_map_lookup k m ≡ m k"
definition [simp]: "op_map_update k v m ≡ m(k\<mapsto>v)"
definition [simp]: "op_map_delete k m ≡ m |` (-{k})"
definition [simp]: "op_map_restrict P m ≡ m |` {k∈dom m. P (k, the (m k))}"
definition [simp]: "op_map_isEmpty x ≡ x=Map.empty"
definition [simp]: "op_map_isSng x ≡ ∃k v. x=[k\<mapsto>v]"
definition [simp]: "op_map_ball m P ≡ Ball (map_to_set m) P"
definition [simp]: "op_map_bex m P ≡ Bex (map_to_set m) P"
definition [simp]: "op_map_size m ≡ card (dom m)"
definition [simp]: "op_map_size_abort n m ≡ min n (card (dom m))"
definition [simp]: "op_map_sel m P ≡ SPEC (λ(k,v). m k = Some v ∧ P k v)"
definition [simp]: "op_map_pick m ≡ SPEC (λ(k,v). m k = Some v)"

definition [simp]: "op_map_pick_remove m ≡ 
  SPEC (λ((k,v),m'). m k = Some v ∧ m' = m |` (-{k}))"


context begin interpretation autoref_syn .

lemma [autoref_op_pat]:
  "Map.empty ≡ op_map_empty"
  "(m::'k\<rightharpoonup>'v) k ≡ op_map_lookup$k$m"
  "m(k\<mapsto>v) ≡ op_map_update$k$v$m"
  "m |` (-{k}) ≡ op_map_delete$k$m"
  "m |` {k∈dom m. P (k, the (m k))} ≡ op_map_restrict$P$m"

  "m=Map.empty ≡ op_map_isEmpty$m"
  "Map.empty=m ≡ op_map_isEmpty$m"
  "dom m = {} ≡ op_map_isEmpty$m"
  "{} = dom m ≡ op_map_isEmpty$m"

  "∃k v. m=[k\<mapsto>v] ≡ op_map_isSng$m"
  "∃k v. [k\<mapsto>v]=m ≡ op_map_isSng$m"
  "∃k. dom m={k} ≡ op_map_isSng$m"
  "∃k. {k} = dom m ≡ op_map_isSng$m"
  "1 = card (dom m) ≡ op_map_isSng$m"

  "!!P. Ball (map_to_set m) P ≡ op_map_ball$m$P"
  "!!P. Bex (map_to_set m) P ≡ op_map_bex$m$P"

  "card (dom m) ≡ op_map_size$m"

  "min n (card (dom m)) ≡ op_map_size_abort$n$m"
  "min (card (dom m)) n ≡ op_map_size_abort$n$m"

  "!!P. SPEC (λ(k,v). m k=Some v ∧ P k v) ≡ op_map_sel$m$P"
  "!!P. SPEC (λ(k,v). P k v ∧ m k=Some v) ≡ op_map_sel$m$P"

  "!!P. SPEC (λ(k,v). m k = Some v) ≡ op_map_pick$m"
  "!!P. SPEC (λ(k,v). (k,v) ∈ map_to_set m) ≡ op_map_pick$m"
  by (auto 
    intro!: eq_reflection ext
    simp: restrict_map_def dom_eq_singleton_conv card_Suc_eq map_to_set_def
    dest!: sym[of "Suc 0" "card (dom m)"] sym[of _ "dom m"]
  )

  lemma [autoref_op_pat]: 
    "SPEC (λ((k,v),m'). m k = Some v ∧ m' = m |` (-{k})) 
      ≡ op_map_pick_remove$m"
    by simp

  lemma op_map_pick_remove_alt: "
    do {((k,v),m) \<leftarrow> op_map_pick_remove m; f k v m}
      = (
    do {
      (k,v)\<leftarrow>SPEC (λ(k,v). m k = Some v); 
       let m=m |` (-{k});
       f k v m
    })"
    unfolding op_map_pick_remove_def
    apply (auto simp: pw_eq_iff refine_pw_simps)
    done

  lemma [autoref_op_pat]: 
    "do {
      (k,v)\<leftarrow>SPEC (λ(k,v). m k = Some v); 
       let m=m |` (-{k});
       f k v m
    } ≡ do {((k,v),m) \<leftarrow> op_map_pick_remove m; f k v m}"
    unfolding op_map_pick_remove_alt .


end

lemma [autoref_itype]:
  "op_map_empty ::i ⟨Ik,Iv⟩ii_map"
  "op_map_lookup ::i Ik ->i ⟨Ik,Iv⟩ii_map ->i ⟨Iv⟩ii_option"
  "op_map_update ::i Ik ->i Iv ->i ⟨Ik,Iv⟩ii_map ->i ⟨Ik,Iv⟩ii_map"
  "op_map_delete ::i Ik ->i ⟨Ik,Iv⟩ii_map ->i ⟨Ik,Iv⟩ii_map"
  "op_map_restrict 
    ::i (⟨Ik,Iv⟩ii_prod ->i i_bool) ->i ⟨Ik,Iv⟩ii_map ->i ⟨Ik,Iv⟩ii_map"
  "op_map_isEmpty ::i ⟨Ik,Iv⟩ii_map ->i i_bool"
  "op_map_isSng ::i ⟨Ik,Iv⟩ii_map ->i i_bool"
  "op_map_ball ::i ⟨Ik,Iv⟩ii_map ->i (⟨Ik,Iv⟩ii_prod ->i i_bool) ->i i_bool"
  "op_map_bex ::i ⟨Ik,Iv⟩ii_map ->i (⟨Ik,Iv⟩ii_prod ->i i_bool) ->i i_bool"
  "op_map_size ::i ⟨Ik,Iv⟩ii_map ->i i_nat"
  "op_map_size_abort ::i i_nat ->i ⟨Ik,Iv⟩ii_map ->i i_nat"
  "op ++ ::i ⟨Ik,Iv⟩ii_map ->i ⟨Ik,Iv⟩ii_map ->i ⟨Ik,Iv⟩ii_map"
  "map_of ::i ⟨⟨Ik,Iv⟩ii_prod⟩ii_list ->i ⟨Ik,Iv⟩ii_map"

  "op_map_sel ::i ⟨Ik,Iv⟩ii_map ->i (Ik ->i Iv ->i i_bool) 
    ->i ⟨⟨Ik,Iv⟩ii_prod⟩ii_nres"
  "op_map_pick ::i ⟨Ik,Iv⟩ii_map ->i ⟨⟨Ik,Iv⟩ii_prod⟩ii_nres"
  "op_map_pick_remove 
    ::i ⟨Ik,Iv⟩ii_map ->i ⟨⟨⟨Ik,Iv⟩ii_prod,⟨Ik,Iv⟩ii_map⟩ii_prod⟩ii_nres"
  by simp_all

lemma hom_map1[autoref_hom]:
  "CONSTRAINT Map.empty (⟨Rk,Rv⟩Rm)"
  "CONSTRAINT map_of (⟨⟨Rk,Rv⟩prod_rel⟩list_rel -> ⟨Rk,Rv⟩Rm)"
  "CONSTRAINT op ++ (⟨Rk,Rv⟩Rm -> ⟨Rk,Rv⟩Rm -> ⟨Rk,Rv⟩Rm)"
  by simp_all

term op_map_restrict
lemma hom_map2[autoref_hom]:
  "CONSTRAINT op_map_lookup (Rk->⟨Rk,Rv⟩Rm->⟨Rv⟩option_rel)"
  "CONSTRAINT op_map_update (Rk->Rv->⟨Rk,Rv⟩Rm->⟨Rk,Rv⟩Rm)"
  "CONSTRAINT op_map_delete (Rk->⟨Rk,Rv⟩Rm->⟨Rk,Rv⟩Rm)"
  "CONSTRAINT op_map_restrict ((⟨Rk,Rv⟩prod_rel -> Id) -> ⟨Rk,Rv⟩Rm -> ⟨Rk,Rv⟩Rm)"
  "CONSTRAINT op_map_isEmpty (⟨Rk,Rv⟩Rm->Id)"
  "CONSTRAINT op_map_isSng (⟨Rk,Rv⟩Rm->Id)"
  "CONSTRAINT op_map_ball (⟨Rk,Rv⟩Rm->(⟨Rk,Rv⟩prod_rel->Id)->Id)"
  "CONSTRAINT op_map_bex (⟨Rk,Rv⟩Rm->(⟨Rk,Rv⟩prod_rel->Id)->Id)"
  "CONSTRAINT op_map_size (⟨Rk,Rv⟩Rm->Id)"
  "CONSTRAINT op_map_size_abort (Id->⟨Rk,Rv⟩Rm->Id)"

  "CONSTRAINT op_map_sel (⟨Rk,Rv⟩Rm->(Rk -> Rv -> bool_rel)->⟨Rk×rRv⟩nres_rel)"
  "CONSTRAINT op_map_pick (⟨Rk,Rv⟩Rm -> ⟨Rk×rRv⟩nres_rel)"
  "CONSTRAINT op_map_pick_remove (⟨Rk,Rv⟩Rm -> ⟨(Rk×rRv)×r⟨Rk,Rv⟩Rm⟩nres_rel)"
  by simp_all


definition "finite_map_rel R ≡ Range R ⊆ Collect (finite o dom)"
lemma finite_map_rel_trigger: "finite_map_rel R ==> finite_map_rel R" .


declaration {* Tagged_Solver.add_triggers 
  "Relators.relator_props_solver" @{thms finite_map_rel_trigger} *}

end