FILTER_CONV : conv -> conv

- STRUCTURE
- SYNOPSIS
- Computes by inference the result of applying a predicate to the elements of a list.
- DESCRIPTION
- FILTER_CONV takes a conversion conv and a term tm in the following form:It returns the theorem
FILTER P [x0;...xn]

where for every xi occurring in the right-hand side of the resulting theorem, conv “P xi” returns a theorem |- P xi = T.|- FILTER P [x0;...xn] = [...xi...]

- FAILURE
- FILTER_CONV conv tm fails if tm is not of the form described above.
- EXAMPLE
- Evaluatingreturns the following theorem:
FILTER_CONV bool_EQ_CONV “FILTER ($= T) [T;F;T]”;

In general, if the predicate P is an explicit lambda abstraction (\x. P x), the conversion should be in the form|- FILTER($= T)[T;F;T] = [T;T]

(BETA_CONV THENC conv')

- SEEALSO

HOL Kananaskis-14