\section{The Theory {\tt shift}}

The theory {\small\verb%shift%}\index{shift, theory@{\ptt shift}, theory} contains 
definitions concerned with shifting lists in various ways.

\ml{PAD\_RIGHT}\index{PAD\_RIGHT@{\ptt PAD\_RIGHT}} pads a list on the right
(tail end) with a given number of copies of a given element.

\[ \begin{array}[t]{@{}l@{}l}
   \ml{PAD\_RIGHT}\; x\; n\; \ml{[}a_1\listsep a_n\ml{]} =
              \ml{[}a_1\listsep a_n\lsep x \listsep x \ml{]}
 \end{array}
\]

\ml{PAD\_LEFT}\index{PAD\_LEFT@{\ptt PAD\_LEFT}} pads a list on the left (front
end) with a given number of copies of a given element.

\[ \begin{array}[t]{@{}l@{}l}
   \ml{PAD\_LEFT}\; x\; n\; \ml{[}a_1\listsep a_n\ml{]} =
              \ml{[} x \listsep x \lsep a_1\listsep a_n\ml{]}
 \end{array}
\]



\ml{ROTATE1\_RIGHT}\index{ROTATE1\_RIGHT@{\ptt ROTATE1\_RIGHT}} rotates a list
right by one position, the last element of the list becoming the head.

\[ \begin{array}[t]{@{}l@{}l}
   \ml{ROTATE1\_RIGHT} \ml{[}a_1\listsep a_{n-1} \lsep a_n\ml{]} =
              \ml{[}a_n \lsep a_1\listsep a_{n-1}\ml{]}
 \end{array}
\]


\ml{ROTATE1\_LEFT}\index{ROTATE1\_LEFT@{\ptt ROTATE1\_LEFT}} rotates a list  left
by one position, the head of the list becoming the last element.

\[ \begin{array}[t]{@{}l@{}l}
   \ml{ROTATE1\_LEFT} \ml{[}a_1\lsep a_2 \listsep a_n\ml{]} =
              \ml{[}a_2\listsep a_n \lsep a_1\ml{]}
 \end{array}
\]


\ml{ROTATE\_RIGHT}\index{ROTATE\_RIGHT@{\ptt ROTATE\_RIGHT}} rotates a list right
by a given number of positions. 

\[ \begin{array}[t]{@{}l@{}l}
   \ml{ROTATE\_RIGHT}\; k\; \ml{[}a_1\listsep a_{n-1} \lsep a_n\ml{]} =
              \ml{[}a_{n-k-1}\listsep a_n \lsep a_1\listsep a_{n-k}\ml{]}
 \end{array}
\]



\ml{ROTATE\_LEFT}\index{ROTATE\_LEFT@{\ptt ROTATE\_LEFT}} rotates a list  left by
a given number of positions. 

\[ \begin{array}[t]{@{}l@{}l}
   \ml{ROTATE\_LEFT}\; k\; \ml{[}a_1\lsep a_2 \listsep a_n\ml{]} =
              \ml{[}a_{k+1}\listsep a_n \lsep a_1 \listsep a_k\ml{]}
 \end{array}
\]




The \HOL\ definitions are

\begin{hol}
\index{PAD\_LEFT@{\ptt PAD\_LEFT}}
\index{PAD\_RIGHT@{\ptt PAD\_RIGHT}}
\index{ROTATE1\_LEFT@{\ptt ROTATE1\_LEFT}}
\index{ROTATE1\_RIGHT@{\ptt ROTATE1\_RIGHT}}
\index{ROTATE\_LEFT@{\ptt ROTATE\_LEFT}}
\index{ROTATE\_RIGHT@{\ptt ROTATE\_RIGHT}}
\begin{verbatim}
  PAD_LEFT      |- (!x l. PAD_LEFT x 0 l = l) /\
                   (!x n l. PAD_LEFT x(SUC n)l = CONS x(PAD_LEFT x n l))

  PAD_RIGHT     |- (!x l. PAD_RIGHT x 0 l = l) /\
                   (!x n l. PAD_RIGHT x(SUC n)l = SNOC x(PAD_RIGHT x n l))

  ROTATE1_LEFT  |- !l. ROTATE1_LEFT l = SNOC(HD l)(TL l)

  ROTATE1_RIGHT |- !l. ROTATE1_RIGHT l = CONS(LAST l)(BUTLAST l)

  ROTATE_LEFT   |- (!l. ROTATE_LEFT 0 l = l) /\
                   (!n l. ROTATE_LEFT(SUC n)l = ROTATE1_LEFT(ROTATE_LEFT n l))

  ROTATE_RIGHT  |- (!l. ROTATE_RIGHT 0 l = l) /\
                   (!n l. ROTATE_RIGHT(SUC n)l =
                                    ROTATE1_RIGHT(ROTATE_RIGHT n l))
\end{verbatim}\end{hol}

An \adhoc\ collection of elementary  theorems are pre-proved in the
theory {\small\verb%shift%}, some of which are given below.

\begin{hol}
\index{LENGTH\_PAD\_LEFT@{\ptt LENGTH\_PAD\_LEFT}}
\index{LENGTH\_PAD\_RIGHT@{\ptt LENGTH\_PAD\_RIGHT}}
\index{ROTATE1\_LEFT\_CONS@{\ptt ROTATE1\_LEFT\_CONS}}
\index{ROTATE1\_RIGHT\_NIL@{\ptt ROTATE1\_RIGHT\_NIL}}
\index{ROTATE\_LEFT\_EL@{\ptt ROTATE\_LEFT\_EL}}
\index{ROTATE\_RIGHT\_ROTATE\_LEFT@{\ptt ROTATE\_RIGHT\_ROTATE\_LEFT}}
\begin{verbatim}
  LENGTH_PAD_LEFT    |- !l n x. LENGTH(PAD_LEFT x n l) = (LENGTH l) + n

  LENGTH_PAD_RIGHT   |- !l n x. LENGTH(PAD_RIGHT x n l) = (LENGTH l) + n

  ROTATE1_LEFT_CONS  |- !x l. ROTATE1_LEFT(CONS x l) = SNOC x l

  ROTATE1_RIGHT_NIL  |- !l. ~NULL l ==> ~NULL(ROTATE1_RIGHT l)

  ROTATE_LEFT_EL     |- !n x. ROTATE_LEFT n[x] = [x]

  ROTATE_RIGHT_ROTATE_LEFT   |- !n l. ~NULL l ==>
                                         (ROTATE_RIGHT n(ROTATE_LEFT n l) = l)
\end{verbatim}\end{hol}
