Theory Separation_Logic_Imperative_HOL.Imp_Map_Spec

section ‹Interface for Maps›
theory Imp_Map_Spec
imports "../Sep_Main"
begin
text ‹
  This file specifies an abstract interface for map data structures. It can
  be implemented by concrete map data structures, as demonstrated in the 
  hash map example.
›

locale imp_map = 
  fixes is_map :: "('k ⇀ 'v) ⇒ 'm ⇒ assn"
  assumes precise: "precise is_map"

locale imp_map_empty = imp_map +
  constrains is_map :: "('k ⇀ 'v) ⇒ 'm ⇒ assn"
  fixes empty :: "'m Heap"
  assumes empty_rule[sep_heap_rules]: "<emp> empty <is_map Map.empty>⇩t"

locale imp_map_is_empty = imp_map +
  constrains is_map :: "('k ⇀ 'v) ⇒ 'm ⇒ assn"
  fixes is_empty :: "'m ⇒ bool Heap"
  assumes is_empty_rule[sep_heap_rules]: 
    "<is_map m p> is_empty p <λr. is_map m p * ↑(r ⟷ m=Map.empty)>⇩t"

locale imp_map_lookup = imp_map +
  constrains is_map :: "('k ⇀ 'v) ⇒ 'm ⇒ assn"
  fixes lookup :: "'k ⇒ 'm ⇒ ('v option) Heap"
  assumes lookup_rule[sep_heap_rules]: 
    "<is_map m p> lookup k p <λr. is_map m p * ↑(r = m k)>⇩t"

locale imp_map_update = imp_map +
  constrains is_map :: "('k ⇀ 'v) ⇒ 'm ⇒ assn"
  fixes update :: "'k ⇒ 'v ⇒ 'm ⇒ 'm Heap"
  assumes update_rule[sep_heap_rules]: 
    "<is_map m p> update k v p <is_map (m(k ↦ v))>⇩t"
    
locale imp_map_delete = imp_map +
  constrains is_map :: "('k ⇀ 'v) ⇒ 'm ⇒ assn"
  fixes delete :: "'k ⇒ 'm ⇒ 'm Heap"
  assumes delete_rule[sep_heap_rules]: 
    "<is_map m p> delete k p <is_map (m |` (-{k}))>⇩t"

locale imp_map_add = imp_map +
  constrains is_map :: "('k ⇀ 'v) ⇒ 'm ⇒ assn"
  fixes add :: "'m ⇒ 'm ⇒ 'm Heap"
  assumes add_rule[sep_heap_rules]: 
    "<is_map m p * is_map m' p'> add p p' 
     <λr. is_map m p * is_map m' p' * is_map (m ++ m') r>⇩t"


locale imp_map_size = imp_map +
  constrains is_map :: "('k ⇀ 'v) ⇒ 'm ⇒ assn"
  fixes size :: "'m ⇒ nat Heap"
  assumes size_rule[sep_heap_rules]: 
    "<is_map m p> size p <λr. is_map m p * ↑(r = card (dom m))>⇩t"

locale imp_map_iterate = imp_map +
  constrains is_map :: "('k ⇀ 'v) ⇒ 'm ⇒ assn"
  fixes is_it :: "('k ⇀ 'v) ⇒ 'm ⇒ ('k ⇀ 'v) ⇒ 'it ⇒ assn"
  fixes it_init :: "'m ⇒ ('it) Heap"
  fixes it_has_next :: "'it ⇒ bool Heap"
  fixes it_next :: "'it ⇒ (('k×'v)×'it) Heap"
  assumes it_init_rule[sep_heap_rules]: 
    "<is_map s p> it_init p <is_it s p s>⇩t"
  assumes it_next_rule[sep_heap_rules]: "m'≠Map.empty ⟹ 
    <is_it m p m' it> 
      it_next it 
    <λ((k,v),it'). is_it m p (m' |` (-{k})) it' * ↑(m' k = Some v)>⇩t"
  assumes it_has_next_rule[sep_heap_rules]: 
    "<is_it m p m' it> it_has_next it <λr. is_it m p m' it * ↑(r⟷m'≠Map.empty)>⇩t"
  assumes quit_iteration:
    "is_it m p m' it ⟹⇩A is_map m p * true"

locale imp_map_iterate' = imp_map +
  constrains is_map :: "('k ⇀ 'v) ⇒ 'm ⇒ assn"
  fixes is_it :: "('k ⇀ 'v) ⇒ 'm ⇒ ('k×'v) list ⇒ 'it ⇒ assn"
  fixes it_init :: "'m ⇒ ('it) Heap"
  fixes it_has_next :: "'it ⇒ bool Heap"
  fixes it_next :: "'it ⇒ (('k×'v)×'it) Heap"
  assumes it_init_rule[sep_heap_rules]: 
    "<is_map s p> it_init p <λr. ∃⇩Al. ↑(map_of l = s) * is_it s p l r>⇩t"
  assumes it_next_rule[sep_heap_rules]: " 
    <is_it m p (kv#l) it> 
      it_next it 
    <λ(kv',it'). is_it m p l it' * ↑(kv'=kv)>"
  assumes it_has_next_rule[sep_heap_rules]: 
    "<is_it m p l it> it_has_next it <λr. is_it m p l it * ↑(r⟷l≠[])>"
  assumes quit_iteration:
    "is_it m p l it ⟹⇩A is_map m p * true"

end