Theory FingerTree
section "2-3 Finger Trees"
theory FingerTree
imports Main
begin
text ‹
We implement and prove correct 2-3 finger trees as described by Ralf Hinze
and Ross Paterson\<^cite>‹"HiPa06"›.
›
text ‹
This theory is organized as follows:
Section~\ref{sec:datatype} contains the finger-tree datatype, its invariant
and its abstraction function to lists.
The Section~\ref{sec:operations} contains the operations
on finger trees and their correctness lemmas.
Section~\ref{sec:hide_invar} contains a finger tree datatype with implicit
invariant, and, finally, Section~\ref{sec:doc} contains a documentation
of the implemented operations.
›
text_raw ‹\paragraph{Technical Issues}›
text ‹
As Isabelle lacks proper support of namespaces, we
try to simulate namespaces by locales.
The problem is, that we define lots of internal functions that
should not be exposed to the user at all.
Moreover, we define some functions with names equal to names
from Isabelle's standard library. These names make perfect sense
in the context of FingerTrees, however, they shall not be exposed
to anyone using this theory indirectly, hiding the standard library
names there.
Our approach puts all functions and lemmas inside the locale
{\em FingerTree\_loc},
and then interprets this locale with the prefix {\em FingerTree}.
This makes all definitions visible outside the locale, with
qualified names. Inside the locale, however, one can use unqualified names.
›
subsection "Datatype definition"
text_raw‹\label{sec:datatype}›
locale FingerTreeStruc_loc
text ‹
Nodes: Non empty 2-3 trees, with all elements stored within the leafs plus a
cached annotation
›