\section{The Theory {\tt subseq}}

The theory \ml{subseq}\index{subseq, theory@{\ptt subseq}, theory} deals with extracting
subsequences from a list, indexing from the front of the list.

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

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


\ml{SUBSEQ}\index{SUBSEQ@{\ptt SUBSEQ}}, is similar to \ml{FIRSTN} except that
it returns the empty list if {\em k} is larger than the length of
the list.

\[ \begin{array}[t]{@{}l@{}l@{}l}
  \ml{SUBSEQ}\; k \ml{[}a_1\listsep a_k\listsep a_n\ml{]} & =
                                         \ml{[}a_1\listsep a_k\ml{]} \\
  \ml{SUBSEQ}\; k \ml{[}a_1\listsep a_n\ml{]}  & = \ml{[]} & (k>n)
 \end{array}
\]


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


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


\ml{NTAIL}\index{NTAIL@{\ptt NTAIL}}, is similar to \ml{NTL} except that
it returns the empty list if {\em k} is larger than the length of
the list.

\[ \begin{array}[t]{@{}l@{}l@{}l}
  \ml{NTAIL}\; k \ml{[}a_1\listsep a_k\listsep a_n\ml{]}  & =
                                         \ml{[}a_{k+1}\listsep a_n\ml{]} \\
  \ml{NTAIL}\; k \ml{[}a_1\listsep a_n\ml{]}  & = \ml{[]} & (k>n)
 \end{array}
\]


\noindent The  \HOL\ definitions of these operators are 


\begin{hol}
\index{FIRSTN@{\ptt FIRSTN}}
\index{SUBSEQ@{\ptt SUBSEQ}}
\index{NTL@{\ptt NTL}}
\index{NTAIL@{\ptt NTAIL}}
\begin{verbatim}
  FIRSTN    |- (!X. FIRSTN 0 X = []) /\
               (!n X. FIRSTN(SUC n)X = CONS(HD X)(FIRSTN n(TL X)))

  SUBSEQ    |- (!x. SUBSEQ 0 x = []) /\
               (!n x. SUBSEQ(SUC n)x =
                         (NULL x => [] | CONS(HD x)(SUBSEQ n(TAIL x))))

  NTL       |- (!X. NTL 0 X = X) /\ (!n X. NTL(SUC n)X = NTL n(TL X))

  NTAIL     |- (!l. NTAIL 0 l = l) /\ (!n l. NTAIL(SUC n)l = TAIL(NTAIL n l))
 \end{verbatim}\end{hol}

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

\begin{hol}
\index{NTL\_TL\_SYM@{\ptt NTL\_TL\_SYM}}
\index{FIRSTN\_NULL@{\ptt FIRSTN\_NULL}}
\index{SUBSEQ\_SUBSEQ@{\ptt SUBSEQ\_SUBSEQ}}
\index{EL\_HD\_NTAIL@{\ptt EL\_HD\_NTAIL}}
\begin{verbatim}
  NTL_TL_SYM            |- !n X. NTL n(TL X) = TL(NTL n X)

  FIRSTN_NULL           |- !n X. NULL(FIRSTN n X) ==> (n = 0)

  SUBSEQ_SUBSEQ         |- !n x. SUBSEQ n(SUBSEQ n x) = SUBSEQ n x

  EL_HD_NTAIL           |- !x l. ~NULL(NTAIL x l) ==> (EL x l = HD(NTAIL x l))
\end{verbatim}\end{hol}
