\section{The Theory {\tt unappend}}

The theory \ml{unappend}\index{unappend, theory@{\ptt unappend}, theory} deals with the
operators  
\ml{UNAPPEND\_LEFT}\index{UNAPPEND\_LEFT@{\ptt UNAPPEND\_LEFT}} and
\ml{UNAPPEND\_RIGHT}\index{UNAPPEND\_RIGHT@{\ptt UNAPPEND\_RIGHT}}.
The operator \ml{UNAPPEND\_LEFT} removes a given initial sublist 
from the front of a list. It returns the empty list if the first list is not an
initial sublist of the second.  \ml{UNAPPEND\_RIGHT} is similar, removing a
given final sublist from the tail end of a list.


\[ \begin{array}[t]{@{}l@{}l}
  \ml{UNAPPEND\_LEFT}\;  \ml{[}a_1\listsep a_n\ml{]}
                   \ml{[}a_1\listsep a_n \lsep b_1 \listsep b_m\ml{]}=
                                         \ml{[}b_1\listsep b_m\ml{]} 
 \end{array}
\]

\[ \begin{array}[t]{@{}l@{}l}
  \ml{UNAPPEND\_RIGHT}\;  \ml{[}b_1\listsep b_m\ml{]}
                   \ml{[}a_1\listsep a_n \lsep b_1 \listsep b_m\ml{]}=
                                         \ml{[}a_1\listsep a_n\ml{]} 
 \end{array}
\]


\noindent They are defined by  \HOL\ specifications.


\begin{hol}
\index{UNAPPEND\_LEFT@{\ptt UNAPPEND\_LEFT}}
\index{UNAPPEND\_RIGHT@{\ptt UNAPPEND\_RIGHT}}
\begin{verbatim}
  UNAPPEND_LEFT   |- !l1 l2. UNAPPEND_LEFT l1 (APPEND l1 l2) = l2
  UNAPPEND_RIGHT  |- !l1 l2. UNAPPEND_RIGHT l2 (APPEND l1 l2) = l1
\end{verbatim}\end{hol}

\noindent A sample of the theorems contained in this theory is given below.

\begin{hol}
\index{NULL\_UNAPPEND\_LEFT@{\ptt NULL\_UNAPPEND\_LEFT}}
\index{UNAPPEND\_RIGHT\_NIL@{\ptt UNAPPEND\_RIGHT\_NIL}}
\index{APPEND\_UNAPPEND\_LEFT\_ID@{\ptt APPEND\_UNAPPEND\_LEFT\_ID}}
\index{LLESS\_LEFT\_APPEND\_UNAPPEND\_LEFT@{\ptt LLESS\_LEFT\_APPEND\_UNAPPEND\_LEFT}}
\index{LLEQ\_RIGHT\_APPEND\_UNAPPEND\_RIGHT@{\ptt LLEQ\_RIGHT\_APPEND\_UNAPPEND\_RIGHT}}
\begin{verbatim}
  NULL_UNAPPEND_LEFT       |- !l. NULL(UNAPPEND_LEFT l l)

  UNAPPEND_RIGHT_NIL       |- !l. UNAPPEND_RIGHT[]l = l

  APPEND_UNAPPEND_LEFT_ID  |- !l. l = APPEND l(UNAPPEND_LEFT l l)

  LLESS_LEFT_APPEND_UNAPPEND_LEFT
       |- !l1 l2. l1 LLESS_LEFT l2 ==> (l2 = APPEND l1(UNAPPEND_LEFT l1 l2))

  LLEQ_RIGHT_APPEND_UNAPPEND_RIGHT
       |- !l1 l2. l1 LLEQ_RIGHT l2 ==> (l2 = APPEND (UNAPPEND_RIGHT l1 l2) l1)
\end{verbatim}\end{hol}
