----------------------------------------------------------------------
MAP_CONV                                                     (listLib)
----------------------------------------------------------------------
MAP_CONV : conv -> conv

SYNOPSIS
Compute the result of mapping a function down a list.

KEYWORDS
conversion, list.

DESCRIBE
The function {MAP_CONV} is a parameterized conversion for computing the result
of mapping a function {f:ty1->ty2} down a list {“[t1;...;tn]”} of elements of
type {ty1}.  The first argument to {MAP_CONV} is expected to be a conversion
that computes the result of applying the function {f} to an element of this
list. When applied to a term {“f ti”}, this conversion should return a theorem
of the form {|- (f ti) = ri}, where {ri} is the result of applying the function
{f} to the element {ti}.

Given an appropriate {conv}, the conversion {MAP_CONV conv} takes a
term of the form {“MAP f [t1;...;tn]”} to the theorem

   |- MAP f [t1;...;tn] = [r1;...;rn]

where {conv “f ti”} returns {|- (f ti) = ri} for {i} from {1} to {n}.

EXAMPLE
The following is a very simple example in which no computation is done for
applications of the function being mapped down a list:

   - MAP_CONV ALL_CONV “MAP SUC [1;2;1;4]”;
   |- MAP SUC[1;2;1;4] = [SUC 1;SUC 2;SUC 1;SUC 4]

The result just contains applications of {SUC}, since the supplied
conversion {ALL_CONV} does no evaulation.

We now construct a conversion that maps {SUC n} for any numeral {n} to the
numeral standing for the successor of {n}:

   - fun SUC_CONV tm =
        let val n = string_to_int(#Name(dest_const(rand tm)))
            val sucn = mk_const{{Name =int_to_string(n+1), Ty=(==`:num`==)}}
         in
            SYM (num_CONV sucn)
         end;
   SUC_CONV = - : conv

The result is a conversion that inverts {num_CONV}:

   - num_CONV “4”;
   |- 4 = SUC 3

   - SUC_CONV “SUC 3”;
   |- SUC 3 = 4

The conversion {SUC_CONV} can then be used to compute the
result of mapping the successor function down a list of numerals:

   - MAP_CONV SUC_CONV “MAP SUC [1;2;1;4]”;
   |- MAP SUC[1;2;1;4] = [2;3;2;5]


FAILURE
{MAP_CONV conv} fails if applied to a term not of the form
{“MAP f [t1;...;tn]”}.  An application of {MAP_CONV conv} to a term
{“MAP f [t1;...;tn]”} fails unless for all {ti} in the list {[t1;...;tn]},
evaluating {conv “f ti”} returns {|- (f ti) = ri} for some {ri}.

----------------------------------------------------------------------