\section{The Theory {\tt tail}}

It is sometimes useful to be able to say that the tail of an empty list is an
empty list. However \ml{TL}\index{TL@{\ptt TL}} is undefined in this situation.
The theory \ml{tail}\index{tail, theory@{\ptt tail}, theory} provides an alternative
definition \ml{TAIL}\index{TAIL@{\ptt TAIL}} for taking the tail of a list which
has this property. 

\[ \begin{array}[t]{@{}l@{}l}
  \ml{TAIL}\ml{[]} = \ml{[]} \\
  \ml{TAIL}\ml{[}h \lsep a_1\listsep a_n\ml{]} = \ml{[} a_1\listsep a_n\ml{]}
 \end{array}
\]

\noindent It is defined using primitive recursion

\begin{hol}
\index{TAIL@{\ptt TAIL}}
\begin{verbatim}
  TAIL  |- (TAIL[] = []) /\ (!h t. TAIL(CONS h t) = t) 
\end{verbatim}\end{hol}

\noindent Several theorems are pre-proved.

\begin{hol}
\index{CON@{\ptt CON}}
\index{TAIL\_APPEND@{\ptt TAIL\_APPEND}}
\index{list\_CASES2@{\ptt list\_CASES2}}
\index{list\_NULL\_CASES2@{\ptt list\_NULL\_CASES2}}
\index{list\_NULL\_CASES2@{\ptt list\_NULL\_CASES2}}
\index{LENGTH\_TAIL@{\ptt LENGTH\_TAIL}}
\index{TL\_TAIL@{\ptt TL\_TAIL}}
\index{NOT\_NULL\_TAIL@{\ptt NOT\_NULL\_TAIL}}
\begin{verbatim}
  CON               |- !l. ~NULL l ==> (CONS(HD l)(TAIL l) = l)

  TAIL_APPEND       |- !x y. TAIL(APPEND x y) =
                             ((x = []) => TAIL y | APPEND(TAIL x)y)

  list_CASES2       |- !l. (l = []) \/ (l = CONS(HD l)(TAIL l))

  list_NULL_CASES2  |- !l. NULL l \/ (l = CONS(HD l)(TAIL l))

  LENGTH_TAIL       |- !l. ~NULL l ==> (LENGTH(TAIL l) = (LENGTH l) - 1)

  TL_TAIL           |- !l. ~NULL l ==> (TL l = TAIL l)

  NOT_NULL_TAIL     |- !l. ~NULL(TAIL l) ==> ~NULL l
  
\end{verbatim}\end{hol}
