Theory PrioUniqueSpec

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

(*@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)"
begin

  lemma popE: 
    assumes 
    "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
    done

end

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"
begin
  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"
end

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
begin
  lemmas correct = 
    finite_correct 
    empty_correct 
    isEmpty_correct 
    insert_correct 
    prio_correct
end

locale StdUprio_no_invar = StdUprio + uprio_no_invar α invar

end