STRIP_BINDER_CONV : term option -> conv -> conv
STRUCTURE
SYNOPSIS
Applies a conversion underneath a binder prefix.
DESCRIPTION
If the application of conv to M yields |- M = N, then STRIP_BINDER_CONV (SOME c) conv (c(\v1. ... (c(\vn.M))...)) returns |- c(\v1. ... (c(\vn.M))...) = c(\v1. ... (c(\vn.N))...) and STRIP_BINDER_CONV NONE conv (\v1 ... vn.M) returns |- (\v1 ... vn.M) = (\v1 ... vn.N).
FAILURE
If conv M fails. Also fails if some of [v1,...,vn] are free in the hypotheses of conv M.
EXAMPLE
- STRIP_BINDER_CONV NONE BETA_CONV (Term `\u v w. (\a. a + v * w) u`);
> val it = |- (\u v w. (\a. a + v * w) u) = (\u v w. u + v * w) : thm

- STRIP_BINDER_CONV (SOME existential) SYM_CONV
                    (Term `?u v w x y. u + v = w + x + y`);
> val it = |- (?u v w x y. u + v = w + x + y) =
               ?u v w x y. w + x + y = u + v : thm
COMMENTS
STRIP_BINDER_CONV is more efficient than iterated application of BINDER_CONV or ABS_CONV or QUANT_CONV.
SEEALSO
HOL  Kananaskis-14