listLib.MAP

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.