IMAGE_CONV

pred_setLib.IMAGE_CONV : conv -> conv -> conv

Compute the image of a function on a finite set.

The function IMAGE_CONV is a parameterized conversion for computing the image of a function f:ty1->ty2 on a finite set {t1;...;tn} of type ty1->bool. The first argument to IMAGE_CONV is expected to be a conversion that computes the result of applying the function f to each element of this set. 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. This conversion is used by IMAGE_CONV to compute a theorem of the form

   |- IMAGE f {t1;...;tn} = {r1;...;rn}

The second argument to IMAGE_CONV is used (optionally) to simplify the resulting image set {r1;...;rn} by removing redundant occurrences of values. This conversion expected to decide equality of values of the result type ty2; given an equation e1 = e2, where e1 and e2 are terms of type ty2, the conversion should return either |- (e1 = e2) = T or |- (e1 = e2) = F, as appropriate.

Given appropriate conversions conv1 and conv2, the function IMAGE_CONV returns a conversion that maps a term of the form IMAGE f {t1;...;tn} to the theorem

   |- IMAGE f {t1;...;tn} = {rj;...;rk}

where conv1 proves a theorem of the form |- (f ti) = ri for each element ti of the set {t1;...;tn}, and where the set {rj;...;rk} is the smallest subset of {r1;...;rn} such no two elements are alpha-equivalent and conv2 does not map rl = rm to the theorem |- (rl = rm) = T for any pair of values rl and rm in {rj;...;rk}. That is, {rj;...;rk} is the set obtained by removing multiple occurrences of values from the set {r1;...;rn}, where the equality conversion conv2 (or alpha-equivalence) is used to determine which pairs of terms in {r1;...;rn} are equal.

Example

The following is a very simple example in which REFL is used to construct the result of applying the function f to each element of the set {1; 2; 1; 4}, and NO_CONV is the supplied ‘equality conversion’.

   - IMAGE_CONV REFL NO_CONV ``IMAGE (f:num->num) {1; 2; 1; 4}``;
   > val it = |- IMAGE f {1; 2; 1; 4} = {f 2; f 1; f 4} : thm

The result contains only one occurrence of f 1, even though NO_CONV always fails, since IMAGE_CONV simplifies the resulting set by removing elements that are redundant up to alpha-equivalence.

For the next example, we 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 open numLib Arbnum
          val n = dest_numeral (rand tm)
          val sucn = mk_numeral (n + one)
      in
        SYM (num_CONV sucn)
      end;

   > val SUC_CONV = fn : term -> thm

The result is a conversion that inverts num_CONV:

   - numLib.num_CONV ``4``;
   > val it = |- 4 = SUC 3 : thm

   - SUC_CONV ``SUC 3``;
   > val it = |- SUC 3 = 4 : thm

The conversion SUC_CONV can then be used to compute the image of the successor function on a finite set:

   - IMAGE_CONV SUC_CONV NO_CONV ``IMAGE SUC {1; 2; 1; 4}``;
   > val it = |- IMAGE SUC {1; 2; 1; 4} = {3; 2; 5} : thm

Note that 2 (= SUC 1) appears only once in the resulting set.

Finally, here is an example of using IMAGE_CONV to compute the image of a paired addition function on a set of pairs of numbers:

   - IMAGE_CONV (pairLib.PAIRED_BETA_CONV THENC reduceLib.ADD_CONV)
                numLib.REDUCE_CONV
            ``IMAGE (\(n,m).n+m) {{(1,2), (3,4), (0,3), (1,3)}}``;
   > val it = |- IMAGE (\(n,m). n + m) {(1,2); (3,4); (0,3); (1,3)} = {7; 3; 4}

Failure

IMAGE_CONV conv1 conv2 fails if applied to a term not of the form IMAGE f {t1;...;tn}. An application of IMAGE_CONV conv1 conv2 to a term IMAGE f {t1;...;tn} fails unless for all ti in the set {t1;...;tn}, evaluating conv1 ``f ti`` returns |- (f ti) = ri for some ri.