\section{The Theory {\tt last\_subseq}}

The theory \ml{last\_subseq}\index{last\_subseq, theory@{\ptt last\_subseq}, theory} deals with extracting
subsequences from a list. Unlike the operators in the theory \ml{subseq},
the operators in this theory access the list indexing from the tail end.

\ml{LASTN}\index{LASTN@{\ptt LASTN}}, given an argument {\em k}, returns a
list of the last {\em k}  
elements of a list. It is undefined if  {\em k} is larger than the length of
the list.

\begin{hol}
\[
  \ml{LASTN}\; k \ml{[}a_n\listsep a_k\listsep a_1\ml{]} =
                                         \ml{[}a_k\listsep a_1\ml{]}
\]\end{hol}


\ml{NBUTLAST}\index{NBUTLAST@{\ptt NBUTLAST}}, given an argument {\em k}, returns
the remainder 
of a list after the last {\em k} elements have been removed.
 It is undefined if  {\em k} is larger than the length of the list.


\begin{hol}
\[
  \ml{NBUTLAST}\; k \ml{[}a_n\listsep a_k\listsep a_1\ml{]} =
                                         \ml{[}a_n\listsep a_{k+1}\ml{]}
\]\end{hol}

\noindent The  \HOL\ definitions of these operators are 


\begin{hol}
\index{LASTN@{\ptt LASTN}}
\index{NBUTLAST@{\ptt NBUTLAST}}
\begin{verbatim}
  LASTN     |- (!X. LASTN 0 X = []) /\
               (!n X. LASTN(SUC n)X = APPEND(LASTN n(BUTLAST X))[LAST X])

  NBUTLAST  |- (!X. NBUTLAST 0 X = X) /\
               (!n X. NBUTLAST(SUC n)X = NBUTLAST n(BUTLAST X))
 \end{verbatim}\end{hol}

\noindent This theory contains a large number of theorems, a sample of which
is given below.

\begin{hol}
\index{LASTN\_LENGTH\_ID@{\ptt LASTN\_LENGTH\_ID}}
\index{LASTN\_NULLN@{\ptt LASTN\_NULLN}}
\index{NBUTLAST\_BUTLAST\_SYM@{\ptt NBUTLAST\_BUTLAST\_SYM}}
\index{NBUTLAST\_LENGTH\_NULL@{\ptt NBUTLAST\_LENGTH\_NULL}}
\index{APPEND\_NBUTLAST\_LASTN@{\ptt APPEND\_NBUTLAST\_LASTN}}
\begin{verbatim}
  LASTN_LENGTH_ID       |- !X. LASTN(LENGTH X)X = X

  LASTN_NULL            |- !n X. NULL(LASTN n X) ==> (n = 0)

  NBUTLAST_BUTLAST_SYM  |- !n X. NBUTLAST n(BUTLAST X) = BUTLAST(NBUTLAST n X)

  NBUTLAST_LENGTH_NULL  |- !X. NULL(NBUTLAST(LENGTH X)X)

  APPEND_NBUTLAST_LASTN |- !n X. n <= (LENGTH X) ==>
                                         (APPEND(NBUTLAST n X)(LASTN n X) = X)
\end{verbatim}\end{hol}
