\chapter{ML Functions in the more\_lists Library}\label{entries}
\input{entries-intro}
\DOC{BUTLAST\_CONV}

\TYPE {\small\verb%BUTLAST_CONV : conv%}\egroup

\SYNOPSIS
Computes by inference the result of stripping the last element of a list.

\DESCRIBE
For any object language list of the form {\small\verb%"[x0;...x(n-1)]"%} ,
the result of evaluating
{\par\samepage\setseps\small\begin{verbatim}
   BUTLAST_CONV "BUTLAST [x0;...;x(n-1)]"
\end{verbatim}}
\noindent is the theorem
{\par\samepage\setseps\small\begin{verbatim}
   |- BUTLAST [x0;...;x(n-1)] = [x0;...; x(n-2)]
\end{verbatim}}


\FAILURE
{\small\verb%BUTLAST_CONV tm%} fails if {\small\verb%tm%} is not a non-null list.

\ENDDOC

\DOC{ELL\_CONV}

\TYPE {\small\verb%ELL_CONV : conv%}\egroup

\SYNOPSIS
Computes by inference the result of taking an element of a list.

\DESCRIBE
For any object language list of the form {\small\verb%"[x1;...;xk;...xn]"%} ,
the result of evaluating
{\par\samepage\setseps\small\begin{verbatim}
   ELL_CONV "ELL k [x1;...;xk;...;xn]"
\end{verbatim}}
\noindent is the theorem
{\par\samepage\setseps\small\begin{verbatim}
   |- ELL k [x1;...;xk;...;xn] = xk
\end{verbatim}}
\noindent where {\small\verb%k%} must not be greater then the length of the list.
Note that {\small\verb%ELL%} index the list elements from {\small\verb%1%}.

\FAILURE
{\small\verb%ELL_CONV tm%} fails if {\small\verb%tm%} is not of the form described above, 
or {\small\verb%k%} is greater than the length of the list.

\SEEALSO
EL_CONV

\ENDDOC

\DOC{EL\_CONV}

\TYPE {\small\verb%EL_CONV : conv%}\egroup

\SYNOPSIS
Computes by inference the result of taking an element from a list.

\DESCRIBE
For any object language list of the form {\small\verb%"[x0;...xk;...;xn]"%} ,
the result of evaluating
{\par\samepage\setseps\small\begin{verbatim}
   EL_CONV "EL k [x0;...xk;...;xn]"
\end{verbatim}}
\noindent is the theorem
{\par\samepage\setseps\small\begin{verbatim}
   |- EL k [x0;...;xk;...;xn] = xk
\end{verbatim}}


\FAILURE
{\small\verb%EL_CONV tm%} fails if {\small\verb%tm%} is not of the form described above, 
or {\small\verb%k%} is not less than the length of the list.

\SEEALSO
ELL_CONV

\ENDDOC

\DOC{EQ\_LENGTH\_INDUCT\_TAC}

\TYPE {\small\verb%EQ_LENGTH_INDUCT_TAC : tactic%}\egroup

\SYNOPSIS
Performs tactical proof by structural induction on two equal length lists.

\DESCRIBE
{\small\verb%EQ_LENGTH_INDUCT_TAC%} reduces a goal
 {\small\verb%!x y . (LENGTH x = LENGTH y) ==> t[x,y]%},
 where {\small\verb%x%} and {\small\verb%y%} range over lists, to two
subgoals corresponding to the base and step cases in a proof by 
induction on the length of {\small\verb%x%} and {\small\verb%y%}. The induction hypothesis appears among
the assumptions of the
subgoal for the step case.  The specification of {\small\verb%EQ_LENGTH_INDUCT_TAC%} is:
{\par\samepage\setseps\small\begin{verbatim}
         A ?- !x y . (LENGTH x = LENGTH y) ==> t[x,y]
   ====================================================  EQ_LENGTH_INDUCT_TAC
                            A ?- t[NIL/x][NIL/y]
    A u {LENGTH x = LENGTH y, t[x'/x, y'/y]} ?- 
         !h h'. t[(CONS h x)/x, (CONS h' y)/y]
\end{verbatim}}

\FAILURE
{\small\verb%EQ_LENGTH_INDUCT_TAC g%} fails unless the conclusion of the goal {\small\verb%g%} has the
 form 
{\par\samepage\setseps\small\begin{verbatim}
   !x y . (LENGTH x = LENGTH y) ==> t[x,y]
\end{verbatim}}
\noindent  where the variables {\small\verb%x%} and {\small\verb%y%}
 have types {\small\verb%(xty)list%} and {\small\verb%(yty)list%} for some types {\small\verb%xty%} and {\small\verb%yty%}.
 It also fails if either of the variables {\small\verb%x%} or {\small\verb%y%} appear free in the
 assumptions. 

\USES
use this tactic when  structural induction is performed on two lists and
they have identical length.

\SEEALSO
LIST_APPEND_INDUCT_TAC, LIST_INDUCT_TAC, SNOC_INDUCT_TAC,
LENGTH_LIST_INDUCT_TAC, EQ_LENGTH_SNOC_INDUCT_TAC.

\ENDDOC
\DOC{EQ\_LENGTH\_SNOC\_INDUCT\_TAC}

\TYPE {\small\verb%EQ_LENGTH_SNOC_INDUCT_TAC : tactic%}\egroup

\SYNOPSIS
Performs tactical proof by structural induction on two equal length
lists from the tail end.

\DESCRIBE
{\small\verb%EQ_LENGTH_SNOC_INDUCT_TAC%} reduces a goal
 {\small\verb%!x y . (LENGTH x = LENGTH y) ==> t[x,y]%},
 where {\small\verb%x%} and {\small\verb%y%} range over lists, to two
subgoals corresponding to the base and step cases in a proof by 
induction on the length of {\small\verb%x%} and {\small\verb%y%}. The induction hypothesis appears among
the assumptions of the
subgoal for the step case.  The specification of {\small\verb%EQ_LENGTH_SNOC_INDUCT_TAC%} is:
{\par\samepage\setseps\small\begin{verbatim}
     A ?- !x y . (LENGTH x = LENGTH y) ==> t[x,y]
   ================================================  EQ_LENGTH_SNOC_INDUCT_TAC
                            A ?- t[NIL/x][NIL/y]
    A u {LENGTH x = LENGTH y, t[x'/x, y'/y]} ?- 
         !h h'. t[(SNOC h x)/x, (SNOC h' y)/y]
\end{verbatim}}

\FAILURE
{\small\verb%EQ_LENGTH_SNOC_INDUCT_TAC g%} fails unless the conclusion of the goal {\small\verb%g%} has the
 form 
{\par\samepage\setseps\small\begin{verbatim}
   !x y . (LENGTH x = LENGTH y) ==> t[x,y]
\end{verbatim}}
\noindent  where the variables {\small\verb%x%} and {\small\verb%y%}
 have types {\small\verb%(xty)list%} and {\small\verb%(yty)list%} for some types {\small\verb%xty%} and {\small\verb%yty%}.
 It also fails if either of the variables {\small\verb%x%} or {\small\verb%y%} appear free in the
 assumptions. 

\USES
use this tactic when  structural induction is performed on two lists and
they have identical length.

\SEEALSO
LIST_APPEND_INDUCT_TAC, LIST_INDUCT_TAC, SNOC_INDUCT_TAC,
LENGTH_LIST_INDUCT_TAC, EQ_LENGTH_INDUCT_TAC

\ENDDOC
\DOC{LASTN\_CONV}

\TYPE {\small\verb%LASTN_CONV : conv%}\egroup

\SYNOPSIS
Computes by inference the result of taking the last n elements of a list.

\DESCRIBE
For any object language list of the form {\small\verb%"[x0;...x(n-k);...;x(n-1)]"%} ,
the result of evaluating
{\par\samepage\setseps\small\begin{verbatim}
   LASTN_CONV "LASTN k [x0;...x(n-k);...;x(n-1)]"
\end{verbatim}}
\noindent is the theorem
{\par\samepage\setseps\small\begin{verbatim}
   |- LASTN k [x0;...;x(n-k);...;x(n-1)] = [x(n-k);...;x(n-1)]
\end{verbatim}}


\FAILURE
{\small\verb%LASTN_CONV tm%} fails if {\small\verb%tm%} is not of the form described above, 
or {\small\verb%k%} is greater than the length of the list.

\ENDDOC

\DOC{LAST\_CONV}

\TYPE {\small\verb%LAST_CONV : conv%}\egroup

\SYNOPSIS
Computes by inference the result of taking the last element of a list.

\DESCRIBE
For any object language list of the form {\small\verb%"[x0;...x(n-1)]"%} ,
the result of evaluating
{\par\samepage\setseps\small\begin{verbatim}
   LAST_CONV "LAST [x0;...;x(n-1)]"
\end{verbatim}}
\noindent is the theorem
{\par\samepage\setseps\small\begin{verbatim}
   |- LAST [x0;...;x(n-1)] = x(n-1)
\end{verbatim}}


\FAILURE
{\small\verb%LAST_CONV tm%} fails if {\small\verb%tm%} is not a non-null list.

\ENDDOC

\DOC{LENGTH\_LIST\_INDUCT\_TAC}

\TYPE {\small\verb%LENGTH_LIST_INDUCT_TAC : tactic%}\egroup

\SYNOPSIS
Performs tactical proof by structural induction on the length of lists.

\DESCRIBE
{\small\verb%LENGTH_LIST_INDUCT_TAC%} reduces a goal
 {\small\verb%!x y . (LENGTH x = LENGTH y) ==> P%},
 where {\small\verb%x%} and {\small\verb%y%} range over lists, to two
subgoals corresponding to the base and step cases in a proof by 
induction on the length of {\small\verb%x%} and {\small\verb%y%}. The induction hypothesis appears among
the assumptions of the
subgoal for the step case.  The specification of {\small\verb%LENGTH_LIST_INDUCT_TAC%} is:
{\par\samepage\setseps\small\begin{verbatim}
         A ?- !x y . (LENGTH x = LENGTH y) ==> P
   ====================================================  LENGTH_LIST_INDUCT_TAC
                            A ?- P[NIL/x][NIL/y]
    A u {P[TL x/x][TL y/y]} ?- 
         P[(CONS(HD x)(TL x))/x][(CONS(HD y)(TL y))/y]
\end{verbatim}}
\noindent When {\small\verb%LENGTH_LIST_INDUCT_TAC%} is
applied to a goal of the form
{\par\samepage\setseps\small\begin{verbatim}
   !x y . (LENGTH x = LENGTH y) ==> P
\end{verbatim}}
\noindent  where {\small\verb%x%} does not appear free in {\small\verb%P%}, 
the subgoals generated are just  {\small\verb%A ?- P[NIL/x]%} and
 {\small\verb%A u {P[TL x/x]} ?- P[CONS(HD x)(TL x)/x]%}. Similar subgoals are generated
if  {\small\verb%y%} does not appear free in {\small\verb%P%}. If neither {\small\verb%x%} nor {\small\verb%y%} appear free the
goal is unchanged.

\FAILURE
{\small\verb%LENGTH_LIST_INDUCT_TAC g%} fails unless the conclusion of the goal {\small\verb%g%} has the
 form 
{\par\samepage\setseps\small\begin{verbatim}
   !x y . (LENGTH x = LENGTH y) ==> P
\end{verbatim}}
\noindent  where the variables {\small\verb%x%} and {\small\verb%y%}
 have types {\small\verb%(xty)list%} and {\small\verb%(yty)list%} for some types {\small\verb%xty%} and {\small\verb%yty%}.
 It also fails if either of the variables {\small\verb%x%} or {\small\verb%y%} appear free in the
 assumptions. 

\SEEALSO
LIST_APPEND_INDUCT_TAC, LIST_INDUCT_TAC, SNOC_INDUCT_TAC.

\ENDDOC
\DOC{LIST\_APPEND\_INDUCT\_TAC}

\TYPE {\small\verb%LIST_APPEND_INDUCT_TAC : tactic%}\egroup

\SYNOPSIS
Performs tactical proof by structural induction on lists from the tail end
using {\small\verb%APPEND%}.

\DESCRIBE
{\small\verb%LIST_APPEND_INDUCT_TAC%} reduces a goal {\small\verb%!l.P%}, where {\small\verb%l%} ranges over lists,
to two
subgoals corresponding to the base and step cases in a proof by structural
induction on {\small\verb%l%} from the tail end using {\small\verb%APPEND%}. The induction hypothesis
appears among the assumptions of the
subgoal for the step case.  The specification of {\small\verb%LIST_APPEND_INDUCT_TAC%} is:
{\par\samepage\setseps\small\begin{verbatim}
                       A ?- !l. P
   ==================================================  LIST_APPEND_INDUCT_TAC
                  A ?- P[NIL/l]
    A u {P[l'/l]} ?- !h. P[APPEND l' (CONS h NIL)/l]
\end{verbatim}}
\noindent where {\small\verb%l'%} is a primed variant of {\small\verb%l%} that does not appear free in
the assumptions {\small\verb%A%} (usually, {\small\verb%l'%} is just {\small\verb%l%}). When {\small\verb%LIST_APPEND_INDUCT_TAC%} is
applied to a goal of the form {\small\verb%!l.P%}, where {\small\verb%l%} does not appear free in {\small\verb%P%},
the subgoals are just {\small\verb%A ?- P%} and {\small\verb%A u {P} ?- !h.P%}.

\FAILURE
{\small\verb%LIST_APPEND_INDUCT_TAC g%} fails unless the conclusion of the goal {\small\verb%g%} has the form
{\small\verb%!l.t%}, where the variable {\small\verb%l%} has type {\small\verb%(ty)list%} for some type {\small\verb%ty%}.

\SEEALSO
LENGTH_LIST_INDUCT_TAC, LIST_INDUCT_TAC, SNOC_INDUCT_TAC.

\ENDDOC
\DOC{MAP2\_CONV}

\TYPE {\small\verb%MAP2_CONV : conv -> conv%}\egroup

\SYNOPSIS
Compute the result of mapping a binary function down two lists.

\DESCRIBE 
The function {\small\verb%MAP2_CONV%} is a parameterized conversion for computing the result
of mapping a binary function {\small\verb%f:ty1->ty2->ty3%} down two lists
{\small\verb%"[l11;...;l1n]"%} whose elements are of type {\small\verb%ty1%} and
{\small\verb%"[l21;...;l2n]"%} whose elements are of type {\small\verb%ty2%}.  The lengths of
the two lists must be identical. The first
argument to {\small\verb%MAP2_CONV%} is expected to be a conversion 
that computes the result of applying the function {\small\verb%f%} to a pair of
corresponding elements of these lists. When applied to a term
{\small\verb%"f l1i l2i"%}, this conversion should return a theorem of the form
{\small\verb%|- (f l1i l2i) = ri%}, where {\small\verb%ri%} is the result of applying the function
{\small\verb%f%} to the elements {\small\verb%l1i%} and {\small\verb%l2i%}. 

\noindent Given an appropriate {\small\verb%conv%}, the conversion {\small\verb%MAP2_CONV conv%} takes a
term of the form {\small\verb%"[MAP2 f [l11;...;dl2tn] [l21;...;l2n]"%} to the theorem
{\par\samepage\setseps\small\begin{verbatim}
   |- MAP2 f [l11;...;l1n] [l21;...;l2n] = [r1;...;rn] 
\end{verbatim}}
\noindent where {\small\verb%conv "f l1i l2i"%} returns {\small\verb%|- (f l1i l2i) = ri%} for
{\small\verb%i%} from {\small\verb%1%} to {\small\verb%n%}. 

\EXAMPLE

The following is a very simple example in which the corresponding
elements from the two lists are summed to form the resulting list:
{\par\samepage\setseps\small\begin{verbatim}
   #MAP2_CONV ADD_CONV "MAP2 $+ [1;2;3] [1;2;3]";;
   |- MAP2 $+ [1;2;3] [1;2;3] = [2;4;6]
\end{verbatim}}

\FAILURE 
{\small\verb%MAP2_CONV conv%} fails if applied to a term not of the form
described above.  An application of {\small\verb%MAP2_CONV conv%} to a term
{\small\verb%"MAP2 f [l11;...;l1n] [l21;...;l2n]"%} fails unless for all {\small\verb%i%} where {\small\verb%1<=i<=n%}
evaluating {\small\verb%conv "f l1i l2i"%} returns {\small\verb%|- (f l1i l2i) = ri%} for some {\small\verb%ri%}.

\SEEALSO
MAP_CONV

\ENDDOC

\DOC{NBUTLAST\_CONV}

\TYPE {\small\verb%NBUTLAST_CONV : conv%}\egroup

\SYNOPSIS
Computes by inference the result of taking the initial segment of a list.

\DESCRIBE
For any object language list of the form {\small\verb%"[x0;...x(n-k);...;x(n-1)]"%} ,
the result of evaluating
{\par\samepage\setseps\small\begin{verbatim}
   NBUTLAST_CONV "NBUTLAST k [x0;...x(n-k);...;x(n-1)]"
\end{verbatim}}
\noindent is the theorem
{\par\samepage\setseps\small\begin{verbatim}
   |- NBUTLAST k [x0;...;x(n-k);...;x(n-1)] = [x0;...;x(n-k-1)]
\end{verbatim}}


\FAILURE
{\small\verb%NBUTLAST_CONV tm%} fails if {\small\verb%tm%} is not of the form described above, 
or {\small\verb%k%} is greater than the length of the list.

\ENDDOC

\DOC{SNOC\_CONV}

\TYPE {\small\verb%SNOC_CONV : conv%}\egroup

\SYNOPSIS
Computes by inference the result of adding an element to the end of a list.

\DESCRIBE
For any object language list of the form {\small\verb%"[x0;...;x(n-1)]"%} ,
the result of evaluating
{\par\samepage\setseps\small\begin{verbatim}
   SNOC_CONV "SNOC x [x0;...;x(n-1)]"
\end{verbatim}}
\noindent is the theorem
{\par\samepage\setseps\small\begin{verbatim}
   |- SNOC x [x0;...;x(n-1)] = [x0;...;x(n-1);x]
\end{verbatim}}

\FAILURE
{\small\verb%SNOC_CONV tm%} fails if {\small\verb%tm%} is not of the form described above.

\ENDDOC

\DOC{SNOC\_INDUCT\_TAC}

\TYPE {\small\verb%SNOC_INDUCT_TAC : tactic%}\egroup

\SYNOPSIS
Performs tactical proof by structural induction on lists from the tail end
using {\small\verb%SNOC%}.

\DESCRIBE
{\small\verb%SNOC_INDUCT_TAC%} reduces a goal {\small\verb%!l.P%}, where {\small\verb%l%} ranges over lists, to two
subgoals corresponding to the base and step cases in a proof by structural
induction on {\small\verb%l%} from the tail end using {\small\verb%SNOC%}. The induction hypothesis
appears among the assumptions of the
subgoal for the step case.  The specification of {\small\verb%SNOC_INDUCT_TAC%} is:
{\par\samepage\setseps\small\begin{verbatim}
                         A ?- !l. P
   =====================================================  SNOC_INDUCT_TAC
    A ?- P[NIL/l]   A u {P[l'/l]} ?- !h. P[SNOC h l'/l]
\end{verbatim}}
\noindent where {\small\verb%l'%} is a primed variant of {\small\verb%l%} that does not appear free in
the assumptions {\small\verb%A%} (usually, {\small\verb%l'%} is just {\small\verb%l%}). When {\small\verb%SNOC_INDUCT_TAC%} is
applied to a goal of the form {\small\verb%!l.P%}, where {\small\verb%l%} does not appear free in {\small\verb%P%},
the subgoals are just {\small\verb%A ?- P%} and {\small\verb%A u {P} ?- !h.P%}.

\FAILURE
{\small\verb%SNOC_INDUCT_TAC g%} fails unless the conclusion of the goal {\small\verb%g%} has the form
{\small\verb%!l.t%}, where the variable {\small\verb%l%} has type {\small\verb%(ty)list%} for some type {\small\verb%ty%}.

\SEEALSO
LENGTH_LIST_INDUCT_TAC, LIST_APPEND_INDUCT_TAC, LIST_INDUCT_TAC.

\ENDDOC
\DOC{SPLIT\_CONV}

\TYPE {\small\verb%SPLIT_CONV : conv%}\egroup

\SYNOPSIS
Computes by inference the result of splitting a list into two.

\DESCRIBE
For any object language list of the form {\small\verb%"[x0;...xk;...;xn]"%} ,
the result of evaluating
{\par\samepage\setseps\small\begin{verbatim}
   SPLIT_CONV "SPLIT k [x0;...xk;...;xn]"
\end{verbatim}}
\noindent is the theorem
{\par\samepage\setseps\small\begin{verbatim}
   |- SPLIT k [x0;...;xk;...;xn] = [x0;...;x(k-1)],[xk;...;xn]
\end{verbatim}}


\FAILURE
{\small\verb%SPLIT_CONV tm%} fails if {\small\verb%tm%} is not of the form described above, 
or {\small\verb%k%} is not less than the length of the list.

\ENDDOC

\DOC{SUBST\_REVERSE\_CONV}

\TYPE {\small\verb%SUBST_REVERSE_CONV : conv%}\egroup

\SYNOPSIS
Applies a predicate to the reverse of a list rather than the list.

\DESCRIBE
When applied to a term of the form {\small\verb%"!x. P x"%}, where
{\small\verb%x%} has type {\small\verb%:(ty)list%} for some type {\small\verb%ty%}, the conversion
{\small\verb%SUBST_REVERSE_CONV%} returns the theorem:
{\par\samepage\setseps\small\begin{verbatim}
   |- (!x. P x) = (!y. P(REVERSE y))
\end{verbatim}}

\FAILURE
Fails if applied to a term not of the form {\small\verb%"!x. P x"%}, where
{\small\verb%x%} has type {\small\verb%:(ty)list%} for some type {\small\verb%ty%}.

\ENDDOC
