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