Quelle  Deque.thy

section  ‹Double-Ended Queue Specification›

theory Deque
imports Main
begin

text ‹Model-oriented specification in terms of an abstraction function to a list.›

locale Deque =
fixes empty :: "'q"
fixes enqL :: "'a ==> 'q ==> 'q"
fixes enqR :: "'a ==> 'q ==> 'q"
fixes firstL :: "'q ==> 'a"
fixes firstR :: "'q ==> 'a"
fixes deqL :: "'q ==> 'q"
fixes deqR :: "'q ==> 'q"
fixes is_empty :: "'q ==> bool"
fixes listL :: "'q ==> 'a list"
fixes invar :: "'q ==> bool"

assumes list_empty:
 "listL empty = []"

assumes list_enqL:   
 "invar q ==> listL(enqL x q) = x # listL q"
assumes list_enqR:  
 "invar q ==> rev (listL (enqR x q)) = x # rev (listL q)"
assumes list_deqL:   
 "[invar q; ¬ listL q = []] ==> listL(deqL q) = tl(listL q)"
assumes list_deqR: 
 "[invar q; ¬ rev (listL q) = []] ==> rev (listL (deqR q)) = tl (rev (listL q))"

assumes list_firstL:
 "[invar q; ¬ listL q = []] ==> firstL q = hd(listL q)"
assumes list_firstR:
 "[invar q; ¬ rev (listL q) = []] ==> firstR q = hd(rev(listL q))"

assumes list_is_empty:  
 "invar q ==> is_empty q = (listL q = [])"

assumes invar_empty: 
 "invar empty"

assumes invar_enqL:  
 "invar q ==> invar(enqL x q)"
assumes invar_enqR: 
 "invar q ==> invar(enqR x q)"
assumes invar_deqL: 
 "[invar q; ¬ is_empty q] ==> invar(deqL q)"
assumes invar_deqR: 
 "[invar q; ¬ is_empty q] ==> invar(deqR q)"
begin

abbreviation listR :: "'q ==> 'a list" where
  "listR deque ≡ rev (listL deque)"

end



end