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 * ↑(r⟷l'≠[])>⇩t"
  assumes quit_iteration:
    "is_it l p l' it ⟹⇩A is_list l p * true"

end