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 * (rm'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 * (rl[])>"
  assumes quit_iteration:
    "is_it m p l it A is_map m p * true"

end