Theory HOL-Data_Structures.Priority_Queue_Specs

(* Author: Tobias Nipkow, Peter Lammich *)

section ‹Priority Queue Specifications›

theory Priority_Queue_Specs
imports "HOL-Library.Multiset"
begin

text ‹Priority queue interface + specification:›
    
locale Priority_Queue =
fixes empty :: "'q"
and is_empty :: "'q ⇒ bool"
and insert :: "'a::linorder ⇒ 'q ⇒ 'q"
and get_min :: "'q ⇒ 'a"
and del_min :: "'q ⇒ 'q"
and invar :: "'q ⇒ bool"
and mset :: "'q ⇒ 'a multiset"
assumes mset_empty: "mset empty = {#}"
and is_empty: "invar q ⟹ is_empty q = (mset q = {#})"
and mset_insert: "invar q ⟹ mset (insert x q) = mset q + {#x#}"
and mset_del_min: "invar q ⟹ mset q ≠ {#} ⟹ 
    mset (del_min q) = mset q - {# get_min q #}"
and mset_get_min: "invar q ⟹ mset q ≠ {#} ⟹ get_min q = Min_mset (mset q)"
and invar_empty: "invar empty"
and invar_insert: "invar q ⟹ invar (insert x q)"
and invar_del_min: "invar q ⟹ mset q ≠ {#} ⟹ invar (del_min q)"

text ‹Extend locale with ‹merge›. Need to enforce that ‹'q› is the same in both locales.›

locale Priority_Queue_Merge = Priority_Queue where empty = empty for empty :: 'q +
fixes merge :: "'q ⇒ 'q ⇒ 'q"
assumes mset_merge: "⟦ invar q1; invar q2 ⟧ ⟹ mset (merge q1 q2) = mset q1 + mset q2"
and invar_merge: "⟦ invar q1; invar q2 ⟧ ⟹ invar (merge q1 q2)"

end