MAP2_CONV : conv -> conv
STRUCTURE
listLib
SYNOPSIS
Compute the result of mapping a binary function down two lists.
DESCRIPTION
The function MAP2_CONV is a conversion for computing the result of mapping a binary function f:ty1->ty2->ty3 down two lists “[l11;...;l1n]” whose elements are of type ty1 and “[l21;...;l2n]” whose elements are of type ty2. The lengths of the two lists must be identical. The first argument to MAP2_CONV is expected to be a conversion that computes the result of applying the function f to a pair of corresponding elements of these lists. When applied to a term “f l1i l2i”, this conversion should return a theorem of the form |- (f l1i l2i) = ri, where ri is the result of applying the function f to the elements l1i and l2i.

Given an appropriate conv, the conversion MAP2_CONV conv takes a term of the form “MAP2 f [l11;...;dl2tn] [l21;...;l2n]” and returns the theorem 

   |- MAP2 f [l11;...;l1n] [l21;...;l2n] = [r1;...;rn]
where conv “f l1i l2i” returns |- (f l1i l2i) = ri for i from 1 to 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: 
   - load_library_in_place num_lib;
   - MAP2_CONV Num_lib.ADD_CONV “MAP2 $+ [1;2;3] [1;2;3]”;
   |- MAP2 $+ [1;2;3] [1;2;3] = [2;4;6]
FAILURE
MAP2_CONV conv fails if applied to a term not of the form described above. An application of MAP2_CONV conv to a term “MAP2 f [l11;...;l1n] [l21;...;l2n]” fails unless for all i where 1<=i<=n evaluating conv “f l1i l2i” returns |- (f l1i l2i) = ri for some ri.
SEEALSO
MAP_CONV
HOL  Kananaskis-14