Theory PrioSpec

header {*\isaheader{Specification of Priority Queues}*}
theory PrioSpec
imports Main "~~/src/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"

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_of (α 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

end