\chapter{The more\_lists Library}

This document describes the facilities provided by the \ml{more\_lists}
library. The 
library contains an \adhoc\ collection of definitions 
and theorems about lists which extends the standard theory \ml{list}. Included
are many general purpose theorems about the list operators defined in the
theory \ml{list}. In addition, definitions of new operators are given with
associated 
theorems. Several tactics and conversions related to lists are also
provided.  
The library is split into several theories, the ancestry of which is shown
below. 
{\samepage
\begin{center}
\begin{picture}(75,135)(-10,10)

\thicklines

% -----------------------------------------------------------
% Lines in theory hierarchy graph
% -----------------------------------------------------------

\put(30,27.5){\line(0,1){2.5}}      % more_lists --> num_lists
\put(10,25){\line(0,1){5}}	 % more_lists --> unappend
\put(-10,27.5){\line(0,1){2.5}}	 % more_lists --> shift
\put(50,27.5){\line(0,1){2.5}}	 % more_lists --> zip

\put(-10,27.5){\line(1,0){60}}	 % more_lists --> zip

\put(10,35){\line(0,1){5}}	 % unappend --> member
\put(10,45){\line(0,1){5}}	 % member --> last_subseq
\put(10,55){\line(0,1){5}}	 % last_subseq --> subseq
\put(10,65){\line(0,1){5}}	 % subseq --> ell
\put(10,75){\line(0,1){5}}	 % ell --> el
\put(10,85){\line(0,1){5}}	 % el --> map
\put(10,95){\line(0,1){5}}	 % map --> append
\put(10,105){\line(0,1){5}}	 % append --> snoc
\put(10,115){\line(0,1){5}}	 % snoc --> general_lists
\put(10,125){\line(0,1){5}}	 % general_lists --> list

\put(-10,35){\line(0,1){12.5}}	 % shift --> last_subseq
\put(-10,47.5){\line(1,0){20}}	 % shift --> last_subseq


\put(-10,115){\line(0,1){2.5}}     % tail --> general_lists
\put(-10,117.5){\line(1,0){20}}     % tail --> general_lists
\put(-10,97.5){\line(0,1){12.5}} % map --> tail
\put(-10,97.5){\line(1,0){20}}	 % map --> tail


\put(30,35){\line(0,1){42.5}}	 % num_lists --> el
\put(10,77.5){\line(1,0){20}}	 % num_lists --> el

\put(10,127.5){\line(1,0){40}}     % list --> zip
\put(50,35){\line(0,1){92.5}}     % list --> zip

% -----------------------------------------------------------
% Theory names:
% -----------------------------------------------------------

\put(10,22.5){\makebox(0,0){\verb!more\_lists!}}

\put(50,32.5){\makebox(0,0){\verb!zip!}}
\put(-10,32.5){\makebox(0,0){\verb!shift!}}
\put(30,32.5){\makebox(0,0){\verb!num\_lists!}}
\put(10,32.5){\makebox(0,0){\verb!unappend!}}

\put(10,82.5){\makebox(0,0){\verb!el!}}
\put(10,72.5){\makebox(0,0){\verb!ell!}}
\put(10,92.5){\makebox(0,0){\verb!map!}}

\put(-10,112.5){\makebox(0,0){\verb!tail!}}
\put(10,62.5){\makebox(0,0){\verb!subseq!}}
\put(10,52.5){\makebox(0,0){\verb!last\_subseq!}}
\put(10,42.5){\makebox(0,0){\verb!member!}}
\put(10,102.5){\makebox(0,0){\verb!append!}}
\put(10,112.5){\makebox(0,0){\verb!snoc!}}

\put(10,122.5){\makebox(0,0){\verb!general\_lists!}}

\put(10,132.5){\makebox(0,0){\verb!list!}}
\end{picture}
\end{center}

}

\noindent
A complete list of the theorems which are available in the library is given in
Chapter \ref{thms}. Due 
to the large number of theorems, users of the library may find the theorem
retrieval library of help. The above hierarchy should be kept in mind when
searching for theorems.
 All definitions and theorems from the ancestor theories are
automatically loaded, if possible, when their names are first mentioned during
a \HOL\ session. 


\section{The Theory {\tt more\_lists}}

The theory \ml{more\_lists}\index{more\_lists, theory@{\ptt more\_lists}, theory}
is the descendant theory of all the theories in 
the library. It contains no theorems or definitions itself.

