\section{The Theory {\tt append}}

The theory \ml{append}\index{append, theory@{\ptt append}, theory}
contains theorems
and definitions for constructing lists from smaller elements. It contains
further  theorems about \ml{APPEND}\index{APPEND@{\ptt APPEND}} (which is defined
in the theory \ml{list}). In addition it contains 
definitions and associated theorems for
\ml{ITERATED}\index{ITERATED@{\ptt ITERATED}} and
\ml{REPLICATE}\index{REPLICATE@{\ptt REPLICATE}}. 
\ml{ITERATED} appends a given number of copies of a list together, whereas
\ml{REPLICATE} forms a list of a given number of copies of a single element.

\begin{hol}
\[
  \ml{ITERATED}\; n \ml{[}a_1\listsep a_n\ml{]} =
      \ml{[}a_1\listsep a_n \lsep a_1 \listsep a_n \lsep \ldots\ml{]}
\]\end{hol}

\begin{hol}
\[
  \ml{REPLICATE}\; n\; a =  \ml{[}a \listsep a \ml{]}
\]\end{hol}

\noindent They are defined in \HOL\ by primitive recursion.

\begin{hol}
\index{REPLICATE@{\ptt REPLICATE}}
\index{ITERATED@{\ptt ITERATED}}
\begin{verbatim}
  REPLICATE    |- (!in. REPLICATE 0 in = []) /\
                  (!n in. REPLICATE(SUC n)in = CONS in(REPLICATE n in))

  ITERATED     |- (!s. ITERATED 0 s = []) /\
                  (!n s. ITERATED(SUC n)s = APPEND s(ITERATED n s))
\end{verbatim}\end{hol}

\noindent There are a large collection of pre-proved theorems in this theory, a few of
which are given below.
\begin{hol}
\index{APPEND\_CLAUSES@{\ptt APPEND\_CLAUSES}}
\index{APPEND\_IS\_NULL@{\ptt APPEND\_IS\_NULL}}
\index{CONS\_APPEND\_CONS@{\ptt CONS\_APPEND\_CONS}}
\index{SNOC\_APPEND\_CONS@{\ptt SNOC\_APPEND\_CONS}}
\index{HD\_APPEND\_NULL@{\ptt HD\_APPEND\_NULL}}
\index{REVERSE@{\ptt REVERSE}}
\index{ITERATED\_EMPTY@{\ptt ITERATED\_EMPTY}}
\index{LENGTH\_REPLICATE@{\ptt LENGTH\_REPLICATE}}
\begin{verbatim}
  APPEND_CLAUSES  |- (!l. APPEND[]l = l) /\
                     (!l1. APPEND l1[] = l1) /\
                     (!l1 l2 h. APPEND(CONS h l1)l2 = CONS h(APPEND l1 l2)) /\
                     (!d l1 l2. APPEND l1(SNOC d l2) = SNOC d(APPEND l1 l2))

  APPEND_IS_NULL    |- !l1 l2. NULL(APPEND l1 l2) = NULL l1 /\ NULL l2

  CONS_APPEND_CONS  |- !a l. CONS a l = APPEND[a]l

  SNOC_APPEND_CONS  |- !l h. SNOC h l = APPEND l[h]

  HD_APPEND_NULL    |- !l1. ~NULL l1 ==> (!l2. HD(APPEND l1 l2) = HD l1)

  REVERSE           |- (REVERSE[] = []) /\
                       (!h t. REVERSE(CONS h t) = APPEND(REVERSE t)[h])

  ITERATED_EMPTY    |- !n. ITERATED n[] = []

  LENGTH_REPLICATE  |- !x n. LENGTH(REPLICATE n x) = n
\end{verbatim}\end{hol}

A similar tactic to 
\ml{SNOC\_INDUCT\_TAC}\index{SNOC\_INDUCT_TAC@{\ptt SNOC\_INDUCT\_TAC}},
\ml{LIST\_APPEND\_INDUCT\_TAC}\index{LIST\_APPEND\_INDUCT\_TAC@{\ptt LIST\_APPEND\_INDUCT\_TAC}}  is
provided  which uses \ml{APPEND} to access the tail of the list rather than
\ml{SNOC}.   If this tactic is applied to the goal 

\begin{hol}\begin{verbatim}
  ?- !(l:* list). P l
\end{verbatim}\end{hol}

\noindent it will yield the following subgoals:

\begin{hol}\begin{verbatim}
  ?- P[]

  P l ?- !h. P(APPEND l [h])
\end{verbatim}\end{hol}

\noindent See the documentation of the function  in
Chapter \ref{entries} for more details. 

\noindent 