\section{The Theory {\tt map}}

The theory \ml{map}\index{map, theory@{\ptt map}, theory} is concerned with higher-order
functions and predicates which act on the elements of a list. Examples which
occur in the theory \ml{list} are \ml{MAP}\index{MAP@{\ptt MAP}} and
\ml{EVERY}\index{EVERY@{\ptt EVERY}}.
Further theorems about these operators are pre-proved in this theory.
Additionally, the operator \ml{ITLIST}\index{ITLIST@{\ptt ITLIST}} is provided.

\begin{hol}
\[
  \ml{ITLIST}\; f \ml{[}a_1 \lsep a_2 \listsep a_n\ml{]}\; x = 
       f\; a_1\; (f\; a_2\; (\; \ldots\; f\; a_n\; x)\;\ldots\;)
\]\end{hol}

\noindent Its definition is

\begin{hol}
\index{ITLIST@{\ptt ITLIST}}
\begin{verbatim}
  ITLIST    |- (!f x. ITLIST f[]x = x) /\
               (!f hd tl x. ITLIST f(CONS hd tl)x = f hd(ITLIST f tl x))
\end{verbatim}\end{hol}

\noindent Theorems about \ml{MAP}, \ml{EVERY}, and \ml{ITLIST} which are
pre-proved include 

\begin{hol}
\index{MAP\_MAP\_o@{\ptt MAP\_MAP\_o}}
\index{EVERY\_MAP@{\ptt EVERY\_MAP}}
\index{HD\_MAP@{\ptt HD\_MAP}}
\index{TL\_MAP@{\ptt TL\_MAP}}
\index{ITLIST\_MAP@{\ptt ITLIST\_MAP}}
\begin{verbatim}
  MAP_MAP_o      |- !f g l. MAP f(MAP g l) = MAP(f o g)l

  EVERY_MAP      |- !f P l. EVERY P(MAP f l) = EVERY(P o f)l

  HD_MAP         |- !f l. ~NULL l ==> (HD(MAP f l) = f(HD l))

  TL_MAP         |- !f l. ~NULL l ==> (TL(MAP f l) = MAP f(TL l))

  ITLIST_MAP     |- !l. ITLIST p(MAP f l) = ITLIST(\x y. p(f x)y)l
\end{verbatim}\end{hol}
