Theory Queue_Spec

(* Author: Tobias Nipkow *)

section ‹Queue Specification›

theory Queue_Spec
imports Main
begin

text ‹The basic queue interface with list›-based specification:›

locale Queue =
fixes empty :: "'q"
fixes enq :: "'a  'q  'q"
fixes first :: "'q  'a"
fixes deq :: "'q  'q"
fixes is_empty :: "'q  bool"
fixes list :: "'q  'a list"
fixes invar :: "'q  bool"
assumes list_empty:    "list empty = []"
assumes list_enq:      "invar q  list(enq x q) = list q @ [x]"
assumes list_deq:      "invar q  list(deq q) = tl(list q)"
assumes list_first:    "invar q  ¬ list q = []  first q = hd(list q)"
assumes list_is_empty: "invar q  is_empty q = (list q = [])"
assumes invar_empty:   "invar empty"
assumes invar_enq:     "invar q  invar(enq x q)"
assumes invar_deq:     "invar q  invar(deq q)"

end