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

The theory \ml{num\_lists}\index{num\_lists, theory@{\ptt num\_lists}, theory} deals with lists of
numbers (of type \ml{:num list}).

\ml{FROM0}\index{FROM0@{\ptt FROM0}} returns a list of numbers from 0 up to a
given number.


\begin{hol}
\[
  \ml{FROM0}\; n = \ml{[}0 \lsep 1 \listsep n\ml{]}
\]\end{hol}

\ml{UPTO}\index{UPTO@{\ptt UPTO}} is an infix operator which returns a list of
the numbers between two given numbers. It returns an empty list if the second
argument is smaller than the first.

\[ \begin{array}[t]{@{}l@{}l}
m\; \ml{UPTO}\; n  = \ml{[}m \lsep m+1 \listsep n\ml{]} & (m<n) \\
m\; \ml{UPTO}\; m  = \ml{[}m\ml{]} \\
m\; \ml{UPTO}\; n  = \ml{[}\ml{]} & (m>n)
 \end{array}
\]

\ml{RANGE}\index{RANGE@{\ptt RANGE}} is similar to \ml{UPTO} except that the
second argument gives the length of the list.


\[ \begin{array}[t]{@{}l@{}l}
\ml{RANGE}\; m\; n  = \ml{[}m \lsep m+1 \listsep m+n-1\ml{]} \\
\ml{RANGE}\; m\; 0  = \ml{[}\ml{]}
 \end{array}
\]

\noindent The definitions in \HOL\ are


\begin{hol}
\index{RANGE@{\ptt RANGE}}
\index{FROM0@{\ptt FROM0}}
\index{UPTO@{\ptt UPTO}}
\begin{verbatim}
  FROM0    |- (FROM0 0 = [0]) /\ (!n. FROM0(SUC n) = CONS 0(MAP SUC(FROM0 n)))

  UPTO     |- !n1 n2. n1 UPTO n2 = MAP($+ n1)(n1 <= n2 => FROM0(n2 - n1) | [])

  RANGE    |- (!m. RANGE m 0 = []) /\
              (!m n. RANGE m(SUC n) = CONS m(RANGE(SUC m)n))
\end{verbatim}\end{hol}

Below is a selection of theorems proved about them in the theory.

\begin{hol}
\index{RANGE\_TOP@{\ptt RANGE\_TOP}}
\index{RANGE\_SHIFT@{\ptt RANGE\_SHIFT}}
\index{FROM0\_APPEND@{\ptt FROM0\_APPEND}}
\index{UPTO\_EQ\_CONS\_SUC\_UPTO@{\ptt UPTO\_EQ\_CONS\_SUC\_UPTO}}
\index{INTERVAL@{\ptt INTERVAL}}
\begin{verbatim}
  RANGE_TOP             |- !n m. RANGE m(SUC n) = APPEND(RANGE m n)[m + n]

  RANGE_SHIFT           |- !n m. RANGE(SUC m)n = MAP SUC(RANGE m n)

  FROM0_APPEND          |- !n. FROM0(SUC n) = APPEND(FROM0 n)[SUC n]

  UPTO_EQ_CONS_SUC_UPTO |- !m n. m <= n ==>
                                  (m UPTO n = CONS m((SUC m) UPTO n))

  INTERVAL              |- (!m. m UPTO 0 = (m > 0 => [] | [0])) /\
                           (!m n. m UPTO (SUC n) =
                                  (m > (SUC n) => [] | SNOC(SUC n)(m UPTO n)))
\end{verbatim}\end{hol}
