1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
|
\DOC SOME_EL_CONV
\TYPE {SOME_EL_CONV : conv -> conv}
\SYNOPSIS
Computes by inference the result of applying a predicate to elements of a list.
\KEYWORDS
conversion, list.
\DESCRIBE
{SOME_EL_CONV} takes a conversion {conv} and a term {tm} in the following form:
{
SOME_EL P [x0;...xn]
}
\noindent It returns the theorem
{
|- SOME_EL P [x0;...xn] = F
}
\noindent 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]";;
}
\noindent returns the following theorem:
{
|- SOME_EL($= T)[T;F;T] = T
}
\noindent 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')
}
\SEEALSO
ALL_EL_CONV, IS_EL_CONV, FOLDL_CONV, FOLDR_CONV, list_FOLD_CONV.
\ENDDOC
|
