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