Theory Deque

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