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
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
|
\DOC IN_CONV
\TYPE {IN_CONV : conv -> conv}
\SYNOPSIS
Decision procedure for membership in finite sets.
\LIBRARY sets
\DESCRIBE
The function {IN_CONV} is a parameterized conversion for proving or disproving
membership assertions of the general form:
{
"t IN {{t1,...,tn}}"
}
\noindent where {{{t1,...,tn}}} is a set of type {(ty)set} and {t} is a value
of the base type {ty}. The first argument to {IN_CONV} is expected to be a
conversion that decides equality between values of the base type {ty}. Given
an equation {"e1 = e2"}, where {e1} and {e2} are terms of type {ty}, this
conversion should return the theorem {|- (e1 = e2) = T} or the theorem
{|- (e1 = e2) = F}, as appropriate.
Given such a conversion, the function {IN_CONV} returns a conversion that
maps a term of the form {"t IN {{t1,...,tn}}"} to the theorem
{
|- t IN {{t1,...,tn}} = T
}
\noindent if {t} is alpha-equivalent to any {ti}, or if the supplied conversion
proves {|- (t = ti) = T} for any {ti}. If the supplied conversion proves
{|- (t = ti) = F} for every {ti}, then the result is the theorem
{
|- t IN {{t1,...,tn}} = F
}
\noindent In all other cases, {IN_CONV} will fail.
\EXAMPLE
In the following example, the conversion {num_EQ_CONV} is supplied as a
parameter and used to test equality of the candidate element {1} with the
actual elements of the given set.
{
#IN_CONV num_EQ_CONV "2 IN {{0,SUC 1,3}}";;
|- 2 IN {{0,SUC 1,3}} = T
}
\noindent The result is {T} because {num_EQ_CONV} is able to prove that {2} is
equal to {SUC 1}. An example of a negative result is:
{
#IN_CONV num_EQ_CONV "1 IN {{0,2,3}}";;
|- 1 IN {{0,2,3}} = F
}
\noindent Finally the behaviour of the supplied conversion is irrelevant when
the value to be tested for membership is alpha-equivalent to an actual element:
{
#IN_CONV NO_CONV "1 IN {{3,2,1}}";;
|- 1 IN {{3,2,1}} = T
}
\noindent The conversion {NO_CONV} always fails, but {IN_CONV} is nontheless
able in this case to prove the required result.
\FAILURE
{IN_CONV conv} fails if applied to a term that is not of the form {"t IN
{{t1,...,tn}}"}. A call {IN_CONV conv "t IN {{t1,...,tn}}"} fails unless the
term {t} is alpha-equivalent to some {ti}, or {conv "t = ti"} returns
{|- (t = ti) = T} for some {ti}, or {conv "t = ti"} returns
{|- (t = ti) = F} for every {ti}.
\ENDDOC
|
