Theory PrioUniqueSpec

section ‹\isaheader{Specification of Unique Priority Queues}›
theory PrioUniqueSpec
imports ICF_Spec_Base

(*@intf PrioUnique
  @abstype ('e ⇀ 'a::linorder)
  Priority queues without duplicate elements. This interface defines a
  decrease-key operation.

text ‹
  We define unique priority queues, where each element may occur at most once.
  We provide operations to get and remove the element with the minimum priority,
  as well as to access and change an elements priority (decrease-key operation).

  Unique priority queues are abstracted to maps from elements to priorities.
locale uprio =  
  fixes α :: "'s  ('e  'a::linorder)" 
  fixes invar :: "'s  bool"                     

locale uprio_no_invar = uprio +
  assumes invar[simp, intro!]: "s. invar s"
locale uprio_finite = uprio +
  assumes finite_correct: 
  "invar s  finite (dom (α s))"

subsection "Basic Upriority Queue Functions"

subsubsection "Empty Queue"
locale uprio_empty = uprio +
  constrains α :: "'s  ('e  'a::linorder)"
  fixes empty :: "unit  's"
  assumes empty_correct: 
  "invar (empty ())" 
  "α (empty ()) = Map.empty"

subsubsection "Emptiness Predicate"
locale uprio_isEmpty = uprio +
  constrains α :: "'s  ('e  'a::linorder)"
  fixes isEmpty :: "'s  bool"
  assumes isEmpty_correct: 
  "invar s  (isEmpty s) = (α s = Map.empty)" 

subsubsection "Find and Remove Minimal Element"
locale uprio_pop = uprio +
  constrains α :: "'s  ('e  'a::linorder)"
  fixes pop :: "'s  ('e × 'a × 's)"
  assumes pop_correct:
  "invar s; α s  Map.empty; pop s = (e,a,s')  
    invar s'  
    α s' = (α s)(e := None)  
    (α s) e = Some a  
    (y  ran (α s). a  y)"

  lemma popE: 
    "invar s" 
    "α s  Map.empty" 
    obtains e a s' where 
    "pop s = (e, a, s')" 
    "invar s'" 
    "α s' = (α s)(e := None)" 
    "(α s) e = Some a" 
    "(y  ran (α s). a  y)"
    using assms
    apply (cases "pop s")
    apply (drule (2) pop_correct)
    apply blast


subsubsection "Insert"
text ‹
  If an existing element is inserted, its priority will be overwritten.
  This can be used to implement a decrease-key operation.
(* TODO: Implement decrease-key generic algorithm, and specify decrease-key operation here! *)
locale uprio_insert = uprio +
  constrains α :: "'s  ('e  'a::linorder)"
  fixes insert :: "'s  'e  'a  's"
  assumes insert_correct: 
  "invar s  invar (insert s e a)"
  "invar s  α (insert s e a) = (α s)(e  a)" 

subsubsection "Distinct Insert"
text ‹
  This operation only allows insertion of elements
  that are not yet in the queue.
locale uprio_distinct_insert = uprio +
  constrains α :: "'s  ('e  'a::linorder)"
  fixes insert :: "'s  'e  'a  's"
  assumes distinct_insert_correct: 
  "invar s; e  dom (α s)  invar (insert s e a)"
  "invar s; e  dom (α s)  α (insert s e a) = (α s)(e  a)" 

subsubsection "Looking up Priorities"
locale uprio_prio = uprio +
  constrains α :: "'s  ('e  'a::linorder)"
  fixes prio :: "'s  'e  'a option"
  assumes prio_correct: 
  "invar s  prio s e = (α s) e"

subsection "Record Based Interface"

record ('e, 'a, 's) uprio_ops =
  upr_α :: "'s  ('e  'a)" 
  upr_invar :: "'s  bool"                 
  upr_empty :: "unit  's"
  upr_isEmpty :: "'s  bool"
  upr_insert :: "'s  'e  'a  's"
  upr_pop :: "'s  ('e × 'a × 's)"
  upr_prio :: "'s  'e  'a option"

locale StdUprioDefs =
  fixes ops :: "('e,'a::linorder,'s, 'more) uprio_ops_scheme"
  abbreviation α where "α == upr_α ops"
  abbreviation invar where "invar == upr_invar ops"
  abbreviation empty where "empty == upr_empty ops"
  abbreviation isEmpty where "isEmpty == upr_isEmpty ops"
  abbreviation insert where "insert == upr_insert ops"
  abbreviation pop where "pop == upr_pop ops"
  abbreviation prio where "prio == upr_prio ops"

locale StdUprio =  StdUprioDefs ops +
  uprio_finite α invar + 
  uprio_empty α invar empty + 
  uprio_isEmpty α invar isEmpty + 
  uprio_insert α invar insert + 
  uprio_pop α invar pop + 
  uprio_prio α invar prio
  for ops
  lemmas correct = 

locale StdUprio_no_invar = StdUprio + uprio_no_invar α invar