# 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
```