Theory PrioUniqueByAnnotatedList
section ‹\isaheader{Implementing Unique Priority Queues by Annotated Lists}›
theory PrioUniqueByAnnotatedList
imports
"../spec/AnnotatedListSpec"
"../spec/PrioUniqueSpec"
begin
text ‹
In this theory we use annotated lists to implement unique priority queues
with totally ordered elements.
This theory is written as a generic adapter from the AnnotatedList interface
to the unique priority queue interface.
The annotated list stores a sequence of elements annotated with
priorities\footnote{Technically, the annotated list elements are of unit-type,
and the annotations hold both, the priority queue elements and the priorities.
This is required as we defined annotated lists to only sum up the elements
annotations.}
The monoids operations forms the maximum over the elements and
the minimum over the priorities.
The sequence of pairs is ordered by ascending elements' order.
The insertion point for a new element, or the priority of an existing element
can be found by splitting the
sequence at the point where the maximum of the elements read so far gets
bigger than the element to be inserted.
The minimum priority can be read out as the sum over the whole sequence.
Finding the element with minimum priority is done by splitting the sequence
at the point where the minimum priority of the elements read so far becomes
equal to the minimum priority of the whole sequence.
›
subsection "Definitions"
subsubsection "Monoid"