Theory Separation_Logic_Imperative_HOL.Imp_List_Spec

section ‹Interface for Lists›
theory Imp_List_Spec
imports "../Sep_Main"
begin
text ‹
  This file specifies an abstract interface for list data structures. It can
  be implemented by concrete list data structures, as demonstrated in the open
  and circular singly linked list examples.
›

locale imp_list =
  fixes is_list :: "'a list  'l  assn"
  assumes precise: "precise is_list"
    (*"∀l l'. h⊨(is_list l p * F1) ∧A (is_list l' p * F2) ⟶ l=l'"*)

locale imp_list_empty = imp_list +
  constrains is_list :: "'a list  'l  assn"
  fixes empty :: "'l Heap"
  assumes empty_rule[sep_heap_rules]: "<emp> empty <is_list []>t"

locale imp_list_is_empty = imp_list +
  constrains is_list :: "'a list  'l  assn"
  fixes is_empty :: "'l  bool Heap"
  assumes is_empty_rule[sep_heap_rules]: 
    "<is_list l p> is_empty p <λr. is_list l p * (r  l=[])>t"

locale imp_list_append = imp_list +
  constrains is_list :: "'a list  'l  assn"
  fixes append :: "'a  'l  'l Heap"
  assumes append_rule[sep_heap_rules]: 
    "<is_list l p> append a p <is_list (l@[a])>t"

locale imp_list_prepend = imp_list +
  constrains is_list :: "'a list  'l  assn"
  fixes prepend :: "'a  'l  'l Heap"
  assumes prepend_rule[sep_heap_rules]: 
    "<is_list l p> prepend a p <is_list (a#l)>t"
    
locale imp_list_head = imp_list +
  constrains is_list :: "'a list  'l  assn"
  fixes head :: "'l  'a Heap"
  assumes head_rule[sep_heap_rules]: 
    "l[]  <is_list l p> head p <λr. is_list l p * (r=hd l)>t"

locale imp_list_pop = imp_list +
  constrains is_list :: "'a list  'l  assn"
  fixes pop :: "'l  ('a×'l) Heap"
  assumes pop_rule[sep_heap_rules]: 
    "l[]  
      <is_list l p> 
      pop p 
      <λ(r,p'). is_list (tl l) p' * (r=hd l)>t"

locale imp_list_rotate = imp_list +
  constrains is_list :: "'a list  'l  assn"
  fixes rotate :: "'l  'l Heap"
  assumes rotate_rule[sep_heap_rules]: 
    "<is_list l p> rotate p <is_list (rotate1 l)>t"

locale imp_list_reverse = imp_list +
  constrains is_list :: "'a list  'l  assn"
  fixes reverse :: "'l  'l Heap"
  assumes reverse_rule[sep_heap_rules]: 
    "<is_list l p> reverse p <is_list (rev l)>t"

locale imp_list_iterate = imp_list +
  constrains is_list :: "'a list  'l  assn"
  fixes is_it :: "'a list  'l  'a list  'it  assn"
  fixes it_init :: "'l  ('it) Heap"
  fixes it_has_next :: "'it  bool Heap"
  fixes it_next :: "'it  ('a×'it) Heap"
  assumes it_init_rule[sep_heap_rules]: 
    "<is_list l p> it_init p <is_it l p l>t"
  assumes it_next_rule[sep_heap_rules]: "l'[]  
    <is_it l p l' it> 
      it_next it 
    <λ(a,it'). is_it l p (tl l') it' * (a=hd l')>t"
  assumes it_has_next_rule[sep_heap_rules]: 
    "<is_it l p l' it> 
       it_has_next it 
     <λr. is_it l p l' it * (rl'[])>t"
  assumes quit_iteration:
    "is_it l p l' it A is_list l p * true"

end