STRIP_BINDER_CONV
Conv.STRIP_BINDER_CONV : term option -> conv -> conv
Applies a conversion underneath a binder prefix.
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.
See also
Conv.BINDER_CONV,
Conv.ABS_CONV,
Conv.QUANT_CONV,
Conv.STRIP_BINDER_CONV,
Conv.STRIP_QUANT_CONV