\section{The Theory {\tt el}}

The theory \ml{el}\index{el, theory@{\ptt el}, theory} is concerned with selecting elements from
a list. It contains several new theorems about the function
\ml{EL}\index{EL@{\ptt EL}}, defined in the theory \ml{list}.
A similar function \ml{EL1}\index{EL1@{\ptt EL1}} is also defined here. It
chooses an 
element from a list indexing from 1. It is undefined  for an index of 0.
This contrasts with \ml{EL} which indexes from 0.


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

\noindent It is defined as follows:

\begin{hol}
\index{EL1@{\ptt EL1}}
\begin{verbatim}
  EL1          |- !n l. EL1(SUC n)l = EL n l 
\end{verbatim}\end{hol}

\noindent Following are some of the theorems pre-proved in this theory.

\begin{hol}
\index{EL\_HD@{\ptt EL\_HD}}
\index{EL\_APPEND\_1@{\ptt EL\_APPEND\_1}}
\index{EL\_APPEND\_2@{\ptt EL\_APPEND\_2}}
\index{EL1\_SUC\_CONS@{\ptt EL1\_SUC\_CONS}}
\index{EL1\_HD@{\ptt EL1\_HD}}
\begin{verbatim}
  EL_HD        |- !l. ~NULL l ==> (EL 0 l = HD l)

  EL_APPEND_1  |- !l1 l2 k. k < (LENGTH l1) ==> (EL k(APPEND l1 l2) = EL k l1)

  EL_APPEND_2  |- !l1 l2 k.  (LENGTH l1) <= k ==>
                                  (EL k(APPEND l1 l2) = EL(k - (LENGTH l1))l2)

  EL1_SUC_CONS |- !n h l. 0 < n ==> (EL1(SUC n)(CONS h l) = EL1 n l)

  EL1_HD       |- !l. ~NULL l ==> (EL1 1 l = HD l)
\end{verbatim}\end{hol}
