Theory 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(k↦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↦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⇀'v) k ≡ op_map_lookup$k$m"
  "m(k↦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↦v] ≡ op_map_isSng$m"
  "∃k v. [k↦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) ← 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,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"
  "(++) ::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 (++) (⟨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 ∘ 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