Applies a pair of conversions to the arguments of a binary operator.
DESCRIPTION
If the conversion c1 maps a term t1 to the theorem |- t1 = t1',
and the conversion c2 maps t2 to |- t2 = t2', then the
conversion FORK_CONV (c1,c2) maps terms of the form f t1 t2 to
theorems of the form |- f t1 t2 = f t1' t2'.
FAILURE
FORK_CONV (c1,c2) t will fail if t is not of the general form
f t1 t2, or if c1 fails when applied to t1, or if c2 fails when
applied to t2, or if c1 or c2 aren’t really conversions, and
thereby fail to return appropriate equational theorems.
EXAMPLE
- FORK_CONV (BETA_CONV,REDUCE_CONV) (Term`(\x. x + 1)y * (10 DIV 3)`);
> val it = |- (\x. x + 1) y * (10 DIV 3) = (y + 1) * 3 : thm