Theory Binomial-Heaps.SkewBinomialHeap
section "Skew Binomial Heaps"
theory SkewBinomialHeap
imports Main "HOL-Library.Multiset"
begin
text ‹Skew Binomial Queues as specified by Brodal and Okasaki \<^cite>‹"BrOk96"›
are a data structure for priority queues with worst case O(1) {\em findMin},
{\em insert}, and {\em meld} operations, and worst-case logarithmic
{\em deleteMin} operation.
They are derived from priority queues in three steps:
\begin{enumerate}
\item Skew binomial trees are used to eliminate the possibility of
cascading links during insert operations. This reduces the complexity
of an insert operation to $O(1)$.
\item The current minimal element is cached. This approach, known as
{\em global root}, reduces the cost of a {\em findMin}-operation to
O(1).
\item By allowing skew binomial queues to contain skew binomial queues,
the cost for meld-operations is reduced to $O(1)$. This approach
is known as {\em data-structural bootstrapping}.
\end{enumerate}
In this theory, we combine Steps~2 and 3, i.e. we first implement skew binomial
queues, and then bootstrap them. The bootstrapping implicitly introduces a
global root, such that we also get a constant time findMin operation.
›
locale SkewBinomialHeapStruc_loc
begin
subsection "Datatype"