Theory 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