Theory Collections.PrioSpec

section ‹\isaheader{Specification of Priority Queues}›
theory PrioSpec
imports ICF_Spec_Base "HOL-Library.Multiset"
begin

(*@intf Prio
  @abstype ('e × 'a::linorder) multiset
  Priority queues that may contain duplicate elements.
*)

text ‹
  We specify priority queues, that are abstracted to
  multisets of pairs of elements and priorities.
›

locale prio = 
  fixes α :: "'p  ('e × 'a::linorder) multiset" ― ‹Abstraction to multiset›
  fixes invar :: "'p  bool"                     ― ‹Invariant›

locale prio_no_invar = prio +
  assumes invar[simp, intro!]: "s. invar s"

subsection "Basic Priority Queue Functions"
subsubsection "Empty Queue"
locale prio_empty = prio +
  constrains α :: "'p  ('e × 'a::linorder) multiset"
  fixes empty :: "unit  'p"
  assumes empty_correct: 
  "invar (empty ())" 
  "α (empty ()) = {#}"


subsubsection "Emptiness Predicate"
locale prio_isEmpty = prio +
  constrains α :: "'p  ('e × 'a::linorder) multiset"
  fixes isEmpty :: "'p  bool"
  assumes isEmpty_correct: 
  "invar p  (isEmpty p) = (α p = {#})" 


subsubsection "Find Minimal Element"
locale prio_find = prio +
  constrains α :: "'p  ('e × 'a::linorder) multiset"
  fixes find :: "'p  ('e × 'a::linorder)"
  assumes find_correct: "invar p; α p  {#}  
       (find p) ∈# (α p)  (y  set_mset (α p). snd (find p)  snd y)"

subsubsection "Insert"
locale prio_insert = prio +
  constrains α :: "'p  ('e × 'a::linorder) multiset"
  fixes insert :: "'e  'a  'p  'p"
  assumes insert_correct: 
  "invar p  invar (insert e a p)"
  "invar p  α (insert e a p) = (α p) + {#(e,a)#}" 

subsubsection "Meld Two Queues"
locale prio_meld = prio +
  constrains α :: "'p  ('e × 'a::linorder) multiset"
  fixes meld :: "'p  'p  'p"
  assumes meld_correct:
  "invar p; invar p'  invar (meld p p')"
  "invar p; invar p'  α (meld p p') = (α p) + (α p')"

subsubsection "Delete Minimal Element"
text ‹Delete the same element that find will return›
locale prio_delete = prio_find +
  constrains α :: "'p  ('e × 'a::linorder) multiset"
  fixes delete :: "'p  'p"
  assumes delete_correct:
  "invar p; α p  {#}  invar (delete p)"
  "invar p; α p  {#}  α (delete p) = (α p) - {# (find p) #}"


subsection "Record based interface"
record ('e, 'a, 'p) prio_ops =
  prio_op_α :: "'p  ('e × 'a) multiset" 
  prio_op_invar :: "'p  bool" 
  prio_op_empty :: "unit  'p" 
  prio_op_isEmpty :: "'p  bool" 
  prio_op_insert :: "'e  'a  'p  'p" 
  prio_op_find :: "'p  'e × 'a" 
  prio_op_delete :: "'p  'p" 
  prio_op_meld :: "'p  'p  'p"

locale StdPrioDefs =
  fixes ops :: "('e,'a::linorder,'p) prio_ops"
begin
  abbreviation α where "α == prio_op_α ops"
  abbreviation invar where "invar == prio_op_invar ops"
  abbreviation empty where "empty == prio_op_empty ops"
  abbreviation isEmpty where "isEmpty == prio_op_isEmpty ops"
  abbreviation insert where "insert == prio_op_insert ops"
  abbreviation find where "find == prio_op_find ops"
  abbreviation delete where "delete == prio_op_delete ops"
  abbreviation meld where "meld == prio_op_meld ops"
end

locale StdPrio = StdPrioDefs ops +
  prio α invar +
  prio_empty α invar empty +
  prio_isEmpty α invar isEmpty +
  prio_find α invar find +
  prio_insert α invar insert +
  prio_meld α invar meld +
  prio_delete α invar find delete
  for ops
begin
  lemmas correct =
    empty_correct
    isEmpty_correct
    find_correct
    insert_correct
    meld_correct
    delete_correct
end

locale StdPrio_no_invar = StdPrio + prio_no_invar α invar

end