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

The theory {\small\verb%general_lists%}\index{general\_lists, theory@{\ptt general\_lists}, theory} contains
an \adhoc\ collection of theorems about the basic list operators defined in
the standard theory \ml{list}. In particular, it contains theorems about the
operators \ml{CONS}\index{CONS@{\ptt CONS}}, \ml{TL}\index{TL@{\ptt TL}}, \ml{NULL}\index{NULL@{\ptt NULL}} and \ml{LENGTH}\index{LENGTH@{\ptt LENGTH}}.
It does not contain theorems about the standard operators \ml{APPEND} or
\ml{EL} which may be found in the theories \ml{append} and \ml{el},
respectively, nor about \ml{MAP} and \ml{EVERY} which may be found in the
theory \ml{map}. A selection of the theorems available are given below.
\begin{hol}
\index{NULL\_EQ\_EMPTY@{\ptt NULL\_EQ\_EMPTY}}
\index{LENGTH\_EQ@{\ptt LENGTH\_EQ}}
\index{TL\_NULL@{\ptt TL\_NULL}}
\index{LENGTH\_NULL@{\ptt LENGTH\_NULL}}
\index{CONS\_ONE\_ONE@{\ptt CONS\_ONE\_ONE}}
\begin{verbatim}
  NULL_EQ_EMPTY  |- !l. NULL l = (l = [])

  LENGTH_EQ      |- !x y. (x = y) ==> (LENGTH x = LENGTH y)

  TL_NULL        |- !l. (LENGTH l = 1) ==> NULL(TL l)

  LENGTH_NULL    |- !l. (LENGTH l = 0) = NULL l

  CONS_ONE_ONE   |- !h t h' t'. (CONS h t = CONS h' t') ==>
                                          (h = h') /\ (t = t')
\end{verbatim}\end{hol}

The tactic
\ml{LIST\_LENGTH\_INDUCT\_TAC}\index{LIST\_LENGTH\_INDUCT\_TAC@{\ptt LIST\_LENGTH\_INDUCT\_TAC}}  performs induction on the length of a
list. If the tactic is applied to the goal

\begin{hol}\begin{verbatim}
  ?- !(x :* list) (y:** list). (LENGTH x = LENGTH y) ==> P x y
\end{verbatim}\end{hol}

\noindent it will yield the following subgoals:

\begin{hol}\begin{verbatim}
  ?- P[][]

  P(TL x)(TL y) ?- P(CONS(HD x)(TL x))(CONS(HD y)(TL y))
\end{verbatim}\end{hol}

\noindent See the documentation of the function in Chapter 
\ref{entries} for
more details. 
