\section{The Theory {\tt zip}}

The theory {\small\verb%zip%}\index{zip, theory@{\ptt zip}, theory} contains primitive recursive
definitions for forming a list of pairs from two lists and vice versa.
Given two lists, \ml{ZIP}\index{ZIP@{\ptt ZIP}} pairs corresponding elements to
give a list of pairs. 
If one list is longer than the other the extra elements are discarded.


\[ \begin{array}[t]{@{}l@{}l}
   \ml{ZIP [}a_1\listsep a_n\ml{]}
       \ml{[}b_1\listsep b_m\ml{]} =
       \ml{[(}a_1\ml{,}b_1\ml{)}\listsep\ml{(}a_n\ml{,}b_n\ml{)]} & (n \leq m) \\
   \ml{ZIP [}a_1\listsep a_n\ml{]}
       \ml{[}b_1\listsep b_m\ml{]} =
       \ml{[(}a_1\ml{,}b_1\ml{)}\listsep\ml{(}a_m\ml{,}b_m\ml{)]} & (n > m)
 \end{array}
\]

\noindent Given a list of pairs
\ml{UNZIP\_FST}\index{UNZIP\_FST@{\ptt UNZIP\_FST}} extracts a list of the first 
elements and \ml{UNZIP\_SND}\index{UNZIP\_SND@{\ptt UNZIP\_SND}}  extracts a list
of the second elements. 

\begin{hol}
\[
   \ml{UNZIP\_FST}\ml{[(}a_1\ml{,}b_1\ml{)}\listsep\ml{(}a_n\ml{,}b_n\ml{)]} = \ml{[}a_1\listsep a_n\ml{]}
\]\end{hol}
\begin{hol}
\[
   \ml{UNZIP\_SND}\ml{[(}a_1\ml{,}b_1\ml{)}\listsep\ml{(}a_n\ml{,}b_n\ml{)]} = \ml{[}b_1\listsep b_n\ml{]}
\]\end{hol}

The \HOL\ definitions are

\begin{hol}
\index{ZIP\_DEF@{\ptt ZIP\_DEF}}
\index{UNZIP\_FST@{\ptt UNZIP\_FST}}
\index{UNZIP\_SND@{\ptt UNZIP\_SND}}
\begin{verbatim}
  ZIP_DEF       |- (!l. ZIP l[] = []) /\
                   (!l h t. ZIP l(CONS h t) =
                                (NULL l => [] | CONS(HD l,h)(ZIP(TL l)t)))

  UNZIP_FST     |- (UNZIP_FST[] = []) /\
                   (!h t. UNZIP_FST(CONS h t) = CONS(FST h)(UNZIP_FST t))

  UNZIP_SND     |- (UNZIP_SND[] = []) /\
                   (!h t. UNZIP_SND(CONS h t) = CONS(SND h)(UNZIP_SND t))
\end{verbatim}\end{hol}

A collection of elementary  theorems are pre-proved in the
theory {\small\verb%zip%}.


\begin{hol}
\index{ZIP@{\ptt ZIP}}
\index{ZIP\_CLAUSES@{\ptt ZIP\_CLAUSES}}
\index{ZIP\_UNZIP\_FST\_SND@{\ptt ZIP\_UNZIP\_FST\_SND}}
\index{UNZIP\_FST\_ZIP@{\ptt UNZIP\_FST\_ZIP}}
\index{UNZIP\_SND\_ZIP@{\ptt UNZIP\_SND\_ZIP}}
\index{FST\_SND\_UNZIP\_ZIP@{\ptt FST\_SND\_UNZIP\_ZIP}}
\begin{verbatim}
  ZIP_CLAUSES       |- (!l. ZIP[]l = []) /\
                       (!l. ZIP l[] = []) /\
                       (!h1 t1 h2 t2. ZIP(CONS h1 t1)(CONS h2 t2) =
                                        CONS(h1,h2)(ZIP t1 t2))

  ZIP_UNZIP_FST_SND |- !l. ZIP(UNZIP_FST l)(UNZIP_SND l) = l

  UNZIP_FST_ZIP     |- !l1 l2. (LENGTH l1) <= (LENGTH l2) =
                                         (UNZIP_FST(ZIP l1 l2) = l1)

  UNZIP_SND_ZIP     |- !l1 l2. (LENGTH l2) <= (LENGTH l1) =
                                         (UNZIP_SND(ZIP l1 l2) = l2)

  FST_SND_UNZIP_ZIP |- !l1 l2. (LENGTH l1 = LENGTH l2) =
                                         (UNZIP_FST(ZIP l1 l2) = l1) /\
                                         (UNZIP_SND(ZIP l1 l2) = l2)
\end{verbatim}\end{hol}
