SOME_EL_CONV
listLib.SOME_EL_CONV : conv -> conv
Computes by inference the result of applying a predicate to the elements of a list.
SOME_EL_CONV takes a conversion conv and a term tm of the
following form:
SOME_EL P [x0;...xn]
It returns the theorem
|- SOME_EL P [x0;...xn] = F
if for every xi occurred in the list, conv “P xi” returns a theorem
|- P xi = F, otherwise, if for at least one xi, evaluating
conv “P xi” returns the theorem |- P xi = T, then it returns the
theorem
|- SOME_EL P [x0;...xn] = T
Failure
SOME_EL_CONV conv tm fails if tm is not of the form described above,
or failure occurs when evaluating conv “P xi” for some xi.
Example
Evaluating
SOME_EL_CONV bool_EQ_CONV “SOME_EL ($= T) [T;F;T]”;
returns the following theorem:
|- SOME_EL($= T)[T;F;T] = T
In general, if the predicate P is an explicit lambda abstraction
(\x. P x), the conversion should be in the form
(BETA_CONV THENC conv')
See also
listLib.ALL_EL_CONV,
listLib.IS_EL_CONV,
listLib.FOLDL_CONV,
listLib.FOLDR_CONV,
listLib.list_FOLD_CONV