MAP_CONV : conv -> conv
STRUCTURE
SYNOPSIS
Compute the result of mapping a function down a list.
DESCRIPTION
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.
HOL  Kananaskis-10