\section{The Theory {\tt snoc}}

The theory \ml{snoc}\index{snoc, theory@{\ptt snoc}, theory} introduces operators for 
accessing the tail end of a list.
For problems which naturally use both ends of a list, proofs can
be simplified considerably using this theory.
The operators \ml{SNOC}\index{SNOC@{\ptt SNOC}}, \ml{LAST}\index{LAST@{\ptt LAST}}
and \ml{BUTLAST}\index{BUTLAST@{\ptt BUTLAST}} 
are equivalent to \ml{CONS}\index{CONS@{\ptt CONS}}, \ml{HD}\index{HD@{\ptt HD}}
and \ml{TL}\index{TL@{\ptt TL}} respectively, except working 
from the tail end of the list rather than the start.
\ml{REVERSE}\index{REVERSE@{\ptt REVERSE}} is also defined, providing a link
between accessing the start and the tail end of a list.
The ability to make recursive definitions and perform induction using
\ml{SNOC} is provided. 

\ml{SNOC} \index{SNOC@{\ptt SNOC}} adds an element to the tail end of a list.
\begin{hol}
\[
\ml{SNOC}\; h \ml{[}a_1\lsep a_2\listsep a_n\ml{]} = \ml{[}a_1\lsep a_2\listsep a_n\lsep h\ml{]}
\]\end{hol}


\noindent It is defined by primitive recursion.

\begin{hol}
\index{SNOC\_DEF@{\ptt SNOC\_DEF}}
\begin{verbatim}
  SNOC_DEF       |- (!d. SNOC d[] = [d]) /\
                    (!d h t. SNOC d(CONS h t) = CONS h(SNOC d t))
\end{verbatim}\end{hol}

\noindent The theorems pre-proved about \ml{SNOC} include:

\begin{hol}
\index{SNOC\_NOT\_NULL@{\ptt SNOC\_NOT\_NULL}}
\index{HD\_SNOC@{\ptt HD\_SNOC}}
\index{TL\_SNOC@{\ptt TL\_SNOC}}
\index{SNOC\_Axiom@{\ptt SNOC\_Axiom}}
\index{SNOC\_INDUCT@{\ptt SNOC\_INDUCT}}
\begin{verbatim}
  SNOC_NOT_NULL  |- !d l. ~NULL(SNOC d l)

  HD_SNOC        |- !h t. HD(SNOC h t) = (NULL t => h | HD t)

  TL_SNOC        |- !h t. TL(SNOC h t) = (NULL t => [] | SNOC h(TL t))

  SNOC_Axiom     |- !x f. ?! fn. (fn[] = x) /\
                                 (!h t. fn(SNOC h t) = f(fn t)h t)

  SNOC_INDUCT    |- !P. P[] /\ (!t. P t ==> (!h. P(SNOC h t))) ==> (!l. P l)
\end{verbatim}\end{hol}

\noindent  The theorem \ml{SNOC\_INDUCT} allows induction to be
performed from the tail end of the list. It is in the correct form for use
with the built-in induction tactic \ml{INDUCT\_THEN}. See the \HOL\ manual for
details of this function.
An associated tactic
\ml{SNOC\_INDUCT\_TAC}\index{SNOC_INDUCT_TAC@{\ptt SNOC\_INDUCT\_TAC}} is
provided.   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 subgoals:

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

  P l ?- !h. P(SNOC h l)
\end{verbatim}\end{hol}

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

The theorem \ml{SNOC\_Axiom} is in the form produced by the type definition
package of the \HOL\ system. The tools provided with the package can therefore
be used. In particular the function
\ml{new\_recursive\_definition} can be used to make recursive definitions
using \ml{SNOC}.
For example, an alternative definition for  the length of the list could be
made as follows:


\begin{session}\begin{verbatim}
#let S_LENGTH =  
   new_recursive_definition false SNOC_Axiom `S_LENGTH`
     "(S_LENGTH NIL = 0) /\
      (!h:*. !t. S_LENGTH (SNOC h t) = SUC (S_LENGTH t))";;
S_LENGTH = |- (S_LENGTH[] = 0) /\ (!h t. S_LENGTH(SNOC h t) = SUC(S_LENGTH t))
\end{verbatim}\end{session}


\ml{LAST} returns the last element of a list and \ml{BUTLAST} returns the
remainder of the list with the last element removed. Both are undefined for
null lists.

\begin{hol}
\[
\ml{LAST [}a_1\listsep a_n\lsep h\ml{]} = h
\]\end{hol}

\begin{hol}
\[
\ml{BUTLAST [}a_1\listsep a_n\lsep h\ml{]} =  \ml{[}a_1\listsep a_n\ml{]}
\]\end{hol}

\noindent They are defined in \HOL\ by

\begin{hol}
\index{LAST\_DEF@{\ptt LAST\_DEF}}
\index{BUTLAST\_DEF@{\ptt BUTLAST\_DEF}}
\begin{verbatim}
  LAST_DEF            |- !l. LAST l = (@h. ?t. SNOC h t = l)

  BUTLAST_DEF         |- !l. BUTLAST l = (@t. SNOC(LAST l)t = l)
\end{verbatim}\end{hol}


 A sample of the theorems pre-proved about \ml{LAST} and \ml{BUTLAST} is given
below.

\begin{hol}
\index{LAST@{\ptt LAST}}
\index{BUTLAST@{\ptt BUTLAST}}
\index{LAST\_CONS@{\ptt LAST\_CONS}}
\index{BUTLAST\_CONS@{\ptt BUTLAST\_CONS}}
\index{LAST\_EL@{\ptt LAST\_EL}}
\begin{verbatim}
  LAST                |- !h t. LAST(SNOC h t) = h

  BUTLAST             |- !h t. BUTLAST(SNOC h t) = t

  LAST_CONS           |- !h t. LAST(CONS h t) = (NULL t => h | LAST t)

  BUTLAST_CONS        |- !h t. BUTLAST(CONS h t) =
                                  (NULL t => [] | CONS h(BUTLAST t))

  LAST_EL             |- !a. LAST[a] = a
\end{verbatim}\end{hol}

\ml{REVERSE} reverses the elements in a list.

\begin{hol}
\[
   \ml{REVERSE [}a_1\listsep a_n\ml{]} =  \ml{[}a_n\listsep a_1\ml{]}
\]\end{hol}

\noindent It is defined by

\begin{hol}
\index{REVERSE\_DEF@{\ptt REVERSE\_DEF}}
\begin{verbatim}
  REVERSE_DEF         |- (REVERSE[] = []) /\
                         (!h l. REVERSE(CONS h l) = SNOC h(REVERSE l))
\end{verbatim}\end{hol}

\noindent Pre-proved theorems about \ml{REVERSE} include

\begin{hol}
\index{REVERSE\_CLAUSES@{\ptt REVERSE\_CLAUSES}}
\index{REVERSE\_SINGLE@{\ptt REVERSE\_SINGLE}}
\index{REVERSE\_NULL@{\ptt REVERSE\_NULL}}
\index{LENGTH\_REVERSE@{\ptt LENGTH\_REVERSE}}
\begin{verbatim}
  REVERSE_CLAUSES    |- (REVERSE[] = []) /\
                        (!h l. REVERSE(CONS h l) = SNOC h(REVERSE l)) /\
                        (!d l. REVERSE(SNOC d l) = CONS d(REVERSE l)) /\
                        (!l. REVERSE(REVERSE l) = l)

  REVERSE_SINGLE     |- !h. REVERSE[h] = [h]

  REVERSE_NULL       |- !l. NULL(REVERSE l) = NULL l

  LENGTH_REVERSE     |- !l. LENGTH(REVERSE l) = LENGTH l
\end{verbatim}\end{hol}

A conversion
\ml{SUBST\_REVERSE\_CONV}\index{SUBST\_REVERSE\_CONV@{\ptt SUBST\_REVERSE\_CONV}}
is also provided.  
When applied to a term of the form \ml{!x.P x} it returns the theorem:

\begin{hol}\begin{verbatim}
   |- (!x. P x) = (!y. P(REVERSE y))
\end{verbatim}\end{hol}

