Theory Collections.Intf_Map

section ‹\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'v)  'v"
  where [simp]: "op_map_lookup k m  m k"
definition [simp]: "op_map_update k v m  m(kv)"
definition [simp]: "op_map_delete k m  m |` (-{k})"
definition [simp]: "op_map_restrict P m  m |` {kdom m. P (k, the (m k))}"
definition [simp]: "op_map_isEmpty x  x=Map.empty"
definition [simp]: "op_map_isSng x  k v. x=[kv]"
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'v) k  op_map_lookup$k$m"
  "m(kv)  op_map_update$k$v$m"
  "m |` (-{k})  op_map_delete$k$m"
  "m |` {kdom 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=[kv]  op_map_isSng$m"
  "k v. [kv]=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)  op_map_pick_remove m; f k v m}
      = (
    do {
      (k,v)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)SPEC (λ(k,v). m k = Some v); 
       let m=m |` (-{k});
       f k v m
    }  do {((k,v),m)  op_map_pick_remove m; f k v m}"
    unfolding op_map_pick_remove_alt .


end

lemma [autoref_itype]:
  "op_map_empty ::i Ik,Ivii_map"
  "op_map_lookup ::i Ik i Ik,Ivii_map i Ivii_option"
  "op_map_update ::i Ik i Iv i Ik,Ivii_map i Ik,Ivii_map"
  "op_map_delete ::i Ik i Ik,Ivii_map i Ik,Ivii_map"
  "op_map_restrict 
    ::i (Ik,Ivii_prod i i_bool) i Ik,Ivii_map i Ik,Ivii_map"
  "op_map_isEmpty ::i Ik,Ivii_map i i_bool"
  "op_map_isSng ::i Ik,Ivii_map i i_bool"
  "op_map_ball ::i Ik,Ivii_map i (Ik,Ivii_prod i i_bool) i i_bool"
  "op_map_bex ::i Ik,Ivii_map i (Ik,Ivii_prod i i_bool) i i_bool"
  "op_map_size ::i Ik,Ivii_map i i_nat"
  "op_map_size_abort ::i i_nat i Ik,Ivii_map i i_nat"
  "(++) ::i Ik,Ivii_map i Ik,Ivii_map i Ik,Ivii_map"
  "map_of ::i Ik,Ivii_prodii_list i Ik,Ivii_map"

  "op_map_sel ::i Ik,Ivii_map i (Ik i Iv i i_bool) 
    i Ik,Ivii_prodii_nres"
  "op_map_pick ::i Ik,Ivii_map i Ik,Ivii_prodii_nres"
  "op_map_pick_remove 
    ::i Ik,Ivii_map i Ik,Ivii_prod,Ik,Ivii_mapii_prodii_nres"
  by simp_all

lemma hom_map1[autoref_hom]:
  "CONSTRAINT Map.empty (Rk,RvRm)"
  "CONSTRAINT map_of (Rk,Rvprod_rellist_rel  Rk,RvRm)"
  "CONSTRAINT (++) (Rk,RvRm  Rk,RvRm  Rk,RvRm)"
  by simp_all

term op_map_restrict
lemma hom_map2[autoref_hom]:
  "CONSTRAINT op_map_lookup (RkRk,RvRmRvoption_rel)"
  "CONSTRAINT op_map_update (RkRvRk,RvRmRk,RvRm)"
  "CONSTRAINT op_map_delete (RkRk,RvRmRk,RvRm)"
  "CONSTRAINT op_map_restrict ((Rk,Rvprod_rel  Id)  Rk,RvRm  Rk,RvRm)"
  "CONSTRAINT op_map_isEmpty (Rk,RvRmId)"
  "CONSTRAINT op_map_isSng (Rk,RvRmId)"
  "CONSTRAINT op_map_ball (Rk,RvRm(Rk,Rvprod_relId)Id)"
  "CONSTRAINT op_map_bex (Rk,RvRm(Rk,Rvprod_relId)Id)"
  "CONSTRAINT op_map_size (Rk,RvRmId)"
  "CONSTRAINT op_map_size_abort (IdRk,RvRmId)"

  "CONSTRAINT op_map_sel (Rk,RvRm(Rk  Rv  bool_rel)Rk×rRvnres_rel)"
  "CONSTRAINT op_map_pick (Rk,RvRm  Rk×rRvnres_rel)"
  "CONSTRAINT op_map_pick_remove (Rk,RvRm  (Rk×rRv)×rRk,RvRmnres_rel)"
  by simp_all


definition "finite_map_rel R  Range R  Collect (finite  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